Project

General

Profile

Revision e135421f src/corelang.ml

View differences:

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