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
|
|