make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
authorwenzelm
Fri Nov 26 22:29:41 2010 +0100 (2010-11-26)
changeset 40722441260986b63
parent 40721 e5089e903e39
child 40728 aef83e8fa2a4
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
NEWS
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/record.ML
src/Pure/Proof/reconstruct.ML
src/Pure/consts.ML
src/Pure/drule.ML
src/Pure/library.ML
src/Pure/pattern.ML
src/Tools/eqsubst.ML
src/Tools/induct_tacs.ML
     1.1 --- a/NEWS	Fri Nov 26 22:04:33 2010 +0100
     1.2 +++ b/NEWS	Fri Nov 26 22:29:41 2010 +0100
     1.3 @@ -507,6 +507,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Former exception Library.UnequalLengths now coincides with
     1.8 +ListPair.UnequalLengths.
     1.9 +
    1.10  * Renamed raw "explode" function to "raw_explode" to emphasize its
    1.11  meaning.  Note that internally to Isabelle, Symbol.explode is used in
    1.12  almost all situations.
     2.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Nov 26 22:04:33 2010 +0100
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Nov 26 22:29:41 2010 +0100
     2.3 @@ -324,7 +324,7 @@
     2.4             \ nested recursion")
     2.5         | (SOME {index, descr, ...}) =>
     2.6             let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
     2.7 -               val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
     2.8 +               val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
     2.9                   typ_error T ("Type constructor " ^ tname ^ " used with wrong\
    2.10                    \ number of arguments")
    2.11             in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
     3.1 --- a/src/HOL/Tools/Function/function_lib.ML	Fri Nov 26 22:04:33 2010 +0100
     3.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Fri Nov 26 22:29:41 2010 +0100
     3.3 @@ -44,11 +44,11 @@
     3.4  
     3.5  fun map4 _ [] [] [] [] = []
     3.6    | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us
     3.7 -  | map4 _ _ _ _ _ = raise Library.UnequalLengths;
     3.8 +  | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
     3.9  
    3.10  fun map7 _ [] [] [] [] [] [] [] = []
    3.11    | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
    3.12 -  | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths;
    3.13 +  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.14  
    3.15  
    3.16  
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Nov 26 22:04:33 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Fri Nov 26 22:29:41 2010 +0100
     4.3 @@ -393,7 +393,7 @@
     4.4    | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
     4.5                    accum =
     4.6      (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
     4.7 -     handle Library.UnequalLengths =>
     4.8 +     handle ListPair.UnequalLengths =>
     4.9              raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], []))
    4.10    | do_mtype_comp _ _ (MType _) (MType _) accum =
    4.11      accum (* no need to compare them thanks to the cache *)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Nov 26 22:04:33 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Nov 26 22:29:41 2010 +0100
     5.3 @@ -527,7 +527,7 @@
     5.4           | NONE =>
     5.5             Const (@{const_name Ex}, (T --> bool_T) --> bool_T)
     5.6             $ Abs (s, T, kill ss Ts ts))
     5.7 -      | kill _ _ _ = raise UnequalLengths
     5.8 +      | kill _ _ _ = raise ListPair.UnequalLengths
     5.9      fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) =
    5.10          gather (ss @ [s1]) (Ts @ [T1]) t1
    5.11        | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1)
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 26 22:04:33 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Nov 26 22:29:41 2010 +0100
     6.3 @@ -204,7 +204,7 @@
     6.4  
     6.5  fun map3 _ [] [] [] = []
     6.6    | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
     6.7 -  | map3 _ _ _ _ = raise UnequalLengths
     6.8 +  | map3 _ _ _ _ = raise ListPair.UnequalLengths
     6.9  
    6.10  fun double_lookup eq ps key =
    6.11    case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
     7.1 --- a/src/HOL/Tools/record.ML	Fri Nov 26 22:04:33 2010 +0100
     7.2 +++ b/src/HOL/Tools/record.ML	Fri Nov 26 22:29:41 2010 +0100
     7.3 @@ -917,7 +917,7 @@
     7.4                      val fields' = extern f :: map Long_Name.base_name fs;
     7.5                      val (args', more) = split_last args;
     7.6                    in (fields' ~~ args') @ strip_fields more end
     7.7 -                  handle Library.UnequalLengths => [("", t)])
     7.8 +                  handle ListPair.UnequalLengths => [("", t)])
     7.9                | NONE => [("", t)])
    7.10            | NONE => [("", t)])
    7.11         | _ => [("", t)]);
     8.1 --- a/src/Pure/Proof/reconstruct.ML	Fri Nov 26 22:04:33 2010 +0100
     8.2 +++ b/src/Pure/Proof/reconstruct.ML	Fri Nov 26 22:29:41 2010 +0100
     8.3 @@ -137,7 +137,7 @@
     8.4                  NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env
     8.5                | SOME Ts => (Ts, env));
     8.6              val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
     8.7 -              (forall_intr_vfs prop) handle Library.UnequalLengths =>
     8.8 +              (forall_intr_vfs prop) handle ListPair.UnequalLengths =>
     8.9                  error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
    8.10            in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
    8.11  
     9.1 --- a/src/Pure/consts.ML	Fri Nov 26 22:04:33 2010 +0100
     9.2 +++ b/src/Pure/consts.ML	Fri Nov 26 22:29:41 2010 +0100
     9.3 @@ -215,7 +215,7 @@
     9.4    let
     9.5      val declT = type_scheme consts c;
     9.6      val vars = map Term.dest_TVar (typargs consts (c, declT));
     9.7 -    val inst = vars ~~ Ts handle UnequalLengths =>
     9.8 +    val inst = vars ~~ Ts handle ListPair.UnequalLengths =>
     9.9        raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
    9.10    in declT |> Term_Subst.instantiateT inst end;
    9.11  
    10.1 --- a/src/Pure/drule.ML	Fri Nov 26 22:04:33 2010 +0100
    10.2 +++ b/src/Pure/drule.ML	Fri Nov 26 22:29:41 2010 +0100
    10.3 @@ -891,7 +891,7 @@
    10.4          handle TYPE (msg, _, _) => err msg;
    10.5  
    10.6      fun zip_vars xs ys =
    10.7 -      zip_options xs ys handle Library.UnequalLengths =>
    10.8 +      zip_options xs ys handle ListPair.UnequalLengths =>
    10.9          err "more instantiations than variables in thm";
   10.10  
   10.11      (*instantiate types first!*)
    11.1 --- a/src/Pure/library.ML	Fri Nov 26 22:04:33 2010 +0100
    11.2 +++ b/src/Pure/library.ML	Fri Nov 26 22:29:41 2010 +0100
    11.3 @@ -58,7 +58,6 @@
    11.4    val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
    11.5  
    11.6    (*lists*)
    11.7 -  exception UnequalLengths
    11.8    val single: 'a -> 'a list
    11.9    val the_single: 'a list -> 'a
   11.10    val singleton: ('a list -> 'b list) -> 'a -> 'b
   11.11 @@ -322,8 +321,6 @@
   11.12  
   11.13  (** lists **)
   11.14  
   11.15 -exception UnequalLengths;
   11.16 -
   11.17  fun single x = [x];
   11.18  
   11.19  fun the_single [x] = x
   11.20 @@ -496,7 +493,7 @@
   11.21        let val (ps, qs) = chop (length xs) ys
   11.22        in ps :: unflat xss qs end
   11.23    | unflat [] [] = []
   11.24 -  | unflat _ _ = raise UnequalLengths;
   11.25 +  | unflat _ _ = raise ListPair.UnequalLengths;
   11.26  
   11.27  fun burrow f xss = unflat xss (f (flat xss));
   11.28  
   11.29 @@ -535,19 +532,17 @@
   11.30  
   11.31  (* lists of pairs *)
   11.32  
   11.33 -exception UnequalLengths;
   11.34 -
   11.35  fun map2 _ [] [] = []
   11.36    | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
   11.37 -  | map2 _ _ _ = raise UnequalLengths;
   11.38 +  | map2 _ _ _ = raise ListPair.UnequalLengths;
   11.39  
   11.40  fun fold2 f [] [] z = z
   11.41    | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
   11.42 -  | fold2 f _ _ _ = raise UnequalLengths;
   11.43 +  | fold2 f _ _ _ = raise ListPair.UnequalLengths;
   11.44  
   11.45  fun fold_rev2 f [] [] z = z
   11.46    | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
   11.47 -  | fold_rev2 f _ _ _ = raise UnequalLengths;
   11.48 +  | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths;
   11.49  
   11.50  fun forall2 P [] [] = true
   11.51    | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
   11.52 @@ -563,13 +558,13 @@
   11.53  fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys
   11.54    | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys
   11.55    | zip_options _ [] = []
   11.56 -  | zip_options [] _ = raise UnequalLengths;
   11.57 +  | zip_options [] _ = raise ListPair.UnequalLengths;
   11.58  
   11.59  (*combine two lists forming a list of pairs:
   11.60    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
   11.61  fun [] ~~ [] = []
   11.62    | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
   11.63 -  | _ ~~ _ = raise UnequalLengths;
   11.64 +  | _ ~~ _ = raise ListPair.UnequalLengths;
   11.65  
   11.66  (*inverse of ~~; the old 'split':
   11.67    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
   11.68 @@ -848,10 +843,11 @@
   11.69  
   11.70  fun map_transpose f xss =
   11.71    let
   11.72 -    val n = case distinct (op =) (map length xss)
   11.73 -     of [] => 0
   11.74 +    val n =
   11.75 +      (case distinct (op =) (map length xss) of
   11.76 +        [] => 0
   11.77        | [n] => n
   11.78 -      | _ => raise UnequalLengths;
   11.79 +      | _ => raise ListPair.UnequalLengths);
   11.80    in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end;
   11.81  
   11.82  
   11.83 @@ -1071,3 +1067,5 @@
   11.84  
   11.85  structure Basic_Library: BASIC_LIBRARY = Library;
   11.86  open Basic_Library;
   11.87 +
   11.88 +datatype legacy = UnequalLengths;
    12.1 --- a/src/Pure/pattern.ML	Fri Nov 26 22:04:33 2010 +0100
    12.2 +++ b/src/Pure/pattern.ML	Fri Nov 26 22:29:41 2010 +0100
    12.3 @@ -365,7 +365,7 @@
    12.4    and cases(binders,env as (iTs,itms),pat,obj) =
    12.5      let val (ph,pargs) = strip_comb pat
    12.6          fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
    12.7 -				 handle UnequalLengths => raise MATCH
    12.8 +				 handle ListPair.UnequalLengths => raise MATCH
    12.9          fun rigrig2((a:string,Ta),(b,Tb),oargs) =
   12.10                if a <> b then raise MATCH
   12.11                else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
    13.1 --- a/src/Tools/eqsubst.ML	Fri Nov 26 22:04:33 2010 +0100
    13.2 +++ b/src/Tools/eqsubst.ML	Fri Nov 26 22:29:41 2010 +0100
    13.3 @@ -235,13 +235,13 @@
    13.4            val initenv =
    13.5              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
    13.6            val useq = Unify.smash_unifiers thry [a] initenv
    13.7 -              handle UnequalLengths => Seq.empty
    13.8 +              handle ListPair.UnequalLengths => Seq.empty
    13.9                     | Term.TERM _ => Seq.empty;
   13.10            fun clean_unify' useq () =
   13.11                (case (Seq.pull useq) of
   13.12                   NONE => NONE
   13.13                 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   13.14 -              handle UnequalLengths => NONE
   13.15 +              handle ListPair.UnequalLengths => NONE
   13.16                     | Term.TERM _ => NONE
   13.17          in
   13.18            (Seq.make (clean_unify' useq))
    14.1 --- a/src/Tools/induct_tacs.ML	Fri Nov 26 22:04:33 2010 +0100
    14.2 +++ b/src/Tools/induct_tacs.ML	Fri Nov 26 22:29:41 2010 +0100
    14.3 @@ -96,7 +96,7 @@
    14.4      val _ = Method.trace ctxt [rule'];
    14.5  
    14.6      val concls = Logic.dest_conjunctions (Thm.concl_of rule);
    14.7 -    val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths =>
    14.8 +    val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
    14.9        error "Induction rule has different numbers of variables";
   14.10    in res_inst_tac ctxt insts rule' i st end
   14.11    handle THM _ => Seq.empty;