Library langs.L2.well_boundness
Well-bounded L2 expressions, declarations and programs, as in
paper Fig. 17.
Context `{G: Graph (@AT T)}.
Inductive wb_exp : exp → Prop :=
| wb_cnum :
∀ s t z,
wb_exp (E s t (CNum z))
| wb_ctrue :
∀ s t,
wb_exp (E s t CTrue)
| wb_cfalse :
∀ s t,
wb_exp (E s t CFalse)
| wb_plus :
∀
s t s1 t1 e1 s2 t2 e2
(WB1: wb_exp (E s1 t1 e1))
(WB2:wb_exp (E s2 t2 e2)),
s = s2 →
s = s1 →
wb_exp (E s t (Plus (E s1 t1 e1) (E s2 t2 e2)))
| wb_gt :
∀
s t s1 t1 e1 s2 t2 e2
(WB1: wb_exp (E s1 t1 e1))
(WB2: wb_exp (E s2 t2 e2)),
s = s1 →
s = s2 →
wb_exp (E s t (Gt (E s1 t1 e1) (E s2 t2 e2)))
| wb_lhs_ :
∀
s t lhs
(WB: wb_lhs s lhs),
wb_exp (E s t (Lhs lhs))
| wb_fn :
∀
s t ds s1 t1 e1
(WB1: wb_exp (E s1 t1 e1))
(PS: linksofScopeP s1 [(P, [s])])
(DS: declsofScopeP s1 ds),
wb_exp (E s t (Fn ds (E s1 t1 e1)))
| wb_app :
∀
s t s1 t1 e1 s2 e2s
(WB1: wb_exp (E s1 t1 e1))
(WB2: ∀ e2,
In e2 e2s →
(expScope e2) = s2 ∧
wb_exp e2),
s = s1 →
s = s2 →
wb_exp (E s t (App (E s1 t1 e1) e2s))
| wb_letpar :
∀
s t s1 bs ds e1s s2 t2 e2
(UNZIP: unzipb bs = (ds,e1s))
(WB1: ∀ e1,
In e1 e1s →
(expScope e1) = s1 ∧
wb_exp e1)
(PS: linksofScopeP s2 [(P, [s])])
(DS: declsofScopeP s2 ds)
(WB2:wb_exp (E s2 t2 e2)),
s = s1 →
wb_exp (E s t (LetPar bs (E s2 t2 e2)))
| wb_letseq :
∀
s t bs ds e1s s2 t2 e2
(UNZIP: unzipb bs = (ds, e1s))
(WB1: ForallFold2 (fun d e ps newPs ⇒
(linksofScopeP newPs [(P, [ps])]) ∧
declsofScopeP newPs [d] ∧
(expScope e) = ps ∧
wb_exp e)
ds e1s s s2)
(WB2:wb_exp (E s2 t2 e2)),
wb_exp (E s t (LetSeq bs (E s2 t2 e2)))
| wb_letrec :
∀
s t bs ds e1s s2 t2 e2
(UNZIP: unzipb bs = (ds,e1s))
(WB1: ∀ e1,
In e1 e1s →
(expScope e1) = s2 ∧ wb_exp e1)
(LS: linksofScopeP s2 [(P, [s])])
(DS: declsofScopeP s2 ds)
(WB2: wb_exp (E s2 t2 e2)),
wb_exp (E s t (LetRec bs (E s2 t2 e2)))
| wb_asgn :
∀
s t s1 t1 e1 lhs
(WB1: wb_lhs s1 lhs)
(WB2: wb_exp (E s1 t1 e1)),
s = s1 →
wb_exp (E s t (Asgn lhs (E s1 t1 e1)))
| wb_if : ∀
s t s1 t1 e1 s2 t2 e2 s3 t3 e3
(WB1: wb_exp (E s1 t1 e1))
(WB2: wb_exp (E s2 t2 e2))
(WB3: wb_exp (E s3 t3 e3)),
s = s1 →
s = s2 →
s = s3 →
wb_exp (E s t (If (E s1 t1 e1) (E s2 t2 e2) (E s3 t3 e3)))
| wb_seq :
∀
s t s1 t1 e1 s2 t2 e2
(WB1: wb_exp (E s1 t1 e1))
(WB2: wb_exp (E s2 t2 e2)),
s = s1 →
s = s2 →
wb_exp (E s t (Seq (E s1 t1 e1) (E s2 t2 e2)))
| wb_new :
∀
s t r srec p s' d'
(SR: scopeofRefP r s)
(SR: rlookup r p s' d')
(ASC: assocScope d' srec)
(PS: linksofScopeP srec []),
wb_exp (E s t (New r))
with wb_lhs : ScopeId → lhs → Prop :=
| wb_lhs_var :
∀
s r
(SR: scopeofRefP r s),
wb_lhs s (Var r)
| wb_lhs_field :
∀
s e r srec s'
(WB: wb_exp e)
(ES: expScope e = s)
(SR: scopeofRefP r s')
(LS: linksofScopeP s' [(I,[srec])])
(DSs: declsofScopeP s' []),
wb_lhs s (Field e r)
.
Inductive wb_dec : ScopeId → decl → Prop :=
| wb_rec_dec :
∀
d lf s s'
(DS: scopeofDeclP d s)
(SD: assocScope d s')
(WS: ∀ fd,
In fd lf →
scopeofDeclP (fldDecl fd) s'),
wb_dec s (Rdef d lf)
.
Inductive wb_prog : prog → Prop :=
| wb_prog_ :
∀
decs s t e
(WBD: ∀ dec,
In dec decs →
wb_dec s dec)
(WBE: wb_exp (E s t e))
(LS : linksofScopeP s []),
wb_prog (Prog decs (E s t e))
.
End WellBoundness.