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

5
Coercion LitInt : Z >-> base_lit.
6
Coercion LitBool : bool >-> base_lit.
7
8
Coercion LitLoc : loc >-> base_lit.

9
10
11
Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.

12
13
Coercion Var : string >-> expr.

14
Coercion BNamed : string >-> binder.
15
Notation "<>" := BAnon : binder_scope.
16

17
18
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
19
20
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
21

22
23
24
(** 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
25
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48

(*
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
*)
49
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
Ralf Jung's avatar
Ralf Jung committed
50
  (Match e0 x1%bind e1 x2%bind e2)
51
  (e0, x1, e1, x2, e2 at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
52
   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
53
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
Ralf Jung's avatar
Ralf Jung committed
54
  (Match e0 x2%bind e2 x1%bind e1)
Ralf Jung's avatar
Ralf Jung committed
55
  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
56

57
Notation "()" := LitUnit : val_scope.
58
59
60
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
Notation "'ref' e" := (Alloc e%E)
  (at level 30, right associativity) : expr_scope.
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope.

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

76
Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
77
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
78
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
80
81

(* 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. *)
Ralf Jung's avatar
Ralf Jung committed
82
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
83
  (at level 200, f at level 1, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
84
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
85
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
86
  (at level 200, f at level 1, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
87
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
88
89
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.
90
91
92
93
94

(** 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. *)
Ralf Jung's avatar
Ralf Jung committed
95
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
96
  (at level 200, f, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
97
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
98
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
99
  (at level 200, f, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
100
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.
101

Robbert Krebbers's avatar
Robbert Krebbers committed
102
103
(* 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. *)
Ralf Jung's avatar
Ralf Jung committed
104
Notation "λ: x , e" := (Lam x%bind e%E)
105
  (at level 200, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
106
   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
107
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
108
  (at level 200, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
109
110
111
112
113
114
115
116
117
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.

(* When parsing lambdas, we want them to be locked (so as to avoid needless
unfolding by tactics and unification). However, unlocked lambda-values sometimes
appear as part of compound expressions, in which case we want them to be pretty
printed too. We achieve that by first defining the non-locked notation, and then
the locked notation. Both will be used for pretty-printing, but only the last
will be used for parsing. *)
Notation "λ: x , e" := (LamV x%bind e%E)
118
  (at level 200, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
119
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
120
Notation "λ: x , e" := (locked (LamV x%bind e%E))
121
  (at level 200, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
124
  (at level 200, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
125
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
126
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
127
  (at level 200, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
128
129
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.

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

137
(* Shortcircuit Boolean connectives *)
138
Notation "e1 && e2" :=
Robbert Krebbers's avatar
Oops.    
Robbert Krebbers committed
139
  (If e1%E e2%E (Lit (LitBool false))) (only parsing) : expr_scope.
140
Notation "e1 || e2" :=
Robbert Krebbers's avatar
Oops.    
Robbert Krebbers committed
141
  (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
142

143
(** Notations for option *)
144
145
Notation NONE := (InjL #()) (only parsing).
Notation SOME x := (InjR x) (only parsing).
146

147
148
Notation NONEV := (InjLV #()) (only parsing).
Notation SOMEV x := (InjRV x) (only parsing).
149
150
151

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