Project

General

Profile

Revision d3e4c22f

View differences:

src/clock_calculus.ml
519 519
  | Mismatch (cr1,cr2) ->
520 520
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
521 521

  
522
(* Checks whether ck1 is a subtype of ck2 *)
523
let rec clock_subtyping ck1 ck2 =
522
(* ck1 is a subtype of ck2 *)
523
let rec sub_unify sub ck1 ck2 =
524 524
  match (repr ck1).cdesc, (repr ck2).cdesc with
525
  | Ccarrying _         , Ccarrying _ -> unify ck1 ck2
526
  | Ccarrying (cr', ck'), _           -> unify ck' ck2
527
  | _                                 -> unify ck1 ck2
525
  | Ctuple [c1]        , Ctuple [c2]        -> sub_unify sub c1 c2
526
  | Ctuple cl1         , Ctuple cl2         ->
527
    if List.length cl1 <> List.length cl2
528
    then raise (Unify (ck1, ck2))
529
    else List.iter2 (sub_unify sub) cl1 cl2
530
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
531
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
532
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
533
    begin
534
      unify_carrier cr1 cr2;
535
      sub_unify sub c1 c2
536
    end
537
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
538
    begin
539
      unify_carrier cr1 cr2;
540
      sub_unify sub c1 c2
541
    end
542
  | Ccarrying (_, c1)  , _         when sub -> sub_unify sub c1 ck2
543
  | _                                       -> unify ck1 ck2
544

  
545
let try_sub_unify sub ck1 ck2 loc =
546
  try
547
    sub_unify sub ck1 ck2
548
  with
549
  | Unify (ck1',ck2') ->
550
    raise (Error (loc, Clock_clash (ck1',ck2')))
551
  | Subsume (ck,cset) ->
552
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
553
  | Mismatch (cr1,cr2) ->
554
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
528 555

  
529 556
(* Clocks a list of arguments of Lustre builtin operators:
530 557
   - type each expression, remove carriers of clocks as
......
539 566

  
540 567
(* emulates a subtyping relation between clocks c and (cr : c),
541 568
   used during node application only *)
542
and clock_subtyping_arg env real_arg formal_clock =
569
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
543 570
  let loc = real_arg.expr_loc in
544 571
  let real_clock = clock_expr env real_arg in
545
  try
546
    clock_subtyping real_clock formal_clock
547
  with
548
  | Unify (ck1',ck2') ->
549
    raise (Error (loc, Clock_clash (real_clock, formal_clock)))
550
  | Subsume (ck,cset) ->
551
    raise (Error (loc, Clock_set_mismatch (ck, cset)))
552
  | Mismatch (cr1,cr2) ->
553
    raise (Error (loc, Carrier_mismatch (cr1, cr2)))
572
  try_sub_unify sub real_clock formal_clock loc
554 573

  
555 574
(* computes clocks for node application *)
556 575
and clock_appl env f args clock_reset loc =
......
779 798
  let ck_outs = clock_of_vlist nd.node_outputs in
780 799
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
781 800
  unify_imported_clock None ck_node;
782
  (*Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);*)
