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 34 KB
Newer Older
1
2
/**************************************************************************/
/*                                                                        */
MARCHE Claude's avatar
MARCHE Claude committed
3
/*  Copyright (C) 2010-2012                                               */
4
5
6
/*    François Bobot                                                      */
/*    Jean-Christophe Filliâtre                                           */
/*    Claude Marché                                                       */
MARCHE Claude's avatar
MARCHE Claude committed
7
/*    Guillaume Melquiond                                                 */
Jean-Christophe Filliâtre's avatar
headers    
Jean-Christophe Filliâtre committed
8
/*    Andrei Paskevich                                                    */
9
10
11
12
13
14
15
16
17
18
19
/*                                                                        */
/*  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
20
21

%{
22
module Incremental = struct
23
24
25
26
27
28
29
  let stack = Stack.create ()
  let open_file inc = Stack.push inc stack
  let close_file () = ignore (Stack.pop stack)
  let open_theory id = (Stack.top stack).Ptree.open_theory id
  let close_theory () = (Stack.top stack).Ptree.close_theory ()
  let open_module id = (Stack.top stack).Ptree.open_module id
  let close_module () = (Stack.top stack).Ptree.close_module ()
30
31
  let open_namespace n = (Stack.top stack).Ptree.open_namespace n
  let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
32
33
34
35
  let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
  let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
  let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
  let use_module loc use = (Stack.top stack).Ptree.use_module loc use
36
end
37

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38
39
40
  open Ptree

  let loc () = (symbol_start_pos (), symbol_end_pos ())
41
42
  let floc () = Loc.extract (loc ())

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
43
  let loc_i i = (rhs_start_pos i, rhs_end_pos i)
44
  let floc_i i = Loc.extract (loc_i i)
45
(* dead code
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
46
  let loc_ij i j = (rhs_start_pos i, rhs_end_pos j)
47
  let floc_ij i j = Loc.extract (loc_ij i j)
48
*)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
49
50

  let mk_ppl loc d = { pp_loc = loc; pp_desc = d }
51
  let mk_pp d = mk_ppl (floc ()) d
52
(* dead code
53
  let mk_pp_i i d = mk_ppl (floc_i i) d
54
*)
55
  let mk_pat p = { pat_loc = floc (); pat_desc = p }
Andrei Paskevich's avatar
Andrei Paskevich committed
56

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

60
  let prefix_ppl loc p a = mk_ppl loc (PPunop (p, a))
61
  let prefix_pp p a = prefix_ppl (floc ()) p a
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
62

63
  let infix  s = "infix "  ^ s
64
  let prefix s = "prefix " ^ s
Andrei Paskevich's avatar
Andrei Paskevich committed
65
  let mixfix s = "mixfix " ^ s
66

67
68
  let quote id = { id with id = "'" ^ id.id }

69
70
71
72
  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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
  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]))

89
90
91
92
93
  let () = Exn_printer.register
    (fun fmt exn -> match exn with
      | Parsing.Parse_error -> Format.fprintf fmt "syntax error"
      | _ -> raise exn
    )
94

95
96
  let mk_expr d = { expr_loc = floc (); expr_desc = d }
  let mk_expr_i i d = { expr_loc = floc_i i; expr_desc = d }
97
98
99
100
101
102
103

  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
    | [] ->
104
        assert false
105
    | [a] ->
106
        Eapply (f, a)
107
    | a :: l ->
108
109
        let loc = Loc.join f.expr_loc a.expr_loc in
        mk_apply { expr_loc = loc; expr_desc = Eapply (f, a) } l
110
111
112
113
114
115
116

  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
117
118
  let mk_mixfix2 op e1 e2 =
    let id = mk_id (mixfix op) (floc_i 2) in
119
120
    mk_expr (mk_apply_id id [e1; e2])

Andrei Paskevich's avatar
Andrei Paskevich committed
121
122
  let mk_mixfix3 op e1 e2 e3 =
    let id = mk_id (mixfix op) (floc_i 2) in
123
124
    mk_expr (mk_apply_id id [e1; e2; e3])

125
  let mk_infix e1 op e2 =
Andrei Paskevich's avatar
Andrei Paskevich committed
126
    let id = mk_id (infix op) (floc_i 2) in
127
128
129
    mk_expr (mk_apply_id id [e1; e2])

  let mk_prefix op e1 =
Andrei Paskevich's avatar
Andrei Paskevich committed
130
    let id = mk_id (prefix op) (floc_i 1) in
131
132
    mk_expr (mk_apply_id id [e1])

Andrei Paskevich's avatar
Andrei Paskevich committed
133
134
  let exit_exn () = Qident (mk_id "%Exit" (floc ()))
  let id_anonymous () = mk_id "_" (floc ())
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135
  let ty_unit () = PPTtuple []
136

137
(* dead code
Andrei Paskevich's avatar
Andrei Paskevich committed
138
  let id_lt_nat () = Qident (mk_id "lt_nat" (floc ()))
139
*)
140
141
142

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

143
144
145
146
147
148
149
  let effect_union e1 e2 =
    let { pe_reads = r1; pe_writes = w1; pe_raises = x1 } = e1 in
    let { pe_reads = r2; pe_writes = w2; pe_raises = x2 } = e2 in
    { pe_reads = r1 @ r2; pe_writes = w1 @ w2; pe_raises = x1 @ x2 }

  let effect_exprs ghost l = List.map (fun x -> (ghost, x)) l

150
151
152
153
154
  let type_c p ty ef q =
    { pc_result_type = ty;
      pc_effect      = ef;
      pc_pre         = p;
      pc_post        = q; }
155

156
(* dead code
157
  let add_init_mark e =
158
    let init = { id = "Init"; id_lab = []; id_loc = e.expr_loc } in
159
    { e with expr_desc = Emark (init, e) }
160
*)
161

162
163
164
165
166
167
168
169
170
  let small_integer i =
    try
      match i with
      | Term.IConstDecimal s -> int_of_string s
      | Term.IConstHexa    s -> int_of_string ("0x"^s)
      | Term.IConstOctal   s -> int_of_string ("0o"^s)
      | Term.IConstBinary  s -> int_of_string ("0b"^s)
    with Failure _ -> raise Parsing.Parse_error

171
172
173
  let qualid_last = function
    | Qident x | Qdot (_, x) -> x.id

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
174
175
%}

176
/* Tokens */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177

