Commit 3a86d2ff authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 30394154 46fafcf5
......@@ -19,8 +19,6 @@ Inductive expr :=
| Var (x : string)
| Rec (f x : string) (e : expr)
| App (e1 e2 : expr)
(* Let *)
| Let (x : string) (e1 e2 : expr)
(* Base types and their operations *)
| Lit (l : base_lit)
| UnOp (op : un_op) (e : expr)
......@@ -78,7 +76,6 @@ Definition state := gmap loc val.
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| LetCtx (x : string) (e2 : expr)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (e2 : expr)
| BinOpRCtx (op : bin_op) (v1 : val)
......@@ -104,7 +101,6 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 => App e e2
| AppRCtx v1 => App (of_val v1) e
| LetCtx x e2 => Let x e e2
| UnOpCtx op => UnOp op e
| BinOpLCtx op e2 => BinOp op e e2
| BinOpRCtx op v1 => BinOp op (of_val v1) e
......@@ -133,8 +129,6 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
| Var y => if decide (x = y x "") then of_val v else Var y
| Rec f y e => Rec f y (if decide (x f x y) then subst e x v else e)
| App e1 e2 => App (subst e1 x v) (subst e2 x v)
| Let y e1 e2 =>
Let y (subst e1 x v) (if decide (x y) then subst e2 x v else e2)
| Lit l => Lit l
| UnOp op e => UnOp op (subst e x v)
| BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
......@@ -178,9 +172,6 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
to_val e2 = Some v2
head_step (App (Rec f x e1) e2) σ
(subst (subst e1 f (RecV f x e1)) x v2) σ None
| DeltaS x e1 e2 v1 σ :
to_val e1 = Some v1
head_step (Let x e1 e2) σ (subst e2 x v1) σ None
| UnOpS op l l' σ :
un_op_eval op l = Some l'
head_step (UnOp op (Lit l)) σ (Lit l') σ None
......
......@@ -90,14 +90,6 @@ Proof.
last by intros; inv_step; eauto.
Qed.
Lemma wp_let E x e1 e2 v Q :
to_val e1 = Some v
wp E (subst e2 x v) Q wp E (Let x e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Let _ _ _)
(subst e2 x v) None) ?right_id //=; intros; inv_step; eauto.
Qed.
Lemma wp_un_op E op l l' Q :
un_op_eval op l = Some l'
Q (LitV l') wp E (UnOp op (Lit l)) Q.
......
......@@ -3,8 +3,10 @@ Import uPred heap_lang.
(** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
Notation Lam x e := (Rec "" x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let "" e1 e2).
Notation LamV x e := (RecV "" x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx "" e2).
Module notations.
......@@ -14,7 +16,7 @@ Module notations.
Coercion LitNat : nat >-> base_lit.
Coercion LitBool : bool >-> base_lit.
(* No coercion from base_lit to expr. This makes is slightly easier to tell
(** No coercion from base_lit to expr. This makes is slightly easier to tell
apart language and Coq expressions. *)
Coercion Var : string >-> expr.
Coercion App : expr >-> Funclass.
......@@ -22,6 +24,7 @@ Module notations.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* What about Arguments for hoare triples?. *)
Notation "' l" := (Lit l) (at level 8, format "' l") : 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 "e1 + e2" := (BinOp PlusOp e1%L e2%L)
......@@ -33,18 +36,21 @@ Module notations.
Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
Notation "'let:' x := e1 'in' e2" := (Let x e1%L e2%L)
(at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
Notation "e1 ; e2" := (Seq e1%L e2%L)
(at level 100, e2 at level 200) : lang_scope.
Notation "'rec:' f x := e" := (Rec f x e%L)
(at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
(at level 200, e1, e2, e3 at level 200) : lang_scope.
(* derived notions, in order of declaration *)
(** Derived notions, in order of declaration. The notations for let and seq
are stated explicitly instead of relying on the Notations Let and Seq as
defined above. This is needed because App is now a coercion, and these
notations are otherwise not pretty printed back accordingly. *)
Notation "λ: x , e" := (Lam x e%L)
(at level 102, x at level 1, e at level 200) : lang_scope.
Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
(at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
Notation "e1 ; e2" := (Lam "" e2%L e1%L)
(at level 100, e2 at level 200) : lang_scope.
End notations.
Section suger.
......@@ -57,6 +63,10 @@ Lemma wp_lam E x ef e v Q :
to_val e = Some v wp E (subst ef x v) Q wp E (App (Lam x ef) e) Q.
Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed.
Lemma wp_let E x e1 e2 v Q :
to_val e1 = Some v wp E (subst e2 x v) Q wp E (Let x e1 e2) Q.
Proof. apply wp_lam. Qed.
Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, wp E e2 Q) wp E (Seq e1 e2) Q.
Proof.
rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
......
......@@ -4,20 +4,20 @@ Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang uPred notations.
Module LangTests.
Definition add := (Lit 21 + Lit 21)%L.
Goal σ, prim_step add σ (Lit 42) σ None.
Definition add := ('21 + '21)%L.
Goal σ, prim_step add σ ('42) σ None.
Proof. intros; do_step done. Qed.
Definition rec_app : expr := (rec: "f" "x" := "f" "x") (Lit 0).
Definition rec_app : expr := ((rec: "f" "x" := "f" "x") '0)%L.
Goal σ, prim_step rec_app σ rec_app σ None.
Proof.
intros. rewrite /rec_app. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ (LitV (LitNat 0))).
Qed.
Definition lam : expr := λ: "x", "x" + Lit 21.
Goal σ, prim_step (lam (Lit 21)) σ add σ None.
Definition lam : expr := λ: "x", "x" + '21.
Goal σ, prim_step (lam '21)%L σ add σ None.
Proof.
intros. rewrite /lam. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + Lit 21) _ (LitV 21)).
by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + '21) _ (LitV 21)).
Qed.
End LangTests.
......@@ -27,7 +27,7 @@ Module LiftingTests.
Implicit Types Q : val iProp heap_lang Σ.
Definition e : expr :=
let: "x" := ref (Lit 1) in "x" <- !"x" + Lit 1; !"x".
let: "x" := ref '1 in "x" <- !"x" + '1; !"x".
Goal σ E, ownP (Σ:=Σ) σ wp E e (λ v, v = LitV 2).
Proof.
move=> σ E. rewrite /e.
......@@ -56,13 +56,13 @@ Module LiftingTests.
Definition FindPred (n2 : expr) : expr :=
rec: "pred" "y" :=
let: "yp" := "y" + Lit 1 in
let: "yp" := "y" + '1 in
if "yp" < n2 then "pred" "yp" else "y".
Definition Pred : expr :=
λ: "x", if "x" Lit 0 then Lit 0 else FindPred "x" (Lit 0).
λ: "x", if "x" '0 then '0 else FindPred "x" '0.
Lemma FindPred_spec n1 n2 E Q :
( (n1 < n2) Q (LitV (pred n2))) wp E (FindPred (Lit n2) (Lit n1)) Q.
( (n1 < n2) Q (LitV (pred n2))) wp E (FindPred 'n2 'n1)%L Q.
Proof.
revert n1. apply löb_all_1=>n1.
rewrite (commutative uPred_and ( _)%I) associative; apply const_elim_r=>?.
......@@ -82,7 +82,7 @@ Module LiftingTests.
by rewrite -!later_intro -wp_value' // and_elim_r.
Qed.
Lemma Pred_spec n E Q : Q (LitV (pred n)) wp E (Pred (Lit n)) Q.
Lemma Pred_spec n E Q : Q (LitV (pred n)) wp E (Pred 'n)%L Q.
Proof.
rewrite -wp_lam //=.
rewrite -(wp_bindi (IfCtx _ _)).
......@@ -96,7 +96,7 @@ Module LiftingTests.
Qed.
Goal E,
True wp (Σ:=Σ) E (let: "x" := Pred (Lit 42) in Pred "x")
True wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x")
(λ v, v = LitV 40).
Proof.
intros E.
......
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