801
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
783 802
  (* Local variables may contain first-order carrier variables that should be generalized.
784 803
     That's not the case for types. *)
785 804
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
......
789 808
(*  if (is_main && is_polymorphic ck_node) then
790 809
    raise (Error (loc,(Cannot_be_polymorphic ck_node)));
791 810
*)
811
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
792 812
  nd.node_clock <- ck_node;
793 813
  Env.add_value env nd.node_id ck_node
794 814

  
......
832 852
  nd.nodei_clock <- ck_node;
833 853
  Env.add_value env nd.nodei_id ck_node
834 854

  
835
let clock_function env loc fcn =
836
  let new_env = clock_var_decl_list env false fcn.fun_inputs in
837
  ignore(clock_var_decl_list new_env false fcn.fun_outputs);
838
  let ck_ins = clock_of_vlist fcn.fun_inputs in
839
  let ck_outs = clock_of_vlist fcn.fun_outputs in
840
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
841
  unify_imported_clock None ck_node;
842
  check_imported_pclocks loc ck_node;
843
  try_generalize ck_node loc;
844
  Env.add_value env fcn.fun_id ck_node
845

  
846 855
let clock_top_consts env clist =
847 856
  List.fold_left (fun env cdecl ->
848 857
    let ck = new_var false in
......
855 864
    clock_node env decl.top_decl_loc nd
856 865
  | ImportedNode nd ->
857 866
    clock_imported_node env decl.top_decl_loc nd
858
  | ImportedFun fcn ->
859
    clock_function env decl.top_decl_loc fcn
860 867
  | Consts clist ->
861 868
    clock_top_consts env clist
862 869
  | Open _ ->
......
891 898
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
892 899
  | ImportedNode nd ->
893 900
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
894
  | ImportedFun nd ->
895
      ()
896 901
  | Consts clist -> ()
897 902
  | Open _  -> ()
898 903

  
src/clocks.ml
447 447
 (*
448 448
      if cvar.cscoped
449 449
      then
450
	fprintf fmt "['_%s%a]"
450
	fprintf fmt "[_%s%a]"
451 451
	  (name_of_type cvar.cid)
452 452
	  print_ckset cset
453 453
      else
454 454
 *)
455
	fprintf fmt "'_%s%a"
455
	fprintf fmt "_%s%a"
456 456
	  (name_of_type cvar.cid)
457 457
	  print_ckset cset
458 458
  | Cunivar cset ->
......
494 494
(*
495 495
      if ck.cscoped
496 496
      then
497
        fprintf fmt "['_%s]" (name_of_type ck.cid)
497
        fprintf fmt "[_%s]" (name_of_type ck.cid)
498 498
      else
499 499
*)
500
	fprintf fmt "'_%s" (name_of_type ck.cid)
500
	fprintf fmt "_%s" (name_of_type ck.cid)
501 501
    | Cunivar cset ->
502 502
(*
503 503
      if ck.cscoped
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 =
src/corelang.mli
97 97
     mutable node_checks: Dimension.dim_expr list;
98 98
     node_asserts: assert_t list; 
99 99
     node_eqs: eq list;
100
     node_dec_stateless: bool;
101
     mutable node_stateless: bool option;
100 102
     node_spec: LustreSpec.node_annot option;
101 103
     node_annot: LustreSpec.expr_annot option;}
102 104

  
......
108 110
     nodei_outputs: var_decl list;
109 111
     nodei_stateless: bool;
110 112
     nodei_spec: LustreSpec.node_annot option;}
111

  
113
(*
112 114
type imported_fun_desc =
113 115
    {fun_id: ident;
114 116
     mutable fun_type: Types.type_expr;
115 117
     fun_inputs: var_decl list;
116 118
     fun_outputs: var_decl list;
117 119
     fun_spec: LustreSpec.node_annot option;}
118

  
120
*)
119 121
type const_desc = 
120 122
    {const_id: ident; 
121 123
     const_loc: Location.t; 
......
134 136
  | Node of node_desc
135 137
  | Consts of const_desc list
136 138
  | ImportedNode of imported_node_desc
137
  | ImportedFun of imported_fun_desc
139
  (* | ImportedFun of imported_fun_desc *)
138 140
  (* | SensorDecl of sensor_desc *)
139 141
  (* | ActuatorDecl of actuator_desc *)
140 142
  | Open of string
......
151 153
  | No_main_specified
152 154
  | Unbound_symbol of ident
153 155
  | Already_bound_symbol of ident
156
  | Stateful of ident
154 157

  
155
exception Error of error * Location.t
158
exception Error of Location.t * error
156 159

  
157 160
val mktyp: Location.t -> type_dec_desc -> type_dec
158 161
val mkclock: Location.t -> clock_dec_desc -> clock_dec
......
172 175
val node_inputs: top_decl -> var_decl list
173 176
val node_from_name: ident -> top_decl
174 177
val is_generic_node: top_decl -> bool
178
val check_stateless_node: top_decl -> bool
175 179
val is_imported_node: top_decl -> bool
176 180

  
177 181
val consts_table: (ident, const_desc) Hashtbl.t
......
203 207

  
204 208
val sort_handlers : (label * 'a) list -> (label * 'a) list
205 209

  
210
val is_stateless_expr: expr -> bool
206 211
val is_eq_expr: expr -> expr -> bool
207 212

  
208 213
val pp_error :  Format.formatter -> error -> unit
src/inliner.ml
209 209
	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
210 210
	  mkexpr loc (Expr_appl ("=", args, None))
211 211
      }];
