Revision e135421f src/corelang.ml
src/corelang.ml  

104  104 
mutable node_checks: Dimension.dim_expr list; 
105  105 
node_asserts: assert_t list; 
106  106 
node_eqs: eq list; 
107 
node_dec_stateless: bool; 

107 
mutable node_dec_stateless: bool;


108  108 
mutable node_stateless: bool option; 
109  109 
node_spec: LustreSpec.node_annot option; 
110  110 
node_annot: LustreSpec.expr_annot option; 
...  ...  
145  145 
 No_main_specified 
146  146 
 Unbound_symbol of ident 
147  147 
 Already_bound_symbol of ident 
148 
 Stateful of ident 

149  148  
150  149 
exception Error of Location.t * error 
151  150  
...  ...  
262  261 
 ImportedNode nd > true 
263  262 
 _ > assert false 
264  263  
265 
let rec is_stateless_expr expr = 

266 
match expr.expr_desc with 

267 
 Expr_const _ 

268 
 Expr_ident _ > true 

269 
 Expr_tuple el 

270 
 Expr_array el > List.for_all is_stateless_expr el 

271 
 Expr_access (e1, _) 

272 
 Expr_power (e1, _) > is_stateless_expr e1 

273 
 Expr_ite (c, t, e) > is_stateless_expr c && is_stateless_expr t && is_stateless_expr e 

274 
 Expr_arrow (e1, e2) 

275 
 Expr_fby (e1, e2) > is_stateless_expr e1 && is_stateless_expr e2 

276 
 Expr_pre e' > is_stateless_expr e' 

277 
 Expr_when (e', i, l)> is_stateless_expr e' 

278 
 Expr_merge (i, hl) > List.for_all (fun (t, h) > is_stateless_expr h) hl 

279 
 Expr_appl (i, e', i') > 

280 
is_stateless_expr e' && 

281 
(Basic_library.is_internal_fun i  check_stateless_node (node_from_name i)) 

282 
 Expr_uclock _ 

283 
 Expr_dclock _ 

284 
 Expr_phclock _ > assert false 

285 
and compute_stateless_node nd = 

286 
List.for_all (fun eq > is_stateless_expr eq.eq_rhs) nd.node_eqs 

287 
and check_stateless_node td = 

288 
match td.top_decl_desc with 

289 
 Node nd > ( 

290 
match nd.node_stateless with 

291 
 None > 

292 
begin 

293 
let stateless = compute_stateless_node nd in 

294 
nd.node_stateless < Some (false && stateless); 

295 
if nd.node_dec_stateless && (not stateless) 

296 
then raise (Error (td.top_decl_loc, Stateful nd.node_id)) 

297 
else stateless 

298 
end 

299 
 Some stl > stl) 

300 
 ImportedNode nd > nd.nodei_stateless 

301 
 _ > true 

302  264  
303  265 
(* alias and type definition table *) 
304  266 
let type_table = 
...  ...  
766  728 
fprintf fmt 
767  729 
"%s is already defined.@." 
768  730 
sym 
769 
 Stateful nd > 

770 
fprintf fmt 

771 
"node %s is declared stateless, but it is stateful.@." 

772 
nd 

773  731  
774  732 
(* filling node table with internal functions *) 
775  733 
let vdecls_of_typ_ck cpt ty = 
Also available in: Unified diff