Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / cocospec / kindLustreParser.mly @ bc504848

History | View | Annotate | Download (34.1 KB)

1
(* This file is part of the Kind 2 model checker.
2

    
3
   Copyright (c) 2015 by the Board of Trustees of the University of Iowa
4

    
5
   Licensed under the Apache License, Version 2.0 (the "License"); you
6
   may not use this file except in compliance with the License.  You
7
   may obtain a copy of the License at
8

    
9
   http://www.apache.org/licenses/LICENSE-2.0 
10

    
11
   Unless required by applicable law or agreed to in writing, software
12
   distributed under the License is distributed on an "AS IS" BASIS,
13
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
14
   implied. See the License for the specific language governing
15
   permissions and limitations under the License. 
16

    
17
*)
18

    
19

    
20
%{
21
open KindLib
22

    
23
module A = KindLustreAst
24

    
25
let mk_pos = position_of_lexing 
26

    
27

    
28
let rec add_else_branch b belse =
29
  match b with
30
  | A.Target _ -> failwith "Cannot add else branch to unconditional target"
31
  | A.TransIf (p, e, b1, None) -> A.TransIf (p, e, b1, Some belse)
32
  | A.TransIf (p, e, b1, Some b2) ->
33
     A.TransIf (p, e, b1, Some (add_else_branch b2 belse))
34
     
35
           
36
let merge_branches transitions =
37
  List.fold_right (fun (p, b) acc ->
38
      match acc, b with
39
      | None, _ -> Some (p, b)
40
      | Some (_, b2), b1 -> Some (p, add_else_branch b1 b2)
41
    ) transitions None
42
  
43
%}
44

    
45
(* Special characters *)
46
%token SEMICOLON 
47
%token EQUALS 
48
%token COLON 
49
%token COMMA 
50
%token LSQBRACKET 
51
%token RSQBRACKET 
52
%token LPAREN 
53
%token RPAREN 
54
%token DOTPERCENT
55

    
56
(* Tokens for enumerated types *)
57
%token ENUM
58

    
59
(* Tokens for records *)
60
%token STRUCT
61
%token DOT
62
%token LCURLYBRACKET 
63
%token RCURLYBRACKET 
64

    
65
(* Tokens for decimals and numerals *)
66
%token <string>DECIMAL
67
%token <string>NUMERAL
68

    
69
%token <string>STRING
70

    
71
(* Identifier token *)
72
%token <string>SYM 
73
%token <string>QUOTSYM 
74
      
75
(* Tokens for types *)
76
%token TYPE
77
%token INT
78
%token REAL
79
%token BOOL
80
%token SUBRANGE
81
%token OF
82
    
83
(* Tokens for arrays *)
84
(* %token ARRAY *)
85
%token CARET
86
%token DOTDOT
87
%token PIPE
88

    
89
(* Token for constant declarations *)
90
%token CONST
91
    
92
(* Tokens for node declarations *)
93
%token IMPORTED
94
%token NODE
95
%token LPARAMBRACKET
96
%token RPARAMBRACKET
97
%token FUNCTION
98
%token RETURNS
99
%token VAR
100
%token LET
101
%token TEL
102
    
103
(* Tokens for annotations *)
104

    
105
(* Inline annotations. *)
106
%token PERCENTANNOT
107
%token BANGANNOT
108
(* %token ATANNOT *)
109
(* Parenthesis star (PS) block annotations. *)
110
%token PSBLOCKSTART
111
%token PSATBLOCK
112
%token PSBLOCKEND
113
(* Slash star (PS) block annotations. *)
114
%token SSBLOCKSTART
115
%token SSATBLOCK
116
%token SSBLOCKEND
117
(* Generic annotations. *)
118
%token PROPERTY
119
%token MAIN
120
(* Contract annotations. *)
121
%token CONTRACT
122
%token IMPORTCONTRACT
123
(* %token IMPORTMODE *)
124
%token ASSUME
125
%token GUARANTEE
126
%token MODE
127
%token REQUIRE
128
%token ENSURE
129

    
130
(* Token for assertions *)
131
%token ASSERT
132
    
133
(* Token for check *)
134
%token CHECK
135

    
136
(* Tokens for Boolean operations *)
137
%token TRUE
138
%token FALSE
139
%token NOT
140
%token AND
141
%token XOR
142
%token OR
143
%token IF
144
%token WITH
145
%token THEN
146
%token ELSE
147
%token IMPL
148
%token HASH
149
%token FORALL
150
%token EXISTS
151
    
152
(* Tokens for relations *)
153
%token LTE
154
%token GTE
155
%token LT
156
%token GT
157
%token NEQ
158
    
159
(* Tokens for arithmetic operators *)
160
%token MINUS
161
%token PLUS
162
%token DIV
163
%token MULT
164
%token INTDIV
165
%token MOD
166
    
167
(* Tokens for clocks *)
168
%token WHEN
169
%token CURRENT
170
%token CONDACT
171
%token ACTIVATE
172
%token INITIAL
173
%token DEFAULT
174
%token EVERY
175
%token RESTART
176
%token MERGE
177

    
178
(* Tokens for automata *)
179
%token AUTOMATON
180
%token STATE
181
%token UNLESS
182
%token UNTIL
183
%token RESUME
184
%token ELSIF
185
%token END
186

    
187
(* Tokens for temporal operators *)
188
%token PRE
189
%token LAST
190
%token FBY
191
%token ARROW
192
    
193
(* Token for end of file marker *)
194
%token EOF
195
    
196
(* Priorities and associativity of operators, lowest first *)
197
%nonassoc WHEN CURRENT 
198
%left PIPE
199
%nonassoc ELSE
200
%right ARROW
201
%nonassoc prec_forall prec_exists
202
%right IMPL
203
%left OR XOR
204
%left AND
205
%left LT LTE EQUALS NEQ GTE GT
206
%left PLUS MINUS
207
%left MULT INTDIV MOD DIV
208
%nonassoc PRE 
209
%nonassoc INT REAL 
210
%nonassoc NOT 
211
%left CARET 
212
%left LSQBRACKET DOT DOTPERCENT
213

    
214
(* Start token *)
215
%start <KindLustreAst.t> main
216
%start <KindLustreAst.expr> one_expr
217
%start <KindLustreAst.contract> contract_in_block_main
218
%%
219
(** Parser for lustre systems. *)
220

    
221
one_expr: e = expr EOF { e }
222

    
223

    
224
(* A Lustre program is a list of declarations *)
225
main: p = list(decl) EOF { List.flatten p }
226

    
227
(* A declaration is a type, a constant, a node or a function declaration *)
228
decl:
229
  | d = const_decl { List.map 
230
                       (function e -> A.ConstDecl (mk_pos $startpos, e)) 
231
                       d }
