Project

General

Profile

Download (21 KB) Statistics
| Branch: | Tag: | Revision:
1
/********************************************************************/
2
/*                                                                  */
3
/*  The LustreC compiler toolset   /  The LustreC Development Team  */
4
/*  Copyright 2012 -    --   ONERA - CNRS - INPT                    */
5
/*                                                                  */
6
/*  LustreC is free software, distributed WITHOUT ANY WARRANTY      */
7
/*  under the terms of the GNU Lesser General Public License        */
8
/*  version 2.1.                                                    */
9
/*                                                                  */
10
/********************************************************************/
11

    
12
%{
13
open Utils
14
open Lustre_types
15
open Corelang
16
open Dimension
17

    
18
   
19
let mkident loc x = x, loc
20
let mkotyp loc x = match x with Some t -> Some (mktyp loc t) | None -> None
21
let mkvar_decl loc x = mkvar_decl loc ~orig:true x
22
let mktop_decl loc x = mktop_decl loc (Location.get_module ()) x
23
let mkpredef_call_b loc f x1 x2 = mkpredef_call loc f [x1; x2]
24
let mkpredef_call_u loc f x = mkpredef_call loc f [x]
25

    
26
let mkdim_appl_b loc f x1 x2 = mkdim_appl loc f [x1; x2]
27
let mkdim_appl_u loc f x = mkdim_appl loc f [x]
28

    
29
let mkarraytype = List.fold_left (fun t d -> Tydec_array (d, t))
30

    
31
let mkvdecls const typ clock expr =
32
  List.map (fun (id, loc) ->
33
      mkvar_decl loc
34
        (id,
35
         mktyp loc (match typ with Some t -> t | None -> Tydec_any),
36
         (match clock with Some ck -> ck | None -> mkclock loc Ckdec_any),
37
         const, expr, None))
38

    
39
(* let mkannots annots = { annots = annots; annot_loc = get_loc () } *)
40

    
41
let node_stack : ident list ref = ref []
42
(* let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack *)
43
let push_node nd = node_stack := nd :: !node_stack; nd
44
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
45
let get_current_node () = try List.hd !node_stack with _ -> assert false
46

    
47
let rec fby loc expr n init =
48
  mkexpr loc
49
    (Expr_arrow
50
       (init,
51
        mkexpr loc (Expr_pre
52
                      (if n <= 1 then expr else fby loc expr (n - 1) init))))
53

    
54
 
55
%}
56

    
57
%token <int> INT
58
%token <Real.t> REAL
59

    
60
%token <string> STRING
61
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
62
%token ASSERT OPEN INCLUDE QUOTE POINT FUNCTION
63
%token <string> IDENT
64
%token <string> UIDENT
65
%token TRUE FALSE
66
%token <Lustre_types.expr_annot> ANNOT
67
%token <Lustre_types.spec_types> NODESPEC
68
%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
69
%token AMPERAMPER BARBAR NOT POWER
70
%token IF THEN ELSE
71
%token MERGE FBY WHEN WHENNOT EVERY
72
%token NODE LET TEL RETURNS VAR TYPE CONST
73
%token STRUCT ENUM
74
%token TINT TREAL TBOOL TCLOCK
75
%token EQ LT GT LTE GTE NEQ
76
%token AND OR XOR IMPL
77
%token MULT DIV MOD
78
%token MINUS PLUS 
79
%token PRE ARROW
80
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT
81
%token INVARIANT MODE CCODE MATLAB
82
%token EXISTS FORALL
83
%token PROTOTYPE LIB
84
%token EOF
85

    
86
%nonassoc p_string
87
(* %nonassoc p_vdecl *)
88
(* %left SCOL *)
89
%nonassoc EVERY
90
%nonassoc ELSE
91
%right ARROW FBY
92
%left WHEN WHENNOT 
93
%right IMPL
94
%left OR XOR BARBAR
95
%left AND AMPERAMPER
96
%left NOT
97
%nonassoc EQ LT GT LTE GTE NEQ
98
%left MINUS PLUS
99
%left MULT DIV MOD
100
%left p_uminus
101
%left POWER
102
%left PRE
103
%nonassoc RBRACKET
104
%nonassoc LBRACKET
105

    
106
%start <Lustre_types.top_decl list> prog
107

    
108
%start <Lustre_types.top_decl list> header
109

    
110
%start <Lustre_types.expr_annot> lustre_annot
111

    
112
%start <Lustre_types.spec_types> lustre_spec
113

    
114
%%
115

    
116
ident:
117
| x=UIDENT { x }
118
| x=IDENT  { x }
119

    
120
module_ident:
121
| m=ident { m }
122

    
123
file_ident:
124
| m=module_ident                    { m }
125
| m=module_ident POINT f=file_ident { m ^ "." ^ f }
126

    
127
path_ident:
128
| POINT DIV p=path_ident        { "./" ^ p }
129
| f=file_ident DIV p=path_ident { f ^ "/" ^ p }
130
| DIV p=path_ident              { "/" ^ p }
131
| f=file_ident                  { f }
132

    
133
tag_bool:
134
| TRUE  { tag_true }
135
| FALSE { tag_false }
136

    
137
tag_ident:
138
| t=UIDENT   { t }
139
| t=tag_bool { t }
140

    
141
node_ident:
142
| n=ident { n }
143

    
144
node_ident_decl:
145
| n=node_ident { push_node n }
146

    
147
vdecl_ident:
148
| x=ident { mkident $sloc x }
149

    
150
const_ident:
151
| c=ident { c }
152

    
153
type_ident:
154
| t=IDENT { t }
155

    
156
prog:
157
| p=prefix ds=flatten(top_decl*) EOF { List.map ((|>) false) p @ ds }
158

    
159
header:
160
| p=prefix ds=flatten(top_decl_header*) EOF { List.map ((|>) true) p @ ds }
161

    
162
prefix:
163
|                      { [] }
164
| o=open_lusi p=prefix { (fun _ -> o) :: p }
165
| td=typ_def p=prefix  { (fun is_header -> td is_header) :: p }
166

    
167
open_lusi:
168
| OPEN QUOTE p=path_ident QUOTE    { mktop_decl $sloc false (Open (true, p)) }
169
| INCLUDE QUOTE p=path_ident QUOTE { mktop_decl $sloc false (Include p) }
170
| OPEN LT p=path_ident GT          { mktop_decl $sloc false (Open (false, p))  }
171

    
172
state_annot:
173
| FUNCTION { true }
174
| NODE     { false }
175

    
176
top_decl_header:
177
| CONST ds=cdecl+ SCOL
178
  { List.map ((|>) true) ds }
