--- a/src/Pure/General/graph.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/General/graph.ML Thu Sep 01 18:48:50 2005 +0200
@@ -86,11 +86,11 @@
fun maximals (Graph tab) = Table.fold (fn (m, (_, (_, []))) => cons m | _ => I) tab [];
fun get_entry (Graph tab) x =
- (case Table.lookup (tab, x) of
+ (case Table.curried_lookup tab x of
SOME entry => entry
| NONE => raise UNDEF x);
-fun map_entry x f (G as Graph tab) = Graph (Table.update ((x, f (get_entry G x)), tab));
+fun map_entry x f (G as Graph tab) = Graph (Table.curried_update (x, f (get_entry G x)) tab);
(* nodes *)
@@ -142,7 +142,7 @@
(* nodes *)
fun new_node (x, info) (Graph tab) =
- Graph (Table.update_new ((x, (info, ([], []))), tab));
+ Graph (Table.curried_update_new (x, (info, ([], []))) tab);
fun default_node (x, info) (Graph tab) =
Graph (Table.default (x, (info, ([], []))) tab);
--- a/src/Pure/General/name_space.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/General/name_space.ML Thu Sep 01 18:48:50 2005 +0200
@@ -113,7 +113,7 @@
val empty = NameSpace Symtab.empty;
fun lookup (NameSpace tab) xname =
- (case Symtab.lookup (tab, xname) of
+ (case Symtab.curried_lookup tab xname of
NONE => (xname, true)
| SOME ([], []) => (xname, true)
| SOME ([name], _) => (name, true)
@@ -150,7 +150,7 @@
(* basic operations *)
fun map_space f xname (NameSpace tab) =
- NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
+ NameSpace (Symtab.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab);
fun del (name: string) = remove (op =) name;
fun add name names = name :: del name names;
--- a/src/Pure/General/output.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/General/output.ML Thu Sep 01 18:48:50 2005 +0200
@@ -84,7 +84,7 @@
exception MISSING_DEFAULT_OUTPUT;
-fun lookup_mode name = Symtab.lookup (! modes, name);
+fun lookup_mode name = Symtab.curried_lookup (! modes) name;
fun get_mode () =
(case Library.get_first lookup_mode (! print_mode) of SOME p => p
@@ -141,7 +141,7 @@
fun add_mode name (f, g, h) =
(if is_none (lookup_mode name) then ()
else warning ("Redeclaration of symbol print mode: " ^ quote name);
- modes := Symtab.update ((name, {output_width = f, indent = g, raw = h}), ! modes));
+ modes := Symtab.curried_update (name, {output_width = f, indent = g, raw = h}) (! modes));
(* produce errors *)
--- a/src/Pure/General/symbol.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/General/symbol.ML Thu Sep 01 18:48:50 2005 +0200
@@ -350,7 +350,7 @@
else if is_ascii_quasi s then Quasi
else if is_ascii_blank s then Blank
else if is_char s then Other
- else if_none (Symtab.lookup (symbol_kinds, s)) Other;
+ else if_none (Symtab.curried_lookup symbol_kinds s) Other;
end;
fun is_letter s = kind s = Letter;
--- a/src/Pure/Isar/attrib.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Sep 01 18:48:50 2005 +0200
@@ -104,7 +104,7 @@
val attrs = #2 (AttributesData.get thy);
fun attr src =
let val ((name, _), pos) = Args.dest_src src in
- (case Symtab.lookup (attrs, name) of
+ (case Symtab.curried_lookup attrs name of
NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos)
| SOME ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src))
end;
--- a/src/Pure/Isar/isar_output.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/isar_output.ML Thu Sep 01 18:48:50 2005 +0200
@@ -59,7 +59,7 @@
fun add_item kind (name, x) tab =
(if not (Symtab.defined tab name) then ()
else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name);
- Symtab.update ((name, x), tab));
+ Symtab.curried_update (name, x) tab);
in
@@ -68,13 +68,13 @@
fun command src =
let val ((name, _), pos) = Args.dest_src src in
- (case Symtab.lookup (! global_commands, name) of
+ (case Symtab.curried_lookup (! global_commands) name of
NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos)
| SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src))
end;
fun option (name, s) f () =
- (case Symtab.lookup (! global_options, name) of
+ (case Symtab.curried_lookup (! global_options) name of
NONE => error ("Unknown antiquotation option: " ^ quote name)
| SOME opt => opt s f ());
--- a/src/Pure/Isar/locale.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/locale.ML Thu Sep 01 18:48:50 2005 +0200
@@ -168,7 +168,7 @@
fun tinst_tab_type tinst T = if Symtab.is_empty tinst
then T
else Term.map_type_tfree
- (fn (v as (x, _)) => getOpt (Symtab.lookup (tinst, x), (TFree v))) T;
+ (fn (v as (x, _)) => getOpt (Symtab.curried_lookup tinst x, (TFree v))) T;
fun tinst_tab_term tinst t = if Symtab.is_empty tinst
then t
@@ -201,7 +201,7 @@
else (* instantiate terms and types simultaneously *)
let
fun instf (Const (x, T)) = Const (x, tinst_tab_type tinst T)
- | instf (Free (x, T)) = (case Symtab.lookup (inst, x) of
+ | instf (Free (x, T)) = (case Symtab.curried_lookup inst x of
NONE => Free (x, tinst_tab_type tinst T)
| SOME t => t)
| instf (Var (xi, T)) = Var (xi, tinst_tab_type tinst T)
@@ -322,7 +322,7 @@
val sups =
List.filter (fn (t', _) => Pattern.matches sign (t, t')) (Termtab.dest regs);
val sups' = map (apfst untermify) sups
- in (Termtab.update ((t, (attn, [])), regs), sups') end
+ in (Termtab.curried_update (t, (attn, [])) regs, sups') end
| _ => (regs, []))
end;
@@ -331,9 +331,9 @@
fun add_witness ts thm regs =
let
val t = termify ts;
- val (x, thms) = valOf (Termtab.lookup (regs, t));
+ val (x, thms) = valOf (Termtab.curried_lookup regs t);
in
- Termtab.update ((t, (x, thm::thms)), regs)
+ Termtab.curried_update (t, (x, thm::thms)) regs
end;
end;
@@ -398,9 +398,9 @@
fun put_locale name loc =
GlobalLocalesData.map (fn (space, locs, regs) =>
- (space, Symtab.update ((name, loc), locs), regs));
+ (space, Symtab.curried_update (name, loc) locs, regs));
-fun get_locale thy name = Symtab.lookup (#2 (GlobalLocalesData.get thy), name);
+fun get_locale thy name = Symtab.curried_lookup (#2 (GlobalLocalesData.get thy)) name;
fun the_locale thy name =
(case get_locale thy name of
@@ -417,7 +417,7 @@
(* retrieve registration from theory or context *)
fun gen_get_registrations get thy_ctxt name =
- case Symtab.lookup (get thy_ctxt, name) of
+ case Symtab.curried_lookup (get thy_ctxt) name of
NONE => []
| SOME reg => Registrations.dest reg;
@@ -427,7 +427,7 @@
gen_get_registrations LocalLocalesData.get;
fun gen_get_registration get thy_of thy_ctxt (name, ps) =
- case Symtab.lookup (get thy_ctxt, name) of
+ case Symtab.curried_lookup (get thy_ctxt) name of
NONE => NONE
| SOME reg => Registrations.lookup (thy_of thy_ctxt) (reg, ps);
@@ -452,7 +452,7 @@
map_data (fn regs =>
let
val thy = thy_of thy_ctxt;
- val reg = getOpt (Symtab.lookup (regs, name), Registrations.empty);
+ val reg = getOpt (Symtab.curried_lookup regs name, Registrations.empty);
val (reg', sups) = Registrations.insert thy (ps, attn) reg;
val _ = if not (null sups) then warning
("Subsumed interpretation(s) of locale " ^
@@ -460,7 +460,7 @@
"\nby interpretation(s) with the following prefix(es):\n" ^
commas_quote (map (fn (_, ((s, _), _)) => s) sups))
else ();
- in Symtab.update ((name, reg'), regs) end) thy_ctxt;
+ in Symtab.curried_update (name, reg') regs end) thy_ctxt;
val put_global_registration =
gen_put_registration (fn f =>
@@ -480,13 +480,8 @@
(* add witness theorem to registration in theory or context,
ignored if registration not present *)
-fun gen_add_witness map (name, ps) thm =
- map (fn regs =>
- let
- val reg = valOf (Symtab.lookup (regs, name));
- in
- Symtab.update ((name, Registrations.add_witness ps thm reg), regs)
- end handle Option => regs);
+fun gen_add_witness map_regs (name, ps) thm =
+ map_regs (Symtab.map_entry name (Registrations.add_witness ps thm));
val add_global_witness =
gen_add_witness (fn f =>
@@ -550,7 +545,7 @@
val loc_int = intern thy loc;
val regs = get_regs thy_ctxt;
- val loc_regs = Symtab.lookup (regs, loc_int);
+ val loc_regs = Symtab.curried_lookup regs loc_int;
in
(case loc_regs of
NONE => Pretty.str ("No interpretations in " ^ msg ^ ".")
@@ -762,7 +757,7 @@
fun params_of' elemss = gen_distinct eq_fst (List.concat (map (snd o fst o fst) elemss));
fun params_syn_of syn elemss =
gen_distinct eq_fst (List.concat (map (snd o fst) elemss)) |>
- map (apfst (fn x => (x, valOf (Symtab.lookup (syn, x)))));
+ map (apfst (fn x => (x, valOf (Symtab.curried_lookup syn x))));
(* CB: param_types has the following type:
@@ -1008,7 +1003,7 @@
val {params = (ps, qs), elems, ...} = the_locale thy name;
val ps' = map (apsnd SOME o #1) ps;
val ren = map #1 ps' ~~
- map (fn x => (x, valOf (Symtab.lookup (syn, x)))) xs;
+ map (fn x => (x, valOf (Symtab.curried_lookup syn x))) xs;
val (params', elems') =
if null ren then ((ps', qs), map #1 elems)
else ((map (apfst (rename ren)) ps', map (rename ren) qs),
@@ -1740,7 +1735,7 @@
|> Symtab.make;
(* replace parameter names in ids by instantiations *)
val vinst = Symtab.make (parms ~~ vts);
- fun vinst_names ps = map (fn p => Symtab.lookup (vinst, p) |> valOf) ps;
+ fun vinst_names ps = map (the o Symtab.curried_lookup vinst) ps;
val inst = Symtab.make (parms ~~ ts);
val ids' = map (apsnd vinst_names) ids;
val wits = List.concat (map (snd o valOf o get_global_registration thy) ids');
@@ -2008,7 +2003,7 @@
|> put_locale name {predicate = predicate, import = import,
elems = map (fn e => (e, stamp ())) elems',
params = (params_of elemss' |>
- map (fn (x, SOME T) => ((x, T), valOf (Symtab.lookup (syn, x)))), map #1 (params_of body_elemss)),
+ map (fn (x, SOME T) => ((x, T), the (Symtab.curried_lookup syn x))), map #1 (params_of body_elemss)),
regs = []}
|> pair (elems', body_ctxt)
end;
@@ -2177,7 +2172,7 @@
NONE => error ("Instance missing for parameter " ^ quote p)
| SOME (Free (_, T), t) => (t, T);
val d = t |> inst_tab_term (inst, tinst) |> Envir.beta_norm;
- in (Symtab.update_new ((p, d), inst), tinst) end;
+ in (Symtab.curried_update_new (p, d) inst, tinst) end;
val (inst, tinst) = Library.foldl add_def ((inst, tinst), not_given);
(* Note: inst and tinst contain no vars. *)
--- a/src/Pure/Isar/method.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/method.ML Thu Sep 01 18:48:50 2005 +0200
@@ -560,7 +560,7 @@
val ((raw_name, _), pos) = Args.dest_src src;
val name = NameSpace.intern space raw_name;
in
- (case Symtab.lookup (meths, name) of
+ (case Symtab.curried_lookup meths name of
NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
| SOME ((mth, _), _) => transform_failure (curry METHOD_FAIL (name, pos)) (mth src))
end;
--- a/src/Pure/Isar/outer_syntax.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Sep 01 18:48:50 2005 +0200
@@ -125,10 +125,10 @@
fun get_lexicons () = ! global_lexicons;
fun get_parsers () = ! global_parsers;
-fun get_parser () = Option.map (#2 o #1) o curry Symtab.lookup (get_parsers ());
+fun get_parser () = Option.map (#2 o #1) o Symtab.curried_lookup (get_parsers ());
fun command_tags name =
- (case Symtab.lookup (get_parsers (), name) of
+ (case Symtab.curried_lookup (get_parsers ()) name of
SOME (((_, k), _), _) => OuterKeyword.tags_of k
| NONE => []);
@@ -143,7 +143,7 @@
fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
(if not (Symtab.defined tab name) then ()
else warning ("Redefined outer syntax command " ^ quote name);
- Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
+ Symtab.curried_update (name, (((comment, kind), (int_only, parse)), markup)) tab);
fun add_parsers parsers =
(change_parsers (fold add_parser parsers);
--- a/src/Pure/Isar/proof_context.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Sep 01 18:48:50 2005 +0200
@@ -364,18 +364,18 @@
(** default sorts and types **)
-fun def_sort ctxt xi = Vartab.lookup (#2 (defaults_of ctxt), xi);
+val def_sort = Vartab.curried_lookup o #2 o defaults_of;
fun def_type ctxt pattern xi =
let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in
- (case Vartab.lookup (types, xi) of
+ (case Vartab.curried_lookup types xi of
NONE =>
if pattern then NONE
- else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2)
+ else Vartab.curried_lookup binds xi |> Option.map (TypeInfer.polymorphicT o #2)
| some => some)
end;
-fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt), (x, ~1));
+fun default_type ctxt x = Vartab.curried_lookup (#1 (defaults_of ctxt)) (x, ~1);
val used_types = #3 o defaults_of;
@@ -492,7 +492,7 @@
val binds = binds_of ctxt;
fun norm (t as Var (xi, T)) =
- (case Vartab.lookup (binds, xi) of
+ (case Vartab.curried_lookup binds xi of
SOME (u, U) =>
let
val env = unifyT ctxt (T, U) handle Type.TUNIFY =>
@@ -596,24 +596,24 @@
local
val ins_types = fold_aterms
- (fn Free (x, T) => curry Vartab.update ((x, ~1), T)
- | Var v => curry Vartab.update v
+ (fn Free (x, T) => Vartab.curried_update ((x, ~1), T)
+ | Var v => Vartab.curried_update v
| _ => I);
val ins_sorts = fold_types (fold_atyps
- (fn TFree (x, S) => curry Vartab.update ((x, ~1), S)
- | TVar v => curry Vartab.update v
+ (fn TFree (x, S) => Vartab.curried_update ((x, ~1), S)
+ | TVar v => Vartab.curried_update v
| _ => I));
val ins_used = fold_term_types (fn t =>
fold_atyps (fn TFree (x, _) => insert (op =) x | _ => I));
val ins_occs = fold_term_types (fn t =>
- fold_atyps (fn TFree (x, _) => curry Symtab.update_multi (x, t) | _ => I));
+ fold_atyps (fn TFree (x, _) => Symtab.curried_update_multi (x, t) | _ => I));
fun ins_skolem def_ty = fold_rev (fn (x, x') =>
(case def_ty x' of
- SOME T => curry Vartab.update ((x, ~1), T)
+ SOME T => Vartab.curried_update ((x, ~1), T)
| NONE => I));
fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
@@ -632,7 +632,7 @@
|> declare_term_syntax t
|> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
|> map_defaults (fn (types, sorts, used, occ) =>
- (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) (fixes_of ctxt) types,
+ (ins_skolem (fn x => Vartab.curried_lookup types (x, ~1)) (fixes_of ctxt) types,
sorts, used, occ));
end;
@@ -690,7 +690,7 @@
val occs_outer = type_occs_of outer;
fun add a gen =
if Symtab.defined occs_outer a orelse
- exists still_fixed (Symtab.lookup_multi (occs_inner, a))
+ exists still_fixed (Symtab.curried_lookup_multi occs_inner a)
then gen else a :: gen;
in fn tfrees => fold add tfrees [] end;
@@ -777,7 +777,7 @@
else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
in
map_context (fn (syntax, asms, binds, thms, cases, defs) =>
- (syntax, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs))
+ (syntax, asms, Vartab.curried_update ((x, i), (t', T)) binds, thms, cases, defs))
o declare_term t'
end;
@@ -935,7 +935,7 @@
val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
val name = PureThy.name_of_thmref thmref;
in
- (case Symtab.lookup (tab, name) of
+ (case Symtab.curried_lookup tab name of
SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
| NONE => from_thy thy xthmref) |> pick name
end
@@ -990,7 +990,7 @@
let
val name = NameSpace.full naming bname;
val space' = NameSpace.declare naming name space;
- val tab' = Symtab.update ((name, ths), tab);
+ val tab' = Symtab.curried_update (name, ths) tab;
val index' = FactIndex.add (is_known ctxt) (name, ths) index;
in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
--- a/src/Pure/Isar/term_style.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Isar/term_style.ML Thu Sep 01 18:48:50 2005 +0200
@@ -2,7 +2,8 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Styles for terms, to use with the "term_style" and "thm_style" antiquotations.
+Styles for terms, to use with the "term_style" and "thm_style"
+antiquotations.
*)
signature TERM_STYLE =
@@ -39,12 +40,12 @@
(* accessors *)
fun the_style thy name =
- (case Symtab.lookup (StyleData.get thy, name) of
+ (case Symtab.curried_lookup (StyleData.get thy) name of
NONE => error ("Unknown antiquote style: " ^ quote name)
| SOME (style, _) => style);
fun add_style name style thy =
- StyleData.map (curry Symtab.update_new (name, (style, stamp ()))) thy
+ StyleData.map (Symtab.curried_update_new (name, (style, stamp ()))) thy
handle Symtab.DUP _ => err_dup_styles [name];
--- a/src/Pure/Syntax/ast.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Syntax/ast.ML Thu Sep 01 18:48:50 2005 +0200
@@ -157,7 +157,7 @@
if a = b then env else raise NO_MATCH
| mtch (Variable a) (Constant b) env =
if a = b then env else raise NO_MATCH
- | mtch ast (Variable x) env = Symtab.update ((x, ast), env)
+ | mtch ast (Variable x) env = Symtab.curried_update (x, ast) env
| mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
| mtch _ _ _ = raise NO_MATCH
and mtch_lst (ast :: asts) (pat :: pats) env =
@@ -189,7 +189,7 @@
val changes = ref 0;
fun subst _ (ast as Constant _) = ast
- | subst env (Variable x) = the (Symtab.lookup (env, x))
+ | subst env (Variable x) = the (Symtab.curried_lookup env x)
| subst env (Appl asts) = Appl (map (subst env) asts);
fun try_rules ((lhs, rhs) :: pats) ast =
--- a/src/Pure/Syntax/parser.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Syntax/parser.ML Thu Sep 01 18:48:50 2005 +0200
@@ -446,9 +446,9 @@
let
(*Get tag for existing nonterminal or create a new one*)
fun get_tag nt_count tags nt =
- case Symtab.lookup (tags, nt) of
+ case Symtab.curried_lookup tags nt of
SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
+ | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
nt_count);
(*Convert symbols to the form used by the parser;
@@ -523,9 +523,9 @@
(*get existing tag from grammar1 or create a new one*)
fun get_tag nt_count tags nt =
- case Symtab.lookup (tags, nt) of
+ case Symtab.curried_lookup tags nt of
SOME tag => (nt_count, tags, tag)
- | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
+ | NONE => (nt_count+1, Symtab.curried_update_new (nt, nt_count) tags,
nt_count)
val ((nt_count1', tags1'), tag_table) =
@@ -868,7 +868,7 @@
fun earley prods tags chains startsymbol indata =
let
- val start_tag = case Symtab.lookup (tags, startsymbol) of
+ val start_tag = case Symtab.curried_lookup tags startsymbol of
SOME tag => tag
| NONE => error ("parse: Unknown startsymbol " ^
quote startsymbol);
--- a/src/Pure/Syntax/printer.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Syntax/printer.ML Thu Sep 01 18:48:50 2005 +0200
@@ -248,7 +248,7 @@
val tab = fold f fmts (mode_tab prtabs mode);
in AList.update (op =) (mode, tab) prtabs end;
-fun extend_prtabs m = change_prtabs (curry Symtab.update_multi) m;
+fun extend_prtabs m = change_prtabs Symtab.curried_update_multi m;
fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
fun merge_prtabs prtabs1 prtabs2 =
@@ -330,7 +330,7 @@
(*find matching table entry, or print as prefix / postfix*)
fun prnt ([], []) = prefixT tup
- | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi (tb, a), tbs)
+ | prnt ([], tb :: tbs) = prnt (Symtab.curried_lookup_multi tb a, tbs)
| prnt ((pr, n, p') :: prnps, tbs) =
if nargs = n then parT (pr, args, p, p')
else if nargs > n andalso not type_mode then
--- a/src/Pure/Syntax/syntax.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Sep 01 18:48:50 2005 +0200
@@ -82,7 +82,7 @@
(* parse (ast) translations *)
-fun lookup_tr tab c = Option.map fst (Symtab.lookup (tab, c));
+fun lookup_tr tab c = Option.map fst (Symtab.curried_lookup tab c);
fun err_dup_trfuns name cs =
error ("More than one " ^ name ^ " for " ^ commas_quote cs);
@@ -98,8 +98,8 @@
(* print (ast) translations *)
-fun lookup_tr' tab c = map fst (Symtab.lookup_multi (tab, c));
-fun extend_tr'tab trfuns = fold_rev (curry Symtab.update_multi) trfuns;
+fun lookup_tr' tab c = map fst (Symtab.curried_lookup_multi tab c);
+fun extend_tr'tab trfuns = fold_rev Symtab.curried_update_multi trfuns;
fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
@@ -147,16 +147,12 @@
type ruletab = (Ast.ast * Ast.ast) list Symtab.table;
fun dest_ruletab tab = List.concat (map snd (Symtab.dest tab));
-fun lookup_ruletab tab a = Symtab.lookup_multi (tab, a);
(* empty, extend, merge ruletabs *)
-val extend_ruletab =
- fold_rev (fn r => fn tab => Symtab.update_multi ((Ast.head_of_rule r, r), tab));
-
+val extend_ruletab = fold_rev (fn r => Symtab.curried_update_multi (Ast.head_of_rule r, r));
val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
-
fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
@@ -389,7 +385,7 @@
val asts = read_asts thy is_logtype syn false (SynExt.typ_to_nonterm ty) str;
in
SynTrans.asts_to_terms thy (lookup_tr parse_trtab)
- (map (Ast.normalize_ast (lookup_ruletab parse_ruletab)) asts)
+ (map (Ast.normalize_ast (Symtab.curried_lookup_multi parse_ruletab)) asts)
end;
@@ -473,7 +469,7 @@
in
prt_t thy curried prtabs (lookup_tr' print_ast_trtab)
(lookup_tokentr tokentrtab (! print_mode))
- (Ast.normalize_ast (lookup_ruletab print_ruletab) ast)
+ (Ast.normalize_ast (Symtab.curried_lookup_multi print_ruletab) ast)
end;
val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
--- a/src/Pure/Thy/html.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Thy/html.ML Thu Sep 01 18:48:50 2005 +0200
@@ -205,7 +205,7 @@
fun output_sym s =
if Symbol.is_raw s then (1.0, Symbol.decode_raw s)
else
- (case Symtab.lookup (html_syms, s) of SOME x => x
+ (case Symtab.curried_lookup html_syms s of SOME x => x
| NONE => (real (size s), translate_string escape s));
fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
--- a/src/Pure/Thy/present.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Thy/present.ML Thu Sep 01 18:48:50 2005 +0200
@@ -172,13 +172,13 @@
fun init_theory_info name info =
change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
- (Symtab.update ((name, info), theories), files, tex_index, html_index, graph));
+ (Symtab.curried_update (name, info) theories, files, tex_index, html_index, graph));
fun change_theory_info name f =
change_browser_info (fn (info as (theories, files, tex_index, html_index, graph)) =>
- (case Symtab.lookup (theories, name) of
+ (case Symtab.curried_lookup theories name of
NONE => (warning ("Browser info: cannot access theory document " ^ quote name); info)
- | SOME info => (Symtab.update ((name, map_theory_info f info), theories), files,
+ | SOME info => (Symtab.curried_update (name, map_theory_info f info) theories, files,
tex_index, html_index, graph)));
--- a/src/Pure/Thy/thm_database.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Thy/thm_database.ML Thu Sep 01 18:48:50 2005 +0200
@@ -88,7 +88,7 @@
fun result prfx bname =
if (prfx = "" orelse is_ml_identifier prfx) andalso is_ml_identifier bname andalso
NameSpace.intern space xname = name then
- SOME (prfx, (bname, xname, length (the (Symtab.lookup (thms, name))) = 1))
+ SOME (prfx, (bname, xname, length (the (Symtab.curried_lookup thms name)) = 1))
else NONE;
val names = NameSpace.unpack name;
in
--- a/src/Pure/Thy/thy_parse.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/Thy/thy_parse.ML Thu Sep 01 18:48:50 2005 +0200
@@ -469,7 +469,7 @@
end;
fun sect tab ((Keyword, s, n) :: toks) =
- (case Symtab.lookup (tab, s) of
+ (case Symtab.curried_lookup tab s of
SOME parse => !! parse toks
| NONE => syn_err "section" s n)
| sect _ ((_, s, n) :: _) = syn_err "section" s n
--- a/src/Pure/axclass.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/axclass.ML Thu Sep 01 18:48:50 2005 +0200
@@ -153,7 +153,7 @@
(* get and put data *)
-fun lookup_axclass_info thy c = Symtab.lookup (AxclassesData.get thy, c);
+val lookup_axclass_info = Symtab.curried_lookup o AxclassesData.get;
fun get_axclass_info thy c =
(case lookup_axclass_info thy c of
@@ -161,7 +161,7 @@
| SOME info => info);
fun put_axclass_info c info thy =
- thy |> AxclassesData.put (Symtab.update ((c, info), AxclassesData.get thy));
+ thy |> AxclassesData.put (Symtab.curried_update (c, info) (AxclassesData.get thy));
(* class_axms *)
--- a/src/Pure/compress.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/compress.ML Thu Sep 01 18:48:50 2005 +0200
@@ -42,11 +42,11 @@
let
val typs = #1 (CompressData.get thy);
fun compress T =
- (case Typtab.lookup (! typs, T) of
+ (case Typtab.curried_lookup (! typs) T of
SOME T' => T'
| NONE =>
let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
- in change typs (curry Typtab.update (T', T')); T' end);
+ in change typs (Typtab.curried_update (T', T')); T' end);
in compress end;
@@ -58,9 +58,9 @@
fun compress (t $ u) = compress t $ compress u
| compress (Abs (a, T, t)) = Abs (a, T, compress t)
| compress t =
- (case Termtab.lookup (! terms, t) of
+ (case Termtab.curried_lookup (! terms) t of
SOME t' => t'
- | NONE => (change terms (curry Termtab.update (t, t)); t));
+ | NONE => (change terms (Termtab.curried_update (t, t)); t));
in compress o map_term_types (typ thy) end;
end;
--- a/src/Pure/context.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/context.ML Thu Sep 01 18:48:50 2005 +0200
@@ -121,7 +121,7 @@
val kinds = ref (Inttab.empty: kind Inttab.table);
fun invoke meth_name meth_fn k =
- (case Inttab.lookup (! kinds, k) of
+ (case Inttab.curried_lookup (! kinds) k of
SOME kind => meth_fn kind |> transform_failure (fn exn =>
DATA_FAIL (exn, "Theory data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
| NONE => sys_error ("Invalid theory data identifier " ^ string_of_int k));
@@ -140,7 +140,7 @@
val kind = {name = name, empty = empty, copy = copy, extend = extend, merge = merge};
val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
warning ("Duplicate declaration of theory data " ^ quote name));
- val _ = kinds := Inttab.update ((k, kind), ! kinds);
+ val _ = change kinds (Inttab.curried_update (k, kind));
in k end;
val copy_data = Inttab.map' invoke_copy;
@@ -256,7 +256,7 @@
if draft_id id orelse Inttab.defined ids (#1 id) then ids
else if Inttab.exists (equal (#2 id) o #2) ids then
raise TERM ("Different versions of theory component " ^ quote (#2 id), [])
- else Inttab.update (id, ids);
+ else Inttab.curried_update id ids;
fun check_insert intermediate id (ids, iids) =
let val ids' = check_ins id ids and iids' = check_ins id iids
@@ -423,12 +423,12 @@
val declare = declare_theory_data;
fun get k dest thy =
- (case Inttab.lookup (#theory (data_of thy), k) of
+ (case Inttab.curried_lookup (#theory (data_of thy)) k of
SOME x => (dest x handle Match =>
error ("Failed to access theory data " ^ quote (invoke_name k)))
| NONE => error ("Uninitialized theory data " ^ quote (invoke_name k)));
-fun put k mk x = modify_thy (map_theory (curry Inttab.update (k, mk x)));
+fun put k mk x = modify_thy (map_theory (Inttab.curried_update (k, mk x)));
fun init k = put k I (invoke_empty k);
end;
@@ -525,7 +525,7 @@
val kinds = ref (Inttab.empty: kind Inttab.table);
fun invoke meth_name meth_fn k =
- (case Inttab.lookup (! kinds, k) of
+ (case Inttab.curried_lookup (! kinds) k of
SOME kind => meth_fn kind |> transform_failure (fn exn =>
DATA_FAIL (exn, "Proof data method " ^ #name kind ^ "." ^ meth_name ^ " failed"))
| NONE => sys_error ("Invalid proof data identifier " ^ string_of_int k));
@@ -549,18 +549,18 @@
val kind = {name = name, init = init};
val _ = conditional (Inttab.exists (equal name o #name o #2) (! kinds)) (fn () =>
warning ("Duplicate declaration of proof data " ^ quote name));
- val _ = kinds := Inttab.update ((k, kind), ! kinds);
+ val _ = change kinds (Inttab.curried_update (k, kind));
in k end;
-fun init k = modify_thy (map_proof (curry Inttab.update (k, ())));
+fun init k = modify_thy (map_proof (Inttab.curried_update (k, ())));
fun get k dest prf =
- (case Inttab.lookup (data_of_proof prf, k) of
+ (case Inttab.curried_lookup (data_of_proof prf) k of
SOME x => (dest x handle Match =>
error ("Failed to access proof data " ^ quote (invoke_name k)))
| NONE => error ("Uninitialized proof data " ^ quote (invoke_name k)));
-fun put k mk x = map_prf (curry Inttab.update (k, mk x));
+fun put k mk x = map_prf (Inttab.curried_update (k, mk x));
end;
--- a/src/Pure/fact_index.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/fact_index.ML Thu Sep 01 18:48:50 2005 +0200
@@ -55,7 +55,7 @@
fun add pred (name, ths) (Index {next, facts, consts, frees}) =
let
- fun upd a tab = Symtab.update_multi ((a, (next, (name, ths))), tab);
+ fun upd a = Symtab.curried_update_multi (a, (next, (name, ths)));
val (cs, xs) = fold (index_thm pred) ths ([], []);
in
Index {next = next + 1, facts = (name, ths) :: facts,
@@ -74,7 +74,7 @@
fun find idx ([], []) = facts idx
| find (Index {consts, frees, ...}) (cs, xs) =
- (map (curry Symtab.lookup_multi consts) cs @
- map (curry Symtab.lookup_multi frees) xs) |> intersects |> map #2;
+ (map (Symtab.curried_lookup_multi consts) cs @
+ map (Symtab.curried_lookup_multi frees) xs) |> intersects |> map #2;
end;
--- a/src/Pure/net.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/net.ML Thu Sep 01 18:48:50 2005 +0200
@@ -94,8 +94,8 @@
Net{comb=comb, var=ins1(keys,var), atoms=atoms}
| ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
let
- val net' = if_none (Symtab.lookup (atoms, a)) empty;
- val atoms' = Symtab.update ((a, ins1(keys,net')), atoms);
+ val net' = if_none (Symtab.curried_lookup atoms a) empty;
+ val atoms' = Symtab.curried_update (a, ins1 (keys, net')) atoms;
in Net{comb=comb, var=var, atoms=atoms'} end
in ins1 (keys,net) end;
@@ -126,12 +126,12 @@
newnet{comb=comb, var=del1(keys,var), atoms=atoms}
| del1 (AtomK a :: keys, Net{comb,var,atoms}) =
let val atoms' =
- (case Symtab.lookup (atoms, a) of
+ (case Symtab.curried_lookup atoms a of
NONE => raise DELETE
| SOME net' =>
(case del1 (keys, net') of
Leaf [] => Symtab.delete a atoms
- | net'' => Symtab.update ((a, net''), atoms)))
+ | net'' => Symtab.curried_update (a, net'') atoms))
in newnet{comb=comb, var=var, atoms=atoms'} end
in del1 (keys,net) end;
@@ -143,7 +143,7 @@
exception ABSENT;
fun the_atom atoms a =
- (case Symtab.lookup (atoms, a) of
+ (case Symtab.curried_lookup atoms a of
NONE => raise ABSENT
| SOME net => net);
@@ -222,7 +222,7 @@
subtr comb1 comb2
#> subtr var1 var2
#> Symtab.fold (fn (a, net) =>
- subtr (if_none (Symtab.lookup (atoms1, a)) emptynet) net) atoms2
+ subtr (if_none (Symtab.curried_lookup atoms1 a) emptynet) net) atoms2
in subtr net1 net2 [] end;
fun entries net = subtract (K false) empty net;
--- a/src/Pure/pattern.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/pattern.ML Thu Sep 01 18:48:50 2005 +0200
@@ -357,7 +357,7 @@
if loose_bvar(t,0) then raise MATCH
else (case Envir.lookup' (insts, (ixn, T)) of
NONE => (typ_match thy (tyinsts, (T, fastype_of t)),
- Vartab.update_new ((ixn, (T, t)), insts))
+ Vartab.curried_update_new (ixn, (T, t)) insts)
| SOME u => if t aeconv u then instsp else raise MATCH)
| (Free (a,T), Free (b,U)) =>
if a=b then (typ_match thy (tyinsts,(T,U)), insts) else raise MATCH
@@ -378,11 +378,11 @@
fun match_bind(itms,binders,ixn,T,is,t) =
let val js = loose_bnos t
in if null is
- then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH
+ then if null js then Vartab.curried_update_new (ixn, (T, t)) itms else raise MATCH
else if js subset_int is
then let val t' = if downto0(is,length binders - 1) then t
else mapbnd (idx is) t
- in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end
+ in Vartab.curried_update_new (ixn, (T, mkabs (binders, is, t'))) itms end
else raise MATCH
end;
--- a/src/Pure/proof_general.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/proof_general.ML Thu Sep 01 18:48:50 2005 +0200
@@ -811,11 +811,11 @@
fun get_keywords_classification_table () =
case (!keywords_classification_table) of
- SOME t => t
- | NONE => (let
- val tab = Library.foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab))
- (Symtab.empty,OuterSyntax.dest_parsers())
- in (keywords_classification_table := SOME tab; tab) end)
+ SOME t => t
+ | NONE => (let
+ val tab = fold (fn (c, _, k, _) => Symtab.curried_update (c, k))
+ (OuterSyntax.dest_parsers ()) Symtab.empty;
+ in (keywords_classification_table := SOME tab; tab) end)
@@ -959,7 +959,7 @@
fun xmls_of_transition (name,str,toks) =
let
- val classification = Symtab.lookup (get_keywords_classification_table(),name)
+ val classification = Symtab.curried_lookup (get_keywords_classification_table ()) name
in case classification of
SOME k => (xmls_of_kind k (name,toks,str))
| NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
--- a/src/Pure/proofterm.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/proofterm.ML Thu Sep 01 18:48:50 2005 +0200
@@ -143,10 +143,10 @@
| oras_of (prf % _) = oras_of prf
| oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
| oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
- case Symtab.lookup (thms, name) of
- NONE => oras_of prf (Symtab.update ((name, [prop]), thms), oras)
+ case Symtab.curried_lookup thms name of
+ NONE => oras_of prf (Symtab.curried_update (name, [prop]) thms, oras)
| SOME ps => if prop mem ps then tabs else
- oras_of prf (Symtab.update ((name, prop::ps), thms), oras))
+ oras_of prf (Symtab.curried_update (name, prop::ps) thms, oras))
| oras_of (Oracle (s, prop, _)) =
apsnd (OrdList.insert string_term_ord (s, prop))
| oras_of (MinProof (thms, _, oras)) =
@@ -162,10 +162,10 @@
| thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
| thms_of_proof (prf % _) = thms_of_proof prf
| thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
- case Symtab.lookup (tab, s) of
- NONE => thms_of_proof prf (Symtab.update ((s, [(prop, prf')]), tab))
+ case Symtab.curried_lookup tab s of
+ NONE => thms_of_proof prf (Symtab.curried_update (s, [(prop, prf')]) tab)
| SOME ps => if exists (equal prop o fst) ps then tab else
- thms_of_proof prf (Symtab.update ((s, (prop, prf')::ps), tab)))
+ thms_of_proof prf (Symtab.curried_update (s, (prop, prf')::ps) tab))
| thms_of_proof (MinProof (prfs, _, _)) = fold (thms_of_proof o proof_of_min_thm) prfs
| thms_of_proof _ = I;
@@ -173,7 +173,7 @@
| axms_of_proof (AbsP (_, _, prf)) = axms_of_proof prf
| axms_of_proof (prf1 %% prf2) = axms_of_proof prf1 #> axms_of_proof prf2
| axms_of_proof (prf % _) = axms_of_proof prf
- | axms_of_proof (prf as PAxm (s, _, _)) = curry Symtab.update (s, prf)
+ | axms_of_proof (prf as PAxm (s, _, _)) = Symtab.curried_update (s, prf)
| axms_of_proof (MinProof (_, prfs, _)) = fold (axms_of_proof o proof_of_min_axm) prfs
| axms_of_proof _ = I;
--- a/src/Pure/pure_thy.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/pure_thy.ML Thu Sep 01 18:48:50 2005 +0200
@@ -208,8 +208,8 @@
val (space, thms) = #theorems (get_theorems thy);
in
fn name =>
- Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*)
- (Symtab.lookup (thms, NameSpace.intern space name)) (*static content*)
+ Option.map (map (Thm.transfer (Theory.deref thy_ref))) (*dynamic identity*)
+ (Symtab.curried_lookup thms (NameSpace.intern space name)) (*static content*)
end;
fun get_thms_closure thy =
@@ -309,10 +309,10 @@
val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
val r as ref {theorems = (space, theorems), index} = get_theorems_ref thy';
val space' = Sign.declare_name thy' name space;
- val theorems' = Symtab.update ((name, thms'), theorems);
+ val theorems' = Symtab.curried_update (name, thms') theorems;
val index' = FactIndex.add (K false) (name, thms') index;
in
- (case Symtab.lookup (theorems, name) of
+ (case Symtab.curried_lookup theorems name of
NONE => ()
| SOME thms'' =>
if Thm.eq_thms (thms', thms'') then warn_same name
--- a/src/Pure/sign.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/sign.ML Thu Sep 01 18:48:50 2005 +0200
@@ -282,8 +282,8 @@
fun const_constraint thy c =
let val ((_, consts), constraints) = #consts (rep_sg thy) in
- (case Symtab.lookup (constraints, c) of
- NONE => Option.map #1 (Symtab.lookup (consts, c))
+ (case Symtab.curried_lookup constraints c of
+ NONE => Option.map #1 (Symtab.curried_lookup consts c)
| some => some)
end;
@@ -291,7 +291,7 @@
(case const_constraint thy c of SOME T => T
| NONE => raise TYPE ("Undeclared constant " ^ quote c, [], []));
-fun const_type thy c = Option.map #1 (Symtab.lookup (#2 (#1 (#consts (rep_sg thy))), c));
+val const_type = Option.map #1 oo (Symtab.curried_lookup o #2 o #1 o #consts o rep_sg);
fun the_const_type thy c =
(case const_type thy c of SOME T => T
@@ -514,7 +514,7 @@
fun read_tyname thy raw_c =
let val c = intern_type thy raw_c in
- (case Symtab.lookup (#2 (#types (Type.rep_tsig (tsig_of thy))), c) of
+ (case Symtab.curried_lookup (#2 (#types (Type.rep_tsig (tsig_of thy)))) c of
SOME (Type.LogicalType n, _) => Type (c, replicate n dummyT)
| _ => error ("Undeclared type constructor: " ^ quote c))
end;
@@ -714,7 +714,7 @@
handle TYPE (msg, _, _) => error msg;
val _ = cert_term thy (Const (c, T))
handle TYPE (msg, _, _) => error msg;
- in thy |> map_consts (apsnd (curry Symtab.update (c, T))) end;
+ in thy |> map_consts (apsnd (Symtab.curried_update (c, T))) end;
val add_const_constraint = gen_add_constraint intern_const (read_typ o no_def_sort);
val add_const_constraint_i = gen_add_constraint (K I) certify_typ;
--- a/src/Pure/sorts.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/sorts.ML Thu Sep 01 18:48:50 2005 +0200
@@ -180,7 +180,7 @@
fun mg_domain (classes, arities) a S =
let
fun dom c =
- (case AList.lookup (op =) (Symtab.lookup_multi (arities, a)) c of
+ (case AList.lookup (op =) (Symtab.curried_lookup_multi arities a) c of
NONE => raise DOMAIN (a, c)
| SOME Ss => Ss);
fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);
--- a/src/Pure/thm.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/thm.ML Thu Sep 01 18:48:50 2005 +0200
@@ -524,7 +524,7 @@
fun get_axiom_i theory name =
let
fun get_ax thy =
- Symtab.lookup (#2 (#axioms (Theory.rep_theory thy)), name)
+ Symtab.curried_lookup (#2 (#axioms (Theory.rep_theory thy))) name
|> Option.map (fn prop =>
Thm {thy_ref = Theory.self_ref thy,
der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
@@ -1482,7 +1482,7 @@
fun invoke_oracle_i thy1 name =
let
val oracle =
- (case Symtab.lookup (#2 (#oracles (Theory.rep_theory thy1)), name) of
+ (case Symtab.curried_lookup (#2 (#oracles (Theory.rep_theory thy1))) name of
NONE => raise THM ("Unknown oracle: " ^ name, 0, [])
| SOME (f, _) => f);
val thy_ref1 = Theory.self_ref thy1;
--- a/src/Pure/type.ML Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/type.ML Thu Sep 01 18:48:50 2005 +0200
@@ -167,7 +167,7 @@
val Ts' = map cert Ts;
fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
in
- (case Symtab.lookup (types, c) of
+ (case Symtab.curried_lookup types c of
SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
| SOME (Abbreviation (vs, U, syn), _) => (nargs (length vs);
if syn then check_syntax c else ();
@@ -284,7 +284,7 @@
[TVar (ixn, S), TVar (ixn, S')], []);
fun lookup (tye, (ixn, S)) =
- (case Vartab.lookup (tye, ixn) of
+ (case Vartab.curried_lookup tye ixn of
NONE => NONE
| SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
@@ -298,7 +298,7 @@
fun match (TVar (v, S), T) subs =
(case lookup (subs, (v, S)) of
NONE =>
- if of_sort tsig (T, S) then Vartab.update_new ((v, (S, T)), subs)
+ if of_sort tsig (T, S) then Vartab.curried_update_new (v, (S, T)) subs
else raise TYPE_MATCH
| SOME U => if U = T then subs else raise TYPE_MATCH)
| match (Type (a, Ts), Type (b, Us)) subs =
@@ -317,7 +317,7 @@
(*purely structural matching*)
fun raw_match (TVar (v, S), T) subs =
(case lookup (subs, (v, S)) of
- NONE => Vartab.update_new ((v, (S, T)), subs)
+ NONE => Vartab.curried_update_new (v, (S, T)) subs
| SOME U => if U = T then subs else raise TYPE_MATCH)
| raw_match (Type (a, Ts), Type (b, Us)) subs =
if a <> b then raise TYPE_MATCH
@@ -366,8 +366,8 @@
fun meet (_, []) tye = tye
| meet (TVar (xi, S'), S) tye =
if Sorts.sort_le classes (S', S) then tye
- else Vartab.update_new ((xi, (S',
- gen_tyvar (Sorts.inter_sort classes (S', S)))), tye)
+ else Vartab.curried_update_new
+ (xi, (S', gen_tyvar (Sorts.inter_sort classes (S', S)))) tye
| meet (TFree (_, S'), S) tye =
if Sorts.sort_le classes (S', S) then tye
else raise TUNIFY
@@ -381,19 +381,19 @@
if eq_ix (v, w) then
if S1 = S2 then tye else tvar_clash v S1 S2
else if Sorts.sort_le classes (S1, S2) then
- Vartab.update_new ((w, (S2, T)), tye)
+ Vartab.curried_update_new (w, (S2, T)) tye
else if Sorts.sort_le classes (S2, S1) then
- Vartab.update_new ((v, (S1, U)), tye)
+ Vartab.curried_update_new (v, (S1, U)) tye
else
let val S = gen_tyvar (Sorts.inter_sort classes (S1, S2)) in
- Vartab.update_new ((v, (S1, S)), Vartab.update_new ((w, (S2, S)), tye))
+ Vartab.curried_update_new (v, (S1, S)) (Vartab.curried_update_new (w, (S2, S)) tye)
end
| (TVar (v, S), T) =>
if occurs v tye T then raise TUNIFY
- else meet (T, S) (Vartab.update_new ((v, (S, T)), tye))
+ else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
| (T, TVar (v, S)) =>
if occurs v tye T then raise TUNIFY
- else meet (T, S) (Vartab.update_new ((v, (S, T)), tye))
+ else meet (T, S) (Vartab.curried_update_new (v, (S, T)) tye)
| (Type (a, Ts), Type (b, Us)) =>
if a <> b then raise TUNIFY
else unifs (Ts, Us) tye
@@ -408,13 +408,13 @@
(T as TVar (v, S1), U as TVar (w, S2)) =>
if eq_ix (v, w) then
if S1 = S2 then tye else tvar_clash v S1 S2
- else Vartab.update_new ((w, (S2, T)), tye)
+ else Vartab.curried_update_new (w, (S2, T)) tye
| (TVar (v, S), T) =>
if occurs v tye T then raise TUNIFY
- else Vartab.update_new ((v, (S, T)), tye)
+ else Vartab.curried_update_new (v, (S, T)) tye
| (T, TVar (v, S)) =>
if occurs v tye T then raise TUNIFY
- else Vartab.update_new ((v, (S, T)), tye)
+ else Vartab.curried_update_new (v, (S, T)) tye
| (Type (a, Ts), Type (b, Us)) =>
if a <> b then raise TUNIFY
else raw_unifys (Ts, Us) tye
@@ -476,9 +476,9 @@
fun insert_arities pp classes (t, ars) arities =
let val ars' =
- Symtab.lookup_multi (arities, t)
+ Symtab.curried_lookup_multi arities t
|> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
- in Symtab.update ((t, ars'), arities) end;
+ in Symtab.curried_update (t, ars') arities end;
fun insert_table pp classes = Symtab.fold (fn (t, ars) =>
insert_arities pp classes (t, map (apsnd (map (Sorts.norm_sort classes))) ars));
@@ -488,7 +488,7 @@
fun add_arities pp decls tsig = tsig |> map_tsig (fn (classes, default, types, arities) =>
let
fun prep (t, Ss, S) =
- (case Symtab.lookup (#2 types, t) of
+ (case Symtab.curried_lookup (#2 types) t of
SOME (LogicalType n, _) =>
if length Ss = n then
(t, map (cert_sort tsig) Ss, cert_sort tsig S)
@@ -591,18 +591,18 @@
val c' = NameSpace.full naming c;
val space' = NameSpace.declare naming c' space;
val types' =
- (case Symtab.lookup (types, c') of
+ (case Symtab.curried_lookup types c' of
SOME (decl', _) => err_in_decls c' decl decl'
- | NONE => Symtab.update ((c', (decl, stamp ())), types));
+ | NONE => Symtab.curried_update (c', (decl, stamp ())) types);
in (space', types') end;
-fun the_decl (_, types) c = fst (the (Symtab.lookup (types, c)));
+fun the_decl (_, types) = fst o the o Symtab.curried_lookup types;
fun change_types f = map_tsig (fn (classes, default, types, arities) =>
(classes, default, f types, arities));
fun syntactic types (Type (c, Ts)) =
- (case Symtab.lookup (types, c) of SOME (Nonterminal, _) => true | _ => false)
+ (case Symtab.curried_lookup types c of SOME (Nonterminal, _) => true | _ => false)
orelse exists (syntactic types) Ts
| syntactic _ _ = false;