avoid polymorphic equality;
authorwenzelm
Thu Jan 01 14:23:39 2009 +0100 (2009-01-01)
changeset 29288253bcf2a5854
parent 29287 5b0bfd63b5da
child 29289 f45c9c3b40a3
avoid polymorphic equality;
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/refute.ML
src/Pure/Isar/code_unit.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/new_locale.ML
src/Pure/thm.ML
src/Tools/value.ML
     1.1 --- a/src/HOL/Tools/inductive_set_package.ML	Thu Jan 01 14:23:39 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Thu Jan 01 14:23:39 2009 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4      ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
     1.5        set_arities = set_arities1, pred_arities = pred_arities1},
     1.6       {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
     1.7 -      set_arities = set_arities2, pred_arities = pred_arities2}) =
     1.8 +      set_arities = set_arities2, pred_arities = pred_arities2}) : T =
     1.9      {to_set_simps = Thm.merge_thms (to_set_simps1, to_set_simps2),
    1.10       to_pred_simps = Thm.merge_thms (to_pred_simps1, to_pred_simps2),
    1.11       set_arities = Symtab.merge_list op = (set_arities1, set_arities2),
     2.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Jan 01 14:23:39 2009 +0100
     2.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Jan 01 14:23:39 2009 +0100
     2.3 @@ -1,6 +1,5 @@
     2.4  (*  Title:      HOL/Tools/lin_arith.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tjark Weber and Tobias Nipkow
     2.7 +    Author:     Tjark Weber and Tobias Nipkow, TU Muenchen
     2.8  
     2.9  HOL setup for linear arithmetic (see Provers/Arith/fast_lin_arith.ML).
    2.10  *)
    2.11 @@ -99,8 +98,9 @@
    2.12              tactics: arith_tactic list};
    2.13    val empty = {splits = [], inj_consts = [], discrete = [], tactics = []};
    2.14    val extend = I;
    2.15 -  fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
    2.16 -             {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) =
    2.17 +  fun merge _
    2.18 +   ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
    2.19 +    {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) : T =
    2.20     {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
    2.21      inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
    2.22      discrete = Library.merge (op =) (discrete1, discrete2),
     3.1 --- a/src/HOL/Tools/refute.ML	Thu Jan 01 14:23:39 2009 +0100
     3.2 +++ b/src/HOL/Tools/refute.ML	Thu Jan 01 14:23:39 2009 +0100
     3.3 @@ -389,11 +389,6 @@
     3.4  (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
     3.5  (* ------------------------------------------------------------------------- *)
     3.6  
     3.7 -  (* (''a * 'b) list -> ''a -> 'b *)
     3.8 -
     3.9 -  fun lookup xs key =
    3.10 -    Option.valOf (AList.lookup (op =) xs key);
    3.11 -
    3.12  (* ------------------------------------------------------------------------- *)
    3.13  (* typ_of_dtyp: converts a data type ('DatatypeAux.dtyp') into a type        *)
    3.14  (*              ('Term.typ'), given type parameters for the data type's type *)
    3.15 @@ -405,12 +400,12 @@
    3.16  
    3.17    fun typ_of_dtyp descr typ_assoc (DatatypeAux.DtTFree a) =
    3.18      (* replace a 'DtTFree' variable by the associated type *)
    3.19 -    lookup typ_assoc (DatatypeAux.DtTFree a)
    3.20 +    the (AList.lookup (op =) typ_assoc (DatatypeAux.DtTFree a))
    3.21      | typ_of_dtyp descr typ_assoc (DatatypeAux.DtType (s, ds)) =
    3.22      Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    3.23      | typ_of_dtyp descr typ_assoc (DatatypeAux.DtRec i) =
    3.24      let
    3.25 -      val (s, ds, _) = lookup descr i
    3.26 +      val (s, ds, _) = the (AList.lookup (op =) descr i)
    3.27      in
    3.28        Type (s, map (typ_of_dtyp descr typ_assoc) ds)
    3.29      end;
    3.30 @@ -850,14 +845,14 @@
    3.31        | Const ("The", T)                =>
    3.32          let
    3.33            val ax = specialize_type thy ("The", T)
    3.34 -            (lookup axioms "HOL.the_eq_trivial")
    3.35 +            (the (AList.lookup (op =) axioms "HOL.the_eq_trivial"))
    3.36          in
    3.37            collect_this_axiom ("HOL.the_eq_trivial", ax) axs
    3.38          end
    3.39        | Const ("Hilbert_Choice.Eps", T) =>
    3.40          let
    3.41            val ax = specialize_type thy ("Hilbert_Choice.Eps", T)
    3.42 -            (lookup axioms "Hilbert_Choice.someI")
    3.43 +            (the (AList.lookup (op =) axioms "Hilbert_Choice.someI"))
    3.44          in
    3.45            collect_this_axiom ("Hilbert_Choice.someI", ax) axs
    3.46          end
    3.47 @@ -955,7 +950,7 @@
    3.48            let
    3.49              val index        = #index info
    3.50              val descr        = #descr info
    3.51 -            val (_, typs, _) = lookup descr index
    3.52 +            val (_, typs, _) = the (AList.lookup (op =) descr index)
    3.53              val typ_assoc    = typs ~~ Ts
    3.54              (* sanity check: every element in 'dtyps' must be a *)
    3.55              (* 'DtTFree'                                        *)
    3.56 @@ -981,7 +976,7 @@
    3.57                    acc  (* prevent infinite recursion *)
    3.58                  else
    3.59                    let
    3.60 -                    val (_, dtyps, dconstrs) = lookup descr i
    3.61 +                    val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i)
    3.62                      (* if the current type is a recursive IDT (i.e. a depth *)
    3.63                      (* is required), add it to 'acc'                        *)
    3.64                      val acc_dT = if Library.exists (fn (_, ds) =>
    3.65 @@ -1165,7 +1160,7 @@
    3.66              let
    3.67                val index           = #index info
    3.68                val descr           = #descr info
    3.69 -              val (_, _, constrs) = lookup descr index
    3.70 +              val (_, _, constrs) = the (AList.lookup (op =) descr index)
    3.71              in
    3.72                (* recursive datatype? *)
    3.73                Library.exists (fn (_, ds) =>
    3.74 @@ -1657,7 +1652,7 @@
    3.75        fun interpret_groundtype () =
    3.76        let
    3.77          (* the model must specify a size for ground types *)
    3.78 -        val size = (if T = Term.propT then 2 else lookup typs T)
    3.79 +        val size = if T = Term.propT then 2 else the (AList.lookup (op =) typs T)
    3.80          val next = next_idx+size
    3.81          (* check if 'maxvars' is large enough *)
    3.82          val _    = (if next-1>maxvars andalso maxvars>0 then
    3.83 @@ -2020,7 +2015,7 @@
    3.84              let
    3.85                val index               = #index info
    3.86                val descr               = #descr info
    3.87 -              val (_, dtyps, constrs) = lookup descr index
    3.88 +              val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
    3.89                val typ_assoc           = dtyps ~~ Ts
    3.90                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
    3.91                val _ = if Library.exists (fn d =>
    3.92 @@ -2144,7 +2139,7 @@
    3.93              let
    3.94                val index               = #index info
    3.95                val descr               = #descr info
    3.96 -              val (_, dtyps, constrs) = lookup descr index
    3.97 +              val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
    3.98                val typ_assoc           = dtyps ~~ Ts
    3.99                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   3.100                val _ = if Library.exists (fn d =>
   3.101 @@ -2204,7 +2199,7 @@
   3.102              let
   3.103                val index               = #index info
   3.104                val descr               = #descr info
   3.105 -              val (_, dtyps, constrs) = lookup descr index
   3.106 +              val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
   3.107                val typ_assoc           = dtyps ~~ Ts'
   3.108                (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   3.109                val _ = if Library.exists (fn d =>
   3.110 @@ -2400,7 +2395,7 @@
   3.111                    (* the index of some mutually recursive IDT               *)
   3.112                    val index         = #index info
   3.113                    val descr         = #descr info
   3.114 -                  val (_, dtyps, _) = lookup descr index
   3.115 +                  val (_, dtyps, _) = the (AList.lookup (op =) descr index)
   3.116                    (* sanity check: we assume that the order of constructors *)
   3.117                    (*               in 'descr' is the same as the order of   *)
   3.118                    (*               corresponding parameters, otherwise the  *)
   3.119 @@ -2459,7 +2454,7 @@
   3.120                          end
   3.121                        | DatatypeAux.DtRec i =>
   3.122                          let
   3.123 -                          val (_, ds, _) = lookup descr i
   3.124 +                          val (_, ds, _) = the (AList.lookup (op =) descr i)
   3.125                            val (_, Ts)    = dest_Type T
   3.126                          in
   3.127                            rec_typ_assoc ((d, T)::acc) ((ds ~~ Ts) @ xs)
   3.128 @@ -2473,10 +2468,10 @@
   3.129                          raise REFUTE ("IDT_recursion_interpreter",
   3.130                            "different type associations for the same dtyp"))
   3.131                    (* (DatatypeAux.dtyp * Term.typ) list *)
   3.132 -                  val typ_assoc = List.filter
   3.133 +                  val typ_assoc = filter
   3.134                      (fn (DatatypeAux.DtTFree _, _) => true | (_, _) => false)
   3.135                      (rec_typ_assoc []
   3.136 -                      (#2 (lookup descr idt_index) ~~ (snd o dest_Type) IDT))
   3.137 +                      (#2 (the (AList.lookup (op =) descr idt_index)) ~~ (snd o dest_Type) IDT))
   3.138                    (* sanity check: typ_assoc must associate types to the   *)
   3.139                    (*               elements of 'dtyps' (and only to those) *)
   3.140                    val _ = if not (Library.eq_set (dtyps, map fst typ_assoc))
   3.141 @@ -2600,7 +2595,7 @@
   3.142                            SOME args => (n, args)
   3.143                          | NONE      => get_cargs_rec (n+1, xs))
   3.144                      in
   3.145 -                      get_cargs_rec (0, lookup mc_intrs idx)
   3.146 +                      get_cargs_rec (0, the (AList.lookup (op =) mc_intrs idx))
   3.147                      end
   3.148                    (* computes one entry in 'REC_OPERATORS', and recursively *)
   3.149                    (* all entries needed for it, where 'idx' gives the       *)
   3.150 @@ -2608,7 +2603,7 @@
   3.151                    (* int -> int -> interpretation *)
   3.152                    fun compute_array_entry idx elem =
   3.153                    let
   3.154 -                    val arr          = lookup REC_OPERATORS idx
   3.155 +                    val arr          = the (AList.lookup (op =) REC_OPERATORS idx)
   3.156                      val (flag, intr) = Array.sub (arr, elem)
   3.157                    in
   3.158                      if flag then
   3.159 @@ -2622,7 +2617,7 @@
   3.160                          val (c, args) = get_cargs idx elem
   3.161                          (* find the indices of the constructor's /recursive/ *)
   3.162                          (* arguments                                         *)
   3.163 -                        val (_, _, constrs) = lookup descr idx
   3.164 +                        val (_, _, constrs) = the (AList.lookup (op =) descr idx)
   3.165                          val (_, dtyps)      = List.nth (constrs, c)
   3.166                          val rec_dtyps_args  = List.filter
   3.167                            (DatatypeAux.is_rec_type o fst) (dtyps ~~ args)
   3.168 @@ -2674,7 +2669,7 @@
   3.169                          result
   3.170                        end
   3.171                    end
   3.172 -                  val idt_size = Array.length (lookup REC_OPERATORS idt_index)
   3.173 +                  val idt_size = Array.length (the (AList.lookup (op =) REC_OPERATORS idt_index))
   3.174                    (* sanity check: the size of 'IDT' should be 'idt_size' *)
   3.175                    val _ = if idt_size <> size_of_type thy (typs, []) IDT then
   3.176                          raise REFUTE ("IDT_recursion_interpreter",
   3.177 @@ -2973,8 +2968,8 @@
   3.178          (* nat -> nat -> interpretation *)
   3.179          fun append m n =
   3.180            let
   3.181 -            val (len_m, off_m) = lookup lenoff_lists m
   3.182 -            val (len_n, off_n) = lookup lenoff_lists n
   3.183 +            val (len_m, off_m) = the (AList.lookup (op =) lenoff_lists m)
   3.184 +            val (len_n, off_n) = the (AList.lookup (op =) lenoff_lists n)
   3.185              val len_elem = len_m + len_n
   3.186              val off_elem = off_m * power (size_elem, len_n) + off_n
   3.187            in
   3.188 @@ -3262,7 +3257,7 @@
   3.189            val (typs, _)           = model
   3.190            val index               = #index info
   3.191            val descr               = #descr info
   3.192 -          val (_, dtyps, constrs) = lookup descr index
   3.193 +          val (_, dtyps, constrs) = the (AList.lookup (op =) descr index)
   3.194            val typ_assoc           = dtyps ~~ Ts
   3.195            (* sanity check: every element in 'dtyps' must be a 'DtTFree' *)
   3.196            val _ = if Library.exists (fn d =>
     4.1 --- a/src/Pure/Isar/code_unit.ML	Thu Jan 01 14:23:39 2009 +0100
     4.2 +++ b/src/Pure/Isar/code_unit.ML	Thu Jan 01 14:23:39 2009 +0100
     4.3 @@ -229,7 +229,7 @@
     4.4    val empty = ([], []);
     4.5    val copy = I;
     4.6    val extend = I;
     4.7 -  fun merge _ ((alias1, classes1), (alias2, classes2)) =
     4.8 +  fun merge _ ((alias1, classes1), (alias2, classes2)) : T =
     4.9      (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2),
    4.10        Library.merge (op =) (classes1, classes2));
    4.11  );
     5.1 --- a/src/Pure/Isar/expression.ML	Thu Jan 01 14:23:39 2009 +0100
     5.2 +++ b/src/Pure/Isar/expression.ML	Thu Jan 01 14:23:39 2009 +0100
     5.3 @@ -74,7 +74,7 @@
     5.4        end;
     5.5  
     5.6      fun match_bind (n, b) = (n = Binding.base_name b);
     5.7 -    fun parm_eq ((b1, mx1), (b2, mx2)) =
     5.8 +    fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
     5.9        (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
    5.10        (Binding.base_name b1 = Binding.base_name b2) andalso
    5.11        (if mx1 = mx2 then true
     6.1 --- a/src/Pure/Isar/new_locale.ML	Thu Jan 01 14:23:39 2009 +0100
     6.2 +++ b/src/Pure/Isar/new_locale.ML	Thu Jan 01 14:23:39 2009 +0100
     6.3 @@ -115,17 +115,17 @@
     6.4    val extend = I;
     6.5  
     6.6    fun join_locales _
     6.7 -    (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
     6.8 -      Loc {decls = (decls1', decls2'), notes = notes',
     6.9 -        dependencies = dependencies', ...}) =
    6.10 -        let fun s_merge x = merge (eq_snd (op =)) x in
    6.11 -          Loc {parameters = parameters,
    6.12 -            spec = spec,
    6.13 -            decls = (s_merge (decls1, decls1'), s_merge (decls2, decls2')),
    6.14 -            notes = s_merge (notes, notes'),
    6.15 -            dependencies = s_merge (dependencies, dependencies')
    6.16 -          }          
    6.17 -        end;
    6.18 +   (Loc {parameters, spec, decls = (decls1, decls2), notes, dependencies},
    6.19 +    Loc {decls = (decls1', decls2'), notes = notes', dependencies = dependencies', ...}) =
    6.20 +      Loc {
    6.21 +        parameters = parameters,
    6.22 +        spec = spec,
    6.23 +        decls =
    6.24 +         (merge (eq_snd op =) (decls1, decls1'),
    6.25 +          merge (eq_snd op =) (decls2, decls2')),
    6.26 +        notes = merge (eq_snd op =) (notes, notes'),
    6.27 +        dependencies = merge (eq_snd op =) (dependencies, dependencies')};
    6.28 +
    6.29    fun merge _ = NameSpace.join_tables join_locales;
    6.30  );
    6.31  
    6.32 @@ -197,7 +197,7 @@
    6.33  
    6.34  val empty = ([] : identifiers);
    6.35  
    6.36 -fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    6.37 +fun ident_eq thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    6.38  
    6.39  local
    6.40  
    6.41 @@ -221,7 +221,7 @@
    6.42      Ready _ => NONE |
    6.43      ids => SOME (Context.theory_map (IdentifiersData.put (Ready (finish thy ids))) thy))
    6.44    )));
    6.45 -  
    6.46 +
    6.47  fun get_global_idents thy =
    6.48    let val (Ready ids) = (IdentifiersData.get o Context.Theory) thy in ids end;
    6.49  val put_global_idents = Context.theory_map o IdentifiersData.put o Ready;
    6.50 @@ -331,7 +331,7 @@
    6.51        in
    6.52          ctxt |> fold Variable.auto_fixes (maps (map fst o snd) assms') |>
    6.53            ProofContext.add_assms_i Assumption.assume_export assms' |> snd
    6.54 -     end 
    6.55 +     end
    6.56    | init_local_elem (Defines defs) ctxt =
    6.57        let
    6.58          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs
    6.59 @@ -376,7 +376,7 @@
    6.60    in
    6.61      Pretty.big_list "locale elements:"
    6.62        (activate_all name' thy (cons_elem show_facts) (K (Element.transfer_morphism thy))
    6.63 -        (empty, []) |> snd |> rev |> 
    6.64 +        (empty, []) |> snd |> rev |>
    6.65          map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
    6.66    end
    6.67  
    6.68 @@ -393,7 +393,7 @@
    6.69      (* registrations, in reverse order of declaration *)
    6.70    val empty = [];
    6.71    val extend = I;
    6.72 -  fun merge _ = Library.merge (eq_snd (op =));
    6.73 +  fun merge _ data : T = Library.merge (eq_snd op =) data;
    6.74      (* FIXME consolidate with dependencies, consider one data slot only *)
    6.75  );
    6.76  
     7.1 --- a/src/Pure/thm.ML	Thu Jan 01 14:23:39 2009 +0100
     7.2 +++ b/src/Pure/thm.ML	Thu Jan 01 14:23:39 2009 +0100
     7.3 @@ -1695,7 +1695,7 @@
     7.4    val empty = NameSpace.empty_table;
     7.5    val copy = I;
     7.6    val extend = I;
     7.7 -  fun merge _ oracles = NameSpace.merge_tables (op =) oracles
     7.8 +  fun merge _ oracles : T = NameSpace.merge_tables (op =) oracles
     7.9      handle Symtab.DUP dup => err_dup_ora dup;
    7.10  );
    7.11  
     8.1 --- a/src/Tools/value.ML	Thu Jan 01 14:23:39 2009 +0100
     8.2 +++ b/src/Tools/value.ML	Thu Jan 01 14:23:39 2009 +0100
     8.3 @@ -20,7 +20,7 @@
     8.4    val empty = [];
     8.5    val copy = I;
     8.6    val extend = I;
     8.7 -  fun merge pp = AList.merge (op =) (K true);
     8.8 +  fun merge _ data = AList.merge (op =) (K true) data;
     8.9  )
    8.10  
    8.11  val add_evaluator = Evaluator.map o AList.update (op =);