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.

parser.mly 32 KB
Newer Older
1
2
/**************************************************************************/
/*                                                                        */
3
/*  Copyright (C) 2010-2011                                               */
MARCHE Claude's avatar
MARCHE Claude committed
4
5
6
/*    François Bobot                                                     */
/*    Jean-Christophe Filliâtre                                          */
/*    Claude Marché                                                      */
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
7
/*    Andrei Paskevich                                                    */
8
9
10
11
12
13
14
15
16
17
18
/*                                                                        */
/*  This software is free software; you can redistribute it and/or        */
/*  modify it under the terms of the GNU Library General Public           */
/*  License version 2.1, with the special exception on linking            */
/*  described in file LICENSE.                                            */
/*                                                                        */
/*  This software is distributed in the hope that it will be useful,      */
/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  */
/*                                                                        */
/**************************************************************************/
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
19
20

%{
21
module Incremental = struct
22
23
24
25
26
27
28
29
30
31
32
33
  let env_ref  = ref []
  let lenv_ref = ref []
  let uc_ref   = ref []

  let ref_get  ref = List.hd !ref
  let ref_tail ref = List.tl !ref
  let ref_drop ref = ref := ref_tail ref
  let ref_pop  ref = let v = ref_get ref in ref_drop ref; v

  let ref_push ref v = ref := v :: !ref
  let ref_set  ref v = ref := v :: ref_tail ref

34
  let open_logic_file env =
35
    ref_push env_ref env; ref_push lenv_ref Util.Mstr.empty
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56

  let close_logic_file () =
    ref_drop env_ref; ref_pop lenv_ref

  let open_theory id =
    ref_push uc_ref (Theory.create_theory (Denv.create_user_id id))

  let close_theory loc =
    let uc = ref_pop uc_ref in
    ref_set lenv_ref (Typing.close_theory loc (ref_get lenv_ref) uc)

  let open_namespace () =
    ref_set uc_ref (Theory.open_namespace (ref_get uc_ref))

  let close_namespace loc import name =
    ref_set uc_ref (Typing.close_namespace loc import name (ref_get uc_ref))

  let new_decl d =
    let env = ref_get env_ref in let lenv = ref_get lenv_ref in
    ref_set uc_ref (Typing.add_decl env lenv (ref_get uc_ref) d)
end
57

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
59
60
61
  open Ptree
  open Parsing

  let loc () = (symbol_start_pos (), symbol_end_pos ())
62
63
  let floc () = Loc.extract (loc ())

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
64
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
65
  let floc_i i = Loc.extract (loc_i i)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
67
  let floc_ij i j = Loc.extract (loc_ij i j)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
68
69

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
70
71
  let mk_pp d = mk_ppl (floc ()) d
  let mk_pp_i i d = mk_ppl (floc_i i) d
72

73
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
74

75
  let infix_ppl loc a i b = mk_ppl loc (PPbinop (a, i, b))
76
  let infix_pp a i b = infix_ppl (floc ()) a i b
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
77

78
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
79
  let prefix_pp p a = prefix_ppl (floc ()) p a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80

81
  let infix  s = "infix "  ^ s
82
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
83
  let mixfix s = "mixfix " ^ s
84

85
86
87
88
  let mk_id id loc = { id = id; id_lab = []; id_loc = loc }

  let add_lab id l = { id with id_lab = l }

Andrei Paskevich's avatar
Andrei Paskevich committed
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
  let mk_l_prefix op e1 =
    let id = mk_id (prefix op) (floc_i 1) in
    mk_pp (PPapp (Qident id, [e1]))

  let mk_l_infix e1 op e2 =
    let id = mk_id (infix op) (floc_i 2) in
    mk_pp (PPinfix (e1, id, e2))

  let mk_l_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
    mk_pp (PPapp (Qident id, [e1;e2]))

  let mk_l_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
    mk_pp (PPapp (Qident id, [e1;e2;e3]))

105
106
107
108
109
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )
110

111
112
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
113
114
115
116
117
118
119

  let cast_body c ((p,e,q) as t) = match c with
    | None -> t
    | Some pt -> p, { e with expr_desc = Ecast (e, pt) }, q

  let rec mk_apply f = function
    | [] ->
120
        assert false
121
    | [a] ->
122
        Eapply (f, a)
123
    | a :: l ->
124
125
        let loc = Loc.join f.expr_loc a.expr_loc in
        mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
126
127
128
129
130
131
132

  let mk_apply_id id =
    let e =
      { expr_desc = Eident (Qident id); expr_loc = id.id_loc }
    in
    mk_apply e

Andrei Paskevich's avatar
Andrei Paskevich committed
133
134
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
135
136
    mk_expr (mk_apply_id id [e1; e2])

Andrei Paskevich's avatar
Andrei Paskevich committed
137
138
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
139
140
    mk_expr (mk_apply_id id [e1; e2; e3])

141
  let mk_infix e1 op e2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
142
    let id = mk_id (infix op) (floc_i 2) in
143
144
145
    mk_expr (mk_apply_id id [e1; e2])

  let mk_prefix op e1 =
Andrei Paskevich's avatar
Andrei Paskevich committed
146
    let id = mk_id (prefix op) (floc_i 1) in
147
148
    mk_expr (mk_apply_id id [e1])

Andrei Paskevich's avatar
Andrei Paskevich committed
149
150
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
151
  let ty_unit () = Tpure (PPTtuple [])
152

Andrei Paskevich's avatar
Andrei Paskevich committed
153
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
154
155
156
157
158
159
160
161

  let empty_effect = { pe_reads = []; pe_writes = []; pe_raises = [] }

  let type_c p ty ef q =
    { pc_result_type = ty;
      pc_effect      = ef;
      pc_pre         = p;
      pc_post        = q; }
162
163
164
165
166

  let add_init_label e =
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
    { e with expr_desc = Elabel (init, e) }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
167
168
%}

169
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
170

171
%token <string> LIDENT UIDENT
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
172
%token <string> INTEGER
173
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174
175
%token <Ptree.real_constant> FLOAT
%token <string> STRING
176
%token <Loc.position> POSITION
177
178
179

/* keywords */

180
181
%token AND AS AXIOM CLONE
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
182
%token GOAL IF IFF IMPLIES IMPORT IN INDUCTIVE LEMMA
183
%token LET LOGIC MATCH META NAMESPACE NOT PROP OR
Andrei Paskevich's avatar
Andrei Paskevich committed
184
%token THEN THEORY TRUE TYPE USE WITH
185

186
187
/* program keywords */

188
189
190
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token EXCEPTION FOR
%token FUN INVARIANT LABEL LOOP MODEL MODULE MUTABLE PARAMETER RAISE
191
192
%token RAISES READS REC TO TRY VARIANT WHILE WRITES

193
194
/* symbols */

195
%token ARROW
196
%token BACKQUOTE BAR
197
%token COLON COMMA
198
%token DOT EQUAL FUNC LAMBDA LTGT
199
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTREC LEFTSQ
200
%token LARROW LRARROW
201
%token PRED QUOTE
202
%token RIGHTPAR RIGHTREC RIGHTSQ
203
%token TILDE UNDERSCORE
204
205
206

%token EOF

207
208
/* program symbols */

209
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
210

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
211
212
/* Precedences */

213
%nonassoc prec_label
214
215
216
217
218
219
220
221
222
223
%nonassoc prec_post
%nonassoc BAR

%nonassoc prec_triple
%nonassoc prec_simple

%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
%nonassoc DOT ELSE
224
%nonassoc prec_named
225
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
226

227
%right ARROW IMPLIES LRARROW IFF
228
229
%right OR BARBAR
%right AND AMPAMP
230
%nonassoc NOT TILDE
231
%left EQUAL LTGT OP1
232
233
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
234
%left OP2
235
%left OP3
236
%left OP4
237
%nonassoc prec_prefix_op
238
%left prec_app
239
240
%nonassoc LEFTSQ
%nonassoc OPPREF
241

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
242
243
/* Entry points */

244
245
%type <Env.env -> unit> pre_logic_file
%start pre_logic_file
246
%type <Theory.theory Util.Mstr.t> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
247
%start logic_file
248
249
%type <Ptree.program_file> program_file
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
250
251
%%

252
253
254
255
pre_logic_file:
| /* epsilon */  { Incremental.open_logic_file }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
256
logic_file:
257
| list0_theory EOF  { Incremental.close_logic_file () }
258
259
260
;

/* File, theory, namespace */
261

262
263
264
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
265
266
;

267
theory_head:
268
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
269
270
;

271
theory:
272
| theory_head list0_decl END  { Incremental.close_theory (floc_i 1) }
273
274
;

275
list0_decl:
276
277
278
279
280
281
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
282
   { Incremental.new_decl $1 }
283
| namespace_head namespace_import namespace_name list0_decl END
284
   { Incremental.close_namespace (floc_i 3) $2 $3 }
285
286
;

287
namespace_head:
288
| NAMESPACE  { Incremental.open_namespace () }
289
290
291
292
293
294
295
296
297
298
299
300
301
302
;

namespace_import:
| /* epsilon */  { false }
| IMPORT         { true }
;

namespace_name:
| uident      { Some $1 }
| UNDERSCORE  { None }
;

/* Declaration */

303
decl:
304
305
306
307
308
309
| TYPE list1_type_decl
    { TypeDecl $2 }
| LOGIC list1_logic_decl
    { LogicDecl $2 }
| INDUCTIVE list1_inductive_decl
    { IndDecl $2 }
310
| AXIOM ident labels COLON lexpr
311
    { PropDecl (floc (), Kaxiom, add_lab $2 $3, $5) }
312
| LEMMA ident labels COLON lexpr
313
    { PropDecl (floc (), Klemma, add_lab $2 $3, $5) }
314
| GOAL ident labels COLON lexpr
315
    { PropDecl (floc (), Kgoal, add_lab $2 $3, $5) }
316
| USE use
317
    { UseClone (floc (), $2, None) }
318
| CLONE use clone_subst
319
    { UseClone (floc (), $2, Some $3) }
320
| META ident list1_meta_arg_sep_comma
321
    { Meta (floc (), $2, $3) }