232
  | d = type_decl { List.map 
233
                      (function e -> A.TypeDecl (mk_pos $startpos, e)) 
234
                      d }
235
  | NODE ; decl = node_decl ; def = node_def {
236
    let (n, p, i, o, r) = decl in
237
    let (l, e) = def in
238
    [A.NodeDecl ( mk_pos $startpos, (n, false, p, i, o, l, e, r) )]
239
  }
240
  | FUNCTION ; decl = node_decl ; def = node_def {
241
    let (n, p, i, o, r) = decl in
242
    let (l, e) = def in
243
    [A.FuncDecl (mk_pos $startpos, (n, false, p, i, o, l, e, r))]
244
  }
245
  | NODE ; IMPORTED ; decl = node_decl {
246
    let (n, p, i, o, r) = decl in
247
    [A.NodeDecl ( mk_pos $startpos, (n, true, p, i, o, [], [], r) )]
248
  }
249
  | FUNCTION ; IMPORTED ; decl = node_decl {
250
    let (n, p, i, o, r) = decl in
251
    [A.FuncDecl (mk_pos $startpos, (n, true, p, i, o, [], [], r))]
252
  }
253
  | d = contract_decl { [A.ContractNodeDecl (mk_pos $startpos, d)] }
254
  | d = node_param_inst { [A.NodeParamInst (mk_pos $startpos, d)] }
255

    
256

    
257
(* ********************************************************************** *)
258

    
259

    
260
(* A constant declaration *)
261
const_decl: CONST; l = nonempty_list(const_decl_body) { List.flatten l }
262

    
263
(* The body of a constant declaration *)
264
const_decl_body:
265

    
266
  (* Imported (free) constant 
267

    
268
     Separate rule for singleton list to avoid shift/reduce conflict *)
269
  | h = ident; COLON; t = lustre_type; SEMICOLON 
270
    { [A.FreeConst (mk_pos $startpos, h, t)] } 
271

    
272
  (* Imported (free) constant *)
273
  | h = ident; COMMA; l = ident_list; COLON; t = lustre_type; SEMICOLON 
274
    { List.map (function e -> A.FreeConst (mk_pos $startpos, e, t)) (h :: l) } 
275

    
276
  (* Defined constant without a type *)
277
  | s = ident; EQUALS; e = expr; SEMICOLON 
278
    { [A.UntypedConst (mk_pos $startpos, s, e)] }
279

    
280
  (* Defined constant with a type *)
281
  | c = typed_ident; EQUALS; e = expr; SEMICOLON 
282
    { let (_, s, t) = c in [A.TypedConst (mk_pos $startpos, s, e, t)] }
283

    
284

    
285
(* ********************************************************************** *)
286

    
287

    
288
(* A type declaration *) 
289
type_decl: 
290

    
291
  (* A free type *)
292
  | TYPE; l = ident_list; SEMICOLON 
293
     { List.map (fun e -> A.FreeType (mk_pos $startpos, e)) l }
294

    
295
  (* A type alias *)
296
  | TYPE; l = ident_list; EQUALS; t = lustre_type; SEMICOLON
297
     { List.map (fun e -> match t with 
298
                 | A.EnumType (p, _, cs) ->
299
                    A.AliasType (mk_pos $startpos, e,
300
                                 A.EnumType (p, Some e, cs))
301
                 | _ -> A.AliasType (mk_pos $startpos, e, t)) l }
302

    
303
  (* A record type, can only be defined as alias *)
304
  | TYPE; l = ident_list; EQUALS; t = record_type; SEMICOLON
305
     { List.map 
306
         (function e -> 
307
           A.AliasType (mk_pos $startpos, 
308
                        e, 
309
                        A.RecordType (mk_pos $startpos, t))) 
310
         l }
311

    
312

    
313
(* A type *)
314
lustre_type:
315

    
316
  (* Predefined types *)
317
  | BOOL { A.Bool (mk_pos $startpos) }
318
  | INT { A.Int (mk_pos $startpos)}
319
  | REAL { A.Real (mk_pos $startpos)}
320

    
321
  | SUBRANGE;
322
    LSQBRACKET;
323
    l = expr; 
324
    COMMA; 
325
    u = expr; 
326
    RSQBRACKET 
327
    OF
328
    INT 
329
    { A.IntRange (mk_pos $startpos, l, u)}
330

    
331
  (* User-defined type *)
332
  | s = ident { A.UserType (mk_pos $startpos, s) }
333

    
334
  (* Tuple type *)
335
  | t = tuple_type { A.TupleType (mk_pos $startpos, t) } 
336

    
337
(* Record types can only be defined as aliases 
338
  (* Record type (V6) *)
339
  | t = record_type { A.RecordType t } 
340
*)
341

    
342
  (* Array type (V6) *)
343
  | t = array_type { A.ArrayType (mk_pos $startpos, t) }
344

    
345
  (* Enum type (V6) *)
346
  | t = enum_type { A.EnumType (mk_pos $startpos, None, t) }
347

    
348

    
349
(* A tuple type *)
350
tuple_type:
351

    
352
  (* Tuples are between square brackets *)
353
  | LSQBRACKET; l = lustre_type_list; RSQBRACKET { l } 
354

    
355

    
356
(* A record type (V6) *)
357
record_type:
358

    
359
  (* Keyword "struct" is optional *)
360
  | option(STRUCT); 
361
    f = tlist(LCURLYBRACKET, SEMICOLON, RCURLYBRACKET, typed_idents)
362
  
363
    { List.flatten f  }
364

    
365

    
366
(* An array type (V6) *)
367
array_type: 
368
  | t = lustre_type; CARET; s = expr { t, s }
369

    
370
(*
371
  (* Alternate syntax: array [size] of type *)
372
  | ARRAY; s = expr; OF; LSQBRACKET; t = lustre_type; RSQBRACKET { t, s }
373
*)
374

    
375
(* An enum type (V6) *)
376
enum_type: ENUM LCURLYBRACKET; l = ident_list; RCURLYBRACKET { l } 
377

    
378

    
379
(* ********************************************************************** *)
380

    
381

    
382
(* A node declaration and contract. *)
383
node_decl:
384
| n = ident;
385
  p = loption(static_params);
386
  i = tlist(LPAREN, SEMICOLON, RPAREN, const_clocked_typed_idents);
