notation.v 5.71 KB
Newer Older
1
From iris.heap_lang Require Export derived.
2
Export heap_lang.
3

4
Arguments wp {_ _} _ _%E _.
5

6
Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
7
  (at level 20, e, Φ at level 200,
8 9
   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
Notation "'WP' e {{ Φ } }" := (wp  e%E Φ)
10
  (at level 20, e, Φ at level 200,
11
   format "'WP'  e  {{  Φ  } }") : uPred_scope.
12

13 14 15 16 17 18 19
Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
Notation "'WP' e {{ v , Q } }" := (wp  e%E (λ v, Q))
  (at level 20, e, Q at level 200,
   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.

20
Coercion LitInt : Z >-> base_lit.
21
Coercion LitBool : bool >-> base_lit.
22 23
Coercion LitLoc : loc >-> base_lit.

24 25 26
Coercion App : expr >-> Funclass.
Coercion of_val : val >-> expr.

27
Coercion BNamed : string >-> binder.
28
Notation "<>" := BAnon : binder_scope.
29

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

Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
36
Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
37

38 39 40
(** 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
41
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
42
Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
Ralf Jung's avatar
Ralf Jung committed
43
  (Match e0 x1%bind e1 x2%bind e2)
44
  (e0, x1, e1, x2, e2 at level 200) : expr_scope.
45
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
Ralf Jung's avatar
Ralf Jung committed
46
  (Match e0 x2%bind e2 x1%bind e1)
47
  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
48
Notation "()" := LitUnit : val_scope.
49 50 51 52 53 54 55 56 57 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.
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.
61
Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr_scope.
62
Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
63
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
64
Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
65
Notation "'rec:' f x := e" := (Rec f%bind x%bind e%E)
66
  (at level 102, f at level 1, x at level 1, e at level 200) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
67
Notation "'rec:' f x := e" := (RecV f%bind x%bind e%E)
68
  (at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
69 70
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.
71 72 73 74 75

(** 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
76
Notation "'rec:' f x y := e" := (Rec f%bind x%bind (Lam y%bind e%E))
77
  (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
78
Notation "'rec:' f x y := e" := (RecV f%bind x%bind (Lam y%bind e%E))
79
  (at level 102, f, x, y at level 1, e at level 200) : val_scope.
Ralf Jung's avatar
Ralf Jung committed
80
Notation "'rec:' f x y .. z := e" := (Rec f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
81
  (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
82
Notation "'rec:' f x y .. z := e" := (RecV f%bind x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
83 84
  (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.

Ralf Jung's avatar
Ralf Jung committed
85
Notation "λ: x , e" := (Lam x%bind e%E)
86
  (at level 102, x at level 1, e at level 200) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
87
Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
88
  (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
Ralf Jung's avatar
Ralf Jung committed
89
Notation "λ: x , e" := (LamV x%bind e%E)
90
  (at level 102, x at level 1, e at level 200) : val_scope.
Ralf Jung's avatar
Ralf Jung committed
91
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
92
  (at level 102, x, y, z at level 1, e at level 200) : val_scope.
93

Ralf Jung's avatar
Ralf Jung committed
94
Notation "'let:' x := e1 'in' e2" := (Lam x%bind e2%E e1%E)
95 96 97
  (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
  (at level 100, e2 at level 200, format "e1  ;;  e2") : expr_scope.
98
(* These are not actually values, but we want them to be pretty-printed. *)
Ralf Jung's avatar
Ralf Jung committed
99
Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E)
100
  (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
101
Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
102
  (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
103

104 105 106 107
(* Shortcircuit Boolean connectives *)
Notation "e1 && e2" := (If e1%E e2%E (Lit (LitBool false))) : expr_scope.
Notation "e1 || e2" := (If e1%E (Lit (LitBool true)) e2%E) : expr_scope.

108 109 110 111 112 113 114 115 116 117 118 119 120
(** Notations for option *)
Notation NONE := (InjL #()).
Notation SOME x := (InjR x).

Notation NONEV := (InjLV #()).
Notation SOMEV x := (InjRV x).

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