Library langs.L2.GCsemantics
A version of L2 semantics that safely drops frames on a non-deterministic basis.
Attempting to apply a null value
Getting stuck
Values
Inductive V :=
| NumV : Z → V
| BoolV : bool → V
| ClosV : list D → exp → FrameId → V
| DefFunV : V → V
| RecordV : FrameId → V
| NullV : V
| AbortV : Error → V
.
| NumV : Z → V
| BoolV : bool → V
| ClosV : list D → exp → FrameId → V
| DefFunV : V → V
| RecordV : FrameId → V
| NullV : V
| AbortV : Error → V
.
Outcomes of auxiliary computations:
Inductive AuxV :=
| UnitAV
| FrameAV : FrameId → AuxV
| AbortAV : Error → AuxV
| AddrAV : Addr → AuxV
.
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.
Definition good (v: V) :=
match v with
| AbortV _ ⇒ False
| _ ⇒ True
end.
| UnitAV
| FrameAV : FrameId → AuxV
| AbortAV : Error → AuxV
| AddrAV : Addr → AuxV
.
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.
Definition good (v: V) :=
match v with
| AbortV _ ⇒ False
| _ ⇒ True
end.
Checks if a value refers to a frame:
Inductive vrefers' : V → FrameId → Prop :=
| vr_clos : ∀ v xs e f,
v = ClosV xs e f →
vrefers' v f
| vr_deffun : ∀ v v' f,
v = DefFunV v' →
vrefers' v' f →
vrefers' v f
| vr_record : ∀ v f,
v = RecordV f →
vrefers' v f
.
Instance VR : @VRefers V :=
{ vrefers := vrefers'
}.
| vr_clos : ∀ v xs e f,
v = ClosV xs e f →
vrefers' v f
| vr_deffun : ∀ v v' f,
v = DefFunV v' →
vrefers' v' f →
vrefers' v f
| vr_record : ∀ v f,
v = RecordV f →
vrefers' v f
.
Instance VR : @VRefers V :=
{ vrefers := vrefers'
}.
In this version, the "machine state" is augmented with an auxiliary stack
of roots that must be preserved by GC.
The only different transition in this version: safely drop any set of frames
outside of the current frame and the auxiliary root stack.
∀ h0 h1 h2 frm roots s t e v fs,
safeRemoval h0 fs h1 →
(∀ f, In f fs → ¬ In f (frm::roots)) →
eval_exp h1 frm roots (E s t e) v h2 →
eval_exp h0 frm roots (E s t e) v h2
| eval_cnum_ :
∀
frm roots z h s t,
eval_exp h frm roots (E s t (CNum z)) (NumV z) h
| eval_true_ :
∀
frm roots h s t,
eval_exp h frm roots (E s t CTrue) (BoolV true) h
| eval_false_:
∀
frm roots h s t,
eval_exp h frm roots (E s t CFalse) (BoolV false) h
| eval_plus_:
∀
frm roots e1 e2 z1 z2 h0 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 (NumV z2) h2),
eval_exp h0 frm roots (E s t (Plus e1 e2)) (NumV (z1+z2)%Z) h2
| eval_plus_b1 :
∀
frm roots e1 e2 h0 v1 h1 s t
(EVALL: eval_exp h0 frm roots e1 v1 h1)
(ABORTL: ∀ z1, v1 ≠ NumV z1),
eval_exp h0 frm roots (E s t (Plus e1 e2)) (abort v1) h1
| eval_plus_b2 :
∀
frm roots e1 e2 h0 z1 v2 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 v2 h2)
(ABORTR: ∀ z2, v2 ≠ NumV z2),
eval_exp h0 frm roots (E s t (Plus e1 e2)) (abort v2) h2
| eval_gt_:
∀
frm roots e1 e2 z1 z2 h0 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 (NumV z2) h2),
eval_exp h0 frm roots (E s t (Gt e1 e2)) (BoolV (Z.gtb z1 z2)) h2
| eval_gt_b1 :
∀
frm roots e1 e2 h0 v1 h1 s t
(EVALL: eval_exp h0 frm roots e1 v1 h1)
(ABORTL:∀ z1, v1 ≠ NumV z1),
eval_exp h0 frm roots (E s t (Gt e1 e2)) (abort v1) h1
| eval_gt_b2 :
∀
frm roots e1 e2 h0 z1 v2 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 v2 h2)
(ABORTR: ∀ z2, v2 ≠ NumV z2),
eval_exp h0 frm roots (E s t (Gt e1 e2)) (abort v2) h2
| eval_lhs_:
∀
frm roots s t lhs h0 h1 ff d v
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(GET: getSlot h1 ff d v),
eval_exp h0 frm roots (E s t (Lhs lhs)) v h1
| eval_lhs_b1 :
∀
frm roots lhs h0 s t h1 q
(EVLHS: eval_lhs h0 frm roots lhs (AbortAV q) h1),
eval_exp h0 frm roots (E s t (Lhs lhs)) (AbortV q) h1
| eval_lhs_b2 :
∀
frm roots s t lhs h0 h1 ff d
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(GET: ∀ v, ¬ getSlot h1 ff d v),
eval_exp h0 frm roots (E s t (Lhs lhs)) (AbortV Wrong) h1
| eval_fn_ :
∀
frm roots h s t ds e,
eval_exp h frm roots (E s t (Fn ds e)) (ClosV ds e frm) h
| eval_app :
∀
frm roots h0 h1 h2 h3 h4 e1 e2s s t vb ff sf f e ds
(EVAL1: eval_exp h0 frm roots 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::roots) f ds e2s UnitAV h3)
(EVALBODY: eval_exp h3 f (frm::roots) e vb h4),
eval_exp h0 frm roots (E s t (App e1 e2s)) vb h4
| eval_app_dfun :
∀
h0 frm roots h1 s t e1 e2s v
(EVAL1: eval_exp h0 frm roots e1 (DefFunV v) h1),
eval_exp h0 frm roots (E s t (App e1 e2s)) v h1
| eval_app_b1 :
∀
h0 frm roots v1 h1 s t e1 e2s
(EVAL1: eval_exp h0 frm roots e1 v1 h1)
(ABORT1: match v1 with
| ClosV _ _ _ ⇒ False
| DefFunV _ ⇒ False
| _ ⇒ True
end),
eval_exp h0 frm roots (E s t (App e1 e2s)) (abort v1) h1
| eval_app_b2 :
∀
h0 frm roots e1 h1 e2s h2 h3 s t ds e ff sf f q
(EVAL1: eval_exp h0 frm roots 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::roots) f ds e2s (AbortAV q) h3),
eval_exp h0 frm roots (E s t (App e1 e2s)) (AbortV q) h3
| eval_letpar_ :
∀
frm roots 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::roots) ff ds es UnitAV h2)
(EVAL2: eval_exp h2 ff (frm::roots) e2 v2 h3),
eval_exp h0 frm roots (E s t (LetPar lb e2)) v2 h3
| eval_letpar_b1 :
∀
frm roots 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::roots) ff ds es (AbortAV q) h2),
eval_exp h0 frm roots (E s t (LetPar lb e2)) (AbortV q) h2
| eval_letseq_ :
∀
frm roots h0 h1 h2 lb ds es e2 v2 s t fi
(UNZIP: unzipb lb = (ds, es))
(EVAL1: fill_slots_seq h0 frm roots ds es (FrameAV fi) h1)
(EVAL2: eval_exp h1 fi (frm::roots) e2 v2 h2),
eval_exp h0 frm roots (E s t (LetSeq lb e2)) v2 h2
| eval_letseq_b1 :
∀
frm roots h0 h1 lb ds es e2 s t q
(UNZIP: unzipb lb = (ds, es))
(ABORT1 : fill_slots_seq h0 frm roots ds es (AbortAV q) h1),
eval_exp h0 frm roots (E s t (LetSeq lb e2)) (AbortV q) h1
| eval_letrec_ :
∀
frm roots 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 (frm::roots) ds evs UnitAV h2)
(EVAL2: eval_exp h2 ff (frm::roots) e2 v2 h3),
eval_exp h0 frm roots (E s t (LetRec lvb e2)) v2 h3
| eval_letrec_b1 :
∀
frm roots 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 (frm::roots) ds es (AbortAV q) h2),
eval_exp h0 frm roots (E s t (LetRec lb e2)) (AbortV q) h2
| eval_asgn_ :
∀
h0 frm roots s t lhs e h1 h2 ff d v h3
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(EVAL: eval_exp h1 frm (ff::roots) e v h2)
(SET: setSlot h2 ff d v h3),
eval_exp h0 frm roots (E s t (Asgn lhs e)) v h3
| eval_asgn_b1 :
∀
h0 frm roots s t lhs e h1 q
(EVAL: eval_lhs h0 frm roots lhs (AbortAV q) h1),
eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV q) h1
| eval_asgn_b2 :
∀
h0 frm roots s t lhs e h1 ff d q h2
(EVAL: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(ABORT: eval_exp h1 frm (ff::roots) e (AbortV q) h2),
eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV q) h2
| eval_asgn_b3 :
∀
h0 frm roots s t lhs e h1 h2 ff d v
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(EVAL: eval_exp h1 frm (ff::roots) e v h2)
(SET: ∀ h3, ¬ setSlot h2 ff d v h3),
eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV Wrong) h2
| eval_if_t :
∀
frm roots e1 e2 e3 v h0 h1 h2 s t
(EVAL1: eval_exp h0 frm roots e1 (BoolV true) h1)
(EVAL2: eval_exp h1 frm roots e2 v h2),
eval_exp h0 frm roots (E s t (If e1 e2 e3)) v h2
| eval_if_f :
∀
frm roots e1 e2 e3 v h0 h1 h2 s t
(EVAL1: eval_exp h0 frm roots e1 (BoolV false) h1)
(EVAL3: eval_exp h1 frm roots e3 v h2),
eval_exp h0 frm roots (E s t (If e1 e2 e3)) v h2
| eval_if_b1:
∀
frm roots e1 e2 e3 h0 h1 v1 s t
(EVAL1: eval_exp h0 frm roots e1 v1 h1)
(ABORT1: ∀ b, v1 ≠ BoolV b),
eval_exp h0 frm roots (E s t (If e1 e2 e3)) (abort v1) h1
| eval_seq_ :
∀
frm roots e1 e2 v1 v2 h0 h1 h2 s t
(EVAL1: eval_exp h0 frm roots e1 v1 h1)
(GOOD1: good v1)
(EVAL2: eval_exp h1 frm roots e2 v2 h2),
eval_exp h0 frm roots (E s t (Seq e1 e2)) v2 h2
| eval_seq_b1 :
∀
frm roots e1 e2 h0 h1 s t q
(EVAL1: eval_exp h0 frm roots e1 (AbortV q) h1),
eval_exp h0 frm roots (E s t (Seq e1 e2)) (AbortV q) h1
| eval_new_ :
∀
frm roots 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 roots (E s t (New r)) (RecordV rf) h1
| eval_new_b1 :
∀
frm roots r h0 s t
(RLOOK: ∀ p s' d' s0, ¬ (rlookup r p s' d' ∧ assocScope d' s0)),
eval_exp h0 frm roots (E s t (New r)) (AbortV Wrong) h0
with eval_lhs : H → FrameId → list FrameId → lhs → AuxV → H → Prop :=
| eval_lhs_var_ :
∀
h frm roots r a
(ADDR: getAddr h frm r a),
eval_lhs h frm roots (Var r) (AddrAV a) h
| eval_lhs_var_b :
∀
h frm roots r
(ADDR: ∀ a, ¬ getAddr h frm r a),
eval_lhs h frm roots (Var r) (AbortAV Wrong) h
| eval_lhs_field :
∀
h0 frm roots e r s rf scf h1 h2 a sf
(EVAL: eval_exp h0 frm roots 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 roots (Field e r) (AddrAV a) h2
| eval_lhs_field_null :
∀
h0 frm roots e r h1
(EVAL: eval_exp h0 frm roots e NullV h1),
eval_lhs h0 frm roots (Field e r) (AbortAV NullPointer) h1
| eval_lhs_field_b1:
∀
h0 frm roots e r h1 v
(EVAL: eval_exp h0 frm roots e v h1)
(BAD: match v with
| RecordV _ ⇒ False
| NullV ⇒ False
| _ ⇒ True
end),
eval_lhs h0 frm roots (Field e r) (aborta v) h1
| eval_lhs_field_b2:
∀
h0 frm roots e r s rf scf h1 h2 sf
(EVAL: eval_exp h0 frm roots 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 roots (Field e r) (AbortAV Wrong) h2
with fill_slots_par : H → FrameId → list FrameId → FrameId → list D → list exp → AuxV → H → Prop :=
| fill_par_nil :
∀
h frm roots fc,
fill_slots_par h frm roots fc nil nil UnitAV h
| fill_par_b1 :
∀
h frm roots fc ld,
ld ≠ nil →
fill_slots_par h frm roots fc ld nil (AbortAV Wrong) h
| fill_par_b2 :
∀
h frm roots fc le,
le ≠ nil →
fill_slots_par h frm roots fc nil le (AbortAV Wrong) h
| fill_par_cons :
∀
h0 frm roots e d es ds fc v h1 h2 h3 v1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: setSlot h1 fc d v h2)
(TAIL: fill_slots_par h2 frm roots fc ds es v1 h3),
fill_slots_par h0 frm roots fc (d::ds) (e::es) v1 h3
| fill_par_cons_b1 :
∀
h0 frm roots e es d ds fc h1 q
(EVAL: eval_exp h0 frm roots e (AbortV q) h1),
fill_slots_par h0 frm roots fc (d :: ds) (e :: es) (AbortAV q) h1
| fill_par_cons_b2 :
∀
h0 frm roots e d es ds fc v h1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: ∀ h2, ¬ setSlot h1 fc d v h2),
fill_slots_par h0 frm roots fc (d::ds) (e::es) (AbortAV Wrong) h1
with fill_slots_seq : H → FrameId → list FrameId → list D → list exp → AuxV → H → Prop :=
| fill_seq_nil :
∀
h frm roots,
fill_slots_seq h frm roots nil nil (FrameAV frm) h
| fill_seq_b1 :
∀
h frm roots ld,
ld ≠ nil →
fill_slots_seq h frm roots ld nil (AbortAV Wrong) h
| fill_seq_b2 :
∀
h frm roots le,
le ≠ nil →
fill_slots_seq h frm roots nil le (AbortAV Wrong) h
| fill_seq_cons :
∀
h0 frm roots 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 (fc::roots) e v h2)
(GOOD: good v)
(SS: setSlot h2 fc d v h3)
(TAIL: fill_slots_seq h3 fc (frm::roots) ds es v1 h4),
fill_slots_seq h0 frm roots (d :: ds) (e :: es) v1 h4
| fill_seq_cons_b1 :
∀
h0 frm roots 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 (fc::roots) e (AbortV q) h2),
fill_slots_seq h0 frm roots (d :: ds) (e :: es) (AbortAV q) h2
| fill_seq_cons_b2 :
∀
h0 frm roots 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 (fc::roots) e v h2)
(GOOD: good v)
(SS: ∀ h3, ¬ setSlot h2 fc d v h3),
fill_slots_seq h0 frm roots (d :: ds) (e :: es) (AbortAV Wrong) h2
with fill_slots_rec : H → FrameId → list FrameId → list D → list exp → AuxV → H → Prop :=
| fill_rec_nil :
∀
h frm roots,
fill_slots_rec h frm roots nil nil UnitAV h
| fill_rec_b1 :
∀
h frm roots ld,
ld ≠ nil →
fill_slots_rec h frm roots ld nil (AbortAV Wrong) h
| fill_rec_b2 :
∀
h frm roots le,
le ≠ nil →
fill_slots_rec h frm roots nil le (AbortAV Wrong) h
| fill_rec_cons :
∀
h0 frm roots e d es ds v h1 h2 h3 v1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: setSlot h1 frm d v h2)
(TAIL: fill_slots_rec h2 frm roots ds es v1 h3),
fill_slots_rec h0 frm roots (d::ds) (e::es) v1 h3
| fill_rec_cons_b1 :
∀
h0 frm roots e es d ds h1 q
(EVAL: eval_exp h0 frm roots e (AbortV q) h1),
fill_slots_rec h0 frm roots (d :: ds) (e :: es) (AbortAV q) h1
| fill_rec_cons_b2 :
∀
h0 frm roots e d es ds v h1 v1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: ∀ h2, ¬ setSlot h1 frm d v h2),
fill_slots_rec h0 frm roots (d::ds) (e::es) v1 h1
.
Scheme eval_exp_ind2 := Minimality for eval_exp Sort Prop
with eval_lhs_ind2 := Minimality for eval_lhs 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.
Combined Scheme eval_exp_ind3
from eval_exp_ind2, eval_lhs_ind2, fill_par_ind2, fill_seq_ind2, fill_rec_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 nil e v h1),
eval_prog (Prog rds e) v
.
End DynamicSemantics.
safeRemoval h0 fs h1 →
(∀ f, In f fs → ¬ In f (frm::roots)) →
eval_exp h1 frm roots (E s t e) v h2 →
eval_exp h0 frm roots (E s t e) v h2
| eval_cnum_ :
∀
frm roots z h s t,
eval_exp h frm roots (E s t (CNum z)) (NumV z) h
| eval_true_ :
∀
frm roots h s t,
eval_exp h frm roots (E s t CTrue) (BoolV true) h
| eval_false_:
∀
frm roots h s t,
eval_exp h frm roots (E s t CFalse) (BoolV false) h
| eval_plus_:
∀
frm roots e1 e2 z1 z2 h0 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 (NumV z2) h2),
eval_exp h0 frm roots (E s t (Plus e1 e2)) (NumV (z1+z2)%Z) h2
| eval_plus_b1 :
∀
frm roots e1 e2 h0 v1 h1 s t
(EVALL: eval_exp h0 frm roots e1 v1 h1)
(ABORTL: ∀ z1, v1 ≠ NumV z1),
eval_exp h0 frm roots (E s t (Plus e1 e2)) (abort v1) h1
| eval_plus_b2 :
∀
frm roots e1 e2 h0 z1 v2 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 v2 h2)
(ABORTR: ∀ z2, v2 ≠ NumV z2),
eval_exp h0 frm roots (E s t (Plus e1 e2)) (abort v2) h2
| eval_gt_:
∀
frm roots e1 e2 z1 z2 h0 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 (NumV z2) h2),
eval_exp h0 frm roots (E s t (Gt e1 e2)) (BoolV (Z.gtb z1 z2)) h2
| eval_gt_b1 :
∀
frm roots e1 e2 h0 v1 h1 s t
(EVALL: eval_exp h0 frm roots e1 v1 h1)
(ABORTL:∀ z1, v1 ≠ NumV z1),
eval_exp h0 frm roots (E s t (Gt e1 e2)) (abort v1) h1
| eval_gt_b2 :
∀
frm roots e1 e2 h0 z1 v2 h1 h2 s t
(EVALL: eval_exp h0 frm roots e1 (NumV z1) h1)
(EVALR: eval_exp h1 frm roots e2 v2 h2)
(ABORTR: ∀ z2, v2 ≠ NumV z2),
eval_exp h0 frm roots (E s t (Gt e1 e2)) (abort v2) h2
| eval_lhs_:
∀
frm roots s t lhs h0 h1 ff d v
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(GET: getSlot h1 ff d v),
eval_exp h0 frm roots (E s t (Lhs lhs)) v h1
| eval_lhs_b1 :
∀
frm roots lhs h0 s t h1 q
(EVLHS: eval_lhs h0 frm roots lhs (AbortAV q) h1),
eval_exp h0 frm roots (E s t (Lhs lhs)) (AbortV q) h1
| eval_lhs_b2 :
∀
frm roots s t lhs h0 h1 ff d
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(GET: ∀ v, ¬ getSlot h1 ff d v),
eval_exp h0 frm roots (E s t (Lhs lhs)) (AbortV Wrong) h1
| eval_fn_ :
∀
frm roots h s t ds e,
eval_exp h frm roots (E s t (Fn ds e)) (ClosV ds e frm) h
| eval_app :
∀
frm roots h0 h1 h2 h3 h4 e1 e2s s t vb ff sf f e ds
(EVAL1: eval_exp h0 frm roots 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::roots) f ds e2s UnitAV h3)
(EVALBODY: eval_exp h3 f (frm::roots) e vb h4),
eval_exp h0 frm roots (E s t (App e1 e2s)) vb h4
| eval_app_dfun :
∀
h0 frm roots h1 s t e1 e2s v
(EVAL1: eval_exp h0 frm roots e1 (DefFunV v) h1),
eval_exp h0 frm roots (E s t (App e1 e2s)) v h1
| eval_app_b1 :
∀
h0 frm roots v1 h1 s t e1 e2s
(EVAL1: eval_exp h0 frm roots e1 v1 h1)
(ABORT1: match v1 with
| ClosV _ _ _ ⇒ False
| DefFunV _ ⇒ False
| _ ⇒ True
end),
eval_exp h0 frm roots (E s t (App e1 e2s)) (abort v1) h1
| eval_app_b2 :
∀
h0 frm roots e1 h1 e2s h2 h3 s t ds e ff sf f q
(EVAL1: eval_exp h0 frm roots 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::roots) f ds e2s (AbortAV q) h3),
eval_exp h0 frm roots (E s t (App e1 e2s)) (AbortV q) h3
| eval_letpar_ :
∀
frm roots 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::roots) ff ds es UnitAV h2)
(EVAL2: eval_exp h2 ff (frm::roots) e2 v2 h3),
eval_exp h0 frm roots (E s t (LetPar lb e2)) v2 h3
| eval_letpar_b1 :
∀
frm roots 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::roots) ff ds es (AbortAV q) h2),
eval_exp h0 frm roots (E s t (LetPar lb e2)) (AbortV q) h2
| eval_letseq_ :
∀
frm roots h0 h1 h2 lb ds es e2 v2 s t fi
(UNZIP: unzipb lb = (ds, es))
(EVAL1: fill_slots_seq h0 frm roots ds es (FrameAV fi) h1)
(EVAL2: eval_exp h1 fi (frm::roots) e2 v2 h2),
eval_exp h0 frm roots (E s t (LetSeq lb e2)) v2 h2
| eval_letseq_b1 :
∀
frm roots h0 h1 lb ds es e2 s t q
(UNZIP: unzipb lb = (ds, es))
(ABORT1 : fill_slots_seq h0 frm roots ds es (AbortAV q) h1),
eval_exp h0 frm roots (E s t (LetSeq lb e2)) (AbortV q) h1
| eval_letrec_ :
∀
frm roots 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 (frm::roots) ds evs UnitAV h2)
(EVAL2: eval_exp h2 ff (frm::roots) e2 v2 h3),
eval_exp h0 frm roots (E s t (LetRec lvb e2)) v2 h3
| eval_letrec_b1 :
∀
frm roots 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 (frm::roots) ds es (AbortAV q) h2),
eval_exp h0 frm roots (E s t (LetRec lb e2)) (AbortV q) h2
| eval_asgn_ :
∀
h0 frm roots s t lhs e h1 h2 ff d v h3
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(EVAL: eval_exp h1 frm (ff::roots) e v h2)
(SET: setSlot h2 ff d v h3),
eval_exp h0 frm roots (E s t (Asgn lhs e)) v h3
| eval_asgn_b1 :
∀
h0 frm roots s t lhs e h1 q
(EVAL: eval_lhs h0 frm roots lhs (AbortAV q) h1),
eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV q) h1
| eval_asgn_b2 :
∀
h0 frm roots s t lhs e h1 ff d q h2
(EVAL: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(ABORT: eval_exp h1 frm (ff::roots) e (AbortV q) h2),
eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV q) h2
| eval_asgn_b3 :
∀
h0 frm roots s t lhs e h1 h2 ff d v
(EVLHS: eval_lhs h0 frm roots lhs (AddrAV (Addr_ ff d)) h1)
(EVAL: eval_exp h1 frm (ff::roots) e v h2)
(SET: ∀ h3, ¬ setSlot h2 ff d v h3),
eval_exp h0 frm roots (E s t (Asgn lhs e)) (AbortV Wrong) h2
| eval_if_t :
∀
frm roots e1 e2 e3 v h0 h1 h2 s t
(EVAL1: eval_exp h0 frm roots e1 (BoolV true) h1)
(EVAL2: eval_exp h1 frm roots e2 v h2),
eval_exp h0 frm roots (E s t (If e1 e2 e3)) v h2
| eval_if_f :
∀
frm roots e1 e2 e3 v h0 h1 h2 s t
(EVAL1: eval_exp h0 frm roots e1 (BoolV false) h1)
(EVAL3: eval_exp h1 frm roots e3 v h2),
eval_exp h0 frm roots (E s t (If e1 e2 e3)) v h2
| eval_if_b1:
∀
frm roots e1 e2 e3 h0 h1 v1 s t
(EVAL1: eval_exp h0 frm roots e1 v1 h1)
(ABORT1: ∀ b, v1 ≠ BoolV b),
eval_exp h0 frm roots (E s t (If e1 e2 e3)) (abort v1) h1
| eval_seq_ :
∀
frm roots e1 e2 v1 v2 h0 h1 h2 s t
(EVAL1: eval_exp h0 frm roots e1 v1 h1)
(GOOD1: good v1)
(EVAL2: eval_exp h1 frm roots e2 v2 h2),
eval_exp h0 frm roots (E s t (Seq e1 e2)) v2 h2
| eval_seq_b1 :
∀
frm roots e1 e2 h0 h1 s t q
(EVAL1: eval_exp h0 frm roots e1 (AbortV q) h1),
eval_exp h0 frm roots (E s t (Seq e1 e2)) (AbortV q) h1
| eval_new_ :
∀
frm roots 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 roots (E s t (New r)) (RecordV rf) h1
| eval_new_b1 :
∀
frm roots r h0 s t
(RLOOK: ∀ p s' d' s0, ¬ (rlookup r p s' d' ∧ assocScope d' s0)),
eval_exp h0 frm roots (E s t (New r)) (AbortV Wrong) h0
with eval_lhs : H → FrameId → list FrameId → lhs → AuxV → H → Prop :=
| eval_lhs_var_ :
∀
h frm roots r a
(ADDR: getAddr h frm r a),
eval_lhs h frm roots (Var r) (AddrAV a) h
| eval_lhs_var_b :
∀
h frm roots r
(ADDR: ∀ a, ¬ getAddr h frm r a),
eval_lhs h frm roots (Var r) (AbortAV Wrong) h
| eval_lhs_field :
∀
h0 frm roots e r s rf scf h1 h2 a sf
(EVAL: eval_exp h0 frm roots 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 roots (Field e r) (AddrAV a) h2
| eval_lhs_field_null :
∀
h0 frm roots e r h1
(EVAL: eval_exp h0 frm roots e NullV h1),
eval_lhs h0 frm roots (Field e r) (AbortAV NullPointer) h1
| eval_lhs_field_b1:
∀
h0 frm roots e r h1 v
(EVAL: eval_exp h0 frm roots e v h1)
(BAD: match v with
| RecordV _ ⇒ False
| NullV ⇒ False
| _ ⇒ True
end),
eval_lhs h0 frm roots (Field e r) (aborta v) h1
| eval_lhs_field_b2:
∀
h0 frm roots e r s rf scf h1 h2 sf
(EVAL: eval_exp h0 frm roots 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 roots (Field e r) (AbortAV Wrong) h2
with fill_slots_par : H → FrameId → list FrameId → FrameId → list D → list exp → AuxV → H → Prop :=
| fill_par_nil :
∀
h frm roots fc,
fill_slots_par h frm roots fc nil nil UnitAV h
| fill_par_b1 :
∀
h frm roots fc ld,
ld ≠ nil →
fill_slots_par h frm roots fc ld nil (AbortAV Wrong) h
| fill_par_b2 :
∀
h frm roots fc le,
le ≠ nil →
fill_slots_par h frm roots fc nil le (AbortAV Wrong) h
| fill_par_cons :
∀
h0 frm roots e d es ds fc v h1 h2 h3 v1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: setSlot h1 fc d v h2)
(TAIL: fill_slots_par h2 frm roots fc ds es v1 h3),
fill_slots_par h0 frm roots fc (d::ds) (e::es) v1 h3
| fill_par_cons_b1 :
∀
h0 frm roots e es d ds fc h1 q
(EVAL: eval_exp h0 frm roots e (AbortV q) h1),
fill_slots_par h0 frm roots fc (d :: ds) (e :: es) (AbortAV q) h1
| fill_par_cons_b2 :
∀
h0 frm roots e d es ds fc v h1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: ∀ h2, ¬ setSlot h1 fc d v h2),
fill_slots_par h0 frm roots fc (d::ds) (e::es) (AbortAV Wrong) h1
with fill_slots_seq : H → FrameId → list FrameId → list D → list exp → AuxV → H → Prop :=
| fill_seq_nil :
∀
h frm roots,
fill_slots_seq h frm roots nil nil (FrameAV frm) h
| fill_seq_b1 :
∀
h frm roots ld,
ld ≠ nil →
fill_slots_seq h frm roots ld nil (AbortAV Wrong) h
| fill_seq_b2 :
∀
h frm roots le,
le ≠ nil →
fill_slots_seq h frm roots nil le (AbortAV Wrong) h
| fill_seq_cons :
∀
h0 frm roots 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 (fc::roots) e v h2)
(GOOD: good v)
(SS: setSlot h2 fc d v h3)
(TAIL: fill_slots_seq h3 fc (frm::roots) ds es v1 h4),
fill_slots_seq h0 frm roots (d :: ds) (e :: es) v1 h4
| fill_seq_cons_b1 :
∀
h0 frm roots 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 (fc::roots) e (AbortV q) h2),
fill_slots_seq h0 frm roots (d :: ds) (e :: es) (AbortAV q) h2
| fill_seq_cons_b2 :
∀
h0 frm roots 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 (fc::roots) e v h2)
(GOOD: good v)
(SS: ∀ h3, ¬ setSlot h2 fc d v h3),
fill_slots_seq h0 frm roots (d :: ds) (e :: es) (AbortAV Wrong) h2
with fill_slots_rec : H → FrameId → list FrameId → list D → list exp → AuxV → H → Prop :=
| fill_rec_nil :
∀
h frm roots,
fill_slots_rec h frm roots nil nil UnitAV h
| fill_rec_b1 :
∀
h frm roots ld,
ld ≠ nil →
fill_slots_rec h frm roots ld nil (AbortAV Wrong) h
| fill_rec_b2 :
∀
h frm roots le,
le ≠ nil →
fill_slots_rec h frm roots nil le (AbortAV Wrong) h
| fill_rec_cons :
∀
h0 frm roots e d es ds v h1 h2 h3 v1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: setSlot h1 frm d v h2)
(TAIL: fill_slots_rec h2 frm roots ds es v1 h3),
fill_slots_rec h0 frm roots (d::ds) (e::es) v1 h3
| fill_rec_cons_b1 :
∀
h0 frm roots e es d ds h1 q
(EVAL: eval_exp h0 frm roots e (AbortV q) h1),
fill_slots_rec h0 frm roots (d :: ds) (e :: es) (AbortAV q) h1
| fill_rec_cons_b2 :
∀
h0 frm roots e d es ds v h1 v1
(EVAL: eval_exp h0 frm roots e v h1)
(GOOD: good v)
(SS: ∀ h2, ¬ setSlot h1 frm d v h2),
fill_slots_rec h0 frm roots (d::ds) (e::es) v1 h1
.
Scheme eval_exp_ind2 := Minimality for eval_exp Sort Prop
with eval_lhs_ind2 := Minimality for eval_lhs 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.
Combined Scheme eval_exp_ind3
from eval_exp_ind2, eval_lhs_ind2, fill_par_ind2, fill_seq_ind2, fill_rec_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 nil e v h1),
eval_prog (Prog rds e) v
.
End DynamicSemantics.