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

_CoqProject

@@ -41,13 +41,13 @@ algebra/cmra_tactics.v
 algebra/sts.v
 algebra/auth.v
 algebra/fin_maps.v
-logic/upred.v
 algebra/cofe.v
 algebra/base.v
 algebra/dra.v
 algebra/cofe_solver.v
 algebra/agree.v
 algebra/excl.v
+program_logic/upred.v
 program_logic/model.v
 program_logic/adequacy.v
 program_logic/hoare_lifting.v

heap_lang/sugar.v

@@ -17,6 +17,43 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
 Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
 
+Delimit Scope lang_scope with L.
+Bind Scope lang_scope with expr.
+Arguments wp {_ _} _ _%L _.
+(* TODO: The levels are all random. Also maybe we should not
+   make 'new' a keyword. What about Arguments for hoare triples?. *)
+(* The colons indicate binders. "let" is not consistent here though,
+   thing are only bound in the "in". *)
+Notation "'rec::' e" := (Rec e) (at level 100) : lang_scope.
+Notation "'λ:' e" := (Lam e) (at level 100) : lang_scope.
+Notation "'let:' e1 'in' e2" := (Let e1 e2) (at level 70) : lang_scope.
+Notation "e1 ';' e2" := (Seq e1 e2) (at level 70) : lang_scope.
+Notation "'if' e1 'then' e2 'else' e3" := (If e1 e2 e3) : lang_scope.
+
+Notation "#0" := (Var 0) (at level 0) : lang_scope.
+Notation "#1" := (Var 1) (at level 0) : lang_scope.
+Notation "#2" := (Var 2) (at level 0) : lang_scope.
+Notation "#3" := (Var 3) (at level 0) : lang_scope.
+Notation "#4" := (Var 4) (at level 0) : lang_scope.
+Notation "#5" := (Var 5) (at level 0) : lang_scope.
+Notation "#6" := (Var 6) (at level 0) : lang_scope.
+Notation "#7" := (Var 7) (at level 0) : lang_scope.
+Notation "#8" := (Var 8) (at level 0) : lang_scope.
+Notation "#9" := (Var 9) (at level 0) : lang_scope.
+
+Notation "'★' e" := (Load e) (at level 30) : lang_scope.
+Notation "e1 '<-' e2" := (Store e1 e2) (at level 60) : lang_scope.
+Notation "'new' e" := (Alloc e) (at level 60) : lang_scope.
+Notation "e1 '+' e2" := (Plus e1 e2) : lang_scope.
+Notation "e1 '≤' e2" := (Le e1 e2) : lang_scope.
+Notation "e1 '<' e2" := (Lt e1 e2) : lang_scope.
+
+Coercion LitNat : nat >-> expr.
+Coercion LitNatV : nat >-> val.
+Coercion Loc : loc >-> expr.
+Coercion LocV : loc >-> val.
+Coercion App : expr >-> Funclass.
+
 Section suger.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.

heap_lang/tests.v

 (** This file is essentially a bunch of testcases. *)
-Require Import logic.upred.
+Require Import program_logic.upred.
 Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang.
 Import uPred.
 
 Module LangTests.
-  Definition add := Plus (LitNat 21) (LitNat 21).
-  Goal ∀ σ, prim_step add σ (LitNat 42) σ None.
+  Definition add := (21 + 21)%L.
+  Goal ∀ σ, prim_step add σ 42 σ None.
   Proof. intros; do_step done. Qed.