212
    node_dec_stateless = true;
213
    node_stateless = None;
212 214
    node_spec = Some 
213 215
      {requires = []; 
214 216
       ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];
src/lexer_lustre.mll
40 40
  "last", LAST;
41 41
  "resume", RESUME;
42 42
  "restart", RESTART;
43
  "stateless", STATELESS;
44 43
  "if", IF;
45 44
  "then", THEN;
46 45
  "else", ELSE;
src/machine_code.ml
157 157
    node_checks = [];
158 158
    node_asserts = [];
159 159
    node_eqs= [];
160
    node_dec_stateless = false;
161
    node_stateless = Some false;
160 162
    node_spec = None;
161 163
    node_annot = None;  }
162 164

  
......
193 195
    mannot = None;
194 196
  }
195 197

  
196
let is_stateless_node node =
197
  (node_name node <> arrow_id) &&
198
    match node.top_decl_desc with
199
    | Node id -> false (* TODO: add a check after the machines are produced. Start from the main node and do a DFS to compute the stateless/statefull property of nodes. Stateless nodes should not be reset *)
200
    | ImportedNode id -> id.nodei_stateless
201
    | ImportedFun _ -> true
202
    | _       -> assert false
203

  
204 198
let new_instance =
205 199
  let cpt = ref (-1) in
206 200
  fun caller callee tag ->
207 201
    begin
208 202
      let o =
209
	if is_stateless_node callee then
203
	if Corelang.check_stateless_node callee then
210 204
	  node_name callee
211 205
	else
212 206
	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
......
220 214
let const_of_carrier cr =
221 215
 match (carrier_repr cr).carrier_desc with
222 216
 | Carry_const id -> id
223
 | Carry_name -> assert false
224
 | Carry_var -> assert false
225
 | Carry_link _ -> assert false (* TODO check this Xavier *)
217
 | Carry_name
218
 | Carry_var
219
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
226 220

  
227 221
(* translate_<foo> : node -> context -> <foo> -> machine code/expression *)
228 222
(* the context contains  m : state aka memory variables  *)
......
370 364
      NodeDep.filter_static_inputs (node_inputs node_f) el in 
371 365
    let o = new_instance node node_f eq.eq_rhs.expr_tag in
