Commit 05bccfb8 authored by Ralf Jung's avatar Ralf Jung

centralize all heap_lang notation in one file

parent a555a33c
Pipeline #17490 passed with stage
in 19 minutes and 49 seconds
...@@ -735,19 +735,3 @@ Proof. ...@@ -735,19 +735,3 @@ Proof.
apply (H κs (fill_item K (foldl (flip fill_item) e2' Ks)) σ' efs). 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. econstructor 1 with (K := Ks ++ [K]); last done; simpl; by rewrite fill_app.
Qed. 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).
...@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Export proph_map. ...@@ -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 Export weakestpre.
From iris.program_logic Require Import ectx_lifting total_ectx_lifting. From iris.program_logic Require Import ectx_lifting total_ectx_lifting.
From iris.heap_lang Require Export lang. 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 iris.proofmode Require Import tactics.
From stdpp Require Import fin_maps. From stdpp Require Import fin_maps.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
From iris.program_logic Require Import language. 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". Set Default Proof Using "Type".
Delimit Scope expr_scope with E. Delimit Scope expr_scope with E.
Delimit Scope val_scope with V. Delimit Scope val_scope with V.
(** Coercions to make programs easier to type. *)
Coercion LitInt : Z >-> base_lit. Coercion LitInt : Z >-> base_lit.
Coercion LitBool : bool >-> base_lit. Coercion LitBool : bool >-> base_lit.
Coercion LitLoc : loc >-> base_lit. Coercion LitLoc : loc >-> base_lit.
Coercion LitProphecy : proph_id >-> base_lit. Coercion LitProphecy : proph_id >-> base_lit.
Coercion App : expr >-> Funclass. Coercion App : expr >-> Funclass.
Coercion Val : val >-> expr.
Coercion Val : val >-> expr.
Coercion Var : string >-> 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 (* No scope for the values, does not conflict and scope is often not inferred
properly. *) properly. *)
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l"). 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'" := ...@@ -141,4 +156,5 @@ Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
(Match e0 BAnon e1 x%binder e2) (Match e0 BAnon e1 x%binder e2)
(e0, e1, x, e2 at level 200, only parsing) : expr_scope. (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. Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.
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