diff --git a/src/plugins/wp/Why3Import.ml b/src/plugins/wp/Why3Import.ml
index 8ab9ed78effcb0de5886d3b5518e555b41d97f6c..833fcef95e84f9125c98ff0b7a1d3dc0b07161fc 100644
--- a/src/plugins/wp/Why3Import.ml
+++ b/src/plugins/wp/Why3Import.ml
@@ -20,6 +20,8 @@
(* *)
(**************************************************************************)
+open Cil_datatype
+
module C = Cil_types
module Cpp = Cil_printer
module L = Wp_parameters
@@ -28,8 +30,6 @@ module F = Filepath.Normalized
module W = Why3
module WConf = Why3.Whyconf
-
-
let dkey = L.register_category "why3.import"
(* -------------------------------------------------------------------------- *)
@@ -40,8 +40,6 @@ let create_why3_env loadpath =
let main = WConf.get_main @@ WConf.read_config None in
W.Env.create_env @@ WConf.loadpath main @ F.to_string_list loadpath
-
-
let extract_path thname =
let segments = String.split_on_char '.' thname in
match List.rev segments with
@@ -59,7 +57,6 @@ let of_infix s =
else unwrap_any s others
in unwrap_any s ["prefix ";"infix ";"mixfix "]
-
let construct_acsl_name (id : W.Ident.ident) =
let (paths,name,scopes) = T.restore_path id in
match List.rev scopes with
@@ -68,7 +65,6 @@ let construct_acsl_name (id : W.Ident.ident) =
| [] -> ""
-
(* For debug only*)
let pp_id fmt (id: W.Ident.ident) =
Format.pp_print_string fmt id.id_string
@@ -106,52 +102,43 @@ let pp_lvs fmt (lvs : C.logic_var list) =
(* --- Types --- *)
(* -------------------------------------------------------------------------- *)
-type tenv = C.logic_type_info W.Ty.Hts.t
-type lenv = C.logic_info W.Term.Hls.t
-type tvars = C.logic_type W.Ty.Mtv.t
-type lils = W.Term.lsymbol Logic_info.Hashtbl.t
-type ltits = W.Ty.tysymbol Logic_type_info.Hashtbl.t
-type menv = C.global Datatype.String.Hashtbl.t
+type tvars = C.logic_type W.Ty.Mtv.t
-type genv = {
+type env = {
wenv : W.Env.env;
- tenv : tenv;
- lenv : lenv;
- lils : lils;
- ltits : ltits;
- menv : menv
+ tenv : C.logic_type_info W.Ty.Hts.t;
+ lenv : C.logic_info W.Term.Hls.t;
+ _lils : W.Term.lsymbol Logic_info.Hashtbl.t;
+ _ltits : W.Ty.tysymbol Logic_type_info.Hashtbl.t;
+ _menv : C.global Datatype.String.Hashtbl.t
}
+
(* -------------------------------------------------------------------------- *)
(* --- Built-in --- *)
(* -------------------------------------------------------------------------- *)
-let add_builtin (tenv : tenv) ts lt_name lt_params =
+let add_builtin (tenv) ts lt_name lt_params =
W.Ty.Hts.add tenv ts C.{lt_name ; lt_params; lt_def=None; lt_attr=[] }
-let find_ts genv pkg thy name =
- let th = Why3.Env.read_theory genv.wenv pkg thy in
+let find_ts env pkg thy name =
+ let th = Why3.Env.read_theory env.wenv pkg thy in
try
Why3.Theory.ns_find_ts th.th_export name
with Not_found ->
L.fatal "Cannot find %s.%s.%s"
(String.concat "." pkg ) thy (String.concat "." name)
-let add_builtins genv =
+let add_builtins env =
begin
- let ts_list = find_ts genv ["list"] "List" ["list"] in
- let ts_set = find_ts genv ["set"] "Set" ["set"] in
- add_builtin genv.tenv W.Ty.ts_bool Utf8_logic.boolean [];
- add_builtin genv.tenv ts_list "\\list" ["A"];
- add_builtin genv.tenv ts_set "set" ["A"];
+ let ts_list = find_ts env ["list"] "List" ["list"] in
+ let ts_set = find_ts env ["set"] "Set" ["set"] in
+ add_builtin env.tenv W.Ty.ts_bool Utf8_logic.boolean [];
+ add_builtin env.tenv ts_list "\\list" ["A"];
+ add_builtin env.tenv ts_set "set" ["A"];
end
-(* -------------------------------------------------------------------------- *)
-(* --- Reverse tables --- *)
-(* -------------------------------------------------------------------------- *)
-
-
(* -------------------------------------------------------------------------- *)
(* --- Type conversion --- *)
@@ -167,23 +154,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 (tenv : tenv) (tvs : tvars) (ty: W.Ty.ty) : C.logic_type =
+let rec lt_of_ty (env : env) (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 tenv s ,
- List.map (lt_of_ty tenv tvs ) ts)
+ | Tyapp(s,ts) -> C.Ltype( lti_of_ts env s ,
+ List.map (lt_of_ty env tvs ) ts)
-
-and lti_of_ts (tenv : tenv) (ts : W.Ty.tysymbol) : C.logic_type_info =
- try W.Ty.Hts.find tenv ts with Not_found ->
+and lti_of_ts (env : env) (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 tenv tvars ty))
+ | Alias ty -> Some (C.LTsyn (lt_of_ty env tvars ty))
in
let lti =
C.{
@@ -191,27 +176,29 @@ and lti_of_ts (tenv : tenv) (ts : W.Ty.tysymbol) : C.logic_type_info =
lt_params ; lt_def ;
lt_attr = [];
}
- in W.Ty.Hts.add tenv ts lti ;
+ in W.Ty.Hts.add env.tenv ts lti ;
+ Logic_type_info.Hashtbl.add env._ltits lti ts;
lti
+
(* -------------------------------------------------------------------------- *)
(* --- Functions conversion --- *)
(* -------------------------------------------------------------------------- *)
-let lv_of_ty (tenv:tenv) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
+let lv_of_ty (env:env) (tvars:tvars) (index) (ty:W.Ty.ty) : C.logic_var =
Cil_const.make_logic_var_formal (Printf.sprintf "x%d" index)
- @@ (lt_of_ty tenv tvars ty)
+ @@ (lt_of_ty env 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 (tenv:tenv) (ls : W.Term.lsymbol) (lenv:lenv) : C.logic_info =
+let li_of_ls (env:env) (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 tenv tvars ) ls.ls_value in
- let l_profile = List.mapi (lv_of_ty tenv tvars ) ls.ls_args 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_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 =
@@ -224,18 +211,19 @@ let li_of_ls (tenv:tenv) (ls : W.Term.lsymbol) (lenv:lenv) : C.logic_info =
l_type;
l_profile ;
l_body = C.LBnone;
- } in W.Term.Hls.add lenv ls li; li
+ } in W.Term.Hls.add env.lenv ls li;
+ Logic_info.Hashtbl.add env._lils li ls;
+ li
(* -------------------------------------------------------------------------- *)
(* --- Theory --- *)
(* -------------------------------------------------------------------------- *)
-
-let import_theory env (tenv:tenv) (lenv:lenv) thname =
+let import_theory (env : env) thname =
let theory_name, theory_path = extract_path thname in
try
- let theory = W.Env.read_theory env theory_path theory_name 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
| Decl decl ->
@@ -244,14 +232,14 @@ let import_theory env (tenv:tenv) (lenv:lenv) 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 tenv ts in
+ let lti = lti_of_ts env 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 tenv ts in
+ let lti = lti_of_ts env ts in
L.debug ~dkey "Correspondign data LTI %a" pp_lti lti;
) ddatas
| Dparam ls ->
@@ -262,7 +250,7 @@ let import_theory env (tenv:tenv) (lenv:lenv) 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 tenv ls lenv in
+ let li = li_of_ls env ls in
L.debug ~dkey "Corresponding dlogic LTI %a" pp_li li;
) dlogics
| _ -> L.debug ~dkey "Decl and whatever"
@@ -272,6 +260,7 @@ let import_theory env (tenv:tenv) (lenv:lenv) thname =
with W.Env.LibraryNotFound _ ->
L.error "Library %s not found" thname
+
(* -------------------------------------------------------------------------- *)
(* --- Main --- *)
(* -------------------------------------------------------------------------- *)
@@ -284,14 +273,14 @@ let () =
if libs <> [] || imports <> [] then
begin
let wenv = create_why3_env @@ libs in
- let tenv : tenv = W.Ty.Hts.create 0 in
- let lenv : lenv = W.Term.Hls.create 0 in
- let lils : lils = Logic_info.Hashtbl.create 0 in
- let ltits : ltits = Logic_type_info.Hashtbl.create 0 in
- let menv : menv = Datatype.String.Hashtbl.create 0 in
- let genv : genv = { wenv ; tenv; lenv; lils; ltits; menv } in
- add_builtins genv;
- List.iter (import_theory wenv tenv lenv) @@ imports;
+ let tenv = W.Ty.Hts.create 0 in
+ let lenv = W.Term.Hls.create 0 in
+ let _lils = Logic_info.Hashtbl.create 0 in
+ let _ltits = Logic_type_info.Hashtbl.create 0 in
+ let _menv = Datatype.String.Hashtbl.create 0 in
+ let env : env = { wenv; tenv; lenv; _lils; _ltits; _menv } in
+ add_builtins env;
+ List.iter (import_theory env) @@ imports;
W.Ty.Hts.iter (fun (tys) (lti) ->
L.result "Why3 type symbol : %a" pp_tys tys;
L.result "Corresponding CIL logic type info %a" pp_lti lti;