Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

notation.v 9.15 KB
Newer Older
1
From cosmo.lang Require Export lang.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
2
3
4
5
6
7

(* This file is largely inspired from heap_lang's notation.v. *)

Delimit Scope expr_scope with E.
Delimit Scope val_scope with V.

8
9
Notation "e 'at' V" := (mkExpr e V) (at level 180) : expr_scope.
Notation "v 'at' V" := (mkVal v V) (at level 180) : val_scope.
10

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
11
(* Some coercions for expresions *)
Glen Mével's avatar
Glen Mével committed
12
Coercion LitLoc : location >-> lit.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
Coercion LitInt : Z >-> lit.
Coercion LitBool : bool >-> lit.

Coercion App : expr >-> Funclass.

Coercion Val : val >-> expr.
Coercion Var : string >-> expr.

(** 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).

(* 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)).

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

38
39
(** Syntax inspired by Coq/Ocaml. *)

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
40
41
Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : expr_scope.
Notation "( e1 , e2 , .. , en )" := (PairV .. (PairV e1 e2) .. en) : val_scope.
Glen Mével's avatar
Glen Mével committed
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
Notation "'let:' ( x , y1 , .. , yn ) := e1 'in' e2" :=
  (* this syntax unfolds to the following:
      let: x := e1 in
      let: yn := Snd x in
      let: x  := Fst x in
      ..
      let: y2 := Snd x in
      let: x  := Fst x in
      let: y1 := Snd x in
      let: x  := Fst x in
      e2
    we reuse the name x to store temporary results, so x must not be BAnon
  *)
  (Lam x%binder
    (Lam yn%binder
      (Lam x%binder
        (..
          (Lam y1%binder
            (Lam x%binder
              (e2%E)
              (Fst x%binder))
             (Snd x%binder)
          )
        ..)
        (Fst x%binder))
      (Snd x%binder))
    e1%E)
  (at level 200, x, y1, yn at level 1, e1, e2 at level 200,
   format "'[' 'let:'  (  x , y1  ,  ..  ,  yn  )  :=  '[' e1 ']'  'in'  '/' e2 ']'")
  : expr_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
  (Match e0 x1%binder e1 x2%binder e2)
  (e0, x1, e1, x2, e2 at level 200,
   format "'[hv' 'match:'  e0  'with'  '/  ' '[' 'InjL'  x1  =>  '/  ' e1 ']'  '/' '[' |  'InjR'  x2  =>  '/  ' e2 ']'  '/' 'end' ']'") : expr_scope.
Notation "'match:' e0 'with' 'InjR' x1 => e1 | 'InjL' x2 => e2 'end'" :=
  (Match e0 x2%binder e2 x1%binder e1)
  (e0, x1, e1, x2, e2 at level 200, only parsing) : expr_scope.
(*
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
*)
Glen Mével's avatar
Glen Mével committed
102

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
103
Notation "()" := LitUnit : val_scope.
Glen Mével's avatar
Glen Mével committed
104

Glen Mével's avatar
Glen Mével committed
105
Notation "'ref' e" := (Alloc NonAtomic (Val$LitV$LitInt 1) e%E) (at level 10) : expr_scope.
106
107
Notation "! e" := (Read NonAtomic e%E (Val$LitV$LitInt 0)) (at level 9, right associativity) : expr_scope.
Notation "e1 <- e2" := (Write NonAtomic e1%E (Val$LitV$LitInt 0) e2%E) (at level 80) : expr_scope.
Glen Mével's avatar
Glen Mével committed
108
109
(* The unicode  is already part of the notation "_ ← _; _" for bind. *)

Glen Mével's avatar
Glen Mével committed
110
Notation "'ref_at' e" := (Alloc Atomic (Val$LitV$LitInt 1) e%E) (at level 10) : expr_scope.
111
112
113
114
Notation "!at e" := (Read Atomic e%E (Val$LitV$LitInt 0)) (at level 9, right associativity) : expr_scope.
Notation "e1 <-at e2" := (Write Atomic e1%E (Val$LitV$LitInt 0) e2%E) (at level 80) : expr_scope.

Notation CAS_ref e1 e2 e3 := (CAS e1 (Val$LitV$LitInt 0) e2 e3).
Glen Mével's avatar
Glen Mével committed
115

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
116
Notation "- e" := (UnOp MinusUnOp e%E) : expr_scope.
117
Notation "¬ e" := (UnOp NotOp e%E)%E : expr_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
118
119
120

