Project

General

Profile

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