notation.v 7.02 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
61
62
63
64
65
66
67
68
69
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.
Notation "- e" := (UnOp MinusUnOp e%E)
  (at level 35, right associativity) : expr_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E)
  (at level 50, left associativity) : expr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
  (at level 50, left associativity) : expr_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) (at level 70) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope.
70
Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr_scope.
71
Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
72
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
73
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
75
76

(* 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
77
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
78
  (at level 102, f at level 1, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
79
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
80
Notation "'rec:' f x := e" := (locked (RecV f%bind x%bind e%E))
81
  (at level 102, f at level 1, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
82
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
83
84
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.
85
86
87
88
89

(** 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
90
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
91
  (at level 102, f, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
92
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
93
Notation "'rec:' f x y .. z := e" := (locked (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..)))
94
  (at level 102, f, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
95
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.
96

Robbert Krebbers's avatar
Robbert Krebbers committed
97
98
(* 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
99
Notation "λ: x , e" := (Lam x%bind e%E)
100
  (at level 102, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
101
   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
102
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
103
  (at level 102, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
104
105
106
107
108
109
110
111
112
113
114
   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)
  (at level 102, x at level 1, e at level 200,
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
115
Notation "λ: x , e" := (locked (LamV x%bind e%E))
116
  (at level 102, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
117
118
119
120
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
  (at level 102, x, y, z at level 1, e at level 200,
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.
121
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
122
  (at level 102, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
123
124
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.

125

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

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

139
(** Notations for option *)
140
141
Notation NONE := (InjL #()) (only parsing).
Notation SOME x := (InjR x) (only parsing).
142

143
144
Notation NONEV := (InjLV #()) (only parsing).
Notation SOMEV x := (InjRV x) (only parsing).
145
146
147

Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
  (Match e0 BAnon e1 x%bind e2)
148
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
149
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
150
151
  (Match e0 BAnon e1 x%bind e2)
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.