Commit 33bb423f authored by Andrei Paskevich's avatar Andrei Paskevich

make api of maps/sets more consistent

- change takes function as the first argument
- add_new takes exception as the first argument
- find_default is renamed to find_def and takes the default value
  as the first argument
- find_option is renamed to find_opt (to align with find_exn and find_def)
- default_option is renamed def_option
parent 216e869f
......@@ -347,8 +347,8 @@ and let_defn denv env impl { e_node = n ; e_loc = loc } =
let rec check ss vl al = match vl,al with
| [],[] -> ()
| (v,_)::vl, { e_node = Evar u }::al when u = v ->
let ss = Sstr.change v (fun b ->
not (b && error ~loc MalformedLet)) ss in
let ss = Sstr.change (fun b ->
not (b && error ~loc MalformedLet)) v ss in
check ss vl al
| _,_ -> error ~loc MalformedLet in
let dig vl d isf e = match d.e_node with
......
......@@ -48,7 +48,7 @@ let check_tl ty t = ty_equal_check ty (t_type t)
let make_ls_defn ls vl t =
(* check for duplicate arguments *)
let add_v s v = Svs.add_new v (DuplicateVar v) s in
let add_v s v = Svs.add_new (DuplicateVar v) v s in
ignore (List.fold_left add_v Svs.empty vl);
(* build the definition axiom *)
let hd = t_app ls (List.map t_var vl) t.t_ty in
......@@ -149,7 +149,7 @@ let rec match_term vm t acc p = match t.t_node, p.pat_node with
let build_call_graph cgr syms ls =
let call vm s tl =
let desc t = match t.t_node with
| Tvar v -> Mvs.find_default v Unknown vm
| Tvar v -> Mvs.find_def Unknown v vm
| _ -> Unknown
in
Hls.add cgr s (ls, Array.of_list (List.map desc tl))
......@@ -399,7 +399,7 @@ exception EmptyIndDecl of lsymbol
exception NonPositiveTypeDecl of tysymbol * lsymbol * ty
let news_id s id = Sid.add_new id (ClashIdent id) s
let news_id s id = Sid.add_new (ClashIdent id) id s
let syms_ts s ts = Sid.add ts.ts_name s
let syms_ls s ls = Sid.add ls.ls_name s
......
......@@ -68,9 +68,9 @@ module Compile (X : Action) = struct
(* dispatch every case to a primitive constructor/wild case *)
let cases,wilds =
let add_case fs pl a cases =
Mls.change fs (function
Mls.change (function
| None -> Some [pl,a]
| Some rl -> Some ((pl,a)::rl)) cases
| Some rl -> Some ((pl,a)::rl)) fs cases
in
let union_cases pl a types cases =
let add pl q = pat_wild q.pat_ty :: pl in
......
......@@ -148,8 +148,8 @@ let print_prelude fmt pl =
let print_prelude_of_theories th_used fmt pm =
List.iter (fun th ->
let prel = Mid.find_default th.th_name [] pm in
print_prelude fmt prel) th_used
let prel = Mid.find_def [] th.th_name pm in
print_prelude fmt prel) th_used
let print_th_prelude task fmt pm =
let th_used = task_fold (fun acc -> function
......@@ -186,11 +186,11 @@ let remove_prop pr =
type syntax_map = string Mid.t
let sm_add_ts sm = function
| [MAts ts; MAstr rs] -> Mid.add_new ts.ts_name rs (KnownTypeSyntax ts) sm
| [MAts ts; MAstr rs] -> Mid.add_new (KnownTypeSyntax ts) ts.ts_name rs sm
| _ -> assert false
let sm_add_ls sm = function
| [MAls ls; MAstr rs] -> Mid.add_new ls.ls_name rs (KnownLogicSyntax ls) sm
| [MAls ls; MAstr rs] -> Mid.add_new (KnownLogicSyntax ls) ls.ls_name rs sm
| _ -> assert false
let sm_add_pr sm = function
......@@ -213,7 +213,7 @@ let get_syntax_map_of_theory theory =
sm
*)
let query_syntax sm id = Mid.find_option id sm
let query_syntax sm id = Mid.find_opt id sm
let fold_tdecls fn acc =
Trans.on_meta meta_syntax_type (fun sts ->
......
......@@ -54,16 +54,16 @@ let tds_hash tds = Hashweak.tag_hash tds.tds_tag
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
let cm_find cm th = Mid.find_default th.th_name tds_empty cm
let mm_find mm t = Mmeta.find_default t tds_empty mm
let cm_find cm th = Mid.find_def tds_empty th.th_name cm
let mm_find mm t = Mmeta.find_def tds_empty t mm
let cm_add cm th td = Mid.change th.th_name (function
let cm_add cm th td = Mid.change (function
| None -> Some (tds_singleton td)
| Some tds -> Some (tds_add td tds)) cm
| Some tds -> Some (tds_add td tds)) th.th_name cm
let mm_add mm t td = Mmeta.change t (function
let mm_add mm t td = Mmeta.change (function
| None -> Some (tds_singleton td)
| Some tds -> Some (tds_add td tds)) mm
| Some tds -> Some (tds_add td tds)) t mm
let mm_add mm t td = if t.meta_excl
then Mmeta.add t (tds_singleton td) mm
......
......@@ -155,7 +155,7 @@ let pat_wild ty = mk_pattern Pwild Svs.empty ty
let pat_var v = mk_pattern (Pvar v) (Svs.singleton v) v.vs_ty
let pat_as p v =
let s = Svs.add_new v (DuplicateVar v) p.pat_vars in
let s = Svs.add_new (DuplicateVar v) v p.pat_vars in
mk_pattern (Pas (p,v)) s v.vs_ty
let pat_or p q =
......@@ -599,7 +599,7 @@ let rec t_subst_unsafe m t =
let nosubst (_,b,_) = Mvs.set_disjoint m b.bv_vars in
match t.t_node with
| Tvar u ->
Mvs.find_default u t m
Mvs.find_def t u m
| Tlet (e, bt) ->
let d = t_subst e in
if t_equal d e && nosubst bt then t else
......@@ -878,7 +878,7 @@ let rec t_gen_map fnT fnL m t =
let fn = t_gen_map fnT fnL m in
t_label_copy t (match t.t_node with
| Tvar v ->
let u = Mvs.find_default v v m in
let u = Mvs.find_def v v m in
ty_equal_check (fnT v.vs_ty) u.vs_ty;
t_var u
| Tconst _ ->
......@@ -1253,7 +1253,7 @@ let rec t_hash_alpha c m t =
let fn = t_hash_alpha c m in
match t.t_node with
| Tvar v ->
Hashcons.combine 0 (Mvs.find_default v (vs_hash v) m)
Hashcons.combine 0 (Mvs.find_def (vs_hash v) v m)
| Tconst c ->
Hashcons.combine 1 (Hashtbl.hash c)
| Tapp (s,l) ->
......@@ -1428,7 +1428,7 @@ let small t = match t.t_node with
| _ -> false
let t_let_simp e ((v,b,t) as bt) =
let n = Mvs.find_default v 0 t.t_vars in
let n = Mvs.find_def 0 v t.t_vars in
if n = 0 then
t_subst_unsafe b.bv_subst t else
if n = 1 || small e then begin
......@@ -1438,7 +1438,7 @@ let t_let_simp e ((v,b,t) as bt) =
t_let e bt
let t_let_close_simp v e t =
let n = Mvs.find_default v 0 t.t_vars in
let n = Mvs.find_def 0 v t.t_vars in
if n = 0 then t else
if n = 1 || small e then
t_subst_single v e t
......
......@@ -57,13 +57,13 @@ let rec merge_ns chk ns1 ns2 =
ns_pr = ns_union pr_equal chk ns1.ns_pr ns2.ns_pr;
ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mstr.change x (function
let nm_add chk x ns m = Mstr.change (function
| None -> Some ns
| Some os -> Some (merge_ns chk ns os)) m
| Some os -> Some (merge_ns chk ns os)) x m
let ns_add eq chk x v m = Mstr.change x (function
let ns_add eq chk x v m = Mstr.change (function
| None -> Some v
| Some vo -> Some (ns_replace eq chk x vo v)) m
| Some vo -> Some (ns_replace eq chk x vo v)) x m
let ts_add = ns_add ts_equal
let ls_add = ns_add ls_equal
......@@ -627,9 +627,9 @@ let clone_export uc th inst =
let g_ts _ ts = not (Mts.mem ts inst.inst_ts) in
let g_ls _ ls = not (Mls.mem ls inst.inst_ls) in
let f_ts ts = Mts.find_default ts ts cl.ts_table in
let f_ls ls = Mls.find_default ls ls cl.ls_table in
let f_pr pr = Mpr.find_default pr pr cl.pr_table in
let f_ts ts = Mts.find_def ts ts cl.ts_table in
let f_ls ls = Mls.find_def ls ls cl.ls_table in
let f_pr pr = Mpr.find_def pr pr cl.pr_table in
let rec f_ns ns = {
ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.ns_ts);
......@@ -694,9 +694,9 @@ let add_meta uc s al = add_tdecl uc (create_meta s al)
let clone_meta tdt sm = match tdt.td_node with
| Meta (t,al) ->
let find_ts ts = Mts.find_default ts ts sm.sm_ts in
let find_ls ls = Mls.find_default ls ls sm.sm_ls in
let find_pr pr = Mpr.find_default pr pr sm.sm_pr in
let find_ts ts = Mts.find_def ts ts sm.sm_ts in
let find_ls ls = Mls.find_def ls ls sm.sm_ls in
let find_pr pr = Mpr.find_def pr pr sm.sm_pr in
let cl_marg = function
| MAty ty -> MAty (ty_s_map find_ts ty)
| MAts ts -> MAts (find_ts ts)
......
......@@ -157,7 +157,7 @@ exception DuplicateTypeVar of tvsymbol
exception UnboundTypeVar of tvsymbol
let create_tysymbol name args def =
let add s v = Stv.add_new v (DuplicateTypeVar v) s in
let add s v = Stv.add_new (DuplicateTypeVar v) v s in
let s = List.fold_left add Stv.empty args in
let check v = Stv.mem v s || raise (UnboundTypeVar v) in
ignore (option_map (ty_v_all check) def);
......@@ -194,7 +194,7 @@ let ty_s_any pr ty =
(* type matching *)
let rec ty_inst s ty = match ty.ty_node with
| Tyvar n -> Mtv.find_default n ty s
| Tyvar n -> Mtv.find_def ty n s
| _ -> ty_map (ty_inst s) ty
let rec ty_match s ty1 ty2 =
......@@ -206,7 +206,7 @@ let rec ty_match s ty1 ty2 =
match ty1.ty_node, ty2.ty_node with
| Tyapp (f1,l1), Tyapp (f2,l2) when ts_equal f1 f2 ->
List.fold_left2 ty_match s l1 l2
| Tyvar n1, _ -> Mtv.change n1 set s
| Tyvar n1, _ -> Mtv.change set n1 s
| _ -> raise Exit
exception TypeMismatch of ty * ty
......
......@@ -175,7 +175,7 @@ let call_on_file ~command ?(timelimit=0) ?(memlimit=0)
(try List.assoc n exitcodes with Not_found -> grep out regexps)
in
Debug.dprintf debug "Call_provers: prover output:@\n%s@." out;
let time = Util.default_option time (grep_time out timeregexps) in
let time = Util.def_option time (grep_time out timeregexps) in
let ans = match ans with
| HighFailure when !on_timelimit && timelimit > 0
&& time >= (0.9 *. float timelimit) -> Timeout
......
......@@ -141,7 +141,7 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
in
let add_local th = function
| Rprelude s ->
let l = Mid.find_default th.th_name [] !thprelude in
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (c,q,s) ->
let td = syntax_type (find_ts th q) s in
......
......@@ -473,7 +473,7 @@ let do_theory env drv fname tname th glist =
end
let do_global_theory env drv (tname,p,t,glist) =
let format = Util.default_option "why" !opt_parser in
let format = Util.def_option "why" !opt_parser in
let th = try Env.read_theory ~format env p t with Env.TheoryNotFound _ ->
eprintf "Theory '%s' not found.@." tname;
exit 1
......
......@@ -146,7 +146,7 @@ let create_user_id { id = x ; id_lab = ll ; id_loc = loc } =
| Lpos p -> ll, Some p
in
let label,p = List.fold_left get_labels (Slab.empty,None) ll in
id_user ~label x (default_option loc p)
id_user ~label x (def_option loc p)
let create_user_vs id ty = create_vsymbol (create_user_id id) ty
......
......@@ -246,7 +246,7 @@ let is_projection uc ls =
| _ -> (* not a function with 1 argument *) raise Exit
in
ignore (List.fold_left (fun tvs t -> match t.ty_node with
| Ty.Tyvar tv -> Stv.add_new tv Exit tvs
| Ty.Tyvar tv -> Stv.add_new Exit tv tvs
| _ -> (* not a generic type *) raise Exit) Stv.empty tl);
let kn = get_known uc in
let lsc = match Decl.find_constructors kn ts with
......
......@@ -54,13 +54,13 @@ let rec merge_ns chk ns1 ns2 =
{ ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mstr.change x (function
let nm_add chk x ns m = Mstr.change (function
| None -> Some ns
| Some os -> Some (merge_ns chk ns os)) m
| Some os -> Some (merge_ns chk ns os)) x m
let ns_add eq chk x v m = Mstr.change x (function
let ns_add eq chk x v m = Mstr.change (function
| None -> Some v
| Some vo -> Some (ns_replace eq chk x vo v)) m
| Some vo -> Some (ns_replace eq chk x vo v)) x m
let ex_add = ns_add ls_equal
let mt_add = ns_add mt_equal
......
......@@ -374,7 +374,7 @@ let rec dexpr ~ghost ~userloc env e =
let loc = e.Ptree.expr_loc in
let labs, userloc, d = extract_labels [] userloc e in
let d, ty = dexpr_desc ~ghost ~userloc env loc d in
let loc = default_option loc userloc in
let loc = def_option loc userloc in
let e = {
dexpr_desc = d; dexpr_loc = loc; dexpr_lab = labs; dexpr_type = ty; }
in
......@@ -480,7 +480,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
let s = fs_tuple n in
let tyl = List.map (fun _ -> create_type_var loc) el in
let ty = tyapp (ts_tuple n) tyl in
let uloc = default_option loc userloc in
let uloc = def_option loc userloc in
let create d ty = { dexpr_desc = d; dexpr_type = ty;
dexpr_loc = uloc; dexpr_lab = [] } in
let apply e1 e2 ty2 =
......@@ -498,7 +498,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
new_regions_vars ();
let tyl, ty = specialize_lsymbol ~loc (Htv.create 17) cs in
let ty = of_option ty in
let uloc = default_option loc userloc in
let uloc = def_option loc userloc in
let create d ty = { dexpr_desc = d; dexpr_type = ty;
dexpr_loc = uloc; dexpr_lab = [] } in
let constructor d f tyf = match f with
......@@ -550,7 +550,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
Queue.push v q
in
List.iter2 set_pat_var_ty fl tyl;
let uloc = default_option loc userloc in
let uloc = def_option loc userloc in
let create d ty = { dexpr_desc = d; dexpr_type = ty;
dexpr_loc = uloc; dexpr_lab = [] } in
let apply t f tyf = match f with
......
......@@ -233,7 +233,7 @@ let quantify env rm sreg f =
| Tyvar _ -> assert false
in
let id = Spv.fold test vars None in
let id = id_clone (default_option r.R.r_tv.tv_name id) in
let id = id_clone (def_option r.R.r_tv.tv_name id) in
let r' = create_vsymbol id (purify r.R.r_ty) in
Mtv.add r.R.r_tv r' m
in
......
......@@ -300,7 +300,7 @@ exception NoTask
let goal_task g = Util.exn_option NoTask g.goal_task
let goal_task_option g = g.goal_task
let goal_expl g = Util.default_option g.goal_name.Ident.id_string g.goal_expl
let goal_expl g = Util.def_option g.goal_name.Ident.id_string g.goal_expl
(************************)
(* saving state on disk *)
......@@ -1105,7 +1105,7 @@ let load_prover eS prover =
PHprover.find eS.loaded_provers prover
with Not_found ->
let provers = Whyconf.get_provers eS.whyconf in
let r = Mprover.find_option prover provers in
let r = Mprover.find_opt prover provers in
let r = match r with
| None -> None
| Some pr ->
......@@ -1147,11 +1147,11 @@ let copy_external_proof
let session = match env_session with
| Some eS -> Some eS.session
| _ -> session in
let obsolete = default_option a.proof_obsolete obsolete in
let archived = default_option a.proof_archived archived in
let timelimit = default_option a.proof_timelimit timelimit in
let pas = default_option a.proof_state attempt_status in
let ngoal = default_option a.proof_parent goal in
let obsolete = def_option a.proof_obsolete obsolete in
let archived = def_option a.proof_archived archived in
let timelimit = def_option a.proof_timelimit timelimit in
let pas = def_option a.proof_state attempt_status in
let ngoal = def_option a.proof_parent goal in
let nprover = match prover with
| None -> a.proof_prover
| Some prover -> prover in
......
......@@ -45,7 +45,7 @@ let convert_unknown_prover ~keygen env_session =
let unknown_provers =
Mprover.mapi (utkp known_provers) unknown_provers in
session_iter_proof_attempt (fun pr ->
let pks = Mprover.find_default pr.proof_prover [] unknown_provers in
let pks = Mprover.find_def [] pr.proof_prover unknown_provers in
List.iter (fun pk ->
(** If such a prover already exists we add nothing *)
if not (PHprover.mem pr.proof_parent.goal_external_proofs pk) then
......
......@@ -62,8 +62,8 @@ module Lsmap = struct
| None -> Some (create_lsymbol (id_clone ls.ls_name) tyl tyv)
| nls -> nls
in
let insts = Mls.find_default ls Mtyl.empty lsmap in
Mls.add ls (Mtyl.change (oty_cons tyl tyv) newls insts) lsmap
let insts = Mls.find_def Mtyl.empty ls lsmap in
Mls.add ls (Mtyl.change newls (oty_cons tyl tyv) insts) lsmap
let print_env fmt menv =
Format.fprintf fmt "defined_lsymbol (%a)@."
......@@ -85,7 +85,7 @@ module Lsmap = struct
| [MAls ls; MAls lsinst] ->
let tydisl = oty_cons lsinst.ls_args lsinst.ls_value in
if not (List.for_all Ty.ty_closed tydisl) then env else
let insts = Mls.find_default ls Mtyl.empty env in
let insts = Mls.find_def Mtyl.empty ls env in
Mls.add ls (Mtyl.add tydisl lsinst insts) env
| _ -> assert false
in
......@@ -98,9 +98,9 @@ let find_logic env ls tyl tyv =
try Mtyl.find (oty_cons tyl tyv) (Mls.find ls env)
with Not_found -> ls
module Ssubst =
Set.Make(struct type t = ty Mtv.t
let compare = Mtv.compare OHTy.compare end)
module Ssubst = Set.Make(struct
type t = ty Mtv.t
let compare = Mtv.compare OHTy.compare end)
(* find all the possible instantiation which can create a kept instantiation *)
let ty_quant env t =
......@@ -112,7 +112,7 @@ let ty_quant env t =
let fold_inst inst _ acc =
let fold_subst subst acc =
try
let subst = List.fold_left2 ty_match subst tyl inst in
let subst = List.fold_left2 ty_match subst tyl inst in
Ssubst.add subst acc
with TypeMismatch _ -> acc
in
......@@ -129,7 +129,7 @@ let ts_of_ls env ls decls =
let add_ts sts ts = Sts.add ts sts in
let add_ty sts ty = ty_s_fold add_ts sts ty in
let add_tyl tyl _ sts = List.fold_left add_ty sts tyl in
let insts = Mls.find_default ls Mtyl.empty env in
let insts = Mls.find_def Mtyl.empty ls env in
let sts = Mtyl.fold add_tyl insts Sts.empty in
let add_ts ts dl = create_ty_decl [ts,Tabstract] :: dl in
Sts.fold add_ts sts decls
......@@ -141,7 +141,7 @@ let map env d = match d.d_node with
"Algebraic and recursively-defined types are \
not supported, run eliminate_algebraic"
| Dlogic [ls, None] ->
let lls = Mtyl.values (Mls.find_default ls Mtyl.empty env) in
let lls = Mtyl.values (Mls.find_def Mtyl.empty ls env) in
let lds = List.map (fun ls -> create_logic_decl [ls,None]) lls in
ts_of_ls env ls (d::lds)
| Dlogic [ls, Some ld] when not (Sid.mem ls.ls_name d.d_syms) ->
......
......@@ -26,7 +26,7 @@ open Theory
open Task
let t_unfold env fs tl ty =
match Mls.find_option fs env with
match Mls.find_opt fs env with
| None ->
t_app fs tl ty
| Some (vl,e) ->
......
......@@ -107,7 +107,7 @@ let empty_section = Mstr.empty
let make_t tl =
let add_key acc (key,value) =
let l = Mstr.find_default key [] acc in
let l = Mstr.find_def [] key acc in
Mstr.add key (value::l) acc in
let add_section t (args,sectionl) =
let sname,arg = match args with
......@@ -117,7 +117,7 @@ let make_t tl =
| sname::_ -> raise (ExtraParameters sname) in
let m = List.fold_left add_key empty_section sectionl in
let m = Mstr.map List.rev m in
let l = Mstr.find_default sname [] t in
let l = Mstr.find_def [] sname t in
Mstr.add sname ((arg,m)::l) t in
List.fold_left add_section empty tl
......
......@@ -31,8 +31,8 @@ module type S =
val add: key -> 'a -> 'a t -> 'a t
val singleton: key -> 'a -> 'a t
val remove: key -> 'a t -> 'a t
val merge: (key -> 'a option -> 'b option -> 'c option)
-> 'a t -> 'b t -> 'c t
val merge:
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val compare: ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal: ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter: (key -> 'a -> unit) -> 'a t -> unit
......@@ -52,7 +52,7 @@ module type S =
val mapi: (key -> 'a -> 'b) -> 'a t -> 'b t
(** Added into why stdlib version *)
val change : key -> ('a option -> 'a option) -> 'a t -> 'a t
val change : ('a option -> 'a option) -> key -> 'a t -> 'a t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val inter : (key -> 'a -> 'b -> 'c option) -> 'a t -> 'b t -> 'c t
val diff : (key -> 'a -> 'b -> 'a option) -> 'a t -> 'b t -> 'a t
......@@ -62,20 +62,20 @@ module type S =
val set_diff : 'a t -> 'b t -> 'a t
val set_submap : 'a t -> 'b t -> bool
val set_disjoint : 'a t -> 'b t -> bool
val find_default : key -> 'a -> 'a t -> 'a
val find_option : key -> 'a t -> 'a option
val find_def : 'a -> key -> 'a t -> 'a
val find_opt : key -> 'a t -> 'a option
val find_exn : exn -> key -> 'a t -> 'a
val map_filter: ('a -> 'b option) -> 'a t -> 'b t
val mapi_filter: (key -> 'a -> 'b option) -> 'a t -> 'b t
val mapi_fold:
(key -> 'a -> 'acc -> 'acc * 'b) -> 'a t -> 'acc -> 'acc * 'b t
val fold2_inter: (key -> 'a -> 'b -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val fold2_union: (key -> 'a option -> 'b option -> 'c -> 'c) ->
'a t -> 'b t -> 'c -> 'c
val fold2_union:
(key -> 'a option -> 'b option -> 'c -> 'c) -> 'a t -> 'b t -> 'c -> 'c
val translate : (key -> key) -> 'a t -> 'a t
val mapi_filter_fold:
(key -> 'a -> 'acc -> 'acc * 'b option) -> 'a t -> 'acc -> 'acc * 'b t
val add_new : key -> 'a -> exn -> 'a t -> 'a t
val add_new : exn -> key -> 'a -> 'a t -> 'a t
val keys: 'a t -> key list
val values: 'a t -> 'a list
......@@ -107,13 +107,13 @@ module type S =
val max_elt: t -> elt
val choose: t -> elt
val split: elt -> t -> t * bool * t
val change : elt -> (bool -> bool) -> t -> t
val change : (bool -> bool) -> elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val fold2: (elt -> 'a -> 'a) -> t -> t -> 'a -> 'a
val translate : (elt -> elt) -> t -> t
val add_new : elt -> exn -> t -> t
val add_new : exn -> elt -> t -> t
end
module Set : Set
......@@ -401,7 +401,7 @@ module Make(Ord: OrderedType) = struct
(** Added into why stdlib version *)
let rec change x f = function
let rec change f x = function
| Empty ->
begin match f None with
| None -> Empty
......@@ -415,9 +415,9 @@ module Make(Ord: OrderedType) = struct
| None -> merge_bal l r
| Some d -> Node(l, x, d, r, h)
else if c < 0 then
bal (change x f l) v d r
bal (change f x l) v d r
else
bal l v d (change x f r)
bal l v d (change f x r)
let rec union f s1 s2 =
match (s1, s2) with
......@@ -426,7 +426,7 @@ module Make(Ord: OrderedType) = struct
| (Node(l1, v1, d1, r1, h1), Node(l2, v2, d2, r2, h2)) ->
if h1 >= h2 then
if h2 = 1 then
change v2 (function None -> Some d2 | Some d1 -> f v2 d1 d2) s1
change (function None -> Some d2 | Some d1 -> f v2 d1 d2) v2 s1
else begin
let (l2, d2, r2) = split v1 s2 in
match d2 with
......@@ -437,7 +437,7 @@ module Make(Ord: OrderedType) = struct
end
else
if h1 = 1 then
change v1 (function None -> Some d1 | Some d2 -> f v1 d1 d2) s2
change (function None -> Some d1 | Some d2 -> f v1 d1 d2) v1 s2
else begin
let (l1, d1, r1) = split v2 s1 in
match d1 with
......@@ -504,19 +504,19 @@ module Make(Ord: OrderedType) = struct
let set_disjoint m1 m2 = disjoint (fun _ _ _ -> false) m1 m2
let rec find_default x def = function
let rec find_def def x = function
Empty -> def
| Node(l, v, d, r, _) ->
let c = Ord.compare x v in
if c = 0 then d
else find_default x def (if c < 0 then l else r)
else find_def def x (if c < 0 then l else r)
let rec find_option x = function
let rec find_opt x = function
Empty -> None
| Node(l, v, d, r, _) ->
let c = Ord.compare x v in
if c = 0 then Some d
else find_option x (if c < 0 then l else r)
else find_opt x (if c < 0 then l else r)
let rec find_exn exn x = function
Empty -> raise exn
......@@ -604,9 +604,9 @@ module Make(Ord: OrderedType) = struct
let acc,r' = mapi_filter_fold f r acc in
acc, concat_or_join l' v d' r'
let add_new x v e m = change x (function