14 |
14 |
open Lustre_types
|
15 |
15 |
open Corelang
|
16 |
16 |
open Dimension
|
17 |
|
open Parse
|
18 |
17 |
|
19 |
18 |
|
20 |
19 |
let get_loc () = Location.symbol_rloc ()
|
21 |
20 |
|
22 |
21 |
let mkident x = x, get_loc ()
|
23 |
|
let mktyp x = mktyp (get_loc ()) x
|
24 |
|
let mkclock x = mkclock (get_loc ()) x
|
|
22 |
let mktyp = mktyp (get_loc ())
|
|
23 |
let mkotyp x = match x with Some t -> Some (mktyp t) | None -> None
|
|
24 |
let mkclock = mkclock (get_loc ())
|
25 |
25 |
let mkvar_decl x loc = mkvar_decl loc ~orig:true x
|
26 |
|
let mkexpr x = mkexpr (get_loc ()) x
|
27 |
|
let mkeexpr x = mkeexpr (get_loc ()) x
|
28 |
|
let mkeq x = mkeq (get_loc ()) x
|
29 |
|
let mkassert x = mkassert (get_loc ()) x
|
30 |
|
let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x
|
31 |
|
let mkpredef_call x = mkpredef_call (get_loc ()) x
|
32 |
|
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
|
33 |
|
|
34 |
|
let mkdim_int i = mkdim_int (get_loc ()) i
|
35 |
|
let mkdim_bool b = mkdim_bool (get_loc ()) b
|
36 |
|
let mkdim_ident id = mkdim_ident (get_loc ()) id
|
37 |
|
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
|
38 |
|
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
|
39 |
|
|
40 |
|
let mkannots annots = { annots = annots; annot_loc = get_loc () }
|
|
26 |
let mkexpr = mkexpr (get_loc ())
|
|
27 |
let mkeexpr = mkeexpr (get_loc ())
|
|
28 |
let mkeq = mkeq (get_loc ())
|
|
29 |
let mkassert = mkassert (get_loc ())
|
|
30 |
let mktop_decl = mktop_decl (get_loc ()) (Location.get_module ())
|
|
31 |
let mkpredef_call = mkpredef_call (get_loc ())
|
|
32 |
let mkpredef_call_b f x1 x2 = mkpredef_call f [x1; x2]
|
|
33 |
let mkpredef_call_u f x = mkpredef_call f [x]
|
|
34 |
|
|
35 |
let mkdim_int = mkdim_int (get_loc ())
|
|
36 |
(* let mkdim_bool b = mkdim_bool (get_loc ()) b *)
|
|
37 |
let mkdim_ident = mkdim_ident (get_loc ())
|
|
38 |
let mkdim_appl = mkdim_appl (get_loc ())
|
|
39 |
let mkdim_appl_b f x1 x2 = mkdim_appl f [x1; x2]
|
|
40 |
let mkdim_appl_u f x = mkdim_appl f [x]
|
|
41 |
let mkdim_ite = mkdim_ite (get_loc ())
|
|
42 |
|
|
43 |
let mkarraytype = List.fold_left (fun t d -> Tydec_array (d, t))
|
|
44 |
|
|
45 |
let mkvdecls const typ clock expr =
|
|
46 |
List.map (fun (id, loc) ->
|
|
47 |
mkvar_decl (id,
|
|
48 |
mktyp (match typ with Some t -> t | None -> Tydec_any),
|
|
49 |
(match clock with Some ck -> ck | None -> mkclock Ckdec_any),
|
|
50 |
const, expr, None) loc)
|
|
51 |
|
|
52 |
(* let mkannots annots = { annots = annots; annot_loc = get_loc () } *)
|
41 |
53 |
|
42 |
54 |
let node_stack : ident list ref = ref []
|
43 |
|
let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack
|
44 |
|
let push_node nd = node_stack:= nd :: !node_stack
|
|
55 |
(* let debug_calls () = Format.eprintf "call stack: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) !node_stack *)
|
|
56 |
let push_node nd = node_stack := nd :: !node_stack; nd
|
45 |
57 |
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
|
46 |
58 |
let get_current_node () = try List.hd !node_stack with _ -> assert false
|
47 |
59 |
|
48 |
60 |
let rec fby expr n init =
|
49 |
|
if n<=1 then
|
|
61 |
if n <= 1 then
|
50 |
62 |
mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
|
51 |
63 |
else
|
52 |
|
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
|
|
64 |
mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n - 1) init))))
|
53 |
65 |
|
54 |
66 |
|
55 |
67 |
%}
|
... | ... | |
69 |
81 |
%token AMPERAMPER BARBAR NOT POWER
|
70 |
82 |
%token IF THEN ELSE
|
71 |
83 |
%token MERGE FBY WHEN WHENNOT EVERY
|
72 |
|
%token NODE LET TEL RETURNS VAR IMPORTED TYPE CONST
|
|
84 |
%token NODE LET TEL RETURNS VAR TYPE CONST
|
73 |
85 |
%token STRUCT ENUM
|
74 |
86 |
%token TINT TREAL TBOOL TCLOCK
|
75 |
87 |
%token EQ LT GT LTE GTE NEQ
|
76 |
88 |
%token AND OR XOR IMPL
|
77 |
89 |
%token MULT DIV MOD
|
78 |
|
%token MINUS PLUS UMINUS
|
|
90 |
%token MINUS PLUS
|
79 |
91 |
%token PRE ARROW
|
80 |
92 |
%token REQUIRE ENSURE ASSUME GUARANTEES IMPORT CONTRACT
|
81 |
93 |
%token INVARIANT MODE CCODE MATLAB
|
... | ... | |
83 |
95 |
%token PROTOTYPE LIB
|
84 |
96 |
%token EOF
|
85 |
97 |
|
86 |
|
%nonassoc prec_exists prec_forall
|
87 |
|
%nonassoc COMMA
|
|
98 |
%nonassoc p_string
|
|
99 |
%nonassoc p_vdecl
|
|
100 |
%left SCOL
|
88 |
101 |
%nonassoc EVERY
|
89 |
|
%left MERGE IF
|
90 |
102 |
%nonassoc ELSE
|
91 |
103 |
%right ARROW FBY
|
92 |
104 |
%left WHEN WHENNOT
|
93 |
|
%right COLCOL
|
94 |
105 |
%right IMPL
|
95 |
106 |
%left OR XOR BARBAR
|
96 |
107 |
%left AND AMPERAMPER
|
97 |
108 |
%left NOT
|
98 |
|
%nonassoc INT
|
99 |
109 |
%nonassoc EQ LT GT LTE GTE NEQ
|
100 |
110 |
%left MINUS PLUS
|
101 |
111 |
%left MULT DIV MOD
|
102 |
|
%left UMINUS
|
|
112 |
%left p_uminus
|
103 |
113 |
%left POWER
|
104 |
|
%left PRE LAST
|
|
114 |
%left PRE
|
105 |
115 |
%nonassoc RBRACKET
|
106 |
116 |
%nonassoc LBRACKET
|
107 |
117 |
|
108 |
|
%start prog
|
109 |
|
%type <Lustre_types.top_decl list> prog
|
|
118 |
%start <Lustre_types.top_decl list> prog
|
110 |
119 |
|
111 |
|
%start header
|
112 |
|
%type <Lustre_types.top_decl list> header
|
|
120 |
%start <Lustre_types.top_decl list> header
|
113 |
121 |
|
114 |
|
%start lustre_annot
|
115 |
|
%type <Lustre_types.expr_annot> lustre_annot
|
|
122 |
%start <Lustre_types.expr_annot> lustre_annot
|
116 |
123 |
|
117 |
|
%start lustre_spec
|
118 |
|
%type <Lustre_types.spec_types> lustre_spec
|
|
124 |
%start <Lustre_types.spec_types> lustre_spec
|
119 |
125 |
|
120 |
|
%start signed_const
|
121 |
|
%type <Lustre_types.constant> signed_const
|
122 |
|
|
123 |
|
%start expr
|
124 |
|
%type <Lustre_types.expr> expr
|
125 |
|
|
126 |
|
%start stmt_list
|
127 |
|
%type <Lustre_types.statement list * Lustre_types.assert_t list * Lustre_types.expr_annot list > stmt_list
|
128 |
|
|
129 |
|
%start vdecl_list
|
130 |
|
%type <Lustre_types.var_decl list> vdecl_list
|
131 |
126 |
%%
|
132 |
127 |
|
|
128 |
ident:
|
|
129 |
| x=UIDENT { x }
|
|
130 |
| x=IDENT { x }
|
133 |
131 |
|
134 |
132 |
module_ident:
|
135 |
|
UIDENT { $1 }
|
136 |
|
| IDENT { $1 }
|
|
133 |
| m=ident { m }
|
137 |
134 |
|
138 |
135 |
file_ident:
|
139 |
|
module_ident { $1 }
|
140 |
|
| module_ident POINT file_ident { $1 ^ "." ^ $3 }
|
|
136 |
| m=module_ident { m }
|
|
137 |
| m=module_ident POINT f=file_ident { m ^ "." ^ f }
|
141 |
138 |
|
142 |
139 |
path_ident:
|
143 |
|
POINT DIV path_ident { "./" ^ $3 }
|
144 |
|
| file_ident DIV path_ident { $1 ^ "/" ^ $3 }
|
145 |
|
| DIV path_ident { "/" ^ $2 }
|
146 |
|
| file_ident { $1 }
|
|
140 |
| POINT DIV p=path_ident { "./" ^ p }
|
|
141 |
| f=file_ident DIV p=path_ident { f ^ "/" ^ p }
|
|
142 |
| DIV p=path_ident { "/" ^ p }
|
|
143 |
| f=file_ident { f }
|
147 |
144 |
|
148 |
145 |
tag_bool:
|
149 |
|
| TRUE { tag_true }
|
150 |
|
| FALSE { tag_false }
|
|
146 |
| TRUE { tag_true }
|
|
147 |
| FALSE { tag_false }
|
151 |
148 |
|
152 |
149 |
tag_ident:
|
153 |
|
UIDENT { $1 }
|
154 |
|
| tag_bool { $1 }
|
|
150 |
| t=UIDENT { t }
|
|
151 |
| t=tag_bool { t }
|
155 |
152 |
|
156 |
153 |
node_ident:
|
157 |
|
UIDENT { $1 }
|
158 |
|
| IDENT { $1 }
|
|
154 |
| n=ident { n }
|
159 |
155 |
|
160 |
156 |
node_ident_decl:
|
161 |
|
node_ident { push_node $1; $1 }
|
|
157 |
| n=node_ident { push_node n }
|
162 |
158 |
|
163 |
159 |
vdecl_ident:
|
164 |
|
UIDENT { mkident $1 }
|
165 |
|
| IDENT { mkident $1 }
|
|
160 |
| x=ident { mkident x }
|
166 |
161 |
|
167 |
162 |
const_ident:
|
168 |
|
UIDENT { $1 }
|
169 |
|
| IDENT { $1 }
|
|
163 |
| c=ident { c }
|
170 |
164 |
|
171 |
165 |
type_ident:
|
172 |
|
IDENT { $1 }
|
|
166 |
| t=IDENT { t }
|
173 |
167 |
|
174 |
168 |
prog:
|
175 |
|
prefix_prog top_decl_list EOF { $1 @ (List.rev $2) }
|
176 |
|
|
177 |
|
prefix_prog:
|
178 |
|
{ [] }
|
179 |
|
| open_lusi prefix_prog { $1 :: $2 }
|
180 |
|
| typ_def prefix_prog { ($1 false (* not a header *)) :: $2 }
|
181 |
|
|
182 |
|
prefix_header:
|
183 |
|
{ [] }
|
184 |
|
| open_lusi prefix_header { $1 :: $2 }
|
185 |
|
| typ_def prefix_header { ($1 true (* is a header *)) :: $2 }
|
|
169 |
| p=prefix ds=flatten(top_decl*) EOF { List.map ((|>) false) p @ ds }
|
186 |
170 |
|
187 |
171 |
header:
|
188 |
|
prefix_header top_decl_header_list EOF { $1 @ (List.rev $2) }
|
|
172 |
| p=prefix ds=flatten(top_decl_header*) EOF { List.map ((|>) true) p @ ds }
|
189 |
173 |
|
|
174 |
prefix:
|
|
175 |
| { [] }
|
|
176 |
| o=open_lusi p=prefix { (fun _ -> o) :: p }
|
|
177 |
| td=typ_def p=prefix { (fun is_header -> td is_header) :: p }
|
190 |
178 |
|
191 |
179 |
open_lusi:
|
192 |
|
| OPEN QUOTE path_ident QUOTE { mktop_decl false (Open (true, $3)) }
|
193 |
|
| INCLUDE QUOTE path_ident QUOTE { mktop_decl false (Include ($3)) }
|
194 |
|
| OPEN LT path_ident GT { mktop_decl false (Open (false, $3)) }
|
195 |
|
|
196 |
|
top_decl_list:
|
197 |
|
{[]}
|
198 |
|
| top_decl_list top_decl {$2@$1}
|
199 |
|
|
200 |
|
|
201 |
|
top_decl_header_list:
|
202 |
|
{ [] }
|
203 |
|
| top_decl_header_list top_decl_header { $2@$1 }
|
|
180 |
| OPEN QUOTE p=path_ident QUOTE { mktop_decl false (Open (true, p)) }
|
|
181 |
| INCLUDE QUOTE p=path_ident QUOTE { mktop_decl false (Include p) }
|
|
182 |
| OPEN LT p=path_ident GT { mktop_decl false (Open (false, p)) }
|
204 |
183 |
|
205 |
184 |
state_annot:
|
206 |
|
FUNCTION { true }
|
207 |
|
| NODE { false }
|
|
185 |
| FUNCTION { true }
|
|
186 |
| NODE { false }
|
208 |
187 |
|
209 |
188 |
top_decl_header:
|
210 |
|
| CONST cdecl_list { List.rev ($2 true) }
|
211 |
|
| nodespecs state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL
|
212 |
|
{
|
213 |
|
let inputs = List.rev $5 in
|
214 |
|
let outputs = List.rev $10 in
|
215 |
|
let nd = mktop_decl true (ImportedNode
|
216 |
|
{nodei_id = $3;
|
217 |
|
nodei_type = Types.new_var ();
|
218 |
|
nodei_clock = Clocks.new_var true;
|
219 |
|
nodei_inputs = inputs;
|
220 |
|
nodei_outputs = outputs;
|
221 |
|
nodei_stateless = $2;
|
222 |
|
nodei_spec = $1;
|
223 |
|
nodei_prototype = $13;
|
224 |
|
nodei_in_lib = $14;})
|
225 |
|
in
|
226 |
|
pop_node ();
|
227 |
|
[nd] }
|
228 |
|
| top_contract { [$1] }
|
229 |
|
|
230 |
|
|
231 |
|
prototype_opt:
|
232 |
|
{ None }
|
233 |
|
| PROTOTYPE node_ident { Some $2}
|
234 |
|
|
235 |
|
in_lib_list:
|
236 |
|
{ [] }
|
237 |
|
| LIB module_ident in_lib_list { $2::$3 }
|
|
189 |
| CONST ds=cdecl+ SCOL
|
|
190 |
{ List.map ((|>) true) ds }
|
|
191 |
| nodei_spec=nodespecs nodei_stateless=state_annot nodei_id=node_ident_decl
|
|
192 |
LPAR nodei_inputs=vdecl_list SCOL? RPAR
|
|
193 |
RETURNS LPAR nodei_outputs=vdecl_list SCOL? RPAR
|
|
194 |
nodei_prototype=preceded(PROTOTYPE, node_ident)?
|
|
195 |
nodei_in_lib=preceded(LIB, module_ident)* SCOL
|
|
196 |
{ let nd = mktop_decl true (ImportedNode {
|
|
197 |
nodei_id;
|
|
198 |
nodei_type = Types.new_var ();
|
|
199 |
nodei_clock = Clocks.new_var true;
|
|
200 |
nodei_inputs;
|
|
201 |
nodei_outputs;
|
|
202 |
nodei_stateless;
|
|
203 |
nodei_spec;
|
|
204 |
nodei_prototype;
|
|
205 |
nodei_in_lib
|
|
206 |
})
|
|
207 |
in
|
|
208 |
pop_node ();
|
|
209 |
[nd]
|
|
210 |
}
|
|
211 |
| c=top_contract
|
|
212 |
{ [c] }
|
238 |
213 |
|
239 |
214 |
top_decl:
|
240 |
|
| CONST cdecl_list { List.rev ($2 false) }
|
241 |
|
| state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt nodespecs locals LET stmt_list TEL
|
242 |
|
{
|
243 |
|
let stmts, asserts, annots = $16 in
|
244 |
|
(* Declaring eqs annots *)
|
245 |
|
List.iter (fun ann ->
|
246 |
|
List.iter (fun (key, _) ->
|
247 |
|
Annotations.add_node_ann $2 key
|
248 |
|
) ann.annots
|
249 |
|
) annots;
|
250 |
|
(* Building the node *)
|
251 |
|
let inputs = List.rev $4 in
|
252 |
|
let outputs = List.rev $9 in
|
253 |
|
let nd = mktop_decl false (Node
|
254 |
|
{node_id = $2;
|
255 |
|
node_type = Types.new_var ();
|
256 |
|
node_clock = Clocks.new_var true;
|
257 |
|
node_inputs = inputs;
|
258 |
|
node_outputs = outputs;
|
259 |
|
node_locals = List.rev $14;
|
260 |
|
node_gencalls = [];
|
261 |
|
node_checks = [];
|
262 |
|
node_asserts = asserts;
|
263 |
|
node_stmts = stmts;
|
264 |
|
node_dec_stateless = $1;
|
265 |
|
node_stateless = None;
|
266 |
|
node_spec = $13;
|
267 |
|
node_annot = annots;
|
268 |
|
node_iscontract = false;
|
269 |
|
})
|
270 |
|
in
|
271 |
|
pop_node ();
|
272 |
|
(*add_node $3 nd;*) [nd] }
|
273 |
|
|
274 |
|
|
275 |
|
| NODESPEC
|
276 |
|
{ match $1 with
|
277 |
|
| LocalContract c -> assert false
|
278 |
|
| TopContract c -> c
|
279 |
|
|
280 |
|
}
|
|
215 |
| CONST ds=cdecl+ SCOL
|
|
216 |
{ List.map ((|>) false) ds }
|
|
217 |
| node_dec_stateless=state_annot node_id=node_ident_decl
|
|
218 |
LPAR node_inputs=vdecl_list SCOL? RPAR
|
|
219 |
RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?
|
|
220 |
node_spec=nodespecs
|
|
221 |
node_locals=locals LET content=stmt_list TEL
|
|
222 |
{ let node_stmts, node_asserts, node_annot = content in
|
|
223 |
(* Declaring eqs annots *)
|
|
224 |
List.iter (fun ann ->
|
|
225 |
List.iter (fun (key, _) ->
|
|
226 |
Annotations.add_node_ann node_id key)
|
|
227 |
ann.annots)
|
|
228 |
node_annot;
|
|
229 |
(* Building the node *)
|
|
230 |
let nd = mktop_decl false (Node
|
|
231 |
{node_id;
|
|
232 |
node_type = Types.new_var ();
|
|
233 |
node_clock = Clocks.new_var true;
|
|
234 |
node_inputs;
|
|
235 |
node_outputs;
|
|
236 |
node_locals;
|
|
237 |
node_gencalls = [];
|
|
238 |
node_checks = [];
|
|
239 |
node_asserts;
|
|
240 |
node_stmts;
|
|
241 |
node_dec_stateless;
|
|
242 |
node_stateless = None;
|
|
243 |
node_spec;
|
|
244 |
node_annot;
|
|
245 |
node_iscontract = false;
|
|
246 |
})
|
|
247 |
in
|
|
248 |
pop_node ();
|
|
249 |
(*add_node $3 nd;*)
|
|
250 |
[nd]
|
|
251 |
}
|
|
252 |
| s=NODESPEC
|
|
253 |
{ match s with
|
|
254 |
| LocalContract _ -> assert false
|
|
255 |
| TopContract c -> c
|
|
256 |
}
|
281 |
257 |
|
282 |
258 |
nodespecs:
|
283 |
|
nodespec_list {
|
284 |
|
match $1 with
|
285 |
|
| None -> None
|
286 |
|
| Some c -> Some (Contract c)
|
287 |
|
}
|
|
259 |
| ss=nodespec_list
|
|
260 |
{ match ss with
|
|
261 |
| None -> None
|
|
262 |
| Some c -> Some (Contract c)
|
|
263 |
}
|
288 |
264 |
|
289 |
265 |
nodespec_list:
|
290 |
|
{ None }
|
291 |
|
| NODESPEC nodespec_list {
|
292 |
|
let extract x = match x with LocalContract c -> c | _ -> assert false in
|
293 |
|
let s1 = extract $1 in
|
294 |
|
match $2 with
|
295 |
|
| None -> Some s1
|
296 |
|
| Some s2 -> Some (merge_contracts s1 s2) }
|
297 |
|
|
298 |
|
typ_def_list:
|
299 |
|
/* empty */ { (fun itf -> []) }
|
300 |
|
| typ_def typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($2 itf)) }
|
|
266 |
| { None }
|
|
267 |
| s=NODESPEC ss=nodespec_list
|
|
268 |
{ let extract x = match x with LocalContract c -> c | _ -> assert false in
|
|
269 |
let s1 = extract s in
|
|
270 |
match ss with
|
|
271 |
| None -> Some s1
|
|
272 |
| Some s2 -> Some (merge_contracts s1 s2)
|
|
273 |
}
|
301 |
274 |
|
302 |
275 |
typ_def:
|
303 |
|
TYPE type_ident EQ typ_def_rhs SCOL { (fun itf ->
|
304 |
|
let typ = mktop_decl itf (TypeDef { tydef_id = $2;
|
305 |
|
tydef_desc = $4
|
306 |
|
})
|
307 |
|
in (*add_type itf $2 typ;*) typ) }
|
|
276 |
| TYPE tydef_id=type_ident EQ tydef_desc=typ_def_rhs SCOL
|
|
277 |
{ fun itf ->
|
|
278 |
let typ = mktop_decl itf (TypeDef { tydef_id; tydef_desc }) in
|
|
279 |
(*add_type itf $2 typ;*)
|
|
280 |
typ
|
|
281 |
}
|
308 |
282 |
|
309 |
283 |
typ_def_rhs:
|
310 |
|
typeconst { $1 }
|
311 |
|
| ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) }
|
312 |
|
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
|
|
284 |
| t=typeconst
|
|
285 |
{ t }
|
|
286 |
| ENUM LCUR ts=separated_nonempty_list(COMMA, UIDENT) RCUR
|
|
287 |
{ Tydec_enum ts }
|
|
288 |
| STRUCT LCUR fs=separated_list(SCOL, separated_pair(IDENT, COL, typeconst)) RCUR
|
|
289 |
{ Tydec_struct fs }
|
313 |
290 |
|
314 |
|
array_typ_decl:
|
315 |
|
%prec POWER { fun typ -> typ }
|
316 |
|
| POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
|
|
291 |
%inline array_typ_decl:
|
|
292 |
| { [] }
|
|
293 |
| ds=preceded(POWER, dim)+ { ds }
|
317 |
294 |
|
318 |
295 |
typeconst:
|
319 |
|
TINT array_typ_decl { $2 Tydec_int }
|
320 |
|
| TBOOL array_typ_decl { $2 Tydec_bool }
|
321 |
|
| TREAL array_typ_decl { $2 Tydec_real }
|
322 |
|
/* | TFLOAT array_typ_decl { $2 Tydec_float } */
|
323 |
|
| type_ident array_typ_decl { $2 (Tydec_const $1) }
|
324 |
|
| TBOOL TCLOCK { Tydec_clock Tydec_bool }
|
325 |
|
| IDENT TCLOCK { Tydec_clock (Tydec_const $1) }
|
326 |
|
|
327 |
|
tag_list:
|
328 |
|
UIDENT { $1 :: [] }
|
329 |
|
| tag_list COMMA UIDENT { $3 :: $1 }
|
330 |
|
|
331 |
|
field_list: { [] }
|
332 |
|
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
|
333 |
|
|
|
296 |
| TINT ds=array_typ_decl { mkarraytype Tydec_int ds }
|
|
297 |
| TBOOL ds=array_typ_decl { mkarraytype Tydec_bool ds }
|
|
298 |
| TREAL ds=array_typ_decl { mkarraytype Tydec_real ds }
|
|
299 |
/* | TFLOAT ds=array_typ_decl { mkarraytype Tydec_float ds } */
|
|
300 |
| t=type_ident ds=array_typ_decl { mkarraytype (Tydec_const t) ds }
|
|
301 |
| TBOOL TCLOCK { Tydec_clock Tydec_bool }
|
|
302 |
| t=IDENT TCLOCK { Tydec_clock (Tydec_const t) }
|
|
303 |
|
334 |
304 |
stmt_list:
|
335 |
|
{ [], [], [] }
|
336 |
|
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
|
337 |
|
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
|
338 |
|
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
|
339 |
|
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
|
|
305 |
| { [], [], [] }
|
|
306 |
| e=eq ss=stmt_list
|
|
307 |
{ let eql, assertl, annotl = ss in
|
|
308 |
Eq e :: eql, assertl, annotl
|
|
309 |
}
|
|
310 |
| a=assert_ ss=stmt_list
|
|
311 |
{ let eql, assertl, annotl = ss in
|
|
312 |
eql, a :: assertl, annotl
|
|
313 |
}
|
|
314 |
| a=ANNOT ss=stmt_list
|
|
315 |
{ let eql, assertl, annotl = ss in
|
|
316 |
eql, assertl, a :: annotl
|
|
317 |
}
|
|
318 |
| a=automaton ss=stmt_list
|
|
319 |
{ let eql, assertl, annotl = ss in
|
|
320 |
Aut a :: eql, assertl, annotl
|
|
321 |
}
|
340 |
322 |
|
341 |
323 |
automaton:
|
342 |
|
AUTOMATON type_ident handler_list { Automata.mkautomata (get_loc ()) $2 $3 }
|
343 |
|
|
344 |
|
handler_list:
|
345 |
|
{ [] }
|
346 |
|
| handler handler_list { $1::$2 }
|
|
324 |
| AUTOMATON t=type_ident hs=handler* { Automata.mkautomata (get_loc ()) t hs }
|
347 |
325 |
|
348 |
326 |
handler:
|
349 |
|
STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
|
350 |
|
|
351 |
|
unless_list:
|
352 |
|
{ [] }
|
353 |
|
| unless unless_list { $1::$2 }
|
354 |
|
|
355 |
|
until_list:
|
356 |
|
{ [] }
|
357 |
|
| until until_list { $1::$2 }
|
|
327 |
| STATE x=UIDENT COL ul=unless* l=locals LET ss=stmt_list TEL ut=until*
|
|
328 |
{ Automata.mkhandler (get_loc ()) x ul ut l ss }
|
358 |
329 |
|
359 |
330 |
unless:
|
360 |
|
UNLESS expr RESTART UIDENT { (get_loc (), $2, true, $4) }
|
361 |
|
| UNLESS expr RESUME UIDENT { (get_loc (), $2, false, $4) }
|
|
331 |
| UNLESS e=expr RESTART s=UIDENT { get_loc (), e, true, s }
|
|
332 |
| UNLESS e=expr RESUME s=UIDENT { get_loc (), e, false, s }
|
362 |
333 |
|
363 |
334 |
until:
|
364 |
|
UNTIL expr RESTART UIDENT { (get_loc (), $2, true, $4) }
|
365 |
|
| UNTIL expr RESUME UIDENT { (get_loc (), $2, false, $4) }
|
|
335 |
| UNTIL e=expr RESTART s=UIDENT { get_loc (), e, true, s }
|
|
336 |
| UNTIL e=expr RESUME s=UIDENT { get_loc (), e, false, s }
|
366 |
337 |
|
367 |
338 |
assert_:
|
368 |
|
| ASSERT expr SCOL {mkassert ($2)}
|
|
339 |
| ASSERT e=expr SCOL { mkassert e }
|
369 |
340 |
|
370 |
341 |
eq:
|
371 |
|
ident_list EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
|
372 |
|
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
|
|
342 |
| xs=pattern EQ e=expr SCOL {mkeq (List.map fst xs, e)}
|
373 |
343 |
|
374 |
|
lustre_spec:
|
375 |
|
| top_contracts EOF { TopContract $1 }
|
376 |
|
| contract_content EOF { LocalContract $1}
|
|
344 |
%inline pattern:
|
|
345 |
| xs=ident_list { xs }
|
|
346 |
| LPAR xs=ident_list RPAR { xs }
|
377 |
347 |
|
378 |
|
top_contracts:
|
379 |
|
| top_contract { [$1] }
|
380 |
|
| top_contract top_contracts { $1::$2 }
|
|
348 |
lustre_spec:
|
|
349 |
| cs=top_contract+ EOF { TopContract cs }
|
|
350 |
| c=contract_content EOF { LocalContract c }
|
381 |
351 |
|
382 |
352 |
top_contract:
|
383 |
|
| CONTRACT node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt LET contract_content TEL
|
384 |
|
{
|
385 |
|
let nd = mktop_decl true (Node
|
386 |
|
{node_id = $2;
|
387 |
|
node_type = Types.new_var ();
|
388 |
|
node_clock = Clocks.new_var true;
|
389 |
|
node_inputs = List.rev $4;
|
390 |
|
node_outputs = List.rev $9;
|
391 |
|
node_locals = []; (* will be filled later *)
|
392 |
|
node_gencalls = [];
|
393 |
|
node_checks = [];
|
394 |
|
node_asserts = [];
|
395 |
|
node_stmts = []; (* will be filled later *)
|
396 |
|
node_dec_stateless = false;
|
397 |
|
(* By default we assume contracts as stateful *)
|
398 |
|
node_stateless = None;
|
399 |
|
node_spec = Some (Contract $14);
|
400 |
|
node_annot = [];
|
401 |
|
node_iscontract = true;
|
402 |
|
}
|
403 |
|
)
|
404 |
|
in
|
405 |
|
pop_node ();
|
406 |
|
(*add_imported_node $3 nd;*)
|
407 |
|
nd }
|
|
353 |
| CONTRACT node_id=node_ident_decl
|
|
354 |
LPAR node_inputs=vdecl_list SCOL? RPAR
|
|
355 |
RETURNS LPAR node_outputs=vdecl_list SCOL? RPAR SCOL?
|
|
356 |
LET cc=contract_content TEL
|
|
357 |
{ let nd = mktop_decl true (Node {
|
|
358 |
node_id;
|
|
359 |
node_type = Types.new_var ();
|
|
360 |
node_clock = Clocks.new_var true;
|
|
361 |
node_inputs;
|
|
362 |
node_outputs;
|
|
363 |
node_locals = []; (* will be filled later *)
|
|
364 |
node_gencalls = [];
|
|
365 |
node_checks = [];
|
|
366 |
node_asserts = [];
|
|
367 |
node_stmts = []; (* will be filled later *)
|
|
368 |
node_dec_stateless = false;
|
|
369 |
(* By default we assume contracts as stateful *)
|
|
370 |
node_stateless = None;
|
|
371 |
node_spec = Some (Contract cc);
|
|
372 |
node_annot = [];
|
|
373 |
node_iscontract = true;
|
|
374 |
}
|
|
375 |
)
|
|
376 |
in
|
|
377 |
pop_node ();
|
|
378 |
(*add_imported_node $3 nd;*)
|
|
379 |
nd
|
|
380 |
}
|
408 |
381 |
|
409 |
382 |
contract_content:
|
410 |
|
{ empty_contract }
|
411 |
|
| CONTRACT contract_content { $2 }
|
412 |
|
| CONST IDENT EQ expr SCOL contract_content
|
413 |
|
{ merge_contracts (mk_contract_var $2 true None $4 (get_loc())) $6 }
|
414 |
|
| CONST IDENT COL typeconst EQ expr SCOL contract_content
|
415 |
|
{ merge_contracts (mk_contract_var $2 true (Some(mktyp $4)) $6 (get_loc())) $8 }
|
416 |
|
| VAR IDENT COL typeconst EQ expr SCOL contract_content
|
417 |
|
{ merge_contracts (mk_contract_var $2 false (Some(mktyp $4)) $6 (get_loc())) $8 }
|
418 |
|
| ASSUME qexpr SCOL contract_content
|
419 |
|
{ merge_contracts (mk_contract_assume $2) $4 }
|
420 |
|
| ASSUME STRING qexpr SCOL contract_content
|
421 |
|
{ merge_contracts (mk_contract_assume ~name:$2 $3) $5 }
|
422 |
|
| GUARANTEES qexpr SCOL contract_content
|
423 |
|
{ merge_contracts (mk_contract_guarantees $2) $4 }
|
424 |
|
| GUARANTEES STRING qexpr SCOL contract_content
|
425 |
|
{ merge_contracts (mk_contract_guarantees ~name:$2 $3) $5 }
|
426 |
|
| MODE IDENT LPAR mode_content RPAR SCOL contract_content
|
427 |
|
{ merge_contracts (
|
428 |
|
let r, e = $4 in
|
429 |
|
mk_contract_mode $2 r e (get_loc())) $7 }
|
430 |
|
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
|
431 |
|
{ merge_contracts (mk_contract_import $2 (mkexpr (Expr_tuple (List.rev $4))) (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
|
432 |
|
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR tuple_expr RPAR SCOL contract_content
|
433 |
|
{ merge_contracts (mk_contract_import $2 $4 (mkexpr (Expr_tuple (List.rev $8))) (get_loc())) $11 }
|
434 |
|
| IMPORT IDENT LPAR tuple_expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
|
435 |
|
{ merge_contracts (mk_contract_import $2 (mkexpr (Expr_tuple (List.rev $4))) $8 (get_loc())) $11 }
|
436 |
|
| IMPORT IDENT LPAR expr RPAR RETURNS LPAR expr RPAR SCOL contract_content
|
437 |
|
{ merge_contracts (mk_contract_import $2 $4 $8 (get_loc())) $11 }
|
|
383 |
| { empty_contract }
|
|
384 |
| CONTRACT cc=contract_content
|
|
385 |
{ cc }
|
|
386 |
| CONST x=IDENT COL t=typeconst? EQ e=expr SCOL cc=contract_content
|
|
387 |
{ merge_contracts (mk_contract_var x true (mkotyp t) e (get_loc())) cc }
|
|
388 |
| VAR x=IDENT COL t=typeconst EQ e=expr SCOL cc=contract_content
|
|
389 |
{ merge_contracts (mk_contract_var x false (Some (mktyp t)) e (get_loc())) cc }
|
|
390 |
| ASSUME x=ioption(STRING) e=qexpr SCOL cc=contract_content
|
|
391 |
{ merge_contracts (mk_contract_assume x e) cc }
|
|
392 |
| GUARANTEES x=ioption(STRING) e=qexpr SCOL cc=contract_content
|
|
393 |
{ merge_contracts (mk_contract_guarantees x e) cc }
|
|
394 |
| MODE x=IDENT LPAR mc=mode_content RPAR SCOL cc=contract_content
|
|
395 |
{ merge_contracts (
|
|
396 |
let r, e = mc in
|
|
397 |
mk_contract_mode x r e (get_loc())) cc
|
|
398 |
}
|
|
399 |
| IMPORT x=IDENT LPAR xs=expr_or_tuple RPAR RETURNS LPAR ys=expr_or_tuple RPAR
|
|
400 |
SCOL cc=contract_content
|
|
401 |
{ merge_contracts (mk_contract_import x xs ys (get_loc())) cc }
|
|
402 |
|
|
403 |
%inline expr_or_tuple:
|
|
404 |
| e=expr { e }
|
|
405 |
| e=expr COMMA es=array_expr { mkexpr (Expr_tuple (e :: es)) }
|
438 |
406 |
|
439 |
407 |
mode_content:
|
440 |
|
{ [], [] }
|
441 |
|
| REQUIRE qexpr SCOL mode_content { let (r,e) = $4 in $2::r, e }
|
442 |
|
| REQUIRE STRING qexpr SCOL mode_content { let (r,e) = $5 in {$3 with eexpr_name = Some $2}::r, e }
|
443 |
|
| ENSURE qexpr SCOL mode_content { let (r,e) = $4 in r, $2::e }
|
444 |
|
| ENSURE STRING qexpr SCOL mode_content { let (r,e) = $5 in r, {$3 with eexpr_name = Some $2}::e }
|
445 |
|
|
446 |
|
/* WARNING: UNUSED RULES */
|
447 |
|
tuple_qexpr:
|
448 |
|
| qexpr COMMA qexpr {[$3;$1]}
|
449 |
|
| tuple_qexpr COMMA qexpr {$3::$1}
|
|
408 |
| { [], [] }
|
|
409 |
| REQUIRE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
|
|
410 |
{ let (r, e) = mc in
|
|
411 |
{ qe with eexpr_name } :: r, e }
|
|
412 |
| ENSURE eexpr_name=ioption(STRING) qe=qexpr SCOL mc=mode_content
|
|
413 |
{ let (r, e) = mc in
|
|
414 |
r, { qe with eexpr_name } :: e }
|
|
415 |
|
|
416 |
(* /* WARNING: UNUSED RULES */
|
|
417 |
* tuple_qexpr:
|
|
418 |
* | qexpr COMMA qexpr {[$3;$1]}
|
|
419 |
* | tuple_qexpr COMMA qexpr {$3::$1} *)
|
450 |
420 |
|
451 |
421 |
qexpr:
|
452 |
|
| expr { mkeexpr $1 }
|
|
422 |
| e=expr { mkeexpr e }
|
453 |
423 |
/* Quantifiers */
|
454 |
|
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 }
|
455 |
|
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
|
|
424 |
| EXISTS x=vdecl SCOL e=qexpr { extend_eexpr [Exists, x] e }
|
|
425 |
| FORALL x=vdecl SCOL e=qexpr { extend_eexpr [Forall, x] e }
|
456 |
426 |
|
457 |
|
|
458 |
|
tuple_expr:
|
459 |
|
expr COMMA expr {[$3;$1]}
|
460 |
|
| tuple_expr COMMA expr {$3::$1}
|
|
427 |
(* %inline tuple_expr:
|
|
428 |
* | e=expr COMMA es=array_expr { e :: es } *)
|
461 |
429 |
|
462 |
430 |
// Same as tuple expr but accepting lists with single element
|
463 |
|
array_expr:
|
464 |
|
expr {[$1]}
|
465 |
|
| expr COMMA array_expr {$1::$3}
|
466 |
|
|
467 |
|
dim_list:
|
468 |
|
dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
|
469 |
|
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
|
|
431 |
%inline array_expr:
|
|
432 |
| es=separated_nonempty_list(COMMA, expr) { es }
|
470 |
433 |
|
471 |
434 |
expr:
|
472 |
435 |
/* constants */
|
473 |
|
INT {mkexpr (Expr_const (Const_int $1))}
|
474 |
|
| REAL {mkexpr (Expr_const (Const_real $1))}
|
475 |
|
| STRING {mkexpr (Expr_const (Const_string $1))}
|
476 |
|
| COLCOL IDENT {mkexpr (Expr_const (Const_modeid $2))}
|
477 |
|
|
478 |
|
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
|
|
436 |
| c=INT { mkexpr (Expr_const (Const_int c)) }
|
|
437 |
| c=REAL { mkexpr (Expr_const (Const_real c)) }
|
|
438 |
| c=STRING %prec p_string { mkexpr (Expr_const (Const_string c)) }
|
|
439 |
| COLCOL c=IDENT { mkexpr (Expr_const (Const_modeid c)) }
|
|
440 |
/* | c=FLOAT { mkexpr (Expr_const (Const_float c)) }*/
|
|
441 |
|
479 |
442 |
/* Idents or type enum tags */
|
480 |
|
| IDENT { mkexpr (Expr_ident $1) }
|
481 |
|
| UIDENT { mkexpr (Expr_ident $1) (* TODO we will differenciate enum constants from variables later *) }
|
482 |
|
| tag_bool {
|
483 |
|
(* on sept 2014, X chenged the Const to
|
484 |
|
mkexpr (Expr_ident $1)
|
485 |
|
reverted back to const on july 2019 *)
|
486 |
|
mkexpr (Expr_const (Const_tag $1)) }
|
487 |
|
| LPAR ANNOT expr RPAR
|
488 |
|
{update_expr_annot (get_current_node ()) $3 $2}
|
489 |
|
| LPAR expr RPAR
|
490 |
|
{$2}
|
491 |
|
| LPAR tuple_expr RPAR
|
492 |
|
{mkexpr (Expr_tuple (List.rev $2))}
|
|
443 |
| x=IDENT { mkexpr (Expr_ident x) }
|
|
444 |
| x=UIDENT { mkexpr (Expr_ident x) (* TODO we will differenciate enum constants from variables later *) }
|
|
445 |
| t=tag_bool { mkexpr (Expr_const (Const_tag t)) } (* on sept 2014, X changed the Const to
|
|
446 |
mkexpr (Expr_ident $1)
|
|
447 |
reverted back to const on july 2019 *)
|
|
448 |
| LPAR a=ANNOT e=expr RPAR { update_expr_annot (get_current_node ()) e a }
|
|
449 |
| LPAR e=expr_or_tuple RPAR { e }
|
493 |
450 |
|
494 |
451 |
/* Array expressions */
|
495 |
|
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
|
496 |
|
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
|
497 |
|
| expr LBRACKET dim_list { $3 $1 }
|
|
452 |
| LBRACKET es=array_expr RBRACKET
|
|
453 |
{ mkexpr (Expr_array es) }
|
|
454 |
| e=expr POWER d=dim
|
|
455 |
{ mkexpr (Expr_power (e, d)) }
|
|
456 |
| e=expr ds=delimited(LBRACKET, dim, RBRACKET)+
|
|
457 |
{ List.fold_left (fun base d -> mkexpr (Expr_access (base, d))) e ds }
|
498 |
458 |
|
499 |
459 |
/* Temporal operators */
|
500 |
|
| PRE expr
|
501 |
|
{mkexpr (Expr_pre $2)}
|
502 |
|
| expr ARROW expr
|
503 |
|
{mkexpr (Expr_arrow ($1,$3))}
|
504 |
|
| expr FBY expr
|
505 |
|
{(*mkexpr (Expr_fby ($1,$3))*)
|
506 |
|
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
|
507 |
|
| expr WHEN vdecl_ident
|
508 |
|
{mkexpr (Expr_when ($1,fst $3,tag_true))}
|
509 |
|
| expr WHENNOT vdecl_ident
|
510 |
|
{mkexpr (Expr_when ($1,fst $3,tag_false))}
|
511 |
|
| expr WHEN tag_ident LPAR vdecl_ident RPAR
|
512 |
|
{mkexpr (Expr_when ($1, fst $5, $3))}
|
513 |
|
| MERGE vdecl_ident handler_expr_list
|
514 |
|
{mkexpr (Expr_merge (fst $2,$3))}
|
|
460 |
| PRE e=expr
|
|
461 |
{ mkexpr (Expr_pre e) }
|
|
462 |
| e1=expr ARROW e2=expr
|
|
463 |
{ mkexpr (Expr_arrow (e1, e2)) }
|
|
464 |
| e1=expr FBY e2=expr
|
|
465 |
{ mkexpr (Expr_arrow (e1, mkexpr (Expr_pre e2))) }
|
|
466 |
| e=expr WHEN x=vdecl_ident
|
|
467 |
{ mkexpr (Expr_when (e, fst x, tag_true)) }
|
|
468 |
| e=expr WHENNOT x=vdecl_ident
|
|
469 |
{ mkexpr (Expr_when (e, fst x, tag_false)) }
|
|
470 |
| e=expr WHEN t=tag_ident LPAR x=vdecl_ident RPAR
|
|
471 |
{ mkexpr (Expr_when (e, fst x, t)) }
|
|
472 |
| MERGE x=vdecl_ident
|
|
473 |
hs=delimited(LPAR, separated_pair(tag_ident, ARROW, expr), RPAR)*
|
|
474 |
{ mkexpr (Expr_merge (fst x, hs)) }
|
515 |
475 |
|
516 |
476 |
/* Applications */
|
517 |
|
| node_ident LPAR expr RPAR
|
518 |
|
{mkexpr (Expr_appl ($1, $3, None))}
|
519 |
|
| node_ident LPAR expr RPAR EVERY expr
|
520 |
|
{mkexpr (Expr_appl ($1, $3, Some $6))}
|
521 |
|
| node_ident LPAR tuple_expr RPAR
|
522 |
|
{
|
523 |
|
let id=$1 in
|
524 |
|
let args=List.rev $3 in
|
525 |
|
match id, args with
|
526 |
|
| "fbyn", [expr;n;init] ->
|
527 |
|
let n = match n.expr_desc with
|
528 |
|
| Expr_const (Const_int n) -> n
|
529 |
|
| _ -> assert false
|
530 |
|
in
|
531 |
|
fby expr n init
|
532 |
|
| _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
|
533 |
|
}
|
534 |
|
| node_ident LPAR tuple_expr RPAR EVERY expr
|
535 |
|
{
|
536 |
|
let id=$1 in
|
537 |
|
let args=List.rev $3 in
|
538 |
|
let clock=$6 in
|
539 |
|
if id="fby" then
|
540 |
|
assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
|
541 |
|
else
|
542 |
|
mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock))
|
543 |
|
}
|
|
477 |
| f=node_ident LPAR es=expr_or_tuple RPAR r=preceded(EVERY, expr)?
|
|
478 |
{ match f, es.expr_desc, r with
|
|
479 |
| "fbyn", Expr_tuple [expr; n; init], None ->
|
|
480 |
let n = match n.expr_desc with
|
|
481 |
| Expr_const (Const_int n) -> n
|
|
482 |
| _ -> assert false
|
|
483 |
in
|
|
484 |
fby expr n init
|
|
485 |
| "fbyn", _ , Some _ ->
|
|
486 |
assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
|
|
487 |
| _ -> mkexpr (Expr_appl (f, es, r))
|
|
488 |
}
|
544 |
489 |
|
545 |
490 |
/* Boolean expr */
|
546 |
|
| expr AND expr
|
547 |
|
{mkpredef_call "&&" [$1;$3]}
|
548 |
|
| expr AMPERAMPER expr
|
549 |
|
{mkpredef_call "&&" [$1;$3]}
|
550 |
|
| expr OR expr
|
551 |
|
{mkpredef_call "||" [$1;$3]}
|
552 |
|
| expr BARBAR expr
|
553 |
|
{mkpredef_call "||" [$1;$3]}
|
554 |
|
| expr XOR expr
|
555 |
|
{mkpredef_call "xor" [$1;$3]}
|
556 |
|
| NOT expr
|
557 |
|
{mkpredef_call "not" [$2]}
|
558 |
|
| expr IMPL expr
|
559 |
|
{mkpredef_call "impl" [$1;$3]}
|
|
491 |
| e1=expr AND e2=expr { mkpredef_call_b "&&" e1 e2 }
|
|
492 |
| e1=expr AMPERAMPER e2=expr { mkpredef_call_b "&&" e1 e2 }
|
|
493 |
| e1=expr OR e2=expr { mkpredef_call_b "||" e1 e2 }
|
|
494 |
| e1=expr BARBAR e2=expr { mkpredef_call_b "||" e1 e2 }
|
|
495 |
| e1=expr XOR e2=expr { mkpredef_call_b "xor" e1 e2 }
|
|
496 |
| NOT e=expr { mkpredef_call_u "not" e }
|
|
497 |
| e1=expr IMPL e2=expr { mkpredef_call_b "impl" e1 e2 }
|
560 |
498 |
|
561 |
499 |
/* Comparison expr */
|
562 |
|
| expr EQ expr
|
563 |
|
{mkpredef_call "=" [$1;$3]}
|
564 |
|
| expr LT expr
|
565 |
|
{mkpredef_call "<" [$1;$3]}
|
566 |
|
| expr LTE expr
|
567 |
|
{mkpredef_call "<=" [$1;$3]}
|
568 |
|
| expr GT expr
|
569 |
|
{mkpredef_call ">" [$1;$3]}
|
570 |
|
| expr GTE expr
|
571 |
|
{mkpredef_call ">=" [$1;$3]}
|
572 |
|
| expr NEQ expr
|
573 |
|
{mkpredef_call "!=" [$1;$3]}
|
|
500 |
| e1=expr EQ e2=expr { mkpredef_call_b "=" e1 e2 }
|
|
501 |
| e1=expr LT e2=expr { mkpredef_call_b "<" e1 e2 }
|
|
502 |
| e1=expr LTE e2=expr { mkpredef_call_b "<=" e1 e2 }
|
|
503 |
| e1=expr GT e2=expr { mkpredef_call_b ">" e1 e2 }
|
|
504 |
| e1=expr GTE e2=expr { mkpredef_call_b ">=" e1 e2 }
|
|
505 |
| e1=expr NEQ e2=expr { mkpredef_call_b "!=" e1 e2 }
|
574 |
506 |
|
575 |
507 |
/* Arithmetic expr */
|
576 |
|
| expr PLUS expr
|
577 |
|
{mkpredef_call "+" [$1;$3]}
|
578 |
|
| expr MINUS expr
|
579 |
|
{mkpredef_call "-" [$1;$3]}
|
580 |
|
| expr MULT expr
|
581 |
|
{mkpredef_call "*" [$1;$3]}
|
582 |
|
| expr DIV expr
|
583 |
|
{mkpredef_call "/" [$1;$3]}
|
584 |
|
| MINUS expr %prec UMINUS
|
585 |
|
{mkpredef_call "uminus" [$2]}
|
586 |
|
| expr MOD expr
|
587 |
|
{mkpredef_call "mod" [$1;$3]}
|
|
508 |
| e1=expr PLUS e2=expr { mkpredef_call_b "+" e1 e2 }
|
|
509 |
| e1=expr MINUS e2=expr { mkpredef_call_b "-" e1 e2 }
|
|
510 |
| e1=expr MULT e2=expr { mkpredef_call_b "*" e1 e2 }
|
|
511 |
| e1=expr DIV e2=expr { mkpredef_call_b "/" e1 e2 }
|
|
512 |
| MINUS e=expr %prec p_uminus { mkpredef_call_u "uminus" e }
|
|
513 |
| e1=expr MOD e2=expr { mkpredef_call_b "mod" e1 e2 }
|
588 |
514 |
|
589 |
515 |
/* If */
|
590 |
|
| IF expr THEN expr ELSE expr
|
591 |
|
{mkexpr (Expr_ite ($2, $4, $6))}
|
592 |
|
|
593 |
|
handler_expr_list:
|
594 |
|
{ [] }
|
595 |
|
| handler_expr handler_expr_list { $1 :: $2 }
|
596 |
|
|
597 |
|
handler_expr:
|
598 |
|
LPAR tag_ident ARROW expr RPAR { ($2, $4) }
|
599 |
|
|
600 |
|
signed_const_array:
|
601 |
|
| signed_const { [$1] }
|
602 |
|
| signed_const COMMA signed_const_array { $1 :: $3 }
|
603 |
|
|
604 |
|
signed_const_struct:
|
605 |
|
| IDENT EQ signed_const { [ ($1, $3) ] }
|
606 |
|
| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
|
|
516 |
| IF e=expr THEN t=expr ELSE f=expr { mkexpr (Expr_ite (e, t, f)) }
|
607 |
517 |
|
608 |
518 |
signed_const:
|
609 |
|
INT {Const_int $1}
|
610 |
|
| REAL {Const_real $1}
|
611 |
|
/* | FLOAT {Const_float $1} */
|
612 |
|
| tag_ident {Const_tag $1}
|
613 |
|
| MINUS INT {Const_int (-1 * $2)}
|
614 |
|
| MINUS REAL {Const_real (Real.uminus $2)}
|
615 |
|
/* | MINUS FLOAT {Const_float (-1. *. $2)} */
|
616 |
|
| LCUR signed_const_struct RCUR { Const_struct $2 }
|
617 |
|
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
|
|
519 |
| c=INT
|
|
520 |
{ Const_int c }
|
|
521 |
| c=REAL
|
|
522 |
{ Const_real c }
|
|
523 |
/* | c=FLOAT { Const_float c } */
|
|
524 |
| t=tag_ident { Const_tag t }
|
|
525 |
| MINUS c=INT
|
|
526 |
{ Const_int (-1 * c) }
|
|
527 |
| MINUS c=REAL
|
|
528 |
{ Const_real (Real.uminus c) }
|
|
529 |
/* | MINUS c=FLOAT { Const_float (-1. *. c) } */
|
|
530 |
| LCUR
|
|
531 |
cs=separated_nonempty_list(COMMA, separated_pair(IDENT, EQ, signed_const))
|
|
532 |
RCUR
|
|
533 |
{ Const_struct cs }
|
|
534 |
| LBRACKET cs=separated_nonempty_list(COMMA, signed_const) RBRACKET
|
|
535 |
{ Const_array cs }
|
618 |
536 |
|
619 |
537 |
dim:
|
620 |
|
INT { mkdim_int $1 }
|
621 |
|
| LPAR dim RPAR { $2 }
|
622 |
|
| UIDENT { mkdim_ident $1 }
|
623 |
|
| IDENT { mkdim_ident $1 }
|
624 |
|
| dim AND dim
|
625 |
|
{mkdim_appl "&&" [$1;$3]}
|
626 |
|
| dim AMPERAMPER dim
|
627 |
|
{mkdim_appl "&&" [$1;$3]}
|
628 |
|
| dim OR dim
|
629 |
|
{mkdim_appl "||" [$1;$3]}
|
630 |
|
| dim BARBAR dim
|
631 |
|
{mkdim_appl "||" [$1;$3]}
|
632 |
|
| dim XOR dim
|
633 |
|
{mkdim_appl "xor" [$1;$3]}
|
634 |
|
| NOT dim
|
635 |
|
{mkdim_appl "not" [$2]}
|
636 |
|
| dim IMPL dim
|
637 |
|
{mkdim_appl "impl" [$1;$3]}
|
|
538 |
| i=INT { mkdim_int i }
|
|
539 |
| LPAR d=dim RPAR { d }
|
|
540 |
| x=ident { mkdim_ident x }
|
|
541 |
| d1=dim AND d2=dim { mkdim_appl_b "&&" d1 d2 }
|
|
542 |
| d1=dim AMPERAMPER d2=dim { mkdim_appl_b "&&" d1 d2 }
|
|
543 |
| d1=dim OR d2=dim { mkdim_appl_b "||" d1 d2 }
|
|
544 |
| d1=dim BARBAR d2=dim { mkdim_appl_b "||" d1 d2 }
|
|
545 |
| d1=dim XOR d2=dim { mkdim_appl_b "xor" d1 d2 }
|
|
546 |
| NOT d=dim { mkdim_appl_u "not" d }
|
|
547 |
| d1=dim IMPL d2=dim { mkdim_appl_b "impl" d1 d2 }
|
638 |
548 |
|
639 |
549 |
/* Comparison dim */
|
640 |
|
| dim EQ dim
|
641 |
|
{mkdim_appl "=" [$1;$3]}
|
642 |
|
| dim LT dim
|
643 |
|
{mkdim_appl "<" [$1;$3]}
|
644 |
|
| dim LTE dim
|
645 |
|
{mkdim_appl "<=" [$1;$3]}
|
646 |
|
| dim GT dim
|
647 |
|
{mkdim_appl ">" [$1;$3]}
|
648 |
|
| dim GTE dim
|
649 |
|
{mkdim_appl ">=" [$1;$3]}
|
650 |
|
| dim NEQ dim
|
651 |
|
{mkdim_appl "!=" [$1;$3]}
|
|
550 |
| d1=dim EQ d2=dim { mkdim_appl_b "=" d1 d2 }
|
|
551 |
| d1=dim LT d2=dim { mkdim_appl_b "<" d1 d2 }
|
|
552 |
| d1=dim LTE d2=dim { mkdim_appl_b "<=" d1 d2 }
|
|
553 |
| d1=dim GT d2=dim { mkdim_appl_b ">" d1 d2 }
|
|
554 |
| d1=dim GTE d2=dim { mkdim_appl_b ">=" d1 d2 }
|
|
555 |
| d1=dim NEQ d2=dim { mkdim_appl_b "!=" d1 d2 }
|
652 |
556 |
|
653 |
557 |
/* Arithmetic dim */
|
654 |
|
| dim PLUS dim
|
655 |
|
{mkdim_appl "+" [$1;$3]}
|
656 |
|
| dim MINUS dim
|
657 |
|
{mkdim_appl "-" [$1;$3]}
|
658 |
|
| dim MULT dim
|
659 |
|
{mkdim_appl "*" [$1;$3]}
|
660 |
|
| dim DIV dim
|
661 |
|
{mkdim_appl "/" [$1;$3]}
|
662 |
|
| MINUS dim %prec UMINUS
|
663 |
|
{mkdim_appl "uminus" [$2]}
|
664 |
|
| dim MOD dim
|
665 |
|
{mkdim_appl "mod" [$1;$3]}
|
|
558 |
| d1=dim PLUS d2=dim { mkdim_appl_b "+" d1 d2 }
|
|
559 |
| d1=dim MINUS d2=dim { mkdim_appl_b "-" d1 d2 }
|
|
560 |
| d1=dim MULT d2=dim { mkdim_appl_b "*" d1 d2 }
|
|
561 |
| d1=dim DIV d2=dim { mkdim_appl_b "/" d1 d2 }
|
|
562 |
| MINUS d=dim %prec p_uminus { mkdim_appl_u "uminus" d }
|
|
563 |
| d1=dim MOD d2=dim { mkdim_appl_b "mod" d1 d2 }
|
|
564 |
|
666 |
565 |
/* If */
|
667 |
|
| IF dim THEN dim ELSE dim
|
668 |
|
{mkdim_ite $2 $4 $6}
|
|
566 |
| IF d=dim THEN t=dim ELSE f=dim { mkdim_ite d t f }
|
669 |
567 |
|
670 |
|
locals:
|
671 |
|
{[]}
|
672 |
|
| VAR local_vdecl_list SCOL {$2}
|
|
568 |
%inline locals:
|
|
569 |
| xs=loption(preceded(VAR, flatten(separated_nonempty_list(SCOL, local_vdecl))))
|
|
570 |
{ xs }
|
673 |
571 |
|
674 |
572 |
vdecl_list:
|
675 |
|
vdecl {$1}
|
676 |
|
| vdecl_list SCOL vdecl {$3 @ $1}
|
|
573 |
| d=vdecl %prec p_vdecl { d }
|
|
574 |
| d=vdecl SCOL ds=vdecl_list { d @ ds }
|
677 |
575 |
|
678 |
576 |
vdecl:
|
679 |
|
ident_list COL typeconst clock
|
680 |
|
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
|
681 |
|
| CONST ident_list /* static parameters don't have clocks */
|
682 |
|
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
|
683 |
|
| CONST ident_list COL typeconst /* static parameters don't have clocks */
|
684 |
|
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
|
685 |
|
|
686 |
|
local_vdecl_list:
|
687 |
|
local_vdecl {$1}
|
688 |
|
| local_vdecl_list SCOL local_vdecl {$3 @ $1}
|
|
577 |
| xs=ident_list COL t=typeconst c=clock?
|
|
578 |
{ mkvdecls false (Some t) c None xs }
|
|
579 |
| CONST xs=ident_list t=preceded(COL, typeconst)?
|
|
580 |
/* static parameters don't have clocks */
|
|
581 |
{ mkvdecls true t None None xs }
|
689 |
582 |
|
690 |
583 |
local_vdecl:
|
691 |
|
/* Useless no ?*/ ident_list
|
692 |
|
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
|
693 |
|
| ident_list COL typeconst clock
|
694 |
|
{ List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
|
695 |
|
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
|
696 |
|
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
|
697 |
|
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
|
698 |
|
{ let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
|
699 |
|
|
700 |
|
cdecl_list:
|
701 |
|
cdecl SCOL { (fun itf -> [$1 itf]) }
|
702 |
|
| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
|
|
584 |
| xs=ident_list /* Useless no ?*/
|
|
585 |
{ mkvdecls false None None None xs }
|
|
586 |
| xs=ident_list COL t=typeconst c=clock?
|
|
587 |
{ mkvdecls false (Some t) c None xs }
|
|
588 |
| CONST x=vdecl_ident t=preceded(COL, typeconst)? EQ e=expr
|
|
589 |
/* static parameters don't have clocks */
|
|
590 |
{ mkvdecls true t None (Some e) [x] }
|
703 |
591 |
|
704 |
592 |
cdecl:
|
705 |
|
const_ident EQ signed_const {
|
706 |
|
(fun itf ->
|
707 |
|
let c = mktop_decl itf (Const {
|
708 |
|
const_id = $1;
|
709 |
|
const_loc = get_loc ();
|
710 |
|
const_type = Types.new_var ();
|
711 |
|
const_value = $3})
|
712 |
|
in
|
713 |
|
(*add_const itf $1 c;*) c)
|
714 |
|
}
|
715 |
|
|
716 |
|
clock:
|
717 |
|
{mkclock Ckdec_any}
|
718 |
|
| when_list
|
719 |
|
{mkclock (Ckdec_bool (List.rev $1))}
|
|
593 |
| x=const_ident EQ c=signed_const
|
|
594 |
{ fun itf ->
|
|
595 |
let c = mktop_decl itf (Const {
|
|
596 |
const_id = x;
|
|
597 |
const_loc = get_loc ();
|
|
598 |
const_type = Types.new_var ();
|
|
599 |
const_value = c
|
|
600 |
})
|
|
601 |
in
|
|
602 |
(*add_const itf $1 c;*)
|
|
603 |
c
|
|
604 |
}
|
|
605 |
|
|
606 |
%inline clock:
|
|
607 |
| l=when_cond+ { mkclock (Ckdec_bool l) }
|
720 |
608 |
|
721 |
609 |
when_cond:
|
722 |
|
WHEN IDENT {($2, tag_true)}
|
723 |
|
| WHENNOT IDENT {($2, tag_false)}
|
724 |
|
| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
|
725 |
|
|
726 |
|
when_list:
|
727 |
|
when_cond {[$1]}
|
728 |
|
| when_list when_cond {$2::$1}
|
729 |
|
|
730 |
|
ident_list:
|
731 |
|
vdecl_ident {[$1]}
|
732 |
|
| ident_list COMMA vdecl_ident {$3::$1}
|
733 |
|
|
734 |
|
SCOL_opt:
|
735 |
|
SCOL {} | {}
|
|
610 |
| WHEN x=IDENT { x, tag_true }
|
|
611 |
| WHENNOT x=IDENT { x, tag_false }
|
|
612 |
| WHEN t=tag_ident LPAR x=IDENT RPAR { x, t }
|
736 |
613 |
|
|
614 |
%inline ident_list:
|
|
615 |
| ds=separated_nonempty_list(COMMA, vdecl_ident) { ds }
|
737 |
616 |
|
738 |
617 |
lustre_annot:
|
739 |
|
lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
|
|
618 |
| lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
|
740 |
619 |
|
741 |
620 |
lustre_annot_list:
|
742 |
621 |
{ [] }
|
rewrite a bit the menhir parser