notation.v 6.52 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 6
Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.
7

8
Coercion LitInt : Z >-> base_lit.
9
Coercion LitBool : bool >-> base_lit.
10
Coercion LitLoc : loc >-> base_lit.
11
Coercion LitProphecy : proph_id >-> base_lit.
12

13
Coercion App : expr >-> Funclass.
14
Coercion Val : val >-> expr.
15

16 17
Coercion Var : string >-> expr.

18
Coercion BNamed : string >-> binder.
19
Notation "<>" := BAnon : binder_scope.
20

21 22
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
23
Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
24

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

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

60
Notation "()" := LitUnit : val_scope.
61
Notation "! e" := (Load e%E) (at level 9, right associativity) : expr_scope.
62
Notation "'ref' e" := (Alloc e%E) (at level 10) : expr_scope.
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77
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.

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

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

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

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

Notation "λ: x , e" := (LamV x%bind e%E)
114
  (at level 200, x at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
115 116
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
117
  (at level 200, x, y, z at level 1, e at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
118 119
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.

Ralf Jung's avatar
Ralf Jung committed
120
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
121
  (at level 200, x at level 1, e1, e2 at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
122
   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
123
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
124 125 126
  (at level 100, e2 at level 200,
   format "'[' '[hv' '[' e1 ']'  ;;  ']' '/' e2 ']'") : expr_scope.

127
(* Shortcircuit Boolean connectives *)
128
Notation "e1 && e2" :=
129
  (If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
130
Notation "e1 || e2" :=
131
  (If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.
132

133
(** Notations for option *)
134
Notation NONE := (InjL (LitV LitUnit)) (only parsing).
135
Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
136
Notation SOME x := (InjR x) (only parsing).
137 138
Notation SOMEV x := (InjRV x) (only parsing).

139 140
Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
  (Match e0 BAnon e1 x%bind e2)
141
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
142
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
143 144
  (Match e0 BAnon e1 x%bind e2)
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
145

Ralf Jung's avatar
Ralf Jung committed
146
Notation "'resolve_proph:' p 'to:' v" := (ResolveProph p v) (at level 100) : expr_scope.