diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml index 110f91c..dcbf17c 100644 --- a/compiler/main/ctrl2ept.ml +++ b/compiler/main/ctrl2ept.ml @@ -39,6 +39,7 @@ let inputs = ref [] let output = ref "" let input_type = ref None let node = ref "" +let modul = ref "" exception Help let usage = "Usage: ctrl2ept [options] { [-i] | -n } \ @@ -56,6 +57,7 @@ let options = Arg.align "-o", Arg.Set_string output, " Select output file (`-' means \ standard output)"; "-n", Arg.Set_string node, " Select base input node"; + "-m", Arg.Set_string modul, " Select base input module"; "--", Arg.Rest anon, " Treat all remaining arguments as input files"; "-where", Arg.Unit locate_stdlib, doc_locate_stdlib; "-stdlib", Arg.String set_stdlib, doc_stdlib; @@ -122,8 +124,8 @@ let suppress_typedecl ?mo prog = let p_desc = List.fold_left (fun acc d -> match d with - Ptype _ -> acc - | _ -> d::acc) + Ptype _ -> acc + | _ -> d::acc) [] prog.p_desc in let p_opened = @@ -180,7 +182,7 @@ let try_ctrlf typ_symbs nn prog = let node_sig = Modules.find_value node_name in input_function prog typ_symbs filename node_name node_sig else - raise (Error "Unable to load any controller function.") + raise Exit let try_ctrls typ_symbs nn prog = let rec try_ctrls num prog = @@ -208,13 +210,40 @@ let handle_node arg = info "Loading module of controllers for node %s…" (Names.fullname nn); let om = Ctrln_utils.controller_modul mo in info "Translating type declarations of module %s…" (Names.modul_to_string om); - let typs, typ_symbs = CtrlNbacAsEpt.decl_typs_from_module_itf om in - let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in - let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in + let _typs, typ_symbs = CtrlNbacAsEpt.decl_typs_from_module_itf mo in + let prog = CtrlNbacAsEpt.create_prog ~open_modul:[mo] om in + (* let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in *) let prog = try try_ctrls typ_symbs nn prog with - | Exit -> try_ctrlf typ_symbs nn prog in - (* Suppress type declarations in controller *) - let prog = suppress_typedecl ~mo prog in + | Exit -> + try try_ctrlf typ_symbs nn prog with + Exit -> + raise (Error "Unable to load any controller function.") + in + output_prog prog om + +let handle_module modname = + let mo = Names.modul_of_string modname in + if mo = Names.Pervasives || mo = Names.LocalModule then + raise (Error (sprintf "Invalid module specification: `%s'." modname)); + Modules.open_module Names.Pervasives; + Modules.open_module mo; + Modules.select mo; + let curmod = Modules.current_module () in + info "Loading module of controllers for module %s…" (Names.modul_to_string mo); + let om = Ctrln_utils.controller_modul mo in + info "Translating type declarations of module %s…" (Names.modul_to_string om); + let _typs, typ_symbs = CtrlNbacAsEpt.decl_typs_from_module_itf mo in + let prog = CtrlNbacAsEpt.create_prog ~open_modul:[mo] om in + let prog = + Names.NamesEnv.fold + (fun nodename _node prog -> + info "Handling function %s…" nodename; + let nn = Names.{ qual = mo; name = nodename } in + try try_ctrls typ_symbs nn prog with + | Exit -> + try try_ctrlf typ_symbs nn prog with + Exit -> prog) + curmod.Modules.m_values prog in output_prog prog om (* -------------------------------------------------------------------------- *) @@ -263,14 +292,14 @@ let handle_input_stream = function (** [main] function to be launched *) let main () = Arg.parse options anon usage; - match List.rev !inputs with - | [] when !node <> "" -> handle_node !node - | [] -> handle_input_stream !input_type - | lst -> (if !node <> "" then handle_node !node; - List.iter handle_input_file lst) + match (!modul,!node,List.rev !inputs) with + | "","",[] -> handle_input_stream !input_type + | "",n,lst -> (handle_node n; List.iter handle_input_file lst) + | m,_,lst -> (handle_module m; List.iter handle_input_file lst) (* -------------------------------------------------------------------------- *) -(** Launch the [main] *) + +(* Launch the [main] *) let _ = (* CtrlNbac.Symb.reset (); <- not needed as we have only one input file. *) try diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index c911f8f..083a3ad 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -268,6 +268,8 @@ let add_state_var ~pref gd id ty exp init = let gd, v = add_state_var' ~pref gd id ty exp init in { gd with base = SMap.add v (id, ty) gd.base; } + +(* TODO : add_local_var instead ? (NB : state var used for simulation) *) let add_output_var ~pref gd id ty exp = add_state_var' ~pref gd id ty exp None |> fst @@ -358,7 +360,7 @@ let translate_eq ~pref (gd, equs) let ev = translate_ext ~pref ev in let ev = translate_clk ~pref ev (ref_of_ty ty v) clk in (add_state_var ~pref gd id ty ev init, eq :: equs) - | Eapp ({ a_op = (Enode f | Efun f) }, args, None) + | Eapp ({ a_op = (Enode f | Efun f) }, args, None) (* TODO : handle resets *) when f.qual <> Pervasives -> (translate_abstract_app ~pref gd pat f args, eq :: equs) | _ when IdentSet.mem id gd.output -> @@ -370,7 +372,7 @@ let translate_eq ~pref (gd, equs) end | Etuplepat _ -> begin match exp with - | Eapp ({ a_op = (Enode f | Efun f) }, args, None) + | Eapp ({ a_op = (Enode f | Efun f) }, args, None) (* TODO : handle resets *) when f.qual <> Pervasives -> (translate_abstract_app ~pref gd pat f args, eq :: equs) | _ -> failwith "TODO: Minils.Etuplepat construct!" @@ -427,8 +429,8 @@ let translate_contract ~pref gd in let gd = { gd with - assertion = mk_and' gd.assertion ak; - invariant = mk_and' gd.invariant ok; } in + assertion = mk_and' gd.assertion ak; + invariant = mk_and' gd.invariant ok; } in let opt_and opt_e e' = match opt_e with @@ -695,7 +697,7 @@ let requal_declared_types prog = dependencies between modules due to type declarations. Yet, a better idea might be to integrate the generated controllers into the original program later on. *) -let gen ?(requalify_declared_types = true) ({ p_desc } as p) = +let gen ?(requalify_declared_types = false) ({ p_desc } as p) = let requal_types = requalify_declared_types in @@ -714,9 +716,10 @@ let gen ?(requalify_declared_types = true) ({ p_desc } as p) = end (empty_typdefs, [], []) p_desc in - let cnp_nodes = List.rev nodes and p_desc = List.rev descs in + let cnp_nodes = List.rev nodes + and p_desc = List.rev descs in let prog = { p with p_desc } in - let prog = (* moving types to controller module? *) + let prog = if requalify_declared_types then requal_declared_types prog else prog diff --git a/compiler/obc/c/cgen.ml b/compiler/obc/c/cgen.ml index d4c01c7..67b2d71 100644 --- a/compiler/obc/c/cgen.ml +++ b/compiler/obc/c/cgen.ml @@ -852,6 +852,13 @@ let global_file_header name prog = let dependencies = ModulSet.elements (Obc_utils.Deps.deps_program prog) in let dependencies = List.map header_of_module dependencies in + let dependencies_types = + List.map + (function + "stdio" as s -> s + | s -> s ^ "_types") + dependencies in + let classes = program_classes prog in let (decls, defs) = List.split (List.map cdefs_and_cdecls_of_class_def classes) in @@ -863,7 +870,7 @@ let global_file_header name prog = let (cty_defs, cty_decls) = List.split cdefs_and_cdecls in let types_h = (filename_types ^ ".h", - Cheader ("stdbool"::"assert"::"pervasives"::dependencies, + Cheader ("stdbool"::"assert"::"pervasives"::dependencies_types, List.concat cty_decls)) in let types_c = (filename_types ^ ".c", Csource (concat cty_defs)) in