387
  RETURNS;
388
  o = tlist(LPAREN, SEMICOLON, RPAREN, clocked_typed_idents);
389
  option(SEMICOLON);
390
  r = option(contract_spec)
391
  {
392
    (n, p, List.flatten i, List.flatten o, r)
393
  }
394

    
395
(* A node definition (locals + body). *)
396
node_def:
397
  l = list(node_local_decl);
398
  LET;
399
  e = list(node_item);
400
  TEL
401
  option(node_sep)
402

    
403
  { (List.flatten l, e) }
404

    
405

    
406
contract_ghost_var:
407
  | VAR ;
408
    i = ident ; COLON ; t = lustre_type; EQUALS ; e = qexpr ;
409
    SEMICOLON 
410
    { A.GhostVar (A.TypedConst (mk_pos $startpos, i, e, t)) }
411
(*  | VAR ; i = ident ; EQUALS ; e = expr ; SEMICOLON 
412
    { A.GhostVar (A.UntypedConst (mk_pos $startpos, i, e)) } *)
413

    
414
contract_ghost_const:
415
  | CONST; i = ident; COLON; t = lustre_type; EQUALS; e = qexpr; SEMICOLON 
416
    { A.GhostConst (A.TypedConst (mk_pos $startpos, i, e, t)) }
417
  | CONST; i = ident; EQUALS; e = qexpr; SEMICOLON 
418
    { A.GhostConst (A.UntypedConst (mk_pos $startpos, i, e)) }
419

    
420
contract_assume:
421
  ASSUME; name = option(STRING); e = qexpr; SEMICOLON
422
  { A.Assume (mk_pos $startpos, name, e) }
423

    
424
contract_guarantee:
425
  GUARANTEE; name = option(STRING); e = qexpr; SEMICOLON
426
  { A.Guarantee (mk_pos $startpos, name, e) }
427

    
428
contract_require:
429
  REQUIRE; name = option(STRING); e = qexpr; SEMICOLON
430
  { mk_pos $startpos, name, e }
431

    
432
contract_ensure:
433
  ENSURE; name = option(STRING); e = qexpr; SEMICOLON
434
  { mk_pos $startpos, name, e }
435

    
436
mode_equation:
437
  MODE; n = ident; LPAREN;
438
  reqs = list(contract_require);
439
  enss = list(contract_ensure);
440
  RPAREN; SEMICOLON {
441
    A.Mode (mk_pos $startpos, n, reqs, enss)
442
  }
443

    
444
contract_import:
445
  IMPORTCONTRACT ; n = ident ;
446
  LPAREN ; in_params = separated_list(COMMA, qexpr) ; RPAREN ; RETURNS ;
447
  LPAREN ; out_params = separated_list(COMMA, qexpr) ; RPAREN ; SEMICOLON ; {
448
    A.ContractCall (mk_pos $startpos, n, in_params, out_params)
449
  }
450

    
451

    
452
contract_item:
453
  | v = contract_ghost_var { (*Format.printf "CONTRACT_ITEM (v)@.";*) v } 
454
  | c = contract_ghost_const { (*Format.printf "CONTRACT_ITEM (c)@.";*) c }
455
  | a = contract_assume { (*Format.printf "CONTRACT_ITEM (a)@.";*) a }
456
  | g = contract_guarantee { (*Format.printf "CONTRACT_ITEM (g)@.";*) g }
457
  | m = mode_equation { m }
458
  | i = contract_import { i }
459

    
460
contract_in_block_main:
461
  | c = contract_in_block ; EOF { c }
462

    
463
contract_in_block:
464
  | c = nonempty_list(contract_item) { c }
465

    
466

    
467
(* A contract node declaration. *)
468
contract_decl:
469
  | CONTRACT;
470
    n = ident; 
471
    p = loption(static_params);
472
    i = tlist(LPAREN, SEMICOLON, RPAREN, const_clocked_typed_idents); 
473
    RETURNS; 
474
    o = tlist(LPAREN, SEMICOLON, RPAREN, clocked_typed_idents); 
475
    SEMICOLON;
476
    LET;
477
      e = contract_in_block;
478
    TEL
479
    option(node_sep) 
480

    
481
    { (n,
482
       p,
483
       List.flatten i,
484
       List.flatten o,
485
       e) }
486

    
487

    
488
contract_spec:
489
  (* Block contract, parenthesis star (PS). *)
490
  | PSATBLOCK ; CONTRACT ;
491
    eqs = contract_in_block
492
    PSBLOCKEND
493
    { eqs }
494
  (* Block contract, slash star (SS). *)
495
  | SSATBLOCK ; CONTRACT ;
496
    eqs = contract_in_block
497
    SSBLOCKEND
498
    { eqs }
499

    
500

    
501
(* A node declaration as an instance of a paramterized node *)
502
node_param_inst: 
503
  | NODE; 
504
    n = ident; 
505
    EQUALS;
506
    s = ident; 
507
    p = tlist 
508
         (LPARAMBRACKET, SEMICOLON, RPARAMBRACKET, node_call_static_param); 
509
    SEMICOLON
510
        
511
    { (n, s, p) } 
512

    
513

    
514
(* A node declaration is optionally terminated by a period or a semicolon *)
515
node_sep: DOT | SEMICOLON { }
516

    
517

    
518
(* A static parameter is a type *)
519
static_param:
520
  | TYPE; t = ident { A.TypeParam t }
521

    
522

    
523
(* The static parameters of a node *)
524
static_params:
525
  | l = tlist (LPARAMBRACKET, SEMICOLON, RPARAMBRACKET, static_param)
526
    
527
    { l }  
528

    
529

    
530
(* A node-local declaration of constants or variables *)
531
node_local_decl:
532
  | c = const_decl { List.map 
533
                       (function e -> A.NodeConstDecl (mk_pos $startpos, e))
534
                       c }
535
  | v = var_decls { List.map 
536
                      (function e -> A.NodeVarDecl (mk_pos $startpos, e)) 
537
                      v }
538

    
539

    
540
(* A variable declaration section of a node *)
541
var_decls: 
542
  | VAR; l = nonempty_list(var_decl) { List.flatten l }
543

    
544

    
545
(* A declaration of variables *)
546
var_decl:
547
  | l = clocked_typed_idents; SEMICOLON { l }
548

    
549

    
550
boolean:
551
  | TRUE { true }
552
  | FALSE { false }
553

    
554
percent_or_bang:
555
  | PERCENTANNOT { }
