Revision d3e4c22f
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