Commit 3b3a0a1a authored by Robbert Krebbers's avatar Robbert Krebbers

Improve notations for heap_lang.

parent 095fde7e
Require Export heap_lang.heap_lang heap_lang.lifting. Require Export heap_lang.heap_lang heap_lang.lifting.
Import uPred. Import uPred heap_lang.
Import heap_lang.
(** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *) (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
Definition Lam (e : {bind expr}) := Rec e.[ren(+1)]. Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
...@@ -17,42 +16,38 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)]. ...@@ -17,42 +16,38 @@ Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2). Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]). Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
Delimit Scope lang_scope with L. Module notations.
Bind Scope lang_scope with expr. Delimit Scope lang_scope with L.
Arguments wp {_ _} _ _%L _. Bind Scope lang_scope with expr.
(* TODO: The levels are all random. Also maybe we should not Arguments wp {_ _} _ _%L _.
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. Coercion LitNat : nat >-> expr.
Notation "e1 '<-' e2" := (Store e1 e2) (at level 60) : lang_scope. Coercion LitNatV : nat >-> val.
Notation "'new' e" := (Alloc e) (at level 60) : lang_scope. Coercion Loc : loc >-> expr.
Notation "e1 '+' e2" := (Plus e1 e2) : lang_scope. Coercion LocV : loc >-> val.
Notation "e1 '≤' e2" := (Le e1 e2) : lang_scope. Coercion App : expr >-> Funclass.
Notation "e1 '<' e2" := (Lt e1 e2) : lang_scope.
Coercion LitNat : nat >-> expr. (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
Coercion LitNatV : nat >-> val. first. *)
Coercion Loc : loc >-> expr. (* What about Arguments for hoare triples?. *)
Coercion LocV : loc >-> val. (* The colons indicate binders. "let" is not consistent here though,
Coercion App : expr >-> Funclass. thing are only bound in the "in". *)
Notation "# n" := (Var n) (at level 1, format "# n") : 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" := (Plus e1%L e2%L)
(at level 50, left associativity) : lang_scope.
Notation "e1 ≤ e2" := (Le e1%L e2%L) (at level 70) : lang_scope.
Notation "e1 < e2" := (Lt 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 "e1 ; e2" := (Seq e1%L e2%L) (at level 100) : lang_scope.
Notation "'let:' e1 'in' e2" := (Let e1%L e2%L) (at level 102) : lang_scope.
Notation "'λ:' e" := (Lam e%L) (at level 102) : lang_scope.
Notation "'rec::' e" := (Rec e%L) (at level 102) : 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, only parsing) : lang_scope.
End notations.
Section suger. Section suger.
Context {Σ : iFunctor}. Context {Σ : iFunctor}.
......
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
Require Import program_logic.upred. Require Import program_logic.upred.
Require Import heap_lang.lifting heap_lang.sugar. Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang. Import heap_lang uPred notations.
Import uPred.
Module LangTests. Module LangTests.
Definition add := (21 + 21)%L. Definition add := (21 + 21)%L.
...@@ -24,7 +23,7 @@ Module LiftingTests. ...@@ -24,7 +23,7 @@ Module LiftingTests.
Implicit Types Q : val iProp heap_lang Σ. Implicit Types Q : val iProp heap_lang Σ.
(* FIXME: Fix levels so that we do not need the parenthesis here. *) (* FIXME: Fix levels so that we do not need the parenthesis here. *)
Definition e : expr := let: new 1 in (#0 <- #0 + 1 ; #0)%L. Definition e : expr := (let: ref 1 in #0 <- !#0 + 1; !#0)%L.
Goal σ E, (ownP σ : iProp heap_lang Σ) (wp E e (λ v, (v = 2))). Goal σ E, (ownP σ : iProp heap_lang Σ) (wp E e (λ v, (v = 2))).
Proof. Proof.
move=> σ E. rewrite /e. move=> σ E. rewrite /e.
...@@ -56,15 +55,12 @@ Module LiftingTests. ...@@ -56,15 +55,12 @@ Module LiftingTests.
(* TODO: once asimpl preserves notation, we don't need (* TODO: once asimpl preserves notation, we don't need
FindPred' anymore. *) FindPred' anymore. *)
(* FIXME: fix notation so that we do not need parenthesis or %L *) (* FIXME: fix notation so that we do not need parenthesis or %L *)
Definition FindPred' n1 Sn1 n2 f : expr := if Sn1 < n2 Definition FindPred' n1 Sn1 n2 f : expr :=
then f Sn1 if Sn1 < n2 then f Sn1 else n1.
else n1. Definition FindPred n2 : expr :=
Definition FindPred n2 : expr := rec:: (let: (#1 + 1) in rec:: (let: #1 + 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L.
FindPred' #2 #0 n2.[ren(+3)] #1)%L. Definition Pred : expr :=
Definition Pred : expr := λ: (if #0 0 λ: (if #0 0 then 0 else FindPred #0 0)%L.
then 0
else FindPred (#0) 0
)%L.
Lemma FindPred_spec n1 n2 E Q : Lemma FindPred_spec n1 n2 E Q :
((n1 < n2) Q (pred n2)) ((n1 < n2) Q (pred n2))
...@@ -112,9 +108,7 @@ Module LiftingTests. ...@@ -112,9 +108,7 @@ Module LiftingTests.
Qed. Qed.
Goal E, Goal E,
True wp (Σ:=Σ) E True wp (Σ:=Σ) E (let: Pred 42 in Pred #0) (λ v, (v = 40)).
(* FIXME why do we need %L here? *)
(let: Pred 42 in Pred #0)%L (λ v, (v = 40)).
Proof. Proof.
intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro. intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *) 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