372 366
    (m,
373
     (if is_stateless_node node_f then si else MReset o :: si),
367
     (if check_stateless_node node_f then si else MReset o :: si),
374 368
     (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j),
375 369
     d,
376 370
     reset_instance node args o r eq.eq_rhs.expr_clock @
......
442 436
    mname = nd;
443 437
    mmemory = ISet.elements m;
444 438
    mcalls = mmap;
445
    minstances = List.filter (fun (_, (n,_)) -> not (is_stateless_node n)) mmap;
439
    minstances = List.filter (fun (_, (n,_)) -> not (check_stateless_node n)) mmap;
446 440
    minit = init;
447 441
    mstatic = List.filter (fun v -> v.var_dec_const) nd.node_inputs;
448 442
    mstep = {
src/main_lustre_compiler.ml
30 30

  
31 31
let extensions = [".ec"; ".lus"; ".lusi"]
32 32

  
33
let check_stateless_decls decls =
34
  report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@,@?");
35
  try
36
    List.iter (fun td -> ignore (Corelang.check_stateless_node td)) decls
37
  with (Corelang.Error (loc, err)) as exc ->
38
    Format.eprintf "Stateless status error at loc %a: %a@]@."
39
      Location.pp_loc loc
40
      Corelang.pp_error err;
41
    raise exc
42

  
33 43
let type_decls env decls =  
34 44
  report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?");
35 45
  let new_env = 
......
77 87
  | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 
78 88
    Parse.report_error err;
79 89
    raise exc
80
  | Corelang.Error (err, loc) as exc ->
90
  | Corelang.Error (loc, err) as exc ->
81 91
     Format.eprintf "Parsing error at loc %a: %a@]@."
82 92
       Location.pp_loc loc
83 93
       Corelang.pp_error err;
......
104 114
    | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> 
105 115
      Parse.report_error err;
106 116
      raise exc
107
    | Corelang.Error (err, loc) as exc ->
117
    | Corelang.Error (loc, err) as exc ->
108 118
      Format.eprintf "Parsing error at loc %a: %a@]@."
109 119
	Location.pp_loc loc
110 120
	Corelang.pp_error err;
......
141 151
  (* Sorting nodes *)
142 152
  let prog = SortProg.sort prog in
143 153
  
154
  (* Checking stateless/stateful status *)
155
  check_stateless_decls prog;
156

  
144 157
  (* Typing *)
145 158
  let computed_types_env = type_decls type_env prog in
146 159
  
......
192 205
      let _, declared_types_env, declared_clocks_env = check_lusi header in
193 206
      (* checking type compatibility with computed types*)
194 207
      Typing.check_env_compat header declared_types_env computed_types_env;
208
      Typing.uneval_prog_generics prog;
195 209
      (* checking clocks compatibility with computed clocks*)
196 210
      Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
197
      Typing.uneval_prog_generics prog;
198 211
      Clock_calculus.uneval_prog_generics prog
199 212
    with Sys_error _ -> ( 
200 213
      (* Printing lusi file is necessary *)
src/normalization.ml
196 196
  | Expr_uclock _
197 197
  | Expr_dclock _ 
198 198
  | Expr_phclock _ -> assert false (* Not handled yet *)
199

  
199
(* Creates a conditional with a merge construct, which is more lazy *)
200
(*
201
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
202
 match expr.expr_desc with
203
 | Expr_ite (c, t, e) ->
204
   let defvars, norm_t = norm_expr (alias node offsets defvars t in
205
 | _ -> assert false
206
*)
200 207
and normalize_branches node offsets defvars hl =
201 208
 List.fold_right
202 209
   (fun (t, h) (defvars, norm_q) ->
......
308 315
  match decl.top_decl_desc with
309 316
  | Node nd ->
310 317
    {decl with top_decl_desc = Node (normalize_node nd)}
311
  | Open _ | ImportedNode _ | ImportedFun _ | Consts _ -> decl
318
  | Open _ | ImportedNode _ | Consts _ -> decl
312 319
  
313 320
let normalize_prog decls = 
314 321
  List.map normalize_decl decls
src/parserLustreSpec.mly
189 189
| IDENT {
190 190
  try 
191 191
    mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1))
192
  with Not_found -> raise (Corelang.Error (Corelang.Unbound_symbol ("type " ^ $1), Location.symbol_rloc()))
192
  with Not_found -> raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1)))
193 193
}
194 194
| TFLOAT {mktyp Tydec_float}
195 195
| TREAL {mktyp Tydec_real}
src/parser_lustre.mly
51 51
    | ImportedNode _, _ ->
52 52
       Hashtbl.add hashtbl name value
53 53
    | Node _        , _ -> 