556
  | BANGANNOT { }
557

    
558

    
559
    
560
main_annot:
561
  | PERCENTANNOT ; MAIN ; SEMICOLON { A.AnnotMain true }
562
  | PSBLOCKSTART ; MAIN ; option (SEMICOLON) ; PSBLOCKEND { A.AnnotMain true }
563
  | SSBLOCKSTART ; MAIN ; option (SEMICOLON) ; SSBLOCKEND { A.AnnotMain true }
564
  | BANGANNOT ; MAIN ; COLON ; b = boolean ; SEMICOLON { A.AnnotMain b }
565
  | PSBLOCKSTART ; MAIN ; COLON ; b = boolean ; option (SEMICOLON) ; PSBLOCKEND {
566
    A.AnnotMain b
567
  }
568
  | SSBLOCKSTART ; MAIN ; COLON ; b = boolean ; option (SEMICOLON) ; SSBLOCKEND {
569
    A.AnnotMain b
570
  }
571

    
572
property:
573
  | percent_or_bang ; PROPERTY ; name = option(STRING) ; e = qexpr ; SEMICOLON
574
    { A.AnnotProperty (mk_pos $startpos, name, e) }
575
  | PSBLOCKSTART ; PROPERTY ; name = option(STRING);
576
    e = qexpr; SEMICOLON ; PSBLOCKEND
577
    { A.AnnotProperty (mk_pos $startpos, name, e) }
578
  | PSBLOCKSTART ; PROPERTY ; name = option(STRING);
579
    COLON; e = qexpr; SEMICOLON ; PSBLOCKEND
580
    { A.AnnotProperty (mk_pos $startpos, name, e) }
581
  | SSBLOCKSTART ; PROPERTY ; name = option(STRING);
582
    e = qexpr ; SEMICOLON; SSBLOCKEND
583
    { A.AnnotProperty (mk_pos $startpos, name, e) }
584
  | SSBLOCKSTART ; PROPERTY ; name = option(STRING);
585
    COLON; e = qexpr ; SEMICOLON; SSBLOCKEND
586
    { A.AnnotProperty (mk_pos $startpos, name, e) }
587

    
588
check:
589
  | CHECK ; name = option(STRING) ; e = qexpr ; SEMICOLON
590
    { A.AnnotProperty (mk_pos $startpos, name, e) }
591

    
592
node_item:
593
  | e = node_equation { A.Body e }
594
  | a = main_annot { a }
595
  | p = property { p }
596
  | p = check { p }
597

    
598

    
599
(* An equations of a node *)
600
node_equation:
601

    
602
  (* An assertion *)
603
  | ASSERT; e = qexpr; SEMICOLON
604
    { A.Assert (mk_pos $startpos, e) }
605

    
606
  (* An equation, multiple (optionally parenthesized) identifiers on 
607
     the left-hand side, an expression on the right *)
608
  | l = left_side; EQUALS; e = expr; SEMICOLON
609
    { A.Equation (mk_pos $startpos, l, e) }
610

    
611
  (* An automaton *)
612
  | AUTOMATON; i = option(ident); s = list(state);
613
    RETURNS; out = ident_list; SEMICOLON
614
    { A.Automaton (mk_pos $startpos, i, s, A.Given out) }
615

    
616
  | AUTOMATON; i = option(ident); s = list(state);
617
    RETURNS DOTDOT SEMICOLON
618
    { A.Automaton (mk_pos $startpos, i, s, A.Inferred) }
619

    
620
  | AUTOMATON; i = option(ident); s = nonempty_list(state)
621
    { A.Automaton (mk_pos $startpos, i, s, A.Inferred) }
622

    
623

    
624
state_decl:
625
  | STATE; i = ident { i, false }
626
  | INITIAL STATE; i = ident { i, true }
627

    
628
state:
629
  | ii = state_decl; option(COLON)
630
    us = unless_transitions;
631
    l = list(node_local_decl);
632
    LET;
633
    e = list(node_equation);
634
    TEL;
635
    ul = until_transitions
636
    { let i, init = ii in
637
      A.State (mk_pos $startpos, i, init, List.flatten l, e,
638
               merge_branches us, merge_branches ul) }
639

    
640
  | ii = state_decl; option(COLON)
641
    us = unless_transitions;
642
    ul = until_transitions
643
    { let i, init = ii in
644
      A.State (mk_pos $startpos, i, init, [], [],
645
               merge_branches us, merge_branches ul) }
646

    
647

    
648
unless_transitions:
649
  | { [] }
650
  | UNLESS; b = transition_branch; u = unless_transitions
651
    { (mk_pos $startpos, b) :: u }
652

    
653

    
654
until_transitions:
655
  | { [] }
656
  | UNTIL; b = transition_branch; u = until_transitions
657
    { (mk_pos $startpos, b) :: u }
658

    
659

    
660
transition_branch:
661
  | b = branch; option(SEMICOLON)
662
    { b }
663
  | e = expr; t = target; option(SEMICOLON)
664
    { A.TransIf (mk_pos $startpos, e, A.Target t, None) }
665
  | IF; e = expr; t = target; option(SEMICOLON)
666
    { A.TransIf (mk_pos $startpos, e, A.Target t, None) }
667

    
668

    
669
branch:
670
  | t = target
671
    { A.Target t }
672
  | IF; e = expr; b = branch; END
673
    { A.TransIf (mk_pos $startpos, e, b, None) }
674
  | IF; e = expr; b = branch; b2 = elsif_branch; END
675
    { A.TransIf (mk_pos $startpos, e, b, Some b2) }
676
    
677
elsif_branch:
678
  | ELSE; b = branch
679
    { b } 
680
  | ELSIF; e = expr; b = branch
681
    { A.TransIf (mk_pos $startpos, e, b, None) }
682
  | ELSIF; e = expr; b = branch; b2 = elsif_branch
683
    { A.TransIf (mk_pos $startpos, e, b, Some b2) }
684

    
685
target_state:
686
  | s = ident
687
    { mk_pos $startpos, s }
688

    
689
target:
690
  | RESTART; s = target_state
691
    { A.TransRestart (mk_pos $startpos, s) }
692

    
693
  | RESUME; s = target_state
694
    { A.TransResume (mk_pos $startpos, s) }
695

    
696
left_side:
697

    
698
  (* List without parentheses *)
699
  | l = struct_item_list { A.StructDef (mk_pos $startpos, l) }
700

    
701
  (* Parenthesized list *)
702
  | LPAREN; l = struct_item_list; RPAREN { A.StructDef (mk_pos $startpos, l) }
