map_product and fold_product
authorhaftmann
Wed Dec 05 14:16:05 2007 +0100 (2007-12-05 ago)
changeset 2553858e8ba3b792b
parent 25537 55017c8b0a24
child 25539 8b7ed8aef001
map_product and fold_product
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/lexicographic_order.ML
src/HOL/Tools/function_package/pattern_split.ML
src/HOL/Tools/refute.ML
src/Pure/General/graph.ML
src/Pure/library.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 05 14:15:59 2007 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 05 14:16:05 2007 +0100
     1.3 @@ -817,20 +817,20 @@
     1.4  		in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end;
     1.5               (* list of all dj_inst-theorems *)
     1.6               val djs = 
     1.7 -	       let fun djs_fun (ak1,ak2) = 
     1.8 +	       let fun djs_fun ak1 ak2 = 
     1.9  		     if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1)))
    1.10 -	       in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end;
    1.11 +	       in map_filter I (map_product djs_fun ak_names ak_names) end;
    1.12               (* list of all fs_inst-theorems *)
    1.13               val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names
    1.14               (* list of all at_inst-theorems *)
    1.15               val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names
    1.16  
    1.17 -             fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms);
    1.18 -             fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms);
    1.19 -             fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms);
    1.20 -             fun inst_cp thms cps = Library.flat (inst_mult thms cps);
    1.21 +             fun inst_pt thms = maps (fn ti => instR ti pts) thms;
    1.22 +             fun inst_at thms = maps (fn ti => instR ti ats) thms;
    1.23 +             fun inst_fs thms = maps (fn ti => instR ti fss) thms;
    1.24 +             fun inst_cp thms cps = flat (inst_mult thms cps);
    1.25  	     fun inst_pt_at thms = inst_zip ats (inst_pt thms);
    1.26 -             fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms);
    1.27 +             fun inst_dj thms = maps (fn ti => instR ti djs) thms;
    1.28  	     fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps;
    1.29               fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms));
    1.30  	     fun inst_pt_pt_at_cp thms =
     2.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Dec 05 14:15:59 2007 +0100
     2.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Dec 05 14:16:05 2007 +0100
     2.3 @@ -316,7 +316,7 @@
     2.4      let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1))
     2.5          val phists = filter (fn (p,_) => not (null p)) npols
     2.6          val bas = grobner_interreduce [] (map monic phists)
     2.7 -        val prs0 = product bas bas
     2.8 +        val prs0 = map_product pair bas bas
     2.9          val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0
    2.10          val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1
    2.11          val prs3 =
     3.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Wed Dec 05 14:15:59 2007 +0100
     3.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Dec 05 14:16:05 2007 +0100
     3.3 @@ -97,8 +97,8 @@
     3.4      in
     3.5        IntGraph.empty
     3.6          |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
     3.7 -        |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
     3.8 -        (product num_branches num_branches)
     3.9 +        |> fold_product (fn (i,(c1,_)) => fn (j,(_, t2)) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
    3.10 +             num_branches num_branches
    3.11      end
    3.12      
    3.13  val add_congs = map (fn c => c RS eq_reflection) [cong, ext] 
     4.1 --- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 05 14:15:59 2007 +0100
     4.2 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Dec 05 14:16:05 2007 +0100
     4.3 @@ -120,8 +120,7 @@
     4.4    | mk_funorder_funs T = [ constant_1 T ]
     4.5  
     4.6  fun mk_ext_base_funs thy (Type("+", [fT, sT])) =
     4.7 -    product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
     4.8 -       |> map (uncurry mk_sum_case)
     4.9 +      map_product mk_sum_case (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT)
    4.10    | mk_ext_base_funs thy T = mk_base_funs thy T
    4.11  
    4.12  fun mk_all_measure_funs thy (T as Type ("+", _)) =
     5.1 --- a/src/HOL/Tools/function_package/pattern_split.ML	Wed Dec 05 14:15:59 2007 +0100
     5.2 +++ b/src/HOL/Tools/function_package/pattern_split.ML	Wed Dec 05 14:16:05 2007 +0100
     5.3 @@ -48,7 +48,7 @@
     5.4                              
     5.5  
     5.6  fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2)
     5.7 -fun join_product (xs, ys) = map join (product xs ys)
     5.8 +fun join_product (xs, ys) = map_product (curry join) xs ys
     5.9  
    5.10  fun join_list [] = []
    5.11    | join_list xs = foldr1 (join_product) xs
     6.1 --- a/src/HOL/Tools/refute.ML	Wed Dec 05 14:15:59 2007 +0100
     6.2 +++ b/src/HOL/Tools/refute.ML	Wed Dec 05 14:16:05 2007 +0100
     6.3 @@ -2181,7 +2181,7 @@
     6.4                    (* C_i x_1 ... x_n < C_i y_1 ... y_n if *)
     6.5                    (* (x_1, ..., x_n) < (y_1, ..., y_n)    *)
     6.6                    constructor_terms
     6.7 -                    (map (op $) (Library.product terms d_terms)) ds
     6.8 +                    (map_product (curry op $) terms d_terms) ds
     6.9                  end
    6.10              in
    6.11                (* C_i ... < C_j ... if i < j *)
     7.1 --- a/src/Pure/General/graph.ML	Wed Dec 05 14:15:59 2007 +0100
     7.2 +++ b/src/Pure/General/graph.ML	Wed Dec 05 14:16:05 2007 +0100
     7.3 @@ -257,7 +257,7 @@
     7.4  
     7.5  fun add_edge_trans_acyclic (x, y) G =
     7.6    add_edge_acyclic (x, y) G
     7.7 -  |> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y]));
     7.8 +  |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
     7.9  
    7.10  fun merge_trans_acyclic eq (G1, G2) =
    7.11    merge_acyclic eq (G1, G2)
     8.1 --- a/src/Pure/library.ML	Wed Dec 05 14:15:59 2007 +0100
     8.2 +++ b/src/Pure/library.ML	Wed Dec 05 14:16:05 2007 +0100
     8.3 @@ -100,13 +100,14 @@
     8.4    val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     8.5    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     8.6    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     8.7 +  val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
     8.8 +  val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
     8.9    val zip_options: 'a list -> 'b option list -> ('a * 'b) list
    8.10    val ~~ : 'a list * 'b list -> ('a * 'b) list
    8.11    val split_list: ('a * 'b) list -> 'a list * 'b list
    8.12    val separate: 'a -> 'a list -> 'a list
    8.13    val replicate: int -> 'a -> 'a list
    8.14    val multiply: 'a list -> 'a list list -> 'a list list
    8.15 -  val product: 'a list -> 'b list -> ('a * 'b) list
    8.16    val filter: ('a -> bool) -> 'a list -> 'a list
    8.17    val filter_out: ('a -> bool) -> 'a list -> 'a list
    8.18    val map_filter: ('a -> 'b option) -> 'a list -> 'b list
    8.19 @@ -429,6 +430,11 @@
    8.20  fun maps f [] = []
    8.21    | maps f (x :: xs) = f x @ maps f xs;
    8.22  
    8.23 +(*copy the list preserving elements that satisfy the predicate*)
    8.24 +val filter = List.filter;
    8.25 +fun filter_out f = filter (not o f);
    8.26 +val map_filter = List.mapPartial;
    8.27 +
    8.28  fun chop (0: int) xs = ([], xs)
    8.29    | chop _ [] = ([], [])
    8.30    | chop n (x :: xs) = chop (n - 1) xs |>> cons x;
    8.31 @@ -540,20 +546,15 @@
    8.32    | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss;
    8.33  
    8.34  (*direct product*)
    8.35 -fun product _ [] = []
    8.36 -  | product [] _ = []
    8.37 -  | product (x :: xs) ys = map (pair x) ys @ product xs ys;
    8.38 -
    8.39 -
    8.40 -(* filter *)
    8.41 +fun map_product f _ [] = []
    8.42 +  | map_product f [] _ = []
    8.43 +  | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys;
    8.44  
    8.45 -(*copy the list preserving elements that satisfy the predicate*)
    8.46 -val filter = List.filter;
    8.47 -fun filter_out f = filter (not o f);
    8.48 -val map_filter = List.mapPartial;
    8.49 +fun fold_product f _ [] z = z
    8.50 +  | fold_product f [] _ z = z
    8.51 +  | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys;
    8.52  
    8.53 -
    8.54 -(* lists of pairs *)
    8.55 +(*lists of pairs*)
    8.56  
    8.57  exception UnequalLengths;
    8.58  
     9.1 --- a/src/Tools/code/code_target.ML	Wed Dec 05 14:15:59 2007 +0100
     9.2 +++ b/src/Tools/code/code_target.ML	Wed Dec 05 14:16:05 2007 +0100
     9.3 @@ -1037,7 +1037,7 @@
     9.4                #> fold2 (fn name' => fn base' =>
     9.5                     Graph.new_node (name', (Def (base', NONE)))) names' bases')))
     9.6          |> apsnd (fold (fn name => fold (add_dep name) deps) names)
     9.7 -        |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names))
     9.8 +        |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names)
     9.9        end;
    9.10      fun group_defs [(_, CodeThingol.Bot)] =
    9.11            I