Commit 9a137a0e authored by Ralf Jung's avatar Ralf Jung

some more work on notation

parent 7347e89e
......@@ -21,27 +21,25 @@ 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. *)
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.
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 "#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.
......@@ -49,8 +47,12 @@ 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}.
......
......@@ -9,8 +9,8 @@ Module LangTests.
Goal σ, prim_step add σ 42 σ None.
Proof. intros; do_step done. Qed.
(* 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.
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. Set Printing All. intros; do_step done. Qed.
Definition lam : expr := (λ: #0 + 21)%L.
......@@ -23,11 +23,9 @@ Module LiftingTests.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ.
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))).
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.
......@@ -55,19 +53,22 @@ Module LiftingTests.
by apply const_intro.
Qed.
Definition FindPred' n1 Sn1 n2 f : expr := if (Sn1 < n2)
then f $ Sn1
(* 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 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
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.
......@@ -76,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 /=.
......@@ -97,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 _ _)).
......@@ -113,7 +114,7 @@ Module LiftingTests.
Goal E,
True wp (Σ:=Σ) E
(* FIXME why do we need %L here? *)
(let: Pred $ 42 in Pred $ #0)%L (λ v, (v = LitNatV 40)).
(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? *)
......
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