-  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
-  Definition rec_app := App rec (LitNat 0).
+  (* FIXME RJ why do I need the %L ? *)
+  Definition rec : expr := (rec:: #0 #1)%L. (* fix f x => f x *)
+  Definition rec_app : expr := rec 0.
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
-  Proof. intros; do_step done. Qed.
-  Definition lam := Lam (Plus (Var 0) (LitNat 21)).
+  Proof. Set Printing All. intros; do_step done. Qed.
+  Definition lam : expr := (λ: #0 + 21)%L.
   Goal ∀ σ, prim_step (App lam (LitNat 21)) σ add σ None.
   Proof. intros; do_step done. Qed.
 End LangTests.
@@ -22,11 +23,9 @@ Module LiftingTests.
   Implicit Types P : iProp heap_lang Σ.
   Implicit Types Q : val → iProp heap_lang Σ.
 
-  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
-  Definition e3 := Load (Var 0).
-  Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
-  Definition e := Let (Alloc (LitNat 1)) e2.
-  Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
+  (* FIXME: Fix levels so that we do not need the parenthesis here. *)
+  Definition e  : expr := let: new 1 in (#0 <- ★#0 + 1 ; ★#0)%L.
+  Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = 2))).
   Proof.
     move=> σ E. rewrite /e.
     rewrite -wp_let. rewrite -wp_alloc_pst; last done.
@@ -34,11 +33,13 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
+    (* TODO RJ: If you go here, you can see how the sugar does not print
+       all so nicely. *)
     rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
     rewrite -(wp_bindi (StoreRCtx (LocV _))).
     rewrite -(wp_bindi (PlusLCtx _)).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
+    { by rewrite lookup_insert. } (* RJ FIXME: figure out why apply and eapply fail. *)
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_plus -later_intro.
     rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
@@ -52,19 +53,22 @@ Module LiftingTests.
     by apply const_intro.
   Qed.
 
-  Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
-                                      (App f Sn1)
-                                      n1.
-  Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1))
-                                     (FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))).
-  Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
-                             (LitNat 0)
-                             (App (FindPred (Var 0)) (LitNat 0))
-                         ).
+  (* TODO: once asimpl preserves notation, we don't need
+     FindPred' anymore. *)
+  (* FIXME: fix notation so that we do not need parenthesis or %L *)
+  Definition FindPred' n1 Sn1 n2 f : expr := if Sn1 < n2
+                                             then f Sn1
+                                             else n1.
+  Definition FindPred n2 : expr := rec:: (let: (#1 + 1) in
+                                     FindPred' #2 #0 n2.[ren(+3)] #1)%L.
+  Definition Pred : expr := λ: (if #0 ≤ 0
+                                then 0
+                                else FindPred (#0) 0
+                               )%L.
 
   Lemma FindPred_spec n1 n2 E Q :
-    (■(n1 < n2) ∧ Q (LitNatV $ pred n2)) ⊑
-       wp E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
+    (■(n1 < n2) ∧ Q (pred n2)) ⊑
+       wp E (FindPred n2 n1) Q.
   Proof.
     revert n1. apply löb_all_1=>n1.
     rewrite -wp_rec //. asimpl.
@@ -73,7 +77,7 @@ Module LiftingTests.
     { apply and_mono; first done. by rewrite -later_intro. }
     apply later_mono.
     (* Go on. *)
-    rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
+    rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2))).
     rewrite -wp_plus. asimpl.
     rewrite -(wp_bindi (CaseCtx _ _)).
     rewrite -!later_intro /=.
@@ -94,7 +98,7 @@ Module LiftingTests.
   Qed.
 
   Lemma Pred_spec n E Q :
-    ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
+    ▷Q (pred n) ⊑ wp E (Pred n) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
     rewrite -(wp_bindi (CaseCtx _ _)).
@@ -109,7 +113,8 @@ Module LiftingTests.
 
   Goal ∀ E,
     True ⊑ wp (Σ:=Σ) E
-      (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, ■(v = LitNatV 40)).
+         (* FIXME why do we need %L here? *)
+      (let: Pred 42 in Pred #0)%L (λ v, ■(v = 40)).
   Proof.
     intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
     asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)

program_logic/model.v

-Require Export logic.upred program_logic.resources.
+Require Export program_logic.upred program_logic.resources.
 Require Import algebra.cofe_solver.
 
 Module iProp.