From 307f3d8418c2277f2865aee978e78b1d6525a4e5 Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Mon, 15 Dec 2014 15:47:21 +0100 Subject: [PATCH] Controllable-Nbac import&export now support relocation of alias types. - Controllable-Nbac export (CtrlNbacGen): correct handling of float expressions, as well as alias types; - Controllable-Nbac controller importer (CtrlNbacAsEpt): Declaration of enumerated types and aliases that are relocated to controller modules is now performed based on the interface. Dependencies between type aliases are also taken into account now; - ctrl2ept tool: correct loading of pervasives module. --- compiler/heptagon/ctrln/ctrlNbacAsEpt.ml | 134 ++++++++++++++++------- compiler/main/ctrl2ept.ml | 3 +- compiler/minils/ctrln/ctrlNbacGen.ml | 47 ++++---- 3 files changed, 123 insertions(+), 61 deletions(-) diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml index 508226b..1c41d61 100644 --- a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml +++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml @@ -28,6 +28,7 @@ (* *) (***********************************************************************) +open Format open Signature open Types open Names @@ -72,7 +73,7 @@ let translate_typ gd vdecl = function | `Int -> Initial.tint | `Real -> Initial.tfloat | `Enum tn -> Tid (SMap.find tn gd.tdefs) - | t -> raise (Untranslatable (Format.asprintf "type %a" print_typ t, + | t -> raise (Untranslatable (asprintf "type %a" print_typ t, opt_decl_loc gd vdecl)) let symb_typ gd s = try match SMap.find s gd.decls with | typ, _, _ -> typ with @@ -83,9 +84,8 @@ let symb_typ' gd s = translate_typ gd s (symb_typ gd s) let translate_label gd l = gd.qname (Symb.to_string (label_symb l)) let ts gd v = try SMap.find v gd.var_names with Not_found -> - failwith (Format.asprintf "Variable name `%a' unavailable; \ - was it an output of the main node?" - Symb.print v) + failwith (asprintf "Variable name `%a' unavailable; \ + was it an output of the main node?" Symb.print v) let pat_of_var gd v = Evarpat (ts gd v) @@ -123,30 +123,43 @@ let eqrel: eqrel -> fun_name = function | `Eq -> Initial.mk_pervasives "=" | `Ne -> Initial.mk_pervasives "<>" -let totrel t : totrel -> fun_name = function - | `Lt when t = Initial.tfloat -> Initial.mk_pervasives "<" - | `Le when t = Initial.tfloat -> Initial.mk_pervasives "<=" - | `Gt when t = Initial.tfloat -> Initial.mk_pervasives ">" - | `Ge when t = Initial.tfloat -> Initial.mk_pervasives ">=" - | `Lt -> Initial.mk_pervasives "<" - | `Le -> Initial.mk_pervasives "<=" - | `Gt -> Initial.mk_pervasives ">" - | `Ge -> Initial.mk_pervasives ">=" - | #eqrel as r -> eqrel r +let float_typ t = Modules.unalias_type t = Initial.tfloat -let nuop t : nuop -> fun_name = function - | `Opp when t = Initial.tfloat -> Initial.mk_pervasives "~-." - | `Opp -> Initial.mk_pervasives "~-" +let totrel t : totrel -> fun_name = + if float_typ t + then function + | `Lt -> Initial.mk_pervasives "<." + | `Le -> Initial.mk_pervasives "<=." + | `Gt -> Initial.mk_pervasives ">." + | `Ge -> Initial.mk_pervasives ">=." + | `Eq -> Initial.mk_pervasives "=." (* XXX: error case? *) + | `Ne -> Initial.mk_pervasives "<>." (* ibid *) + else function + | `Lt -> Initial.mk_pervasives "<" + | `Le -> Initial.mk_pervasives "<=" + | `Gt -> Initial.mk_pervasives ">" + | `Ge -> Initial.mk_pervasives ">=" + | #eqrel as r -> eqrel r -let nnop t : nnop -> fun_name = function - | `Sum when t = Initial.tfloat -> Initial.mk_pervasives "+." - | `Sub when t = Initial.tfloat -> Initial.mk_pervasives "-." - | `Mul when t = Initial.tfloat -> Initial.mk_pervasives "*." - | `Div when t = Initial.tfloat -> Initial.mk_pervasives "/." - | `Sum -> Initial.mk_pervasives "+" - | `Sub -> Initial.mk_pervasives "-" - | `Mul -> Initial.mk_pervasives "*" - | `Div -> Initial.mk_pervasives "/" +let nuop t : nuop -> fun_name = + if float_typ t + then function + | `Opp -> Initial.mk_pervasives "~-." + else function + | `Opp -> Initial.mk_pervasives "~-" + +let nnop t : nnop -> fun_name = + if float_typ t + then function + | `Sum -> Initial.mk_pervasives "+." + | `Sub -> Initial.mk_pervasives "-." + | `Mul -> Initial.mk_pervasives "*." + | `Div -> Initial.mk_pervasives "/." + else function + | `Sum -> Initial.mk_pervasives "+" + | `Sub -> Initial.mk_pervasives "-" + | `Mul -> Initial.mk_pervasives "*" + | `Div -> Initial.mk_pervasives "/" let buop: buop -> fun_name = function | `Neg -> Initial.pnot @@ -198,8 +211,8 @@ let translate_expr gd e = | `Int i -> mkp Initial.tint (Econst (Initial.mk_static_int i)) | `Real r -> mkp Initial.tfloat (Econst (Initial.mk_static_float r)) | `Mpq r -> tn ?flag (`Real (Mpqf.to_float r)) - | `Bint (s, w, _) -> raise (Untranslatable (Format.asprintf "constant of \ - type %a" print_typ (`Bint (s, w)), flag)) + | `Bint (s, w, _) -> raise (Untranslatable (asprintf "constant of type \ + %a" print_typ (`Bint (s, w)), flag)) | `Nuop (op, e) -> mk_nuapp ?flag op e | `Nnop (op, e, f, l) -> mk_nnapp ?flag op e f l | #cond as c -> trcond ?flag tb tn c @@ -228,17 +241,56 @@ let translate_expr gd e = (* --- *) -let decl_typs typdefs gd = - fold_typdefs begin fun tname tdef typs -> - let name = gd.qname (Symb.to_string tname |> String.uncapitalize) in - match tdef with - | EnumDef labels -> - let constrs = List.map (fun (l, _) -> translate_label gd l) labels in - gd.tdefs <- SMap.add tname name gd.tdefs; - { t_name = name; - t_desc = Type_enum constrs; - t_loc = Location.no_location }:: typs - end typdefs [] +(* let decl_typs typdefs gd = *) +(* fold_typdefs begin fun tname tdef typs -> *) +(* let name = gd.qname (Symb.to_string tname |> String.uncapitalize) in *) +(* match tdef with *) +(* | EnumDef labels -> *) +(* let constrs = List.map (fun (l, _) -> translate_label gd l) labels in *) +(* gd.tdefs <- SMap.add tname name gd.tdefs; *) +(* Ptype { t_name = name; *) +(* t_desc = Type_enum constrs; *) +(* t_loc = Location.no_location } :: typs *) +(* end typdefs [] *) + +let decl_typs_from_module_itf gd = + (* Note we need to sort type declarations according to their respective + dependencies; hence the implicit topological traversal of the type + definitions. *) + let rec decl_types rem types = + if QualEnv.is_empty rem then + types + else + let t_name, tdef = QualEnv.choose rem in + let rem, types = decl_typ t_name tdef rem types in + decl_types rem types + and decl_typ t_name tdef rem types = + let rem = QualEnv.remove t_name rem in + if tdef = Tabstract || t_name.qual = Names.Pervasives then + rem, types + else + let t_desc, rem, types = match tdef with + | Tenum cl -> + (* Compiler_utils.info "declaring enum type %s" (shortname t_name); *) + let name = Symb.of_string (String.capitalize (shortname t_name)) in + gd.tdefs <- SMap.add name t_name gd.tdefs; + (Type_enum cl, rem, types) + | Talias (Tid tn) when tn.qual = t_name.qual -> (* declare deps 1st *) + (* Compiler_utils.info "declaring alias type %s" (shortname t_name); *) + let tdef = QualEnv.find tn rem in + let rem, types = decl_typ tn tdef (QualEnv.remove tn rem) types in + (Type_alias (Tid tn), rem, types) + | Talias t -> + (* Compiler_utils.info "declaring alias type %s" (shortname t_name); *) + (Type_alias t, rem, types) + | Tstruct _ -> + failwith (asprintf "Unexpected struct type `%s' in module interface" + (shortname t_name)) + | Tabstract -> assert false + in + rem, Ptype { t_name; t_desc; t_loc = Location.no_location; } :: types + in + decl_types Modules.g_env.Modules.types [] (* --- *) @@ -343,13 +395,15 @@ let gen_func ?node_sig ~node_name func = let { fn_typs; fn_decls } = func_desc func in let modul = modul node_name in let gd = mk_gen_data modul (fn_decls:> ('f, 'f var_spec) decls) fn_typs in - let typs = List.map (fun t -> Ptype t) (decl_typs fn_typs gd) in + (* let typs = decl_typs fn_typs gd in *) + let typs = decl_typs_from_module_itf gd in let node = node_of_func gd ?node_sig node_name func in node, typs (* --- *) let create_prog ?(open_modul = []) modul = + Modules.open_module modul; { p_modname = modul; p_opened = open_modul; diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml index cc4101d..3dd0c56 100644 --- a/compiler/main/ctrl2ept.ml +++ b/compiler/main/ctrl2ept.ml @@ -204,10 +204,9 @@ let handle_node arg = if mo = Names.Pervasives || mo = Names.LocalModule then raise (Error (sprintf "Invalid node specification: `%s'." arg)); - Initial.initialize Names.Pervasives; + Modules.open_module Names.Pervasives; info "Loading module of controllers for node %s…" (Names.fullname nn); let om = Ctrln_utils.controller_modul mo in - Modules.open_module om; let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in let prog = try try_ctrls nn prog with Exit -> try_ctrlf nn prog in output_prog prog om diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index 47003b1..4eb9825 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -34,6 +34,7 @@ (* -------------------------------------------------------------------------- *) +open Compiler_utils open Ctrln_utils open Signature open Types @@ -103,12 +104,13 @@ let translate_constrs cl = mk_etyp (List.map translate_constr cl) (* --- *) -let translate_typ typ = match Modules.unalias_type typ with +let rec translate_typ typ = match Modules.unalias_type typ with | Tid ({ qual = Pervasives; name = "bool" }) -> `Bool | Tid ({ qual = Pervasives; name = "int" }) -> `Int - | Tid ({ qual = Pervasives; name = "real" }) -> `Real (* XXX? *) + | Tid ({ qual = Pervasives; name = "float" }) -> `Real | Tid ({ name = tn } as t) -> (match Modules.find_type t with | Tenum _ -> `Enum (mk_typname (mk_symb tn)) + | Talias t -> translate_typ t (* XXX? *) | _ -> raise & Untranslatable ("type "^ fullname t)) | Tprod _ -> raise & Untranslatable ("product type") | Tarray _ -> raise & Untranslatable ("array type") @@ -126,21 +128,24 @@ let simplify_static_exp se = (Static.simplify QualEnv.empty se).se_desc let translate_static_bexp se = match simplify_static_exp se with | Sbool true | Sconstructor { qual = Pervasives; name = "true" } -> tt | Sbool false | Sconstructor { qual = Pervasives; name = "false" } -> ff - | _ -> failwith ("Boolean static expression expected!") + | _ -> failwith (Format.asprintf "Boolean static expression expected! (found@ \ + `%a')" Global_printer.print_static_exp se) let translate_static_eexp se = match simplify_static_exp se with | Sconstructor { qual = Pervasives; name = "true" as n } | Sconstructor { qual = Pervasives; name = "false" as n } -> failwith ("Enum static expression expected! (found `"^n^"')") | Sconstructor c -> `Enum (translate_constr c) - | _ -> failwith ("Enum static expression expected!") + | _ -> failwith (Format.asprintf "Enum static expression expected! (found@ \ + `%a')" Global_printer.print_static_exp se) let translate_static_nexp se = match simplify_static_exp se with | Sint v -> `Int v | Sfloat v -> `Real v | Sop ({ qual = Pervasives; name="~-" },[{ se_desc = Sint v }]) -> `Int (-v) | Sop ({ qual = Pervasives; name="~-." },[{ se_desc=Sfloat v }]) -> `Real (-.v) - | _ -> failwith ("Numerical static expression expected!") + | _ -> failwith (Format.asprintf "Numerical static expression expected! (found\ + @ `%a')" Global_printer.print_static_exp se) (* --- *) @@ -173,6 +178,7 @@ let translate_ext ~pref ext = match translate_typ ext.w_ty with let translate_app ~pref op el = let pervasives = function | "not", [e] -> mk_neg e + |("~-" | "~-."), [e] -> mk_opp e | "or", e::l -> mk_disj e l | "&", e::l -> mk_conj e l | "xor", [e;f] -> mk_xor e f @@ -564,9 +570,8 @@ let translate_node ~requal_types typdefs = function (* --- *) (** Moves all type declarations into the given module, declare aliases for them - (in cases). Also requalifies constructor names in the program, FIXME: as - well as types of expressions to avoid some errors in code generation later - on. *) + (in cases). Also requalifies constructor names in the program, as well as + types of expressions to avoid some errors in code generation later on. *) let requal_declared_types prog = let cmodul = controller_modul prog.p_modname in @@ -575,25 +580,29 @@ let requal_declared_types prog = let requal_constr ({ qual; name } as cstr) = if requal qual then { qual = cmodul; name } else cstr in + let requal_type = function (* requalify enum and alias types. *) + | Tid ({ qual; name } as ty) as t when requal qual -> + (match Modules.find_type ty with + | Tenum _ | Talias _ -> Tid { qual = cmodul; name } + | _ -> t) + | t -> t + in + let requal_type_dec = function - | { t_name = tn; t_desc = Type_enum cl } as t when requal tn.qual -> + | { t_name = tn; t_desc } as t when requal tn.qual -> + let new_type = match t_desc with + | Type_enum cl -> Signature.Tenum (List.map requal_constr cl) + | Type_alias t -> Signature.Talias (requal_type t) + | _ -> raise Errors.Fallback + in let tn' = { tn with qual = cmodul } in let t = { t with t_name = tn; t_desc = Type_alias (Tid tn') } in Modules.replace_type tn (Signature.Talias (Tid tn')); - Modules.add_type tn' (Signature.Tenum (List.map requal_constr cl)); + Modules.add_type tn' new_type; t | _ -> raise Errors.Fallback in - let requal_type = function (* requalify only enum types. *) - | Tid ({ qual; name } as ty) as t when requal qual -> - begin match Modules.find_type ty with - | Tenum _ -> Tid { qual = cmodul; name } - | _ -> t - end - | t -> t - in - let open Mls_mapfold in let open Global_mapfold in let funcs = { Mls_mapfold.defaults with