Revision f22632aa
src/basic_library.ml | ||
---|---|---|
35 | 35 |
type_static (mkdim_var ()) ty |
36 | 36 |
|
37 | 37 |
let type_env = |
38 |
let init_env = TE.initial in |
|
39 |
let env' = TE.add_value init_env "+" (static_op type_bin_poly_op) in |
|
40 |
let env' = TE.add_value env' "uminus" (static_op type_unary_poly_op) in |
|
41 |
let env' = TE.add_value env' "-" (static_op type_bin_poly_op) in |
|
42 |
let env' = TE.add_value env' "*" (static_op type_bin_poly_op) in |
|
43 |
let env' = TE.add_value env' "/" (static_op type_bin_poly_op) in |
|
44 |
let env' = TE.add_value env' "mod" (static_op type_bin_int_op) in |
|
45 |
let env' = TE.add_value env' "&&" (static_op type_bin_bool_op) in |
|
46 |
let env' = TE.add_value env' "||" (static_op type_bin_bool_op) in |
|
47 |
let env' = TE.add_value env' "xor" (static_op type_bin_bool_op) in |
|
48 |
let env' = TE.add_value env' "impl" (static_op type_bin_bool_op) in |
|
49 |
let env' = TE.add_value env' "<" (static_op type_bin_comp_op) in |
|
50 |
let env' = TE.add_value env' "<=" (static_op type_bin_comp_op) in |
|
51 |
let env' = TE.add_value env' ">" (static_op type_bin_comp_op) in |
|
52 |
let env' = TE.add_value env' ">=" (static_op type_bin_comp_op) in |
|
53 |
let env' = TE.add_value env' "!=" (static_op type_bin_comp_op) in |
|
54 |
let env' = TE.add_value env' "=" (static_op type_bin_comp_op) in |
|
55 |
let env' = TE.add_value env' "not" (static_op type_unary_bool_op) in |
|
56 |
env' |
|
57 |
|
|
38 |
List.fold_left |
|
39 |
(fun env (op, op_type) -> TE.add_value env op op_type) |
|
40 |
TE.initial |
|
41 |
[ |
|
42 |
"+", (static_op type_bin_poly_op); |
|
43 |
"uminus", (static_op type_unary_poly_op); |
|
44 |
"-", (static_op type_bin_poly_op); |
|
45 |
"*", (static_op type_bin_poly_op); |
|
46 |
"/", (static_op type_bin_poly_op); |
|
47 |
"mod", (static_op type_bin_int_op); |
|
48 |
"&&", (static_op type_bin_bool_op); |
|
49 |
"||", (static_op type_bin_bool_op); |
|
50 |
"xor", (static_op type_bin_bool_op); |
|
51 |
"impl", (static_op type_bin_bool_op); |
|
52 |
"<", (static_op type_bin_comp_op); |
|
53 |
"<=", (static_op type_bin_comp_op); |
|
54 |
">", (static_op type_bin_comp_op); |
|
55 |
">=", (static_op type_bin_comp_op); |
|
56 |
"!=", (static_op type_bin_comp_op); |
|
57 |
"=", (static_op type_bin_comp_op); |
|
58 |
"not", (static_op type_unary_bool_op) |
|
59 |
] |
|
60 |
|
|
58 | 61 |
module CE = Env |
59 | 62 |
|
60 | 63 |
let clock_env = |
... | ... | |
85 | 88 |
module VE = Env |
86 | 89 |
|
87 | 90 |
let eval_env = |
88 |
let init_env = VE.initial in |
|
89 |
let env' = VE.add_value init_env "uminus" (fun [Dint a] -> Dint (-a)) in |
|
90 |
let env' = VE.add_value env' "not" (fun [Dbool b] -> Dbool (not b)) in |
|
91 |
let env' = VE.add_value env' "+" (fun [Dint a; Dint b] -> Dint (a+b)) in |
|
92 |
let env' = VE.add_value env' "-" (fun [Dint a; Dint b] -> Dint (a-b)) in |
|
93 |
let env' = VE.add_value env' "*" (fun [Dint a; Dint b] -> Dint (a*b)) in |
|
94 |
let env' = VE.add_value env' "/" (fun [Dint a; Dint b] -> Dint (a/b)) in |
|
95 |
let env' = VE.add_value env' "mod" (fun [Dint a; Dint b] -> Dint (a mod b)) in |
|
96 |
let env' = VE.add_value env' "&&" (fun [Dbool a; Dbool b] -> Dbool (a&&b)) in |
|
97 |
let env' = VE.add_value env' "||" (fun [Dbool a; Dbool b] -> Dbool (a||b)) in |
|
98 |
let env' = VE.add_value env' "xor" (fun [Dbool a; Dbool b] -> Dbool (a<>b)) in |
|
99 |
let env' = VE.add_value env' "impl" (fun [Dbool a; Dbool b] -> Dbool (a<=b)) in |
|
100 |
let env' = VE.add_value env' "<" (fun [Dint a; Dint b] -> Dbool (a<b)) in |
|
101 |
let env' = VE.add_value env' ">" (fun [Dint a; Dint b] -> Dbool (a>b)) in |
|
102 |
let env' = VE.add_value env' "<=" (fun [Dint a; Dint b] -> Dbool (a<=b)) in |
|
103 |
let env' = VE.add_value env' ">=" (fun [Dint a; Dint b] -> Dbool (a>=b)) in |
|
104 |
let env' = VE.add_value env' "!=" (fun [a; b] -> Dbool (a<>b)) in |
|
105 |
let env' = VE.add_value env' "=" (fun [a; b] -> Dbool (a=b)) in |
|
106 |
env' |
|
91 |
let defs = [ |
|
92 |
"uminus", (function [Dint a] -> Dint (-a) | _ -> assert false); |
|
93 |
"not", (function [Dbool b] -> Dbool (not b) | _ -> assert false); |
|
94 |
"+", (function [Dint a; Dint b] -> Dint (a+b) | _ -> assert false); |
|
95 |
"-", (function [Dint a; Dint b] -> Dint (a-b) | _ -> assert false); |
|
96 |
"*", (function [Dint a; Dint b] -> Dint (a*b) | _ -> assert false); |
|
97 |
"/", (function [Dint a; Dint b] -> Dint (a/b) | _ -> assert false); |
|
98 |
"mod", (function [Dint a; Dint b] -> Dint (a mod b) | _ -> assert false); |
|
99 |
"&&", (function [Dbool a; Dbool b] -> Dbool (a&&b) | _ -> assert false); |
|
100 |
"||", (function [Dbool a; Dbool b] -> Dbool (a||b) | _ -> assert false); |
|
101 |
"xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false); |
|
102 |
"impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false); |
|
103 |
"<", (function [Dint a; Dint b] -> Dbool (a<b) | _ -> assert false); |
|
104 |
">", (function [Dint a; Dint b] -> Dbool (a>b) | _ -> assert false); |
|
105 |
"<=", (function [Dint a; Dint b] -> Dbool (a<=b) | _ -> assert false); |
|
106 |
">=", (function [Dint a; Dint b] -> Dbool (a>=b) | _ -> assert false); |
|
107 |
"!=", (function [a; b] -> Dbool (a<>b) | _ -> assert false); |
|
108 |
"=", (function [a; b] -> Dbool (a=b) | _ -> assert false); |
|
109 |
] |
|
110 |
in |
|
111 |
List.fold_left |
|
112 |
(fun env (op, op_eval) -> VE.add_value env op op_eval) |
|
113 |
VE.initial |
|
114 |
defs |
|
107 | 115 |
|
108 | 116 |
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"] |
109 | 117 |
|
src/c_backend.ml | ||
---|---|---|
432 | 432 |
(* Header Printing functions *) |
433 | 433 |
(********************************************************************************************) |
434 | 434 |
|
435 |
(* Removed because of "open" constructs. No more extern functions *) |
|
436 |
(* |
|
435 | 437 |
let print_prototype fmt decl = |
436 | 438 |
match decl.top_decl_desc with |
437 | 439 |
| ImportedFun m -> ( |
... | ... | |
455 | 457 |
) |
456 | 458 |
) |
457 | 459 |
| _ -> () (* We don't do anything here *) |
460 |
*) |
|
458 | 461 |
|
462 |
let print_prototype fmt decl = |
|
463 |
match decl.top_decl_desc with |
|
464 |
| Open m -> fprintf fmt "#include \"%s.h\"@," m |
|
465 |
| _ -> () (* We don't do anything here *) |
|
466 |
|
|
459 | 467 |
let pp_registers_struct fmt m = |
460 | 468 |
if m.mmemory <> [] |
461 | 469 |
then |
... | ... | |
762 | 770 |
(pp_c_type_decl cpt_type var) def |
763 | 771 |
| _ -> ()) type_table |
764 | 772 |
|
773 |
let print_makefile basename nodename fmt = |
|
774 |
fprintf fmt "GCC=gcc@."; |
|
775 |
fprintf fmt "INC=/usr/local/include/lustrec@."; |
|
776 |
fprintf fmt "@."; |
|
777 |
fprintf fmt "main:@."; |
|
778 |
fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename; |
|
779 |
fprintf fmt "\t${GCC} -I${INC} -c ${INC}/io_frontend.c@."; |
|
780 |
fprintf fmt "\t${GCC} -I${INC} -c ${INC}/StdLibrary.c@."; |
|
781 |
fprintf fmt "\t${GCC} -o %s_%s io_frontend.o StdLibrary.o -lm %s.o@." basename nodename basename |
|
782 |
|
|
765 | 783 |
(********************************************************************************************) |
766 | 784 |
(* Translation function *) |
767 | 785 |
(********************************************************************************************) |
768 | 786 |
|
769 |
let translate_to_c header_fmt source_fmt spec_fmt_opt basename prog machines = |
|
787 |
let translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename prog machines =
|
|
770 | 788 |
(* Generating H file *) |
771 | 789 |
|
772 | 790 |
(* Include once: start *) |
... | ... | |
795 | 813 |
(* Generating C file *) |
796 | 814 |
|
797 | 815 |
(* If a main node is identified, generate a main function for it *) |
798 |
let main_include, main_print = |
|
816 |
let main_include, main_print, main_makefile =
|
|
799 | 817 |
match !Options.main_node with |
800 |
| "" -> (fun _ -> ()), (fun _ -> ()) |
|
818 |
| "" -> (fun _ -> ()), (fun _ -> ()), (fun _ -> ())
|
|
801 | 819 |
| main_node -> ( |
802 | 820 |
let main_node_opt = |
803 | 821 |
List.fold_left |
... | ... | |
808 | 826 |
None machines |
809 | 827 |
in |
810 | 828 |
match main_node_opt with |
811 |
| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()), (fun _ -> ()) |
|
812 |
| Some m -> print_main_header, print_main_fun machines m |
|
829 |
| None -> eprintf "Unable to find a main node named %s@.@?" main_node; (fun _ -> ()), (fun _ -> ()), (fun _ -> ())
|
|
830 |
| Some m -> print_main_header, print_main_fun machines m, print_makefile basename !Options.main_node
|
|
813 | 831 |
) |
814 | 832 |
in |
815 | 833 |
main_include source_fmt; |
... | ... | |
829 | 847 |
pp_print_newline source_fmt (); |
830 | 848 |
(* Print nodes one by one (in the previous order) *) |
831 | 849 |
List.iter (print_machine source_fmt) machines; |
832 |
main_print source_fmt |
|
833 |
|
|
834 |
|
|
835 |
|
|
850 |
main_print source_fmt; |
|
836 | 851 |
|
852 |
(* Generating Makefile *) |
|
853 |
main_makefile makefile_fmt |
|
837 | 854 |
|
838 | 855 |
(* Local Variables: *) |
839 | 856 |
(* compile-command:"make -C .." *) |
src/clock_calculus.ml | ||
---|---|---|
769 | 769 |
clock_function env decl.top_decl_loc fcn |
770 | 770 |
| Consts clist -> |
771 | 771 |
clock_top_consts env clist |
772 |
| Include _ ->
|
|
772 |
| Open _ ->
|
|
773 | 773 |
env |
774 | 774 |
|
775 | 775 |
let clock_prog env decls = |
776 |
ignore(List.fold_left (fun e decl -> clock_top_decl e decl) env decls) |
|
777 |
|
|
776 |
List.fold_left (fun e decl -> clock_top_decl e decl) env decls |
|
778 | 777 |
|
778 |
let check_env_compat declared computed = |
|
779 |
Env.iter declared (fun k decl_clock_k -> |
|
780 |
let computed_c = Env.lookup_value computed k in |
|
781 |
try_unify decl_clock_k computed_c Location.dummy_loc |
|
782 |
) |
|
779 | 783 |
(* Local Variables: *) |
780 | 784 |
(* compile-command:"make -C .." *) |
781 | 785 |
(* End: *) |
src/corelang.ml | ||
---|---|---|
136 | 136 |
| Consts of const_desc list |
137 | 137 |
| ImportedNode of imported_node_desc |
138 | 138 |
| ImportedFun of imported_fun_desc |
139 |
| Include of string
|
|
139 |
| Open of string
|
|
140 | 140 |
|
141 | 141 |
type top_decl = |
142 | 142 |
{top_decl_desc: top_decl_desc; |
... | ... | |
493 | 493 |
fun consts decl -> |
494 | 494 |
match decl.top_decl_desc with |
495 | 495 |
| Consts clist -> clist@consts |
496 |
| Node _ | ImportedNode _ | ImportedFun _ | Include _ -> consts
|
|
496 |
| Node _ | ImportedNode _ | ImportedFun _ | Open _ -> consts
|
|
497 | 497 |
) [] prog |
498 | 498 |
|
499 | 499 |
|
... | ... | |
502 | 502 |
fun nodes decl -> |
503 | 503 |
match decl.top_decl_desc with |
504 | 504 |
| Node nd -> nd::nodes |
505 |
| Consts _ | ImportedNode _ | ImportedFun _ | Include _ -> nodes
|
|
505 |
| Consts _ | ImportedNode _ | ImportedFun _ | Open _ -> nodes
|
|
506 | 506 |
) [] prog |
507 | 507 |
|
508 | 508 |
let prog_unfold_consts prog = |
... | ... | |
587 | 587 |
fprintf fmt "%s: " ind.fun_id; |
588 | 588 |
Utils.reset_names (); |
589 | 589 |
fprintf fmt "%a@ " Types.print_ty ind.fun_type |
590 |
| Consts _ | Include _ -> ()
|
|
590 |
| Consts _ | Open _ -> ()
|
|
591 | 591 |
|
592 | 592 |
let pp_prog_type fmt tdecl_list = |
593 | 593 |
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list |
... | ... | |
600 | 600 |
fprintf fmt "%a@ " Clocks.print_ck nd.node_clock |
601 | 601 |
| ImportedNode ind -> |
602 | 602 |
fprintf fmt "%s: " ind.nodei_id; |
603 |
Utils.reset_names ();
|
|
604 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
|
|
605 |
| ImportedFun _ | Consts _ | Include _ -> ()
|
|
603 |
Utils.reset_names (); |
|
604 |
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock |
|
605 |
| ImportedFun _ | Consts _ | Open _ -> ()
|
|
606 | 606 |
|
607 | 607 |
let pp_prog_clock fmt prog = |
608 | 608 |
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog |
src/corelang.mli | ||
---|---|---|
133 | 133 |
| ImportedFun of imported_fun_desc |
134 | 134 |
(* | SensorDecl of sensor_desc *) |
135 | 135 |
(* | ActuatorDecl of actuator_desc *) |
136 |
| Include of string
|
|
136 |
| Open of string
|
|
137 | 137 |
|
138 | 138 |
type top_decl = |
139 | 139 |
{top_decl_desc: top_decl_desc; |
src/env.ml | ||
---|---|---|
36 | 36 |
let exists_value env ident = |
37 | 37 |
IMap.mem ident env |
38 | 38 |
|
39 |
let iter env f = IMap.iter f env |
|
40 |
|
|
39 | 41 |
let overwrite x y = |
40 | 42 |
IMap.merge ( |
41 | 43 |
fun k _old _new -> match _new with |
src/lexer_lustre.mll | ||
---|---|---|
72 | 72 |
"pre", PRE; |
73 | 73 |
"div", DIV; |
74 | 74 |
"const", CONST; |
75 |
"include", INCLUDE;
|
|
75 |
"open", OPEN;
|
|
76 | 76 |
"assert", ASSERT; |
77 | 77 |
] |
78 | 78 |
|
src/main_lustre_compiler.ml | ||
---|---|---|
30 | 30 |
|
31 | 31 |
let extensions = [".ec";".lus"] |
32 | 32 |
|
33 |
let type_decls env decls = |
|
34 |
report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?"); |
|
35 |
let new_env = |
|
36 |
begin |
|
37 |
try |
|
38 |
Typing.type_prog env decls |
|
39 |
(*Typing.uneval_prog_generics prog*) |
|
40 |
with (Types.Error (loc,err)) as exc -> |
|
41 |
Format.eprintf "Typing error at loc %a: %a@]@." |
|
42 |
Location.pp_loc loc |
|
43 |
Types.pp_error err; |
|
44 |
raise exc |
|
45 |
end |
|
46 |
in |
|
47 |
if !Options.print_types then |
|
48 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_type decls); |
|
49 |
new_env |
|
50 |
|
|
51 |
let clock_decls env decls = |
|
52 |
report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@,@?"); |
|
53 |
let new_env = |
|
54 |
begin |
|
55 |
try |
|
56 |
Clock_calculus.clock_prog env decls |
|
57 |
with (Clocks.Error (loc,err)) as exc -> |
|
58 |
Location.print loc; |
|
59 |
eprintf "Clock calculus error at loc %a: %a@]@." Location.pp_loc loc Clocks.pp_error err; |
|
60 |
raise exc |
|
61 |
end |
|
62 |
in |
|
63 |
if !Options.print_clocks then |
|
64 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_clock decls); |
|
65 |
new_env |
|
66 |
|
|
67 |
(* Loading Lusi file and filing type tables with parsed |
|
68 |
functions/nodes *) |
|
69 |
let load_lusi filename = |
|
70 |
Location.input_name := filename; |
|
71 |
let lexbuf = Lexing.from_channel (open_in filename) in |
|
72 |
Location.init lexbuf filename; |
|
73 |
(* Parsing *) |
|
74 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing header file %s@,@?" filename); |
|
75 |
let header = |
|
76 |
try |
|
77 |
Parse.prog Parser_lustre.header Lexer_lustre.token lexbuf |
|
78 |
with (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc -> |
|
79 |
Parse.report_error err; |
|
80 |
raise exc |
|
81 |
in |
|
82 |
let new_tenv = type_decls Basic_library.type_env header in (* Typing *) |
|
83 |
let new_cenv: Clocks.clock_expr Utils.IMap.t = clock_decls Basic_library.clock_env header in (* Clock calculus *) |
|
84 |
header, new_tenv, new_cenv |
|
85 |
|
|
86 |
|
|
33 | 87 |
let rec compile basename extension = |
88 |
(* Loading the input file *) |
|
34 | 89 |
let source_name = basename^extension in |
35 | 90 |
Location.input_name := source_name; |
36 | 91 |
let lexbuf = Lexing.from_channel (open_in source_name) in |
37 | 92 |
Location.init lexbuf source_name; |
38 | 93 |
(* Parsing *) |
39 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v>.. parsing file %s@,@?" source_name); |
|
94 |
report ~level:1 |
|
95 |
(fun fmt -> fprintf fmt "@[<v>.. parsing file %s@,@?" source_name); |
|
40 | 96 |
let prog = |
41 | 97 |
try |
42 | 98 |
Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf |
... | ... | |
44 | 100 |
Parse.report_error err; |
45 | 101 |
raise exc |
46 | 102 |
in |
47 |
(* Extract includes *)
|
|
48 |
report ~level:1 (fun fmt -> fprintf fmt ".. extracting includes@,@?");
|
|
49 |
let includes =
|
|
103 |
(* Extracting dependencies *)
|
|
104 |
report ~level:1 (fun fmt -> fprintf fmt ".. extracting dependencies@,@?");
|
|
105 |
let dependencies =
|
|
50 | 106 |
List.fold_right |
51 |
(fun d accu -> match d.Corelang.top_decl_desc with | Corelang.Include s -> s::accu | _ -> accu) |
|
107 |
(fun d accu -> match d.Corelang.top_decl_desc with |
|
108 |
| Corelang.Open s -> s::accu |
|
109 |
| _ -> accu) |
|
52 | 110 |
prog [] |
53 | 111 |
in |
54 |
List.iter (fun s -> let basename = Filename.chop_suffix s ".lus" in |
|
55 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ "); |
|
56 |
compile basename ".lus"; |
|
57 |
report ~level:1 (fun fmt -> fprintf fmt "@]@,@?") |
|
58 |
|
|
59 |
) includes; |
|
112 |
let type_env, clock_env = |
|
113 |
List.fold_left (fun (type_env, clock_env) s -> |
|
114 |
try |
|
115 |
let basename = s ^ ".lusi" in |
|
116 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>Library %s@ " s); |
|
117 |
let _, lusi_type_env, lusi_clock_env = load_lusi basename in |
|
118 |
report ~level:1 (fun fmt -> fprintf fmt "@]@,@?"); |
|
119 |
Env.overwrite type_env lusi_type_env, |
|
120 |
Env.overwrite clock_env lusi_clock_env |
|
121 |
with Sys_error msg -> ( |
|
122 |
Format.eprintf "Failure: impossible to load library %s.@.%s@." s msg; |
|
123 |
exit 1 |
|
124 |
) |
|
125 |
) (Basic_library.type_env, Basic_library.clock_env) dependencies |
|
126 |
in |
|
127 |
|
|
60 | 128 |
(* Unfold consts *) |
61 | 129 |
(*let prog = Corelang.prog_unfold_consts prog in*) |
62 | 130 |
|
63 | 131 |
(* Sorting nodes *) |
64 | 132 |
let prog = SortProg.sort prog in |
65 |
|
|
133 |
|
|
66 | 134 |
(* Typing *) |
67 |
report ~level:1 (fun fmt -> fprintf fmt ".. typing@,@?"); |
|
68 |
begin |
|
69 |
try |
|
70 |
Typing.type_prog Basic_library.type_env prog |
|
71 |
(*Typing.uneval_prog_generics prog*) |
|
72 |
with (Types.Error (loc,err)) as exc -> |
|
73 |
Format.eprintf "Typing error at loc %a: %a@]@." |
|
74 |
Location.pp_loc loc |
|
75 |
Types.pp_error err; |
|
76 |
raise exc |
|
77 |
end; |
|
78 |
if !Options.print_types then |
|
79 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_type prog); |
|
135 |
let computed_types_env = type_decls type_env prog in |
|
80 | 136 |
|
81 | 137 |
(* Clock calculus *) |
82 |
report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@,@?"); |
|
83 |
begin |
|
84 |
try |
|
85 |
Clock_calculus.clock_prog Basic_library.clock_env prog |
|
86 |
with (Clocks.Error (loc,err)) as exc -> |
|
87 |
Location.print loc; |
|
88 |
eprintf "Clock calculus error at loc %a: %a@]@." Location.pp_loc loc Clocks.pp_error err; |
|
89 |
raise exc |
|
90 |
end; |
|
91 |
if !Options.print_clocks then |
|
92 |
report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" Corelang.pp_prog_clock prog); |
|
138 |
let computed_clocks_env = clock_decls clock_env prog in |
|
93 | 139 |
|
94 | 140 |
(* Delay calculus *) |
95 |
(* |
|
96 |
if(!Options.delay_calculus) |
|
97 |
then |
|
141 |
(*
|
|
142 |
if(!Options.delay_calculus)
|
|
143 |
then
|
|
98 | 144 |
begin |
99 |
report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
|
|
100 |
try
|
|
101 |
Delay_calculus.delay_prog Basic_library.delay_env prog
|
|
102 |
with (Delay.Error (loc,err)) as exc ->
|
|
103 |
Location.print loc;
|
|
104 |
eprintf "%a" Delay.pp_error err;
|
|
105 |
Utils.track_exception ();
|
|
106 |
raise exc
|
|
145 |
report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?"); |
|
146 |
try |
|
147 |
Delay_calculus.delay_prog Basic_library.delay_env prog
|
|
148 |
with (Delay.Error (loc,err)) as exc -> |
|
149 |
Location.print loc;
|
|
150 |
eprintf "%a" Delay.pp_error err;
|
|
151 |
Utils.track_exception ();
|
|
152 |
raise exc
|
|
107 | 153 |
end; |
108 |
*) |
|
154 |
*)
|
|
109 | 155 |
(* |
110 | 156 |
eprintf "Causality analysis@.@?"; |
111 |
(* Causality analysis *) |
|
157 |
(* Causality analysis *)
|
|
112 | 158 |
begin |
113 | 159 |
try |
114 | 160 |
Causality.check_causal_prog prog |
... | ... | |
139 | 185 |
let machine_code = Machine_code.translate_prog normalized_prog in |
140 | 186 |
report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,@?" |
141 | 187 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
142 |
|
|
143 | 188 |
machine_code); |
144 | 189 |
|
190 |
(* Checking the existence of a lusi (Lustre Interface file) *) |
|
191 |
let lusi_name = basename ^ ".lusi" in |
|
192 |
let _ = |
|
193 |
try |
|
194 |
let _ = open_in lusi_name in |
|
195 |
let _, declared_types_env, declared_clocks_env = load_lusi lusi_name in |
|
196 |
(* checking type compatibilty with computed types*) |
|
197 |
Typing.check_env_compat declared_types_env computed_types_env; |
|
198 |
(* checking clocks compatibilty with computed clocks*) |
|
199 |
Clock_calculus.check_env_compat declared_clocks_env computed_clocks_env; |
|
200 |
|
|
201 |
with Sys_error _ -> ( |
|
202 |
(* Printing lusi file is necessary *) |
|
203 |
report ~level:1 |
|
204 |
(fun fmt -> |
|
205 |
fprintf fmt |
|
206 |
".. generating lustre interface file %s@,@?" lusi_name); |
|
207 |
let lusi_out = open_out lusi_name in |
|
208 |
let lusi_fmt = formatter_of_out_channel lusi_out in |
|
209 |
Printers.pp_lusi_header lusi_fmt source_name normalized_prog |
|
210 |
) |
|
211 |
| (Types.Error (loc,err)) as exc -> |
|
212 |
Format.eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@]@." |
|
213 |
Types.pp_error err; |
|
214 |
raise exc |
|
215 |
in |
|
216 |
|
|
145 | 217 |
(* Printing code *) |
146 | 218 |
let basename = Filename.basename basename in |
147 | 219 |
if !Options.java then |
148 | 220 |
failwith "Sorry, but not yet supported !" |
149 | 221 |
(*let source_file = basename ^ ".java" in |
150 |
report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file); |
|
151 |
let source_out = open_out source_file in |
|
152 |
let source_fmt = formatter_of_out_channel source_out in |
|
153 |
report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?"); |
|
154 |
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*) |
|
222 |
report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
|
|
223 |
let source_out = open_out source_file in
|
|
224 |
let source_fmt = formatter_of_out_channel source_out in
|
|
225 |
report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
|
|
226 |
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
|
|
155 | 227 |
else begin |
156 | 228 |
let header_file = basename ^ ".h" in (* Could be changed *) |
157 | 229 |
let source_file = basename ^ ".c" in (* Could be changed *) |
230 |
let makefile_file = basename ^ ".makefile" in (* Could be changed *) |
|
158 | 231 |
let spec_file_opt = if !Options.c_spec then |
159 | 232 |
( |
160 | 233 |
let spec_file = basename ^ "_spec.c" in |
... | ... | |
169 | 242 |
let header_fmt = formatter_of_out_channel header_out in |
170 | 243 |
let source_out = open_out source_file in |
171 | 244 |
let source_fmt = formatter_of_out_channel source_out in |
245 |
let makefile_out = open_out makefile_file in |
|
246 |
let makefile_fmt = formatter_of_out_channel makefile_out in |
|
172 | 247 |
let spec_fmt_opt = match spec_file_opt with |
173 | 248 |
None -> None |
174 | 249 |
| Some f -> Some (formatter_of_out_channel (open_out f)) |
175 | 250 |
in |
176 | 251 |
report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,@?"); |
177 |
C_backend.translate_to_c header_fmt source_fmt spec_fmt_opt basename normalized_prog machine_code; |
|
252 |
C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code;
|
|
178 | 253 |
end; |
179 | 254 |
report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
180 | 255 |
(* We stop the process here *) |
src/normalization.ml | ||
---|---|---|
308 | 308 |
match decl.top_decl_desc with |
309 | 309 |
| Node nd -> |
310 | 310 |
{decl with top_decl_desc = Node (normalize_node nd)} |
311 |
| Include _ | ImportedNode _ | ImportedFun _ | Consts _ -> decl
|
|
311 |
| Open _ | ImportedNode _ | ImportedFun _ | Consts _ -> decl
|
|
312 | 312 |
|
313 | 313 |
let normalize_prog decls = |
314 | 314 |
List.map normalize_decl decls |
src/parser_lustre.mly | ||
---|---|---|
48 | 48 |
%token <string> REAL |
49 | 49 |
%token <float> FLOAT |
50 | 50 |
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST |
51 |
%token STATELESS ASSERT INCLUDE QUOTE FUNCTION
|
|
51 |
%token STATELESS ASSERT OPEN QUOTE FUNCTION
|
|
52 | 52 |
%token <string> IDENT |
53 | 53 |
%token <LustreSpec.expr_annot> ANNOT |
54 | 54 |
%token <LustreSpec.node_annot> NODESPEC |
... | ... | |
91 | 91 |
|
92 | 92 |
%start prog |
93 | 93 |
%type <Corelang.top_decl list> prog |
94 |
%start header |
|
95 |
%type <Corelang.top_decl list> header |
|
94 | 96 |
|
95 | 97 |
%% |
96 | 98 |
|
97 | 99 |
prog: |
98 | 100 |
typ_def_list top_decl_list EOF {$1;(List.rev $2)} |
99 | 101 |
|
102 |
header: |
|
103 |
typ_def_list top_decl_header_list EOF {$1;(List.rev $2)} |
|
104 |
|
|
100 | 105 |
top_decl_list: |
101 | 106 |
top_decl {[$1]} |
102 | 107 |
| top_decl_list top_decl {$2::$1} |
103 | 108 |
|
104 |
top_decl: |
|
105 |
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) } |
|
106 | 109 |
|
107 |
| NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
108 |
{let eqs, asserts, annots = $14 in |
|
109 |
let nd = mktop_decl (Node |
|
110 |
{node_id = $2; |
|
111 |
node_type = Types.new_var (); |
|
112 |
node_clock = Clocks.new_var true; |
|
113 |
node_inputs = List.rev $4; |
|
114 |
node_outputs = List.rev $8; |
|
115 |
node_locals = List.rev $12; |
|
116 |
node_gencalls = []; |
|
117 |
node_checks = []; |
|
118 |
node_asserts = asserts; |
|
119 |
node_eqs = eqs; |
|
120 |
node_spec = None; |
|
121 |
node_annot = match annots with [] -> None | _ -> Some annots}) |
|
122 |
in |
|
123 |
Hashtbl.add node_table $2 nd; nd} |
|
110 |
top_decl_header_list: |
|
111 |
top_decl_header {[$1]} |
|
112 |
| top_decl_header_list top_decl_header {$2::$1} |
|
124 | 113 |
|
125 |
| nodespec_list NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
126 |
{let eqs, asserts, annots = $15 in |
|
127 |
let nd = mktop_decl (Node |
|
128 |
{node_id = $3; |
|
129 |
node_type = Types.new_var (); |
|
130 |
node_clock = Clocks.new_var true; |
|
131 |
node_inputs = List.rev $5; |
|
132 |
node_outputs = List.rev $9; |
|
133 |
node_locals = List.rev $13; |
|
134 |
node_gencalls = []; |
|
135 |
node_checks = []; |
|
136 |
node_asserts = asserts; |
|
137 |
node_eqs = eqs; |
|
138 |
node_spec = Some $1; |
|
139 |
node_annot = match annots with [] -> None | _ -> Some annots}) |
|
140 |
in |
|
141 |
Hashtbl.add node_table $3 nd; nd} |
|
142 | 114 |
|
143 |
| IMPORTED NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR stateless_opt SCOL |
|
115 |
top_decl_header: |
|
116 |
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL |
|
144 | 117 |
{let nd = mktop_decl (ImportedNode |
145 |
{nodei_id = $3;
|
|
118 |
{nodei_id = $2;
|
|
146 | 119 |
nodei_type = Types.new_var (); |
147 | 120 |
nodei_clock = Clocks.new_var true; |
148 |
nodei_inputs = List.rev $5;
|
|
121 |
nodei_inputs = List.rev $4;
|
|
149 | 122 |
nodei_outputs = List.rev $9; |
150 |
nodei_stateless = $11;
|
|
123 |
nodei_stateless = $12;
|
|
151 | 124 |
nodei_spec = None}) |
152 | 125 |
in |
153 |
Hashtbl.add node_table $3 nd; nd}
|
|
126 |
Hashtbl.add node_table $2 nd; nd}
|
|
154 | 127 |
|
155 |
| nodespec_list IMPORTED NODE IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR stateless_opt SCOL
|
|
128 |
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR stateless_opt SCOL
|
|
156 | 129 |
{let nd = mktop_decl (ImportedNode |
157 |
{nodei_id = $4;
|
|
130 |
{nodei_id = $3;
|
|
158 | 131 |
nodei_type = Types.new_var (); |
159 | 132 |
nodei_clock = Clocks.new_var true; |
160 |
nodei_inputs = List.rev $6;
|
|
133 |
nodei_inputs = List.rev $5;
|
|
161 | 134 |
nodei_outputs = List.rev $10; |
162 |
nodei_stateless = $12;
|
|
135 |
nodei_stateless = $13;
|
|
163 | 136 |
nodei_spec = Some $1}) |
164 | 137 |
in |
165 |
Hashtbl.add node_table $4 nd; nd}
|
|
138 |
Hashtbl.add node_table $3 nd; nd}
|
|
166 | 139 |
|
167 |
| FUNCTION IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR SCOL
|
|
140 |
| FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
|
|
168 | 141 |
{let nd = mktop_decl (ImportedNode |
169 | 142 |
{nodei_id = $2; |
170 | 143 |
nodei_type = Types.new_var (); |
171 | 144 |
nodei_clock = Clocks.new_var true; |
172 | 145 |
nodei_inputs = List.rev $4; |
173 |
nodei_outputs = List.rev $8;
|
|
146 |
nodei_outputs = List.rev $9;
|
|
174 | 147 |
nodei_stateless = true; |
175 | 148 |
nodei_spec = None}) |
176 | 149 |
in |
177 | 150 |
Hashtbl.add node_table $2 nd; nd} |
178 | 151 |
|
179 |
| nodespec_list FUNCTION IDENT LPAR vdecl_list RPAR RETURNS LPAR vdecl_list RPAR SCOL
|
|
152 |
| nodespec_list FUNCTION IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL
|
|
180 | 153 |
{let nd = mktop_decl (ImportedNode |
181 | 154 |
{nodei_id = $3; |
182 | 155 |
nodei_type = Types.new_var (); |
183 | 156 |
nodei_clock = Clocks.new_var true; |
184 | 157 |
nodei_inputs = List.rev $5; |
185 |
nodei_outputs = List.rev $9;
|
|
158 |
nodei_outputs = List.rev $10;
|
|
186 | 159 |
nodei_stateless = true; |
187 | 160 |
nodei_spec = Some $1}) |
188 | 161 |
in |
189 | 162 |
Hashtbl.add node_table $3 nd; nd} |
190 | 163 |
|
191 |
| INCLUDE QUOTE IDENT QUOTE { mktop_decl (Include $3) } |
|
164 |
top_decl: |
|
165 |
| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) } |
|
166 |
|
|
167 |
| NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
168 |
{let eqs, asserts, annots = $15 in |
|
169 |
let nd = mktop_decl (Node |
|
170 |
{node_id = $2; |
|
171 |
node_type = Types.new_var (); |
|
172 |
node_clock = Clocks.new_var true; |
|
173 |
node_inputs = List.rev $4; |
|
174 |
node_outputs = List.rev $9; |
|
175 |
node_locals = List.rev $13; |
|
176 |
node_gencalls = []; |
|
177 |
node_checks = []; |
|
178 |
node_asserts = asserts; |
|
179 |
node_eqs = eqs; |
|
180 |
node_spec = None; |
|
181 |
node_annot = match annots with [] -> None | _ -> Some annots}) |
|
182 |
in |
|
183 |
Hashtbl.add node_table $2 nd; nd} |
|
184 |
|
|
185 |
| nodespec_list NODE IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL |
|
186 |
{let eqs, asserts, annots = $16 in |
|
187 |
let nd = mktop_decl (Node |
|
188 |
{node_id = $3; |
|
189 |
node_type = Types.new_var (); |
|
190 |
node_clock = Clocks.new_var true; |
|
191 |
node_inputs = List.rev $5; |
|
192 |
node_outputs = List.rev $10; |
|
193 |
node_locals = List.rev $14; |
|
194 |
node_gencalls = []; |
|
195 |
node_checks = []; |
|
196 |
node_asserts = asserts; |
|
197 |
node_eqs = eqs; |
|
198 |
node_spec = Some $1; |
|
199 |
node_annot = match annots with [] -> None | _ -> Some annots}) |
|
200 |
in |
|
201 |
Hashtbl.add node_table $3 nd; nd} |
|
202 |
|
|
203 |
| OPEN QUOTE IDENT QUOTE { mktop_decl (Open $3) } |
|
192 | 204 |
|
193 | 205 |
nodespec_list: |
194 | 206 |
NODESPEC { $1 } |
src/printers.ml | ||
---|---|---|
185 | 185 |
(fprintf_list ~sep:"@ " (fun fmt cdecl -> |
186 | 186 |
fprintf fmt "%s = %a;" |
187 | 187 |
cdecl.const_id pp_const cdecl.const_value)) clist) |
188 |
| Include s -> fprintf fmt "include %s" s
|
|
188 |
| Open s -> fprintf fmt "open \"%s\"" s
|
|
189 | 189 |
|
190 | 190 |
|
191 | 191 |
let pp_prog fmt prog = |
... | ... | |
200 | 200 |
fprintf fmt "const %a@ " |
201 | 201 |
(fprintf_list ~sep:"@ " (fun fmt cdecl -> |
202 | 202 |
pp_print_string fmt cdecl.const_id)) clist) |
203 |
| Include s -> fprintf fmt "include %s" s |
|
204 |
|
|
203 |
| Open s -> fprintf fmt "open \"%s\"" s |
|
205 | 204 |
|
205 |
let pp_lusi fmt decl = |
|
206 |
match decl.top_decl_desc with |
|
207 |
| Node nd -> |
|
208 |
fprintf fmt |
|
209 |
"@[<v>node %s (%a) returns (%a);@ @]@ " |
|
210 |
nd.node_id |
|
211 |
pp_node_args nd.node_inputs |
|
212 |
pp_node_args nd.node_outputs |
|
213 |
| ImportedNode _ | ImportedFun _ | Consts _ | Open _ -> () |
|
206 | 214 |
|
207 | 215 |
let pp_econst fmt c = |
208 | 216 |
match c with |
... | ... | |
287 | 295 |
) fmt spec.behaviors; |
288 | 296 |
fprintf fmt "@]@ */@."; |
289 | 297 |
() |
298 |
|
|
299 |
|
|
300 |
let pp_lusi_header fmt filename prog = |
|
301 |
fprintf fmt "(* Generated Lustre Interface file from %s *)@." filename; |
|
302 |
fprintf fmt "(* generated by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ())); |
|
303 |
fprintf fmt "(* feel free to mask some of the nodes by removing them from this file. *)@.@."; |
|
304 |
List.iter (fprintf fmt "%a@." pp_lusi) prog |
|
305 |
|
|
290 | 306 |
(* Local Variables: *) |
291 | 307 |
(* compile-command:"make -C .." *) |
292 | 308 |
(* End: *) |
src/typing.ml | ||
---|---|---|
331 | 331 |
expr.expr_type <- ty; |
332 | 332 |
ty |
333 | 333 |
| Expr_appl (id, args, r) -> |
334 |
(* application of non internal function is not legal in a constant expression *) |
|
334 |
(* application of non internal function is not legal in a constant |
|
335 |
expression *) |
|
335 | 336 |
(match r with |
336 | 337 |
| None -> () |
337 |
| Some (x, l) -> check_constant expr.expr_loc const false; |
|
338 |
let expr_x = expr_of_ident x expr.expr_loc in |
|
339 |
let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in |
|
340 |
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |
|
338 |
| Some (x, l) -> |
|
339 |
check_constant expr.expr_loc const false; |
|
340 |
let expr_x = expr_of_ident x expr.expr_loc in |
|
341 |
let typ_l = |
|
342 |
Type_predef.type_clock |
|
343 |
(type_const expr.expr_loc (Const_tag l)) in |
|
344 |
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |
|
341 | 345 |
let touts = type_appl env in_main expr.expr_loc const id args in |
342 | 346 |
expr.expr_type <- touts; |
343 | 347 |
touts |
... | ... | |
583 | 587 |
type_imported_fun env nd decl.top_decl_loc |
584 | 588 |
| Consts clist -> |
585 | 589 |
type_top_consts env clist |
586 |
| Include _ -> env
|
|
590 |
| Open _ -> env
|
|
587 | 591 |
|
588 | 592 |
let type_prog env decls = |
589 | 593 |
try |
590 |
ignore(List.fold_left type_top_decl env decls)
|
|
594 |
List.fold_left type_top_decl env decls
|
|
591 | 595 |
with Failure _ as exc -> raise exc |
592 | 596 |
|
593 | 597 |
(* Once the Lustre program is fully typed, |
... | ... | |
632 | 636 |
| ImportedFun nd -> |
633 | 637 |
() |
634 | 638 |
| Consts clist -> () |
635 |
| Include _ -> ()
|
|
639 |
| Open _ -> ()
|
|
636 | 640 |
|
637 | 641 |
let uneval_prog_generics prog = |
638 | 642 |
List.iter uneval_top_generics prog |
643 |
|
|
644 |
let check_env_compat declared computed = |
|
645 |
Env.iter declared (fun k decl_type_k -> |
|
646 |
let computed_t = Env.lookup_value computed k in |
|
647 |
try_unify decl_type_k computed_t Location.dummy_loc |
|
648 |
) |
|
649 |
|
|
639 | 650 |
(* Local Variables: *) |
640 | 651 |
(* compile-command:"make -C .." *) |
641 | 652 |
(* End: *) |
src/utils.ml | ||
---|---|---|
308 | 308 |
in |
309 | 309 |
pp_list lid pp_fun "" "." "." |
310 | 310 |
|
311 |
let pp_date fmt tm = |
|
312 |
Format.fprintf fmt "%i/%i/%i, %i:%i:%i" |
|
313 |
(tm.Unix.tm_year + 1900) |
|
314 |
tm.Unix.tm_mon |
|
315 |
tm.Unix.tm_mday |
|
316 |
tm.Unix.tm_hour |
|
317 |
tm.Unix.tm_min |
|
318 |
tm.Unix.tm_sec |
|
311 | 319 |
|
312 | 320 |
(* Used for uid in variables *) |
313 | 321 |
|
test/test-compile.sh | ||
---|---|---|
1 | 1 |
#!/bin/bash |
2 | 2 |
|
3 | 3 |
NOW=`date "+%y%m%d%H%M"` |
4 |
|
|
4 |
LUSTREC="../../_build/src/lustrec" |
|
5 | 5 |
mkdir -p build |
6 | 6 |
cd build |
7 | 7 |
|
... | ... | |
11 | 11 |
# echo main:$main |
12 | 12 |
# echo opts:$opts |
13 | 13 |
if [ "$main" != "" ]; then |
14 |
lustrec -d build -verbose 0 $opts -node $main ../$file;
|
|
14 |
$LUSTREC -d build -verbose 0 $opts -node $main ../$file;
|
|
15 | 15 |
else |
16 |
lustrec -d build -verbose 0 $opts ../$file
|
|
16 |
$LUSTREC -d build -verbose 0 $opts ../$file
|
|
17 | 17 |
fi |
18 | 18 |
if [ $? -ne 0 ]; then |
19 | 19 |
rlustrec="INVALID"; |
Also available in: Unified diff