diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v index f0b7642901132ed9744a5362d500e63aaaedfff8..0791353e7adb17ce1b9c602579143f26b158255b 100644 --- a/theories/heap_lang/lang.v +++ b/theories/heap_lang/lang.v @@ -735,19 +735,3 @@ Proof. apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs). econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app. Qed. - -(** Define some derived forms. *) -Notation Lam x e := (Rec BAnon x e) (only parsing). -Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing). -Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing). -Notation LamV x e := (RecV BAnon x e) (only parsing). -Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing). -Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing). -Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing). -Notation Alloc e := (AllocN (Val \$ LitV \$ LitInt 1) e) (only parsing). - -(* Skip should be atomic, we sometimes open invariants around - it. Hence, we need to explicitly use LamV instead of e.g., Seq. *) -Notation Skip := (App (Val \$ LamV BAnon (Val \$ LitV LitUnit)) (Val \$ LitV LitUnit)). - -Notation ResolveProph e1 e2 := (Resolve Skip e1 e2) (only parsing). diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v index 347e58868d602d75318b5df02f46a449d0137bc2..00802e47193a21f5572bcf3dabbebe01b333f0f6 100644 --- a/theories/heap_lang/lifting.v +++ b/theories/heap_lang/lifting.v @@ -4,7 +4,7 @@ From iris.base_logic.lib Require Export proph_map. From iris.program_logic Require Export weakestpre. From iris.program_logic Require Import ectx_lifting total_ectx_lifting. From iris.heap_lang Require Export lang. -From iris.heap_lang Require Import tactics. +From iris.heap_lang Require Import tactics notation. From iris.proofmode Require Import tactics. From stdpp Require Import fin_maps. Set Default Proof Using "Type". diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v index 420fb7154b8fcd495c82da743315c9ba56dedd49..ae3d54943398868d220d02a885f142349408b181 100644 --- a/theories/heap_lang/notation.v +++ b/theories/heap_lang/notation.v @@ -1,20 +1,35 @@ From iris.program_logic Require Import language. -From iris.heap_lang Require Export lang tactics. +From iris.heap_lang Require Export lang. Set Default Proof Using "Type". Delimit Scope expr_scope with E. Delimit Scope val_scope with V. +(** Coercions to make programs easier to type. *) Coercion LitInt : Z >-> base_lit. Coercion LitBool : bool >-> base_lit. Coercion LitLoc : loc >-> base_lit. Coercion LitProphecy : proph_id >-> base_lit. Coercion App : expr >-> Funclass. -Coercion Val : val >-> expr. +Coercion Val : val >-> expr. Coercion Var : string >-> expr. +(** Define some derived forms. *) +Notation Lam x e := (Rec BAnon x e) (only parsing). +Notation Let x e1 e2 := (App (Lam x e2) e1) (only parsing). +Notation Seq e1 e2 := (Let BAnon e1 e2) (only parsing). +Notation LamV x e := (RecV BAnon x e) (only parsing). +Notation LetCtx x e2 := (AppRCtx (LamV x e2)) (only parsing). +Notation SeqCtx e2 := (LetCtx BAnon e2) (only parsing). +Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)) (only parsing). +Notation Alloc e := (AllocN (Val \$ LitV \$ LitInt 1) e) (only parsing). + +(* Skip should be atomic, we sometimes open invariants around + it. Hence, we need to explicitly use LamV instead of e.g., Seq. *) +Notation Skip := (App (Val \$ LamV BAnon (Val \$ LitV LitUnit)) (Val \$ LitV LitUnit)). + (* No scope for the values, does not conflict and scope is often not inferred properly. *) Notation "# l" := (LitV l%Z%V) (at level 8, format "# l"). @@ -141,4 +156,5 @@ Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := (Match e0 BAnon e1 x%binder e2) (e0, e1, x, e2 at level 200, only parsing) : expr_scope. +Notation ResolveProph e1 e2 := (Resolve Skip e1 e2) (only parsing). Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.