# HG changeset patch # User wenzelm # Date 1290806981 -3600 # Node ID 441260986b631b795b5eb81a0a6d905b0aea8076 # Parent e5089e903e394b7c70991ca58d70e95c46883e9f make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths; diff -r e5089e903e39 -r 441260986b63 NEWS --- a/NEWS Fri Nov 26 22:04:33 2010 +0100 +++ b/NEWS Fri Nov 26 22:29:41 2010 +0100 @@ -507,6 +507,9 @@ *** ML *** +* Former exception Library.UnequalLengths now coincides with +ListPair.UnequalLengths. + * Renamed raw "explode" function to "raw_explode" to emphasize its meaning. Note that internally to Isabelle, Symbol.explode is used in almost all situations. diff -r e5089e903e39 -r 441260986b63 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Nov 26 22:29:41 2010 +0100 @@ -324,7 +324,7 @@ \ nested recursion") | (SOME {index, descr, ...}) => let val (_, vars, _) = (the o AList.lookup (op =) descr) index; - val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths => + val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths => typ_error T ("Type constructor " ^ tname ^ " used with wrong\ \ number of arguments") in (i + index, map (fn (j, (tn, args, cs)) => (i + j, diff -r e5089e903e39 -r 441260986b63 src/HOL/Tools/Function/function_lib.ML --- a/src/HOL/Tools/Function/function_lib.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/Function/function_lib.ML Fri Nov 26 22:29:41 2010 +0100 @@ -44,11 +44,11 @@ fun map4 _ [] [] [] [] = [] | map4 f (x :: xs) (y :: ys) (z :: zs) (u :: us) = f x y z u :: map4 f xs ys zs us - | map4 _ _ _ _ _ = raise Library.UnequalLengths; + | map4 _ _ _ _ _ = raise ListPair.UnequalLengths; fun map7 _ [] [] [] [] [] [] [] = [] | 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 - | map7 _ _ _ _ _ _ _ _ = raise Library.UnequalLengths; + | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; diff -r e5089e903e39 -r 441260986b63 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Nov 26 22:29:41 2010 +0100 @@ -393,7 +393,7 @@ | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22)) accum = (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)] - handle Library.UnequalLengths => + handle ListPair.UnequalLengths => raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2], [])) | do_mtype_comp _ _ (MType _) (MType _) accum = accum (* no need to compare them thanks to the cache *) diff -r e5089e903e39 -r 441260986b63 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Nov 26 22:29:41 2010 +0100 @@ -527,7 +527,7 @@ | NONE => Const (@{const_name Ex}, (T --> bool_T) --> bool_T) $ Abs (s, T, kill ss Ts ts)) - | kill _ _ _ = raise UnequalLengths + | kill _ _ _ = raise ListPair.UnequalLengths fun gather ss Ts (Const (@{const_name Ex}, _) $ Abs (s1, T1, t1)) = gather (ss @ [s1]) (Ts @ [T1]) t1 | gather [] [] (Abs (s, T, t1)) = Abs (s, T, gather [] [] t1) diff -r e5089e903e39 -r 441260986b63 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 26 22:29:41 2010 +0100 @@ -204,7 +204,7 @@ fun map3 _ [] [] [] = [] | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs - | map3 _ _ _ _ = raise UnequalLengths + | map3 _ _ _ _ = raise ListPair.UnequalLengths fun double_lookup eq ps key = case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps diff -r e5089e903e39 -r 441260986b63 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/HOL/Tools/record.ML Fri Nov 26 22:29:41 2010 +0100 @@ -917,7 +917,7 @@ val fields' = extern f :: map Long_Name.base_name fs; val (args', more) = split_last args; in (fields' ~~ args') @ strip_fields more end - handle Library.UnequalLengths => [("", t)]) + handle ListPair.UnequalLengths => [("", t)]) | NONE => [("", t)]) | NONE => [("", t)]) | _ => [("", t)]); diff -r e5089e903e39 -r 441260986b63 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Pure/Proof/reconstruct.ML Fri Nov 26 22:29:41 2010 +0100 @@ -137,7 +137,7 @@ NONE => fold_map mk_tvar (map snd tvars @ map snd tfrees) env | SOME Ts => (Ts, env)); val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts) - (forall_intr_vfs prop) handle Library.UnequalLengths => + (forall_intr_vfs prop) handle ListPair.UnequalLengths => error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf)) in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end; diff -r e5089e903e39 -r 441260986b63 src/Pure/consts.ML --- a/src/Pure/consts.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Pure/consts.ML Fri Nov 26 22:29:41 2010 +0100 @@ -215,7 +215,7 @@ let val declT = type_scheme consts c; val vars = map Term.dest_TVar (typargs consts (c, declT)); - val inst = vars ~~ Ts handle UnequalLengths => + val inst = vars ~~ Ts handle ListPair.UnequalLengths => raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]); in declT |> Term_Subst.instantiateT inst end; diff -r e5089e903e39 -r 441260986b63 src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Pure/drule.ML Fri Nov 26 22:29:41 2010 +0100 @@ -891,7 +891,7 @@ handle TYPE (msg, _, _) => err msg; fun zip_vars xs ys = - zip_options xs ys handle Library.UnequalLengths => + zip_options xs ys handle ListPair.UnequalLengths => err "more instantiations than variables in thm"; (*instantiate types first!*) diff -r e5089e903e39 -r 441260986b63 src/Pure/library.ML --- a/src/Pure/library.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Pure/library.ML Fri Nov 26 22:29:41 2010 +0100 @@ -58,7 +58,6 @@ val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c (*lists*) - exception UnequalLengths val single: 'a -> 'a list val the_single: 'a list -> 'a val singleton: ('a list -> 'b list) -> 'a -> 'b @@ -322,8 +321,6 @@ (** lists **) -exception UnequalLengths; - fun single x = [x]; fun the_single [x] = x @@ -496,7 +493,7 @@ let val (ps, qs) = chop (length xs) ys in ps :: unflat xss qs end | unflat [] [] = [] - | unflat _ _ = raise UnequalLengths; + | unflat _ _ = raise ListPair.UnequalLengths; fun burrow f xss = unflat xss (f (flat xss)); @@ -535,19 +532,17 @@ (* lists of pairs *) -exception UnequalLengths; - fun map2 _ [] [] = [] | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys - | map2 _ _ _ = raise UnequalLengths; + | map2 _ _ _ = raise ListPair.UnequalLengths; fun fold2 f [] [] z = z | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z) - | fold2 f _ _ _ = raise UnequalLengths; + | fold2 f _ _ _ = raise ListPair.UnequalLengths; fun fold_rev2 f [] [] z = z | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z) - | fold_rev2 f _ _ _ = raise UnequalLengths; + | fold_rev2 f _ _ _ = raise ListPair.UnequalLengths; fun forall2 P [] [] = true | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys @@ -563,13 +558,13 @@ fun zip_options (x :: xs) (SOME y :: ys) = (x, y) :: zip_options xs ys | zip_options (_ :: xs) (NONE :: ys) = zip_options xs ys | zip_options _ [] = [] - | zip_options [] _ = raise UnequalLengths; + | zip_options [] _ = raise ListPair.UnequalLengths; (*combine two lists forming a list of pairs: [x1, ..., xn] ~~ [y1, ..., yn] ===> [(x1, y1), ..., (xn, yn)]*) fun [] ~~ [] = [] | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys) - | _ ~~ _ = raise UnequalLengths; + | _ ~~ _ = raise ListPair.UnequalLengths; (*inverse of ~~; the old 'split': [(x1, y1), ..., (xn, yn)] ===> ([x1, ..., xn], [y1, ..., yn])*) @@ -848,10 +843,11 @@ fun map_transpose f xss = let - val n = case distinct (op =) (map length xss) - of [] => 0 + val n = + (case distinct (op =) (map length xss) of + [] => 0 | [n] => n - | _ => raise UnequalLengths; + | _ => raise ListPair.UnequalLengths); in map_range (fn m => f (map (fn xs => nth xs m) xss)) n end; @@ -1071,3 +1067,5 @@ structure Basic_Library: BASIC_LIBRARY = Library; open Basic_Library; + +datatype legacy = UnequalLengths; diff -r e5089e903e39 -r 441260986b63 src/Pure/pattern.ML --- a/src/Pure/pattern.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Pure/pattern.ML Fri Nov 26 22:29:41 2010 +0100 @@ -365,7 +365,7 @@ and cases(binders,env as (iTs,itms),pat,obj) = let val (ph,pargs) = strip_comb pat fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms) - handle UnequalLengths => raise MATCH + handle ListPair.UnequalLengths => raise MATCH fun rigrig2((a:string,Ta),(b,Tb),oargs) = if a <> b then raise MATCH else rigrig1(typ_match thy (Ta,Tb) iTs, oargs) diff -r e5089e903e39 -r 441260986b63 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Tools/eqsubst.ML Fri Nov 26 22:29:41 2010 +0100 @@ -235,13 +235,13 @@ val initenv = Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab}; val useq = Unify.smash_unifiers thry [a] initenv - handle UnequalLengths => Seq.empty + handle ListPair.UnequalLengths => Seq.empty | Term.TERM _ => Seq.empty; fun clean_unify' useq () = (case (Seq.pull useq) of NONE => NONE | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t))) - handle UnequalLengths => NONE + handle ListPair.UnequalLengths => NONE | Term.TERM _ => NONE in (Seq.make (clean_unify' useq)) diff -r e5089e903e39 -r 441260986b63 src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Fri Nov 26 22:04:33 2010 +0100 +++ b/src/Tools/induct_tacs.ML Fri Nov 26 22:29:41 2010 +0100 @@ -96,7 +96,7 @@ val _ = Method.trace ctxt [rule']; val concls = Logic.dest_conjunctions (Thm.concl_of rule); - val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths => + val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths => error "Induction rule has different numbers of variables"; in res_inst_tac ctxt insts rule' i st end handle THM _ => Seq.empty;