179
| nodei_spec=nodespecs nodei_stateless=state_annot nodei_id=node_ident_decl
180
  LPAR nodei_inputs=var_decl_list(vdecl) RPAR
181
  RETURNS LPAR nodei_outputs=var_decl_list(vdecl) RPAR
182
  nodei_prototype=preceded(PROTOTYPE, node_ident)?
183
  nodei_in_lib=preceded(LIB, module_ident)* SCOL
184
  { let nd = mktop_decl $sloc true
185
                           (ImportedNode {
186
                                nodei_id;
187
                                nodei_type = Types.new_var ();
188
                                nodei_clock = Clocks.new_var true;
189
                                nodei_inputs;
190
                                nodei_outputs;
191
                                nodei_stateless;
192
                                nodei_spec;
193
                                nodei_prototype;
194
                                nodei_in_lib
195
                           })
196
    in
197
    pop_node ();
198
    [nd]
199
  }
200
| c=top_contract
201
  { [c] }
202

    
203
top_decl:
204
| CONST ds=cdecl+ SCOL
205
  { List.map ((|>) false) ds }
206
| node_dec_stateless=state_annot node_id=node_ident_decl
207
  LPAR node_inputs=var_decl_list(vdecl) RPAR
208
  RETURNS LPAR node_outputs=var_decl_list(vdecl) RPAR SCOL?
209
  node_spec=nodespecs
210
  node_locals=locals LET content=stmt_list TEL
211
  { let node_stmts, node_asserts, node_annot = content in
212
    (* Declaring eqs annots *)
213
    List.iter (fun ann ->
214
        List.iter (fun (key, _) ->
215
            Annotations.add_node_ann node_id key)
216
          ann.annots)
217
      node_annot;
218
    (* Building the node *)
219
    let nd = mktop_decl $sloc false
220
                           (Node {
221
                                node_id;
222
                                node_type = Types.new_var ();
223
                                node_clock = Clocks.new_var true;
224
                                node_inputs;
225
                                node_outputs;
226
                                node_locals;
227
                                node_gencalls = [];
228
                                node_checks = [];
229
                                node_asserts;
230
                                node_stmts;
231
                                node_dec_stateless;
232
                                node_stateless = None;
233
                                node_spec;
234
                                node_annot;
235
                                node_iscontract = false;
236
                           })
237
    in
238
    pop_node ();
239
    (*add_node $3 nd;*)
240
    [nd]
241
  }
242
| s=NODESPEC
243
  { match s with
244
    | LocalContract _ -> assert false
245
    | TopContract c   -> c
246
  }
247

    
248
nodespecs:
249
| ss=nodespec_list
250
  { match ss with
251
    | None   -> None
252
    | Some c -> Some (Contract c)
253
  }
254

    
255
nodespec_list:
256
| { None }
257
| s=NODESPEC ss=nodespec_list
258
  { let extract x = match x with LocalContract c -> c | _ -> assert false in
259
    let s1 = extract s in
260
    match ss with
261
    | None -> Some s1
262
    | Some s2 -> Some (merge_contracts s1 s2)
263
  }
264

    
265
typ_def:
266
| TYPE tydef_id=type_ident EQ tydef_desc=typ_def_rhs SCOL
267
  { fun itf ->
268
    let typ = mktop_decl $sloc itf (TypeDef { tydef_id; tydef_desc }) in
269
    (*add_type itf $2 typ;*)
270
    typ
271
  }
272

    
273
typ_def_rhs:
274
| t=typeconst
275
  { t }
276
| ENUM LCUR ts=separated_nonempty_list(COMMA, UIDENT) RCUR
277
  { Tydec_enum ts }
278
| STRUCT LCUR fs=separated_list(SCOL, separated_pair(IDENT, COL, typeconst)) RCUR
279
  { Tydec_struct fs }
280

    
281
%inline array_typ_decl:
282
|                          { [] }
283
| ds=preceded(POWER, dim)+ { ds }
284

    
285
typeconst:
286
| TINT ds=array_typ_decl         { mkarraytype Tydec_int ds }
287
| TBOOL ds=array_typ_decl        { mkarraytype Tydec_bool ds }
288
| TREAL ds=array_typ_decl        { mkarraytype Tydec_real ds }
289
/* | TFLOAT ds=array_typ_decl { mkarraytype Tydec_float ds } */
290
| t=type_ident ds=array_typ_decl { mkarraytype (Tydec_const t) ds }
291
| TBOOL TCLOCK                   { Tydec_clock Tydec_bool }
292
| t=IDENT TCLOCK                 { Tydec_clock (Tydec_const t) }
293

    
294
stmt_list:
295
| { [], [], [] }
296
| e=eq ss=stmt_list
297
  { let eql, assertl, annotl = ss in
298
    Eq e :: eql, assertl, annotl
299
  }
300
| a=assert_ ss=stmt_list
301
  { let eql, assertl, annotl = ss in
302
    eql, a :: assertl, annotl
303
  }
304
| a=ANNOT ss=stmt_list
305
  { let eql, assertl, annotl = ss in
306
    eql, assertl, a :: annotl
307
  }
308
| a=automaton ss=stmt_list
309
  { let eql, assertl, annotl = ss in
310
    Aut a :: eql, assertl, annotl
311
  }
312

    
313
automaton:
314
| AUTOMATON t=type_ident hs=handler* { Automata.mkautomata $sloc t hs }
315

    
316
handler:
317
| STATE x=UIDENT COL ul=unless* l=locals LET ss=stmt_list TEL ut=until*
318
  { Automata.mkhandler $sloc x ul ut l ss }
319

    
320
unless:
321
| UNLESS e=expr RESTART s=UIDENT { $sloc, e, true, s  }
322
| UNLESS e=expr RESUME s=UIDENT  { $sloc, e, false, s }
323

    
324
until:
325
| UNTIL e=expr RESTART s=UIDENT { $sloc, e, true, s }
326
| UNTIL e=expr RESUME s=UIDENT  { $sloc, e, false, s }
327

    
328
assert_:
329
| ASSERT e=expr SCOL { mkassert $sloc e }
330

    
331
eq:
332
| xs=pattern EQ e=expr SCOL {mkeq $sloc (List.map fst xs, e)}
333

    
334
%inline pattern:
335
| xs=ident_list           { xs }
336
| LPAR xs=ident_list RPAR { xs }
337

    
338
lustre_spec:
339
| cs=top_contract+ EOF             { TopContract cs }
340
| CONTRACT? c=contract_content EOF { LocalContract c }
341

    
342
top_contract:
343
| CONTRACT node_id=node_ident_decl
344
  LPAR node_inputs=var_decl_list(vdecl) RPAR
345
  RETURNS LPAR node_outputs=var_decl_list(vdecl) RPAR SCOL?
346
  LET cc=contract_content TEL
347
  { let nd = mktop_decl $sloc true
348
                           (Node {
349
                                node_id;
350
                                node_type = Types.new_var ();
351
                                node_clock = Clocks.new_var true;
352
                                node_inputs;
353
                                node_outputs;
354
                                node_locals = []; (* will be filled later *)
355
                                node_gencalls = [];
356
                                node_checks = [];
357
                                node_asserts = [];
358
                                node_stmts = []; (* will be filled later *)
359
                                node_dec_stateless = false;
360
                                (* By default we assume contracts as stateful *)
361
                                node_stateless = None;
362
                                node_spec = Some (Contract cc);
363
                                node_annot = [];
364
                                node_iscontract = true;
365
                              })
366
    in
367
    pop_node ();
368
    (*add_imported_node $3 nd;*)
369
    nd
370
  }
371

    
372
contract_content:
373
| { empty_contract }
374
/* | CONTRACT cc=contract_content */
375
/*   { cc } */
376
| CONST x=IDENT t=option(preceded(COL, typeconst)) EQ e=expr SCOL cc=contract_content
377
  { merge_contracts (mk_contract_var x true (mkotyp $sloc t) e $sloc) cc }
378
| VAR x=IDENT COL t=typeconst EQ e=expr SCOL cc=contract_content
379
  { merge_contracts (mk_contract_var x false (Some (mktyp $sloc t)) e $sloc) cc }
380
| ASSUME x=ioption(STRING) e=qexpr SCOL cc=contract_content
381
  { merge_contracts (mk_contract_assume x e) cc }
382
| GUARANTEES x=ioption(STRING) e=qexpr SCOL cc=contract_content
383
  { merge_contracts (mk_contract_guarantees x e) cc }
384
| MODE x=IDENT LPAR mc=mode_content RPAR SCOL cc=contract_content
385
  { merge_contracts (
386
        let r, e = mc in
387
        mk_contract_mode x r e $sloc) cc
388
  }
389
| IMPORT x=IDENT LPAR xs=expr_or_tuple RPAR RETURNS LPAR ys=expr_or_tuple RPAR
390
  SCOL cc=contract_content
391
  { merge_contracts (mk_contract_import x xs ys $sloc) cc }
392

    
393
%inline expr_or_tuple:
394
| e=expr                     { e }
395
| e=expr COMMA es=array_expr { mkexpr $sloc (Expr_tuple (e :: es)) }
396

    
397
mode_content:
398
| { [], [] }
399
| REQUIRE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
400
  { let (r, e) = mc in
401
    { qe with eexpr_name } :: r, e }
402
| ENSURE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
403
  { let (r, e) = mc in
404
    r, { qe with eexpr_name } :: e }
405

    
406
(* /* WARNING: UNUSED RULES */
407
 * tuple_qexpr:
408
 * | qexpr COMMA qexpr {[$3;$1]}
409
 * | tuple_qexpr COMMA qexpr {$3::$1} *)
410

    
411
qexpr:
412
| e=expr                      { mkeexpr $sloc e }
413
  /* Quantifiers */
414
| EXISTS x=vdecl SCOL e=qexpr { extend_eexpr [Exists, x] e }
415
| FORALL x=vdecl SCOL e=qexpr { extend_eexpr [Forall, x] e }
416

    
417
(* %inline tuple_expr:
418
 * | e=expr COMMA es=array_expr { e :: es } *)
419

    
420
// Same as tuple expr but accepting lists with single element
421
%inline array_expr:
422
| es=separated_nonempty_list(COMMA, expr) { es }
423

    
424
expr:
425
/* constants */
426
| c=INT                   { mkexpr $sloc (Expr_const (Const_int c)) }
427
| c=REAL                  { mkexpr $sloc (Expr_const (Const_real c)) }
428
| c=STRING %prec p_string { mkexpr $sloc (Expr_const (Const_string c)) }
429
| COLCOL c=IDENT          { mkexpr $sloc (Expr_const (Const_modeid c)) }
430
/* | c=FLOAT { mkexpr $sloc (Expr_const (Const_float c)) }*/
431

    
432
/* Idents or type enum tags */
433
| x=IDENT    { mkexpr $sloc (Expr_ident x) }
434
| x=UIDENT   { mkexpr $sloc (Expr_ident x) (* TODO we will differenciate enum constants from variables later *) }
435
| t=tag_bool { mkexpr $sloc (Expr_const (Const_tag t)) } (* on sept 2014, X changed the Const to
436
                                                      mkexpr $sloc (Expr_ident $1)
437
                                                      reverted back to const on july 2019 *)
438
| LPAR a=ANNOT e=expr RPAR  { update_expr_annot (get_current_node ()) e a }
439
| LPAR e=expr_or_tuple RPAR { e }
440

    
441
/* Array expressions */
442
| LBRACKET es=array_expr RBRACKET
443
  { mkexpr $sloc (Expr_array es) }
444
| e=expr POWER d=dim
445
  { mkexpr $sloc (Expr_power (e, d)) }
446
| e=expr ds=delimited(LBRACKET, dim, RBRACKET)+
447
  { List.fold_left (fun base d -> mkexpr $sloc (Expr_access (base, d))) e ds }
448

    
449
/* Temporal operators */
450
| PRE e=expr
451
  { mkexpr $sloc (Expr_pre e) }
452
| e1=expr ARROW e2=expr
453
  { mkexpr $sloc (Expr_arrow (e1, e2)) }
454
| e1=expr FBY e2=expr
455
  { mkexpr $sloc (Expr_arrow (e1, mkexpr $loc(e2) (Expr_pre e2))) }
456
| e=expr WHEN x=vdecl_ident
457
  { mkexpr $sloc (Expr_when (e, fst x, tag_true)) }
458
| e=expr WHENNOT x=vdecl_ident
459
  { mkexpr $sloc (Expr_when (e, fst x, tag_false)) }
460
| e=expr WHEN t=tag_ident LPAR x=vdecl_ident RPAR
461
  { mkexpr $sloc (Expr_when (e, fst x, t)) }
462
| MERGE x=vdecl_ident
463
  hs=delimited(LPAR, separated_pair(tag_ident, ARROW, expr), RPAR)*
464
  { mkexpr $sloc (Expr_merge (fst x, hs)) }
465

    
466
/* Applications */
467
| f=node_ident LPAR es=expr_or_tuple RPAR r=preceded(EVERY, expr)?
468
  { match f, es.expr_desc, r with
469
    | "fbyn", Expr_tuple [expr; n; init], None ->
470
       let n = match n.expr_desc with
471
         | Expr_const (Const_int n) -> n
472
         | _ -> assert false
473
       in
474
       fby $sloc expr n init
475
    | "fbyn", _ , Some _ ->
476
       assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
477
    | _ -> mkexpr $sloc (Expr_appl (f, es, r))
478
  }
479

    
480
/* Boolean expr */
481
| e1=expr AND e2=expr         { mkpredef_call_b $sloc "&&" e1 e2 }
482
| e1=expr AMPERAMPER e2=expr  { mkpredef_call_b $sloc "&&" e1 e2 }
483
| e1=expr OR e2=expr          { mkpredef_call_b $sloc "||" e1 e2 }
484
| e1=expr BARBAR e2=expr      { mkpredef_call_b $sloc "||" e1 e2 }
485
| e1=expr XOR e2=expr         { mkpredef_call_b $sloc "xor" e1 e2 }
486
| NOT e=expr                  { mkpredef_call_u $sloc "not" e }
487
| e1=expr IMPL e2=expr        { mkpredef_call_b $sloc "impl" e1 e2 }
488

    
489
/* Comparison expr */
490
| e1=expr EQ e2=expr          { mkpredef_call_b $sloc "=" e1 e2 }
491
| e1=expr LT e2=expr          { mkpredef_call_b $sloc "<" e1 e2 }
492
| e1=expr LTE e2=expr         { mkpredef_call_b $sloc "<=" e1 e2 }
493
| e1=expr GT e2=expr          { mkpredef_call_b $sloc ">" e1 e2 }
494
| e1=expr GTE e2=expr         { mkpredef_call_b $sloc ">=" e1 e2 }
495
| e1=expr NEQ e2=expr         { mkpredef_call_b $sloc "!=" e1 e2 }
496

    
497
/* Arithmetic expr */
498
| e1=expr PLUS e2=expr        { mkpredef_call_b $sloc "+" e1 e2 }
499
| e1=expr MINUS e2=expr       { mkpredef_call_b $sloc "-" e1 e2 }
500
| e1=expr MULT e2=expr        { mkpredef_call_b $sloc "*" e1 e2 }
501
| e1=expr DIV e2=expr         { mkpredef_call_b $sloc "/" e1 e2 }
502
| MINUS e=expr %prec p_uminus { mkpredef_call_u $sloc "uminus" e }
503
| e1=expr MOD e2=expr         { mkpredef_call_b $sloc "mod" e1 e2 }
504

    
505
/* If */
506
| IF e=expr THEN t=expr ELSE f=expr { mkexpr $sloc (Expr_ite (e, t, f)) }
507

    
508
signed_const:
509
| c=INT
510
  { Const_int c }
511
| c=REAL
512
  { Const_real c }
513
/* | c=FLOAT { Const_float c } */
514
| t=tag_ident { Const_tag t }
515
| MINUS c=INT
516
  { Const_int (-1 * c) }
517
| MINUS c=REAL
518
  { Const_real (Real.uminus c) }
519
/* | MINUS c=FLOAT { Const_float (-1. *. c) } */
520
| LCUR
521
  cs=separated_nonempty_list(COMMA, separated_pair(IDENT, EQ, signed_const))
522
  RCUR
523
  { Const_struct cs }
524
| LBRACKET cs=separated_nonempty_list(COMMA, signed_const) RBRACKET
525
  { Const_array cs }
526

    
527
dim:
528
| i=INT                      { mkdim_int $sloc i }
529
| LPAR d=dim RPAR            { d }
530
| x=ident                    { mkdim_ident $sloc x }
531
| d1=dim AND d2=dim          { mkdim_appl_b $sloc "&&" d1 d2 }
532
| d1=dim AMPERAMPER d2=dim   { mkdim_appl_b $sloc "&&" d1 d2 }
533
| d1=dim OR d2=dim           { mkdim_appl_b $sloc "||" d1 d2 }
534
| d1=dim BARBAR d2=dim       { mkdim_appl_b $sloc "||" d1 d2 }
535
| d1=dim XOR d2=dim          { mkdim_appl_b $sloc "xor" d1 d2 }
536
| NOT d=dim                  { mkdim_appl_u $sloc "not" d }
537
| d1=dim IMPL d2=dim         { mkdim_appl_b $sloc "impl" d1 d2 }
538

    
539
/* Comparison dim */                      
540
| d1=dim EQ d2=dim           { mkdim_appl_b $sloc "=" d1 d2 }
541
| d1=dim LT d2=dim           { mkdim_appl_b $sloc "<" d1 d2 }
542
| d1=dim LTE d2=dim          { mkdim_appl_b $sloc "<=" d1 d2 }
543
| d1=dim GT d2=dim           { mkdim_appl_b $sloc ">" d1 d2 }
544
| d1=dim GTE  d2=dim         { mkdim_appl_b $sloc ">=" d1 d2 }
545
| d1=dim NEQ d2=dim          { mkdim_appl_b $sloc "!=" d1 d2 }
546

    
547
/* Arithmetic dim */                    
548
| d1=dim PLUS d2=dim         { mkdim_appl_b $sloc "+" d1 d2 }
549
| d1=dim MINUS d2=dim        { mkdim_appl_b $sloc "-" d1 d2 }
550
| d1=dim MULT d2=dim         { mkdim_appl_b $sloc "*" d1 d2 }
551
| d1=dim DIV d2=dim          { mkdim_appl_b $sloc "/" d1 d2 }
552
| MINUS d=dim %prec p_uminus { mkdim_appl_u $sloc "uminus" d }
553
| d1=dim MOD d2=dim          { mkdim_appl_b $sloc "mod" d1 d2 }
554

    
555
/* If */
556
| IF d=dim THEN t=dim ELSE f=dim { mkdim_ite $sloc d t f }
557

    
558
%inline locals:
559
| xs=loption(preceded(VAR, var_decl_list(local_vdecl))) { xs }
560

    
561
var_decl_list(X):
562
| d=X ioption(SCOL)            { d }
563
| d=X SCOL ds=var_decl_list(X) { d @ ds }
564

    
565
vdecl:
566
| xs=ident_list COL t=typeconst c=clock?
567
  { mkvdecls false (Some t) c None xs }
568
| CONST xs=ident_list t=preceded(COL, typeconst)?
569
  /* static parameters don't have clocks */
570
  { mkvdecls true t None None xs }
571

    
572
local_vdecl:
573
| xs=ident_list /* Useless no ?*/
574
  { mkvdecls false None None None xs }
575
| xs=ident_list COL t=typeconst c=clock?
576
  { mkvdecls false (Some t) c None xs }
577
| CONST x=vdecl_ident t=preceded(COL, typeconst)? EQ e=expr
578
  /* static parameters don't have clocks */
579
  { mkvdecls true t None (Some e) [x] }
580

    
581
cdecl:
582
| x=const_ident EQ c=signed_const
583
  { fun itf ->
584
    let c = mktop_decl $sloc itf (Const {
585
                                      const_id = x;
586
                                      const_loc = $sloc;
587
                                      const_type = Types.new_var ();
588
                                      const_value = c
589
                          })
590
    in
591
    (*add_const itf $1 c;*)
592
    c
593
  }
594

    
595
%inline clock:
596
| l=when_cond+ { mkclock $sloc (Ckdec_bool l) }
597

    
598
when_cond:
599
| WHEN x=IDENT                       { x, tag_true }
600
| WHENNOT x=IDENT                    { x, tag_false }
601
| WHEN t=tag_ident LPAR x=IDENT RPAR { x, t }
602

    
603
%inline ident_list:
604
| ds=separated_nonempty_list(COMMA, vdecl_ident) { ds }
605

    
606
lustre_annot:
607
| annots=lustre_annot_list EOF { { annots; annot_loc = $sloc } }
608

    
609
lustre_annot_list:
610
  { [] } 
611
| k=kwd COL e=qexpr SCOL anns=lustre_annot_list     { (k, e) :: anns }
612
| x=IDENT COL e=qexpr SCOL anns=lustre_annot_list   { ([x], e) :: anns }
613
| INVARIANT COL e=qexpr SCOL anns=lustre_annot_list { (["invariant"], e) :: anns }
614
// (* | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } *)
615
| CCODE COL e=qexpr SCOL anns=lustre_annot_list     { (["c_code"], e) :: anns }
616
| MATLAB COL e=qexpr SCOL anns=lustre_annot_list    { (["matlab"], e) :: anns }
617

    
618

    
619
kwd:
620
| DIV               { [] }
621
| DIV x=IDENT k=kwd { x :: k }
622

    
623
%%
624
(* Local Variables: *)
625
(* compile-command:"make -C .." *)
626
(* End: *)
627

    
628

    
(8-8/8)