178
%token <string> LIDENT UIDENT
179
%token <Ptree.integer_constant> INTEGER
180
%token <string> OP1 OP2 OP3 OP4 OPPREF
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
181
182
%token <Ptree.real_constant> FLOAT
%token <string> STRING
183
%token <Loc.position> POSITION
184
185
186

/* keywords */

187
%token AS AXIOM CLONE COINDUCTIVE CONSTANT
Andrei Paskevich's avatar
Andrei Paskevich committed
188
189
190
%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
%token GOAL IF IMPORT IN INDUCTIVE LEMMA
%token LET MATCH META NAMESPACE NOT PROP PREDICATE
Andrei Paskevich's avatar
Andrei Paskevich committed
191
%token THEN THEORY TRUE TYPE USE WITH
192

193
194
/* program keywords */

195
196
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK DO DONE DOWNTO
%token EXCEPTION FOR
197
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE PRIVATE RAISE
Andrei Paskevich's avatar
Andrei Paskevich committed
198
%token RAISES READS REC TO TRY VAL VARIANT WHILE WRITES
199

200
201
/* symbols */

Andrei Paskevich's avatar
Andrei Paskevich committed
202
%token AND ARROW
203
%token BAR
204
%token COLON COMMA
205
%token DOT EQUAL FUNC LAMBDA LTGT
206
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTREC LEFTSQ
207
%token LARROW LRARROW
Andrei Paskevich's avatar
Andrei Paskevich committed
208
%token OR PRED QUOTE
209
%token RIGHTPAR RIGHTREC RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
210
%token UNDERSCORE
211
212
213

%token EOF

214
215
/* program symbols */

216
%token AMPAMP BARBAR LEFTBRC RIGHTBRC SEMICOLON
217

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
218
219
/* Precedences */

220
%nonassoc prec_mark
221
222
223
224
225
226
227
228
229
%nonassoc prec_post
%nonassoc BAR

