Commit 2b80e398 authored by Ralf Jung's avatar Ralf Jung

tweak heap_lang sugar

parent 24fa20e5
...@@ -7,8 +7,6 @@ Definition loc := positive. (* Really, any countable type. *) ...@@ -7,8 +7,6 @@ Definition loc := positive. (* Really, any countable type. *)
Inductive base_lit : Set := Inductive base_lit : Set :=
| LitNat (n : nat) | LitBool (b : bool) | LitUnit. | LitNat (n : nat) | LitBool (b : bool) | LitUnit.
Notation LitTrue := (LitBool true).
Notation LitFalse := (LitBool false).
Inductive un_op : Set := Inductive un_op : Set :=
| NegOp. | NegOp.
Inductive bin_op : Set := Inductive bin_op : Set :=
...@@ -179,9 +177,9 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop := ...@@ -179,9 +177,9 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
bin_op_eval op l1 l2 = Some l' bin_op_eval op l1 l2 = Some l'
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
| IfTrueS e1 e2 σ : | IfTrueS e1 e2 σ :
head_step (If (Lit LitTrue) e1 e2) σ e1 σ None head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
| IfFalseS e1 e2 σ : | IfFalseS e1 e2 σ :
head_step (If (Lit LitFalse) e1 e2) σ e2 σ None head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
| FstS e1 v1 e2 v2 σ : | FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
head_step (Fst (Pair e1 e2)) σ e1 σ None head_step (Fst (Pair e1 e2)) σ e1 σ None
...@@ -208,11 +206,11 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop := ...@@ -208,11 +206,11 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
| CasFailS l e1 v1 e2 v2 vl σ : | CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some vl vl v1 σ !! l = Some vl vl v1
head_step (Cas (Loc l) e1 e2) σ (Lit LitFalse) σ None head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
| CasSucS l e1 v1 e2 v2 σ : | CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1 σ !! l = Some v1
head_step (Cas (Loc l) e1 e2) σ (Lit LitTrue) (<[l:=v2]>σ) None. head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
(** Atomic expressions *) (** Atomic expressions *)
Definition atomic (e: expr) : Prop := Definition atomic (e: expr) : Prop :=
......
...@@ -121,18 +121,18 @@ Qed. ...@@ -121,18 +121,18 @@ Qed.
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q : Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v' v' v1 to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v' v' v1
(ownP σ (ownP σ - Q (LitV LitFalse))) wp E (Cas (Loc l) e1 e2) Q. (ownP σ (ownP σ - Q (LitV $ LitBool false))) wp E (Cas (Loc l) e1 e2) Q.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitFalse) σ None) intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None)
?right_id //; last by intros; inv_step; eauto. ?right_id //; last by intros; inv_step; eauto.
Qed. Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q : Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v1 to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v1
(ownP σ (ownP (<[l:=v2]>σ) - Q (LitV LitTrue))) (ownP σ (ownP (<[l:=v2]>σ) - Q (LitV $ LitBool true)))
wp E (Cas (Loc l) e1 e2) Q. wp E (Cas (Loc l) e1 e2) Q.
Proof. Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitTrue) (<[l:=v2]>σ) None) intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
?right_id //; last by intros; inv_step; eauto. ?right_id //; last by intros; inv_step; eauto.
Qed. Qed.
...@@ -177,13 +177,13 @@ Proof. ...@@ -177,13 +177,13 @@ Proof.
?right_id -?wp_value' //; intros; inv_step; eauto. ?right_id -?wp_value' //; intros; inv_step; eauto.
Qed. Qed.
Lemma wp_if_true E e1 e2 Q : wp E e1 Q wp E (If (Lit LitTrue) e1 e2) Q. Lemma wp_if_true E e1 e2 Q : wp E e1 Q wp E (If (Lit $ LitBool true) e1 e2) Q.
Proof. Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None) rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
?right_id //; intros; inv_step; eauto. ?right_id //; intros; inv_step; eauto.
Qed. Qed.
Lemma wp_if_false E e1 e2 Q : wp E e2 Q wp E (If (Lit LitFalse) e1 e2) Q. Lemma wp_if_false E e1 e2 Q : wp E e2 Q wp E (If (Lit $ LitBool false) e1 e2) Q.
Proof. Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None) rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
?right_id //; intros; inv_step; eauto. ?right_id //; intros; inv_step; eauto.
......
Require Export heap_lang.heap_lang heap_lang.lifting. Require Export heap_lang.heap_lang heap_lang.lifting.
Import uPred heap_lang. Import uPred heap_lang.
(** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *) (** Define some syntactic sugar. *)
Notation Lam x e := (Rec "" x e). Notation Lam x e := (Rec "" x e).
Notation Let x e1 e2 := (App (Lam x e2) e1). Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let "" e1 e2). Notation Seq e1 e2 := (Let "" e1 e2).
...@@ -11,7 +11,7 @@ Notation SeqCtx e2 := (LetCtx "" e2). ...@@ -11,7 +11,7 @@ Notation SeqCtx e2 := (LetCtx "" e2).
Module notations. Module notations.
Delimit Scope lang_scope with L. Delimit Scope lang_scope with L.
Bind Scope lang_scope with expr. Bind Scope lang_scope with expr val.
Arguments wp {_ _} _ _%L _. Arguments wp {_ _} _ _%L _.
Coercion LitNat : nat >-> base_lit. Coercion LitNat : nat >-> base_lit.
...@@ -20,11 +20,12 @@ Module notations. ...@@ -20,11 +20,12 @@ Module notations.
apart language and Coq expressions. *) apart language and Coq expressions. *)
Coercion Var : string >-> expr. Coercion Var : string >-> expr.
Coercion App : expr >-> Funclass. Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *) first. *)
(* What about Arguments for hoare triples?. *) (* What about Arguments for hoare triples?. *)
Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope. Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope. Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope. Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L) Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
...@@ -52,8 +53,9 @@ Module notations. ...@@ -52,8 +53,9 @@ Module notations.
Notation "e1 ; e2" := (Lam "" e2%L e1%L) Notation "e1 ; e2" := (Lam "" e2%L e1%L)
(at level 100, e2 at level 200) : lang_scope. (at level 100, e2 at level 200) : lang_scope.
End notations. End notations.
Export notations.
Section suger. Section sugar.
Context {Σ : iFunctor}. Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ. Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ. Implicit Types Q : val iProp heap_lang Σ.
...@@ -79,7 +81,7 @@ Qed. ...@@ -79,7 +81,7 @@ Qed.
Lemma wp_le E (n1 n2 : nat) P Q : Lemma wp_le E (n1 n2 : nat) P Q :
(n1 n2 P Q (LitV true)) (n1 n2 P Q (LitV true))
(n1 > n2 P Q (LitV false)) (n1 > n2 P Q (LitV false))
P wp E (BinOp LeOp (Lit n1) (Lit n2)) Q. P wp E ('n1 'n2) Q.
Proof. Proof.
intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 n2)); by eauto with omega. destruct (bool_decide_reflect (n1 n2)); by eauto with omega.
...@@ -88,7 +90,7 @@ Qed. ...@@ -88,7 +90,7 @@ Qed.
Lemma wp_lt E (n1 n2 : nat) P Q : Lemma wp_lt E (n1 n2 : nat) P Q :
(n1 < n2 P Q (LitV true)) (n1 < n2 P Q (LitV true))
(n1 n2 P Q (LitV false)) (n1 n2 P Q (LitV false))
P wp E (BinOp LtOp (Lit n1) (Lit n2)) Q. P wp E ('n1 < 'n2) Q.
Proof. Proof.
intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 < n2)); by eauto with omega. destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
...@@ -97,10 +99,10 @@ Qed. ...@@ -97,10 +99,10 @@ Qed.
Lemma wp_eq E (n1 n2 : nat) P Q : Lemma wp_eq E (n1 n2 : nat) P Q :
(n1 = n2 P Q (LitV true)) (n1 = n2 P Q (LitV true))
(n1 n2 P Q (LitV false)) (n1 n2 P Q (LitV false))
P wp E (BinOp EqOp (Lit n1) (Lit n2)) Q. P wp E ('n1 = 'n2) Q.
Proof. Proof.
intros. rewrite -wp_bin_op //; []. intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 = n2)); by eauto with omega. destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
Qed. Qed.
End suger. End sugar.
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
Require Import program_logic.ownership. Require Import program_logic.ownership.
Require Import heap_lang.lifting heap_lang.sugar. Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang uPred notations. Import heap_lang uPred.
Module LangTests. Module LangTests.
Definition add := ('21 + '21)%L. Definition add := ('21 + '21)%L.
...@@ -11,13 +11,13 @@ Module LangTests. ...@@ -11,13 +11,13 @@ Module LangTests.
Goal σ, prim_step rec_app σ rec_app σ None. Goal σ, prim_step rec_app σ rec_app σ None.
Proof. Proof.
intros. rewrite /rec_app. (* FIXME: do_step does not work here *) intros. rewrite /rec_app. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ (LitV (LitNat 0))). by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ '0)%L.
Qed. Qed.
Definition lam : expr := λ: "x", "x" + '21. Definition lam : expr := λ: "x", "x" + '21.
Goal σ, prim_step (lam '21)%L σ add σ None. Goal σ, prim_step (lam '21)%L σ add σ None.
Proof. Proof.
intros. rewrite /lam. (* FIXME: do_step does not work here *) intros. rewrite /lam. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + '21) _ (LitV 21)). by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + '21) _ '21)%L.
Qed. Qed.
End LangTests. End LangTests.
...@@ -28,7 +28,7 @@ Module LiftingTests. ...@@ -28,7 +28,7 @@ Module LiftingTests.
Definition e : expr := Definition e : expr :=
let: "x" := ref '1 in "x" <- !"x" + '1; !"x". let: "x" := ref '1 in "x" <- !"x" + '1; !"x".
Goal σ E, ownP (Σ:=Σ) σ wp E e (λ v, v = LitV 2). Goal σ E, ownP (Σ:=Σ) σ wp E e (λ v, v = ('2)%L).
Proof. Proof.
move=> σ E. rewrite /e. move=> σ E. rewrite /e.
rewrite -(wp_bindi (LetCtx _ _)) -wp_alloc_pst //=. rewrite -(wp_bindi (LetCtx _ _)) -wp_alloc_pst //=.
...@@ -97,7 +97,7 @@ Module LiftingTests. ...@@ -97,7 +97,7 @@ Module LiftingTests.
Goal E, Goal E,
True wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x") True wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x")
(λ v, v = LitV 40). (λ v, v = ('40)%L).
Proof. Proof.
intros E. intros E.
rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=. rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
......
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