Skip to content
GitLab
Commit 32893b03 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

move [MSH]str and [MSH]int from Util to Stdlib 

Util now is a small module containing misc functions.
parent ba635d27
Hide whitespace changes
Inline Side-by-side
Makefile.in
View file @ 32893b03
......@@ -108,8 +108,8 @@ LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \
src/driver/driver_parser.mli src/driver/driver_parser.ml \
src/driver/driver_lexer.ml src/session/xml.ml
LIB_UTIL = config opt lists strings extmap exthtbl stdlib \
exn_printer pp debug loc print_tree \
LIB_UTIL = config util opt lists strings extmap exthtbl weakhtbl \
hashcons stdlib exn_printer pp debug loc print_tree \
cmdline weakhtbl hashcons util warning sysutil rc plugin
LIB_CORE = ident ty term pattern decl theory task pretty env trans printer
......
examples/runstrat/runstrat.ml
View file @ 32893b03
......@@ -20,7 +20,7 @@
open Format
open Why3
open Util
open Stdlib
open Whyconf
open Theory
open Task
......
plugins/parser/genequlin.ml
View file @ 32893b03
......@@ -45,7 +45,7 @@ open Why3
open Theory
open Term
open Util
open Stdlib
open Ident
......@@ -80,10 +80,10 @@ let read_channel env path filename cin =
(** create a set of constraints *)
let create_fmla nvar m k =
let lvar = mapi (fun _ -> create_vsymbol (id_fresh "x") Ty.ty_int)
let lvar = Util.mapi (fun _ -> create_vsymbol (id_fresh "x") Ty.ty_int)
1 nvar in
let lt = List.map t_var lvar in
let lits = foldi (create_lit lt k) t_true 1 m in
let lits = Util.foldi (create_lit lt k) t_true 1 m in
t_forall_close lvar [] (t_implies_simp lits t_false) in
(** read the first line *)
......
plugins/tptp/tptp_typing.ml
View file @ 32893b03
......@@ -13,7 +13,7 @@ open Format
open Tptp_ast
open Why3
open Util
open Stdlib
open Ident
open Ty
open Term
......@@ -60,7 +60,7 @@ type symbol =
(* dead code
type env = symbol Mstr.t
type implicit = (string,symbol) Hashtbl.t
type implicit = symbol Hstr.t
*)
(** Defined symbols : arithmetic etc... *)
......@@ -107,7 +107,7 @@ let make_denv lib =
let add_theory env impl th =
let s = "$th$" ^ th.th_name.id_string in
if not (Mstr.mem s env) then Hashtbl.replace impl s (Suse th)
if not (Mstr.mem s env) then Hstr.replace impl s (Suse th)
let defined_ty ~loc denv env impl dw tyl =
let ts = match dw with
......@@ -208,9 +208,9 @@ let defined_expr ~loc is_fmla denv env impl dw tl = match dw, tl with
let find_tv ~loc env impl s =
let tv = try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found ->
try Hstr.find impl s with Not_found ->
let tv = STVar (create_tvsymbol (id_user s loc)) in
Hashtbl.add impl s tv;
Hstr.add impl s tv;
tv in
match tv with
| STVar tv -> ty_var tv
......@@ -219,9 +219,9 @@ let find_tv ~loc env impl s =
let find_vs ~loc denv env impl s =
let vs = try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found ->
try Hstr.find impl s with Not_found ->
let vs = SVar (create_vsymbol (id_user s loc) denv.ty_univ) in
Hashtbl.add impl s vs;
Hstr.add impl s vs;
vs in
match vs with
| SVar vs -> t_var vs
......@@ -229,11 +229,11 @@ let find_vs ~loc denv env impl s =
let find_ts ~loc env impl s args =
let ts = try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found ->
try Hstr.find impl s with Not_found ->
let args = List.map (fun _ -> create_tvsymbol (id_fresh "a")) args in
let ss = if s = "int" || s = "real" then "_" ^ s else s in
let ts = SType (create_tysymbol (id_user ss loc) args None) in
Hashtbl.add impl s ts;
Hstr.add impl s ts;
ts in
match ts with
| SType ts -> ts
......@@ -241,29 +241,29 @@ let find_ts ~loc env impl s args =
let find_fs ~loc denv env impl s args =
try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found ->
try Hstr.find impl s with Not_found ->
let args = List.map (fun _ -> denv.ty_univ) args in
let fs = create_fsymbol (id_user s loc) args denv.ty_univ in
let fs = SFunc ([],[],Stv.empty,fs) in
Hashtbl.add impl s fs;
Hstr.add impl s fs;
fs
let find_ps ~loc denv env impl s args =
try Mstr.find s env with Not_found ->
try Hashtbl.find impl s with Not_found ->
try Hstr.find impl s with Not_found ->
let args = List.map (fun _ -> denv.ty_univ) args in
let ps = create_psymbol (id_user s loc) args in
let ps = SPred ([],[],Stv.empty,ps) in
Hashtbl.add impl s ps;
Hstr.add impl s ps;
ps
let find_dobj ~loc denv env impl s =
let ds = "$do$" ^ s in
let fs = try Mstr.find ds env with Not_found ->
try Hashtbl.find impl ds with Not_found ->
try Hstr.find impl ds with Not_found ->
let id = id_user ("do_" ^ s) loc in
let fs = Sdobj (create_fsymbol id [] denv.ty_univ) in
Hashtbl.add impl ds fs;
Hstr.add impl ds fs;
fs in
match fs with
| Sdobj fs -> fs_app fs [] denv.ty_univ
......@@ -369,7 +369,7 @@ and fmla denv env impl pol tvl { e_loc = loc; e_node = n } = match n with
let sk = Format.sprintf "_%s_%d_%d" s ln cn in
let ts = create_tysymbol (id_user sk loc) tvl None in
let tv = ty_app ts (List.map ty_var tvl) in
Hashtbl.add impl sk (SType ts);
Hstr.add impl sk (SType ts);
Mstr.add s (STSko tv) env, pol, tvl, vl, true
else
let ty = ty denv env impl e in
......@@ -535,7 +535,7 @@ let typedecl denv env impl loc s (tvl,(el,e)) =
in
let ss = if s = "int" || s = "real" then "_" ^ s else s in
let ts = create_tysymbol (id_user ss loc) (List.map ntv el) None in
Hashtbl.add impl s (SType ts)
Hstr.add impl s (SType ts)
else
(* function/predicate symbol *)
let ntv (s, { e_node = n ; e_loc = loc }) = match n with
......@@ -558,7 +558,7 @@ let typedecl denv env impl loc s (tvl,(el,e)) =
let tyl = List.map ghost gvl @ tyl in
let ls = create_psymbol (id_user s loc) tyl in
if gvl <> [] then add_theory env impl denv.th_ghost;
Hashtbl.add impl s (SPred (tvl,gvl,mvs,ls))
Hstr.add impl s (SPred (tvl,gvl,mvs,ls))
else
let tyv = ty denv env impl e in
let tvs = ty_freevars tvs tyv in
......@@ -566,7 +566,7 @@ let typedecl denv env impl loc s (tvl,(el,e)) =
let tyl = List.map ghost gvl @ tyl in
let ls = create_fsymbol (id_user s loc) tyl tyv in
if gvl <> [] then add_theory env impl denv.th_ghost;
Hashtbl.add impl s (SFunc (tvl,gvl,mvs,ls))
Hstr.add impl s (SFunc (tvl,gvl,mvs,ls))
let flush_impl ~strict env uc impl =
let update_th _ e uc = match e with
......@@ -603,16 +603,16 @@ let flush_impl ~strict env uc impl =
(* none of these is possible in implicit *)
| SletF _ | SletP _ | STSko _ -> assert false
in
let uc = Hashtbl.fold update_th impl uc in
let res = Hashtbl.fold update impl (env,uc) in
Hashtbl.clear impl;
let uc = Hstr.fold update_th impl uc in
let res = Hstr.fold update impl (env,uc) in
Hstr.clear impl;
res
let typecheck lib path ast =
(* initial environment *)
let env = Mstr.empty in
let denv = make_denv lib in
let impl = Hashtbl.create 17 in
let impl = Hstr.create 17 in
add_theory env impl denv.th_univ;
(* parsing function *)
let conj = ref false in
......
plugins/tptp/tptp_typing.mli
View file @ 32893b03
......@@ -10,5 +10,5 @@
(********************************************************************)
val typecheck : unit Why3.Env.library -> Why3.Env.pathname ->
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Util.Mstr.t
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Stdlib.Mstr.t
src/coq-tactic/why3tac.ml
View file @ 32893b03
......@@ -675,11 +675,11 @@ and decompose_definition dep env c =
| Some b ->
let tvs = List.fold_left Ty.ty_freevars Stv.empty
(Ty.oty_cons ls.ls_args ls.ls_value) in
let add tv tvm = Util.Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Util.Mstr.empty in
let add tv tvm = Stdlib.Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Stdlib.Mstr.empty in
let ty = Global.type_of_global r in
let (_, vars), env, _ = decomp_type_quantifiers env ty in
let conv tv = Util.Mstr.find tv.tv_name.Ident.id_string tvm in
let conv tv = Stdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
let vars = List.map conv vars in
let tvm, env, b = decomp_type_lambdas Idmap.empty env vars b in
let (bv, vsl), env, b =
......
src/core/decl.ml
View file @ 32893b03
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Util
open Stdlib
open Ident
open Ty
open Term
......@@ -260,7 +260,7 @@ type prsymbol = {
pr_name : ident;
}
module Prop = WeakStructMake (struct
module Prop = MakeMSHW (struct
type t = prsymbol
let tag pr = pr.pr_name.id_tag
end)
......@@ -366,7 +366,7 @@ module Hsdecl = Hashcons.Make (struct
end)
module Decl = WeakStructMake (struct
module Decl = MakeMSHW (struct
type t = decl
let tag d = d.d_tag
end)
......@@ -621,7 +621,7 @@ let merge_known kn1 kn2 =
Mid.union check_known kn1 kn2
let known_add_decl kn0 decl =
let kn = Mid.map (const decl) decl.d_news in
let kn = Mid.map (Util.const decl) decl.d_news in
let check id decl0 _ =
if d_equal decl0 decl
then raise (KnownIdent id)
......
src/core/env.ml
View file @ 32893b03
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Util
open Stdlib
open Ident
open Theory
......@@ -47,16 +47,16 @@ let create_env = let c = ref (-1) in fun lp -> {
let get_loadpath env = Sstr.elements env.env_path
let read_format_table = Hashtbl.create 17 (* format name -> read_format *)
let extensions_table = Hashtbl.create 17 (* suffix -> format name *)
let read_format_table = Hstr.create 17 (* format name -> read_format *)
let extensions_table = Hstr.create 17 (* suffix -> format name *)
let lookup_format name =
try Hashtbl.find read_format_table name
try Hstr.find read_format_table name
with Not_found -> raise (UnknownFormat name)
let list_formats () =
let add n (_,_,l,desc) acc = (n,l,desc)::acc in
Hashtbl.fold add read_format_table []
Hstr.fold add read_format_table []
let get_extension file =
let s = try Filename.chop_extension file
......@@ -66,7 +66,7 @@ let get_extension file =
let get_format file =
let ext = get_extension file in
try Hashtbl.find extensions_table ext
try Hstr.find extensions_table ext
with Not_found -> raise (UnknownExtension ext)
let read_channel ?format env file ic =
......@@ -118,11 +118,17 @@ exception CircularDependency of pathname
type 'a contents = 'a * theory Mstr.t
module Hpath = Hashtbl.Make(struct
type t = pathname
let hash = Hashtbl.hash
let equal = (=)
end)
type 'a library = {
lib_env : env;
lib_read : 'a read_format;
lib_exts : extension list;
lib_memo : (pathname, 'a contents option) Hashtbl.t;
lib_memo : ('a contents option) Hpath.t;
}
and 'a read_format =
......@@ -132,7 +138,7 @@ let mk_library read exts env = {
lib_env = env;
lib_read = read;
lib_exts = exts;
lib_memo = Hashtbl.create 17;
lib_memo = Hpath.create 17;
}
let env_of_library lib = lib.lib_env
......@@ -141,18 +147,18 @@ let read_lib_file lib path =
let file = locate_lib_file lib.lib_env path lib.lib_exts in
let ic = open_in file in
try
Hashtbl.replace lib.lib_memo path None;
Hpath.replace lib.lib_memo path None;
let res = lib.lib_read lib path file ic in
Hashtbl.replace lib.lib_memo path (Some res);
Hpath.replace lib.lib_memo path (Some res);
close_in ic;
res
with e ->
Hashtbl.remove lib.lib_memo path;
Hpath.remove lib.lib_memo path;
close_in ic;
raise e
let read_lib_file lib path =
try match Hashtbl.find lib.lib_memo path with
try match Hpath.find lib.lib_memo path with
| Some res -> res
| None -> raise (CircularDependency path)
with Not_found -> read_lib_file lib path
......@@ -172,12 +178,12 @@ let read_lib_theory lib path th =
raise (TheoryNotFound (path,th))
let register_format ~(desc:Pp.formatted) name exts read =
if Hashtbl.mem read_format_table name then raise (KnownFormat name);
if Hstr.mem read_format_table name then raise (KnownFormat name);
let getlib = Wenv.memoize 5 (mk_library read exts) in
let rc env file ic = snd (read (getlib env) [] file ic) in
let rl env path th = read_lib_theory (getlib env) path th in
Hashtbl.add read_format_table name (rc,rl,exts,desc);
List.iter (fun s -> Hashtbl.replace extensions_table s name) exts;
Hstr.add read_format_table name (rc,rl,exts,desc);
List.iter (fun s -> Hstr.replace extensions_table s name) exts;
getlib
let locate_lib_file env format path =
......
src/core/env.mli
View file @ 32893b03
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Util
open Stdlib
open Theory
(** Local type aliases and exceptions *)
......
src/core/ident.ml
View file @ 32893b03
......@@ -10,7 +10,6 @@
(********************************************************************)
open Stdlib
open Util
(** Labels *)
......@@ -19,7 +18,7 @@ type label = {
lab_tag : int;
}
module Lab = StructMake (struct
module Lab = MakeMSH (struct
type t = label
let tag lab = lab.lab_tag
end)
......@@ -52,7 +51,7 @@ type ident = {
id_tag : Weakhtbl.tag; (* unique magical tag *)
}
module Id = WeakStructMake (struct
module Id = MakeMSHW (struct
type t = ident
let tag id = id.id_tag
end)
......
src/core/pattern.ml
View file @ 32893b03
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Util
open Stdlib
open Ident
open Ty
open Term
......
src/core/pretty.ml
View file @ 32893b03
......@@ -11,7 +11,7 @@
open Format
open Pp
open Util
open Stdlib
open Ident
open Ty
open Term
......
src/core/printer.ml
View file @ 32893b03
......@@ -143,9 +143,9 @@ let get_type_arguments t = match t.t_node with
let m = oty_match Mtv.empty ls.ls_value t.t_ty in
let m = List.fold_left2
(fun m ty t -> oty_match m (Some ty) t.t_ty) m ls.ls_args tl in
let name tv = Util.Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Util.Mstr.empty in
Array.of_list (Util.Mstr.values m)
let name tv = Stdlib.Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Stdlib.Mstr.empty in
Array.of_list (Stdlib.Mstr.values m)
| _ ->
[||]
......
src/core/task.ml
View file @ 32893b03
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Util
open Stdlib
open Ident
open Ty
open Term
......
src/core/task.mli
View file @ 32893b03
......@@ -11,7 +11,7 @@
(** Proof Tasks, Cloning and Meta History *)
open Util
open Stdlib
open Ident
open Ty
open Term
......
src/core/term.ml
View file @ 32893b03
......@@ -9,10 +9,9 @@
(* *)
(********************************************************************)
open Util
open Stdlib
open Ident
open Ty
open Stdlib
(** Variable symbols *)
......@@ -21,7 +20,7 @@ type vsymbol = {
vs_ty : ty;
}
module Vsym = WeakStructMake (struct
module Vsym = MakeMSHW (struct
type t = vsymbol
let tag vs = vs.vs_name.id_tag
end)
......@@ -48,7 +47,7 @@ type lsymbol = {
ls_value : ty option;
}
module Lsym = WeakStructMake (struct
module Lsym = MakeMSHW (struct
type t = lsymbol
let tag ls = ls.ls_name.id_tag
end)
......@@ -124,7 +123,7 @@ module Hspat = Hashcons.Make (struct
let tag n p = { p with pat_tag = n }
end)
module Pat = StructMake (struct
module Pat = MakeMSH (struct
type t = pattern
let tag pat = pat.pat_tag
end)
......@@ -181,8 +180,11 @@ let pat_fold fn acc pat = match pat.pat_node with
| Pas (p, _) -> fn acc p
| Por (p, q) -> fn (fn acc p) q
let pat_all pr pat = try pat_fold (all_fn pr) true pat with FoldSkip -> false
let pat_any pr pat = try pat_fold (any_fn pr) false pat with FoldSkip -> true
let pat_all pr pat =
try pat_fold (Util.all_fn pr) true pat with Util.FoldSkip -> false
let pat_any pr pat =
try pat_fold (Util.any_fn pr) false pat with Util.FoldSkip -> true
(* smart constructors for patterns *)
......@@ -443,7 +445,7 @@ module Hsterm = Hashcons.Make (struct
end)
module Term = StructMake (struct
module Term = MakeMSH (struct
type t = term
let tag term = term.t_tag
end)
......@@ -804,7 +806,7 @@ let t_bool_false = fs_app fs_bool_false [] ty_bool
let fs_tuple_ids = Hid.create 17
let fs_tuple = Util.Hint.memo 17 (fun n ->
let fs_tuple = Hint.memo 17 (fun n ->
let ts = ts_tuple n in
let tl = List.map ty_var ts.ts_args in
let ty = ty_app ts tl in
......@@ -955,10 +957,12 @@ let rec t_gen_fold fnT fnL acc t =
let t_s_fold = t_gen_fold
let t_s_all prT prL t =
try t_s_fold (all_fn prT) (all_fn prL) true t with FoldSkip -> false
try t_s_fold (Util.all_fn prT) (Util.all_fn prL) true t
with Util.FoldSkip -> false
let t_s_any prT prL t =
try t_s_fold (any_fn prT) (any_fn prL) false t with FoldSkip -> true
try t_s_fold (Util.any_fn prT) (Util.any_fn prL) false t
with Util.FoldSkip -> true
(* map/fold over types in terms and formulas *)
......@@ -1019,8 +1023,8 @@ let t_fold fn acc t = match t.t_node with
let _, tl, f1 = t_open_quant b in tr_fold fn (fn acc f1) tl
| _ -> t_fold_unsafe fn acc t
let t_all pr t = try t_fold (all_fn pr) true t with FoldSkip -> false
let t_any pr t = try t_fold (any_fn pr) false t with FoldSkip -> true
let t_all pr t = try t_fold (Util.all_fn pr) true t with Util.FoldSkip -> false
let t_any pr t = try t_fold (Util.any_fn pr) false t with Util.FoldSkip -> true
(* safe opening map_fold *)
......
src/core/theory.ml
View file @ 32893b03
......@@ -10,7 +10,7 @@
(********************************************************************)
open Format
open Util
open Stdlib
open Ident
open Ty
open Term
......@@ -101,7 +101,7 @@ let print_meta_desc fmt m =
fprintf fmt "@[%s@\n @[%a@]@]"
m.meta_name Pp.formatted m.meta_desc
module SMmeta = StructMake(struct type t = meta let tag m = m.meta_tag end)
module SMmeta = MakeMSH(struct type t = meta let tag m = m.meta_tag end)
module Smeta = SMmeta.S
module Mmeta = SMmeta.M
......@@ -116,7 +116,7 @@ exception UnknownMeta of string
exception BadMetaArity of meta * int * int
exception MetaTypeMismatch of meta * meta_arg_type * meta_arg_type
let meta_table = Hashtbl.create 17
let meta_table = Hstr.create 17
let mk_meta =
let c = ref (-1) in
......@@ -130,22 +130,20 @@ let mk_meta =
let register_meta ~desc s al excl =
try
let m = Hashtbl.find meta_table s in
let m = Hstr.find meta_table s in
if al = m.meta_type && excl = m.meta_excl then m
else raise (KnownMeta m)
with Not_found ->
let m = mk_meta desc s al excl in
Hashtbl.add meta_table s m;
Hstr.add meta_table s m;
m
let register_meta_excl ~desc s al = register_meta ~desc s al true
let register_meta ~desc s al = register_meta ~desc s al false
let lookup_meta s =
try Hashtbl.find meta_table s
with Not_found -> raise (UnknownMeta s)
let lookup_meta s = Hstr.find_exn meta_table (UnknownMeta s) s
let list_metas () = Hashtbl.fold (fun _ v acc -> v::acc) meta_table []
let list_metas () = Hstr.fold (fun _ v acc -> v::acc) meta_table []
(** Theory *)
......@@ -234,7 +232,7 @@ end)
let mk_tdecl n = Hstdecl.hashcons { td_node = n ; td_tag = -1 }
module Tdecl = StructMake (struct
module Tdecl = MakeMSH (struct
type t = tdecl
let tag td = td.td_tag
end)
......@@ -788,7 +786,7 @@ let highord_theory =
let uc = add_param_decl uc ps_pred_app in
close_theory uc
let tuple_theory = Util.Hint.memo 17 (fun n ->
let tuple_theory = Hint.memo 17 (fun n ->
let ts = ts_tuple n and fs = fs_tuple n in
let pl = List.map (fun _ -> None) ts.ts_args in
let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) [] in
......
src/core/theory.mli
View file @ 32893b03
......@@ -10,7 +10,6 @@
(********************************************************************)