Library langs.L2.semantics
Semantic evaluation rules for L2, as in paper Fig. 19 and Appendix
B.
L2 can abruptly terminate either by getting stuck ("going
Wrong"), or by attempting to use a NullV where an actual value was
expected (NullPointer exception).
Values
Number
Boolean
Closure recording its formal parameter Declarations, function
body expression, and the lexical parent FrameId
Default function, which always returns a value V of the expected
type
Record, given by FrameId
NullV value
Aborted computation due to Error
We use auxiliary relations for iterating iterating through n-ary
lets, etc. These produce auxiliary values.
Units -- for indicating successful termination for relations that
only affect the store
Frame
Address
Aborted computation due to Error
abort either propagates the current reason for aborting, or it
aborts by "going wrong". Similarly for aborta.
Definition abort (v: V) :=
match v with
| AbortV e ⇒ AbortV e
| _ ⇒ AbortV Wrong
end.
Definition aborta (v: V) :=
match v with
| AbortV e ⇒ AbortAV e
| _ ⇒ AbortAV Wrong
end.
We postpone defining default values. DVT asserts that there is
a type class instance which defines it
Context `{G: Graph (@AT T)} `{DVT: DefaultVTyp T V} .
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_true_ :
∀
frm h s t,
eval_exp h frm (E s t CTrue) (BoolV true) h
| eval_false_:
∀
frm h s t,
eval_exp h frm (E s t CFalse) (BoolV false) 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_gt_:
∀
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 (Gt e1 e2)) (BoolV (Z.gtb z1 z2)) h2
| eval_gt_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 (Gt e1 e2)) (abort v1) h1
| eval_gt_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 (Gt e1 e2)) (abort v2) h2
| eval_lhs_:
∀
frm s t lhs h0 h1 ff d v
(EVLHS: eval_lhs h0 frm lhs (AddrAV (Addr_ ff d)) h1)
(GET: getSlot h1 ff d v),
eval_exp h0 frm (E s t (Lhs lhs)) v h1
| eval_lhs_b1 :
∀
frm lhs h0 s t h1 q
(EVLHS: eval_lhs h0 frm lhs (AbortAV q) h1),
eval_exp h0 frm (E s t (Lhs lhs)) (AbortV q) h1
| eval_lhs_b2 :
∀
frm s t lhs h0 h1 ff d
(EVLHS: eval_lhs h0 frm lhs (AddrAV (Addr_ ff d)) h1)
(GET: ∀ v, ¬ getSlot h1 ff d v),
eval_exp h0 frm (E s t (Lhs lhs)) (AbortV Wrong) h1
| eval_fn_ :
∀
frm h s t ds e,
eval_exp h frm (E s t (Fn ds e)) (ClosV ds e frm) h
| eval_app :
∀
frm h0 h1 h2 h3 h4 e1 e2s s t vb ff sf f e ds
(EVAL1: eval_exp h0 frm e1 (ClosV ds e ff) h1)
(SF: scopeofFrame h1 ff sf)
(NF: initDefault h1 (expScope e) [(P, [(sf, ff)])] f h2)
(EVAL2: fill_slots_par h2 frm f ds e2s UnitAV h3)
(EVALBODY: eval_exp h3 f e vb h4),
eval_exp h0 frm (E s t (App e1 e2s)) vb h4
| eval_app_dfun :
∀
h0 frm h1 s t e1 e2s v
(EVAL1: eval_exp h0 frm e1 (DefFunV v) h1),
eval_exp h0 frm (E s t (App e1 e2s)) v h1
| 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
| DefFunV _ ⇒ False
| _ ⇒ True
end),
eval_exp h0 frm (E s t (App e1 e2s)) (abort v1) h1
| eval_app_b2 :
∀
h0 frm e1 h1 e2s h2 h3 s t ds e ff sf f q
(EVAL1: eval_exp h0 frm e1 (ClosV ds e ff) h1)
(SF: scopeofFrame h1 ff sf)
(NF: initDefault h1 (expScope e) [(P, [(sf, ff)])] f h2)
(ABORT2: fill_slots_par h2 frm f ds e2s (AbortAV q) h3),
eval_exp h0 frm (E s t (App e1 e2s)) (AbortV q) h3
| eval_letpar_ :
∀
frm h0 h1 h2 h3 lb ds es e2 v2 ff sf s t
(UNZIP: unzipb lb = (ds,es))
(SF: scopeofFrame h1 frm sf)
(NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
(EVAL1: fill_slots_par h1 frm ff ds es UnitAV h2)
(EVAL2: eval_exp h2 ff e2 v2 h3),
eval_exp h0 frm (E s t (LetPar lb e2)) v2 h3
| eval_letpar_b1 :
∀
frm h0 h1 h2 lb ds es e2 s t ff sf q
(UNZIP : unzipb lb = (ds,es))
(SF: scopeofFrame h1 frm sf)
(NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
(ABORT1: fill_slots_par h1 frm ff ds es (AbortAV q) h2),
eval_exp h0 frm (E s t (LetPar lb e2)) (AbortV q) h2
| eval_letseq_ :
∀
frm h0 h1 h2 lb ds es e2 v2 s t fi
(UNZIP: unzipb lb = (ds, es))
(EVAL1: fill_slots_seq h0 frm ds es (FrameAV fi) h1)
(EVAL2: eval_exp h1 fi e2 v2 h2),
eval_exp h0 frm (E s t (LetSeq lb e2)) v2 h2
| eval_letseq_b1 :
∀
frm h0 h1 lb ds es e2 s t q
(UNZIP: unzipb lb = (ds, es))
(ABORT1 : fill_slots_seq h0 frm ds es (AbortAV q) h1),
eval_exp h0 frm (E s t (LetSeq lb e2)) (AbortV q) h1
| eval_letrec_ :
∀
frm h0 h1 h2 h3 lvb ds evs e2 v2 ff sf s t
(UNZIP: unzipb lvb = (ds,evs))
(SF: scopeofFrame h1 frm sf)
(NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
(EVAL1: fill_slots_rec h1 ff ds evs UnitAV h2)
(EVAL2: eval_exp h2 ff e2 v2 h3),
eval_exp h0 frm (E s t (LetRec lvb e2)) v2 h3
| eval_letrec_b1 :
∀
frm h0 h1 h2 lb ds es e2 s t ff sf q
(UNZIP: unzipb lb = (ds,es))
(SF: scopeofFrame h1 frm sf)
(NF: initDefault h0 (expScope e2) [(P, [(sf, frm)])] ff h1)
(ABORT1: fill_slots_rec h1 ff ds es (AbortAV q) h2),
eval_exp h0 frm (E s t (LetRec lb e2)) (AbortV q) h2
| eval_asgn_ :
∀
h0 frm s t lhs e h1 h2 ff d v h3
(EVLHS: eval_lhs h0 frm lhs (AddrAV (Addr_ ff d)) h1)
(EVAL: eval_exp h1 frm e v h2)
(SET: setSlot h2 ff d v h3),
eval_exp h0 frm (E s t (Asgn lhs e)) v h3
| eval_asgn_b1 :
∀
h0 frm s t lhs e h1 q
(EVAL: eval_lhs h0 frm lhs (AbortAV q) h1),
eval_exp h0 frm (E s t (Asgn lhs e)) (AbortV q) h1
| eval_asgn_b2 :
∀
h0 frm s t lhs e h1 ff d q h2
(EVAL: eval_lhs h0 frm lhs (AddrAV (Addr_ ff d)) h1)
(ABORT: eval_exp h1 frm e (AbortV q) h2),
eval_exp h0 frm (E s t (Asgn lhs e)) (AbortV q) h2
| eval_asgn_b3 :
∀
h0 frm s t lhs e h1 h2 ff d v
(EVLHS: eval_lhs h0 frm lhs (AddrAV (Addr_ ff d)) h1)
(EVAL: eval_exp h1 frm e v h2)
(SET: ∀ h3, ¬ setSlot h2 ff d v h3),
eval_exp h0 frm (E s t (Asgn lhs e)) (AbortV Wrong) h2
| eval_if_t :
∀
frm e1 e2 e3 v h0 h1 h2 s t
(EVAL1: eval_exp h0 frm e1 (BoolV true) h1)
(EVAL2: eval_exp h1 frm e2 v h2),
eval_exp h0 frm (E s t (If e1 e2 e3)) v h2
| eval_if_f :
∀
frm e1 e2 e3 v h0 h1 h2 s t
(EVAL1: eval_exp h0 frm e1 (BoolV false) h1)
(EVAL3: eval_exp h1 frm e3 v h2),
eval_exp h0 frm (E s t (If e1 e2 e3)) v h2
| eval_if_b1:
∀
frm e1 e2 e3 h0 h1 v1 s t
(EVAL1: eval_exp h0 frm e1 v1 h1)
(ABORT1: ∀ b, v1 ≠ BoolV b),
eval_exp h0 frm (E s t (If e1 e2 e3)) (abort v1) h1
| eval_seq_ :
∀
frm e1 e2 v1 v2 h0 h1 h2 s t
(EVAL1: eval_exp h0 frm e1 v1 h1)
(GOOD1: good v1)
(EVAL2: eval_exp h1 frm e2 v2 h2),
eval_exp h0 frm (E s t (Seq e1 e2)) v2 h2
| eval_seq_b1 :
∀
frm e1 e2 h0 h1 s t q
(EVAL1: eval_exp h0 frm e1 (AbortV q) h1),
eval_exp h0 frm (E s t (Seq e1 e2)) (AbortV q) h1
| eval_new_ :
∀
frm r h0 h1 rf s t s0 p s' d'
(RLOOK: rlookup r p s' d')
(ASC: assocScope d' s0)
(RECF: initDefault h0 s0 [] rf h1),
eval_exp h0 frm (E s t (New r)) (RecordV rf) h1
| eval_new_b1 :
∀
frm r h0 s t
(RLOOK: ∀ p s' d' s0, ¬ (rlookup r p s' d' ∧ assocScope d' s0)),
eval_exp h0 frm (E s t (New r)) (AbortV Wrong) h0
with eval_lhs : H → FrameId → lhs → AuxV → H → Prop :=
| eval_lhs_var_ :
∀
h frm r a
(ADDR: getAddr h frm r a),
eval_lhs h frm (Var r) (AddrAV a) h
| eval_lhs_var_b :
∀
h frm r
(ADDR: ∀ a, ¬ getAddr h frm r a),
eval_lhs h frm (Var r) (AbortAV Wrong) h
| eval_lhs_field :
∀
h0 frm e r s rf scf h1 h2 a sf
(EVAL: eval_exp h0 frm e (RecordV rf) h1)
(SF: scopeofFrame h1 rf sf)
(SCF: initDefault h1 s [(I, [(sf, rf)])] scf h2)
(SCR: scopeofRefP r s)
(ADDR: getAddr h2 scf r a),
eval_lhs h0 frm (Field e r) (AddrAV a) h2
| eval_lhs_field_null :
∀
h0 frm e r h1
(EVAL: eval_exp h0 frm e NullV h1),
eval_lhs h0 frm (Field e r) (AbortAV NullPointer) h1
| eval_lhs_field_b1:
∀
h0 frm e r h1 v
(EVAL: eval_exp h0 frm e v h1)
(BAD: match v with
| RecordV _ ⇒ False
| NullV ⇒ False
| _ ⇒ True
end),
eval_lhs h0 frm (Field e r) (aborta v) h1
| eval_lhs_field_b2:
∀
h0 frm e r s rf scf h1 h2 sf
(EVAL: eval_exp h0 frm e (RecordV rf) h1)
(SCR: scopeofRefP r s)
(SF: scopeofFrame h1 rf sf)
(SCF: initDefault h1 s [(I, [(sf, rf)])] scf h2)
(ADDR: ∀ a, ¬ getAddr h2 scf r a),
eval_lhs h0 frm (Field e r) (AbortAV Wrong) h2
with fill_slots_par : H → FrameId → FrameId → list D → list exp → AuxV → H → Prop :=
| fill_par_nil :
∀
h frm fc,
fill_slots_par h frm fc nil nil UnitAV h
| fill_par_b1 :
∀
h frm fc ld,
ld ≠ nil →
fill_slots_par h frm fc ld nil (AbortAV Wrong) h
| fill_par_b2 :
∀
h frm fc le,
le ≠ nil →
fill_slots_par h frm fc nil le (AbortAV Wrong) h
| fill_par_cons :
∀
h0 frm e d es ds fc v h1 h2 h3 v1
(EVAL: eval_exp h0 frm e v h1)
(GOOD: good v)
(SS: setSlot h1 fc d v h2)
(TAIL: fill_slots_par h2 frm fc ds es v1 h3),
fill_slots_par h0 frm fc (d::ds) (e::es) v1 h3
| fill_par_cons_b1 :
∀
h0 frm e es d ds fc h1 q
(EVAL: eval_exp h0 frm e (AbortV q) h1),
fill_slots_par h0 frm fc (d :: ds) (e :: es) (AbortAV q) h1
| fill_par_cons_b2 :
∀
h0 frm e d es ds fc v h1
(EVAL: eval_exp h0 frm e v h1)
(GOOD: good v)
(SS: ∀ h2, ¬ setSlot h1 fc d v h2),
fill_slots_par h0 frm fc (d::ds) (e::es) (AbortAV Wrong) h1
with fill_slots_seq : H → FrameId → list D → list exp → AuxV → H → Prop :=
| fill_seq_nil :
∀
h frm,
fill_slots_seq h frm nil nil (FrameAV frm) h
| fill_seq_b1 :
∀
h frm ld,
ld ≠ nil →
fill_slots_seq h frm ld nil (AbortAV Wrong) h
| fill_seq_b2 :
∀
h frm le,
le ≠ nil →
fill_slots_seq h frm nil le (AbortAV Wrong) h
| fill_seq_cons :
∀
h0 frm e es d ds fc v h1 h2 h3 h4 v1 sd sf
(SD: scopeofDecl d = Some sd)
(SF: scopeofFrame h0 frm sf)
(NF: initDefault h0 sd [(P, [(sf, frm)])] fc h1)
(EVAL: eval_exp h1 frm e v h2)
(GOOD: good v)
(SS: setSlot h2 fc d v h3)
(TAIL: fill_slots_seq h3 fc ds es v1 h4),
fill_slots_seq h0 frm (d :: ds) (e :: es) v1 h4
| fill_seq_cons_b1 :
∀
h0 frm e es d ds h1 sd fc h2 q sf
(SD: scopeofDecl d = Some sd)
(SF: scopeofFrame h0 frm sf)
(NF: initDefault h0 sd [(P, [(sf, frm)])] fc h1)
(EVAL: eval_exp h1 frm e (AbortV q) h2),
fill_slots_seq h0 frm (d :: ds) (e :: es) (AbortAV q) h2
| fill_seq_cons_b2 :
∀
h0 frm e es d ds fc v h1 h2 sd sf
(SD: scopeofDecl d = Some sd)
(SF: scopeofFrame h0 frm sf)
(NF: initDefault h0 sd [(P, [(sf, frm)])] fc h1)
(EVAL: eval_exp h1 frm e v h2)
(GOOD: good v)
(SS: ∀ h3, ¬ setSlot h2 fc d v h3),
fill_slots_seq h0 frm (d :: ds) (e :: es) (AbortAV Wrong) h2
with fill_slots_rec : H → FrameId → list D → list exp → AuxV → H → Prop :=
| fill_rec_nil :
∀
h frm,
fill_slots_rec h frm nil nil UnitAV h
| fill_rec_b1 :
∀
h frm ld,
ld ≠ nil →
fill_slots_rec h frm ld nil (AbortAV Wrong) h
| fill_rec_b2 :
∀
h frm le,
le ≠ nil →
fill_slots_rec h frm nil le (AbortAV Wrong) h
| fill_rec_cons :
∀
h0 frm e d es ds v h1 h2 h3 v1
(EVAL: eval_exp h0 frm e v h1)
(GOOD: good v)
(SS: setSlot h1 frm d v h2)
(TAIL: fill_slots_rec h2 frm ds es v1 h3),
fill_slots_rec h0 frm (d::ds) (e::es) v1 h3
| fill_rec_cons_b1 :
∀
h0 frm e es d ds h1 q
(EVAL: eval_exp h0 frm e (AbortV q) h1),
fill_slots_rec h0 frm (d :: ds) (e :: es) (AbortAV q) h1
| fill_rec_cons_b2 :
∀
h0 frm e d es ds v h1 v1
(EVAL: eval_exp h0 frm e v h1)
(GOOD: good v)
(SS: ∀ h2, ¬ setSlot h1 frm d v h2),
fill_slots_rec h0 frm (d::ds) (e::es) v1 h1
.
Combined induction scheme, used for mutual induction. See also:
https://coq.inria.fr/cocorico/Mutual
Scheme eval_exp_ind2 := Minimality for eval_exp Sort Prop
with fill_par_ind2 := Minimality for fill_slots_par Sort Prop
with fill_seq_ind2 := Minimality for fill_slots_seq Sort Prop
with fill_rec_ind2 := Minimality for fill_slots_rec Sort Prop
with eval_lhs_ind2 := Minimality for eval_lhs Sort Prop.
Combined Scheme eval_exp_ind3
from eval_exp_ind2, fill_par_ind2, fill_seq_ind2, fill_rec_ind2, eval_lhs_ind2.
Inductive eval_prog : prog → V → Prop :=
| eval_prog_ : ∀
e v f h0 h1 rds
(TOPFRM: initDefault (emptyHeap) (expScope e) [] f h0)
(EVALB: eval_exp h0 f e v h1),
eval_prog (Prog rds e) v
.
End DynamicSemantics.
with fill_par_ind2 := Minimality for fill_slots_par Sort Prop
with fill_seq_ind2 := Minimality for fill_slots_seq Sort Prop
with fill_rec_ind2 := Minimality for fill_slots_rec Sort Prop
with eval_lhs_ind2 := Minimality for eval_lhs Sort Prop.
Combined Scheme eval_exp_ind3
from eval_exp_ind2, fill_par_ind2, fill_seq_ind2, fill_rec_ind2, eval_lhs_ind2.
Inductive eval_prog : prog → V → Prop :=
| eval_prog_ : ∀
e v f h0 h1 rds
(TOPFRM: initDefault (emptyHeap) (expScope e) [] f h0)
(EVALB: eval_exp h0 f e v h1),
eval_prog (Prog rds e) v
.
End DynamicSemantics.