# HG changeset patch # User wenzelm # Date 1230816219 -3600 # Node ID 253bcf2a585497f80cb8f512d53f693dec410ccc # Parent 5b0bfd63b5da3f8e01d03ebc0d0ea0ad1bb707c3 avoid polymorphic equality; diff -r 5b0bfd63b5da -r 253bcf2a5854 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/HOL/Tools/inductive_set_package.ML Thu Jan 01 14:23:39 2009 +0100 @@ -169,7 +169,7 @@ ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1, set_arities = set_arities1, pred_arities = pred_arities1}, {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2, - set_arities = set_arities2, pred_arities = pred_arities2}) = + set_arities = set_arities2, pred_arities = pred_arities2}) : T = {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2), to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2), set_arities = Symtab.merge_list op = (set_arities1, set_arities2), diff -r 5b0bfd63b5da -r 253bcf2a5854 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/HOL/Tools/lin_arith.ML Thu Jan 01 14:23:39 2009 +0100 @@ -1,6 +1,5 @@ (* Title: HOL/Tools/lin_arith.ML - ID: $Id$ - Author: Tjark Weber and Tobias Nipkow + Author: Tjark Weber and Tobias Nipkow, TU Muenchen HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML). *) @@ -99,8 +98,9 @@ tactics: arith_tactic list}; val empty = {splits = [], inj_consts = [], discrete = [], tactics = []}; val extend = I; - fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, - {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = + fun merge _ + ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, + {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T = {splits = Library.merge Thm.eq_thm_prop (splits1, splits2), inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), discrete = Library.merge (op =) (discrete1, discrete2), diff -r 5b0bfd63b5da -r 253bcf2a5854 src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/HOL/Tools/refute.ML Thu Jan 01 14:23:39 2009 +0100 @@ -389,11 +389,6 @@ (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL *) (* ------------------------------------------------------------------------- *) - (* (''a * 'b) list -> ''a -> 'b *) - - fun lookup xs key = - Option.valOf (AList.lookup (op =) xs key); - (* ------------------------------------------------------------------------- *) (* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type *) (* ('Term.typ'), given type parameters for the data type's type *) @@ -405,12 +400,12 @@ fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) = (* replace a 'DtTFree' variable by the associated type *) - lookup typ_assoc (DatatypeAux.DtTFree a) + the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a)) | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) = Type (s, map (typ_of_dtyp descr typ_assoc) ds) | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) = let - val (s, ds, _) = lookup descr i + val (s, ds, _) = the (AList.lookup (op =) descr i) in Type (s, map (typ_of_dtyp descr typ_assoc) ds) end; @@ -850,14 +845,14 @@ | Const ("The", T) => let val ax = specialize_type thy ("The", T) - (lookup axioms "HOL.the_eq_trivial") + (the (AList.lookup (op =) axioms "HOL.the_eq_trivial")) in collect_this_axiom ("HOL.the_eq_trivial", ax) axs end | Const ("Hilbert_Choice.Eps", T) => let val ax = specialize_type thy ("Hilbert_Choice.Eps", T) - (lookup axioms "Hilbert_Choice.someI") + (the (AList.lookup (op =) axioms "Hilbert_Choice.someI")) in collect_this_axiom ("Hilbert_Choice.someI", ax) axs end @@ -955,7 +950,7 @@ let val index = #index info val descr = #descr info - val (_, typs, _) = lookup descr index + val (_, typs, _) = the (AList.lookup (op =) descr index) val typ_assoc = typs ~~ Ts (* sanity check: every element in 'dtyps' must be a *) (* 'DtTFree' *) @@ -981,7 +976,7 @@ acc (* prevent infinite recursion *) else let - val (_, dtyps, dconstrs) = lookup descr i + val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i) (* if the current type is a recursive IDT (i.e. a depth *) (* is required), add it to 'acc' *) val acc_dT = if Library.exists (fn (_, ds) => @@ -1165,7 +1160,7 @@ let val index = #index info val descr = #descr info - val (_, _, constrs) = lookup descr index + val (_, _, constrs) = the (AList.lookup (op =) descr index) in (* recursive datatype? *) Library.exists (fn (_, ds) => @@ -1657,7 +1652,7 @@ fun interpret_groundtype () = let (* the model must specify a size for ground types *) - val size = (if T = Term.propT then 2 else lookup typs T) + val size = if T = Term.propT then 2 else the (AList.lookup (op =) typs T) val next = next_idx+size (* check if 'maxvars' is large enough *) val _ = (if next-1>maxvars andalso maxvars>0 then @@ -2020,7 +2015,7 @@ let val index = #index info val descr = #descr info - val (_, dtyps, constrs) = lookup descr index + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) val typ_assoc = dtyps ~~ Ts (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = if Library.exists (fn d => @@ -2144,7 +2139,7 @@ let val index = #index info val descr = #descr info - val (_, dtyps, constrs) = lookup descr index + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) val typ_assoc = dtyps ~~ Ts (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = if Library.exists (fn d => @@ -2204,7 +2199,7 @@ let val index = #index info val descr = #descr info - val (_, dtyps, constrs) = lookup descr index + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) val typ_assoc = dtyps ~~ Ts' (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = if Library.exists (fn d => @@ -2400,7 +2395,7 @@ (* the index of some mutually recursive IDT *) val index = #index info val descr = #descr info - val (_, dtyps, _) = lookup descr index + val (_, dtyps, _) = the (AList.lookup (op =) descr index) (* sanity check: we assume that the order of constructors *) (* in 'descr' is the same as the order of *) (* corresponding parameters, otherwise the *) @@ -2459,7 +2454,7 @@ end | DatatypeAux.DtRec i => let - val (_, ds, _) = lookup descr i + val (_, ds, _) = the (AList.lookup (op =) descr i) val (_, Ts) = dest_Type T in rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs) @@ -2473,10 +2468,10 @@ raise REFUTE ("IDT_recursion_interpreter", "different type associations for the same dtyp")) (* (DatatypeAux.dtyp * Term.typ) list *) - val typ_assoc = List.filter + val typ_assoc = filter (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false) (rec_typ_assoc [] - (#2 (lookup descr idt_index) ~~ (snd o dest_Type) IDT)) + (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT)) (* sanity check: typ_assoc must associate types to the *) (* elements of 'dtyps' (and only to those) *) val _ = if not (Library.eq_set (dtyps, map fst typ_assoc)) @@ -2600,7 +2595,7 @@ SOME args => (n, args) | NONE => get_cargs_rec (n+1, xs)) in - get_cargs_rec (0, lookup mc_intrs idx) + get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx)) end (* computes one entry in 'REC_OPERATORS', and recursively *) (* all entries needed for it, where 'idx' gives the *) @@ -2608,7 +2603,7 @@ (* int -> int -> interpretation *) fun compute_array_entry idx elem = let - val arr = lookup REC_OPERATORS idx + val arr = the (AList.lookup (op =) REC_OPERATORS idx) val (flag, intr) = Array.sub (arr, elem) in if flag then @@ -2622,7 +2617,7 @@ val (c, args) = get_cargs idx elem (* find the indices of the constructor's /recursive/ *) (* arguments *) - val (_, _, constrs) = lookup descr idx + val (_, _, constrs) = the (AList.lookup (op =) descr idx) val (_, dtyps) = List.nth (constrs, c) val rec_dtyps_args = List.filter (DatatypeAux.is_rec_type o fst) (dtyps ~~ args) @@ -2674,7 +2669,7 @@ result end end - val idt_size = Array.length (lookup REC_OPERATORS idt_index) + val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index)) (* sanity check: the size of 'IDT' should be 'idt_size' *) val _ = if idt_size <> size_of_type thy (typs, []) IDT then raise REFUTE ("IDT_recursion_interpreter", @@ -2973,8 +2968,8 @@ (* nat -> nat -> interpretation *) fun append m n = let - val (len_m, off_m) = lookup lenoff_lists m - val (len_n, off_n) = lookup lenoff_lists n + val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m) + val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n) val len_elem = len_m + len_n val off_elem = off_m * power (size_elem, len_n) + off_n in @@ -3262,7 +3257,7 @@ val (typs, _) = model val index = #index info val descr = #descr info - val (_, dtyps, constrs) = lookup descr index + val (_, dtyps, constrs) = the (AList.lookup (op =) descr index) val typ_assoc = dtyps ~~ Ts (* sanity check: every element in 'dtyps' must be a 'DtTFree' *) val _ = if Library.exists (fn d => diff -r 5b0bfd63b5da -r 253bcf2a5854 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/Pure/Isar/code_unit.ML Thu Jan 01 14:23:39 2009 +0100 @@ -229,7 +229,7 @@ val empty = ([], []); val copy = I; val extend = I; - fun merge _ ((alias1, classes1), (alias2, classes2)) = + fun merge _ ((alias1, classes1), (alias2, classes2)) : T = (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), Library.merge (op =) (classes1, classes2)); ); diff -r 5b0bfd63b5da -r 253bcf2a5854 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/Pure/Isar/expression.ML Thu Jan 01 14:23:39 2009 +0100 @@ -74,7 +74,7 @@ end; fun match_bind (n, b) = (n = Binding.base_name b); - fun parm_eq ((b1, mx1), (b2, mx2)) = + fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) = (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *) (Binding.base_name b1 = Binding.base_name b2) andalso (if mx1 = mx2 then true diff -r 5b0bfd63b5da -r 253bcf2a5854 src/Pure/Isar/new_locale.ML --- a/src/Pure/Isar/new_locale.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/Pure/Isar/new_locale.ML Thu Jan 01 14:23:39 2009 +0100 @@ -115,17 +115,17 @@ val extend = I; fun join_locales _ - (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies}, - Loc {decls = (decls1', decls2'), notes = notes', - dependencies = dependencies', ...}) = - let fun s_merge x = merge (eq_snd (op =)) x in - Loc {parameters = parameters, - spec = spec, - decls = (s_merge (decls1, decls1'), s_merge (decls2, decls2')), - notes = s_merge (notes, notes'), - dependencies = s_merge (dependencies, dependencies') - } - end; + (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies}, + Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) = + Loc { + parameters = parameters, + spec = spec, + decls = + (merge (eq_snd op =) (decls1, decls1'), + merge (eq_snd op =) (decls2, decls2')), + notes = merge (eq_snd op =) (notes, notes'), + dependencies = merge (eq_snd op =) (dependencies, dependencies')}; + fun merge _ = NameSpace.join_tables join_locales; ); @@ -197,7 +197,7 @@ val empty = ([] : identifiers); -fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts); +fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts); local @@ -221,7 +221,7 @@ Ready _ => NONE | ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy)) ))); - + fun get_global_idents thy = let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end; val put_global_idents = Context.theory_map o IdentifiersData.put o Ready; @@ -331,7 +331,7 @@ in ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd - end + end | init_local_elem (Defines defs) ctxt = let val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs @@ -376,7 +376,7 @@ in Pretty.big_list "locale elements:" (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy)) - (empty, []) |> snd |> rev |> + (empty, []) |> snd |> rev |> map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln end @@ -393,7 +393,7 @@ (* registrations, in reverse order of declaration *) val empty = []; val extend = I; - fun merge _ = Library.merge (eq_snd (op =)); + fun merge _ data : T = Library.merge (eq_snd op =) data; (* FIXME consolidate with dependencies, consider one data slot only *) ); diff -r 5b0bfd63b5da -r 253bcf2a5854 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/Pure/thm.ML Thu Jan 01 14:23:39 2009 +0100 @@ -1695,7 +1695,7 @@ val empty = NameSpace.empty_table; val copy = I; val extend = I; - fun merge _ oracles = NameSpace.merge_tables (op =) oracles + fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles handle Symtab.DUP dup => err_dup_ora dup; ); diff -r 5b0bfd63b5da -r 253bcf2a5854 src/Tools/value.ML --- a/src/Tools/value.ML Thu Jan 01 14:23:39 2009 +0100 +++ b/src/Tools/value.ML Thu Jan 01 14:23:39 2009 +0100 @@ -20,7 +20,7 @@ val empty = []; val copy = I; val extend = I; - fun merge pp = AList.merge (op =) (K true); + fun merge _ data = AList.merge (op =) (K true) data; ) val add_evaluator = Evaluator.map o AList.update (op =);