Commit b915f56d authored by charguer's avatar charguer

encoded_while_in_progress

parent ae5eed3c
......@@ -72,7 +72,6 @@ with trm : Type :=
| trm_if : trm -> trm -> trm -> trm
| trm_let : var -> trm -> trm -> trm
| trm_app : trm -> trm -> trm
| trm_while : trm -> trm -> trm
| trm_for : var -> trm -> trm -> trm -> trm
| trm_protect : var -> trm -> trm
| trm_tag : tag -> trm -> trm.
......@@ -111,6 +110,15 @@ Definition is_reserved_var (x:var) : bool :=
Definition trm_seq (t1:trm) (t2:trm) : trm :=
trm_tag tag_seq (trm_let "$_" t1 (trm_protect "$_" t2)).
(** Encoding of while loops *)
Definition trm_while (t1:trm) (t2:trm) : trm :=
let F : var := "$f" in
let U : var := "$_" in
let P t := trm_protect F (trm_protect U t) in
let X : val := val_fix F U (trm_if (P t1) (trm_seq (P t2) (F val_unit)) val_unit) in
trm_tag tag_while (X val_unit).
(* ********************************************************************** *)
(* * Source language semantics *)
......@@ -130,7 +138,6 @@ Fixpoint subst (y:var) (w:val) (t:trm) : trm :=
| trm_if t0 t1 t2 => trm_if (aux t0) (aux t1) (aux t2)
| trm_let x t1 t2 => trm_let x (aux t1) (aux_no_capture x t2)
| trm_app t1 t2 => trm_app (aux t1) (aux t2)
| trm_while t1 t2 => trm_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => trm_for x (aux t1) (aux t2) (aux_no_capture x t3)
| trm_protect x t1 => if eq_var_dec x y then t else trm_protect x (aux t1)
| trm_tag g t1 => trm_tag g (aux t1)
......@@ -216,9 +223,6 @@ Inductive red : state -> trm -> state -> val -> Prop :=
red m (val_ptr_add (val_loc l) (val_int n)) m (val_loc l')
| red_eq : forall m v1 v2,
red m (val_eq v1 v2) m (val_bool (isTrue (v1 = v2)))
| red_while : forall m1 m2 t1 t2 r,
red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r ->
red m1 (trm_while t1 t2) m2 r
| red_for_arg : forall m1 m2 m3 m4 v1 v2 x t1 t2 t3 r,
(* LATER: add [not_is_val t1 \/ not_is_val t2] *)
red m1 t1 m2 v1 ->
......@@ -243,7 +247,8 @@ Inductive red : state -> trm -> state -> val -> Prop :=
(* ---------------------------------------------------------------------- *)
(* ** Derived rules *)
Lemma red_seq : forall m1 m2 m3 t1 t2 r,
(* todo: deprecated *)
Lemma red_seq_unit : forall m1 m2 m3 t1 t2 r,
red m1 t1 m2 val_unit ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
......@@ -252,6 +257,37 @@ Proof using.
simpl. applys* red_protect.
Qed.
Lemma red_seq : forall m1 m2 m3 t1 t2 r1 r,
red m1 t1 m2 r1 ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys red_tag. applys* red_let.
simpl. applys* red_protect.
Qed.
Lemma red_seq_inv : forall m1 m3 t1 t2 r,
red m1 (trm_seq t1 t2) m3 r ->
exists m2 r1, red m1 t1 m2 r1 /\ red m2 t2 m3 r.
Proof using.
introv M. inverts M as ;=> M. inverts M as. introv M1 M2.
inverts M2. eauto.
Qed.
Lemma red_while : forall m1 m2 t1 t2 r,
red m1 (trm_if t1 (trm_seq t2 (trm_while t1 t2)) val_unit) m2 r ->
red m1 (trm_while t1 t2) m2 r.
Proof using.
introv M1. unfold trm_while. applys red_tag. applys* red_app_fix.
simpl. inverts M1 as. introv M1 M2. applys red_if.
{ do 2 applys* red_protect. }
{ case_if.
{ lets (m'&r'&M2'&M3'): red_seq_inv (rm M2). applys red_seq.
{ do 2 applys* red_protect. }
{ inverts M3' as; => M4. applys M4. } }
{ auto. } }
Qed.
Lemma red_ptr_add_nat : forall m l (f : nat),
red m (val_ptr_add (val_loc l) (val_int f)) m (val_loc (l+f)%nat).
Proof using. intros. applys* red_ptr_add. math. Qed.
......@@ -557,7 +593,6 @@ Fixpoint trm_size (t:trm) : nat :=
| trm_if t0 t1 t2 => 1 + trm_size t0 + trm_size t1 + trm_size t2
| trm_let x t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_app t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_while t1 t2 => 1 + trm_size t1 + trm_size t2
| trm_for x t1 t2 t3 => 1 + trm_size t1 + trm_size t2 + trm_size t3
| trm_tag g t1 => 1 + trm_size t1
| trm_protect x t1 => 1 + trm_size t1
......@@ -733,6 +768,16 @@ Ltac substs_simpl_proof :=
intros E; induction E as [|(x,w) E' IH]; intros; simpl;
[ | try rewrite IH ]; auto.
Lemma substs_tag : forall E g t1,
substs E (trm_tag g t1)
= trm_tag g (substs E t1).
Proof using. substs_simpl_proof. Qed.
Lemma substs_protect : forall E x t1,
substs E (trm_protect x t1)
= trm_protect x (substs (ctx_rem x E) t1).
Proof using. substs_simpl_proof. case_if; rewrite~ IH. Qed.
Lemma substs_val : forall E v,
substs E (trm_val v) = v.
Proof using. substs_simpl_proof. Qed.
......
......@@ -529,6 +529,27 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Term rules *)
Lemma rule_red : forall t1 t2 H Q,
(forall m m' r, red m t1 m' r -> red m t2 m' r) ->
triple t1 H Q ->
triple t2 H Q.
Proof using.
introv T M. intros Hf h N. lets~ (h'&v&R&K): (rm M) Hf h.
exists h' v. splits~.
Qed.
Lemma rule_tag : forall g t1 H Q,
triple t1 H Q ->
triple (trm_tag g t1) H Q.
Proof using. introv M. applys rule_red M. applys red_tag. Qed.
Lemma rule_protect : forall x t1 H Q,
triple t1 H Q ->
triple (trm_protect x t1) H Q.
Proof using. introv M. applys rule_red M. applys red_protect. Qed.
Lemma rule_val : forall v H Q,
H ==> Q v ->
triple (trm_val v) H Q.
......@@ -587,7 +608,8 @@ Proof using.
{ intros v' N. hpull. intros E. inverts~ E. false N. hnfs*. }
Qed.
Lemma rule_seq : forall t1 t2 H Q Q1,
(* todo: deprecated *)
Lemma rule_seq_unit : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall v, ~ is_val_unit v -> (Q1 v) ==> \[False]) ->
triple t2 (Q1 val_unit) Q ->
......@@ -604,7 +626,7 @@ Proof using.
(* LATER: shorten this, and factorize with rule_if *)
subst. forwards* (h2'&v2&R2&K2): (rm M3) (\Top \* HF) h1'.
exists h2' v2. splits~.
{ applys~ red_seq R2. }
{ applys~ red_seq_unit R2. }
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
......@@ -621,6 +643,16 @@ Proof using.
{ rewrite <- htop_hstar_htop. hhsimpl. }
Qed.
Lemma rule_seq : forall t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple t2 (Q1 X) Q) ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2. unfold trm_seq. apply rule_tag. applys rule_let.
{ applys M1. }
{ simpl. intros. applys rule_protect. applys M2. }
Qed.
Lemma rule_apps_funs : forall xs F (Vs:vals) t1 H Q,
F = (val_funs xs t1) ->
var_funs (length Vs) xs ->
......@@ -1066,14 +1098,14 @@ Proof using.
{ applys* red_if_bool. } }
Qed.
(** An alternative statement for [rule_seq] *)
(** An alternative statement for [rule_seq_unit] -- deprecated *)
Lemma rule_seq' : forall t1 t2 H Q H1,
Lemma rule_seq_unit' : forall t1 t2 H Q H1,
triple t1 H (fun r => \[r = val_unit] \* H1) ->
triple t2 H1 Q ->
triple (trm_seq t1 t2) H Q.
Proof using.
introv M1 M2. applys rule_seq.
introv M1 M2. applys rule_seq_unit.
{ applys M1. }
{ intros v E. hpull; false. }
{ applys rule_extract_hprop. intros. applys M2. }
......
......@@ -17,16 +17,6 @@ Implicit Types v w : val.
Implicit Types t : trm.
(* todo: move *)
Lemma red_seq' : forall m1 m2 m3 t1 t2 r1 r,
red m1 t1 m2 r1 ->
red m2 t2 m3 r ->
red m1 (trm_seq t1 t2) m3 r.
Proof using.
introv M1 M2. applys red_tag. applys* red_let.
simpl. applys* red_protect.
Qed.
(* ********************************************************************** *)
......@@ -233,6 +223,7 @@ Definition wp_var (E:ctx) (x:var) : formula :=
| Some v => (fun Q => Q v)
end).
Fixpoint wp (E:ctx) (t:trm) : formula :=
let aux := wp E in
match t with
......@@ -243,15 +234,23 @@ Fixpoint wp (E:ctx) (t:trm) : formula :=
| trm_if t0 t1 t2 => wp_if (aux t0) (aux t1) (aux t2)
| trm_let x t1 t2 => wp_let (aux t1) (fun X => wp (ctx_add x X E) t2)
| trm_app t1 t2 => local (weakestpre (triple (substs E t)))
| trm_while t1 t2 => wp_while (aux t1) (aux t2)
| trm_for x t1 t2 t3 => wp_for' (aux t1) (aux t2) (fun X => wp (ctx_add x X E) t3)
| trm_protect x t1 => wp (ctx_rem x E) t1
| trm_tag g t0 =>
match g, t0 with
(*| tag_seq, trm_let "$_" t1 (trm_protect "$_" t2) =>
wp_seq' (aux t1) (wp (ctx_rem "$_" E) t2) *)
| tag_seq, trm_let x t1 (trm_protect y t2) =>
if eq_var_dec x y
then wp_seq' (aux t1) (wp (ctx_rem x E) t2)
else wp_fail
else wp_fail
(*
| tag_while, trm_app (val_fix "$f" "$_" (trm_if (trm_protect "$f" (trm_protect "$_" t1))
(trm_let "$_" (trm_protect "$f" (trm_protect U t2))
((trm_protect "$_" t2 (trm_app "$f" val_unit)))
val_unit)) val_unit =>
let aux := wp (ctx_rem "$_" (ctx_rem "$f" E)) in
wp_while (aux t1) (aux t2)*)
| _,_ => wp_fail
end
end.
......@@ -358,39 +357,6 @@ Lemma triple_wp_fail : forall t Q,
Proof using. intros. remove_local. intros. false. Qed.
(* TODO move *)
Lemma substs_tag : forall E g t1,
substs E (trm_tag g t1)
= trm_tag g (substs E t1).
Proof using. substs_simpl_proof. Qed.
Lemma substs_protect : forall E x t1,
substs E (trm_protect x t1)
= trm_protect x (substs (ctx_rem x E) t1).
Proof using. substs_simpl_proof. case_if; rewrite~ IH. Qed.
Lemma rule_red : forall t1 t2 H Q,
(forall m m' r, red m t1 m' r -> red m t2 m' r) ->
triple t1 H Q ->
triple t2 H Q.
Proof using.
introv T M. intros Hf h N. lets~ (h'&v&R&K): (rm M) Hf h.
exists h' v. splits~.
Qed.
Lemma rule_tag : forall g t1 H Q,
triple t1 H Q ->
triple (trm_tag g t1) H Q.
Proof using. introv M. applys rule_red M. applys red_tag. Qed.
Lemma rule_protect : forall x t1 H Q,
triple t1 H Q ->
triple (trm_protect x t1) H Q.
Proof using. introv M. applys rule_red M. applys red_protect. Qed.
Lemma triple_wp : forall t E Q,
triple (substs E t) (wp E t Q) Q.
Proof using.
......
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