--- 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);
--- 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 [] = []
--- 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
--- 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)));