|
|
|---|
|
|
|
|---|
Theorems about check-safe-expression-list and rev.
Lists of expressions are used as function arguments. The static semantics checks them in order, while the dynamic semantics executes them in reverse (see exec-funcall. Since execution may have side effect, order is important. However, it is appropriate, and simpler, for the static semantics to check expressions in order without reversing them: the result is the same.
However, this creates a ``gap'' that needs to be bridged in the static soundness proof. We do that with the theorems below. The first serves to prove the second. The third is a good simplification rule. The fourth is awkward, but it is currently needed to discharge a hypothesis in the main proof; without this, the third theorem rewrites away some relevant term.
Theorem:
(defthm reserrp-of-check-safe-expression-list-of-append (equal (reserrp (check-safe-expression-list (append es es1) varset funtab)) (or (reserrp (check-safe-expression-list es varset funtab)) (reserrp (check-safe-expression-list es1 varset funtab)))))
Theorem:
(defthm reserrp-of-check-safe-expression-list-of-rev (equal (reserrp (check-safe-expression-list (rev es) varset funtab)) (reserrp (check-safe-expression-list es varset funtab))))
Theorem:
(defthm check-safe-expression-list-to-len (implies (not (reserrp (check-safe-expression-list es varset funtab))) (equal (check-safe-expression-list es varset funtab) (len es))))
Theorem:
(defthm check-safe-expression-list-not-error-when-rev (implies (not (reserrp (check-safe-expression-list (rev es) varset funtab))) (not (reserrp (check-safe-expression-list es varset funtab)))))