Notation "e1 + e2" := (BinOp PlusOp e1%E e2%E) : expr_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E) : expr_scope.
121
122
123
Notation "e1 * e2" := (BinOp MultOp e1%E e2%E) : expr_scope.
Notation "e1 / e2" := (BinOp DivOp e1%E e2%E) : expr_scope.
Notation "e1 `mod` e2" := (BinOp ModOp e1%E e2%E) : expr_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
124
125
Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) : expr_scope.
Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) : expr_scope.
126
127
128
Notation "e1 ≠ e2" := (¬ (e1%E = e2%E))%E : expr_scope.
Notation "e1 ∧ e2" := (BinOp AndOp e1%E e2%E) : expr_scope.
Notation "e1 ∨ e2" := (BinOp OrOp e1%E e2%E) : expr_scope.
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
129

130
131
132
133
134
135
(* Short-circuited Boolean connectives *)
Notation "e1 && e2" :=
  (If e1%E e2%E (LitV (LitBool false))) (only parsing) : expr_scope.
Notation "e1 || e2" :=
  (If e1%E (LitV (LitBool true)) e2%E) (only parsing) : expr_scope.

Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
(* 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. *)
Notation "'rec:' f x := e" := (Rec f%binder x%binder e%E)
  (at level 200, f at level 1, x at level 1, e at level 200,
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : expr_scope.
Notation "'rec:' f x := e" := (RecV f%binder x%binder e%E)
  (at level 200, f at level 1, x at level 1, e at level 200,
   format "'[' 'rec:'  f  x  :=  '/  ' e ']'") : val_scope.
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.

(** 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. *)
Notation "'rec:' f x y .. z := e" := (Rec f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
  (at level 200, f, x, y, z at level 1, e at level 200,
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : expr_scope.
Notation "'rec:' f x y .. z := e" := (RecV f%binder x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
  (at level 200, f, x, y, z at level 1, e at level 200,
   format "'[' 'rec:'  f  x  y  ..  z  :=  '/  ' e ']'") : val_scope.

(* 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. *)
Notation "λ: x , e" := (Lam x%binder e%E)
  (at level 200, x at level 1, e at level 200,
   format "'[' 'λ:'  x ,  '/  ' e ']'") : expr_scope.
Notation "λ: x y .. z , e" := (Lam x%binder (Lam y%binder .. (Lam z%binder e%E) ..))
  (at level 200, x, y, z at level 1, e at level 200,
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : expr_scope.

Notation "λ: x , e" := (LamV x%binder e%E)
  (at level 200, x at level 1, e at level 200,
   format "'[' 'λ:'  x ,  '/  ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%binder (Lam y%binder .. (Lam z%binder e%E) .. ))
  (at level 200, x, y, z at level 1, e at level 200,
   format "'[' 'λ:'  x  y  ..  z ,  '/  ' e ']'") : val_scope.

Notation "'let:' x := e1 'in' e2" := (Lam x%binder e2%E e1%E)
  (at level 200, x at level 1, e1, e2 at level 200,
   format "'[' 'let:'  x  :=  '[' e1 ']'  'in'  '/' e2 ']'") : expr_scope.
Notation "e1 ;; e2" := (Lam BAnon e2%E e1%E)
  (at level 100, e2 at level 200,
   format "'[' '[hv' '[' e1 ']'  ;;  ']' '/' e2 ']'") : expr_scope.

(** Notations for option *)
Notation NONE := (InjL (LitV LitUnit)) (only parsing).
Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
Notation SOME x := (InjR x) (only parsing).
Notation SOMEV x := (InjRV x) (only parsing).

Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
  (Match e0 BAnon e1 x%binder e2)
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 'end'" :=
  (Match e0 BAnon e1 x%binder e2)
  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220

(** Shaky notations for imperative constructs *)

(* Beware! This notation captures the variable "_while". *)
Notation While cond body :=
  ((rec: "_while" <> :=
    if: cond then
      body ;; "_while" #()
    else
      #()
  ) #())%E.
Notation "'while:' e1 'do' e2 'enddo'" := (While e1%E e2%E)
  (at level 200, e1, e2 at level 200,
   format "'[' 'while:'  e1  'do'  '/  ' e2  '/' 'enddo' ']'") : expr_scope.

(* Beware! This notation captures the variables "_for", "_i", "_start" and "_stop". *)
Notation For iname start stop body :=
  ((let: "_stop" := stop in
    rec: "_for" "_i" :=
      if: "_i"  "_stop" then
        let: iname := "_i" in
        body ;; "_for" ("_i" + #1)
      else
        #()
   ) start)%E.
Notation "'for:' i 'from' e1 'to' e2 'do' e3 'enddo'" := (For i e1%E e2%E e3%E)
  (at level 200, e1, e2, e3 at level 200,
   format "'[' 'for:'  i  'from'  e1  'to'  e2  'do'  '/  ' e3  '/' 'enddo' ']'") : expr_scope.