From be21bf31d8fd46209a1dee31856122d790f5bf6a Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Tue, 28 Oct 2014 16:34:58 +0100 Subject: [PATCH] Insertion of call to controller(s) when exporting to Controllable-Nbac node. To enable recovery of parameter and output ordering by `ctrl2ept', the Controllable-Nbac generation procedure now declares a new module dedicated to the encapsulation of the controller functions yet to be synthesized. Handling of type declarations are probably buggy. --- compiler/global/modules.ml | 4 + compiler/global/names.ml | 2 +- compiler/heptagon/ctrln/ctrlNbacAsEpt.ml | 104 +++-- compiler/main/ctrl2ept.ml | 143 +++++- compiler/main/heptc.ml | 4 +- compiler/minils/ctrln/ctrlNbacGen.ml | 411 +++++++++++++----- compiler/minils/ctrln/ctrlNbacGen.mli | 3 +- compiler/minils/main/mls_compiler.ml | 29 +- compiler/myocamlbuild.ml | 3 +- compiler/utilities/_tags | 2 +- compiler/utilities/ctrln/ctrln_utils.ml | 67 +++ compiler/utilities/global/compiler_options.ml | 3 +- 12 files changed, 609 insertions(+), 166 deletions(-) create mode 100644 compiler/utilities/ctrln/ctrln_utils.ml diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index ac3f309..e728448 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -160,6 +160,10 @@ let initialize modul = List.iter open_module !default_used_modules +let current () = g_env.current_mod +let select modul = g_env.current_mod <- modul + + (** {3 Add functions prevent redefinitions} *) let _check_not_defined env f = diff --git a/compiler/global/names.ml b/compiler/global/names.ml index 8496922..da0256d 100644 --- a/compiler/global/names.ml +++ b/compiler/global/names.ml @@ -96,7 +96,7 @@ let rec modul_of_string_list = function let qualname_of_string s = let q_l_n = Misc.split_string s "." in match List.rev q_l_n with - | [] -> Misc.internal_error "Names" + | [] -> (* Misc.internal_error "Names" *)raise Exit | n::q_l -> { qual = modul_of_string_list q_l; name = n } let modul_of_string s = diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml index 24c8e68..3ea3dc7 100644 --- a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml +++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml @@ -28,6 +28,7 @@ (* *) (***********************************************************************) +open Signature open Types open Names open Idents @@ -119,6 +120,17 @@ 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 nuop t : nuop -> fun_name = function | `Opp when t = Initial.tfloat -> Initial.mk_pervasives "~-." | `Opp -> Initial.mk_pervasives "~-" @@ -161,13 +173,13 @@ let translate_expr gd e = | `Buop (op, e) -> mkb (mk_uapp (Efun (buop op)) (tb e)) | `Bnop (op, e, f, l) -> mkb_bapp ?flag (Efun (bnop op)) tb e f l | `Bcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tb e) (tb f)) - | `Ncmp _ -> assert false | `Ecmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (te e) (te f)) | `Pcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tp e) (tp f)) + | `Ncmp (re, e, f) -> mkb_ncmp re e f | `Pin (e, f, l) -> mkb_bapp_eq ?flag tp e f l | `Bin (e, f, l) -> mkb_bapp_eq ?flag tb e f l | `Ein (e, f, l) -> mkb_bapp_eq ?flag te e f l - | `BIin _ -> assert false + | `BIin _ -> raise (Untranslatable ("bounded Integer membership", flag)) | #cond as c -> trcond ?flag tb tb c | #flag as e -> apply' tb e and te ?flag = ignore flag; function @@ -183,11 +195,15 @@ 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 _ -> assert false + | `Bint (s, w, _) -> raise (Untranslatable (Format.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 | #flag as e -> apply' tn e + and mkb_ncmp ?flag re e f = + let { e_ty } as e = tn ?flag e and f = tn f in + mkb (mk_bapp (Efun (totrel e_ty re)) e f) and mk_nuapp ?flag op e = let { e_ty } as e = tn ?flag e in mkp e_ty (mk_uapp (Efun (nuop e_ty op)) e) @@ -223,18 +239,26 @@ let decl_typs typdefs gd = (* --- *) -let decl_var_acc gd v t acc = - let ident = ident_of_name (Symb.to_string v) in +let decl_var' gd v id t = let vd = { - v_ident = ident; - v_type = translate_typ gd v t; + v_ident = id; + v_type = t; v_linearity = Linearity.Ltop; v_clock = Clocks.Cbase; v_last = Var; v_loc = Location.no_location; } in - gd.env <- Env.add ident vd gd.env; - gd.var_names <- SMap.add v ident gd.var_names; + gd.env <- Env.add id vd gd.env; + gd.var_names <- SMap.add v id gd.var_names; + vd + +let decl_ident gd id t = + let v = mk_symb (name id) in + decl_var' gd v id t + +let decl_symb_acc gd v t acc = + let ident = ident_of_name (Symb.to_string v) in + let vd = decl_var' gd v ident (translate_typ gd v t) in vd :: acc (* --- *) @@ -250,7 +274,7 @@ let translate_equ_acc gd v e acc = (* --- *) let block_of_func gd { fni_local_vars; fni_all_specs } = - let locals = SMap.fold (decl_var_acc gd) fni_local_vars [] in + let locals = SMap.fold (decl_symb_acc gd) fni_local_vars [] in let equs = SMap.fold (translate_equ_acc gd) fni_all_specs [] in { b_local = locals; @@ -269,26 +293,41 @@ let io_of_func gd { fni_io_vars } = List.rev_append (SMap.bindings fnig_output_vars) o)) ([], []) fni_io_vars in let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in (* rev. *) - let i = List.fold_left (fun acc (v, t) -> decl_var_acc gd v t acc) [] i in + let i = List.fold_left (fun acc (v, t) -> decl_symb_acc gd v t acc) [] i in let o = List.sort (fun (a, _) (b, _) -> scmp b a) o in (* rev. *) - let o = List.fold_left (fun acc (v, t) -> decl_var_acc gd v t acc) [] o in + let o = List.fold_left (fun acc (v, t) -> decl_symb_acc gd v t acc) [] o in i, o (* --- *) -let node_of_func gd func = - let n_name = gd.qname "func" in - enter_node n_name; +(* /!\ Inputs omitted in the signature w.r.t the Controllable-Nbac model should + not appear anywhere in equations... *) +let io_of_func_match gd { node_inputs; node_outputs } = + let decl_arg = function + | { a_name = Some n; a_type = ty } -> decl_ident gd (ident_of_name n) ty + | _ -> failwith "Missing argument names in signature" + in + let i = List.map decl_arg node_inputs in + let o = List.map decl_arg node_outputs in + i, o + +(* --- *) + +let node_of_func gd ?node_sig n_name func = + enter_node n_name; (* ??? *) let fi = gather_func_info func in - let n_input, n_output = io_of_func gd fi in + let n_input, n_output = match node_sig with + | None -> io_of_func gd fi + | Some s -> io_of_func_match gd s + in let block = block_of_func gd fi in - { + Pnode { n_name; - n_stateful = false; (* ??? *) - n_unsafe = false; (* ??? *) + n_stateful = false; + n_unsafe = false; n_input; n_output; - n_contract = None; (* <- TODO *) + n_contract = None; (* <- TODO: assume? *) n_block = block; n_loc = Location.no_location; n_params = []; @@ -297,14 +336,25 @@ let node_of_func gd func = (* --- *) -let gen_func ~module_name func = +let gen_func ?node_sig ~node_name func = let { fn_typs; fn_decls } = func_desc func in - let gd = mk_gen_data module_name (fn_decls:> ('f, 'f var_spec) decls) fn_typs in - let typs = decl_typs fn_typs gd in - let typs = List.rev_map (fun t -> Ptype t) typs in - let node = node_of_func gd 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 node = node_of_func gd ?node_sig node_name func in + node, typs + +(* --- *) + +let create_prog modul = { - p_modname = Module module_name; + p_modname = modul; p_opened = []; - p_desc = List.rev (Pnode node :: typs); + p_desc = []; } + +let add_to_prog e ({ p_desc } as p) = + (* TODO: check typ duplicates *) + { p with p_desc = List.rev (e :: List.rev p_desc); } + +(* --- *) diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml index bcf59df..b425856 100644 --- a/compiler/main/ctrl2ept.ml +++ b/compiler/main/ctrl2ept.ml @@ -23,12 +23,12 @@ let abort ?filename n msgs = (** File extensions officially understood by the tool, with associated input types. *) let ityps_alist = [ - (* "ctrln", `Ctrln; "cn", `Ctrln; *) "ctrlf", `Ctrlf; "cf", `Ctrlf; - (* "ctrlr", `Ctrlr; "cr", `Ctrlr; *) + "ctrls", `Ctrlf; "cs", `Ctrlf; (* No need to discriminate between weaved and + split functions (for now). *) ] -(** Name of official input types as understood by the tool. *) +(** name of official input types as understood by the tool. *) let ityps = List.map fst ityps_alist let set_input_type r t = @@ -38,16 +38,31 @@ let set_input_type r t = let inputs = ref [] let output = ref "" let input_type = ref None +let node = ref "" +exception Help +let usage = "Usage: ctrl2ept [options] { [-i] | -n } \ + [ -- { } ]" +let print_vers () = + fprintf err_formatter "ctrl2ept, version %s (compiled on %s)@." version date; + exit 0 let anon x = inputs := x :: !inputs -let options = +let it = Arg.Symbol (ityps, set_input_type input_type) +let options = Arg.align [ - "-v",Arg.Set verbose, doc_verbose; - "-version", Arg.Unit show_version, doc_version; - "-i", Arg.String anon, " "; - "-input-type", Arg.Symbol (ityps, set_input_type input_type), "Input file type"; - "--input-type", Arg.Symbol (ityps, set_input_type input_type), ""; - "-o", Arg.Set_string output, " "; + "-i", Arg.String anon, " Input file (`-' means standard input)"; + "-input-type", it, " Input file type"; + "--input-type", it, ""; + "-o", Arg.Set_string output, " Select output file (`-' means \ + standard output)"; + "-n", Arg.Set_string node, " Select base input node"; + "--", 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; + "-v",Arg.Set verbose, " Set verbose mode"; + "-version", Arg.Unit print_vers, " Print the version of the compiler"; + "--version", Arg.Unit print_vers, ""; + "-h", Arg.Unit (fun _ -> raise Help), ""; ] (* -------------------------------------------------------------------------- *) @@ -63,7 +78,7 @@ type out = let mk_oc basename = { out_exec = (fun ext -> - let filename = asprintf "%s.%s" basename ext in + let filename = asprintf "%s%s" basename ext in let oc = open_out filename in info "Outputting into `%s'…" filename; oc, (fun () -> flush oc; close_out oc)); @@ -101,16 +116,100 @@ let parse_input ?filename (parse: ?filename:string -> _) = (* -------------------------------------------------------------------------- *) -let handle_ctrlf ?filename mk_oc = +exception Error of string + +(* let hack_filter_inputs = let open AST in function *) +(* | `Desc ({ fn_decls = decls } as f) -> *) +(* (\* TODO: we should actually _substitute_ these variables with ff in the *) +(* definitions; yet I think they are unlikely to appear anywhere in the *) +(* controller. *\) *) +(* let init_symb = Symb.of_string Ctrln_utils.init_cond_str *) +(* and sink_symb = Symb.of_string Ctrln_utils.sink_state_str in *) +(* let decls = SMap.remove init_symb decls in *) +(* let decls = SMap.remove sink_symb decls in *) +(* `Desc { f with fn_decls = decls } *) +(* | _ -> failwith "should be given an unchecked function!" *) + +let parse_n_gen_ept_node ?filename ?node_name ?node_sig () = let name, func = parse_input ?filename CtrlNbac.Parser.Unsafe.parse_func in - let name = match name with None -> "ctrlr" | Some n -> n ^"_ctrlr" in - let prog = CtrlNbacAsEpt.gen_func ~module_name:name func in + let node_name = match node_name with Some n -> n + | None -> match name with None -> assert false + | Some n -> Names.local_qn (n ^ "_ctrlr") + in + (* let name = match name with None -> "ctrlr" | Some n -> n ^"_ctrlr" in *) + (* let func = hack_filter_inputs func in *) + name, CtrlNbacAsEpt.gen_func ~node_name ?node_sig func + +let handle_ctrlf ?filename mk_oc = + let _, (node, typs) = parse_n_gen_ept_node ?filename () in + let prog = CtrlNbacAsEpt.create_prog Names.LocalModule in (* don't care? *) + let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in + let prog = CtrlNbacAsEpt.add_to_prog node prog in let oc, close = mk_oc.out_exec "ept" in Hept_printer.print oc prog; close () (* -------------------------------------------------------------------------- *) +let parse_nodename nn = try Names.qualname_of_string nn with + | Exit -> raise (Error (sprintf "Invalid node name: `%s'" nn)) + +let output_prog prog modul = + Modules.select modul; + let filename = String.uncapitalize (Names.modul_to_string modul) ^ ".ept" in + let oc = open_out filename in + info "Outputting into `%s'…" filename; + Hept_printer.print oc prog; + close_out oc + +let input_function prog filename node_name node_sig = + info "Reading function from `%s'…" filename; + let res = parse_n_gen_ept_node ~filename ~node_name ~node_sig () in + let node, typs = snd res in + let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in + let prog = CtrlNbacAsEpt.add_to_prog node prog in + prog + +let try_ctrlf nn prog = + let node_name = Ctrln_utils.controller_node nn in + if Modules.check_value node_name then + let filename = Ctrln_utils.ctrlf_for_node nn in + let node_sig = Modules.find_value node_name in + input_function prog filename node_name node_sig + else + raise (Error "Unable to load any controller function.") + +let try_ctrls nn prog = + let rec try_ctrls num prog = + let node_name = Ctrln_utils.controller_node ~num nn in + if Modules.check_value node_name then + let filename = Ctrln_utils.ctrls_for_node nn num in + let node_sig = Modules.find_value node_name in + let prog = input_function prog filename node_name node_sig in + try_ctrls (succ num) prog + else + prog + in + try_ctrls 0 prog + +let handle_node arg = + let nn = parse_nodename arg in + + let mo = Names.modul nn in + if mo = Names.Pervasives || mo = Names.LocalModule then + raise (Error (sprintf "Invalid node specification: `%s'." arg)); + + Initial.initialize 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 om in + let prog = try_ctrls nn prog in + let prog = if prog.Heptagon.p_desc = [] then try_ctrlf nn prog else prog in + output_prog prog om + +(* -------------------------------------------------------------------------- *) + let ityp_name_n_handle = function (* | `Ctrln -> "node", handle_ctrln *) | `Ctrlf -> "function", handle_ctrlf @@ -137,11 +236,8 @@ let guesstyp_n_output filename = | Not_found -> raise (Arg.Bad (sprintf "Cannot guess input type of `%s'" filename)) -let handle_input_file ?ityp filename = - let ityp, mk_oc = match ityp with - | None -> guesstyp_n_output filename - | Some ityp -> ityp, snd (guesstyp_n_output filename) - in +let handle_input_file filename = + let ityp, mk_oc = guesstyp_n_output filename in let itypname, handle = ityp_name_n_handle ityp in info "Reading %s from `%s'…" itypname filename; handle ~filename mk_oc @@ -157,10 +253,12 @@ let handle_input_stream = function (** [main] function to be launched *) let main () = - Arg.parse options anon errmsg; + Arg.parse options anon usage; match List.rev !inputs with + | [] when !node <> "" -> handle_node !node | [] -> handle_input_stream !input_type - | lst -> List.iter (handle_input_file ?ityp:!input_type) lst + | lst -> (if !node <> "" then handle_node !node; + List.iter handle_input_file lst) (* -------------------------------------------------------------------------- *) (** Launch the [main] *) @@ -168,5 +266,6 @@ let _ = try main () with + | Help -> Arg.usage options usage | Errors.Error -> error "aborted."; exit 2 - | Arg.Bad s | Sys_error s -> error "%s" s; exit 2 + | Error s | Arg.Bad s | Sys_error s -> error "%s" s; exit 2 diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index dd9a389..4763329 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -114,7 +114,9 @@ let compile source_f = (** [main] function to be launched *) let main () = - let read_qualname f = Arg.String (fun s -> f (Names.qualname_of_string s)) in + let read_qualname f = + Arg.String (fun s -> f (try Names.qualname_of_string s with + | Exit -> raise (Arg.Bad ("Invalid name: "^ s)))) in try Arg.parse [ diff --git a/compiler/minils/ctrln/ctrlNbacGen.ml b/compiler/minils/ctrln/ctrlNbacGen.ml index 6224aff..11f6a66 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.ml +++ b/compiler/minils/ctrln/ctrlNbacGen.ml @@ -34,6 +34,7 @@ (* -------------------------------------------------------------------------- *) +open Ctrln_utils open Signature open Types open Names @@ -48,34 +49,56 @@ exception Untranslatable of string (* XXX not catched yet! *) (* --- *) +let tt = mk_bcst' true +let ff = mk_bcst' false + +(* --- *) + (** Private record gathering temporary generation data *) type 'f gen_data = { typdefs: 'f typdefs; decls: 'f node_decls; - outputs: SSet.t; + base: (var_ident * ty) SMap.t; + local: (var_ident * ty) SMap.t; + contrs: (var_ident * ty) SMap.t; + output: IdentSet.t; init_cond: 'f bexp; init_state: 'f bexp; assertion: 'f bexp; invariant: 'f bexp; (* reachable: bexp; *) + remaining_contrs: SSet.t; (* All controllable inputs that has not yet + been assigned to a U/C group. *) + local_contr_deps: SSet.t SMap.t; (* All variables that depend on a + controllable. *) + extra_inputs: SSet.t; + uc_groups: (SSet.t * SSet.t) list; } (* --- *) -let tt = mk_bcst' true -let ff = mk_bcst' false -let init_cond_str = "__init__" (* XXX uniqueness? *) -and sink_state_str = "__sink__" - -let ref_of_typ = function - | `Bool -> mk_bref - | `Enum _ -> mk_eref - | `Int | `Real -> mk_nref +let mk_gen_data typdefs decls input local output init_cond = + { + typdefs; + decls; + base = input; + local; + contrs = SMap.empty; + output; + remaining_contrs = SSet.empty; + local_contr_deps = SMap.empty; + extra_inputs = SSet.empty; + uc_groups = []; + init_cond; + init_state = tt; + assertion = tt; + invariant = tt; + } (* --- *) -let translate_constr { name } = mk_label & mk_symb name (* XXX use module name (?) *) +let translate_constr { name } = mk_label & mk_symb name (* XXX use qual name? *) let translate_constrs cl = mk_etyp (List.map translate_constr cl) (* --- *) @@ -91,18 +114,23 @@ let translate_typ typ = match Modules.unalias_type typ with | Tarray _ -> raise & Untranslatable ("array type") | Tinvalid -> failwith "Encountered an invalid type!" +let ref_of_ty ty = match translate_typ ty with + | `Bool -> mk_bref + | `Enum _ -> mk_eref + | `Int | `Real -> mk_nref + (* --- *) 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 + | Sbool true | Sconstructor { qual = Pervasives; name = "true" } -> tt + | Sbool false | Sconstructor { qual = Pervasives; name = "false" } -> ff | _ -> failwith ("Boolean static expression expected!") 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 } -> + | 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!") @@ -110,8 +138,8 @@ let translate_static_eexp se = match simplify_static_exp se with 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) + | 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!") (* --- *) @@ -162,15 +190,14 @@ let translate_app ~pref op el = in match op, List.map (translate_ext ~pref) el with | Eequal, [e;f] -> mk_eq e f - | Efun { qual=Pervasives; name }, el -> pervasives (name, el) - (* *) + | Efun { qual = Pervasives; name }, el -> pervasives (name, el) | Eifthenelse, [c;t;e] -> mk_cond c t e | _ -> failwith "Unsupported application!" (** [translate_exp gd e] translates the {e memoryless} expression [e] into its Controllable Nbac representation. *) -let rec translate_exp ~pref t ({ e_desc = desc; e_ty = ty }) = (* XXX clock? *) - let typ = translate_typ ty in assert (t = typ); match desc with +let rec translate_exp ~pref ({ e_desc = desc }) = (* XXX clock? *) + match desc with | Eextvalue ext -> translate_ext ~pref ext | Eapp ({ a_op }, el, _) -> translate_app ~pref a_op el | Emerge (v, (_c, e) :: l) -> @@ -181,7 +208,7 @@ let rec translate_exp ~pref t ({ e_desc = desc; e_ty = ty }) = (* XXX clock? *) (translate_ext ~pref e) x) (translate_ext ~pref e) l - | Ewhen (exp, _, _) -> translate_exp ~pref t exp + | Ewhen (exp, _, _) -> translate_exp ~pref exp | Efby _ -> failwith "TODO: translate_exp (fby)" | Estruct _ -> failwith "TODO: translate_exp (struct)" | _ -> failwith "TODO: translate_exp" @@ -198,7 +225,18 @@ let rec translate_clk ~pref on off = function (* --- *) -let add_state_var gd v typ exp init = +let acc_dependencies_on vars deps_on_vars i e = fold_exp_dependencies + (fun v s -> + if SSet.mem v vars then SSet.add v s + else try SSet.union s (SMap.find v deps_on_vars) with + | Not_found -> s) + e i + +(* --- *) + +let add_state_var' ~pref gd id ty exp init = + let v = pref & mk_symb & name id in + let typ = translate_typ ty in let mk_init = match typ, init with | _, None -> (fun b -> b) | `Bool, Some i -> mk_and' (mk_beq' (mk_bref' v) (translate_static_bexp i)) @@ -207,119 +245,299 @@ let add_state_var gd v typ exp init = in { gd with decls = SMap.add v (typ, `State (exp, None), None) gd.decls; - init_state = mk_init gd.init_state; } + init_state = mk_init gd.init_state; }, v -let add_output_var gd v typ exp = add_state_var gd v typ exp None +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; } -let add_local_var gd v typ exp = - { gd with decls = SMap.add v (typ, `Local (exp, None), None) gd.decls; } +let add_output_var ~pref gd id ty exp = + add_state_var' ~pref gd id ty exp None |> fst + + +let add_local_var ~pref gd id ty exp = + let v = pref & mk_symb & name id in + let typ = translate_typ ty in + let ldeps = fold_exp_dependencies (fun v acc -> + if SSet.mem v gd.remaining_contrs then SSet.add v acc + else try SSet.union acc (SMap.find v gd.local_contr_deps) with + | Not_found -> acc) + exp + SSet.empty + in + let local_contr_deps = SMap.add v ldeps gd.local_contr_deps in + { gd with + decls = SMap.add v (typ, `Local (exp, None), None) gd.decls; + local_contr_deps; } + +let declare_additional_input ~pref gd id = + let l = mk_symb & name id in + try + let v = pref l in + let t = SMap.find l gd.local |> snd |> translate_typ in + { gd with + decls = SMap.add v (t, `Input one, None) gd.decls; + extra_inputs = SSet.add v gd.extra_inputs; } + with + | Not_found -> (* output of the main node. *) + assert (IdentSet.mem id gd.output); + gd (* --- *) -let translate_eq ~pref gd ({ eq_lhs = pat; - eq_rhs = { e_desc = exp; e_ty = typ } as rhs; - eq_base_ck = clk }) = - let typ = translate_typ typ in +let close_uc_group gd defined_contrs = + let rem = SSet.diff gd.remaining_contrs defined_contrs in + let lcd = SMap.map (SSet.inter rem) gd.local_contr_deps in + let lcd = SMap.filter (fun _ d -> not (SSet.is_empty d)) lcd in + { gd with + remaining_contrs = rem; + extra_inputs = SSet.empty; + local_contr_deps = lcd; + uc_groups = (gd.extra_inputs, defined_contrs) :: gd.uc_groups; } + +(* --- *) + +let pat_ids pat = + let rec acc_pat acc = function + | Evarpat id -> ((* pref & *)(* mk_symb & name *)id) :: acc + | Etuplepat pats -> List.fold_left acc_pat acc pats + in + acc_pat [] pat |> List.rev + +let translate_abstract_app ~pref gd pat _f args = + let results = pat_ids (* ~pref *) pat in + let args = List.map (translate_ext ~pref) args in + let gd = + (* in case of dependencies on remainging controllable variables, switch to + next U/C group. *) + let depc = List.fold_left + (acc_dependencies_on gd.remaining_contrs gd.local_contr_deps) + SSet.empty args + in + if SSet.is_empty depc then gd else close_uc_group gd depc + in + (* declare extra inputs. *) + (List.fold_left (declare_additional_input ~pref) gd results, []) + +(* --- *) + +let translate_eq ~pref (gd, equs) + ({ eq_lhs = pat; + eq_rhs = { e_desc = exp; e_ty = ty } as rhs; + eq_base_ck = clk } as eq) + = match pat with | Evarpat id -> - begin - let v = pref & mk_symb & name id in - match exp with - | Efby (init, ev) -> - let ev = translate_ext ~pref ev in - let ev = translate_clk ~pref ev (ref_of_typ typ v) clk in - add_state_var gd v typ ev init - | _ when SSet.mem v gd.outputs -> - add_output_var gd v typ (translate_exp ~pref typ rhs) - | _ -> - add_local_var gd v typ (translate_exp ~pref typ rhs) + begin match exp with + | Efby (init, ev) -> + let v = pref & mk_symb & name id in + 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) + when f.qual <> Pervasives -> + let gd, equs' = translate_abstract_app ~pref gd pat f args in + (gd, eq :: equs' @ equs) + | _ when IdentSet.mem id gd.output -> + (add_output_var ~pref gd id ty (translate_exp ~pref rhs), + eq :: equs) + | _ -> + (add_local_var ~pref gd id ty (translate_exp ~pref rhs), + eq :: equs) + end + | Etuplepat _ -> + begin match exp with + | Eapp ({ a_op = (Enode f | Efun f) }, args, None) + when f.qual <> Pervasives -> + let gd, equs' = translate_abstract_app ~pref gd pat f args in + (gd, eq :: equs' @ equs) + | _ -> failwith "TODO: Minils.Etuplepat construct!" end - | Etuplepat _ -> failwith "TODO: Minils.Etuplepat!" -let translate_eqs ~pref = List.fold_left (translate_eq ~pref) +let translate_eqs ~pref acc equs = + let gd, equs = List.fold_left (translate_eq ~pref) acc equs in + gd, List.rev equs (* --- *) let prefix_vars ~pref vars : symb -> symb = - let vars = List.fold_left - (fun acc { v_ident = id } -> (* XXX "_" only? *) - let v = mk_symb & name id in - SMap.add v (mk_symb ("_" ^ Symb.to_string v)) acc) - (SMap.empty) vars - in + let vars = List.fold_left begin fun acc { v_ident = id } -> + let v = mk_symb & name id in + SMap.add v (mk_symb ("c_" ^ Symb.to_string v)) acc + end (SMap.empty) vars in fun p -> pref (try SMap.find p vars with Not_found -> p) +let declare_contr (decls, contrs, vds) + ({ v_ident = id; v_type = ty } as vd) rank = + let v = mk_symb & name id in + SMap.add v (translate_typ ty, `Contr (one, rank, None), None) decls, + SMap.add v (id, ty) contrs, + vd :: vds + (** Contract translation *) let translate_contract ~pref gd ({ c_local; c_eq = equs; c_assume = a; c_enforce = g; c_assume_loc = a'; c_enforce_loc = g'; - c_controllables = cl }) = - let declare_contr decls { v_ident = id; v_type = typ } rank = - let v = mk_symb & name id in - SMap.add v (translate_typ typ, `Contr (AST.one, rank, None), None) decls in - let declare_contrs decls cl = + c_controllables = cl } as contract) = + let declare_contrs acc cl = fst & List.fold_left - (fun (decls, rank) c -> (declare_contr decls c rank, AST.succ rank)) - (decls, one) cl + (fun (acc, rank) c -> (declare_contr acc c rank, AST.succ rank)) + (acc, one) cl in let pref = prefix_vars ~pref c_local in - let gd = { gd with decls = declare_contrs gd.decls cl } in - let gd = translate_eqs ~pref gd equs in + let decls, contrs, locals = declare_contrs (gd.decls, SMap.empty, []) cl in + let c = SMap.fold (fun v _ -> SSet.add v) contrs SSet.empty in + let gd = { gd with decls; contrs; remaining_contrs = c; } in + let gd, equs' = translate_eqs ~pref (gd, []) equs in let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a') and ok = as_bexp & mk_and (translate_ext ~pref g) (translate_ext ~pref g') in let gd, ok = if !Compiler_options.nosink then (gd, ok) - else let sink = pref & mk_symb sink_state_str in - let ok = `Bexp (mk_bcond' gd.init_cond tt ok) in - (add_state_var gd sink `Bool ok None, mk_bref' sink) + else let sink = gen_var "" sink_state_str in + let sink_expr = mk_bref' & pref & mk_symb & name sink in + let ok = `Bexp ((* mk_bcond' gd.init_cond tt *) ok) in + (add_state_var ~pref gd sink Initial.tbool ok None, sink_expr) in - { gd with - assertion = mk_and' gd.assertion ak; - invariant = mk_and' gd.invariant ok; } + let assertion = mk_and' gd.assertion ak + and invariant = mk_and' gd.invariant ok in + ({ gd with assertion; invariant; }, { contract with c_eq = equs'; }, locals) + +(* --- *) + +let declare_output s { v_ident = id } = + IdentSet.add id s + +let declare_input m { v_ident = id; v_type = typ } = + SMap.add (mk_symb & name id) (translate_typ typ, `Input one, None) m + +let register_var_typ m { v_ident = id; v_type = typ } = + SMap.add (mk_symb & name id) (id, typ) m + +(* --- *) + +let finalize_uc_groups gd = + let gd = if SSet.is_empty gd.remaining_contrs then gd else + (* switch to last U/C group here, and declare controller call. *) + close_uc_group gd gd.remaining_contrs + in + if SSet.is_empty gd.extra_inputs then gd else + { gd with + extra_inputs = SSet.empty; + uc_groups = (gd.extra_inputs, SSet.empty) :: gd.uc_groups; } + +(* Note uc_groups are reversed in gd BEFORE the call to this function. *) +let assign_uc_groups gd = + let gd = finalize_uc_groups gd in + let uc_groups = List.rev gd.uc_groups in (* start from the first group *) + let decls, _ = List.fold_left begin fun (decls, group) (u, c) -> + let decls = SSet.fold (fun u decls -> match SMap.find u decls with + | (t, `Input _, l) -> + SMap.add u (t, `Input group, l) decls + | _ -> decls) u decls + in + let decls = SSet.fold (fun c decls -> match SMap.find c decls with + | (t, `Contr (_, r, l'), l) -> + SMap.add c (t, `Contr (group, r, l'), l) decls + | _ -> decls) c decls + in + decls, AST.succ group + end (gd.decls, AST.succ one) (List.tl uc_groups) in + { gd with decls; uc_groups } + +(* --- *) + +let scmp a b = String.compare (Symb.to_string a) (Symb.to_string b) + +let var_exp v ty = + mk_extvalue ~ty ~clock:Clocks.Cbase ~linearity:Linearity.Ltop (Wvar v) + +let decl_arg (v, t) = + mk_arg (Some (name v)) t Linearity.Ltop Signature.Cbase + +let gen_ctrlf_calls gd node_name equs = + + let equs, _, _ = List.fold_left begin fun (equs, ubase, num) (u, c) -> + + (* Controllable inputs of the current U/C group *) + let c = SSet.elements c in + let c = List.sort scmp c in (* XXX now optional (x) *) + let o = List.map (fun v -> SMap.find v gd.contrs) c in + let os = List.map decl_arg o in + let ov, ot = List.split o in + let ov = Etuplepat (List.map (fun v -> Evarpat v) ov) in + + (* Accumulate state variables and all non-controllable inputs from the + beginning, plus all controllables from previous U/C groups *) + let u = SSet.fold (fun v -> SMap.add v (SMap.find v gd.local)) u ubase in + let i = SMap.bindings u in + let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in (* rev. i + ibid (x) *) + let is = List.rev_map (fun (_, p) -> decl_arg p) i in + let i = List.rev_map (fun (_, (v, t)) -> var_exp v t) i in + + (* Build controller call *) + let func_name = controller_node ~num node_name in + let app = Eapp (mk_app (Efun func_name), i, None) in + let exp = mk_exp ~linearity:Linearity.Ltop Clocks.Cbase (Tprod ot) app in + let equ = mk_equation false ov exp in + + (* Declare new node *) + let node_sig = Signature.mk_node Location.no_location ~extern:false is os + false false [] in + Modules.add_value func_name node_sig; + + (* Augment base non-controllble inputs with current controllables *) + let u = List.fold_left (fun u v -> SMap.add v (SMap.find v gd.contrs) u) u c in + + (equ :: equs, u, num + 1) + end (equs, gd.base, 0) gd.uc_groups in + + equs (* --- *) (** Node translation. Note the given node is not expored if it does not comprize a contract. *) -let translate_node typdefs : 'n -> 'n * (name * 'f AST.node) option = function +let translate_node typdefs : 'n -> 'n * (qualname * 'f AST.node) option = function | ({ n_contract = None } as node) -> node, None - | ({ n_name; n_input; n_output; n_equs; n_contract = Some contr } as node) -> - let declare_output s { v_ident = id } = SSet.add (mk_symb & name id) s in - let declare_input decls { v_ident = id; v_type = typ } = - SMap.add (mk_symb & name id) (translate_typ typ, `Input one, None) - decls in - + | ({ n_name; n_input; n_output; n_local; n_equs; + n_contract = Some contr } as node) -> let pref p = p in - let outputs = List.fold_left declare_output SSet.empty n_output in + let local = List.fold_left register_var_typ SMap.empty n_local in + let input = List.fold_left register_var_typ SMap.empty n_input in + let output = List.fold_left declare_output IdentSet.empty n_output in let decls = List.fold_left declare_input SMap.empty n_input in - let init_cond_var = mk_symb init_cond_str in - let init_cond = mk_bref' init_cond_var in - let decls = SMap.add init_cond_var - (`Bool, `State (`Bexp ff, None), None) decls in - (* let init_cond = tt in *) + let init_cond = mk_bref' init_cond_var in (* XXX what about gd.base? *) + let init_cond_spec = (`Bool, `State (`Bexp ff, None), None) in + let decls = SMap.add init_cond_var init_cond_spec decls in - let gd = { typdefs; decls; outputs; - init_cond; init_state = tt; - assertion = tt; invariant = tt; } in - let gd = translate_contract ~pref gd contr in - let gd = translate_eqs ~pref gd n_equs in + let gd = mk_gen_data typdefs decls input local output init_cond in + let gd, contract, locals' = translate_contract ~pref gd contr in + let gd, equs' = translate_eqs ~pref (gd, []) n_equs in + let gd = assign_uc_groups gd in + let equs' = gen_ctrlf_calls gd n_name equs' in - let ctrln_node_desc = { - cn_typs = typdefs; - cn_decls = gd.decls; - cn_init = mk_and' gd.init_state init_cond; - cn_assertion = (* mk_or' init_cond *)gd.assertion; - cn_invariant = Some (mk_or' init_cond gd.invariant); - cn_reachable = None; - cn_attractive = None; - } in - node, Some (n_name.name, (`Desc ctrln_node_desc : 'f AST.node)) + let ctrln_node_desc = + { cn_typs = typdefs; + cn_decls = gd.decls; + cn_init = mk_and' gd.init_state init_cond; + cn_assertion = (* mk_or' init_cond *)gd.assertion; + cn_invariant = Some (mk_or' init_cond gd.invariant); + cn_reachable = None; + cn_attractive = None; } + and node = + { node with + n_equs = equs'; + n_local = List.rev_append locals' n_local; + n_contract = Some contract; } + in + + (node, Some (n_name, (`Desc ctrln_node_desc : 'f AST.node))) (* --- *) @@ -330,9 +548,7 @@ let translate_node typdefs : 'n -> 'n * (name * 'f AST.node) option = function necessitating controller synthesis), (TODO: and a new Minils program, in which those nodes have been transformed so that they "call" their respective controller). *) -let gen ({ p_desc = desc } as p) = - (* Highly insprited by Sigalimain.program. *) - +let gen ({ p_desc } as p) = let _cnp_typs, nodes, descs = (* XXX Should we gather all the type definitions before translating any node? *) @@ -347,8 +563,7 @@ let gen ({ p_desc = desc } as p) = let typdefs = declare_typ tn typ typdefs in (typdefs, nodes, descs) | p -> (typdefs, nodes, p :: descs) - end (empty_typdefs, [], []) desc + end (empty_typdefs, [], []) p_desc in - (* let cnp_name = Names.modul_to_string p.p_modname *) let cnp_nodes = List.rev nodes and p_desc = List.rev descs in cnp_nodes, { p with p_desc } diff --git a/compiler/minils/ctrln/ctrlNbacGen.mli b/compiler/minils/ctrln/ctrlNbacGen.mli index daab23b..6355d65 100644 --- a/compiler/minils/ctrln/ctrlNbacGen.mli +++ b/compiler/minils/ctrln/ctrlNbacGen.mli @@ -31,4 +31,5 @@ (* Interface documentation is in `ctrlNbacGen.ml' only. *) (** *) -val gen: Minils.program -> (string * 'f CtrlNbac.AST.node) list * Minils.program +val gen: Minils.program -> + (Names.qualname * 'f CtrlNbac.AST.node) list * Minils.program diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 9f14ccb..f128167 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -7,6 +7,7 @@ (* Adrien Guatto, Parkas, ENS *) (* Cedric Pasteur, Parkas, ENS *) (* Marc Pouzet, Parkas, ENS *) +(* Nicolas Berthier, SUMO, INRIA *) (* *) (* Copyright 2012 ENS, INRIA, UJF *) (* *) @@ -41,10 +42,10 @@ let pp p = if !verbose then Mls_printer.print stdout p output into a file called "f_ctrln/n.nbac" *) let gen_n_output_ctrln p = let nodes, p = CtrlNbacGen.gen p in - let filename = filename_of_name (Names.modul_to_string p.Minils.p_modname) in - let dir = clean_dir (build_path (filename ^"_ctrln")) in + Ctrln_utils.save_controller_modul_for p.Minils.p_modname; + ignore (clean_dir (Ctrln_utils.dirname_for_modul p.Minils.p_modname)); List.iter begin fun (node_name, node) -> - let oc = open_out (dir ^"/"^ node_name ^".ctrln") in + let oc = open_out (Ctrln_utils.ctrln_for_node node_name) in let fmt = Format.formatter_of_out_channel oc in CtrlNbac.AST.print_node ~print_header:print_header_info fmt node; close_out oc @@ -53,12 +54,11 @@ let gen_n_output_ctrln p = let maybe_ctrln_pass p = let ctrln = List.mem "ctrln" !target_languages in - let _p = pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp in - () + pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp ;; ELSE -let maybe_ctrln_pass p = p +let maybe_ctrln_pass p = None ;; END @@ -101,20 +101,23 @@ let compile_program p = pass "Scheduling" true Schedule.program p pp in - let _p = maybe_ctrln_pass p in - (* NB: XXX _p is ignored for now... *) - let z3z = List.mem "z3z" !target_languages in + let ctrln = List.mem "ctrln" !target_languages in + let ctrl = z3z || ctrln in + if z3z && ctrln then + warn "ignoring target `ctrln' (incompatible with target `z3z')."; + + let p = maybe_ctrln_pass p in let p = pass "Sigali generation" z3z Sigalimain.program p pp in - (* Re-scheduling after sigali generation *) + + (* Re-scheduling after generation *) let p = if not !Compiler_options.use_old_scheduler then - pass "Scheduling (with minimization of interferences)" z3z Schedule_interf.program p pp + pass "Scheduling (with minimization of interferences)" ctrl Schedule_interf.program p pp else - pass "Scheduling" z3z Schedule.program p pp + pass "Scheduling" ctrl Schedule.program p pp in - (* Memory allocation *) let p = pass "Memory allocation" !do_mem_alloc Interference.program p pp in diff --git a/compiler/myocamlbuild.ml b/compiler/myocamlbuild.ml index 61636e6..1e3e2da 100644 --- a/compiler/myocamlbuild.ml +++ b/compiler/myocamlbuild.ml @@ -49,7 +49,8 @@ let df = function flag ["ocaml"; "parser" ; "menhir" ; "use_menhir"] (S[A"--explain"; A"--table"]); - flag ["ocaml"; "compile" ] (S[A"-w"; A"Ae"; A"-warn-error"; A"PU"; A"-w"; A"-9"]); + flag ["ocaml"; "compile" ] (S[A"-w"; A"Ae"; A"-warn-error"; A"PU"; + A"-w"; A"-9-48"]); | _ -> () diff --git a/compiler/utilities/_tags b/compiler/utilities/_tags index 6ba28ef..d3a0c34 100644 --- a/compiler/utilities/_tags +++ b/compiler/utilities/_tags @@ -1 +1 @@ - or :include + or or :include diff --git a/compiler/utilities/ctrln/ctrln_utils.ml b/compiler/utilities/ctrln/ctrln_utils.ml new file mode 100644 index 0000000..59dc4e9 --- /dev/null +++ b/compiler/utilities/ctrln/ctrln_utils.ml @@ -0,0 +1,67 @@ +(***********************************************************************) +(* *) +(* Heptagon *) +(* *) +(* Gwenael Delaval, LIG/INRIA, UJF *) +(* Leonard Gerard, Parkas, ENS *) +(* Adrien Guatto, Parkas, ENS *) +(* Cedric Pasteur, Parkas, ENS *) +(* Marc Pouzet, Parkas, ENS *) +(* Nicolas Berthier, SUMO, INRIA *) +(* *) +(* Copyright 2014 ENS, INRIA, UJF *) +(* *) +(* This file is part of the Heptagon compiler. *) +(* *) +(* Heptagon is free software: you can redistribute it and/or modify it *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 3 of the License, or *) +(* (at your option) any later version. *) +(* *) +(* Heptagon is distributed in the hope that it will be useful, *) +(* but WITHOUT ANY WARRANTY; without even the implied warranty of *) +(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *) +(* GNU General Public License for more details. *) +(* *) +(* You should have received a copy of the GNU General Public License *) +(* along with Heptagon. If not, see *) +(* *) +(***********************************************************************) +open Compiler_utils +open Names + +let dirname_for_modul modul = + build_path (filename_of_name (modul_to_string modul) ^ "_ctrln") + +let ctrln_for_node { qual; name } = + dirname_for_modul qual ^"/"^ name ^".ctrln" + +let ctrls_for_node { qual; name } = + Printf.sprintf "%s/%s.%d.ctrls" (dirname_for_modul qual) name + +let ctrlf_for_node { qual; name } = + Printf.sprintf "%s/%s.ctrlf" (dirname_for_modul qual) name + +let controller_modul = function + | Module n -> Module (n ^ "_ctrls") + | QualModule ({ name = n } as q) -> QualModule { q with name = n ^ "_ctrls" } + | _ -> failwith "Unexpected module" + +let controller_node ?num { qual; name } = match num with + | Some num -> { qual = controller_modul qual; + name = Printf.sprintf "%s_ctrlr%d" name num } + | None -> { qual = controller_modul qual; + name = Printf.sprintf "%s_ctrlr0" name } + +let save_controller_modul_for modul = + let om = Modules.current () in + let cm = controller_modul modul in + let epci = String.uncapitalize (Names.modul_to_string cm) ^ ".epci" in + Modules.select cm; + let oc = open_out_bin epci in + output_value oc (Modules.current_module ()); + close_out oc; + Modules.select om + +let init_cond_str = "__init__" (* XXX uniqueness? *) +and sink_state_str = "__sink__" diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index dbd5536..94f9373 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -56,7 +56,8 @@ and add_include d = (* where is the standard library *) let locate_stdlib () = print_string (try Sys.getenv "HEPTLIB" with Not_found -> standard_lib); - print_newline () + print_newline (); + exit 0 let show_version () = Format.printf "The Heptagon compiler, version %s (%s)@."