# HG changeset patch # User wenzelm # Date 1125605710 -7200 # Node ID 430edc6b782623db4b61131f08608bc9f6704037 # Parent 819bc7f224233bbd5afc092573b2ca22f8d36224 curried_lookup/update; tuned; diff -r 819bc7f22423 -r 430edc6b7826 src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Thu Sep 01 22:15:10 2005 +0200 @@ -11,7 +11,7 @@ It works by (a) massaging both sides to bring the selected term to the front: - #m*u + (i + j) ~~ #m'*u + (i' + j') + #m*u + (i + j) ~~ #m'*u + (i' + j') (b) then using bal_add1 or bal_add2 to reach @@ -36,7 +36,7 @@ val bal_add1: thm val bal_add2: thm (*proof tools*) - val prove_conv: tactic list -> theory -> + val prove_conv: tactic list -> theory -> thm list -> string list -> term * term -> thm option val trans_tac: simpset -> thm option -> tactic (*applies the initial lemma*) val norm_tac: simpset -> tactic (*proves the initial lemma*) @@ -48,24 +48,22 @@ functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): sig val proc: theory -> simpset -> term -> thm option - end + end = struct (*For t = #n*u then put u in the table*) -fun update_by_coeff (tab, t) = - Termtab.update ((#2 (Data.dest_coeff t), ()), tab); +fun update_by_coeff t = + Termtab.curried_update (#2 (Data.dest_coeff t), ()); (*a left-to-right scan of terms1, seeking a term of the form #n*u, where #m*u is in terms2 for some m*) fun find_common (terms1,terms2) = - let val tab2 = Library.foldl update_by_coeff (Termtab.empty, terms2) - fun seek [] = raise TERM("find_common", []) - | seek (t::terms) = - let val (_,u) = Data.dest_coeff t - in if isSome (Termtab.lookup (tab2, u)) then u - else seek terms - end + let val tab2 = fold update_by_coeff terms2 Termtab.empty + fun seek [] = raise TERM("find_common", []) + | seek (t::terms) = + let val (_,u) = Data.dest_coeff t + in if Termtab.defined tab2 u then u else seek terms end in seek terms1 end; (*the simplification procedure*) @@ -74,7 +72,7 @@ val hyps = prems_of_ss ss; (*first freeze any Vars in the term to prevent flex-flex problems*) val (t', xs) = Term.adhoc_freeze_vars t; - val (t1,t2) = Data.dest_bal t' + val (t1,t2) = Data.dest_bal t' val terms1 = Data.dest_sum t1 and terms2 = Data.dest_sum t2 val u = find_common (terms1,terms2) @@ -83,30 +81,30 @@ and T = Term.fastype_of u fun newshape (i,terms) = Data.mk_sum T (Data.mk_coeff(i,u)::terms) val reshape = (*Move i*u to the front and put j*u into standard form - i + #m + j + k == #m + i + (j + k) *) - if n1=0 orelse n2=0 then (*trivial, so do nothing*) - raise TERM("cancel_numerals", []) - else Data.prove_conv [Data.norm_tac ss] thy hyps xs - (t', - Data.mk_bal (newshape(n1,terms1'), - newshape(n2,terms2'))) + i + #m + j + k == #m + i + (j + k) *) + if n1=0 orelse n2=0 then (*trivial, so do nothing*) + raise TERM("cancel_numerals", []) + else Data.prove_conv [Data.norm_tac ss] thy hyps xs + (t', + Data.mk_bal (newshape(n1,terms1'), + newshape(n2,terms2'))) in Option.map (Data.simplify_meta_eq ss) - (if n2<=n1 then - Data.prove_conv - [Data.trans_tac ss reshape, rtac Data.bal_add1 1, - Data.numeral_simp_tac ss] thy hyps xs - (t', Data.mk_bal (newshape(n1-n2,terms1'), - Data.mk_sum T terms2')) - else - Data.prove_conv - [Data.trans_tac ss reshape, rtac Data.bal_add2 1, - Data.numeral_simp_tac ss] thy hyps xs - (t', Data.mk_bal (Data.mk_sum T terms1', - newshape(n2-n1,terms2')))) + (if n2<=n1 then + Data.prove_conv + [Data.trans_tac ss reshape, rtac Data.bal_add1 1, + Data.numeral_simp_tac ss] thy hyps xs + (t', Data.mk_bal (newshape(n1-n2,terms1'), + Data.mk_sum T terms2')) + else + Data.prove_conv + [Data.trans_tac ss reshape, rtac Data.bal_add2 1, + Data.numeral_simp_tac ss] thy hyps xs + (t', Data.mk_bal (Data.mk_sum T terms1', + newshape(n2-n1,terms2')))) end handle TERM _ => NONE | TYPE _ => NONE; (*Typically (if thy doesn't include Numeral) - Undeclared type constructor "Numeral.bin"*) + Undeclared type constructor "Numeral.bin"*) end; diff -r 819bc7f22423 -r 430edc6b7826 src/Provers/Arith/extract_common_term.ML --- a/src/Provers/Arith/extract_common_term.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Provers/Arith/extract_common_term.ML Thu Sep 01 22:15:10 2005 +0200 @@ -37,12 +37,9 @@ = struct -(*Store the term t in the table*) -fun update_by_coeff t tab = Termtab.update ((t, ()), tab); - (*a left-to-right scan of terms1, seeking a term u that is also in terms2*) fun find_common (terms1,terms2) = - let val tab2 = fold update_by_coeff terms2 Termtab.empty + let val tab2 = fold (Termtab.curried_update o rpair ()) terms2 Termtab.empty fun seek [] = raise TERM("find_common", []) | seek (u::terms) = if Termtab.defined tab2 u then u diff -r 819bc7f22423 -r 430edc6b7826 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Sep 01 22:15:10 2005 +0200 @@ -301,8 +301,7 @@ in ExtractionData.put {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types, - realizers = foldr Symtab.update_multi - realizers (map (prep_rlz thy) (rev rs)), + realizers = fold (Symtab.curried_update_multi o prep_rlz thy) rs realizers, defs = defs, expand = expand, prep = prep} thy end @@ -565,7 +564,7 @@ else fst (extr d defs vs ts Ts hs prf0) in if T = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0) - else case Symtab.lookup (realizers, name) of + else case Symtab.curried_lookup realizers name of NONE => (case find vs' (find' name defs') of NONE => let @@ -601,7 +600,7 @@ in if etype_of thy' vs' [] prop = nullT andalso realizes_null vs' prop aconv prop then (defs, prf0) - else case find vs' (Symtab.lookup_multi (realizers, s)) of + else case find vs' (Symtab.curried_lookup_multi realizers s) of SOME (_, prf) => (defs, prf_subst_TVars tye' prf) | NONE => error ("corr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm @@ -649,7 +648,7 @@ val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye in - case Symtab.lookup (realizers, s) of + case Symtab.curried_lookup realizers s of NONE => (case find vs' (find' s defs) of NONE => let @@ -708,7 +707,7 @@ val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye in - case find vs' (Symtab.lookup_multi (realizers, s)) of + case find vs' (Symtab.curried_lookup_multi realizers s) of SOME (t, _) => (defs, subst_TVars tye' t) | NONE => error ("extr: no realizer for instance of axiom " ^ quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm diff -r 819bc7f22423 -r 430edc6b7826 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Pure/Proof/proof_syntax.ML Thu Sep 01 22:15:10 2005 +0200 @@ -97,10 +97,10 @@ val thms' = map (apsnd Thm.full_prop_of) (PureThy.all_thms_of thy); val tab = Symtab.foldl (fn (tab, (key, ps)) => - let val prop = getOpt (assoc_string (thms', key), Bound 0) + let val prop = if_none (AList.lookup (op =) thms' key) (Bound 0) in fst (foldr (fn ((prop', prf), x as (tab, i)) => if prop <> prop' then - (Symtab.update ((key ^ "_" ^ string_of_int i, prf), tab), i+1) + (Symtab.curried_update (key ^ "_" ^ string_of_int i, prf) tab, i+1) else x) (tab, 1) ps) end) (Symtab.empty, thms); @@ -110,8 +110,8 @@ | rename (prf % t) = rename prf % t | rename (prf' as PThm ((s, tags), prf, prop, Ts)) = let - val prop' = getOpt (assoc_string (thms', s), Bound 0); - val ps = map fst (valOf (Symtab.lookup (thms, s))) \ prop' + val prop' = if_none (AList.lookup (op =) thms' s) (Bound 0); + val ps = map fst (the (Symtab.curried_lookup thms s)) \ prop' in if prop = prop' then prf' else PThm ((s ^ "_" ^ string_of_int (length ps - find_index_eq prop ps), tags), prf, prop, Ts) @@ -138,15 +138,15 @@ "axm" :: xs => let val name = NameSpace.pack xs; - val prop = (case assoc_string (axms, name) of + val prop = (case AList.lookup (op =) axms name of SOME prop => prop | NONE => error ("Unknown axiom " ^ quote name)) in PAxm (name, prop, NONE) end | "thm" :: xs => let val name = NameSpace.pack xs; - in (case assoc_string (thms, name) of + in (case AList.lookup (op =) thms name of SOME thm => fst (strip_combt (Thm.proof_of thm)) - | NONE => (case Symtab.lookup (tab, name) of + | NONE => (case Symtab.curried_lookup tab name of SOME prf => prf | NONE => error ("Unknown theorem " ^ quote name))) end diff -r 819bc7f22423 -r 430edc6b7826 src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Pure/Proof/proofchecker.ML Thu Sep 01 22:15:10 2005 +0200 @@ -19,9 +19,9 @@ (***** construct a theorem out of a proof term *****) fun lookup_thm thy = - let val tab = fold_rev (curry Symtab.update) (PureThy.all_thms_of thy) Symtab.empty + let val tab = fold_rev Symtab.curried_update (PureThy.all_thms_of thy) Symtab.empty in - (fn s => case Symtab.lookup (tab, s) of + (fn s => case Symtab.curried_lookup tab s of NONE => error ("Unknown theorem " ^ quote s) | SOME thm => thm) end; diff -r 819bc7f22423 -r 430edc6b7826 src/Pure/Tools/compute.ML --- a/src/Pure/Tools/compute.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Pure/Tools/compute.ML Thu Sep 01 22:15:10 2005 +0200 @@ -44,13 +44,13 @@ val remove_types = let fun remove_types_var table invtable ccount vcount ldepth t = - (case Termtab.lookup (table, t) of + (case Termtab.curried_lookup table t of NONE => let val a = AbstractMachine.Var vcount in - (Termtab.update ((t, a), table), - AMTermTab.update ((a, t), invtable), + (Termtab.curried_update (t, a) table, + AMTermTab.curried_update (a, t) invtable, ccount, inc vcount, AbstractMachine.Var (add vcount ldepth)) @@ -60,13 +60,13 @@ | SOME _ => sys_error "remove_types_var: lookup should be a var") fun remove_types_const table invtable ccount vcount ldepth t = - (case Termtab.lookup (table, t) of + (case Termtab.curried_lookup table t of NONE => let val a = AbstractMachine.Const ccount in - (Termtab.update ((t, a), table), - AMTermTab.update ((a, t), invtable), + (Termtab.curried_update (t, a) table, + AMTermTab.curried_update (a, t) invtable, inc ccount, vcount, a) @@ -114,12 +114,12 @@ let fun infer_types invtable ldepth bounds ty (AbstractMachine.Var v) = if v < ldepth then (Bound v, List.nth (bounds, v)) else - (case AMTermTab.lookup (invtable, AbstractMachine.Var (v-ldepth)) of + (case AMTermTab.curried_lookup invtable (AbstractMachine.Var (v-ldepth)) of SOME (t as Var (_, ty)) => (t, ty) | SOME (t as Free (_, ty)) => (t, ty) | _ => sys_error "infer_types: lookup should deliver Var or Free") | infer_types invtable ldepth _ ty (c as AbstractMachine.Const _) = - (case AMTermTab.lookup (invtable, c) of + (case AMTermTab.curried_lookup invtable c of SOME (c as Const (_, ty)) => (c, ty) | _ => sys_error "infer_types: lookup should deliver Const") | infer_types invtable ldepth bounds (n,ty) (AbstractMachine.App (a, b)) = @@ -176,10 +176,10 @@ fun make_pattern table invtable n vars (var as AbstractMachine.Var v) = let - val var' = valOf (AMTermTab.lookup (invtable, var)) + val var' = valOf (AMTermTab.curried_lookup invtable var) val table = Termtab.delete var' table val invtable = AMTermTab.delete var invtable - val vars = Inttab.update_new ((v, n), vars) handle Inttab.DUP _ => + val vars = Inttab.curried_update_new (v, n) vars handle Inttab.DUP _ => raise (Make "no duplicate variable in pattern allowed") in (table, invtable, n+1, vars, AbstractMachine.PVar) @@ -217,7 +217,7 @@ fun rename ldepth vars (var as AbstractMachine.Var v) = if v < ldepth then var - else (case Inttab.lookup (vars, v-ldepth) of + else (case Inttab.curried_lookup vars (v - ldepth) of NONE => raise (Make "new variable on right hand side") | SOME n => AbstractMachine.Var ((vcount-n-1)+ldepth)) | rename ldepth vars (c as AbstractMachine.Const _) = c @@ -231,14 +231,12 @@ end val (table, invtable, ccount, rules) = - List.foldl (fn (th, (table, invtable, ccount, rules)) => - let - val (table, invtable, ccount, rule) = - thm2rule table invtable ccount th - in - (table, invtable, ccount, rule::rules) - end) - (Termtab.empty, AMTermTab.empty, 0, []) (List.rev ths) + fold_rev (fn th => fn (table, invtable, ccount, rules) => + let + val (table, invtable, ccount, rule) = + thm2rule table invtable ccount th + in (table, invtable, ccount, rule::rules) end) + ths (Termtab.empty, AMTermTab.empty, 0, []) val prog = AbstractMachine.compile rules diff -r 819bc7f22423 -r 430edc6b7826 src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/Pure/defs.ML Thu Sep 01 22:15:10 2005 +0200 @@ -46,13 +46,13 @@ typ (* type of the constant in this particular definition *) * (edgelabel list) Symtab.table (* The edges, grouped by nodes. *) -fun getnode graph noderef = the (Symtab.lookup (graph, noderef)) +fun getnode graph = the o Symtab.curried_lookup graph fun get_nodedefs (Node (_, defs, _, _, _)) = defs -fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.lookup (defs, defname) -fun get_defnode' graph noderef defname = - Symtab.lookup (get_nodedefs (the (Symtab.lookup (graph, noderef))), defname) +fun get_defnode (Node (_, defs, _, _, _)) defname = Symtab.curried_lookup defs defname +fun get_defnode' graph noderef = + Symtab.curried_lookup (get_nodedefs (the (Symtab.curried_lookup graph noderef))) -fun table_size table = Symtab.foldl (fn (x, _) => x+1) (0, table) +fun table_size table = Symtab.fold (K (fn x => x + 1)) table 0; datatype graphaction = Declare of string * typ @@ -89,14 +89,14 @@ fun rename ty1 ty2 = Logic.incr_tvar ((maxidx_of_typ ty1)+1) ty2; fun subst_incr_tvar inc t = - if (inc > 0) then + if inc > 0 then let val tv = typ_tvars t val t' = Logic.incr_tvar inc t - fun update_subst (((n,i), _), s) = - Vartab.update (((n, i), ([], TVar ((n, i+inc), []))), s) + fun update_subst ((n, i), _) = + Vartab.curried_update ((n, i), ([], TVar ((n, i + inc), []))); in - (t',List.foldl update_subst Vartab.empty tv) + (t', fold update_subst tv Vartab.empty) end else (t, Vartab.empty) @@ -157,9 +157,9 @@ ((tab,max), []) ts fun idx (tab,max) (TVar ((a,i),_)) = - (case Inttab.lookup (tab, i) of + (case Inttab.curried_lookup tab i of SOME j => ((tab, max), TVar ((a,j),[])) - | NONE => ((Inttab.update ((i, max), tab), max+1), TVar ((a,max),[]))) + | NONE => ((Inttab.curried_update (i, max) tab, max + 1), TVar ((a,max),[]))) | idx (tab,max) (Type (t, ts)) = let val ((tab, max), ts) = idxlist idx I fst (tab, max) ts @@ -207,10 +207,10 @@ fun declare' (g as (cost, axmap, actions, graph)) (cty as (name, ty)) = (cost, axmap, (Declare cty)::actions, - Symtab.update_new ((name, Node (ty, Symtab.empty, Symtab.empty, [], Open)), graph)) + Symtab.curried_update_new (name, Node (ty, Symtab.empty, Symtab.empty, [], Open)) graph) handle Symtab.DUP _ => let - val (Node (gty, _, _, _, _)) = the (Symtab.lookup(graph, name)) + val (Node (gty, _, _, _, _)) = the (Symtab.curried_lookup graph name) in if is_instance_r ty gty andalso is_instance_r gty ty then g @@ -227,13 +227,13 @@ val _ = axcounter := c+1 val axname' = axname^"_"^(IntInf.toString c) in - (Symtab.update ((axname', axname), axmap), axname') + (Symtab.curried_update (axname', axname) axmap, axname') end fun translate_ex axmap x = let fun translate (ty, nodename, axname) = - (ty, nodename, the (Symtab.lookup (axmap, axname))) + (ty, nodename, the (Symtab.curried_lookup axmap axname)) in case x of INFINITE_CHAIN chain => raise (INFINITE_CHAIN (map translate chain)) @@ -243,7 +243,7 @@ fun define' (cost, axmap, actions, graph) (mainref, ty) axname orig_axname body = let - val mainnode = (case Symtab.lookup (graph, mainref) of + val mainnode = (case Symtab.curried_lookup graph mainref of NONE => def_err ("constant "^mainref^" is not declared") | SOME n => n) val (Node (gty, defs, backs, finals, _)) = mainnode @@ -273,17 +273,16 @@ let val links = map normalize_edge_idx links in - Symtab.update ((nodename, - case Symtab.lookup (edges, nodename) of + Symtab.curried_update (nodename, + case Symtab.curried_lookup edges nodename of NONE => links - | SOME links' => merge_edges links' links), - edges) + | SOME links' => merge_edges links' links) edges end) fun make_edges ((bodyn, bodyty), edges) = let val bnode = - (case Symtab.lookup (graph, bodyn) of + (case Symtab.curried_lookup graph bodyn of NONE => def_err "body of constant definition references undeclared constant" | SOME x => x) val (Node (general_btyp, bdefs, bbacks, bfinals, closed)) = bnode @@ -346,13 +345,13 @@ sys_error ("install_backrefs: closed node cannot be updated") else () val defnames = - (case Symtab.lookup (backs, mainref) of + (case Symtab.curried_lookup backs mainref of NONE => Symtab.empty | SOME s => s) - val defnames' = Symtab.update_new ((axname, ()), defnames) - val backs' = Symtab.update ((mainref,defnames'), backs) + val defnames' = Symtab.curried_update_new (axname, ()) defnames + val backs' = Symtab.curried_update (mainref, defnames') backs in - Symtab.update ((noderef, Node (ty, defs, backs', finals, closed)), graph) + Symtab.curried_update (noderef, Node (ty, defs, backs', finals, closed)) graph end else graph @@ -365,8 +364,8 @@ else if closed = Open andalso is_instance_r gty ty then Closed else closed val thisDefnode = Defnode (ty, edges) - val graph = Symtab.update ((mainref, Node (gty, Symtab.update_new - ((axname, thisDefnode), defs), backs, finals, closed)), graph) + val graph = Symtab.curried_update (mainref, Node (gty, Symtab.curried_update_new + (axname, thisDefnode) defs, backs, finals, closed)) graph (* Now we have to check all backreferences to this node and inform them about the new defnode. In this section we also check for circularity. *) @@ -378,8 +377,8 @@ getnode graph noderef val _ = if closed = Final then sys_error "update_defs: closed node" else () val (Defnode (def_ty, defnode_edges)) = - the (Symtab.lookup (nodedefs, defname)) - val edges = the (Symtab.lookup (defnode_edges, mainref)) + the (Symtab.curried_lookup nodedefs defname) + val edges = the (Symtab.curried_lookup defnode_edges mainref) val refclosed = ref false (* the type of thisDefnode is ty *) @@ -417,7 +416,7 @@ val defnames' = if edges' = [] then defnames else - Symtab.update ((defname, ()), defnames) + Symtab.curried_update (defname, ()) defnames in if changed then let @@ -425,16 +424,15 @@ if edges' = [] then Symtab.delete mainref defnode_edges else - Symtab.update ((mainref, edges'), defnode_edges) + Symtab.curried_update (mainref, edges') defnode_edges val defnode' = Defnode (def_ty, defnode_edges') - val nodedefs' = Symtab.update ((defname, defnode'), nodedefs) + val nodedefs' = Symtab.curried_update (defname, defnode') nodedefs val closed = if closed = Closed andalso Symtab.is_empty defnode_edges' andalso no_forwards nodedefs' then Final else closed val graph' = - Symtab.update - ((noderef, - Node (nodety, nodedefs', nodebacks, nodefinals, closed)),graph) + Symtab.curried_update + (noderef, Node (nodety, nodedefs', nodebacks, nodefinals, closed)) graph in (defnames', graph') end @@ -449,7 +447,7 @@ (backs, graph') else let - val backs' = Symtab.update_new ((noderef, defnames'), backs) + val backs' = Symtab.curried_update_new (noderef, defnames') backs in (backs', graph') end @@ -460,7 +458,7 @@ (* If a Circular exception is thrown then we never reach this point. *) val (Node (gty, defs, _, finals, closed)) = getnode graph mainref val closed = if closed = Closed andalso no_forwards defs then Final else closed - val graph = Symtab.update ((mainref, Node (gty, defs, backs, finals, closed)), graph) + val graph = Symtab.curried_update (mainref, Node (gty, defs, backs, finals, closed)) graph val actions' = (Define (mainref, ty, axname, orig_axname, body))::actions in (cost+3, axmap, actions', graph) @@ -484,7 +482,7 @@ end fun finalize' (cost, axmap, history, graph) (noderef, ty) = - case Symtab.lookup (graph, noderef) of + case Symtab.curried_lookup graph noderef of NONE => def_err ("cannot finalize constant "^noderef^"; it is not declared") | SOME (Node (nodety, defs, backs, finals, closed)) => let @@ -521,8 +519,7 @@ val closed = if closed = Open andalso is_instance_r nodety ty then Closed else closed - val graph = Symtab.update ((noderef, Node(nodety, defs, backs, finals, closed)), - graph) + val graph = Symtab.curried_update (noderef, Node (nodety, defs, backs, finals, closed)) graph fun update_backref ((graph, backs), (backrefname, backdefnames)) = let @@ -535,7 +532,7 @@ the (get_defnode backnode backdefname) val (defnames', all_edges') = - case Symtab.lookup (all_edges, noderef) of + case Symtab.curried_lookup all_edges noderef of NONE => sys_error "finalize: corrupt backref" | SOME edges => let @@ -545,11 +542,11 @@ if edges' = [] then (defnames, Symtab.delete noderef all_edges) else - (Symtab.update ((backdefname, ()), defnames), - Symtab.update ((noderef, edges'), all_edges)) + (Symtab.curried_update (backdefname, ()) defnames, + Symtab.curried_update (noderef, edges') all_edges) end val defnode' = Defnode (def_ty, all_edges') - val backdefs' = Symtab.update ((backdefname, defnode'), backdefs) + val backdefs' = Symtab.curried_update (backdefname, defnode') backdefs val backclosed' = if backclosed = Closed andalso Symtab.is_empty all_edges' andalso no_forwards backdefs' @@ -557,20 +554,20 @@ val backnode' = Node (backty, backdefs', backbacks, backfinals, backclosed') in - (Symtab.update ((backrefname, backnode'), graph), defnames') + (Symtab.curried_update (backrefname, backnode') graph, defnames') end val (graph', defnames') = Symtab.foldl update_backdef ((graph, Symtab.empty), backdefnames) in (graph', if Symtab.is_empty defnames' then backs - else Symtab.update ((backrefname, defnames'), backs)) + else Symtab.curried_update (backrefname, defnames') backs) end val (graph', backs') = Symtab.foldl update_backref ((graph, Symtab.empty), backs) val Node ( _, defs, _, _, closed) = getnode graph' noderef val closed = if closed = Closed andalso no_forwards defs then Final else closed - val graph' = Symtab.update ((noderef, Node (nodety, defs, backs', - finals, closed)), graph') + val graph' = Symtab.curried_update (noderef, Node (nodety, defs, backs', + finals, closed)) graph' val history' = (Finalize (noderef, ty)) :: history in (cost+1, axmap, history', graph') @@ -580,14 +577,14 @@ fun finalize'' thy g (noderef, ty) = finalize' g (noderef, checkT thy ty) fun update_axname ax orig_ax (cost, axmap, history, graph) = - (cost, Symtab.update ((ax, orig_ax), axmap), history, graph) + (cost, Symtab.curried_update (ax, orig_ax) axmap, history, graph) fun merge' (Declare cty, g) = declare' g cty | merge' (Define (name, ty, axname, orig_axname, body), g as (cost, axmap, history, graph)) = - (case Symtab.lookup (graph, name) of + (case Symtab.curried_lookup graph name of NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body | SOME (Node (_, defs, _, _, _)) => - (case Symtab.lookup (defs, axname) of + (case Symtab.curried_lookup defs axname of NONE => define' (update_axname axname orig_axname g) (name, ty) axname orig_axname body | SOME _ => g)) | merge' (Finalize finals, g) = finalize' g finals @@ -601,14 +598,14 @@ fun finals (_, _, history, graph) = Symtab.foldl (fn (finals, (name, Node(_, _, _, ftys, _))) => - Symtab.update_new ((name, ftys), finals)) + Symtab.curried_update_new (name, ftys) finals) (Symtab.empty, graph) fun overloading_info (_, axmap, _, graph) c = let - fun translate (ax, Defnode (ty, _)) = (the (Symtab.lookup (axmap, ax)), ty) + fun translate (ax, Defnode (ty, _)) = (the (Symtab.curried_lookup axmap ax), ty) in - case Symtab.lookup (graph, c) of + case Symtab.curried_lookup graph c of NONE => NONE | SOME (Node (ty, defnodes, _, _, state)) => SOME (ty, map translate (Symtab.dest defnodes), state) @@ -621,7 +618,7 @@ | monomorphicT _ = false fun monomorphic (_, _, _, graph) c = - (case Symtab.lookup (graph, c) of + (case Symtab.curried_lookup graph c of NONE => true | SOME (Node (ty, defnodes, _, _, _)) => Symtab.min_key defnodes = Symtab.max_key defnodes andalso diff -r 819bc7f22423 -r 430edc6b7826 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Thu Sep 01 18:48:54 2005 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Thu Sep 01 22:15:10 2005 +0200 @@ -70,7 +70,7 @@ struct fun datatype_info thy name = - (case Symtab.lookup (DatatypesData.get thy, name) of + (case Symtab.curried_lookup (DatatypesData.get thy) name of SOME info => info | NONE => error ("Unknown datatype " ^ quote name)); @@ -163,14 +163,12 @@ val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors in - thy |> Theory.add_path (Sign.base_name big_rec_name) - |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]) - |> DatatypesData.put - (Symtab.update - ((big_rec_name, dt_info), DatatypesData.get thy)) - |> ConstructorsData.put - (foldr Symtab.update (ConstructorsData.get thy) con_pairs) - |> Theory.parent_path + thy + |> Theory.add_path (Sign.base_name big_rec_name) + |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]) + |> DatatypesData.put (Symtab.curried_update (big_rec_name, dt_info) (DatatypesData.get thy)) + |> ConstructorsData.put (fold_rev Symtab.curried_update con_pairs (ConstructorsData.get thy)) + |> Theory.parent_path end; fun rep_datatype raw_elim raw_induct raw_case_eqns raw_recursor_eqns thy =