%nonassoc prec_triple
%nonassoc prec_simple

%nonassoc IN
%right SEMICOLON
%nonassoc prec_no_else
230
%nonassoc DOT ELSE GHOST
231
%nonassoc prec_named
232
%nonassoc COLON
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
233

Andrei Paskevich's avatar
Andrei Paskevich committed
234
%right ARROW LRARROW
235
236
%right OR BARBAR
%right AND AMPAMP
Andrei Paskevich's avatar
Andrei Paskevich committed
237
%nonassoc NOT
238
%left EQUAL LTGT OP1
239
240
%nonassoc LARROW
%nonassoc RIGHTSQ    /* stronger than <- for e1[e2 <- e3] */
241
%left OP2
242
%left OP3
243
%left OP4
244
%nonassoc prec_prefix_op
245
%left prec_app
246
247
%nonassoc LEFTSQ
%nonassoc OPPREF
248

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
249
250
/* Entry points */

251
252
253
%type <Ptree.incremental -> unit> open_file
%start open_file
%type <unit> logic_file
Andrei Paskevich's avatar
Andrei Paskevich committed
254
%start logic_file
255
%type <unit> program_file
256
%start program_file
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
257
258
%%

259
260
open_file:
| /* epsilon */  { Incremental.open_file }
261
262
;

Andrei Paskevich's avatar
Andrei Paskevich committed
263
logic_file:
264
| list0_theory EOF  { Incremental.close_file () }
265
266
267
;

/* File, theory, namespace */
268

269
270
271
list0_theory:
| /* epsilon */         { () }
| theory list0_theory   { () }
272
273
;

274
theory_head:
275
| THEORY uident labels  { Incremental.open_theory (add_lab $2 $3) }
276
277
;

278
theory:
279
| theory_head list0_decl END  { Incremental.close_theory () }
280
281
;

282
list0_decl:
283
284
285
286
287
288
| /* epsilon */        { () }
| new_decl list0_decl  { () }
;

new_decl:
| decl
289
   { Incremental.new_decl (floc ()) $1 }
290
| use_clone
291
   { Incremental.use_clone (floc ()) $1 }
292
293
| namespace_head list0_decl END
   { Incremental.close_namespace (floc_i 1) $1 }
294
295
;

296
namespace_head:
297
298
| NAMESPACE namespace_import uident
   { Incremental.open_namespace $3.id; $2 }
299
300
301
302
303
304
305
306
307
;

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

/* Declaration */

308
decl:
309
310
| TYPE list1_type_decl
    { TypeDecl $2 }
311
312
| CONSTANT logic_decl_constant
    { LogicDecl [$2] }
Andrei Paskevich's avatar
Andrei Paskevich committed
313
314
315
| FUNCTION list1_logic_decl_function
    { LogicDecl $2 }
| PREDICATE list1_logic_decl_predicate
316
    { LogicDecl $2 }
317
318
| inductive list1_inductive_decl
    { IndDecl ($1, $2) }
319
| AXIOM ident labels COLON lexpr
320
    { PropDecl (Kaxiom, add_lab $2 $3, $5) }
321
| LEMMA ident labels COLON lexpr
322
    { PropDecl (Klemma, add_lab $2 $3, $5) }
323
| GOAL ident labels COLON lexpr
324
    { PropDecl (Kgoal, add_lab $2 $3, $5) }
