From 7347e89e926ed9ff291d90b65368a3935468afab Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 5 Feb 2016 11:24:07 +0100
Subject: [PATCH] experiment a little with notation for our language
---
heap_lang/sugar.v | 35 +++++++++++++++++++++++++++++++++
heap_lang/tests.v | 50 +++++++++++++++++++++++++----------------------
2 files changed, 62 insertions(+), 23 deletions(-)
diff --git a/heap_lang/sugar.v b/heap_lang/sugar.v
index 36b1ab9dd..867529d14 100644
--- a/heap_lang/sugar.v
+++ b/heap_lang/sugar.v
@@ -17,6 +17,41 @@ 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?
+ Also find better notation for function application. Or maybe
+ we can make "App" a coercion from expr to (expr → expr)? *)
+(* The colons indicate binders. *)
+Notation "'rec::' e" := (Rec e) (at level 100) : lang_scope.
+Notation "'λ:' e" := (Lam e) (at level 100) : lang_scope.
+Infix "$" := App : 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 10) : lang_scope.
+Notation "'#1'" := (Var 1) (at level 10) : lang_scope.
+Notation "'#2'" := (Var 2) (at level 10) : lang_scope.
+Notation "'#3'" := (Var 3) (at level 10) : lang_scope.
+Notation "'#4'" := (Var 4) (at level 10) : lang_scope.
+Notation "'#5'" := (Var 5) (at level 10) : lang_scope.
+Notation "'#6'" := (Var 6) (at level 10) : lang_scope.
+Notation "'#7'" := (Var 7) (at level 10) : lang_scope.
+Notation "'#8'" := (Var 8) (at level 10) : lang_scope.
+Notation "'#9'" := (Var 9) (at level 10) : 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 Loc : loc >-> expr.
+
Section suger.
Context {Σ : iFunctor}.
Implicit Types P : iProp heap_lang Σ.
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 4c1227feb..f5ee7d8e1 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -5,14 +5,15 @@ 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,10 +23,10 @@ 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.
+ Definition e3 : expr := ★ #0.
+ (* FIXME: Fix levels so that we do not need the parenthesis here. *)
+ Definition e2 : expr := (#0 <- ★ #0 + 1) ; e3.
+ Definition e : expr := let: new 1 in e2.
Goal ∀ σ E, (ownP σ : iProp heap_lang Σ) ⊑ (wp E e (λ v, ■(v = LitNatV 2))).
Proof.
move=> σ E. rewrite /e.
@@ -34,11 +35,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,15 +55,15 @@ 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))
- ).
+ 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)) ⊑
@@ -73,7 +76,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' (LitNat n1) (Var 0) (LitNat n2) (FindPred (LitNat n2)))).
rewrite -wp_plus. asimpl.
rewrite -(wp_bindi (CaseCtx _ _)).
rewrite -!later_intro /=.
@@ -94,7 +97,7 @@ Module LiftingTests.
Qed.
Lemma Pred_spec n E Q :
- ▷Q (LitNatV $ pred n) ⊑ wp E (App Pred (LitNat n)) Q.
+ ▷Q (LitNatV (pred n)) ⊑ wp E (App Pred (LitNat n)) Q.
Proof.
rewrite -wp_lam //. asimpl.
rewrite -(wp_bindi (CaseCtx _ _)).
@@ -109,7 +112,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 = LitNatV 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? *)
--
GitLab