This file proves the compilation lemmas for .call expressions. #
theorem
Cedar.Thm.compileCall_interpret
{εs : SymCC.SymEntities}
{xfn : Spec.ExtFun}
{ts : List SymCC.Term}
{t : SymCC.Term}
{I : SymCC.Interpretation}
(hI : I.WellFormed εs)
(hwφ : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t)
(hok : SymCC.compileCall xfn ts = Except.ok t)
:
theorem
Cedar.Thm.compile_interpret_call
{f : Spec.ExtFun}
{xs : List Spec.Expr}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor (Spec.Expr.call f xs))
(hok : SymCC.compile (Spec.Expr.call f xs) εnv = Except.ok t)
(ih : ∀ (x : Spec.Expr), x ∈ xs → CompileInterpret x)
:
SymCC.compile (Spec.Expr.call f xs) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)
theorem
Cedar.Thm.compile_evaluate_call
{f : Spec.ExtFun}
{xs : List Spec.Expr}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(heq : env ∼ εnv)
(hwe : env.WellFormedFor (Spec.Expr.call f xs))
(hwε : εnv.WellFormedFor (Spec.Expr.call f xs))
(hok : SymCC.compile (Spec.Expr.call f xs) εnv = Except.ok t)
(ih : ∀ (x : Spec.Expr), x ∈ xs → CompileEvaluate x)
: