Project

General

Profile

Download (21.1 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 BY
85
%token <int> KINDUCTION
86
%token EOF
87

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

    
108
%start <Lustre_types.top_decl list> prog
109

    
110
%start <Lustre_types.top_decl list> header
111

    
112
%start <Lustre_types.expr_annot> lustre_annot
113

    
114
%start <Lustre_types.spec_types> lustre_spec
115

    
116
%%
117

    
118
ident:
119
| x=UIDENT { x }
120
| x=IDENT  { x }
121

    
122
module_ident:
123
| m=ident { m }
124

    
125
file_ident:
126
| m=module_ident                    { m }
127
| m=module_ident POINT f=file_ident { m ^ "." ^ f }
128

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

    
135
tag_bool:
136
| TRUE  { tag_true }
137
| FALSE { tag_false }
138

    
139
tag_ident:
140
| t=UIDENT   { t }
141
| t=tag_bool { t }
142

    
143
node_ident:
144
| n=ident { n }
145

    
146
node_ident_decl:
147
| n=node_ident { push_node n }
148

    
149
vdecl_ident:
150
| x=ident { mkident $sloc x }
151

    
152
const_ident:
153
| c=ident { c }
154

    
155
type_ident:
156
| t=IDENT { t }
157

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

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

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

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

    
174
state_annot:
175
| FUNCTION { true }
176
| NODE     { false }
177

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

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

    
251
nodespecs:
252
| ss=nodespec_list
253
  { match ss with
254
    | None   -> None
255
    | Some c -> Some (Contract c)
256
  }
257

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

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

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

    
284
%inline array_typ_decl:
285
|                          { [] }
286
| ds=preceded(POWER, dim)+ { ds }
287

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

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

    
316
automaton:
317
| AUTOMATON t=type_ident hs=handler* { Automata.mkautomata $sloc t hs }
318

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

    
323
unless:
324
| UNLESS e=expr RESTART s=UIDENT { $sloc, e, true, s  }
325
| UNLESS e=expr RESUME s=UIDENT  { $sloc, e, false, s }
326

    
327
until:
328
| UNTIL e=expr RESTART s=UIDENT { $sloc, e, true, s }
329
| UNTIL e=expr RESUME s=UIDENT  { $sloc, e, false, s }
330

    
331
assert_:
332
| ASSERT e=expr SCOL { mkassert $sloc e }
333

    
334
eq:
335
| xs=pattern EQ e=expr SCOL {mkeq $sloc (List.map fst xs, e)}
336

    
337
%inline pattern:
338
| xs=ident_list           { xs }
339
| LPAR xs=ident_list RPAR { xs }
340

    
341
lustre_spec:
342
| cs=top_contract+ EOF             { TopContract cs }
343
| CONTRACT? c=contract_content EOF { LocalContract c }
344

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

    
375
proof_annotation:
376
| BY k=KINDUCTION { Kinduction k }
377

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

    
399
%inline expr_or_tuple:
400
| e=expr                     { e }
401
| e=expr COMMA es=array_expr { mkexpr $sloc (Expr_tuple (e :: es)) }
402

    
403
mode_content:
404
| { [], [] }
405
| REQUIRE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
406
  { let (r, e) = mc in
407
    { qe with eexpr_name } :: r, e }
408
| ENSURE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
409
  { let (r, e) = mc in
410
    r, { qe with eexpr_name } :: e }
411

    
412
(* /* WARNING: UNUSED RULES */
413
 * tuple_qexpr:
414
 * | qexpr COMMA qexpr {[$3;$1]}
415
 * | tuple_qexpr COMMA qexpr {$3::$1} *)
416

    
417
qexpr:
418
| e=expr                      { mkeexpr $sloc e }
419
  /* Quantifiers */
420
| EXISTS x=vdecl SCOL e=qexpr { extend_eexpr [Exists, x] e }
421
| FORALL x=vdecl SCOL e=qexpr { extend_eexpr [Forall, x] e }
422

    
423
(* %inline tuple_expr:
424
 * | e=expr COMMA es=array_expr { e :: es } *)
425

    
426
// Same as tuple expr but accepting lists with single element
427
%inline array_expr:
428
| es=separated_nonempty_list(COMMA, expr) { es }
429

    
430
expr:
431
/* constants */
432
| c=INT                   { mkexpr $sloc (Expr_const (Const_int c)) }
433
| c=REAL                  { mkexpr $sloc (Expr_const (Const_real c)) }
434
| c=STRING %prec p_string { mkexpr $sloc (Expr_const (Const_string c)) }
435
| COLCOL c=IDENT          { mkexpr $sloc (Expr_const (Const_modeid c)) }
436
/* | c=FLOAT { mkexpr $sloc (Expr_const (Const_float c)) }*/
437

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

    
447
/* Array expressions */
448
| LBRACKET es=array_expr RBRACKET
449
  { mkexpr $sloc (Expr_array es) }
450
| e=expr POWER d=dim
451
  { mkexpr $sloc (Expr_power (e, d)) }
452
| e=expr ds=delimited(LBRACKET, dim, RBRACKET)+
453
  { List.fold_left (fun base d -> mkexpr $sloc (Expr_access (base, d))) e ds }
454

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

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

    
486
/* Boolean expr */
487
| e1=expr AND e2=expr         { mkpredef_call_b $sloc "&&" e1 e2 }
488
| e1=expr AMPERAMPER e2=expr  { mkpredef_call_b $sloc "&&" e1 e2 }
489
| e1=expr OR e2=expr          { mkpredef_call_b $sloc "||" e1 e2 }
490
| e1=expr BARBAR e2=expr      { mkpredef_call_b $sloc "||" e1 e2 }
491
| e1=expr XOR e2=expr         { mkpredef_call_b $sloc "xor" e1 e2 }
492
| NOT e=expr                  { mkpredef_call_u $sloc "not" e }
493
| e1=expr IMPL e2=expr        { mkpredef_call_b $sloc "impl" e1 e2 }
494

    
495
/* Comparison expr */
496
| e1=expr EQ e2=expr          { mkpredef_call_b $sloc "=" e1 e2 }
497
| e1=expr LT e2=expr          { mkpredef_call_b $sloc "<" e1 e2 }
498
| e1=expr LTE e2=expr         { mkpredef_call_b $sloc "<=" e1 e2 }
499
| e1=expr GT e2=expr          { mkpredef_call_b $sloc ">" e1 e2 }
500
| e1=expr GTE e2=expr         { mkpredef_call_b $sloc ">=" e1 e2 }
501
| e1=expr NEQ e2=expr         { mkpredef_call_b $sloc "!=" e1 e2 }
502

    
503
/* Arithmetic expr */
504
| e1=expr PLUS e2=expr        { mkpredef_call_b $sloc "+" e1 e2 }
505
| e1=expr MINUS e2=expr       { mkpredef_call_b $sloc "-" e1 e2 }
506
| e1=expr MULT e2=expr        { mkpredef_call_b $sloc "*" e1 e2 }
507
| e1=expr DIV e2=expr         { mkpredef_call_b $sloc "/" e1 e2 }
508
| MINUS e=expr %prec p_uminus { mkpredef_call_u $sloc "uminus" e }
509
| e1=expr MOD e2=expr         { mkpredef_call_b $sloc "mod" e1 e2 }
510

    
511
/* If */
512
| IF e=expr THEN t=expr ELSE f=expr { mkexpr $sloc (Expr_ite (e, t, f)) }
513

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

    
533
dim:
534
| i=INT                      { mkdim_int $sloc i }
535
| LPAR d=dim RPAR            { d }
536
| x=ident                    { mkdim_ident $sloc x }
537
| d1=dim AND d2=dim          { mkdim_appl_b $sloc "&&" d1 d2 }
538
| d1=dim AMPERAMPER d2=dim   { mkdim_appl_b $sloc "&&" d1 d2 }
539
| d1=dim OR d2=dim           { mkdim_appl_b $sloc "||" d1 d2 }
540
| d1=dim BARBAR d2=dim       { mkdim_appl_b $sloc "||" d1 d2 }
541
| d1=dim XOR d2=dim          { mkdim_appl_b $sloc "xor" d1 d2 }
542
| NOT d=dim                  { mkdim_appl_u $sloc "not" d }
543
| d1=dim IMPL d2=dim         { mkdim_appl_b $sloc "impl" d1 d2 }
544

    
545
/* Comparison dim */                      
546
| d1=dim EQ d2=dim           { mkdim_appl_b $sloc "=" d1 d2 }
547
| d1=dim LT d2=dim           { mkdim_appl_b $sloc "<" d1 d2 }
548
| d1=dim LTE d2=dim          { mkdim_appl_b $sloc "<=" d1 d2 }
549
| d1=dim GT d2=dim           { mkdim_appl_b $sloc ">" d1 d2 }
550
| d1=dim GTE  d2=dim         { mkdim_appl_b $sloc ">=" d1 d2 }
551
| d1=dim NEQ d2=dim          { mkdim_appl_b $sloc "!=" d1 d2 }
552

    
553
/* Arithmetic dim */                    
554
| d1=dim PLUS d2=dim         { mkdim_appl_b $sloc "+" d1 d2 }
555
| d1=dim MINUS d2=dim        { mkdim_appl_b $sloc "-" d1 d2 }
556
| d1=dim MULT d2=dim         { mkdim_appl_b $sloc "*" d1 d2 }
557
| d1=dim DIV d2=dim          { mkdim_appl_b $sloc "/" d1 d2 }
558
| MINUS d=dim %prec p_uminus { mkdim_appl_u $sloc "uminus" d }
559
| d1=dim MOD d2=dim          { mkdim_appl_b $sloc "mod" d1 d2 }
560

    
561
/* If */
562
| IF d=dim THEN t=dim ELSE f=dim { mkdim_ite $sloc d t f }
563

    
564
%inline locals:
565
| xs=loption(preceded(VAR, var_decl_list(local_vdecl))) { xs }
566

    
567
var_decl_list(X):
568
| d=X ioption(SCOL)            { d }
569
| d=X SCOL ds=var_decl_list(X) { d @ ds }
570

    
571
vdecl:
572
| xs=ident_list COL t=typeconst c=clock?
573
  { mkvdecls false (Some t) c None xs }
574
| CONST xs=ident_list t=preceded(COL, typeconst)?
575
  /* static parameters don't have clocks */
576
  { mkvdecls true t None None xs }
577

    
578
local_vdecl:
579
| xs=ident_list /* Useless no ?*/
580
  { mkvdecls false None None None xs }
581
| xs=ident_list COL t=typeconst c=clock?
582
  { mkvdecls false (Some t) c None xs }
583
| CONST x=vdecl_ident t=preceded(COL, typeconst)? EQ e=expr
584
  /* static parameters don't have clocks */
585
  { mkvdecls true t None (Some e) [x] }
586

    
587
cdecl:
588
| x=const_ident EQ c=signed_const
589
  { fun itf ->
590
    let c = mktop_decl $sloc itf (Const {
591
                                      const_id = x;
592
                                      const_loc = $sloc;
593
                                      const_type = Types.new_var ();
594
                                      const_value = c
595
                          })
596
    in
597
    (*add_const itf $1 c;*)
598
    c
599
  }
600

    
601
%inline clock:
602
| l=when_cond+ { mkclock $sloc (Ckdec_bool l) }
603

    
604
when_cond:
605
| WHEN x=IDENT                       { x, tag_true }
606
| WHENNOT x=IDENT                    { x, tag_false }
607
| WHEN t=tag_ident LPAR x=IDENT RPAR { x, t }
608

    
609
%inline ident_list:
610
| ds=separated_nonempty_list(COMMA, vdecl_ident) { ds }
611

    
612
lustre_annot:
613
| annots=lustre_annot_list EOF { { annots; annot_loc = $sloc } }
614

    
615
lustre_annot_list:
616
  { [] } 
617
| k=kwd COL e=qexpr SCOL anns=lustre_annot_list     { (k, e) :: anns }
618
| x=IDENT COL e=qexpr SCOL anns=lustre_annot_list   { ([x], e) :: anns }
619
| INVARIANT COL e=qexpr SCOL anns=lustre_annot_list { (["invariant"], e) :: anns }
620
// (* | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } *)
621
| CCODE COL e=qexpr SCOL anns=lustre_annot_list     { (["c_code"], e) :: anns }
622
| MATLAB COL e=qexpr SCOL anns=lustre_annot_list    { (["matlab"], e) :: anns }
623

    
624

    
625
kwd:
626
| DIV               { [] }
627
| DIV x=IDENT k=kwd { x :: k }
628

    
629
%%
630
(* Local Variables: *)
631
(* compile-command:"make -C .." *)
632
(* End: *)
633

    
634

    
(9-9/9)