703

    
704
  (* Empty list *)
705
  | LPAREN; RPAREN { A.StructDef (mk_pos $startpos, []) }
706

    
707

    
708
(* Item in a structured equation *)
709
struct_item:
710

    
711
  (* Single identifier *)
712
  | s = ident
713
      { A.SingleIdent (mk_pos $startpos, s) }
714
          
715
  (* Recursive array definition *)
716
  | s = ident; l = nonempty_list(index_var)
717
     { A.ArrayDef (mk_pos $startpos, s, l)}
718

    
719
(*
720
  (* Filter array values *)
721
  | LSQBRACKET; l = struct_item_list; RSQBRACKET 
722
    { A.TupleStructItem (mk_pos $startpos, l) }
723

    
724
  (* Select from tuple *)
725
  | e = ident; LSQBRACKET; i = expr; RSQBRACKET 
726
    { A.TupleSelection (mk_pos $startpos, e, i) }
727

    
728
  (* Select from record *)
729
  | e = ident; DOT; i = ident 
730
    { A.FieldSelection (mk_pos $startpos, e, i) }
731
 
732
  | e = ident; LSQBRACKET; s = array_slice_list; RSQBRACKET 
733
    { A.ArraySliceStructItem (mk_pos $startpos, e, s) }
734
*)
735

    
736
(* List of structured items *)
737
struct_item_list:
738
 | l = separated_nonempty_list(COMMA, struct_item) { l }
739

    
740
(* Running variable for index *)
741
index_var:
742
  | LSQBRACKET; s = ident; RSQBRACKET { s }
743

    
744
(* Two colons (for mode reference). *)
745
two_colons:
746
  | COLON ; COLON {}
747

    
748
(* ********************************************************************** *)
749

    
750
(* dummy rule for parameter of pexpr to signal we allow quantifiers *)
751
%inline quantified:
752
  | { true }
753

    
754
(* dummy rule for parameter of pexpr to signal we do not allow quantifiers *)
755
%inline nonquantified:
756
  | { false }
757
  
758
(* An possibly quantified expression *)
759
pexpr(Q): 
760
  
761
  (* An identifier *)
762
  | s = ident { A.Ident (mk_pos $startpos, s) } 
763

    
764
  (* A mode reference. *)
765
  | two_colons ; mode_ref = separated_nonempty_list(two_colons, ident) {
766
    A.ModeRef (mk_pos $startpos, mode_ref)
767
  }
768

    
769
  (* A propositional constant *)
770
  | TRUE { A.True (mk_pos $startpos) }
771
  | FALSE { A.False (mk_pos $startpos) }
772

    
773
  (* An integer numeral or a floating-point decimal constant *)
774
  | s = NUMERAL { A.Num (mk_pos $startpos, s) } 
775
  | s = DECIMAL { A.Dec (mk_pos $startpos, s) } 
776

    
777
  (* Conversions *)
778
  | INT; e = expr { A.ToInt (mk_pos $startpos, e) }
779
  | REAL; e = expr { A.ToReal (mk_pos $startpos, e) }
780

    
781
  (* A parenthesized single expression *)
782
  | LPAREN; e = pexpr(Q); RPAREN { e } 
783

    
784
  (* An expression list (not quantified)
785

    
786
     Singleton list is in production above *)
787
  | LPAREN; h = pexpr(Q); COMMA; l = pexpr_list(Q); RPAREN 
788
    { A.ExprList (mk_pos $startpos, h :: l) } 
789

    
790
  (* A tuple expression (not quantified) *)
791
  (* | LSQBRACKET; l = qexpr_list; RSQBRACKET { A.TupleExpr (mk_pos $startpos, l) } *)
792
  | LCURLYBRACKET; l = pexpr_list(Q); RCURLYBRACKET { A.TupleExpr (mk_pos $startpos, l) }
793

    
794
  (* An array expression (not quantified) *)
795
  | LSQBRACKET; l = pexpr_list(Q); RSQBRACKET { A.ArrayExpr (mk_pos $startpos, l) }
796

    
797
  (* An array constructor (not quantified) *)
798
  | e1 = pexpr(Q); CARET; e2 = expr { A.ArrayConstr (mk_pos $startpos, e1, e2) }
799

    
800
  (* An array slice or tuple projection (not quantified) *)
801
  | e = pexpr(Q); DOTPERCENT; i = expr 
802
    { A.TupleProject (mk_pos $startpos, e, i) }
803

    
804
  (* An array slice (not quantified) *)
805
  | e = pexpr(Q); LSQBRACKET; s = array_slice; RSQBRACKET
806
    { A.ArraySlice (mk_pos $startpos, e, s) }
807

    
808
  (* A record field projection (not quantified) *)
809
  | s = pexpr(Q); DOT; t = ident 
810
    { A.RecordProject (mk_pos $startpos, s, t) }
811

    
812
  (* A record (not quantified) *)
813
  | t = ident; 
814
    f = tlist(LCURLYBRACKET, SEMICOLON, RCURLYBRACKET, record_field_assign)
815
    { A.RecordExpr (mk_pos $startpos, t, f) }
816

    
817
  (* An array concatenation *)
818
  | e1 = pexpr(Q); PIPE; e2 = pexpr(Q) { A.ArrayConcat (mk_pos $startpos, e1, e2) } 
819

    
820
  (* with operator for updating fields of a structure (not quantified) *)
821
  | LPAREN; 
822
    e1 = pexpr(Q); 
823
    WITH; 
824
    i = nonempty_list(label_or_index); 
825
    EQUALS; 
826
    e2 = pexpr(Q); 
827
    RPAREN
828

    
829
    { A.StructUpdate (mk_pos $startpos, e1, i, e2) } 
830

    
831
  (* An arithmetic operation *)
832
  | e1 = pexpr(Q); MINUS; e2 = pexpr(Q) { A.Minus (mk_pos $startpos, e1, e2) }
833
  | MINUS; e = expr { A.Uminus (mk_pos $startpos, e) } 
834
  | e1 = pexpr(Q); PLUS; e2 = pexpr(Q) { A.Plus (mk_pos $startpos, e1, e2) }
835
  | e1 = pexpr(Q); MULT; e2 = pexpr(Q) { A.Times (mk_pos $startpos, e1, e2) }
836
  | e1 = pexpr(Q); DIV; e2 = pexpr(Q) { A.Div (mk_pos $startpos, e1, e2) }
837
  | e1 = pexpr(Q); INTDIV; e2 = pexpr(Q) { A.IntDiv (mk_pos $startpos, e1, e2) }