325
| META sident list1_meta_arg_sep_comma
326
    { Meta ($2, $3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
327
328
;

329
330
331
332
333
inductive:
| INDUCTIVE   { Decl.Ind }
| COINDUCTIVE { Decl.Coind }
;

334
335
/* Use and clone */

336
337
use_clone:
| USE use
338
    { ($2, None) }
339
| CLONE use clone_subst
340
    { ($2, Some $3) }
341
342
;

343
344
use:
| imp_exp tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
345
    { { use_theory = $2; use_as = qualid_last $2; use_imp_exp = $1 } }
346
| imp_exp tqualid AS uident
Andrei Paskevich's avatar
Andrei Paskevich committed
347
    { { use_theory = $2; use_as = $4.id; use_imp_exp = $1 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
348
349
;

350
imp_exp:
351
352
353
| IMPORT        { Some true }
| EXPORT        { None }
| /* epsilon */ { Some false }
354
355
356
357
358
359
360
361
362
363
364
365
366
;

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

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

subst:
367
368
369
370
371
372
373
| NAMESPACE ns     EQUAL ns     { CSns   (floc (), $2, $4) }
| TYPE      qualid EQUAL qualid { CStsym (floc (), $2, $4) }
| CONSTANT  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| FUNCTION  qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
| LEMMA     qualid              { CSlemma (floc (), $2) }
| GOAL      qualid              { CSgoal  (floc (), $2) }
374
375
;

376
377
378
379
380
ns:
| uqualid { Some $1 }
| DOT     { None }
;

381
382
383
384
385
386
387
388
/* Meta args */

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

meta_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
389
| TYPE      qualid { PMAts  $2 }
390
391
| FUNCTION  qualid { PMAfs  $2 }
| PREDICATE qualid { PMAps  $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
392
393
| PROP      qualid { PMApr  $2 }
| STRING           { PMAstr $1 }
394
| INTEGER          { PMAint (small_integer $1) }
395
396
;

397
398
399
/* Type declarations */

list1_type_decl:
400
401
| type_decl                       { [$1] }
| type_decl WITH list1_type_decl  { $1 :: $3 }
402
403
404
;

type_decl:
405
| lident labels type_args typedefn
406
  { let model, vis, def, inv = $4 in
407
    let vis = if model then Abstract else vis in
408
    { td_loc = floc (); td_ident = add_lab $1 $2;
409
410
      td_params = $3; td_model = model;
      td_vis = vis; td_def = def; td_inv = inv } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
411
412
;

413
type_args:
414
415
| /* epsilon */             { [] }
| type_var labels type_args { add_lab $1 $2 :: $3 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
416
417
418
;

typedefn:
419
420
421
422
423
424
425
426
| /* epsilon */
    { false, Public, TDabstract, None }
| equal_model visibility typecases invariant
    { $1, $2, TDalgebraic $3, $4 }
| equal_model visibility BAR typecases invariant
    { $1, $2, TDalgebraic $4, $5 }
| equal_model visibility record_type invariant
    { $1, $2, TDrecord $3, $4 }
427
428
429
/* abstract/private is not allowed for alias type */
| equal_model visibility primitive_type
    { if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
430
      $1, Public, TDalias $3, None }
431
432
433
434
435
436
;

visibility:
| /* epsilon */ { Public }
| PRIVATE       { Private }
| ABSTRACT      { Abstract }
437
438
439
440
441
;

equal_model:
| EQUAL { false }
| MODEL { true }
442
443
444
;

record_type:
Andrei Paskevich's avatar
Andrei Paskevich committed
445
| LEFTREC list1_record_field opt_semicolon RIGHTREC { List.rev $2 }
446
447
448
449
;

list1_record_field:
| record_field                              { [$1] }
450
| list1_record_field SEMICOLON record_field { $3 :: $1 }
451
452
;

453
454
455
456
457
458
459
460
field_modifiers:
| /* epsilon */ { false, false }
| MUTABLE       { true,  false }
| GHOST         { false, true  }
| GHOST MUTABLE { true,  true  }
| MUTABLE GHOST { true,  true  }
;

461
record_field:
462
463
464
465
466
467
| field_modifiers lident labels COLON primitive_type
   { { f_loc = floc ();
       f_ident = add_lab $2 $3;
       f_mutable = fst $1;
       f_ghost = snd $1;
       f_pty = $5 } }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
468
469
470
471
472
473
474
475
;

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

typecase:
476
| uident labels params   { (floc (), add_lab $1 $2, $3) }
477
478
479
480
;

/* Logic declarations */

Andrei Paskevich's avatar
Andrei Paskevich committed
481
482
483
484
485
486
487
488
489
490
list1_logic_decl_function:
| logic_decl_function                        { [$1] }
| logic_decl_function WITH list1_logic_decl  { $1 :: $3 }
;

list1_logic_decl_predicate:
| logic_decl_predicate                        { [$1] }
| logic_decl_predicate WITH list1_logic_decl  { $1 :: $3 }
;

491
list1_logic_decl:
492
493
| logic_decl                        { [$1] }
| logic_decl WITH list1_logic_decl  { $1 :: $3 }
494
495
;

496
497
498
499
500
501
logic_decl_constant:
| lident_rich labels COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = []; ld_type = Some $4; ld_def = $5 } }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
502
503
504
505
506
507
508
509
510
511
512
513
logic_decl_function:
| lident_rich labels params COLON primitive_type logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = Some $5; ld_def = $6 } }
;

logic_decl_predicate:
| lident_rich labels params logic_def_option
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
      ld_params = $3; ld_type = None; ld_def = $4 } }
;

514
logic_decl:
515
| lident_rich labels params logic_type_option logic_def_option
516
  { { ld_loc = floc (); ld_ident = add_lab $1 $2;
517
      ld_params = $3; ld_type = $4; ld_def = $5 } }
518
519
520
521
522
523
524
525
526
527
;

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
528
529
;

530
531
532
/* Inductive declarations */

list1_inductive_decl:
533
534
| inductive_decl                            { [$1] }
| inductive_decl WITH list1_inductive_decl  { $1 :: $3 }
535
536
537
;

inductive_decl:
538
| lident_rich labels params inddefn
539
  { { in_loc = floc (); in_ident = add_lab $1 $2;
540
      in_params = $3; in_def = $4 } }
Andrei Paskevich's avatar
Andrei Paskevich committed
541
;
542

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
543
544
545
546
547
548
549
550
551
552
553
inddefn:
| /* epsilon */       { [] }
| EQUAL bar_ indcases { $3 }
;

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

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

557
558
559
560
561
562
563
564
/* 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
565
566
| primitive_type_arg_non_lident           { $1 }
| uqualid DOT lident primitive_type_args  { PPTtyapp ($4, Qdot ($1, $3)) }
567
568
569
570
571
572
573
574
;

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
575
| lident                         { PPTtyapp ([], Qident $1) }
576
577
578
579
| primitive_type_arg_non_lident  { $1 }
;

primitive_type_arg_non_lident:
Andrei Paskevich's avatar
Andrei Paskevich committed
580
581
| uqualid DOT lident
   { PPTtyapp ([], Qdot ($1, $3)) }
582
583
584
585
| type_var
   { PPTtyvar $1 }
| LEFTPAR primitive_type COMMA list1_primitive_type_sep_comma RIGHTPAR
   { PPTtuple ($2 :: $4) }
586
587
588
589
590
591
| LEFTPAR RIGHTPAR
   { PPTtuple [] }
| LEFTPAR primitive_type RIGHTPAR
   { $2 }
;

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
592
593
594
595
596
list1_primitive_type_sep_comma:
| primitive_type                                      { [$1] }
| primitive_type COMMA list1_primitive_type_sep_comma { $1 :: $3 }
;

597
type_var:
598
| QUOTE lident { $2 }
599
600
;

601
602
/* Logic expressions */

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
603
lexpr:
604
| lexpr ARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
605
   { infix_pp $1 PPimplies $3 }
606
| lexpr LRARROW lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
607
   { infix_pp $1 PPiff $3 }
608
| lexpr OR lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
609
   { infix_pp $1 PPor $3 }
610
| lexpr BARBAR lexpr
611
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPor $3 }
612
| lexpr AND lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
613
   { infix_pp $1 PPand $3 }
