(* Time-stamp: <modified the 10/05/2013 (at 15:00) by Erwan Jahier> *)
open Verbose
open AstV6
open AstCore
open Lxm
open Lv6errors
open Parsing
open Format
open Lv6MainArgs
let my_exit opt i =
close_out opt.oc;
if Sys.file_exists opt.outfile then Sys.remove opt.outfile;
exit i
let rec first_pack_in =
function
| (AstV6.NSPack pi)::_ -> pi.it.pa_name
| (AstV6.NSModel _)::tail -> first_pack_in tail
| [] -> raise (Global_error "No package has been provided")
(* try to use the filenale to guess the dft node *)
let find_a_node opt =
let first_file = List.hd opt.infiles in
let name =
try Filename.chop_extension (Filename.basename first_file)
with _ ->
print_string ("*** '"^first_file^"': bad file name.\n"); exit 1
in
name
(* Generates a lutin env and a lustre oracle for the node *)
let (gen_autotest_files : LicPrg.t -> Ident.idref option -> Lv6MainArgs.t -> unit) =
fun lic_prg main_node opt ->
let msk, zesoc, main_node =
match main_node with
| None -> (
let name = find_a_node opt in
let main_node = Ident.to_idref name in
let nk = (Lic.node_key_of_idref main_node) in
if LicPrg.node_exists lic_prg nk then (
output_string stdout ("WARNING: No main node is specified. I'll try with " ^ name ^"\n");
flush stdout;
let msk, zesoc = Lic2soc.f lic_prg nk in
msk, zesoc, main_node
) else (
print_string ("Error: no node is specified, cannot exec.\n");
flush stdout;
exit 1
)
)
| Some main_node ->
let msk, zesoc = Lic2soc.f lic_prg (Lic.node_key_of_idref main_node) in
msk, zesoc, main_node
in
let my_type_to_string range_flag t =
(* Remove the module name to have correct Lutin and lv4 type decl *)
let str = Data.type_to_string t in
let idref = Ident.idref_of_string str in
(if range_flag then (
match t with
| Data.Real -> " real [-10000.0;10000.0]"
| Data.Int -> " int [-10000;10000]"
| Data.Enum(_, idl) -> " int [0;"^(string_of_int (List.length idl - 1)) ^"]"
| _ -> idref.Ident.id_id
) else idref.Ident.id_id)
in
let soc = try Soc.SocMap.find msk zesoc with Not_found -> assert false in
let invars,outvars=soc.Soc.profile in
let invars = SocExec.expand_profile false invars in
let outvars = SocExec.expand_profile true outvars in
let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string true t)) invars in
let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) outvars in
let name = main_node.Ident.id_id in
let lutin_file_name = ("_"^name^"_env.lut") in
let oc = open_out lutin_file_name in
Lv6util.dump_entete oc;
output_string oc ("node " ^ (name) ^ "_env("^ (String.concat ";" outvars_str) ^
") returns(" ^ (String.concat ";" invars_str) ^ ") =\n loop true \n");
flush oc;
close_out oc;
output_string stdout (lutin_file_name ^" generated.\n");
let oracle_file_name = ("_"^name^"_oracle.lus") in
let oc = open_out oracle_file_name in
let invars,outvars=soc.Soc.profile in
let locals = List.map (fun (n,t) -> n^"_bis",t) outvars in
let invars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) invars in
let outvars_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) outvars in
let prg = "node "^name^"_oracle("^(String.concat ";" (invars_str@outvars_str)) in
let locals_str = List.map (fun (n,t) -> n^":"^(my_type_to_string false t)) locals in
let ok = (* avoid name clash*)
let all_vars = List.map fst (List.rev_append (List.rev_append locals invars) outvars) in
let rec gen_ok str = if List.mem str all_vars then gen_ok ("_"^str) else str in
gen_ok "ok"
in
let prg = prg ^") returns("^ok^":bool;"^(String.concat ";" locals_str)^");\nlet\n" in
let locals_name = List.map fst locals in
let invars_name = List.map fst invars in
let prg = prg^" ("^(String.concat "," locals_name)^") = "^name in
let prg = prg^"("^(String.concat "," invars_name)^");\n "^ok^" = (" in
let (var_to_equals : Soc.var -> Soc.var -> string list) =
fun (x,t) (y,_) ->
let rec aux x y t =
match t with
| Data.Real -> [x^"-"^y^" < 0.1 and "^ y^"-"^x^" < 0.1 "]
| Data.Array(t,n) ->
let res = ref [] in
for i = 0 to n-1 do
let istr = string_of_int i in
res := !res @ aux (x^"["^istr^"]") (y^"["^istr^"]") t
done;
!res
| Data.Struct(n,fl) ->
let do_field (fn,ft) = aux (x^"."^fn) (y^"."^fn) ft in
List.flatten (List.map do_field fl)
| _ -> [x^"="^y]
in
aux x y t
in
let prg = try prg^(String.concat " and\n \t\t "
(List.flatten (List.map2 var_to_equals locals outvars)))^");\ntel;\n"
with _ -> assert false
in
Lv6util.dump_entete oc;
output_string oc prg;
flush oc;
close_out oc;
output_string stdout (oracle_file_name ^" generated.\n");
flush stdout
let main () = (
(* Compile.init_appli () ; *)
(* parse_args (); *)
let opt = Lv6MainArgs.parse Sys.argv in
Verbose.exe ~level:3 (fun () ->
Gc.set { (Gc.get ()) with Gc.verbose = 0x01 }
);
if opt.run_unit_test then (
UnifyType.unit_test ();
exit 0
);
if (opt.infiles = []) then (
Lv6MainArgs.usage stderr opt;
exit 1
);
let new_dft_pack = Filename.basename (Filename.chop_extension (List.hd opt.infiles)) in
Ident.set_dft_pack_name new_dft_pack;
let main_node =
if opt.main_node = "" then None else
Some (Ident.idref_of_string opt.main_node)
in
if opt.outfile <> "" then opt.oc <- open_out opt.outfile;
(try (
let nsl = Compile.get_source_list opt opt.infiles in
let lic_prg = Compile.doit opt nsl main_node in
if opt.Lv6MainArgs.gen_autotest then
gen_autotest_files lic_prg main_node opt
else if opt.exec then
(match main_node with
| None -> (
let name = find_a_node opt in
let nk = (Lic.node_key_of_idref (Ident.to_idref name)) in
if LicPrg.node_exists lic_prg nk then (
print_string ("WARNING: No main node is specified. I'll try with " ^ name ^"\n");
flush stdout;
let msk, zesoc = Lic2soc.f lic_prg nk in
SocExec.f opt zesoc msk
) else (
print_string ("Error: no node is specified, cannot exec.\n");
flush stdout;
exit 1
)
)
| Some main_node ->
let msk, zesoc = Lic2soc.f lic_prg (Lic.node_key_of_idref main_node) in
SocExec.f opt zesoc msk
) else (
LicPrg.to_file opt lic_prg main_node
);
Verbose.exe ~level:3 (fun () -> Gc.print_stat stdout);
) with
Sys_error(s) ->
prerr_string (s^"\n");
my_exit opt 1
| Global_error s ->
print_global_error s ;
my_exit opt 1
| Parse_error ->
print_compile_error (Lxm.last_made ()) "syntax error";
my_exit opt 1
| Unknown_var(lxm,id) ->
print_compile_error lxm ("unknown variable (" ^ (Ident.to_string id) ^")");
my_exit opt 1
| Unknown_constant(lxm,str) ->
print_compile_error lxm ("unknown constant (" ^ str ^")");
my_exit opt 1
| Compile_error(lxm,msg) ->
print_compile_error lxm msg;
my_exit opt 1
| L2lCheckLoops.Error(lxm,msg,lic_prg) ->
(* Sometime it helps to see the current state of the faulty program *)
LicPrg.to_file opt lic_prg main_node;
flush opt.oc;
print_compile_error lxm msg;
my_exit opt 1
| Assert_failure (file, line, col) ->
prerr_string (
"\n*** oops: lus2lic internal error\n\tFile \""^ file ^
"\", line " ^ (string_of_int line) ^ ", column " ^
(string_of_int col) ^ "\n*** when compiling lustre program" ^
(if List.length opt.infiles > 1 then "s " else " ") ^
(String.concat ", " opt.infiles) ^ "\n"^
"\n*** You migth want to sent a bug report to "^Lv6version.maintainer ^"\n") ;
my_exit opt 2
);
(* | Compile_node_error(nkey,lxm,msg) -> ( *)
(* print_compile_node_error nkey lxm msg ; *)
(* exit 1 *)
(* ) *)
(* | Global_node_error(nkey,msg) -> ( *)
(* print_global_node_error nkey msg ; *)
(* exit 1 *)
(* ) *)
close_out opt.oc
);;
main();