notation.v 7.48 KB
 Robbert Krebbers committed Dec 09, 2016 1 ``````From iris.program_logic Require Import language. `````` Ralf Jung committed Jun 13, 2019 2 ``````From iris.heap_lang Require Export lang. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Feb 11, 2016 4 `````` `````` Ralf Jung committed Jun 13, 2019 5 ``````(** Coercions to make programs easier to type. *) `````` Ralf Jung committed Feb 11, 2016 6 ``````Coercion LitInt : Z >-> base_lit. `````` Ralf Jung committed Feb 11, 2016 7 ``````Coercion LitBool : bool >-> base_lit. `````` Robbert Krebbers committed Apr 19, 2016 8 ``````Coercion LitLoc : loc >-> base_lit. `````` 9 ``````Coercion LitProphecy : proph_id >-> base_lit. `````` Robbert Krebbers committed Apr 19, 2016 10 `````` `````` Ralf Jung committed Feb 11, 2016 11 12 ``````Coercion App : expr >-> Funclass. `````` Ralf Jung committed Jun 13, 2019 13 ``````Coercion Val : val >-> expr. `````` Robbert Krebbers committed Jul 15, 2016 14 15 ``````Coercion Var : string >-> expr. `````` Ralf Jung committed Jun 13, 2019 16 17 18 19 20 21 22 23 24 ``````(** 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). `````` Ralf Jung committed Jun 24, 2019 25 ``````(** Compare-and-set (CAS) returns just a boolean indicating success or failure. *) `````` Ralf Jung committed Jun 24, 2019 26 ``````Notation CAS l e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing). `````` Ralf Jung committed Jun 13, 2019 27 28 29 30 31 `````` (* 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)). `````` Robbert Krebbers committed Apr 19, 2016 32 33 ``````(* No scope for the values, does not conflict and scope is often not inferred properly. *) `````` Rodolphe Lepigre committed Jun 15, 2019 34 ``````Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l"). `````` Robbert Krebbers committed Mar 04, 2016 35 `````` `````` Robbert Krebbers committed Mar 03, 2016 36 37 38 ``````(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come first. *) Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope. `````` Robbert Krebbers committed Mar 05, 2016 39 ``````Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope. `````` Robbert Krebbers committed Sep 09, 2017 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 `````` (* Using the '[hv' ']' printing box, we make sure that when the notation for match does not fit on a single line, line breaks will be inserted for *each* breaking point '/'. Note that after each breaking point /, one can put n spaces (for example '/ '). That way, when the breaking point is turned into a line break, indentation of n spaces will appear after the line break. As such, when the match does not fit on one line, it will print it like: match: e0 with InjL x1 => e1 | InjR x2 => e2 end Moreover, if the branches do not fit on a single line, it will be printed as: match: e0 with InjL x1 => lots of stuff bla bla bla bla bla bla bla bla | InjR x2 => even more stuff bla bla bla bla bla bla bla bla end *) `````` Robbert Krebbers committed Feb 27, 2016 63 ``````Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" := `````` Robbert Krebbers committed Apr 25, 2019 64 `````` (Match e0 x1%binder e1 x2%binder e2) `````` Robbert Krebbers committed Jun 06, 2017 65 `````` (e0, x1, e1, x2, e2 at level 200, `````` Robbert Krebbers committed Sep 09, 2017 66 `````` format "'[hv' 'match:' e0 'with' '/ ' '[' 'InjL' x1 => '/ ' e1 ']' '/' '[' | 'InjR' x2 => '/ ' e2 ']' '/' 'end' ']'") : expr_scope. `````` Ralf Jung committed Mar 05, 2016 67 ``````Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" := `````` Robbert Krebbers committed Apr 25, 2019 68 `````` (Match e0 x2%binder e2 x1%binder e1) `````` Ralf Jung committed Mar 05, 2016 69 `````` (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope. `````` Robbert Krebbers committed Sep 09, 2017 70 `````` `````` Ralf Jung committed Mar 02, 2016 71 ``````Notation "()" := LitUnit : val_scope. `````` Robbert Krebbers committed Mar 03, 2016 72 ``````Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope. `````` Robbert Krebbers committed Apr 07, 2019 73 ``````Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope. `````` Robbert Krebbers committed Dec 05, 2017 74 75 76 ``````Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope. Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope. `````` Robbert Krebbers committed Jun 11, 2019 77 ``````Notation "e1 +ₗ e2" := (BinOp OffsetOp e1%E e2%E) : expr_scope. `````` Robbert Krebbers committed Dec 05, 2017 78 79 80 81 82 83 84 85 86 87 88 89 ``````Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope. Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope. Notation "e1 `quot` e2" := (BinOp QuotOp e1%E e2%E) : expr_scope. Notation "e1 `rem` e2" := (BinOp RemOp e1%E e2%E) : expr_scope. Notation "e1 ≪ e2" := (BinOp ShiftLOp e1%E e2%E) : expr_scope. Notation "e1 ≫ e2" := (BinOp ShiftROp e1%E e2%E) : expr_scope. Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope. Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) : expr_scope. Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope. Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) : expr_scope. `````` Robbert Krebbers committed Mar 03, 2016 90 ``````Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope. `````` Ralf Jung committed Feb 11, 2016 91 ``````(* The unicode ← is already part of the notation "_ ← _; _" for bind. *) `````` Robbert Krebbers committed Mar 03, 2016 92 ``````Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope. `````` Robbert Krebbers committed Sep 09, 2017 93 94 95 `````` (* The breaking point '/ ' makes sure that the body of the rec is indented by two spaces in case the whole rec does not fit on a single line. *) `````` Robbert Krebbers committed Apr 25, 2019 96 ``````Notation "'rec:' f x := e" := (Rec f%binder x%binder e%E) `````` Robbert Krebbers committed Oct 26, 2017 97 `````` (at level 200, f at level 1, x at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 98 `````` format "'[' 'rec:' f x := '/ ' e ']'") : expr_scope. `````` Robbert Krebbers committed Apr 25, 2019 99 ``````Notation "'rec:' f x := e" := (RecV f%binder x%binder e%E) `````` Robbert Krebbers committed Oct 26, 2017 100 `````` (at level 200, f at level 1, x at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 101 `````` format "'[' 'rec:' f x := '/ ' e ']'") : val_scope. `````` Robbert Krebbers committed Mar 03, 2016 102 103 ``````Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E) (at level 200, e1, e2, e3 at level 200) : expr_scope. `````` Ralf Jung committed Feb 11, 2016 104 105 106 107 108 `````` (** Derived notions, in order of declaration. The notations for let and seq are stated explicitly instead of relying on the Notations Let and Seq as defined above. This is needed because App is now a coercion, and these notations are otherwise not pretty printed back accordingly. *) `````` Robbert Krebbers committed Apr 25, 2019 109 ``````Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..)) `````` Robbert Krebbers committed Oct 26, 2017 110 `````` (at level 200, f, x, y, z at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 111 `````` format "'[' 'rec:' f x y .. z := '/ ' e ']'") : expr_scope. `````` Robbert Krebbers committed Apr 25, 2019 112 ``````Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..)) `````` Robbert Krebbers committed Oct 26, 2017 113 `````` (at level 200, f, x, y, z at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 114 `````` format "'[' 'rec:' f x y .. z := '/ ' e ']'") : val_scope. `````` Robbert Krebbers committed Mar 04, 2016 115 `````` `````` Robbert Krebbers committed Sep 09, 2017 116 117 ``````(* The breaking point '/ ' makes sure that the body of the λ: is indented by two spaces in case the whole λ: does not fit on a single line. *) `````` Robbert Krebbers committed Apr 25, 2019 118 ``````Notation "λ: x , e" := (Lam x%binder e%E) `````` Robbert Krebbers committed Oct 26, 2017 119 `````` (at level 200, x at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 120 `````` format "'[' 'λ:' x , '/ ' e ']'") : expr_scope. `````` Robbert Krebbers committed Apr 25, 2019 121 ``````Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..)) `````` Robbert Krebbers committed Oct 26, 2017 122 `````` (at level 200, x, y, z at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 123 124 `````` format "'[' 'λ:' x y .. z , '/ ' e ']'") : expr_scope. `````` Robbert Krebbers committed Apr 25, 2019 125 ``````Notation "λ: x , e" := (LamV x%binder e%E) `````` Robbert Krebbers committed Oct 26, 2017 126 `````` (at level 200, x at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 127 `````` format "'[' 'λ:' x , '/ ' e ']'") : val_scope. `````` Robbert Krebbers committed Apr 25, 2019 128 ``````Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. )) `````` Robbert Krebbers committed Oct 26, 2017 129 `````` (at level 200, x, y, z at level 1, e at level 200, `````` Robbert Krebbers committed Sep 09, 2017 130 131 `````` format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope. `````` Robbert Krebbers committed Apr 25, 2019 132 ``````Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E) `````` Robbert Krebbers committed Oct 26, 2017 133 `````` (at level 200, x at level 1, e1, e2 at level 200, `````` Robbert Krebbers committed Sep 09, 2017 134 `````` format "'[' 'let:' x := '[' e1 ']' 'in' '/' e2 ']'") : expr_scope. `````` Robbert Krebbers committed Mar 03, 2016 135 ``````Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E) `````` Robbert Krebbers committed Jun 06, 2017 136 `````` (at level 100, e2 at level 200, `````` Robbert Krebbers committed Nov 12, 2019 137 `````` format "'[' '[hv' '[' e1 ']' ;; ']' '/' e2 ']'") : expr_scope. `````` Robbert Krebbers committed Jun 06, 2017 138 `````` `````` Robbert Krebbers committed Jul 12, 2016 139 ``````(* Shortcircuit Boolean connectives *) `````` Robbert Krebbers committed Nov 09, 2016 140 ``````Notation "e1 && e2" := `````` Jacques-Henri Jourdan committed Oct 29, 2018 141 `````` (If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope. `````` Robbert Krebbers committed Nov 09, 2016 142 ``````Notation "e1 || e2" := `````` Jacques-Henri Jourdan committed Oct 29, 2018 143 `````` (If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope. `````` Robbert Krebbers committed Jul 12, 2016 144 `````` `````` Robbert Krebbers committed Jun 23, 2016 145 ``````(** Notations for option *) `````` Jacques-Henri Jourdan committed Oct 29, 2018 146 ``````Notation NONE := (InjL (LitV LitUnit)) (only parsing). `````` Ralf Jung committed Jun 30, 2018 147 ``````Notation NONEV := (InjLV (LitV LitUnit)) (only parsing). `````` Jacques-Henri Jourdan committed Oct 29, 2018 148 ``````Notation SOME x := (InjR x) (only parsing). `````` Ralf Jung committed Jun 30, 2018 149 150 ``````Notation SOMEV x := (InjRV x) (only parsing). `````` Robbert Krebbers committed Jun 23, 2016 151 ``````Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" := `````` Robbert Krebbers committed Apr 25, 2019 152 `````` (Match e0 BAnon e1 x%binder e2) `````` Robbert Krebbers committed Dec 09, 2016 153 `````` (e0, e1, x, e2 at level 200, only parsing) : expr_scope. `````` Robbert Krebbers committed Jul 18, 2016 154 ``````Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" := `````` Robbert Krebbers committed Apr 25, 2019 155 `````` (Match e0 BAnon e1 x%binder e2) `````` Robbert Krebbers committed Jun 23, 2016 156 `````` (e0, e1, x, e2 at level 200, only parsing) : expr_scope. `````` Marianna Rapoport committed Oct 05, 2018 157 `````` `````` Ralf Jung committed Jun 13, 2019 158 ``````Notation ResolveProph e1 e2 := (Resolve Skip e1 e2) (only parsing). `````` Ralf Jung committed Oct 05, 2018 159 ``Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.``