838
  | e1 = pexpr(Q); MOD; e2 = pexpr(Q) { A.Mod (mk_pos $startpos, e1, e2) }
839

    
840
  (* A Boolean operation *)
841
  | NOT; e = pexpr(Q) { A.Not (mk_pos $startpos, e) } 
842
  | e1 = pexpr(Q); AND; e2 = pexpr(Q) { A.And (mk_pos $startpos, e1, e2) }
843
  | e1 = pexpr(Q); OR; e2 = pexpr(Q) { A.Or (mk_pos $startpos, e1, e2) }
844
  | e1 = pexpr(Q); XOR; e2 = pexpr(Q) { A.Xor (mk_pos $startpos, e1, e2) }
845
  | e1 = pexpr(Q); IMPL; e2 = pexpr(Q) { A.Impl (mk_pos $startpos, e1, e2) }
846
  | HASH; LPAREN; e = pexpr_list(Q); RPAREN { A.OneHot (mk_pos $startpos, e) }
847

    
848
  (* A quantified expression *)
849
  | FORALL; q = Q;
850
    vars = tlist(LPAREN, SEMICOLON, RPAREN, typed_idents); e = pexpr(Q)
851
    %prec prec_forall
852
    { let pos = mk_pos $startpos in
853
      if not q then
854
        assert false
855
               (*LustreContext.fail_at_position
856
          pos "Quantifiers not allowed in this position" *);
857
      A.Forall (pos, List.flatten vars, e) }
858
  | EXISTS; q = Q;
859
    vars = tlist(LPAREN, SEMICOLON, RPAREN, typed_idents); e = pexpr(Q)
860
    %prec prec_exists
861
    { let pos = mk_pos $startpos in
862
      if not q then
863
        assert false 
864
               (* LustreContext.fail_at_position
865
          pos "Quantifiers not allowed in this position" *);
866
      A.Exists (pos, List.flatten vars, e) }
867
                                                                       
868
  (* A relation *)
869
  | e1 = pexpr(Q); LT; e2 = pexpr(Q) { A.Lt (mk_pos $startpos, e1, e2) }
870
  | e1 = pexpr(Q); GT; e2 = pexpr(Q) { A.Gt (mk_pos $startpos, e1, e2) }
871
  | e1 = pexpr(Q); LTE; e2 = pexpr(Q) { A.Lte (mk_pos $startpos, e1, e2) }
872
  | e1 = pexpr(Q); GTE; e2 = pexpr(Q) { A.Gte (mk_pos $startpos, e1, e2) }
873
  | e1 = pexpr(Q); EQUALS; e2 = pexpr(Q) { A.Eq (mk_pos $startpos, e1, e2) } 
874
  | e1 = pexpr(Q); NEQ; e2 = pexpr(Q) { A.Neq (mk_pos $startpos, e1, e2) } 
875

    
876
  (* An if operation *)
877
  | IF; e1 = pexpr(Q); THEN; e2 = pexpr(Q); ELSE; e3 = pexpr(Q) 
878
    { A.Ite (mk_pos $startpos, e1, e2, e3) }
879

    
880
  (* Recursive node call *)
881
  | WITH; e1 = pexpr(Q); THEN; e2 = pexpr(Q); ELSE; e3 = pexpr(Q) 
882
    { A.With (mk_pos $startpos, e1, e2, e3) }
883

    
884
  (* when operator on qexpression  *)
885
  | e1 = pexpr(Q); WHEN; e2 = clock_expr { A.When (mk_pos $startpos, e1, e2) }
886

    
887
  (* current operator on qexpression *)
888
  | CURRENT; e = pexpr(Q) { A.Current (mk_pos $startpos, e) }
889

    
890
  (* condact call with defaults *)
891
  | CONDACT 
892
    LPAREN; 
893
    e1 = pexpr(Q); 
894
    COMMA; 
895
    s = ident; LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN; 
896
    COMMA; 
897
    d = pexpr_list(Q)
898
    RPAREN
899
    { let pos = mk_pos $startpos in
900
      A.Condact (pos, e1, A.False pos, s, a, d) } 
901

    
902
  (* condact call may have no return values and therefore no defaults *)
903
  | CONDACT 
904
    LPAREN; 
905
    c = pexpr(Q); 
906
    COMMA; 
907
    s = ident; LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN; 
908
    RPAREN
909

    
910
    { let pos = mk_pos $startpos in
911
      A.Condact (pos, c, A.False pos, s, a, []) } 
912

    
913
  (* condact call with defaults and restart *)
914
  | CONDACT LPAREN;
915
    c = pexpr(Q); 
916
    COMMA;
917
    LPAREN RESTART; s = ident; EVERY; r = pexpr(Q); RPAREN;
918
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN; 
919
    COMMA; 
920
    d = pexpr_list(Q);
921
    RPAREN
922
    { let pos = mk_pos $startpos in
923
      A.Condact (pos, c, r, s, a, d) } 
924

    
925
  (* condact call with no return values and restart *)
926
  | CONDACT ; LPAREN;
927
    c = pexpr(Q); 
928
    COMMA; 
929
    LPAREN RESTART; s = ident; EVERY; r = pexpr(Q); RPAREN
930
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN; 
931
    RPAREN
932
    { let pos = mk_pos $startpos in
933
      A.Condact (pos, c, r, s, a, []) } 
934

    
935
  (* [(activate N every h initial default (d1, ..., dn)) (e1, ..., en)] 
936
     is an alias for [condact(h, N(e1, ..., en), d1, ,..., dn) ]*)
937
  | LPAREN; ACTIVATE; s = ident; EVERY; c = pexpr(Q); 
938
    INITIAL DEFAULT; d = separated_list(COMMA, pexpr(Q)); RPAREN; 
939
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
940

    
941
    { let pos = mk_pos $startpos in
942
      A.Condact (pos, c, A.False pos, s, a, d) }
943
    
944
  (* activate operator without initial defaults
945

    
946
     Only supported inside a merge *)
947
  | LPAREN; ACTIVATE; s = ident; EVERY; c = pexpr(Q); RPAREN; 
948
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
949

    
950
    { let pos = mk_pos $startpos in
951
      A.Activate (pos, s, c, A.False pos, a) }
952

    
953
  (* activate restart *)
954
  | LPAREN; ACTIVATE;
955
    LPAREN RESTART; s = ident; EVERY; r = pexpr(Q); RPAREN;
956
    EVERY; c = pexpr(Q); 
957
    INITIAL DEFAULT; d = separated_list(COMMA, pexpr(Q)); RPAREN; 
958
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
959

    
960
    { let pos = mk_pos $startpos in
961
      A.Condact (pos, c, r, s, a, d) }
962
    
963
  (* alternative syntax for activate restart *)
964
  | LPAREN; ACTIVATE; s = ident; EVERY; c = pexpr(Q); 
965
    INITIAL DEFAULT; d = separated_list(COMMA, pexpr(Q));
966
    RESTART EVERY; r = pexpr(Q); RPAREN;
967
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
968

    
969
    { let pos = mk_pos $startpos in
970
      A.Condact (pos, c, r, s, a, d) }
971
    
972
  (* activate operator without initial defaults and restart
973

    
974
     Only supported inside a merge *)
975
  | LPAREN; ACTIVATE;
976
    LPAREN RESTART; s = ident; EVERY; r = pexpr(Q); RPAREN;
977
    EVERY; c = pexpr(Q); RPAREN; 
978
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
979

    
980
    { let pos = mk_pos $startpos in
981
      A.Activate (pos, s, c, r, a) }
982
    
983
  (* alternative syntax of previous construct  *)
984
  | LPAREN; ACTIVATE; s = ident; EVERY; c = pexpr(Q);
985
    RESTART EVERY; r = pexpr(Q); RPAREN;
986
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
987

    
988
    { let pos = mk_pos $startpos in
989
      A.Activate (pos, s, c, r, a) }
990

    
991
    
992
  (* restart node call *)
993
  (*| RESTART; s = ident;
994
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN;
995
    EVERY; c = clock_expr
996

    
997
    { A.RestartEvery (mk_pos $startpos, s, a, c) }
998
   *)
999
    
1000
  (* alternative syntax for restart node call *)
1001
  | LPAREN; RESTART; s = ident; EVERY; c = pexpr(Q); RPAREN; 
1002
    LPAREN; a = separated_list(COMMA, pexpr(Q)); RPAREN
1003

    
1004
    { A.RestartEvery (mk_pos $startpos, s, a, c) }
1005
    
1006
        
1007
  (* Binary merge operator *)
1008
  | MERGE; LPAREN;
1009
    c = ident; SEMICOLON;
1010
    pos = pexpr(Q); SEMICOLON;
1011
    neg = pexpr(Q); RPAREN 
1012
    { A.Merge (mk_pos $startpos, c, ["true", pos; "false", neg]) }
1013

    
1014
  (* N-way merge operator *)
1015
  | MERGE; 
1016
    c = ident;
1017
    l = nonempty_list(merge_case);
1018
    { A.Merge (mk_pos $startpos, c, l) }
1019
    
1020
  (* A temporal operation *)
1021
  | PRE; e = pexpr(Q) { A.Pre (mk_pos $startpos, e) }
1022
  | FBY LPAREN; e1 = pexpr(Q) COMMA; s = NUMERAL; COMMA; e2 = pexpr(Q) RPAREN
1023
    { A.Fby (mk_pos $startpos, e2, (int_of_string s), e2) } 
1024

    
1025
  | e1 = pexpr(Q); ARROW; e2 = pexpr(Q) { A.Arrow (mk_pos $startpos, e1, e2) }
1026

    
1027
  | LAST; i = ident_or_quotident { A.Last (mk_pos $startpos, i) }
1028
    
1029
  (* A node or function call *)
1030
  | e = node_call { e } 
1031

    
1032

    
1033
%inline qexpr:
1034
  | e = pexpr(quantified) { e }
1035

    
1036
%inline expr:
1037
  | e = pexpr(nonquantified) { e }
1038

    
1039

    
1040
(* A list of expressions *)
1041
pexpr_list(Q): l = separated_nonempty_list(COMMA, pexpr(Q)) { l }
1042

    
1043

    
1044
(* Static parameters are only types *)
1045
node_call_static_param:
1046
  | t = lustre_type { t }
1047
      
1048

    
1049
(* A node or function call *)
1050
node_call:
1051

    
1052
  (* Call a node without static parameters *)
1053
  | s = ident; LPAREN; a = separated_list(COMMA, expr); RPAREN 
1054
    { A.Call (mk_pos $startpos, s, a) }
1055

    
1056
  (* Call a node with static parameters *)
1057
  | s = ident; 
1058
    p = tlist 
1059
         (LPARAMBRACKET, SEMICOLON, RPARAMBRACKET, node_call_static_param); 
1060
    LPAREN; 
1061
    a = separated_list(COMMA, expr); 
1062
    RPAREN 
1063
    { A.CallParam (mk_pos $startpos, s, p, a) }
1064

    
1065

    
1066
(* An array slice *)
1067
array_slice:
1068
  | il = expr; DOTDOT; iu = expr { il, iu }
1069
  | i = expr { i, i }
1070

    
1071

    
1072
(* An assignment to a record field *)
1073
record_field_assign: s = ident; EQUALS; e = expr { (s, e) } 
1074

    
1075

    
1076
(* ********************************************************************** *)
1077

    
1078

    
1079
clock_expr:
1080
  | c = ident { A.ClockPos c } 
1081
  | NOT; c = ident { A.ClockNeg c } 
1082
  | NOT; LPAREN; c = ident; RPAREN { A.ClockNeg c } 
1083
  | cs = ident; LPAREN; c = ident; RPAREN { A.ClockConstr (cs, c) } 
1084
  | TRUE { A.ClockTrue }
1085

    
1086
merge_case_id:
1087
  | TRUE { "true" }
1088
  | FALSE { "false" }
1089
  | c = ident { c }
1090

    
1091
merge_case :
1092
  | LPAREN; c = merge_case_id; ARROW; e = expr; RPAREN { c, e }
1093

    
1094
    
1095
(* ********************************************************************** *)
1096

    
1097

    
1098
(* An identifier *)
1099
ident:
1100
  (* Contract tokens are not keywords. *)
1101
  | MODE { "mode" }
1102
  | ASSUME { "assume" }
1103
  | GUARANTEE { "guarantee" }
1104
  | REQUIRE { "require" }
1105
  | ENSURE { "ensure" }
1106
  | s = SYM { s }
1107

    
1108
ident_or_quotident:
1109
  | id = ident { id }
1110
  | s = QUOTSYM { s }
1111

    
1112
(* An identifier with a type *)
1113
typed_ident: s = ident; COLON; t = lustre_type { (mk_pos $startpos, s, t) }
1114

    
1115

    
1116
(* A comma-separated list of identifiers *)
1117
ident_list:
1118
  | l = separated_nonempty_list(COMMA, ident) { l }
1119

    
1120

    
1121
(* A comma-separated list of types *)
1122
lustre_type_list:
1123
  | l = separated_nonempty_list(COMMA, lustre_type) { l }
1124
  
1125

    
1126
(* A comma-separated list of identifiers with position information *)
1127
ident_list_pos :
1128
  | i = ident { [mk_pos $startpos, i] }
1129
  | i = ident; COMMA; l = ident_list_pos
1130
    { (mk_pos $startpos, i) :: l }
1131

    
1132

    
1133
(* A list of comma-separated identifiers with a type *)
1134
typed_idents: 
1135
  | l = ident_list_pos; COLON; t = lustre_type 
1136
    (* Pair each identifier with the type *)
1137
    { List.map (function (pos, e) -> (pos, e, t)) l }
1138

    
1139
(*
1140
(* A list of lists of typed identifiers *)
1141
typed_idents_list:
1142
  | a = separated_list(SEMICOLON, typed_idents) 
1143

    
1144
    (* Return a flat list *)
1145
    { List.flatten a }
1146
*)
1147

    
1148
(* Typed identifiers that may be constant *)
1149
const_typed_idents: 
1150
  | o = boption(CONST); l = typed_idents 
1151

    
1152
    (* Pair each typed identifier with a flag *)
1153
    { List.map (function (_, e, t) -> (e, t, o)) l }
1154

    
1155
(*
1156
(* A list of lists of typed identifiers that may be constant *)
1157
const_typed_idents_list: 
1158
  | a = separated_list(SEMICOLON, const_typed_idents)
1159

    
1160
    (* Return a flat list *)
1161
    { List.flatten a }
1162
*)
1163

    
1164
(* A list of comma-separated identifiers with a type *)
1165
clocked_typed_idents: 
1166

    
1167
  (* Unclocked typed identifiers *)
1168
  | l = typed_idents
1169

    
1170
    (* Pair each typed identifier with the base clock *)
1171
    { List.map (function (pos, e, t) -> (pos, e, t, A.ClockTrue)) l }
1172

    
1173
  (* Clocked typed identifiers *)
1174
  | l = typed_idents; WHEN; c = clock_expr
1175
  | LPAREN; l = typed_idents; RPAREN; WHEN; c = clock_expr
1176

    
1177
    (* Pair each types identifier the given clock *)
1178
    { List.map (function (pos, e, t) -> (pos, e, t, c)) l }
1179

    
1180
  (* Separate rule for non-singleton list to avoid shift/reduce conflict *)
1181
  | LPAREN; 
1182
    h = typed_idents; 
1183
    SEMICOLON; 
1184
    l = tlist_tail(SEMICOLON, RPAREN, typed_idents); 
1185
    WHEN; 
1186
    c = clock_expr
1187

    
1188
    (* Pair each types identifier the given clock *)
1189
    { List.map
1190
        (function (pos, e, t) -> (pos, e, t, c)) 
1191
        (h @ (List.flatten l)) }
1192

    
1193

    
1194
(*
1195
(* A list of lists of typed and clocked identifiers *)
1196
clocked_typed_idents_list: 
1197
  | a = separated_list(SEMICOLON, clocked_typed_idents)
1198

    
1199
    (* Return a flat list *)
1200
    { List.flatten a }
1201
*)
1202

    
1203
(* A list of comma-separated identifiers with a type and a clock that may be constant *)
1204
const_clocked_typed_idents: 
1205

    
1206
  (* Unclocked typed identifiers *)
1207
  | l = const_typed_idents
1208

    
1209
    (* Pair each typed identifier with the base clock *)
1210
    { List.map
1211
        (function (e, t, o) -> (mk_pos $startpos, e, t, A.ClockTrue, o)) 
1212
        l }
1213

    
1214
  (* Clocked typed identifiers *)
1215
  | l = const_typed_idents; WHEN; c = clock_expr
1216
  | LPAREN; l = const_typed_idents; RPAREN; WHEN; c = clock_expr
1217

    
1218
    (* Pair each types identifier the given clock *)
1219
    { List.map
1220
        (function (e, t, o) -> (mk_pos $startpos, e, t, c, o)) 
1221
        l }
1222

    
1223
  (* Separate rule for non-singleton list to avaoid shift/reduce conflict *)
1224
  | LPAREN; 
1225
    h = const_typed_idents; 
1226
    SEMICOLON; 
1227
    l = tlist_tail(SEMICOLON, RPAREN, const_typed_idents); 
1228
    WHEN; 
1229
    c = clock_expr
1230

    
1231
    (* Pair each types identifier the given clock *)
1232
    { List.map (function (e, t, o) -> (mk_pos $startpos, e, t, c, o)) (h @ (List.flatten l)) }
1233

    
1234
(*
1235
(* A list of lists of typed and clocked identifiers that may be constant *)
1236
const_clocked_typed_idents_list: 
1237
  | a = separated_list(SEMICOLON, const_clocked_typed_idents)
1238

    
1239
      { List.flatten a }
1240
*)
1241

    
1242
(* The tail of a list of X *)
1243
tlist_tail(separator, closing, X):
1244
  | x = X; option(separator); closing { [ x ] }
1245
  | x = X; separator; xs = tlist_tail(separator, closing, X)
1246
    { x :: xs }
1247

    
1248
(* A list of elements between opening and closing, separated by separator, 
1249
   the separator may occur at the end of the list *)
1250
tlist(opening, separator, closing, X):
1251
  | opening; l = tlist_tail(separator, closing, X) { l }
1252
  | opening; closing { [ ] }
1253

    
1254
(* ********************************************************************** *)
1255

    
1256

    
1257
(* An index *)
1258
label_or_index: 
1259

    
1260
  (* An index into a record *)
1261
  | DOT; i = ident
1262
     { A.Label (mk_pos $startpos, i) } 
1263

    
1264
  (* An index into an array with a variable or constant *)
1265
  | LSQBRACKET; e = expr; RSQBRACKET
1266
     { A.Index (mk_pos $startpos, e) }
1267

    
1268
  (* An index into a tuple with a variable or constant *)
1269
  | DOTPERCENT; e = expr; 
1270
     { A.Index (mk_pos $startpos, e) }
1271

    
1272

    
1273

    
1274
(* 
1275
   Local Variables:
1276
   compile-command: "make -k"
1277
   indent-tabs-mode: nil
1278
   End: 
1279
*)
1280