# HG changeset patch # User haftmann # Date 1244124664 -7200 # Node ID b1cf26f2919b5d6e1d430b882d68a52b1214064f # Parent d1cb222438d852e6e577d2e6589313b02c69ebc8 avoid Library.foldl_map diff -r d1cb222438d8 -r b1cf26f2919b src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Thu Jun 04 16:11:03 2009 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Thu Jun 04 16:11:04 2009 +0200 @@ -732,17 +732,18 @@ let val xs = Long_Name.explode s; in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end; - val (descr'', ndescr) = ListPair.unzip (List.mapPartial + val (descr'', ndescr) = ListPair.unzip (map_filter (fn (i, ("Nominal.noption", _, _)) => NONE | (i, (s, dts, constrs)) => let val SOME index = AList.lookup op = ty_idxs i; - val (constrs1, constrs2) = ListPair.unzip - (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname))) - (Library.foldl_map (fn (dts, dt) => + val (constrs2, constrs1) = + map_split (fn (cname, cargs) => + apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname))) + (fold_map (fn dt => fn dts => let val (dts', dt') = strip_option dt - in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end) - ([], cargs))) constrs) + in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end) + cargs [])) constrs in SOME ((index, (strip_nth_name 1 s, map reindex dts, constrs1)), (index, constrs2)) end) descr); diff -r d1cb222438d8 -r b1cf26f2919b src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Thu Jun 04 16:11:03 2009 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Thu Jun 04 16:11:04 2009 +0200 @@ -89,10 +89,10 @@ val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts; val T = Type (tname, dts'); val rest = mk_term_of_def gr "and " xs; - val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) => + val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx => let val args = map (fn i => str ("x" ^ string_of_int i)) (1 upto length Ts) - in (" | ", Pretty.blk (4, + in (Pretty.blk (4, [str prfx, mk_term_of gr module' false T, Pretty.brk 1, if null Ts then str (snd (get_const_id gr cname)) else parens (Pretty.block @@ -100,9 +100,9 @@ Pretty.brk 1, mk_tuple args]), str " =", Pretty.brk 1] @ mk_constr_term cname Ts T - (map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U, - Pretty.brk 1, x]]) (args ~~ Ts)))) - end) (prfx, cs') + (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U, + Pretty.brk 1, x]]) args Ts)), " | ") + end) cs' prfx in eqs @ rest end; fun mk_gen_of_def gr prfx [] = [] diff -r d1cb222438d8 -r b1cf26f2919b src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Thu Jun 04 16:11:03 2009 +0200 +++ b/src/HOL/Tools/datatype_realizer.ML Thu Jun 04 16:11:04 2009 +0200 @@ -56,17 +56,17 @@ fun mk_all i s T t = if i mem is then list_all_free ([(s, T)], t) else t; - val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map - (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) => + val (prems, rec_fns) = split_list (flat (fst (fold_map + (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j => let val Ts = map (typ_of_dtyp descr sorts) cargs; val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts); - val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); + val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts); val frees = tnames ~~ Ts; fun mk_prems vs [] = let - val rT = List.nth (rec_result_Ts, i); + val rT = nth (rec_result_Ts) i; val vs' = filter_out is_unit vs; val f = mk_Free "f" (map fastype_of vs' ---> rT) j; val f' = Envir.eta_contract (list_abs_free @@ -80,7 +80,7 @@ val k = body_index dt; val (Us, U) = strip_type T; val i = length Us; - val rT = List.nth (rec_result_Ts, k); + val rT = nth (rec_result_Ts) k; val r = Free ("r" ^ s, Us ---> rT); val (p, f) = mk_prems (vs @ [r]) ds in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies @@ -89,9 +89,8 @@ (app_bnds (Free (s, T)) i))), p)), f) end - in (j + 1, - apfst (curry list_all_free frees) (mk_prems (map Free frees) recs)) - end) (j, constrs)) (1, descr ~~ recTs)))); + in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end) + constrs) (descr ~~ recTs) 1))); fun mk_proj j [] t = t | mk_proj j (i :: is) t = if null is then t else diff -r d1cb222438d8 -r b1cf26f2919b src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Thu Jun 04 16:11:03 2009 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Jun 04 16:11:04 2009 +0200 @@ -315,16 +315,16 @@ fun get f = (these oo Option.map) f; val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); - val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) => - if s mem rsets then + val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) => + if member (op =) rsets s then let val (d :: dummies') = dummies; val (recs1, recs2) = chop (length rs) (if d then tl recs else recs) - in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o - fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1) + in (map (head_of o hd o rev o snd o strip_comb o fst o + HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies')) end - else ((recs, dummies), replicate (length rs) Extraction.nullt)) - ((get #rec_thms dt_info, dummies), rss); + else (replicate (length rs) Extraction.nullt, (recs, dummies))) + rss (get #rec_thms dt_info, dummies); val rintrs = map (fn (intr, c) => Envir.eta_contract (Extraction.realizes_of thy2 vs (if c = Extraction.nullt then c else list_comb (c, map Var (rev @@ -360,7 +360,7 @@ (** realizer for induction rule **) - val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then + val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then SOME (fst (fst (dest_Var (head_of P)))) else NONE) (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));