Commit eb7871f7 authored by charguer's avatar charguer

lifted_cf

parent 70ec029f
......@@ -16,9 +16,9 @@ SRC := $(shell cat FILES)
SRC := ModelState ModelLambda ModelSepFunctor ModelSepBasic ModelSepCredits ModelSepRO ModelCF ModelCFCredits ModelML ModelSepML ModelCFML ModelSepExamples
#ifeq ($(ARTHUR),1)
# SRC := ModelState ModelSepFunctor ModelML ModelSepML ModelCFML ModelSepExamples
#endif
ifeq ($(ARTHUR),1)
SRC = ModelState ModelSepFunctor ModelML ModelSepML ModelCFML ModelSepExamples
endif
PWD := $(shell pwd)
......
......@@ -495,21 +495,21 @@ Notation "'Let' x ':=' F1 'in' F2" :=
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
Notation "'App' f x1 ;" :=
Notation "'App_' f x1 ;" :=
(local (cf_app f [x1]))
(at level 68, f at level 0, x1 at level 0) : charac.
Notation "'App' f x1 x2 ;" :=
Notation "'App_' f x1 x2 ;" :=
(local (cf_app f [x1; x2]))
(at level 68, f at level 0, x1 at level 0,
x2 at level 0) : charac.
Notation "'App' f x1 x2 x3 ;" :=
Notation "'App_' f x1 x2 x3 ;" :=
(local (cf_app f [x1; x2; x3]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0) : charac.
Notation "'App' f x1 x2 x3 x4 ;" :=
Notation "'App_' f x1 x2 x3 x4 ;" :=
(local (cf_app f [x1; x2; x3; x4]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0, x4 at level 0) : charac.
......
This diff is collapsed.
......@@ -364,6 +364,21 @@ Admitted. (* TODO *)
{ rewrite <- hprop_gc_merge. hhsimpl. }
*)
Lemma rule_seq' : forall t1 t2 H Q Q',
triple t1 H Q' ->
triple t2 (Q' val_unit) Q ->
(forall v, Q' v ==> Q' v \* \[v = val_unit]) ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2 HQ'. intros HF h N.
lets~ (h1'&v1&R1&K1): (rm M1) HF h.
forwards* (h2'&v2&R2&K2): (rm M2) (\GC \* HF) h1'.
{ hhsimpl. hchange HQ'. hsimpl. hpull. intro_subst. hsimpl. }
exists h2' v2. splits~.
{ applys~ red_seq R1 R2. }
{ rewrite <- hprop_gc_merge. hhsimpl. }
Qed.
Lemma rule_seq : forall t1 t2 H Q H',
triple t1 H (fun v => H') ->
triple t2 H' Q ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment