lustrec / src / parser_lustre.mly @ 2823bc51
History | View | Annotate | Download (18.1 KB)
1 | 70e1006b | xthirioux | /********************************************************************/ |
---|---|---|---|
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 LustreSpec |
||
15 | open Corelang |
||
16 | open Dimension |
||
17 | open Parse |
||
18 | |||
19 | let get_loc () = Location.symbol_rloc () |
||
20 | |||
21 | 53206908 | xthirioux | let mkident x = x, get_loc () |
22 | 70e1006b | xthirioux | let mktyp x = mktyp (get_loc ()) x |
23 | let mkclock x = mkclock (get_loc ()) x |
||
24 | 53206908 | xthirioux | let mkvar_decl x loc = mkvar_decl loc ~orig:true x |
25 | 70e1006b | xthirioux | let mkexpr x = mkexpr (get_loc ()) x |
26 | let mkeexpr x = mkeexpr (get_loc ()) x |
||
27 | let mkeq x = mkeq (get_loc ()) x |
||
28 | let mkassert x = mkassert (get_loc ()) x |
||
29 | let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x |
||
30 | let mkpredef_call x = mkpredef_call (get_loc ()) x |
||
31 | (*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*) |
||
32 | |||
33 | let mkdim_int i = mkdim_int (get_loc ()) i |
||
34 | let mkdim_bool b = mkdim_bool (get_loc ()) b |
||
35 | let mkdim_ident id = mkdim_ident (get_loc ()) id |
||
36 | let mkdim_appl f args = mkdim_appl (get_loc ()) f args |
||
37 | let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e |
||
38 | |||
39 | let mkannots annots = { annots = annots; annot_loc = get_loc () } |
||
40 | |||
41 | 6394042a | ploc | 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 |
||
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 | e0523910 | ploc | let rec fby expr n init = |
48 | if n<=1 then |
||
49 | mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr))) |
||
50 | else |
||
51 | mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init)))) |
||
52 | |||
53 | 70e1006b | xthirioux | %} |
54 | |||
55 | %token <int> INT |
||
56 | 53206908 | xthirioux | %token <Num.num * int * string> REAL |
57 | |||
58 | 70e1006b | xthirioux | %token <string> STRING |
59 | %token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |
||
60 | %token STATELESS ASSERT OPEN QUOTE FUNCTION |
||
61 | %token <string> IDENT |
||
62 | %token <string> UIDENT |
||
63 | %token TRUE FALSE |
||
64 | %token <LustreSpec.expr_annot> ANNOT |
||
65 | %token <LustreSpec.node_annot> NODESPEC |
||
66 | %token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL |
||
67 | %token AMPERAMPER BARBAR NOT POWER |
||
68 | %token IF THEN ELSE |
||
69 | %token UCLOCK DCLOCK PHCLOCK TAIL |
||
70 | %token MERGE FBY WHEN WHENNOT EVERY |
||
71 | %token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST |
||
72 | %token STRUCT ENUM |
||
73 | 53206908 | xthirioux | %token TINT TREAL TBOOL TCLOCK |
74 | 70e1006b | xthirioux | %token RATE DUE |
75 | %token EQ LT GT LTE GTE NEQ |
||
76 | %token AND OR XOR IMPL |
||
77 | %token MULT DIV MOD |
||
78 | %token MINUS PLUS UMINUS |
||
79 | %token PRE ARROW |
||
80 | %token REQUIRES ENSURES OBSERVER |
||
81 | 85da3a4b | ploc | %token INVARIANT BEHAVIOR ASSUMES CCODE MATLAB |
82 | 70e1006b | xthirioux | %token EXISTS FORALL |
83 | %token PROTOTYPE LIB |
||
84 | %token EOF |
||
85 | |||
86 | %nonassoc prec_exists prec_forall |
||
87 | %nonassoc COMMA |
||
88 | 01d48bb0 | xthirioux | %nonassoc EVERY |
89 | 70e1006b | xthirioux | %left MERGE IF |
90 | %nonassoc ELSE |
||
91 | %right ARROW FBY |
||
92 | %left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK |
||
93 | %right COLCOL |
||
94 | %right IMPL |
||
95 | %left OR XOR BARBAR |
||
96 | %left AND AMPERAMPER |
||
97 | %left NOT |
||
98 | %nonassoc INT |
||
99 | %nonassoc EQ LT GT LTE GTE NEQ |
||
100 | %left MINUS PLUS |
||
101 | %left MULT DIV MOD |
||
102 | %left UMINUS |
||
103 | %left POWER |
||
104 | %left PRE LAST |
||
105 | %nonassoc RBRACKET |
||
106 | %nonassoc LBRACKET |
||
107 | |||
108 | %start prog |
||
109 | %type <LustreSpec.top_decl list> prog |
||
110 | |||
111 | %start header |
||
112 | %type <LustreSpec.top_decl list> header |
||
113 | |||
114 | %start lustre_annot |
||
115 | %type <LustreSpec.expr_annot> lustre_annot |
||
116 | |||
117 | %start lustre_spec |
||
118 | %type <LustreSpec.node_annot> lustre_spec |
||
119 | |||
120 | 53206908 | xthirioux | %start signed_const |
121 | %type <LustreSpec.constant> signed_const |
||
122 | |||
123 | 70e1006b | xthirioux | %% |
124 | |||
125 | module_ident: |
||
126 | UIDENT { $1 } |
||
127 | | IDENT { $1 } |
||
128 | |||
129 | tag_ident: |
||
130 | UIDENT { $1 } |
||
131 | | TRUE { tag_true } |
||
132 | | FALSE { tag_false } |
||
133 | |||
134 | node_ident: |
||
135 | UIDENT { $1 } |
||
136 | | IDENT { $1 } |
||
137 | |||
138 | 6394042a | ploc | node_ident_decl: |
139 | node_ident { push_node $1; $1 } |
||
140 | |||
141 | 70e1006b | xthirioux | vdecl_ident: |
142 | 53206908 | xthirioux | UIDENT { mkident $1 } |
143 | | IDENT { mkident $1 } |
||
144 | 70e1006b | xthirioux | |
145 | const_ident: |
||
146 | UIDENT { $1 } |
||
147 | | IDENT { $1 } |
||
148 | |||
149 | type_ident: |
||
150 | IDENT { $1 } |
||
151 | |||
152 | prog: |
||
153 | open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) } |
||
154 | |||
155 | typ_def_prog: |
||
156 | typ_def_list { $1 false } |
||
157 | |||
158 | header: |
||
159 | open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) } |
||
160 | |||
161 | typ_def_header: |
||
162 | typ_def_list { $1 true } |
||
163 | |||
164 | open_list: |
||
165 | { [] } |
||
166 | | open_lusi open_list { $1 :: $2 } |
||
167 | |||
168 | open_lusi: |
||
169 | | OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))} |
||
170 | | OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) } |
||
171 | |||
172 | top_decl_list: |
||
173 | {[]} |
||
174 | | top_decl_list top_decl {$2@$1} |
||
175 | |||
176 | |||
177 | top_decl_header_list: |
||
178 | { [] } |
||
179 | | top_decl_header_list top_decl_header { $2@$1 } |
||
180 | |||
181 | state_annot: |
||
182 | FUNCTION { true } |
||
183 | | NODE { false } |
||
184 | |||
185 | top_decl_header: |
||
186 | | CONST cdecl_list { List.rev ($2 true) } |
||
187 | 53206908 | xthirioux | | nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL |
188 | 70e1006b | xthirioux | {let nd = mktop_decl true (ImportedNode |
189 | {nodei_id = $3; |
||
190 | nodei_type = Types.new_var (); |
||
191 | nodei_clock = Clocks.new_var true; |
||
192 | nodei_inputs = List.rev $5; |
||
193 | nodei_outputs = List.rev $10; |
||
194 | nodei_stateless = $2; |
||
195 | nodei_spec = $1; |
||
196 | nodei_prototype = $13; |
||
197 | nodei_in_lib = $14;}) |
||
198 | in |
||
199 | (*add_imported_node $3 nd;*) [nd] } |
||
200 | |||
201 | prototype_opt: |
||
202 | { None } |
||
203 | | PROTOTYPE node_ident { Some $2} |
||
204 | |||
205 | 53206908 | xthirioux | in_lib_list: |
206 | { [] } |
||
207 | | LIB module_ident in_lib_list { $2::$3 } |
||
208 | 70e1006b | xthirioux | |
209 | top_decl: |
||
210 | | CONST cdecl_list { List.rev ($2 false) } |
||
211 | 6394042a | ploc | | nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL |
212 | { |
||
213 | 85da3a4b | ploc | let stmts, asserts, annots = $16 in |
214 | 6394042a | ploc | (* Declaring eqs annots *) |
215 | List.iter (fun ann -> |
||
216 | List.iter (fun (key, _) -> |
||
217 | Annotations.add_node_ann $3 key |
||
218 | ) ann.annots |
||
219 | ) annots; |
||
220 | (* Building the node *) |
||
221 | 85da3a4b | ploc | let nd = mktop_decl false (Node |
222 | {node_id = $3; |
||
223 | node_type = Types.new_var (); |
||
224 | node_clock = Clocks.new_var true; |
||
225 | node_inputs = List.rev $5; |
||
226 | node_outputs = List.rev $10; |
||
227 | node_locals = List.rev $14; |
||
228 | node_gencalls = []; |
||
229 | node_checks = []; |
||
230 | node_asserts = asserts; |
||
231 | node_stmts = stmts; |
||
232 | node_dec_stateless = $2; |
||
233 | node_stateless = None; |
||
234 | node_spec = $1; |
||
235 | node_annot = annots}) |
||
236 | in |
||
237 | pop_node (); |
||
238 | 70e1006b | xthirioux | (*add_node $3 nd;*) [nd] } |
239 | 53206908 | xthirioux | |
240 | nodespec_list: |
||
241 | 70e1006b | xthirioux | { None } |
242 | | NODESPEC nodespec_list { |
||
243 | (function |
||
244 | | None -> (fun s1 -> Some s1) |
||
245 | | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 } |
||
246 | |||
247 | typ_def_list: |
||
248 | /* empty */ { (fun itf -> []) } |
||
249 | | typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) } |
||
250 | |||
251 | typ_def: |
||
252 | TYPE type_ident EQ typ_def_rhs { (fun itf -> |
||
253 | let typ = mktop_decl itf (TypeDef { tydef_id = $2; |
||
254 | tydef_desc = $4 |
||
255 | }) |
||
256 | in (*add_type itf $2 typ;*) typ) } |
||
257 | |||
258 | typ_def_rhs: |
||
259 | typeconst { $1 } |
||
260 | | ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) } |
||
261 | | STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) } |
||
262 | |||
263 | array_typ_decl: |
||
264 | 79614a15 | xthirioux | %prec POWER { fun typ -> typ } |
265 | 70e1006b | xthirioux | | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) } |
266 | |||
267 | typeconst: |
||
268 | TINT array_typ_decl { $2 Tydec_int } |
||
269 | | TBOOL array_typ_decl { $2 Tydec_bool } |
||
270 | | TREAL array_typ_decl { $2 Tydec_real } |
||
271 | 53206908 | xthirioux | /* | TFLOAT array_typ_decl { $2 Tydec_float } */ |
272 | 70e1006b | xthirioux | | type_ident array_typ_decl { $2 (Tydec_const $1) } |
273 | | TBOOL TCLOCK { Tydec_clock Tydec_bool } |
||
274 | | IDENT TCLOCK { Tydec_clock (Tydec_const $1) } |
||
275 | |||
276 | tag_list: |
||
277 | UIDENT { $1 :: [] } |
||
278 | | tag_list COMMA UIDENT { $3 :: $1 } |
||
279 | |||
280 | field_list: { [] } |
||
281 | | field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } |
||
282 | |||
283 | 1eda3e78 | xthirioux | stmt_list: |
284 | 70e1006b | xthirioux | { [], [], [] } |
285 | 1eda3e78 | xthirioux | | eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl} |
286 | | assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl} |
||
287 | | ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl} |
||
288 | | automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl} |
||
289 | 70e1006b | xthirioux | |
290 | automaton: |
||
291 | bc7b6c62 | xthirioux | AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 } |
292 | 70e1006b | xthirioux | |
293 | handler_list: |
||
294 | { [] } |
||
295 | | handler handler_list { $1::$2 } |
||
296 | |||
297 | handler: |
||
298 | 6a1a01d2 | xthirioux | STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 } |
299 | 70e1006b | xthirioux | |
300 | unless_list: |
||
301 | 29ced7be | xthirioux | { [] } |
302 | | unless unless_list { $1::$2 } |
||
303 | 70e1006b | xthirioux | |
304 | until_list: |
||
305 | 29ced7be | xthirioux | { [] } |
306 | | until until_list { $1::$2 } |
||
307 | 70e1006b | xthirioux | |
308 | unless: |
||
309 | 29ced7be | xthirioux | UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4) } |
310 | | UNLESS expr RESUME UIDENT { (get_loc (), $2, false, $4) } |
||
311 | 70e1006b | xthirioux | |
312 | until: |
||
313 | 29ced7be | xthirioux | UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4) } |
314 | | UNTIL expr RESUME UIDENT { (get_loc (), $2, false, $4) } |
||
315 | 70e1006b | xthirioux | |
316 | assert_: |
||
317 | | ASSERT expr SCOL {mkassert ($2)} |
||
318 | |||
319 | eq: |
||
320 | 53206908 | xthirioux | ident_list EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)} |
321 | | LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)} |
||
322 | 70e1006b | xthirioux | |
323 | lustre_spec: |
||
324 | | contract EOF { $1 } |
||
325 | |||
326 | contract: |
||
327 | requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } } |
||
328 | |||
329 | requires: |
||
330 | { [] } |
||
331 | | REQUIRES qexpr SCOL requires { $2::$4 } |
||
332 | |||
333 | ensures: |
||
334 | { [] } |
||
335 | | ENSURES qexpr SCOL ensures { $2 :: $4 } |
||
336 | | OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures { |
||
337 | mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7 |
||
338 | } |
||
339 | |||
340 | behaviors: |
||
341 | { [] } |
||
342 | | BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 } |
||
343 | |||
344 | assumes: |
||
345 | { [] } |
||
346 | | ASSUMES qexpr SCOL assumes { $2::$4 } |
||
347 | |||
348 | /* WARNING: UNUSED RULES */ |
||
349 | tuple_qexpr: |
||
350 | | qexpr COMMA qexpr {[$3;$1]} |
||
351 | | tuple_qexpr COMMA qexpr {$3::$1} |
||
352 | |||
353 | qexpr: |
||
354 | | expr { mkeexpr $1 } |
||
355 | /* Quantifiers */ |
||
356 | | EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 } |
||
357 | | FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 } |
||
358 | |||
359 | |||
360 | tuple_expr: |
||
361 | expr COMMA expr {[$3;$1]} |
||
362 | | tuple_expr COMMA expr {$3::$1} |
||
363 | |||
364 | // Same as tuple expr but accepting lists with single element |
||
365 | array_expr: |
||
366 | expr {[$1]} |
||
367 | | expr COMMA array_expr {$1::$3} |
||
368 | |||
369 | dim_list: |
||
370 | dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) } |
||
371 | | dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) } |
||
372 | |||
373 | expr: |
||
374 | /* constants */ |
||
375 | INT {mkexpr (Expr_const (Const_int $1))} |
||
376 | 53206908 | xthirioux | | REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))} |
377 | /* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/ |
||
378 | 70e1006b | xthirioux | /* Idents or type enum tags */ |
379 | | IDENT { mkexpr (Expr_ident $1) } |
||
380 | | tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) } |
||
381 | | LPAR ANNOT expr RPAR |
||
382 | 6394042a | ploc | {update_expr_annot (get_current_node ()) $3 $2} |
383 | 70e1006b | xthirioux | | LPAR expr RPAR |
384 | {$2} |
||
385 | | LPAR tuple_expr RPAR |
||
386 | {mkexpr (Expr_tuple (List.rev $2))} |
||
387 | |||
388 | /* Array expressions */ |
||
389 | | LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) } |
||
390 | | expr POWER dim { mkexpr (Expr_power ($1, $3)) } |
||
391 | | expr LBRACKET dim_list { $3 $1 } |
||
392 | |||
393 | /* Temporal operators */ |
||
394 | | PRE expr |
||
395 | {mkexpr (Expr_pre $2)} |
||
396 | | expr ARROW expr |
||
397 | {mkexpr (Expr_arrow ($1,$3))} |
||
398 | | expr FBY expr |
||
399 | {(*mkexpr (Expr_fby ($1,$3))*) |
||
400 | mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))} |
||
401 | | expr WHEN vdecl_ident |
||
402 | 53206908 | xthirioux | {mkexpr (Expr_when ($1,fst $3,tag_true))} |
403 | 70e1006b | xthirioux | | expr WHENNOT vdecl_ident |
404 | 53206908 | xthirioux | {mkexpr (Expr_when ($1,fst $3,tag_false))} |
405 | 70e1006b | xthirioux | | expr WHEN tag_ident LPAR vdecl_ident RPAR |
406 | 53206908 | xthirioux | {mkexpr (Expr_when ($1, fst $5, $3))} |
407 | 70e1006b | xthirioux | | MERGE vdecl_ident handler_expr_list |
408 | 53206908 | xthirioux | {mkexpr (Expr_merge (fst $2,$3))} |
409 | 70e1006b | xthirioux | |
410 | /* Applications */ |
||
411 | | node_ident LPAR expr RPAR |
||
412 | {mkexpr (Expr_appl ($1, $3, None))} |
||
413 | 6a1a01d2 | xthirioux | | node_ident LPAR expr RPAR EVERY expr |
414 | {mkexpr (Expr_appl ($1, $3, Some $6))} |
||
415 | 70e1006b | xthirioux | | node_ident LPAR tuple_expr RPAR |
416 | 85da3a4b | ploc | { |
417 | let id=$1 in |
||
418 | let args=List.rev $3 in |
||
419 | match id, args with |
||
420 | | "fbyn", [expr;n;init] -> |
||
421 | let n = match n.expr_desc with |
||
422 | | Expr_const (Const_int n) -> n |
||
423 | | _ -> assert false |
||
424 | in |
||
425 | fby expr n init |
||
426 | | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None)) |
||
427 | } |
||
428 | 6a1a01d2 | xthirioux | | node_ident LPAR tuple_expr RPAR EVERY expr |
429 | 85da3a4b | ploc | { |
430 | let id=$1 in |
||
431 | let args=List.rev $3 in |
||
432 | let clock=$6 in |
||
433 | if id="fby" then |
||
434 | assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *) |
||
435 | else |
||
436 | mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) |
||
437 | } |
||
438 | 70e1006b | xthirioux | |
439 | /* Boolean expr */ |
||
440 | | expr AND expr |
||
441 | {mkpredef_call "&&" [$1;$3]} |
||
442 | | expr AMPERAMPER expr |
||
443 | {mkpredef_call "&&" [$1;$3]} |
||
444 | | expr OR expr |
||
445 | {mkpredef_call "||" [$1;$3]} |
||
446 | | expr BARBAR expr |
||
447 | {mkpredef_call "||" [$1;$3]} |
||
448 | | expr XOR expr |
||
449 | {mkpredef_call "xor" [$1;$3]} |
||
450 | | NOT expr |
||
451 | {mkpredef_call "not" [$2]} |
||
452 | | expr IMPL expr |
||
453 | {mkpredef_call "impl" [$1;$3]} |
||
454 | |||
455 | /* Comparison expr */ |
||
456 | | expr EQ expr |
||
457 | {mkpredef_call "=" [$1;$3]} |
||
458 | | expr LT expr |
||
459 | {mkpredef_call "<" [$1;$3]} |
||
460 | | expr LTE expr |
||
461 | {mkpredef_call "<=" [$1;$3]} |
||
462 | | expr GT expr |
||
463 | {mkpredef_call ">" [$1;$3]} |
||
464 | | expr GTE expr |
||
465 | {mkpredef_call ">=" [$1;$3]} |
||
466 | | expr NEQ expr |
||
467 | {mkpredef_call "!=" [$1;$3]} |
||
468 | |||
469 | /* Arithmetic expr */ |
||
470 | | expr PLUS expr |
||
471 | {mkpredef_call "+" [$1;$3]} |
||
472 | | expr MINUS expr |
||
473 | {mkpredef_call "-" [$1;$3]} |
||
474 | | expr MULT expr |
||
475 | {mkpredef_call "*" [$1;$3]} |
||
476 | | expr DIV expr |
||
477 | {mkpredef_call "/" [$1;$3]} |
||
478 | | MINUS expr %prec UMINUS |
||
479 | {mkpredef_call "uminus" [$2]} |
||
480 | | expr MOD expr |
||
481 | {mkpredef_call "mod" [$1;$3]} |
||
482 | |||
483 | /* If */ |
||
484 | | IF expr THEN expr ELSE expr |
||
485 | {mkexpr (Expr_ite ($2, $4, $6))} |
||
486 | |||
487 | handler_expr_list: |
||
488 | { [] } |
||
489 | | handler_expr handler_expr_list { $1 :: $2 } |
||
490 | |||
491 | handler_expr: |
||
492 | LPAR tag_ident ARROW expr RPAR { ($2, $4) } |
||
493 | |||
494 | signed_const_array: |
||
495 | | signed_const { [$1] } |
||
496 | | signed_const COMMA signed_const_array { $1 :: $3 } |
||
497 | |||
498 | signed_const_struct: |
||
499 | | IDENT EQ signed_const { [ ($1, $3) ] } |
||
500 | | IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 } |
||
501 | |||
502 | signed_const: |
||
503 | INT {Const_int $1} |
||
504 | 53206908 | xthirioux | | REAL {let c,e,s =$1 in Const_real (c,e,s)} |
505 | /* | FLOAT {Const_float $1} */ |
||
506 | 70e1006b | xthirioux | | tag_ident {Const_tag $1} |
507 | | MINUS INT {Const_int (-1 * $2)} |
||
508 | 53206908 | xthirioux | | MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)} |
509 | /* | MINUS FLOAT {Const_float (-1. *. $2)} */ |
||
510 | 70e1006b | xthirioux | | LCUR signed_const_struct RCUR { Const_struct $2 } |
511 | | LBRACKET signed_const_array RBRACKET { Const_array $2 } |
||
512 | |||
513 | dim: |
||
514 | INT { mkdim_int $1 } |
||
515 | | LPAR dim RPAR { $2 } |
||
516 | | UIDENT { mkdim_ident $1 } |
||
517 | | IDENT { mkdim_ident $1 } |
||
518 | | dim AND dim |
||
519 | {mkdim_appl "&&" [$1;$3]} |
||
520 | | dim AMPERAMPER dim |
||
521 | {mkdim_appl "&&" [$1;$3]} |
||
522 | | dim OR dim |
||
523 | {mkdim_appl "||" [$1;$3]} |
||
524 | | dim BARBAR dim |
||
525 | {mkdim_appl "||" [$1;$3]} |
||
526 | | dim XOR dim |
||
527 | {mkdim_appl "xor" [$1;$3]} |
||
528 | | NOT dim |
||
529 | {mkdim_appl "not" [$2]} |
||
530 | | dim IMPL dim |
||
531 | {mkdim_appl "impl" [$1;$3]} |
||
532 | |||
533 | /* Comparison dim */ |
||
534 | | dim EQ dim |
||
535 | {mkdim_appl "=" [$1;$3]} |
||
536 | | dim LT dim |
||
537 | {mkdim_appl "<" [$1;$3]} |
||
538 | | dim LTE dim |
||
539 | {mkdim_appl "<=" [$1;$3]} |
||
540 | | dim GT dim |
||
541 | {mkdim_appl ">" [$1;$3]} |
||
542 | | dim GTE dim |
||
543 | {mkdim_appl ">=" [$1;$3]} |
||
544 | | dim NEQ dim |
||
545 | {mkdim_appl "!=" [$1;$3]} |
||
546 | |||
547 | /* Arithmetic dim */ |
||
548 | | dim PLUS dim |
||
549 | {mkdim_appl "+" [$1;$3]} |
||
550 | | dim MINUS dim |
||
551 | {mkdim_appl "-" [$1;$3]} |
||
552 | | dim MULT dim |
||
553 | {mkdim_appl "*" [$1;$3]} |
||
554 | | dim DIV dim |
||
555 | {mkdim_appl "/" [$1;$3]} |
||
556 | | MINUS dim %prec UMINUS |
||
557 | {mkdim_appl "uminus" [$2]} |
||
558 | | dim MOD dim |
||
559 | {mkdim_appl "mod" [$1;$3]} |
||
560 | /* If */ |
||
561 | | IF dim THEN dim ELSE dim |
||
562 | {mkdim_ite $2 $4 $6} |
||
563 | |||
564 | locals: |
||
565 | {[]} |
||
566 | 01d48bb0 | xthirioux | | VAR local_vdecl_list SCOL {$2} |
567 | 70e1006b | xthirioux | |
568 | vdecl_list: |
||
569 | 01d48bb0 | xthirioux | vdecl {$1} |
570 | 70e1006b | xthirioux | | vdecl_list SCOL vdecl {$3 @ $1} |
571 | |||
572 | vdecl: |
||
573 | 01d48bb0 | xthirioux | ident_list COL typeconst clock |
574 | 53206908 | xthirioux | { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 } |
575 | 01d48bb0 | xthirioux | | CONST ident_list /* static parameters don't have clocks */ |
576 | 53206908 | xthirioux | { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None) loc) $2 } |
577 | 01d48bb0 | xthirioux | | CONST ident_list COL typeconst /* static parameters don't have clocks */ |
578 | 53206908 | xthirioux | { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None) loc) $2 } |
579 | 01d48bb0 | xthirioux | |
580 | local_vdecl_list: |
||
581 | local_vdecl {$1} |
||
582 | | local_vdecl_list SCOL local_vdecl {$3 @ $1} |
||
583 | 70e1006b | xthirioux | |
584 | 01d48bb0 | xthirioux | local_vdecl: |
585 | /* Useless no ?*/ ident_list |
||
586 | 53206908 | xthirioux | { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None) loc) $1 } |
587 | 70e1006b | xthirioux | | ident_list COL typeconst clock |
588 | 53206908 | xthirioux | { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 } |
589 | 01d48bb0 | xthirioux | | CONST vdecl_ident EQ expr /* static parameters don't have clocks */ |
590 | 85da3a4b | ploc | { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) loc] } |
591 | 01d48bb0 | xthirioux | | CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */ |
592 | 85da3a4b | ploc | { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6) loc] } |
593 | 70e1006b | xthirioux | |
594 | cdecl_list: |
||
595 | cdecl SCOL { (fun itf -> [$1 itf]) } |
||
596 | | cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) } |
||
597 | |||
598 | cdecl: |
||
599 | const_ident EQ signed_const { |
||
600 | (fun itf -> |
||
601 | let c = mktop_decl itf (Const { |
||
602 | const_id = $1; |
||
603 | const_loc = Location.symbol_rloc (); |
||
604 | const_type = Types.new_var (); |
||
605 | const_value = $3}) |
||
606 | in |
||
607 | (*add_const itf $1 c;*) c) |
||
608 | } |
||
609 | |||
610 | clock: |
||
611 | {mkclock Ckdec_any} |
||
612 | | when_list |
||
613 | {mkclock (Ckdec_bool (List.rev $1))} |
||
614 | |||
615 | when_cond: |
||
616 | WHEN IDENT {($2, tag_true)} |
||
617 | | WHENNOT IDENT {($2, tag_false)} |
||
618 | | WHEN tag_ident LPAR IDENT RPAR {($4, $2)} |
||
619 | |||
620 | when_list: |
||
621 | when_cond {[$1]} |
||
622 | | when_list when_cond {$2::$1} |
||
623 | |||
624 | ident_list: |
||
625 | vdecl_ident {[$1]} |
||
626 | | ident_list COMMA vdecl_ident {$3::$1} |
||
627 | |||
628 | SCOL_opt: |
||
629 | SCOL {} | {} |
||
630 | |||
631 | |||
632 | lustre_annot: |
||
633 | lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } } |
||
634 | |||
635 | lustre_annot_list: |
||
636 | { [] } |
||
637 | | kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 } |
||
638 | | IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 } |
||
639 | | INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 } |
||
640 | | OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 } |
||
641 | 85da3a4b | ploc | | CCODE COL qexpr SCOL lustre_annot_list{ (["c_code"],$3)::$5 } |
642 | | MATLAB COL qexpr SCOL lustre_annot_list{ (["matlab"],$3)::$5 } |
||
643 | |||
644 | 70e1006b | xthirioux | |
645 | kwd: |
||
646 | DIV { [] } |
||
647 | | DIV IDENT kwd { $2::$3} |
||
648 | |||
649 | %% |
||
650 | (* Local Variables: *) |
||
651 | (* compile-command:"make -C .." *) |
||
652 | (* End: *) |
||
653 | |||
654 |