54
       raise (Corelang.Error (Corelang.Already_bound_symbol msg, Location.symbol_rloc ()))
54
       raise (Corelang.Error (Location.symbol_rloc (), Corelang.Already_bound_symbol msg))
55 55
    | _                 -> assert false
56 56
  with
57 57
    Not_found ->
......
59 59

  
60 60
let add_symbol msg hashtbl name value =
61 61
 if Hashtbl.mem hashtbl name
62
 then raise (Corelang.Error (Corelang.Already_bound_symbol msg, Location.symbol_rloc ()))
62
 then raise (Corelang.Error (Location.symbol_rloc (), Corelang.Already_bound_symbol msg))
63 63
 else Hashtbl.add hashtbl name value
64 64

  
65 65
let check_symbol msg hashtbl name =
66 66
 if not (Hashtbl.mem hashtbl name)
67
 then raise (Corelang.Error (Corelang.Unbound_symbol msg, Location.symbol_rloc ()))
67
 then raise (Corelang.Error (Location.symbol_rloc (), Corelang.Unbound_symbol msg))
68 68
 else ()
69 69

  
70 70
%}
......
143 143
  top_decl_header {(fun own -> [$1 own]) }
144 144
| top_decl_header_list top_decl_header {(fun own -> ($2 own)::($1 own)) }
145 145

  
146
state_annot:
147
  FUNCTION { true }
148
| NODE { false }
146 149

  
147 150
top_decl_header:
148
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
149
    {let nd = mktop_decl (ImportedNode
150
                            {nodei_id = $2;
151
                             nodei_type = Types.new_var ();
152
                             nodei_clock = Clocks.new_var true;
153
                             nodei_inputs = List.rev $4;
154
                             nodei_outputs = List.rev $9;
155
			     nodei_stateless = $12;
156
			     nodei_spec = None})
157
    in
158
    (fun own -> add_node own ("node " ^ $2) node_table $2 nd; nd) }
159

  
160
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
151
  nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
161 152
    {let nd = mktop_decl (ImportedNode
162 153
                            {nodei_id = $3;
163 154
                             nodei_type = Types.new_var ();
164 155
                             nodei_clock = Clocks.new_var true;
165 156
                             nodei_inputs = List.rev $5;
166 157
                             nodei_outputs = List.rev $10;
167
			     nodei_stateless = $13;
168
			     nodei_spec = Some $1})
158
			     nodei_stateless = $2;
159
			     nodei_spec = $1})
169 160
    in
170 161
    (fun own -> add_node own ("node " ^ $3) node_table $3 nd; nd) }
171 162

  
172
| FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
173
    {let nd = mktop_decl (ImportedNode
174
                            {nodei_id = $2;
175
                             nodei_type = Types.new_var ();
176
			     nodei_clock = Clocks.new_var true;
177
                             nodei_inputs = List.rev $4;
178
                             nodei_outputs = List.rev $9;
179
			     nodei_stateless = true;
180
			     nodei_spec = None})
181
     in
182
     (fun own -> add_node own ("function " ^ $2) node_table $2 nd; nd) }
183

  
184
| nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
185
    {let nd = mktop_decl (ImportedNode
186
                            {nodei_id = $3;
187
                             nodei_type = Types.new_var ();
188
			     nodei_clock = Clocks.new_var true;
189
                             nodei_inputs = List.rev $5;
190
                             nodei_outputs = List.rev $10;
191
			     nodei_stateless = true;
192
			     nodei_spec = Some $1})
193
     in
194
    (fun own -> add_node own ("function " ^ $3) node_table $3 nd; nd) }
