From bc17d71e3f878fde5bd96a575c05361e8f35465b Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Wed, 22 Oct 2014 17:42:57 +0200 Subject: [PATCH] New tool `ctrl2ept' for translating ReaX's output functions into Heptagon Compilation of the tool is dependent on the presence of the `reatk.ctrlNbac' library. --- compiler/Makefile | 37 +-- compiler/_tags.in | 2 +- compiler/global/initial.ml | 3 + compiler/global/location.ml | 11 - compiler/heptagon/_tags | 3 +- compiler/heptagon/ctrln/ctrlNbacAsEpt.ml | 310 ++++++++++++++++++++ compiler/main/ctrl2ept.ml | 172 +++++++++++ compiler/utilities/global/compiler_utils.ml | 13 +- config.in | 2 + configure | 12 + configure.in | 5 + 11 files changed, 528 insertions(+), 42 deletions(-) create mode 100644 compiler/heptagon/ctrln/ctrlNbacAsEpt.ml create mode 100644 compiler/main/ctrl2ept.ml diff --git a/compiler/Makefile b/compiler/Makefile index d9c66c0..9ce2c29 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -1,13 +1,13 @@ include ../config -BIN:=heptc.$(TARGET) +BIN:=$(COMPILER) ifeq ($(ENABLE_SIMULATOR), yes) - BIN:=$(BIN) hepts.$(TARGET) + BIN:=$(BIN) $(SIMULATOR) endif -ifeq ($(ENABLE_CTRL2EPT), yes) - BIN:=$(BIN) ctrl2ept.$(TARGET) +ifeq ($(ENABLE_CTRL2EPT_TRANSLATOR), yes) + BIN:=$(BIN) $(CTRLNBAC2EPT_TRANSLATOR) endif .PHONY: all clean native byte clean debug install @@ -15,39 +15,20 @@ endif all: $(TARGET) native: -ifeq ($(ENABLE_SIMULATOR), yes) - $(OCAMLBUILD) $(COMPILER).native $(SIMULATOR).native -else - $(OCAMLBUILD) $(COMPILER).native -endif + $(OCAMLBUILD) $(addsuffix .native,$(BIN)) byte: -ifeq ($(ENABLE_SIMULATOR), yes) - $(OCAMLBUILD) $(COMPILER).byte $(SIMULATOR).byte -else - $(OCAMLBUILD) $(COMPILER).byte -endif + $(OCAMLBUILD) $(addsuffix .byte,$(BIN)) debug: -ifeq ($(ENABLE_SIMULATOR), yes) - $(OCAMLBUILD) $(COMPILER).d.byte $(SIMULATOR).d.byte -else - $(OCAMLBUILD) $(COMPILER).d.byte -endif + $(OCAMLBUILD) $(addsuffix .d.byte,$(BIN)) profile: -ifeq ($(ENABLE_SIMULATOR), yes) - $(OCAMLBUILD) $(COMPILER).p.native $(SIMULATOR).p.native -else - $(OCAMLBUILD) $(COMPILER).p.native -endif + $(OCAMLBUILD) $(addsuffix .p.native,$(BIN)) install: $(INSTALL) -d $(INSTALL_BINDIR) - $(INSTALL) $(COMPILER).$(TARGET) $(INSTALL_BINDIR)/$(COMPILER) -ifeq ($(ENABLE_SIMULATOR), yes) - $(INSTALL) $(SIMULATOR).$(TARGET) $(INSTALL_BINDIR)/$(SIMULATOR) -endif + $(foreach t,$(BIN),$(INSTALL) $(t).$(TARGET) $(INSTALL_BINDIR)/$(t);) clean: $(OCAMLBUILD) -clean diff --git a/compiler/_tags.in b/compiler/_tags.in index e6ef86f..3a2e96f 100644 --- a/compiler/_tags.in +++ b/compiler/_tags.in @@ -7,5 +7,5 @@ true: use_menhir <**/heptc.{byte,native}>: package(menhirLib), package(ocamlgraph)
: package(lablgtk2), thread -<**/*.ml*> or <**/heptc.{byte,native}>: @package_reatk_ctrlNbac@ +<**/*.ml*> or <**/{heptc,ctrl2ept}.{byte,native}>: @package_reatk_ctrlNbac@ "minils/main/mls_compiler.ml" or "main/mls2seq.ml": pp(camlp4o pa_macro.cmo @ctrln_pp@) diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml index c925279..55ae51b 100644 --- a/compiler/global/initial.ml +++ b/compiler/global/initial.ml @@ -59,6 +59,9 @@ let mk_static_int_op op args = let mk_static_int i = mk_static_exp tint (Sint i) +let mk_static_float f = + mk_static_exp tint (Sfloat f) + let mk_static_bool b = mk_static_exp tbool (Sbool b) diff --git a/compiler/global/location.ml b/compiler/global/location.ml index 84627cf..e5607a5 100644 --- a/compiler/global/location.ml +++ b/compiler/global/location.ml @@ -32,21 +32,10 @@ open Lexing open Format -(* two important global variables: [input_name] and [input_chan] *) type location = Loc of position (* Position of the first character *) * position (* Position of the next character following the last one *) - -let input_name = ref "" (* Input file name. *) - -let input_chan = ref stdin (* The channel opened on the input. *) - -let initialize iname ic = - input_name := iname; - input_chan := ic - - let no_location = Loc (dummy_pos, dummy_pos) let error_prompt = ">" diff --git a/compiler/heptagon/_tags b/compiler/heptagon/_tags index 42a9e3d..2d36969 100644 --- a/compiler/heptagon/_tags +++ b/compiler/heptagon/_tags @@ -1,4 +1,5 @@ :include :include :include -
:include \ No newline at end of file +
:include +:include diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml new file mode 100644 index 0000000..24c8e68 --- /dev/null +++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml @@ -0,0 +1,310 @@ +(***********************************************************************) +(* *) +(* 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 Types +open Names +open Idents +open Heptagon +open CtrlNbac +open AST + +exception Untranslatable of string * Loc.t option + +(* --- *) + +(** Private record gathering temporary generation data *) +type 'f gen_data = + { + decls: ('f, 'f var_spec) decls; + ltyps: (typ * 'f option) SMap.t; + qname: string -> qualname; + mutable tdefs: type_name SMap.t; + mutable env: var_dec Env.t; + mutable var_names: ident SMap.t; + } + +(* --- *) + +let mk_gen_data _module_name decls typdefs = + { + decls; + ltyps = label_typs typdefs; + qname = (fun name -> { qual = (* Module module_name *)LocalModule; name }); + tdefs = SMap.empty; + env = Env.empty; + var_names = SMap.empty; + } + +(* --- *) + +let opt_decl_loc gd v = match SMap.find v gd.decls with | _, _, loc -> loc + +let translate_typ gd vdecl = function + | `Bool -> Initial.tbool + | `Int -> Initial.tint + | `Real -> Initial.tfloat + | `Enum tn -> Tid (SMap.find tn gd.tdefs) + | t -> raise (Untranslatable (Format.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 + | Not_found -> fst (SMap.find s gd.ltyps) + +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 = SMap.find v gd.var_names + +let pat_of_var gd v = Evarpat (ts gd v) + +(* --- *) + +let mkp t e = + { + e_desc = e; + e_ty = t; + e_ct_annot = None; + e_level_ck = Clocks.Cbase; + e_linearity = Linearity.Ltop; + e_loc = Location.no_location; + } + +let mkb = mkp Initial.tbool + +let mk_app op = + { + a_op = op; + a_params = []; + a_unsafe = false; (* ??? *) + a_inlined = true; (* ??? *) + } + +let mk_uapp op e = Eapp (mk_app op, [e] , None) +let mk_bapp op e f = Eapp (mk_app op, [e; f] , None) +let mk_ite c t e = Eapp (mk_app Eifthenelse, [c; t; e] , None) + +let apptyp = function + | Eapp ({ a_op = Eifthenelse }, _ :: { e_ty } :: _, _) -> e_ty + | _ -> assert false + +let eqrel: eqrel -> fun_name = function + | `Eq -> Initial.mk_pervasives "=" + | `Ne -> Initial.mk_pervasives "<>" + +let nuop t : nuop -> fun_name = function + | `Opp when t = Initial.tfloat -> Initial.mk_pervasives "~-." + | `Opp -> Initial.mk_pervasives "~-" + +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 buop: buop -> fun_name = function + | `Neg -> Initial.pnot + +let bnop: bnop -> fun_name = function + | `Conj -> Initial.pand + | `Disj -> Initial.por + | `Excl -> failwith "TODO: translation of exclusion operator" + +let translate_expr gd e = + let mkb_bapp_eq ?flag tr e f l = + let e = tr ?flag e in + let mkcmp a b = mkb (mk_bapp (Efun (eqrel `Eq)) a b) in + let mkcmp' f = mkcmp e (tr ?flag f) in + let disj = mk_bapp (Efun Initial.por) in + List.fold_left (fun acc f -> mkb (disj acc (mkcmp' f))) (mkcmp' f) l + and mkb_bapp ?flag op tr e f l = + let op = mk_bapp op in + List.fold_left (fun acc e -> mkb (op acc (tr ?flag e))) (tr ?flag e) (f::l) + and trcond ?flag tb tr = ignore flag; function + | `Ite (c, t, e) -> let e = mk_ite (tb c) (tr t) (tr e) in mkp (apptyp e) e + in + + let rec tb ?flag = function + | `Ref v -> mkb (Evar (ts gd v)) + | `Bool b -> mkb (Econst (Initial.mk_static_bool b)) + | `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)) + | `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 + | #cond as c -> trcond ?flag tb tb c + | #flag as e -> apply' tb e + and te ?flag = ignore flag; function + | `Ref v -> mkp (symb_typ' gd v) (Evar (ts gd v)) + | `Enum l -> let s = label_symb l in + let t = symb_typ' gd s in + let c = gd.qname (Symb.to_string s) in + mkp t (Econst (mk_static_exp t (Sconstructor c))) + | #cond as c -> trcond ?flag tb te c + | #flag as e -> apply' te e + and tn ?flag = function + | `Ref v -> mkp (symb_typ' gd v) (Evar (ts gd v)) + | `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 + | `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 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) + and mk_nnapp ?flag op e f l = + let { e_ty } as e = tn ?flag e in + let op = mk_bapp (Efun (nnop e_ty op)) in + List.fold_left (fun acc e -> mkp e_ty (op acc (tn ?flag e))) e (f::l) + and tp ?flag : 'f AST.exp -> _ = function + | `Bexp e -> tb ?flag e + | `Eexp e -> te ?flag e + | `Nexp e -> tn ?flag e + | `Ref v -> (match symb_typ gd v with + | `Enum _ -> te ?flag (`Enum (mk_label v)) + | t -> mkp (translate_typ gd v t) (Evar (ts gd v))) + | #cond as c -> trcond ?flag tb tp c + | #flag as e -> apply' tp e + in + tp 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_var_acc gd v t acc = + let ident = ident_of_name (Symb.to_string v) in + let vd = { + v_ident = ident; + v_type = translate_typ gd v 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; + vd :: acc + +(* --- *) + +let translate_equ_acc gd v e acc = + { + eq_desc = Eeq (pat_of_var gd v, translate_expr gd e); + eq_stateful = false; (* ??? *) + eq_inits = Linearity.Lno_init; + eq_loc = Location.no_location; (* first-level flag of e: (flagof 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 equs = SMap.fold (translate_equ_acc gd) fni_all_specs [] in + { + b_local = locals; + b_equs = List.rev equs; (* for readability... *) + b_defnames = gd.env; + b_stateful = false; + b_loc = Location.no_location; + } + +(* --- *) + +let scmp a b = String.compare (Symb.to_string a) (Symb.to_string b) +let io_of_func gd { fni_io_vars } = + let i, o = List.fold_left (fun (i, o) { fnig_input_vars; fnig_output_vars } -> + (List.rev_append (SMap.bindings fnig_input_vars) i, + 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 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 + i, o + +(* --- *) + +let node_of_func gd func = + let n_name = gd.qname "func" in + enter_node n_name; + let fi = gather_func_info func in + let n_input, n_output = io_of_func gd fi in + let block = block_of_func gd fi in + { + n_name; + n_stateful = false; (* ??? *) + n_unsafe = false; (* ??? *) + n_input; + n_output; + n_contract = None; (* <- TODO *) + n_block = block; + n_loc = Location.no_location; + n_params = []; + n_param_constraints = []; + } + +(* --- *) + +let gen_func ~module_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 + { + p_modname = Module module_name; + p_opened = []; + p_desc = List.rev (Pnode node :: typs); + } diff --git a/compiler/main/ctrl2ept.ml b/compiler/main/ctrl2ept.ml new file mode 100644 index 0000000..bcf59df --- /dev/null +++ b/compiler/main/ctrl2ept.ml @@ -0,0 +1,172 @@ +open Format +open Filename +open CtrlNbac +open Compiler_utils +open Compiler_options + +(* -------------------------------------------------------------------------- *) + +let report_msgs ?filename = + let report_msg = Parser.Reporting.report_msg ?filename err_formatter in + List.iter begin function + | #CtrlNbac.Parser.msg as msg -> report_msg msg + | `TError info -> report_msg (`MError info) + end + +let abort ?filename n msgs = + report_msgs ?filename msgs; + error "Aborting due to errors in %s" n; + exit 1 + +(* -------------------------------------------------------------------------- *) + +(** 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; *) +] + +(** Name of official input types as understood by the tool. *) +let ityps = List.map fst ityps_alist + +let set_input_type r t = + try r := Some (List.assoc t ityps_alist) with + | Not_found -> raise (Arg.Bad (asprintf "Unknown input file type: `%s'" t)) + +let inputs = ref [] +let output = ref "" +let input_type = ref None + +let anon x = inputs := x :: !inputs +let options = + [ + "-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, " "; + ] + +(* -------------------------------------------------------------------------- *) + +type out = + { + out_mult: bool; (* Are multiple calls to `out_exec' allowed? *) + out_exec: string -> out_channel * (unit -> unit); (* oc * close *) + } + +(* --- *) + +let mk_oc basename = + { + out_exec = (fun ext -> + 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)); + out_mult = true; + } + +let mk_oc' filename = + { + out_exec = (fun _ -> + let oc = open_out filename in + info "Outputting into `%s'…" filename; + oc, (fun () -> flush oc; close_out oc)); + out_mult = false; + } + +let mk_std_oc = + { + out_exec = (fun _ -> + info "Outputting onto standard output…"; + stdout, (fun () -> flush stdout)); + out_mult = true; + } + +(* --- *) + +(** Parses the given input file. *) +let parse_input ?filename (parse: ?filename:string -> _) = + try + CtrlNbac.Symb.reset (); + let s, n, msgs = parse ?filename () in + report_msgs ?filename msgs; + s, n + with + | CtrlNbac.Parser.Error (n, msgs) -> abort ?filename n msgs + +(* -------------------------------------------------------------------------- *) + +let handle_ctrlf ?filename mk_oc = + 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 oc, close = mk_oc.out_exec "ept" in + Hept_printer.print oc prog; + close () + +(* -------------------------------------------------------------------------- *) + +let ityp_name_n_handle = function + (* | `Ctrln -> "node", handle_ctrln *) + | `Ctrlf -> "function", handle_ctrlf + (* | `Ctrlr -> "predicate", handle_ctrlr *) + +let guesstyp_n_output filename = + try + let typ = match !input_type with + | Some t -> t + | None -> snd (List.find (fun (suff, _) -> check_suffix filename suff) + ityps_alist) + in + let basename_extra = match typ with + | `Ctrlf -> "_ctrlr" + in + typ, + (match !output with + | "-" -> mk_std_oc + | "" -> (try chop_extension filename ^ basename_extra |> mk_oc with + | Invalid_argument _ when filename <> "" -> mk_oc filename + | Invalid_argument _ -> mk_std_oc) + | o -> mk_oc' o) + with + | 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 itypname, handle = ityp_name_n_handle ityp in + info "Reading %s from `%s'…" itypname filename; + handle ~filename mk_oc + +let handle_input_stream = function + | None -> + info "Reading function from standard input…"; + handle_ctrlf mk_std_oc + | Some ityp -> + let itypname, handle = ityp_name_n_handle ityp in + info "Reading %s from standard input…" itypname; + handle mk_std_oc + +(** [main] function to be launched *) +let main () = + Arg.parse options anon errmsg; + match List.rev !inputs with + | [] -> handle_input_stream !input_type + | lst -> List.iter (handle_input_file ?ityp:!input_type) lst + +(* -------------------------------------------------------------------------- *) +(** Launch the [main] *) +let _ = + try + main () + with + | Errors.Error -> error "aborted."; exit 2 + | Arg.Bad s | Sys_error s -> error "%s" s; exit 2 diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index 20a333a..277552d 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -59,9 +59,20 @@ let separateur = "\n*********************************************\ let comment ?(sep=separateur) s = if !verbose then Format.printf "%s%s@." sep s +let info: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f -> + if !verbose then + Format.kfprintf (fun f -> Format.kfprintf (fun f -> Format.pp_print_newline f ()) f) + Format.err_formatter "Info: " f + else + Format.ifprintf Format.err_formatter f + let warn: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f -> Format.kfprintf (fun f -> Format.kfprintf (fun f -> Format.pp_print_newline f ()) f) - Format.std_formatter "Warning: " f + Format.err_formatter "Warning: " f + +let error: ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a = fun f -> + Format.kfprintf (fun f -> Format.kfprintf (fun f -> Format.pp_print_newline f ()) f) + Format.err_formatter "Error: " f let do_pass d f p pp = comment (d ^ " ...\n"); diff --git a/config.in b/config.in index 09f6119..c6339e2 100644 --- a/config.in +++ b/config.in @@ -11,6 +11,7 @@ INSTALL= @INSTALL@ BUILD= _build COMPILER=heptc SIMULATOR=hepts +CTRLNBAC2EPT_TRANSLATOR=ctrl2ept INSTALL_BINDIR=$(bindir) INSTALL_LIBDIR=$(libdir)/heptagon @@ -20,3 +21,4 @@ OCAMLBUILD=STDLIB=$(STDLIB_DIR) @OCAMLBUILD@ -use-ocamlfind TARGET=byte ENABLE_SIMULATOR=@enable_simulator@ +ENABLE_CTRL2EPT_TRANSLATOR=@enable_ctrl2ept@ diff --git a/configure b/configure index 91cabff..8da7622 100755 --- a/configure +++ b/configure @@ -585,6 +585,7 @@ ac_subst_vars='ctrln_pp package_reatk_ctrlNbac LTLIBOBJS LIBOBJS +enable_ctrl2ept enable_simulator stdlib_dir INSTALL @@ -663,6 +664,7 @@ ac_user_opts=' enable_option_checking enable_simulator enable_local_stdlib +enable_ctrl2ept ' ac_precious_vars='build_alias host_alias @@ -1278,6 +1280,7 @@ Optional Features: --enable-FEATURE[=ARG] include FEATURE [ARG=yes] --enable-simulator enable the graphical simulator --enable-local-stdlib use the in-sources standard library + --enable-ctrl2ept enable the Controllable-Nbac entity translator Report bugs to the package provider. _ACEOF @@ -1879,6 +1882,14 @@ else fi +# Check whether --enable-ctrl2ept was given. +if test "${enable_ctrl2ept+set}" = set; then : + enableval=$enable_ctrl2ept; +else + enable_ctrl2ept=yes +fi + + # checking for ocamlc if test -n "$ac_tool_prefix"; then # Extract the first word of "${ac_tool_prefix}ocamlc", so it can be a program name with args. @@ -4020,6 +4031,7 @@ fi + ac_config_files="$ac_config_files config" cat >confcache <<\_ACEOF diff --git a/configure.in b/configure.in index 130803d..1a78401 100644 --- a/configure.in +++ b/configure.in @@ -12,6 +12,10 @@ AC_ARG_ENABLE(local_stdlib, [ --enable-local-stdlib use the in-sources standard library],, enable_local_stdlib=no) +AC_ARG_ENABLE(ctrl2ept, + [ --enable-ctrl2ept enable the Controllable-Nbac entity translator],, + enable_ctrl2ept=yes) + AC_PROG_OCAML if test "$OCAMLC" = "no"; then AC_MSG_ERROR([Please install the OCaml compiler]) @@ -80,6 +84,7 @@ AC_SUBST(INSTALL) AC_SUBST(stdlib_dir) AC_SUBST(enable_simulator) +AC_SUBST(enable_ctrl2ept) AC_OUTPUT(config)