Library langs.L1.semantics
Semantics of L1 evaluation from paper Fig. 13 and Appendix A.
L1 can only abruptly terminate by getting stuck ("going
Wrong").
Values
Number
Closure recording its formal parameter Declaration, function
body expression, and the lexical parent FrameId
Aborted computation due to Error
abort either propagates the current reason for aborting, or it
aborts by "going wrong".
Unifies the type parameters for the definition of FrameHeap
types
Evaluation depends mainly on pre-terms and, occasionally, on scope
annotations; it ignores type annotations.
Inductive eval_exp : H → FrameId → exp → V → H → Prop :=
| eval_cnum_ :
∀ frm z h s t,
eval_exp h frm (E s t (CNum z)) (NumV z) h
| eval_plus_ :
∀
frm e1 e2 z1 z2 h0 h1 h2 s t
(EVALL: eval_exp h0 frm e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm e2 (NumV z2) h2),
eval_exp h0 frm (E s t (Plus e1 e2)) (NumV (z1+z2)%Z) h2
| eval_plus_b1 :
∀
frm e1 e2 h0 v1 h1 s t
(EVALL: eval_exp h0 frm e1 v1 h1)
(ABORTL: ∀ z1, v1 ≠ NumV z1),
eval_exp h0 frm (E s t (Plus e1 e2)) (abort v1) h1
| eval_plus_b2 :
∀
frm e1 e2 h0 z1 v2 h1 h2 s t
(EVALL: eval_exp h0 frm e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm e2 v2 h2)
(ABORTR: ∀ z2, v2 ≠ NumV z2),
eval_exp h0 frm (E s t (Plus e1 e2)) (abort v2) h2
| eval_var_ :
∀
frm s t r h0 ff d v
(ADDR: getAddr h0 frm r (Addr_ ff d))
(GET: getSlot h0 ff d v),
eval_exp h0 frm (E s t (Var r)) v h0
| eval_var_b1 :
∀
frm r h0 s t
(ADDR: ∀ ff d, ¬ getAddr h0 frm r (Addr_ ff d)),
eval_exp h0 frm (E s t (Var r)) (AbortV Wrong) h0
| eval_var_b2 :
∀
frm r h0 s t ff d
(ADDR: getAddr h0 frm r (Addr_ ff d))
(NGET: ∀ v, ¬ getSlot h0 ff d v),
eval_exp h0 frm (E s t (Var r)) (AbortV Wrong) h0
| eval_fn_ :
∀
frm h s t t0 d e,
eval_exp h frm (E s t (Fn d t0 e)) (ClosV d e frm) h
| eval_app :
∀
frm h0 h1 h2 h3 h4 e1 e2 v2 s t vb ff f e d sp
(EVAL1: eval_exp h0 frm e1 (ClosV d e ff) h1)
(EVAL2: eval_exp h1 frm e2 v2 h2)
(SF: scopeofFrame h2 ff sp)
(NF: initFrame h2 (expScope e) [(P, [(sp, ff)])] [(d,v2)] f h3)
(EVALBODY: eval_exp h3 f e vb h4),
eval_exp h0 frm (E s t (App e1 e2)) vb h4
| eval_app_b1 :
∀
h0 frm v1 h1 s t e1 e2s
(EVAL1: eval_exp h0 frm e1 v1 h1)
(ABORT1: match v1 with
| ClosV _ _ _ ⇒ False
| _ ⇒ True
end),
eval_exp h0 frm (E s t (App e1 e2s)) (abort v1) h1
| eval_app_b2 :
∀
h0 frm e1 h1 e2 h2 s t d e ff q
(EVAL1: eval_exp h0 frm e1 (ClosV d e ff) h1)
(EVAL2: eval_exp h1 frm e2 (AbortV q) h2),
eval_exp h0 frm (E s t (App e1 e2)) (AbortV q) h2
.
Inductive eval_prog : prog → V → Prop :=
| eval_prog_ :
∀
e v f h0 h1
(TOPFRM: initFrame emptyHeap (expScope e) [] [] f h0)
(EVALB: eval_exp h0 f e v h1),
eval_prog (Prog e) v
.
End DynamicSemantics.
| eval_cnum_ :
∀ frm z h s t,
eval_exp h frm (E s t (CNum z)) (NumV z) h
| eval_plus_ :
∀
frm e1 e2 z1 z2 h0 h1 h2 s t
(EVALL: eval_exp h0 frm e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm e2 (NumV z2) h2),
eval_exp h0 frm (E s t (Plus e1 e2)) (NumV (z1+z2)%Z) h2
| eval_plus_b1 :
∀
frm e1 e2 h0 v1 h1 s t
(EVALL: eval_exp h0 frm e1 v1 h1)
(ABORTL: ∀ z1, v1 ≠ NumV z1),
eval_exp h0 frm (E s t (Plus e1 e2)) (abort v1) h1
| eval_plus_b2 :
∀
frm e1 e2 h0 z1 v2 h1 h2 s t
(EVALL: eval_exp h0 frm e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm e2 v2 h2)
(ABORTR: ∀ z2, v2 ≠ NumV z2),
eval_exp h0 frm (E s t (Plus e1 e2)) (abort v2) h2
| eval_var_ :
∀
frm s t r h0 ff d v
(ADDR: getAddr h0 frm r (Addr_ ff d))
(GET: getSlot h0 ff d v),
eval_exp h0 frm (E s t (Var r)) v h0
| eval_var_b1 :
∀
frm r h0 s t
(ADDR: ∀ ff d, ¬ getAddr h0 frm r (Addr_ ff d)),
eval_exp h0 frm (E s t (Var r)) (AbortV Wrong) h0
| eval_var_b2 :
∀
frm r h0 s t ff d
(ADDR: getAddr h0 frm r (Addr_ ff d))
(NGET: ∀ v, ¬ getSlot h0 ff d v),
eval_exp h0 frm (E s t (Var r)) (AbortV Wrong) h0
| eval_fn_ :
∀
frm h s t t0 d e,
eval_exp h frm (E s t (Fn d t0 e)) (ClosV d e frm) h
| eval_app :
∀
frm h0 h1 h2 h3 h4 e1 e2 v2 s t vb ff f e d sp
(EVAL1: eval_exp h0 frm e1 (ClosV d e ff) h1)
(EVAL2: eval_exp h1 frm e2 v2 h2)
(SF: scopeofFrame h2 ff sp)
(NF: initFrame h2 (expScope e) [(P, [(sp, ff)])] [(d,v2)] f h3)
(EVALBODY: eval_exp h3 f e vb h4),
eval_exp h0 frm (E s t (App e1 e2)) vb h4
| eval_app_b1 :
∀
h0 frm v1 h1 s t e1 e2s
(EVAL1: eval_exp h0 frm e1 v1 h1)
(ABORT1: match v1 with
| ClosV _ _ _ ⇒ False
| _ ⇒ True
end),
eval_exp h0 frm (E s t (App e1 e2s)) (abort v1) h1
| eval_app_b2 :
∀
h0 frm e1 h1 e2 h2 s t d e ff q
(EVAL1: eval_exp h0 frm e1 (ClosV d e ff) h1)
(EVAL2: eval_exp h1 frm e2 (AbortV q) h2),
eval_exp h0 frm (E s t (App e1 e2)) (AbortV q) h2
.
Inductive eval_prog : prog → V → Prop :=
| eval_prog_ :
∀
e v f h0 h1
(TOPFRM: initFrame emptyHeap (expScope e) [] [] f h0)
(EVALB: eval_exp h0 f e v h1),
eval_prog (Prog e) v
.
End DynamicSemantics.