Requalify enumeration types only when exporintg to Controllable-Nbac.

This commit is contained in:
Nicolas Berthier 2014-10-31 14:14:15 +01:00
parent 39aa0e13c1
commit 0afdb16c57
5 changed files with 36 additions and 29 deletions

View file

@ -562,11 +562,25 @@ let requal_declared_types prog =
let cmodul = controller_modul prog.p_modname in
let requal m = m = prog.p_modname in
let requal_it ({ qual; name } as cstr) =
let requal_constr ({ qual; name } as cstr) =
if requal qual then { qual = cmodul; name } else cstr in
let requal_type = function
| Tid { qual; name } when requal qual -> Tid { qual = cmodul; name }
let requal_type_dec = function
| { t_name = tn; t_desc = Type_enum cl } as t when requal tn.qual ->
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));
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
@ -574,31 +588,21 @@ let requal_declared_types prog =
let open Global_mapfold in
let funcs = { Mls_mapfold.defaults with
type_dec = (fun _ () -> function
| { t_name = tn; t_desc = Type_enum cl } as t when requal tn.qual ->
let tn' = requal_it tn in
let t = { t with
t_name = tn';
t_desc = Type_alias (Tid { qual = cmodul; name = tn.name});
} in
Modules.replace_type tn (Signature.Talias (Tid tn));
Modules.add_type tn' (Signature.Tenum (List.map requal_it cl));
t, ()
| _ -> raise Errors.Fallback);
type_dec = (fun _ () td -> requal_type_dec td, ());
edesc = (fun funs () -> function
| Ewhen (e, c, x) ->
Ewhen (exp_it funs () e |> fst, requal_it c,
Ewhen (exp_it funs () e |> fst, requal_constr c,
var_ident_it funs.global_funs () x |> fst), ()
| Emerge (i, l) ->
Emerge (var_ident_it funs.global_funs () i |> fst,
List.map (fun (c, x) -> requal_it c,
List.map (fun (c, x) -> requal_constr c,
extvalue_it funs () x |> fst) l), ()
| _ -> raise Errors.Fallback);
extvalue_desc = (fun funs () -> function
| Wwhen (w, c, v) ->
Wwhen (extvalue_it funs () w |> fst, requal_it c,
Wwhen (extvalue_it funs () w |> fst, requal_constr c,
var_ident_it funs.global_funs () v |> fst), ()
| _ -> raise Errors.Fallback);
@ -608,12 +612,12 @@ let requal_declared_types prog =
ck = (fun funs () -> function
| Clocks.Con (ck, c, i) ->
Clocks.Con (ck_it funs () ck |> fst, requal_it c,
Clocks.Con (ck_it funs () ck |> fst, requal_constr c,
var_ident_it funs () i |> fst), ()
| _ -> raise Errors.Fallback);
static_exp_desc = (fun _ () -> function
| Sconstructor c -> Sconstructor (requal_it c), ()
| Sconstructor c -> Sconstructor (requal_constr c), ()
| _ -> raise Errors.Fallback);
};

View file

@ -188,9 +188,9 @@ and contract funs acc c =
let c_local, acc = var_decs_it funs acc c.c_local in
let c_eq, acc = eqs_it funs acc c.c_eq in
{ c with
c_assume = c_assume;
c_assume = c_assume;
c_enforce = c_enforce;
c_assume_loc = c_assume_loc;
c_assume_loc = c_assume_loc;
c_enforce_loc = c_enforce_loc;
c_local = c_local;
c_eq = c_eq }
@ -221,7 +221,9 @@ and const_dec funs acc c =
{ c with c_type = ty; c_value = se }, acc
and type_dec_it funs acc t = funs.type_dec funs acc t
and type_dec_it funs acc t =
try funs.type_dec funs acc t
with Fallback -> type_dec funs acc t
and type_dec funs acc t =
let tdesc, acc = tdesc_it funs acc t.t_desc in
{ t with t_desc = tdesc }, acc

View file

@ -61,18 +61,18 @@ let comment ?(sep=separateur) 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
Format.kfprintf (Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@."))
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.err_formatter "Warning: " f
Format.kfprintf (Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@."))
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
Format.kfprintf (Format.kfprintf (fun fmt -> Format.fprintf fmt "@]@."))
Format.err_formatter "Error: @[" f
let do_pass d f p pp =
comment (d ^ " ...\n");

View file

@ -63,6 +63,7 @@ AC_CHECK_OCAML_PKG([lablgtk2])
AC_MSG_WARN([Could not find 'lablgtk2'. The simulator will not be built])
fi
dnl version should be >= 0.9.6
AC_CHECK_OCAML_PKG([reatk.ctrlNbac])
if test "${OCAML_PKG_reatk_ctrlNbac}" = "no"; then
package_reatk_ctrlNbac="ocaml"; #dummy flag

2
heptc
View file

@ -42,7 +42,7 @@ fi
if [ ! -e "$LIB_DIR/pervasives.epci" ] || [ "$HEPTC" -nt "$LIB_DIR/pervasives.epci" ]
then
pushd "$LIB_DIR" > /dev/null
echo "Recompile pervasives.epci"
echo "Recompile pervasives.epci" > /dev/stderr
"$HEPTC" -nopervasives pervasives.epi
popd > /dev/null
fi