195

  
196 163
top_decl:
197 164
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
198

  
199
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
200
    {let eqs, asserts, annots = $15 in
201
     let nd = mktop_decl (Node
202
                            {node_id = $2;
203
                             node_type = Types.new_var ();
204
                             node_clock = Clocks.new_var true;
205
                             node_inputs = List.rev $4;
206
                             node_outputs = List.rev $9;
207
                             node_locals = List.rev $13;
208
			     node_gencalls = [];
209
			     node_checks = [];
210
			     node_asserts = asserts; 
211
                             node_eqs = eqs;
212
			     node_spec = None;
213
			     node_annot = match annots with [] -> None | _ -> Some annots})
214
    in
215
    add_node true ("node " ^ $2) node_table $2 nd; nd}
216

  
217
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
165
| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL 
218 166
    {let eqs, asserts, annots = $16 in
219 167
     let nd = mktop_decl (Node
220 168
                            {node_id = $3;
......
227 175
			     node_checks = [];
228 176
			     node_asserts = asserts; 
229 177
                             node_eqs = eqs;
230
			     node_spec = Some $1;
178
			     node_dec_stateless = $2;
179
			     node_stateless = None;
180
			     node_spec = $1;
231 181
			     node_annot = match annots with [] -> None | _ -> Some annots})
232 182
    in
233 183
    add_node true ("node " ^ $3) node_table $3 nd; nd}
234 184

  
235 185
nodespec_list:
236
NODESPEC { $1 }
237
| NODESPEC nodespec_list { LustreSpec.merge_node_annot $1 $2 }
238

  
239
stateless_opt:
240
   { false }
241
| STATELESS {true}
186
 { None }
187
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 }
242 188

  
243 189
typ_def_list:
244 190
    /* empty */ {}
src/printers.ml
224 224
  ()
225 225

  
226 226
let pp_node fmt nd = 
227
fprintf fmt "@[<v 0>%a%tnode %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[%a@]@ @]@.tel@]@."
227
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[%a@]@ @]@.tel@]@."
228 228
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
229
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") 
229
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
230
  (if nd.node_dec_stateless then "function" else "node")
230 231
  nd.node_id
231 232
  pp_node_args nd.node_inputs
232 233
  pp_node_args nd.node_outputs
......
248 249
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
249 250

  
250 251
let pp_imported_node fmt ind = 
251
  fprintf fmt "@[<v>node %s (%a) returns (%a) %t@]"
252
  fprintf fmt "@[<v>%s %s (%a) returns (%a) %t@]"
253
    (if ind.nodei_stateless then "function" else "node")
252 254
    ind.nodei_id
253 255
    pp_node_args ind.nodei_inputs
254 256
    pp_node_args ind.nodei_outputs
