## 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