Revision 52cfee34 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; 

108 
mutable node_stateless: bool option; 

107  109 
node_spec: LustreSpec.node_annot option; 
108  110 
node_annot: LustreSpec.expr_annot option; 
109  111 
} 
...  ...  
118  120 
nodei_spec: LustreSpec.node_annot option; 
119  121 
} 
120  122  
121 
type imported_fun_desc = 

122 
{fun_id: ident; 

123 
mutable fun_type: Types.type_expr; 

124 
fun_inputs: var_decl list; 

125 
fun_outputs: var_decl list; 

126 
fun_spec: LustreSpec.node_annot option;} 

127  
128  123 
type const_desc = 
129  124 
{const_id: ident; 
130  125 
const_loc: Location.t; 
...  ...  
136  131 
 Node of node_desc 
137  132 
 Consts of const_desc list 
138  133 
 ImportedNode of imported_node_desc 
139 
 ImportedFun of imported_fun_desc 

140  134 
 Open of string 
141  135  
142  136 
type top_decl = 
...  ...  
151  145 
 No_main_specified 
152  146 
 Unbound_symbol of ident 
153  147 
 Already_bound_symbol of ident 
148 
 Stateful of ident 

154  149  
155 
exception Error of error * Location.t


150 
exception Error of Location.t * error


156  151  
157  152 
module VDeclModule = 
158  153 
struct (* Node module *) 
...  ...  
267  262 
 ImportedNode nd > true 
268  263 
 _ > assert false 
269  264  
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  
270  303 
(* alias and type definition table *) 
271  304 
let type_table = 
272  305 
Utils.create_hashtable 20 [ 
...  ...  
505  538 
fun consts decl > 
506  539 
match decl.top_decl_desc with 
507  540 
 Consts clist > clist@consts 
508 
 Node _  ImportedNode _  ImportedFun _  Open _ > consts


541 
 Node _  ImportedNode _  Open _ > consts 

509  542 
) [] prog 
510  543  
511  544  
...  ...  
514  547 
fun nodes decl > 
515  548 
match decl.top_decl_desc with 
516  549 
 Node nd > nd::nodes 
517 
 Consts _  ImportedNode _  ImportedFun _  Open _ > nodes


550 
 Consts _  ImportedNode _  Open _ > nodes 

518  551 
) [] prog 
519  552  
520  553 
let prog_unfold_consts prog = 
...  ...  
658  691 
node_checks = node_checks; 
659  692 
node_asserts = node_asserts; 
660  693 
node_eqs = eqs; 
694 
node_dec_stateless = nd.node_dec_stateless; 

695 
node_stateless = nd.node_stateless; 

661  696 
node_spec = spec; 
662  697 
node_annot = annot; 
663  698 
} 
...  ...  
675  710 
 Consts c > 
676  711 
{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) } 
677  712 
 ImportedNode _ 
678 
 ImportedFun _ 

679  713 
 Open _ > top) 
680  714 
::accu 
681  715 
) [] prog 
...  ...  
694  728 
fprintf fmt "%s: " ind.nodei_id; 
695  729 
Utils.reset_names (); 
696  730 
fprintf fmt "%a@ " Types.print_ty ind.nodei_type 
697 
 ImportedFun ind > 

698 
fprintf fmt "%s: " ind.fun_id; 

699 
Utils.reset_names (); 

700 
fprintf fmt "%a@ " Types.print_ty ind.fun_type 

701  731 
 Consts _  Open _ > () 
702  732  
703  733 
let pp_prog_type fmt tdecl_list = 
...  ...  
713  743 
fprintf fmt "%s: " ind.nodei_id; 
714  744 
Utils.reset_names (); 
715  745 
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock 
716 
 ImportedFun _  Consts _  Open _ > ()


746 
 Consts _  Open _ > () 

717  747  
718  748 
let pp_prog_clock fmt prog = 
719  749 
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog 
...  ...  
736  766 
fprintf fmt 
737  767 
"%s is already defined.@." 
738  768 
sym 
769 
 Stateful nd > 

770 
fprintf fmt 

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

772 
nd 

739  773  
740  774 
(* filling node table with internal functions *) 
741  775 
let vdecls_of_typ_ck cpt ty = 
Also available in: Unified diff