255 257
    (fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless") 
256 258

  
257
let pp_imported_fun fmt ind = 
258
  fprintf fmt "@[<v>function %s (%a) returns (%a)@]"
259
    ind.fun_id
260
    pp_node_args ind.fun_inputs
261
    pp_node_args ind.fun_outputs
262

  
263 259
let pp_decl fmt decl =
264 260
  match decl.top_decl_desc with
265 261
  | Node nd -> fprintf fmt "%a@ " pp_node nd
266 262
  | ImportedNode ind ->
267 263
    fprintf fmt "imported %a;@ " pp_imported_node ind
268
  | ImportedFun ind ->
269
    fprintf fmt "%a;@ " pp_imported_fun ind
270 264
  | Consts clist -> (
271 265
    fprintf fmt "const %a@ " 
272 266
      (fprintf_list ~sep:"@ " (fun fmt cdecl ->
......
282 276
  match decl.top_decl_desc with
283 277
  | Node nd -> fprintf fmt "node %s@ " nd.node_id
284 278
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
285
  | ImportedFun ind -> fprintf fmt "function %s" ind.fun_id
286 279
  | Consts clist -> (
287 280
    fprintf fmt "const %a@ " 
288 281
      (fprintf_list ~sep:"@ " (fun fmt cdecl ->
......
297 290
      nd.node_id
298 291
      pp_node_args nd.node_inputs
299 292
      pp_node_args nd.node_outputs
300
  | ImportedNode _ | ImportedFun _ | Consts _ | Open _ -> ()
293
  | ImportedNode _ | Consts _ | Open _ -> ()
301 294

  
302 295

  
303 296

  
src/typing.ml
284 284
    if List.map fst tl1 <> List.map fst tl2
285 285
    then raise (Unify (ty1, ty2))
286 286
    else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2
287
  | Tclock t1          , Tclock t2          -> sub_unify sub t1 t2
288
  | Tclock t1          , _   when sub       -> sub_unify sub t1 ty2
287 289
  | Tstatic (d1, t1)   , Tstatic (d2, t2)   ->
288 290
    begin
289 291
      sub_unify sub t1 t2;
......
291 293
      Dimension.eval Basic_library.eval_env (fun c -> None) d2;
292 294
      Dimension.unify d1 d2
293 295
    end
294
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub ty2 t1
295
  | _                                       -> unify ty2 ty1
296
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub t1 ty2
297
  | _                                       -> unify ty1 ty2
296 298

  
297 299
let try_sub_unify sub ty1 ty2 loc =
298 300
  try
......
387 389
	 | Some d' -> try_unify real_type real_static_type loc);
388 390
	 real_static_type
389 391
    else real_type in
390
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
392
  (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
391 393
  try_sub_unify sub real_type formal_type loc
392
(*
393
and type_subtyping_tuple loc real_type formal_type =
394
  let real_types   = type_list_of_type real_type in
395
  let formal_types = type_list_of_type formal_type in
396
  if (List.length real_types) <> (List.length formal_types)
397
  then raise (Unify (real_type, formal_type))
398
  else List.iter2 (type_subtyping loc sub) real_types formal_types
399

  
400
and type_subtyping loc sub real_type formal_type =
401
  match (repr real_type).tdesc, (repr formal_type).tdesc with
402
  | Tstatic _          , Tstatic _ when sub -> try_unify formal_type real_type loc
403
  | Tstatic (r_d, r_ty), _         when sub -> try_unify formal_type r_ty loc
404
  | _                                       -> try_unify formal_type real_type loc
405
*)
394

  
406 395
and type_ident env in_main loc const id =
407 396
  type_expr env in_main const (expr_of_ident id loc)
408 397

  
......
691 680
  nd.nodei_type <- ty_node;
692 681
  new_env
693 682

  
694
let type_imported_fun env nd loc =
695
  let new_env = type_var_decl_list nd.fun_inputs env nd.fun_inputs in
696
  let vd_env =  nd.fun_inputs@nd.fun_outputs in
697
  check_vd_env vd_env;
698
  ignore(type_var_decl_list vd_env new_env nd.fun_outputs);
699
  let ty_ins = type_of_vlist nd.fun_inputs in
700
  let ty_outs = type_of_vlist nd.fun_outputs in
701
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
702
  generalize ty_node;
703
(*
704
  if (is_polymorphic ty_node) then
705
    raise (Error (loc, Poly_imported_node nd.fun_id));
706
*)
707
  let new_env = Env.add_value env nd.fun_id ty_node in
708
  nd.fun_type <- ty_node;
709
  new_env
710

  
711 683
let type_top_consts env clist =
712 684
  List.fold_left (fun env cdecl ->
713 685
    let ty = type_const cdecl.const_loc cdecl.const_value in
......
734 706
  )
735 707
  | ImportedNode nd ->
736 708
      type_imported_node env nd decl.top_decl_loc
737
  | ImportedFun nd ->
738
      type_imported_fun env nd decl.top_decl_loc
739 709
  | Consts clist ->
740 710
      type_top_consts env clist
741 711
  | Open _  -> env
......
769 739
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
770 740
  | ImportedNode nd ->
771 741
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
772
  | ImportedFun nd ->
773
      ()
774 742
  | Consts clist -> ()
775 743
  | Open _  -> ()
776 744

  

Also available in: Unified diff