notation.v 7.48 KB
Newer Older
1
From iris.program_logic Require Import language.
2
From iris.heap_lang Require Export lang.
3
Set Default Proof Using "Type".
4

5
(** Coercions to make programs easier to type. *)
6
Coercion LitInt : Z >-> base_lit.
7
Coercion LitBool : bool >-> base_lit.
8
Coercion LitLoc : loc >-> base_lit.
9
Coercion LitProphecy : proph_id >-> base_lit.
10

11
12
Coercion App : expr >-> Funclass.

13
Coercion Val : val >-> expr.
14
15
Coercion Var : string >-> expr.

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's avatar
Ralf Jung committed
25
(** Compare-and-set (CAS) returns just a boolean indicating success or failure. *)
Ralf Jung's avatar
Ralf Jung committed
26
Notation CAS l e1 e2 := (Snd (CmpXchg l e1 e2)) (only parsing).
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)).

32
33
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
34
Notation "# l" := (LitV l%Z%V%stdpp) (at level 8, format "# l").
35

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's avatar
Robbert Krebbers committed
39
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
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
*)
63
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
64
  (Match e0 x1%binder e1 x2%binder e2)
65
  (e0, x1, e1, x2, e2 at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
66
   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
67
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
68
  (Match e0 x2%binder e2 x1%binder e1)
Ralf Jung's avatar
Ralf Jung committed
69
  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
70

71
Notation "()" := LitUnit : val_scope.
72
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
73
Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope.
74
75
76
Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope.

Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
77
Notation "e1 +ₗ e2" := (BinOp OffsetOp e1%E e2%E) : expr_scope.
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.

90
Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
91
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
92
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)
96
Notation "'rec:' f x := e" := (Rec f%binder x%binder e%E)
97
  (at level 200, f at level 1, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
98
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
99
Notation "'rec:' f x := e" := (RecV f%binder x%binder e%E)
100
  (at level 200, f at level 1, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
101
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
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.
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. *)
109
Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
110
  (at level 200, f, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
111
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
112
Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
113
  (at level 200, f, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
114
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.
115

Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)
118
Notation "λ: x , e" := (Lam x%binder e%E)
119
  (at level 200, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
120
   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
121
Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
122
  (at level 200, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.

125
Notation "λ: x , e" := (LamV x%binder e%E)
126
  (at level 200, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
127
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
128
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
129
  (at level 200, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.

132
Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
133
  (at level 200, x at level 1, e1, e2 at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
134
   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
135
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
136
  (at level 100, e2 at level 200,
137
   format "'[' '[hv' '[' e1 ']' ;;  ']' '/' e2 ']'") : expr_scope.
138

139
(* Shortcircuit Boolean connectives *)
140
Notation "e1 && e2" :=
141
  (If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
142
Notation "e1 || e2" :=
143
  (If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.
144

145
(** Notations for option *)
146
Notation NONE := (InjL (LitV LitUnit)) (only parsing).
147
Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
148
Notation SOME x := (InjR x) (only parsing).
149
150
Notation SOMEV x := (InjRV x) (only parsing).

151
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
152
  (Match e0 BAnon e1 x%binder e2)
153
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
154
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
155
  (Match e0 BAnon e1 x%binder e2)
156
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
157

158
Notation ResolveProph e1 e2 := (Resolve Skip e1 e2) (only parsing).
Ralf Jung's avatar
Ralf Jung committed
159
Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.