introduced new map2, fold
authorhaftmann
Fri Dec 02 08:06:59 2005 +0100 (2005-12-02)
changeset 18330444f16d232a2
parent 18329 221d47d17a81
child 18331 eb3a7d3d874b
introduced new map2, fold
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/induct_method.ML
src/Pure/IsaPlanner/isand.ML
src/Pure/Isar/locale.ML
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/library.ML
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 01 22:43:15 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Fri Dec 02 08:06:59 2005 +0100
     1.3 @@ -505,8 +505,8 @@
     1.4  
     1.5      val Abs_inverse_thms' =
     1.6        map #1 newT_iso_axms @
     1.7 -      map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
     1.8 -        (iso_inj_thms_unfolded, iso_thms);
     1.9 +      map2 (fn r_inj => fn r => f_myinv_f OF [r_inj, r RS mp])
    1.10 +        iso_inj_thms_unfolded iso_thms;
    1.11  
    1.12      val Abs_inverse_thms = List.concat (map mk_funs_inv Abs_inverse_thms');
    1.13  
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Dec 01 22:43:15 2005 +0100
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 02 08:06:59 2005 +0100
     2.3 @@ -448,12 +448,12 @@
     2.4  
     2.5  fun add_cases_induct no_elim no_induct coind names elims induct =
     2.6    let
     2.7 -    fun cases_spec (name, elim) thy =
     2.8 +    fun cases_spec name elim thy =
     2.9        thy
    2.10        |> Theory.add_path (Sign.base_name name)
    2.11        |> (#1 o PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])])
    2.12        |> Theory.parent_path;
    2.13 -    val cases_specs = if no_elim then [] else map2 cases_spec (names, elims);
    2.14 +    val cases_specs = if no_elim then [] else map2 cases_spec names elims;
    2.15  
    2.16      val induct_att =
    2.17        if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global;
     3.1 --- a/src/HOL/Tools/record_package.ML	Thu Dec 01 22:43:15 2005 +0100
     3.2 +++ b/src/HOL/Tools/record_package.ML	Fri Dec 02 08:06:59 2005 +0100
     3.3 @@ -1745,7 +1745,7 @@
     3.4          |> Theory.add_tyabbrs_i recordT_specs
     3.5          |> Theory.add_path bname
     3.6          |> Theory.add_consts_i
     3.7 -            (map2 (fn ((x, T), mx) => (x, T, mx)) (sel_decls, field_syntax @ [Syntax.NoSyn]))
     3.8 +            (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
     3.9          |> (Theory.add_consts_i o map Syntax.no_syn)
    3.10              (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
    3.11          |> (PureThy.add_defs_i false o map Thm.no_attributes) sel_specs
     4.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Dec 01 22:43:15 2005 +0100
     4.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Dec 02 08:06:59 2005 +0100
     4.3 @@ -279,7 +279,7 @@
     4.4  (* ------------------------------------------------------------------------- *)
     4.5  
     4.6  fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) =
     4.7 -  let val l = map2 (op +) (l1,l2)
     4.8 +  let val l = map2 (curry (op +)) l1 l2
     4.9    in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end;
    4.10  
    4.11  (* ------------------------------------------------------------------------- *)
    4.12 @@ -504,7 +504,7 @@
    4.13    let val (m,(lhs,i,rel,rhs,j,discrete)) = integ item
    4.14        val lhsa = map (coeff lhs) atoms
    4.15        and rhsa = map (coeff rhs) atoms
    4.16 -      val diff = map2 (op -) (rhsa,lhsa)
    4.17 +      val diff = map2 (curry (op -)) rhsa lhsa
    4.18        val c = i-j
    4.19        val just = Asm k
    4.20        fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))
     5.1 --- a/src/Provers/induct_method.ML	Thu Dec 01 22:43:15 2005 +0100
     5.2 +++ b/src/Provers/induct_method.ML	Fri Dec 02 08:06:59 2005 +0100
     5.3 @@ -298,7 +298,7 @@
     5.4      val certT = Thm.ctyp_of thy;
     5.5      val pairs = Envir.alist_of env;
     5.6      val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
     5.7 -    val xs = map2 (cert o Var) (map #1 pairs, map (#T o Thm.rep_cterm) ts);
     5.8 +    val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
     5.9    in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
    5.10  
    5.11  in
     6.1 --- a/src/Pure/IsaPlanner/isand.ML	Thu Dec 01 22:43:15 2005 +0100
     6.2 +++ b/src/Pure/IsaPlanner/isand.ML	Fri Dec 02 08:06:59 2005 +0100
     6.3 @@ -635,7 +635,7 @@
     6.4        val (subgoals, expf) = subgoal_thms th;
     6.5  (*       fun export_sg (th, exp) = exp th; *)
     6.6        fun export_sgs expfs solthms = 
     6.7 -          expf (map2 (op |>) (solthms, expfs));
     6.8 +          expf (map2 (curry (op |>)) solthms expfs);
     6.9  (*           expf (map export_sg (ths ~~ expfs)); *)
    6.10      in 
    6.11        apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
     7.1 --- a/src/Pure/Isar/locale.ML	Thu Dec 01 22:43:15 2005 +0100
     7.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 02 08:06:59 2005 +0100
     7.3 @@ -1219,8 +1219,8 @@
     7.4  
     7.5      (* CB: resolve schematic variables (patterns) in conclusion and external
     7.6         elements. *)
     7.7 -    val all_propp' = map2 (op ~~)
     7.8 -      (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp);
     7.9 +    val all_propp' = map2 (curry (op ~~))
    7.10 +      (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
    7.11      val (concl, propp) = splitAt(length raw_concl, all_propp');
    7.12      val propps = unflat raw_propps propp;
    7.13      val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
     8.1 --- a/src/Pure/Tools/class_package.ML	Thu Dec 01 22:43:15 2005 +0100
     8.2 +++ b/src/Pure/Tools/class_package.ML	Fri Dec 02 08:06:59 2005 +0100
     8.3 @@ -186,7 +186,7 @@
     8.4      val vars_used = fold (fn ty => curry (gen_union (op =))
     8.5        (map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs [];
     8.6      val vars_new = Term.invent_names vars_used "'a" (length arities);
     8.7 -    val typ_arity = Type (tyco, map2 TFree (vars_new, arities));
     8.8 +    val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities);
     8.9      val instmem_signs =
    8.10        map (typ_subst_atomic [(TFree ("'a", []), typ_arity)]) const_signs;
    8.11    in consts ~~ instmem_signs end;
    8.12 @@ -225,8 +225,8 @@
    8.13        of (subclass::deriv) => (rev deriv, find_index_eq subclass subclasses);
    8.14      fun mk_lookup (sort_def, (Type (tycon, tys))) =
    8.15            let
    8.16 -            val arity_lookup = map2 mk_lookup
    8.17 -              (map (filter_class thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def), tys)
    8.18 +            val arity_lookup = map2 (curry mk_lookup)
    8.19 +              (map (filter_class thy) (Sorts.mg_domain (Sign.classes_arities_of thy) tycon sort_def)) tys
    8.20            in map (fn class => Instance ((class, tycon), arity_lookup)) sort_def end
    8.21        | mk_lookup (sort_def, TVar ((vname, _), sort_use)) =
    8.22            let
     9.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Dec 01 22:43:15 2005 +0100
     9.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Dec 02 08:06:59 2005 +0100
     9.3 @@ -827,7 +827,7 @@
     9.4        let
     9.5          val vs = gen_names i;
     9.6          val tys = Library.take (i, (fst o strip_type) ty);
     9.7 -        val frees = map2 Free (vs, tys);
     9.8 +        val frees = map2 (curry Free) vs tys;
     9.9          val t' = Envir.beta_norm (list_comb (t, frees));
    9.10        in
    9.11          trns
    10.1 --- a/src/Pure/Tools/codegen_thingol.ML	Thu Dec 01 22:43:15 2005 +0100
    10.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Fri Dec 02 08:06:59 2005 +0100
    10.3 @@ -1109,7 +1109,7 @@
    10.4                |> Term.invent_names ((vars_of_iexprs o map snd) ds @ (vars_of_ipats o Library.flat o map fst) ds) "d"
    10.5                |> unflat (map snd sortctxt);
    10.6              val _ = writeln ("class 2");
    10.7 -            val vname_alist = map2 (fn ((vt, sort), vs) => (vt, vs ~~ sort)) (sortctxt, varnames_ctxt);
    10.8 +            val vname_alist = map2 (fn (vt, sort) => fn vs => (vt, vs ~~ sort)) sortctxt varnames_ctxt;
    10.9              val _ = writeln ("class 3");
   10.10              fun add_typarms ty =
   10.11                map (foldr1 (op xx) o (fn (vt, vss) => map (fn (_, cls) => cls `%% [IVarT (vt, [])]) vss)) vname_alist
    11.1 --- a/src/Pure/library.ML	Thu Dec 01 22:43:15 2005 +0100
    11.2 +++ b/src/Pure/library.ML	Fri Dec 02 08:06:59 2005 +0100
    11.3 @@ -97,7 +97,6 @@
    11.4    val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    11.5    val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    11.6    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
    11.7 -  val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    11.8    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    11.9    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   11.10    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
   11.11 @@ -113,18 +112,16 @@
   11.12    val find_index_eq: ''a -> ''a list -> int
   11.13    val find_first: ('a -> bool) -> 'a list -> 'a option
   11.14    val get_first: ('a -> 'b option) -> 'a list -> 'b option
   11.15 +  val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   11.16 +  val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   11.17 +  val ~~ : 'a list * 'b list -> ('a * 'b) list
   11.18 +  val split_list: ('a * 'b) list -> 'a list * 'b list
   11.19    val separate: 'a -> 'a list -> 'a list
   11.20    val replicate: int -> 'a -> 'a list
   11.21    val multiply: 'a list -> 'a list list -> 'a list list
   11.22    val product: 'a list -> 'b list -> ('a * 'b) list
   11.23    val filter: ('a -> bool) -> 'a list -> 'a list
   11.24    val filter_out: ('a -> bool) -> 'a list -> 'a list
   11.25 -  val map2: ('a * 'b -> 'c) -> 'a list * 'b list -> 'c list
   11.26 -  val exists2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   11.27 -  val forall2: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   11.28 -  val seq2: ('a * 'b -> unit) -> 'a list * 'b list -> unit
   11.29 -  val ~~ : 'a list * 'b list -> ('a * 'b) list
   11.30 -  val split_list: ('a * 'b) list -> 'a list * 'b list
   11.31    val equal_lists: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   11.32    val prefix: ''a list * ''a list -> bool
   11.33    val take_prefix: ('a -> bool) -> 'a list -> 'a list * 'a list
   11.34 @@ -467,13 +464,6 @@
   11.35        | fold_aux (x :: xs) y = fold_aux xs (f x y);
   11.36    in fold_aux end;
   11.37  
   11.38 -fun fold2 f =
   11.39 -  let
   11.40 -    fun fold_aux [] [] z = z
   11.41 -      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
   11.42 -      | fold_aux _ _ _ = raise UnequalLengths;
   11.43 -  in fold_aux end;
   11.44 -
   11.45  fun fold_rev f =
   11.46    let
   11.47      fun fold_aux [] y = y
   11.48 @@ -643,21 +633,17 @@
   11.49  
   11.50  exception UnequalLengths;
   11.51  
   11.52 -fun map2 _ ([], []) = []
   11.53 -  | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys)
   11.54 -  | map2 _ _ = raise UnequalLengths;
   11.55 -
   11.56 -fun exists2 _ ([], []) = false
   11.57 -  | exists2 pred (x :: xs, y :: ys) = pred (x, y) orelse exists2 pred (xs, ys)
   11.58 -  | exists2 _ _ = raise UnequalLengths;
   11.59 +fun map2 _ [] [] = []
   11.60 +  | map2 f (x :: xs) (y :: ys) = f x y :: map2 f xs ys
   11.61 +  | map2 _ _ _ = raise UnequalLengths;
   11.62  
   11.63 -fun forall2 _ ([], []) = true
   11.64 -  | forall2 pred (x :: xs, y :: ys) = pred (x, y) andalso forall2 pred (xs, ys)
   11.65 -  | forall2 _ _ = raise UnequalLengths;
   11.66 +fun fold2 f =
   11.67 +  let
   11.68 +    fun fold_aux [] [] z = z
   11.69 +      | fold_aux (x :: xs) (y :: ys) z = fold_aux xs ys (f x y z)
   11.70 +      | fold_aux _ _ _ = raise UnequalLengths;
   11.71 +  in fold_aux end;
   11.72  
   11.73 -fun seq2 _ ([], []) = ()
   11.74 -  | seq2 f (x :: xs, y :: ys) = (f (x, y); seq2 f (xs, ys))
   11.75 -  | seq2 _ _ = raise UnequalLengths;
   11.76  
   11.77  (*combine two lists forming a list of pairs:
   11.78    [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
   11.79 @@ -669,7 +655,11 @@
   11.80    [(x1, y1), ..., (xn, yn)]  ===>  ([x1, ..., xn], [y1, ..., yn])*)
   11.81  val split_list = ListPair.unzip;
   11.82  
   11.83 -fun equal_lists eq (xs, ys) = length xs = length ys andalso forall2 eq (xs, ys);
   11.84 +fun equal_lists eq (xs, ys) =
   11.85 +  let
   11.86 +    fun eq' [] [] = true
   11.87 +      | eq' (x :: xs) (y :: ys) = eq (x, y) andalso eq' xs ys
   11.88 +  in length xs = length ys andalso eq' xs ys end;
   11.89  
   11.90  
   11.91  (* prefixes, suffixes *)