diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 11ca2e0f729fa2d6e5f3bd5b0c1d87a5d1a5cb5c..9bd3dc48b9c5356b962fdb4762af3ee33c5771ad 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -66,10 +66,6 @@ let construct_acsl_name (id : W.Ident.ident) =
String.concat "::" (paths @ name :: List.rev_append q [of_infix t])
| [] -> ""
-let recover_module (id : W.Ident.ident) =
- let (paths,name,_) = T.restore_path id in
- String.concat "." paths ^ "." ^ name
-
(* For debug only*)
let pp_id fmt (id: W.Ident.ident) =
Format.pp_print_string fmt id.id_string
@@ -125,6 +121,11 @@ type env = {
menv : why3module Datatype.String.Hashtbl.t
}
+type temp_menv = {
+ mutable lti : C.logic_type_info list;
+ mutable li : C.logic_info list;
+}
+
let create_empty_env wenv =
let tenv = W.Ty.Hts.create 0 in
let lenv = W.Term.Hls.create 0 in
@@ -170,21 +171,21 @@ let tvars_of_txs (txs: W.Ty.tvsymbol list) : string list * tvars =
x :: txs, W.Ty.Mtv.add tv (C.Lvar x) tvs
) txs ([], W.Ty.Mtv.empty)
-let rec lt_of_ty (env : env) (tvs : tvars) (ty: W.Ty.ty) : C.logic_type =
+let rec lt_of_ty (env : env) (temp_menv) (tvs : tvars) (ty: W.Ty.ty) : C.logic_type =
match ty.ty_node with
| Tyvar x -> W.Ty.Mtv.find x tvs
| Tyapp(s,[]) when W.Ty.(ts_equal s ts_int) -> C.Linteger
| Tyapp(s,[]) when W.Ty.(ts_equal s ts_real) -> C.Lreal
- | Tyapp(s,ts) -> C.Ltype( lti_of_ts env s ,
- List.map (lt_of_ty env tvs ) ts)
+ | Tyapp(s,ts) -> C.Ltype( lti_of_ts env temp_menv s ,
+ List.map (lt_of_ty env temp_menv tvs ) ts)
-and lti_of_ts (env : env) (ts : W.Ty.tysymbol) : C.logic_type_info =
+and lti_of_ts (env : env) (temp_menv : temp_menv) (ts : W.Ty.tysymbol) : C.logic_type_info =
try W.Ty.Hts.find env.tenv ts with Not_found ->
let (lt_params,tvars) = tvars_of_txs ts.ts_args in
let lt_def =
match ts.ts_def with
| NoDef | Range _ | Float _ -> None
- | Alias ty -> Some (C.LTsyn (lt_of_ty env tvars ty))
+ | Alias ty -> Some (C.LTsyn (lt_of_ty env temp_menv tvars ty))
in
let lti =
C.{
@@ -193,34 +194,29 @@ and lti_of_ts (env : env) (ts : W.Ty.tysymbol) : C.logic_type_info =
lt_attr = [];
}
in W.Ty.Hts.add env.tenv ts lti ;
-
- let cwmod = Datatype.String.Hashtbl.find env.menv @@ recover_module ts.ts_name in
- Datatype.String.Hashtbl.replace env.menv (recover_module ts.ts_name)
- {cwmod with types = cwmod.types @ [lti]};
- try begin let _ = (Logic_type_info.Hashtbl.find env.ltits lti)
- in lti end with Not_found ->
- Logic_type_info.Hashtbl.add env.ltits lti ts;
- lti
+ temp_menv.lti <- lti :: temp_menv.lti;
+ Logic_type_info.Hashtbl.add env.ltits lti ts;
+ lti
(* -------------------------------------------------------------------------- *)
(* --- Functions conversion --- *)
(* -------------------------------------------------------------------------- *)
-let lv_of_ty (env:env) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
+let lv_of_ty (env:env) (temp_menv : temp_menv) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
Cil_const.make_logic_var_formal (Printf.sprintf "x%d" index)
- @@ (lt_of_ty env tvars ty)
+ @@ (lt_of_ty env temp_menv tvars ty)
let lt_of_ty_opt (lt_opt) =
match lt_opt with
| None -> C.Ctype (C.TVoid []) (* Same as logic_typing *)
| Some tr -> tr
-let li_of_ls (env:env) (ls : W.Term.lsymbol) : C.logic_info =
+let li_of_ls (env:env) (temp_menv : temp_menv) (ls : W.Term.lsymbol) : C.logic_info =
let l_tparams,tvars =
tvars_of_txs @@ W.Ty.Stv.elements @@ W.Term.ls_ty_freevars ls in
- let l_type = Option.map (lt_of_ty env tvars ) ls.ls_value in
- let l_profile = List.mapi (lv_of_ty env tvars ) ls.ls_args in
+ let l_type = Option.map (lt_of_ty env temp_menv tvars ) ls.ls_value in
+ let l_profile = List.mapi (lv_of_ty env temp_menv tvars ) ls.ls_args in
let l_args = List.map ( fun (lv:C.logic_var) -> lv.lv_type) l_profile in
let signature = C.Larrow (l_args, lt_of_ty_opt l_type) in
let li =
@@ -234,14 +230,9 @@ let li_of_ls (env:env) (ls : W.Term.lsymbol) : C.logic_info =
l_profile ;
l_body = C.LBnone;
} in W.Term.Hls.add env.lenv ls li;
+ temp_menv.li <- li :: temp_menv.li;
Logic_info.Hashtbl.add env.lils li ls;
- let cwmod = Datatype.String.Hashtbl.find env.menv @@ recover_module ls.ls_name in
- Datatype.String.Hashtbl.replace env.menv (recover_module ls.ls_name)
- {cwmod with logics = cwmod.logics @ [li]};
- try begin let _ = (Logic_info.Hashtbl.find env.lils li)
- in li end with Not_found ->
- Logic_info.Hashtbl.add env.lils li ls;
- li
+ li
(* -------------------------------------------------------------------------- *)
@@ -251,8 +242,7 @@ let li_of_ls (env:env) (ls : W.Term.lsymbol) : C.logic_info =
let import_theory (env : env) thname =
let theory_name, theory_path = extract_path thname in
try
- Datatype.String.Hashtbl.add env.menv thname
- { logics = []; types = []; paths = theory_path};
+ let temp_menv : temp_menv = {li = []; lti = []} in
let theory = W.Env.read_theory env.wenv theory_path theory_name in
List.iter (fun (tdecl : T.tdecl) ->
match tdecl.td_node with
@@ -262,14 +252,14 @@ let import_theory (env : env) thname =
| Dtype ts ->
L.debug ~dkey "Decl and type %a" pp_id ts.ts_name;
L.debug ~dkey "Location %a" pp_id_loc ts.ts_name;
- let lti = lti_of_ts env ts in
+ let lti = lti_of_ts env temp_menv ts in
L.debug ~dkey "Correspondign LTI %a" pp_lti lti;
| Ddata ddatas ->
List.iter
(fun ((ts, _) : W.Decl.data_decl) ->
L.debug ~dkey "Decl and data %a" pp_id ts.ts_name;
L.debug ~dkey "Location %a" pp_id_loc ts.ts_name;
- let lti = lti_of_ts env ts in
+ let lti = lti_of_ts env temp_menv ts in
L.debug ~dkey "Correspondign data LTI %a" pp_lti lti;
) ddatas
| Dparam ls ->
@@ -280,13 +270,17 @@ let import_theory (env : env) thname =
(fun ((ls,_):W.Decl.logic_decl) ->
L.debug ~dkey "Decl and dlogic %a" pp_id ls.ls_name;
L.debug ~dkey "Location %a" pp_id_loc ls.ls_name;
- let li = li_of_ls env ls in
+ let li = li_of_ls env temp_menv ls in
L.debug ~dkey "Corresponding dlogic LTI %a" pp_li li;
) dlogics
| _ -> L.debug ~dkey "Other type of Decl"
end
| Use _| Clone _| Meta _ -> L.debug ~dkey ""
- ) theory.th_decls
+ ) theory.th_decls;
+ Datatype.String.Hashtbl.add env.menv thname
+ { logics = List.rev temp_menv.li;
+ types = List.rev temp_menv.lti;
+ paths = theory_path };
with W.Env.LibraryNotFound _ ->
L.error "Library %s not found" thname