# HG changeset patch # User haftmann # Date 1196860565 -3600 # Node ID 58e8ba3b792ba2969a3dace149664eb8bd9fa7a5 # Parent 55017c8b0a2496785796ae72fe8594b9f5b0772a map_product and fold_product diff -r 55017c8b0a24 -r 58e8ba3b792b src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Dec 05 14:16:05 2007 +0100 @@ -817,20 +817,20 @@ in map (fn aki => (List.mapPartial I (map (cps'_fun aki) ak_names))) ak_names end; (* list of all dj_inst-theorems *) val djs = - let fun djs_fun (ak1,ak2) = + let fun djs_fun ak1 ak2 = if ak1=ak2 then NONE else SOME(PureThy.get_thm thy32 (Name ("dj_"^ak2^"_"^ak1))) - in List.mapPartial I (map djs_fun (Library.product ak_names ak_names)) end; + in map_filter I (map_product djs_fun ak_names ak_names) end; (* list of all fs_inst-theorems *) val fss = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"_inst"))) ak_names (* list of all at_inst-theorems *) val fs_axs = map (fn ak => PureThy.get_thm thy32 (Name ("fs_"^ak^"1"))) ak_names - fun inst_pt thms = Library.flat (map (fn ti => instR ti pts) thms); - fun inst_at thms = Library.flat (map (fn ti => instR ti ats) thms); - fun inst_fs thms = Library.flat (map (fn ti => instR ti fss) thms); - fun inst_cp thms cps = Library.flat (inst_mult thms cps); + fun inst_pt thms = maps (fn ti => instR ti pts) thms; + fun inst_at thms = maps (fn ti => instR ti ats) thms; + fun inst_fs thms = maps (fn ti => instR ti fss) thms; + fun inst_cp thms cps = flat (inst_mult thms cps); fun inst_pt_at thms = inst_zip ats (inst_pt thms); - fun inst_dj thms = Library.flat (map (fn ti => instR ti djs) thms); + fun inst_dj thms = maps (fn ti => instR ti djs) thms; fun inst_pt_pt_at_cp thms = inst_cp (inst_zip ats (inst_zip pts (inst_pt thms))) cps; fun inst_pt_at_fs thms = inst_zip (inst_fs [fs1]) (inst_zip ats (inst_pt thms)); fun inst_pt_pt_at_cp thms = diff -r 55017c8b0a24 -r 58e8ba3b792b src/HOL/Tools/Groebner_Basis/groebner.ML --- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Dec 05 14:16:05 2007 +0100 @@ -316,7 +316,7 @@ let val npols = map2 (fn p => fn n => (p,Start n)) pols (0 upto (length pols - 1)) val phists = filter (fn (p,_) => not (null p)) npols val bas = grobner_interreduce [] (map monic phists) - val prs0 = product bas bas + val prs0 = map_product pair bas bas val prs1 = filter (fn ((x,_),(y,_)) => poly_lt x y) prs0 val prs2 = map (fn (p,q) => (mlcm (hd(fst p)) (hd(fst q)),(p,q))) prs1 val prs3 = diff -r 55017c8b0a24 -r 58e8ba3b792b src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/HOL/Tools/function_package/context_tree.ML Wed Dec 05 14:16:05 2007 +0100 @@ -97,8 +97,8 @@ in IntGraph.empty |> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches - |> fold (fn ((i,(c1,_)),(j,(_, t2))) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j)) - (product num_branches num_branches) + |> 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)) + num_branches num_branches end val add_congs = map (fn c => c RS eq_reflection) [cong, ext] diff -r 55017c8b0a24 -r 58e8ba3b792b src/HOL/Tools/function_package/lexicographic_order.ML --- a/src/HOL/Tools/function_package/lexicographic_order.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/HOL/Tools/function_package/lexicographic_order.ML Wed Dec 05 14:16:05 2007 +0100 @@ -120,8 +120,7 @@ | mk_funorder_funs T = [ constant_1 T ] fun mk_ext_base_funs thy (Type("+", [fT, sT])) = - product (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT) - |> map (uncurry mk_sum_case) + map_product mk_sum_case (mk_ext_base_funs thy fT) (mk_ext_base_funs thy sT) | mk_ext_base_funs thy T = mk_base_funs thy T fun mk_all_measure_funs thy (T as Type ("+", _)) = diff -r 55017c8b0a24 -r 58e8ba3b792b src/HOL/Tools/function_package/pattern_split.ML --- a/src/HOL/Tools/function_package/pattern_split.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/HOL/Tools/function_package/pattern_split.ML Wed Dec 05 14:16:05 2007 +0100 @@ -48,7 +48,7 @@ fun join ((vs1,sub1), (vs2,sub2)) = (merge (op aconv) (vs1,vs2), sub1 @ sub2) -fun join_product (xs, ys) = map join (product xs ys) +fun join_product (xs, ys) = map_product (curry join) xs ys fun join_list [] = [] | join_list xs = foldr1 (join_product) xs diff -r 55017c8b0a24 -r 58e8ba3b792b src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/HOL/Tools/refute.ML Wed Dec 05 14:16:05 2007 +0100 @@ -2181,7 +2181,7 @@ (* C_i x_1 ... x_n < C_i y_1 ... y_n if *) (* (x_1, ..., x_n) < (y_1, ..., y_n) *) constructor_terms - (map (op $) (Library.product terms d_terms)) ds + (map_product (curry op $) terms d_terms) ds end in (* C_i ... < C_j ... if i < j *) diff -r 55017c8b0a24 -r 58e8ba3b792b src/Pure/General/graph.ML --- a/src/Pure/General/graph.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/Pure/General/graph.ML Wed Dec 05 14:16:05 2007 +0100 @@ -257,7 +257,7 @@ fun add_edge_trans_acyclic (x, y) G = add_edge_acyclic (x, y) G - |> fold add_edge (Library.product (all_preds G [x]) (all_succs G [y])); + |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]); fun merge_trans_acyclic eq (G1, G2) = merge_acyclic eq (G1, G2) diff -r 55017c8b0a24 -r 58e8ba3b792b src/Pure/library.ML --- a/src/Pure/library.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/Pure/library.ML Wed Dec 05 14:16:05 2007 +0100 @@ -100,13 +100,14 @@ val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c + val map_product: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list + val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c val zip_options: 'a list -> 'b option list -> ('a * 'b) list val ~~ : 'a list * 'b list -> ('a * 'b) list val split_list: ('a * 'b) list -> 'a list * 'b list val separate: 'a -> 'a list -> 'a list val replicate: int -> 'a -> 'a list val multiply: 'a list -> 'a list list -> 'a list list - val product: 'a list -> 'b list -> ('a * 'b) list val filter: ('a -> bool) -> 'a list -> 'a list val filter_out: ('a -> bool) -> 'a list -> 'a list val map_filter: ('a -> 'b option) -> 'a list -> 'b list @@ -429,6 +430,11 @@ fun maps f [] = [] | maps f (x :: xs) = f x @ maps f xs; +(*copy the list preserving elements that satisfy the predicate*) +val filter = List.filter; +fun filter_out f = filter (not o f); +val map_filter = List.mapPartial; + fun chop (0: int) xs = ([], xs) | chop _ [] = ([], []) | chop n (x :: xs) = chop (n - 1) xs |>> cons x; @@ -540,20 +546,15 @@ | multiply (x :: xs) yss = map (cons x) yss @ multiply xs yss; (*direct product*) -fun product _ [] = [] - | product [] _ = [] - | product (x :: xs) ys = map (pair x) ys @ product xs ys; - - -(* filter *) +fun map_product f _ [] = [] + | map_product f [] _ = [] + | map_product f (x :: xs) ys = map (f x) ys @ map_product f xs ys; -(*copy the list preserving elements that satisfy the predicate*) -val filter = List.filter; -fun filter_out f = filter (not o f); -val map_filter = List.mapPartial; +fun fold_product f _ [] z = z + | fold_product f [] _ z = z + | fold_product f (x :: xs) ys z = z |> fold (f x) ys |> fold_product f xs ys; - -(* lists of pairs *) +(*lists of pairs*) exception UnequalLengths; diff -r 55017c8b0a24 -r 58e8ba3b792b src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Wed Dec 05 14:15:59 2007 +0100 +++ b/src/Tools/code/code_target.ML Wed Dec 05 14:16:05 2007 +0100 @@ -1037,7 +1037,7 @@ #> fold2 (fn name' => fn base' => Graph.new_node (name', (Def (base', NONE)))) names' bases'))) |> apsnd (fold (fn name => fold (add_dep name) deps) names) - |> apsnd (fold (map_node modl_explode o Graph.add_edge) (product names names)) + |> apsnd (fold_product (curry (map_node modl_explode o Graph.add_edge)) names names) end; fun group_defs [(_, CodeThingol.Bot)] = I