322
| META STRING list1_meta_arg_sep_comma
323
    { Meta (floc (), mk_id $2 (floc_i 2), $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
324
325
;

326
327
328
329
330
331
332
333
334
/* Use and clone */

use:
| imp_exp tqualid
    { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
| imp_exp tqualid AS uident
    { { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
    { { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
335
336
;

337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
imp_exp:
| IMPORT        { Import }
| EXPORT        { Export }
| /* epsilon */ { Nothing }
;

clone_subst:
| /* epsilon */          { [] }
| WITH list1_comma_subst { $2 }
;

list1_comma_subst:
| subst                         { [$1] }
| subst COMMA list1_comma_subst { $1 :: $3 }
;

subst:
354
| NAMESPACE ns EQUAL ns     { CSns   ($2, $4) }
355
356
357
358
359
360
| TYPE  qualid EQUAL qualid { CStsym ($2, $4) }
| LOGIC qualid EQUAL qualid { CSlsym ($2, $4) }
| LEMMA qualid              { CSlemma $2 }
| GOAL  qualid              { CSgoal  $2 }
;

361
362
363
364
365
ns:
| uqualid { Some $1 }
| DOT     { None }
;

366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
/* Meta args */

list1_meta_arg_sep_comma:
| meta_arg                                { [$1] }
| meta_arg COMMA list1_meta_arg_sep_comma { $1 :: $3 }
;

meta_arg:
| TYPE  qualid { PMAts  $2 }
| LOGIC qualid { PMAls  $2 }
| PROP  qualid { PMApr  $2 }
| STRING       { PMAstr $1 }
| INTEGER      { PMAint $1 }
;

381
382
383
/* Type declarations */

list1_type_decl:
384
385
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
386
387
388
;

type_decl:
389
| lident labels type_args typedefn
390
391
392
  { let model, def = $4 in
    { td_loc = floc (); td_ident = add_lab $1 $2;
      td_params = $3; td_model = model; td_def = def } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
393
394
;

395
type_args:
396
397
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
398
399
400
;

typedefn:
401
402
403
404
405
406
407
408
409
410
| /* epsilon */                 { false, TDabstract }
| equal_model primitive_type    { $1, TDalias $2 }
| equal_model typecases         { $1, TDalgebraic $2 }
| equal_model BAR typecases     { $1, TDalgebraic $3 }
| equal_model record_type       { $1, TDrecord $2 }
;

equal_model:
| EQUAL { false }
| MODEL { true }
411
412
413
;

record_type:
Andrei Paskevich's avatar
Andrei Paskevich committed
414
| LEFTREC list1_record_field opt_semicolon RIGHTREC { List.rev $2 }
415
416
417
418
;

list1_record_field:
| record_field                              { [$1] }
419
| list1_record_field SEMICOLON record_field { $3 :: $1 }
420
421
422
;

record_field:
423
| opt_mutable lident labels COLON primitive_type
424
   { floc (), $1, add_lab $2 $3, $5 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
425
426
427
428
429
430
431
432
;

typecases:
| typecase                { [$1] }
| typecase BAR typecases  { $1::$3 }
;

typecase:
433
| uident labels params   { (floc (), add_lab $1 $2, $3) }
434
435
436
437
438
;

/* Logic declarations */

list1_logic_decl:
439
440
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
441
442
443
;

logic_decl:
444
| lident_rich labels params logic_type_option logic_def_option
445
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
446
      ld_params = $3; ld_type = $4; ld_def = $5 } }
447
448
449
450
451
452
453
454
455
456
;

logic_type_option:
| /* epsilon */        { None }
| COLON primitive_type { Some $2 }
;

logic_def_option:
| /* epsilon */ { None }
| EQUAL lexpr   { Some $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
457
458
;

459
460
461
/* Inductive declarations */

list1_inductive_decl:
462
463
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
464
465
466
;

inductive_decl:
467
| lident_rich labels params inddefn
468
  { { in_loc = floc (); in_ident = add_lab $1 $2;
469
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
470
;
471

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
472
473
474
475
476
477
478
479
480
481
482
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

indcases:
| indcase               { [$1] }
| indcase BAR indcases  { $1::$3 }
;

indcase:
483
| ident labels COLON lexpr { (floc (), add_lab $1 $2, $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
484
485
;

486
487
488
489
490
491
492
493
/* Type expressions */

primitive_type:
| primitive_type_arg           { $1 }
| lqualid primitive_type_args  { PPTtyapp ($2, $1) }
;

primitive_type_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
494
495
| primitive_type_arg_non_lident           { $1 }
| uqualid DOT lident primitive_type_args  { PPTtyapp ($4, Qdot ($1, $3)) }
496
497
498
499
500
501
502
503
;

primitive_type_args:
| primitive_type_arg                      { [$1] }
| primitive_type_arg primitive_type_args  { $1 :: $2 }
;

primitive_type_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
504
| lident                         { PPTtyapp ([], Qident $1) }
505
506
507
508
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
509
510
| uqualid DOT lident
   { PPTtyapp ([], Qdot ($1, $3)) }
511
512
513
514
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
515
516
517
518
519
520
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
521
522
523
524
525
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

526
527
type_var:
| QUOTE ident { $2 }
528
529
;

530
531
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
532
lexpr:
533
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
534
   { infix_pp $1 PPimplies $3 }
535
536
| lexpr IMPLIES lexpr
   { infix_pp $1 PPimplies $3 }
537
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
538
   { infix_pp $1 PPiff $3 }
539
540
| lexpr IFF lexpr
   { infix_pp $1 PPiff $3 }
541
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
542
   { infix_pp $1 PPor $3 }
543
| lexpr BARBAR lexpr
544
   { mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPor $3)) }
545
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
546
   { infix_pp $1 PPand $3 }
547
| lexpr AMPAMP lexpr
548
   { mk_pp (PPnamed (Lstr "asym_split", infix_pp $1 PPand $3)) }
549
550
| TILDE lexpr
   { prefix_pp PPnot $2 }
551
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
552
   { prefix_pp PPnot $2 }
553
| lexpr EQUAL lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
554
   { mk_l_infix $1 "=" $3 }
555
| lexpr LTGT lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
556
   { prefix_pp PPnot (mk_l_infix $1 "=" $3) }
557
| lexpr OP1 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
558
   { mk_l_infix $1 $2 $3 }
559
| lexpr OP2 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
560
   { mk_l_infix $1 $2 $3 }
561
| lexpr OP3 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
562
   { mk_l_infix $1 $2 $3 }
563
| lexpr OP4 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
564
   { mk_l_infix $1 $2 $3 }
565
| prefix_op lexpr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
566
   { mk_l_prefix $1 $2 }
567
568
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
569
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
570
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
571
572
| quant list1_param_var_sep_comma triggers DOT lexpr
   { mk_pp (PPquant ($1, $2, $3, $5)) }
573
574
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
575
| LET pattern EQUAL lexpr IN lexpr
576
577
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
578
579
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
580
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
581
582
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
583
584
| EPSILON lident labels COLON primitive_type DOT lexpr
   { mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
585
| lexpr COLON primitive_type
586
   { mk_pp (PPcast ($1, $3)) }
587
| lexpr_arg
588
589
590
   { $1 }
;

591
592
593
594
595
596
597
598
599
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

field_value:
| lqualid EQUAL lexpr { $1, $3 }
;

600
601
602
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
603
;
604

605
constant:
Andrei Paskevich's avatar
Andrei Paskevich committed
606
607
| INTEGER   { Term.ConstInt $1 }
| FLOAT     { Term.ConstReal $1 }
608
609
;

610
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
611
612
613
614
615
616
| qualid            { mk_pp (PPvar $1) }
| constant          { mk_pp (PPconst $1) }
| TRUE              { mk_pp PPtrue }
| FALSE             { mk_pp PPfalse }
| OPPREF lexpr_arg  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
617
618
619
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
620
621
622
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
623
624
625
;

lexpr_sub:
626
| lexpr_dot DOT lqualid_rich
Andrei Paskevich's avatar
Andrei Paskevich committed
627
   { mk_pp (PPapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
628
629
| LEFTPAR lexpr RIGHTPAR
   { $2 }
630
631
632
633
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
634
635
| LEFTREC list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPrecord (List.rev $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
636
637
| LEFTREC lexpr_arg WITH list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPupdate ($2, List.rev $4)) }
638
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
639
   { mk_l_mixfix2 "[]" $1 $3 }
640
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
641
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
642
;
643

Andrei Paskevich's avatar
Andrei Paskevich committed
644
645
646
647
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
648
649
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
650
651
;

652
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
653

654
655
656
657
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
658

659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
list1_trigger_sep_bar:
| trigger                           { [$1] }
| trigger BAR list1_trigger_sep_bar { $1 :: $3 }
;

trigger:
| list1_lexpr_sep_comma { $1 }
;

list1_lexpr_sep_comma:
| lexpr                             { [$1] }
| lexpr COMMA list1_lexpr_sep_comma { $1 :: $3 }
;

/* Match expressions */
674

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
675
676
677
678
679
680
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
681
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
682
683
684
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
| pat_conj              { $1 }
| pat_conj BAR pattern  { mk_pat (PPpor ($1, $3)) }
;

pat_conj:
| pat_uni                      { $1 }
| pat_uni COMMA list1_pat_uni  { mk_pat (PPptuple ($1::$3)) }
;

list1_pat_uni:
| pat_uni                      { [$1] }
| pat_uni COMMA list1_pat_uni  { $1::$3 }
;

pat_uni:
700
701
702
| pat_arg                   { $1 }
| uqualid list1_pat_arg     { mk_pat (PPpapp ($1, $2)) }
| pat_uni AS lident labels  { mk_pat (PPpas ($1, add_lab $3 $4)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
703
;
704

705
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
706
707
708
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
709

710
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
711
| UNDERSCORE                { mk_pat (PPpwild) }
712
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
713
714
715
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
716
717
718
719
720
721
722
723
724
725
| LEFTREC pfields RIGHTREC  { mk_pat (PPprec $2) }
;

pfields:
| pat_field opt_semicolon       { [$1] }
| pat_field SEMICOLON pfields   { $1::$3 }
;

pat_field:
| lqualid EQUAL pattern   { ($1, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
726
727
;

728
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
729

730
731
732
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
733
734
;

735
736
737
738
739
740
741
742
743
744
745
746
747
param:
| LEFTPAR param_var RIGHTPAR
   { $2 }
| LEFTPAR param_type RIGHTPAR
   { [None, $2] }
| LEFTPAR param_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { [None, PPTtuple ($2::$4)] }
| LEFTPAR RIGHTPAR
   { [None, PPTtuple []] }
| type_var
   { [None, PPTtyvar $1] }
| lqualid
   { [None, PPTtyapp ([], $1)] }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
748
749
;

750
751
752
753
754
755
756
757
param_type:
| lident param_type_cont
   { PPTtyapp ($2, Qident $1) }
| lident list1_lident param_type_cont
   { let id2ty i = PPTtyapp ([], Qident i) in
     PPTtyapp (List.map id2ty $2 @ $3, Qident $1) }
| primitive_type_non_lident
   { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
758
759
;

760
761
762
763
param_type_cont:
| /* epsilon */                                      { [] }
| primitive_type_arg_non_lident                      { [$1] }
| primitive_type_arg_non_lident primitive_type_args  { $1 :: $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
764
765
;

766
767
768
list1_param_var_sep_comma:
| param_var                                  { $1 }
| param_var COMMA list1_param_var_sep_comma  { $1 @ $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
769
770
;

771
772
773
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
774
775
776
777
778
779
| list1_lident label labels list0_lident_labels COLON primitive_type
   { let l = match List.rev $1 with
       | i :: l -> add_lab i ($2 :: $3) :: l
       | [] -> assert false
     in
     List.map (fun id -> (Some id, $6)) (List.rev_append l $4) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
780
781
;

782
list1_lident:
783
784
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
785
786
;

787
788
789
790
791
list0_lident_labels:
| /* epsilon */                      { [] }
| lident labels list0_lident_labels  { add_lab $1 $2 :: $3 }
;

792
793
794
795
796
/* Idents */

ident:
| uident { $1 }
| lident { $1 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
797
798
;

Andrei Paskevich's avatar
Andrei Paskevich committed
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
uident:
| UIDENT          { mk_id $1 (floc ()) }
;

lident:
| LIDENT          { mk_id $1 (floc ()) }
| lident_keyword  { mk_id $1 (floc ()) }
;

lident_keyword:
| MODEL           { "model" }
;

/* Idents + symbolic operations' names */

814
815
816
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
817
818
;

819
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
820
821
822
| lident                      { $1 }
| LEFTPAR lident_op RIGHTPAR  { mk_id $2 (floc ()) }
| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") (floc ()) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
823
824
;

825
lident_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
826
827
828
829
830
831
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
832
833
;

834
prefix_op:
835
836
837
838
839
840
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
841
/* Qualified idents */
842

Andrei Paskevich's avatar
Andrei Paskevich committed
843
844
845
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
846
847
;

Andrei Paskevich's avatar
Andrei Paskevich committed
848
849
850
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
851
852
853
;

lqualid:
Andrei Paskevich's avatar
Andrei Paskevich committed
854
855
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
856
857
;

Andrei Paskevich's avatar
Andrei Paskevich committed
858
859
860
861
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
862
863
;

Andrei Paskevich's avatar
Andrei Paskevich committed
864
865
866
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
867
868
;

Andrei Paskevich's avatar
Andrei Paskevich committed
869
870
/* Theory/Module names */

871
872
873
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
874
;
875

Andrei Paskevich's avatar
Andrei Paskevich committed
876
877
878
any_qualid:
| ident                 { Qident $1 }
| any_qualid DOT ident  { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
879
;
880
881
882

/* Misc */

883
label:
Andrei Paskevich's avatar
Andrei Paskevich committed
884
885
| STRING    { Lstr $1 }
| POSITION  { Lpos $1 }
886
887
;

888
889
890
891
892
labels:
| /* epsilon */ { [] }
| label labels  { $1 :: $2 }
;

893
894
895
bar_:
| /* epsilon */ { () }
| BAR           { () }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
896
897
;

898
899
900
/****************************************************************************/

program_file:
901
| list0_theory_or_module_ EOF { $1 }
902
903
;

904
list0_theory_or_module_:
905
906
| /* epsilon */
   { [] }
907
| list1_theory_or_module_
908
909
910
   { $1 }
;

911
912
list1_theory_or_module_:
| theory_or_module_
913
   { [$1] }
914
| theory_or_module_ list1_theory_or_module_
915
916
917
   { $1 :: $2 }
;

918
919
920
theory_or_module_:
| THEORY uident labels list0_full_decl END
   { { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
921
922
923
924
| MODULE uident labels list0_program_decl END
   { { mod_name = $2; mod_labels = $3; mod_decl = $4 } }
;

925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
list0_full_decl:
| /* epsilon */
   { [] }
| list1_full_decl
   { $1 }
;

list1_full_decl:
| full_decl
   { [$1] }
| full_decl list1_full_decl
   { $1 :: $2 }
;

full_decl:
| NAMESPACE namespace_import namespace_name list0_full_decl END
941
   { Dnamespace (floc_i 3, $3, $2, $4) }
942
943
944
945
| decl
   { Dlogic $1 }
;

946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
list0_program_decl:
| /* epsilon */
   { [] }
| list1_program_decl
   { $1 }
;

list1_program_decl:
| program_decl
   { [$1] }
| program_decl list1_program_decl
   { $1 :: $2 }
;

program_decl:
| decl
    { Dlogic $1 }
963
| LET lident_rich labels list1_type_v_binder opt_cast EQUAL triple
964
    { Dlet (add_lab $2 $3, mk_expr_i 7 (Efun ($4, cast_body $5 $7))) }
965
| LET lident_rich labels EQUAL FUN list1_type_v_binder ARROW triple
966
967
968
    { Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET REC list1_recfun_sep_and
    { Dletrec $3 }
969
| PARAMETER lident_rich_pgm labels COLON type_v
970
    { Dparam (add_lab $2 $3, $5) }
971
972
973
| PARAMETER lident_rich_pgm labels list1_type_v_param COLON type_c
    { let tv = Tarrow ($4, $6) in
      Dparam (add_lab $2 $3, tv) }
974
975
976
977
978
979
| EXCEPTION uident labels
    { Dexn (add_lab $2 $3, None) }
| EXCEPTION uident labels pure_type
    { Dexn (add_lab $2 $3, Some $4) }
| USE use_module
    { $2 }
980
| NAMESPACE namespace_import namespace_name list0_program_decl END
981
    { Dnamespace (floc_i 3, $3, $2, $4) }
982
983
;

984
985
986
987
lident_rich_pgm:
| lident_rich
    { $1 }
| LEFTPAR LEFTSQ RIGHTSQ LARROW RIGHTPAR
Andrei Paskevich's avatar
Andrei Paskevich committed
988
    { mk_id (mixfix "[]<-") (floc ()) }
989
990
991
992
993
994
995
996
997
998
;

opt_mutable:
| /* epsilon */ { false }
| MUTABLE       { true  }
;

opt_semicolon:
| /* epsilon */ {}
| SEMICOLON     {}
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
;

use_module:
| imp_exp MODULE tqualid
    { Duse ($3, $1, None) }
| imp_exp MODULE tqualid AS uident
    { Duse ($3, $1, Some $5) }
;

list1_recfun_sep_and:
| recfun                           { [ $1 ] }
| recfun WITH list1_recfun_sep_and { $1 :: $3 }
;

recfun:
1014
| lident_rich labels list1_type_v_binder opt_cast opt_variant EQUAL triple
1015
1016
1017
1018
   { add_lab $1 $2, $3, $5, cast_body $4 $7 }
;

expr:
1019
| expr_arg %prec prec_simple
1020
1021
1022
1023
1024
   { $1 }
| expr EQUAL expr
   { mk_infix $1 "=" $3 }
| expr LTGT expr
   { let t = mk_infix $1 "=" $3 in
1025
     mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = floc () } [t]) }
1026
| expr LARROW expr
1027
    { match $1.expr_desc with
1028
1029
1030
        | Eapply (e11, e12) -> begin match e11.expr_desc with
            | Eident x ->
                mk_expr (Eassign (e12, x, $3))
1031
            | Eapply ({ expr_desc = Eident (Qident x) }, e11)
Andrei Paskevich's avatar
Andrei Paskevich committed
1032
            when x.id = mixfix "[]" ->
1033
1034
1035
1036
1037
1038
                mk_mixfix3 "[]<-" e11 e12 $3
            | _ ->
                raise Parsing.Parse_error
          end
        | _ ->
            raise Parsing.Parse_error
1039
    }
1040
1041
1042
1043
1044
1045
1046
1047
| expr OP1 expr
   { mk_infix $1 $2 $3 }
| expr OP2 expr
   { mk_infix $1 $2 $3 }
| expr OP3 expr
   { mk_infix $1 $2 $3 }
| expr OP4 expr
   { mk_infix $1 $2 $3 }
1048
| NOT expr %prec prec_prefix_op
1049
   { mk_expr (mk_apply_id { id = "notb"; id_lab = []; id_loc = floc () } [$2]) }
1050
| prefix_op expr %prec prec_prefix_op
1051
   { mk_prefix $1 $2 }
1052
| expr_arg list1_expr_arg %prec prec_app
1053
1054
1055
1056
   { mk_expr (mk_apply $1 $2) }
| IF expr THEN expr ELSE expr
   { mk_expr (Eif ($2, $4, $6)) }
| IF expr THEN expr %prec prec_no_else
1057
   { mk_expr (Eif ($2, $4, mk_expr (Etuple []))) }
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
| expr SEMICOLON expr
   { mk_expr (Esequence ($1, $3)) }
| assertion_kind annotation
   { mk_expr (Eassert ($1, $2)) }
| expr AMPAMP expr
   { mk_expr (Elazy (LazyAnd, $1, $3)) }
| expr BARBAR expr
   { mk_expr (Elazy (LazyOr, $1, $3)) }
| LET pattern EQUAL expr IN expr
   { match $2.pat_desc with
       | PPpvar id -> mk_expr (Elet (id, $4, $6))
       | _ -> mk_expr (Ematch ($4, [$2, $6])) }
| LET lident labels list1_type_v_binder EQUAL triple IN expr
   { mk_expr (Elet (add_lab $2 $3, mk_expr_i 6 (Efun ($4, $6)), $8)) }
| LET REC list1_recfun_sep_and IN expr
   { mk_expr (Eletrec ($3, $5)) }
| FUN list1_type_v_binder ARROW triple
   { mk_expr (Efun ($2, $4)) }
| MATCH expr WITH bar_ program_match_cases END
   { mk_expr (Ematch ($2, $5)) }
| MATCH expr COMMA list1_expr_sep_comma WITH bar_ program_match_cases END
   { mk_expr (Ematch (mk_expr (Etuple ($2::$4)), $7)) }
1080
| LABEL uident COLON expr %prec prec_label
1081
   { mk_expr (Elabel ($2, $4)) }
1082
| LOOP loop_annotation expr END
1083
   { mk_expr (Eloop ($2, $3)) }
1084
1085
1086
| WHILE expr DO loop_annotation expr DONE
   { mk_expr
       (Etry
1087
1088
1089
1090
1091
          (mk_expr
             (Eloop ($4,
                     mk_expr (Eif ($2, $5,
                                   mk_expr (Eraise (exit_exn (), None)))))),
           [exit_exn (), None, mk_expr (Etuple [])])) }
1092
1093
1094
1095
1096
1097