614
| lexpr AMPAMP lexpr
615
   { infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPand $3 }
616
| NOT lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
617
   { prefix_pp PPnot $2 }
618
| lexpr EQUAL lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
619
   { mk_l_infix $1 "=" $3 }
620
| lexpr LTGT lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
621
   { prefix_pp PPnot (mk_l_infix $1 "=" $3) }
622
| lexpr OP1 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
623
   { mk_l_infix $1 $2 $3 }
624
| lexpr OP2 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
625
   { mk_l_infix $1 $2 $3 }
626
| lexpr OP3 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
627
   { mk_l_infix $1 $2 $3 }
628
| lexpr OP4 lexpr
Andrei Paskevich's avatar
Andrei Paskevich committed
629
   { mk_l_infix $1 $2 $3 }
630
| prefix_op lexpr %prec prec_prefix_op
Andrei Paskevich's avatar
Andrei Paskevich committed
631
   { mk_l_prefix $1 $2 }
632
633
| qualid list1_lexpr_arg
   { mk_pp (PPapp ($1, $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
634
| IF lexpr THEN lexpr ELSE lexpr
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
635
   { mk_pp (PPif ($2, $4, $6)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
636
637
| quant list1_param_var_sep_comma triggers DOT lexpr
   { mk_pp (PPquant ($1, $2, $3, $5)) }
638
639
| label lexpr %prec prec_named
   { mk_pp (PPnamed ($1, $2)) }
640
| LET pattern EQUAL lexpr IN lexpr
641
642
   { match $2.pat_desc with
       | PPpvar id -> mk_pp (PPlet (id, $4, $6))
Andrei Paskevich's avatar
Andrei Paskevich committed
643
644
       | _ -> mk_pp (PPmatch ($4, [$2, $6])) }
| MATCH lexpr WITH bar_ match_cases END
645
   { mk_pp (PPmatch ($2, $5)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
646
647
| MATCH lexpr COMMA list1_lexpr_sep_comma WITH bar_ match_cases END
   { mk_pp (PPmatch (mk_pp (PPtuple ($2::$4)), $7)) }
648
649
| EPSILON lident labels COLON primitive_type DOT lexpr
   { mk_pp (PPeps (add_lab $2 $3, $5, $7)) }
650
| lexpr COLON primitive_type
651
   { mk_pp (PPcast ($1, $3)) }
652
| lexpr_arg
653
654
655
   { $1 }
;

656
657
658
659
660
661
662
663
664
list1_field_value:
| field_value                             { [$1] }
| list1_field_value SEMICOLON field_value { $3 :: $1 }
;

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

665
666
667
list1_lexpr_arg:
| lexpr_arg                 { [$1] }
| lexpr_arg list1_lexpr_arg { $1::$2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
668
;
669

670
constant:
Andrei Paskevich's avatar
Andrei Paskevich committed
671
672
| INTEGER   { Term.ConstInt $1 }
| FLOAT     { Term.ConstReal $1 }
673
674
;

675
lexpr_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
676
677
678
679
680
681
| 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 }
682
| QUOTE uident      { mk_pp (PPvar (Qident (quote $2))) }
Andrei Paskevich's avatar
Andrei Paskevich committed
683
684
685
;

lexpr_dot:
Andrei Paskevich's avatar
Andrei Paskevich committed
686
687
688
| lqualid_copy      { mk_pp (PPvar $1) }
| OPPREF lexpr_dot  { mk_l_prefix $1 $2 }
| lexpr_sub         { $1 }
Andrei Paskevich's avatar
Andrei Paskevich committed
689
690
691
;

lexpr_sub:
692
| lexpr_dot DOT lqualid_rich
Andrei Paskevich's avatar
Andrei Paskevich committed
693
   { mk_pp (PPapp ($3, [$1])) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
694
695
| LEFTPAR lexpr RIGHTPAR
   { $2 }
696
697
698
699
| LEFTPAR RIGHTPAR
   { mk_pp (PPtuple []) }
| LEFTPAR lexpr COMMA list1_lexpr_sep_comma RIGHTPAR
   { mk_pp (PPtuple ($2 :: $4)) }
700
701
| LEFTREC list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPrecord (List.rev $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
702
703
| LEFTREC lexpr_arg WITH list1_field_value opt_semicolon RIGHTREC
   { mk_pp (PPupdate ($2, List.rev $4)) }
704
| lexpr_arg LEFTSQ lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
705
   { mk_l_mixfix2 "[]" $1 $3 }
706
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
Andrei Paskevich's avatar
Andrei Paskevich committed
707
   { mk_l_mixfix3 "[<-]" $1 $3 $5 }
Andrei Paskevich's avatar
Andrei Paskevich committed
708
;
709

Andrei Paskevich's avatar
Andrei Paskevich committed
710
711
712
713
quant:
| FORALL  { PPforall }
| EXISTS  { PPexists }
| LAMBDA  { PPlambda }
714
715
| FUNC    { PPfunc }
| PRED    { PPpred }
Andrei Paskevich's avatar
Andrei Paskevich committed
716
717
;

718
/* Triggers */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
719

720
721
722
723
triggers:
| /* epsilon */                         { [] }
| LEFTSQ list1_trigger_sep_bar RIGHTSQ  { $2 }
;
724

725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
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 */
740

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
741
742
743
744
745
746
match_cases:
| match_case                  { [$1] }
| match_case BAR match_cases  { $1::$3 }
;

match_case:
Andrei Paskevich's avatar
Andrei Paskevich committed
747
| pattern ARROW lexpr   { ($1,$3) }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
748
749
750
;

pattern:
Andrei Paskevich's avatar
Andrei Paskevich committed
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
| 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:
766
767
768
| 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
769
;
770

771
list1_pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
772
773
774
| pat_arg                { [$1] }
| pat_arg list1_pat_arg  { $1::$2 }
;
775

776
pat_arg:
Andrei Paskevich's avatar
Andrei Paskevich committed
777
| UNDERSCORE                { mk_pat (PPpwild) }
778
| lident labels             { mk_pat (PPpvar (add_lab $1 $2)) }
Andrei Paskevich's avatar
Andrei Paskevich committed
779
780
781
| uqualid                   { mk_pat (PPpapp ($1, [])) }
| LEFTPAR RIGHTPAR          { mk_pat (PPptuple []) }
| LEFTPAR pattern RIGHTPAR  { $2 }
Andrei Paskevich's avatar
Andrei Paskevich committed
782
783
784
785
786
787
788
789
790
791
| 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
792
793
;

794
/* Parameters */
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
795

796
797
798
params:
| /* epsilon */   { [] }
| param params    { $1 @ $2 }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
799
800
;

801
802
803
804
805
806
807
808
809
810
811
812
813
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
814
815
;

816
817
818
819
820
821
822
823
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
824
825
;

826
827
828
829
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
830
831
;

832
833
834
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
835
836
;

837
838
839
param_var:
| list1_lident COLON primitive_type
   { List.map (fun id -> (Some id, $3)) $1 }
840
841
842
843
844
845
| 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
846
847
;

848
list1_lident:
849
850
| lident               { [$1] }
| lident list1_lident  { $1 :: $2 }
851
852
;

853
854
855
856
857
list0_lident_labels:
| /* epsilon */                      { [] }
| lident labels list0_lident_labels  { add_lab $1 $2 :: $3 }
;

858
859
860
861
862
/* Idents */

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

Andrei Paskevich's avatar
Andrei Paskevich committed
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
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 */

880
881
882
ident_rich:
| uident      { $1 }
| lident_rich { $1 }
883
884
;

885
lident_rich:
Andrei Paskevich's avatar
Andrei Paskevich committed
886
887
888
| 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
889
890
;

891
lident_op:
Andrei Paskevich's avatar
Andrei Paskevich committed
892
893
894
895
896
897
| prefix_op             { infix $1 }
| prefix_op UNDERSCORE  { prefix $1 }
| EQUAL                 { infix "=" }
| OPPREF                { prefix $1 }
| LEFTSQ RIGHTSQ        { mixfix "[]" }
| LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
898
899
;

900
prefix_op:
901
902
903
904
905
906
| OP1   { $1 }
| OP2   { $1 }
| OP3   { $1 }
| OP4   { $1 }
;

Andrei Paskevich's avatar
Andrei Paskevich committed
907
/* Qualified idents */
908

Andrei Paskevich's avatar
Andrei Paskevich committed
909
910
911
qualid:
| ident_rich              { Qident $1 }
| uqualid DOT ident_rich  { Qdot ($1, $3) }
912
913
;

Andrei Paskevich's avatar
Andrei Paskevich committed
914
915
916
lqualid_rich:
| lident_rich             { Qident $1 }
| uqualid DOT lident_rich { Qdot ($1, $3) }
917
918
919
;

lqualid:
Andrei Paskevich's avatar
Andrei Paskevich committed
920
921
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
922
923
;

Andrei Paskevich's avatar
Andrei Paskevich committed
924
925
926
927
/* copy of lqualid to avoid yacc conflicts */
lqualid_copy:
| lident              { Qident $1 }
| uqualid DOT lident  { Qdot ($1, $3) }
928
929
;

Andrei Paskevich's avatar
Andrei Paskevich committed
930
931
932
uqualid:
| uident              { Qident $1 }
| uqualid DOT uident  { Qdot ($1, $3) }
933
934
;

Andrei Paskevich's avatar
Andrei Paskevich committed
935
936
/* Theory/Module names */

937
938
939
tqualid:
| uident                { Qident $1 }
| any_qualid DOT uident { Qdot ($1, $3) }
Andrei Paskevich's avatar
Andrei Paskevich committed
940
;
941

Andrei Paskevich's avatar
Andrei Paskevich committed
942
any_qualid:
943
944
945
946
947
948
949
| sident                { Qident $1 }
| any_qualid DOT sident { Qdot ($1, $3) }
;

sident:
| ident   { $1 }
| STRING  { mk_id $1 (floc ()) }
Andrei Paskevich's avatar
Andrei Paskevich committed
950
;
951
952
953

/* Misc */

954
label:
Andrei Paskevich's avatar
Andrei Paskevich committed
955
| STRING    { Lstr (Ident.create_label $1) }
Andrei Paskevich's avatar
Andrei Paskevich committed
956
| POSITION  { Lpos $1 }
957
958
;

959
960
961
962
963
labels:
| /* epsilon */ { [] }
| label labels  { $1 :: $2 }
;

964
965
966
bar_:
| /* epsilon */ { () }
| BAR           { () }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
967
968
;

969
970
971
/****************************************************************************/

program_file:
972
| list0_theory_or_module EOF { Incremental.close_file () }
973
974
;

975
976
977
978
list0_theory_or_module:
| /* epsilon */                   { () }
| theory list0_theory_or_module   { () }
| module_ list0_theory_or_module  { () }
979
980
;

981
982
module_head:
| MODULE uident labels  { Incremental.open_module (add_lab $2 $3) }
983
984
;

985
986
module_:
| module_head list0_pdecl END  { Incremental.close_module () }
987
988
;

989
990
991
992
list0_pdecl:
| /* epsilon */         { () }
| new_decl  list0_pdecl { () }
| new_pdecl list0_pdecl { () }
993
994
;

995
996
997
998
999
new_pdecl:
| pdecl
    { Incremental.new_pdecl (floc ()) $1 }
| USE use_module
    { Incremental.use_module (floc ()) $2 }
1000
1001
;

1002
1003
use_module:
| imp_exp MODULE tqualid
Andrei Paskevich's avatar
Andrei Paskevich committed
1004
    { { use_theory = $3; use_as = qualid_last $3; use_imp_exp = $1 } }
1005
| imp_exp MODULE tqualid AS uident
Andrei Paskevich's avatar
Andrei Paskevich committed
1006
    { { use_theory = $3; use_as = $5.id; use_imp_exp = $1 } }
1007
1008
;

1009
pdecl:
1010
1011
1012
1013
| LET ghost lident_rich_pgm labels list1_type_v_binder opt_cast EQUAL triple
    { Dlet (add_lab $3 $4, $2, mk_expr_i 8 (Efun ($5, cast_body $6 $8))) }
| LET ghost lident_rich_pgm labels EQUAL FUN list1_type_v_binder ARROW triple
    { Dlet (add_lab $3 $4, $2, mk_expr_i 9 (Efun ($7, $9))) }
1014
1015
| LET REC list1_recfun_sep_and
    { Dletrec $3 }
1016
1017
1018
1019
| VAL ghost lident_rich_pgm labels COLON type_v
    { Dparam (add_lab $3 $4, $2, $6) }
| VAL ghost lident_rich_pgm labels list1_type_v_param COLON type_c
    { Dparam (add_lab $3 $4, $2, Tarrow ($5, $7)) }
1020
1021
| EXCEPTION uident labels
    { Dexn (add_lab $2 $3, None) }
1022
| EXCEPTION uident labels primitive_type
1023
    { Dexn (add_lab $2 $3, Some $4) }
1024
1025
;