|
|
|---|
|
|
|
|---|
Turn a function environment into a function table.
In formulating the static soundness theorems, we need to relate the ACL2 dynamic execution functions, which take function environments as arguments, with the ACL2 static safety checking functions, which take function tables as arguments: the function tables are the static counterparts of the function environments. This ACL2 function carries out this mapping, by creating function tables for the function scopes and joining them together. It is a run-time invariant that the function scopes in a function environment have disjoint keys; thus, the use of omap::update* is not going to overwrite any mappings. However, we do not need to require this invariant here, as this ACL2 function can be well-defined without it.
Function:
(defun funenv-to-funtable (funenv) (declare (xargs :guard (funenvp funenv))) (let ((__function__ 'funenv-to-funtable)) (declare (ignorable __function__)) (b* (((when (endp funenv)) nil) (funtab-cdr (funenv-to-funtable (cdr funenv))) (funtab-car (funscope-to-funtable (car funenv)))) (omap::update* funtab-car funtab-cdr))))
Theorem:
(defthm funtablep-of-funenv-to-funtable (b* ((funtab (funenv-to-funtable funenv))) (funtablep funtab)) :rule-classes :rewrite)
Theorem:
(defthm funenv-to-funtable-of-funenv-fix-funenv (equal (funenv-to-funtable (funenv-fix funenv)) (funenv-to-funtable funenv)))
Theorem:
(defthm funenv-to-funtable-funenv-equiv-congruence-on-funenv (implies (funenv-equiv funenv funenv-equiv) (equal (funenv-to-funtable funenv) (funenv-to-funtable funenv-equiv))) :rule-classes :congruence)