This file proves the compilation lemmas for .record expressions. #
theorem
Cedar.Thm.compile_attr_expr_wfs
{εnv : SymCC.SymEnv}
{axs : List (Spec.Attr × Spec.Expr)}
{ats : List (Spec.Attr × SymCC.Term)}
(hwε : ∀ (ax : Spec.Attr × Spec.Expr), ax ∈ axs → εnv.WellFormedFor ax.snd)
(hok :
List.Forall₂
(fun (px : Spec.Attr × Spec.Expr) (pt : Spec.Attr × SymCC.Term) =>
px.fst = pt.fst ∧ SymCC.compile px.snd εnv = Except.ok pt.snd)
axs ats)
(a : Spec.Attr)
(t : SymCC.Term)
:
theorem
Cedar.Thm.interpret_attr_terms_wfls
{ats : List (Spec.Attr × SymCC.Term)}
{I : SymCC.Interpretation}
{εs : SymCC.SymEntities}
(hI : I.WellFormed εs)
(hwφ :
∀ (a : Spec.Attr) (t : SymCC.Term),
(a, t) ∈ ats → SymCC.Term.WellFormed εs t ∧ ∃ (ty : SymCC.TermType), t.typeOf = ty.option)
(t : SymCC.Term)
:
theorem
Cedar.Thm.compile_interpret_record
{axs : List (Spec.Attr × Spec.Expr)}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{t : SymCC.Term}
(hI : I.WellFormed εnv.entities)
(hwε : εnv.WellFormedFor (Spec.Expr.record axs))
(hok : SymCC.compile (Spec.Expr.record axs) εnv = Except.ok t)
(ih : ∀ (a : Spec.Attr) (x : Spec.Expr), (a, x) ∈ axs → CompileInterpret x)
:
SymCC.compile (Spec.Expr.record axs) (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)
theorem
Cedar.Thm.compile_evaluate_record
{axs : List (Spec.Attr × Spec.Expr)}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
(heq : env ∼ εnv)
(hwe : env.WellFormedFor (Spec.Expr.record axs))
(hwε : εnv.WellFormedFor (Spec.Expr.record axs))
(hok : SymCC.compile (Spec.Expr.record axs) εnv = Except.ok t)
(ih : ∀ (a : Spec.Attr) (x : Spec.Expr), (a, x) ∈ axs → CompileEvaluate x)
: