avoid Library.foldl_map
authorhaftmann
Thu Jun 04 16:11:04 2009 +0200 (2009-06-04)
changeset 31458b1cf26f2919b
parent 31457 d1cb222438d8
child 31459 ae39b7b2a68a
avoid Library.foldl_map
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Nominal/nominal_package.ML	Thu Jun 04 16:11:03 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_package.ML	Thu Jun 04 16:11:04 2009 +0200
     1.3 @@ -732,17 +732,18 @@
     1.4        let val xs = Long_Name.explode s;
     1.5        in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
     1.6  
     1.7 -    val (descr'', ndescr) = ListPair.unzip (List.mapPartial
     1.8 +    val (descr'', ndescr) = ListPair.unzip (map_filter
     1.9        (fn (i, ("Nominal.noption", _, _)) => NONE
    1.10          | (i, (s, dts, constrs)) =>
    1.11               let
    1.12                 val SOME index = AList.lookup op = ty_idxs i;
    1.13 -               val (constrs1, constrs2) = ListPair.unzip
    1.14 -                 (map (fn (cname, cargs) => apfst (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
    1.15 -                   (Library.foldl_map (fn (dts, dt) =>
    1.16 +               val (constrs2, constrs1) =
    1.17 +                 map_split (fn (cname, cargs) =>
    1.18 +                   apsnd (pair (strip_nth_name 2 (strip_nth_name 1 cname)))
    1.19 +                   (fold_map (fn dt => fn dts =>
    1.20                       let val (dts', dt') = strip_option dt
    1.21 -                     in (dts @ dts' @ [reindex dt'], (length dts, length dts')) end)
    1.22 -                       ([], cargs))) constrs)
    1.23 +                     in ((length dts, length dts'), dts @ dts' @ [reindex dt']) end)
    1.24 +                       cargs [])) constrs
    1.25               in SOME ((index, (strip_nth_name 1 s,  map reindex dts, constrs1)),
    1.26                 (index, constrs2))
    1.27               end) descr);
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Jun 04 16:11:03 2009 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Jun 04 16:11:04 2009 +0200
     2.3 @@ -89,10 +89,10 @@
     2.4              val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
     2.5              val T = Type (tname, dts');
     2.6              val rest = mk_term_of_def gr "and " xs;
     2.7 -            val (_, eqs) = Library.foldl_map (fn (prfx, (cname, Ts)) =>
     2.8 +            val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
     2.9                let val args = map (fn i =>
    2.10                  str ("x" ^ string_of_int i)) (1 upto length Ts)
    2.11 -              in ("  | ", Pretty.blk (4,
    2.12 +              in (Pretty.blk (4,
    2.13                  [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    2.14                   if null Ts then str (snd (get_const_id gr cname))
    2.15                   else parens (Pretty.block
    2.16 @@ -100,9 +100,9 @@
    2.17                      Pretty.brk 1, mk_tuple args]),
    2.18                   str " =", Pretty.brk 1] @
    2.19                   mk_constr_term cname Ts T
    2.20 -                   (map (fn (x, U) => [Pretty.block [mk_term_of gr module' false U,
    2.21 -                      Pretty.brk 1, x]]) (args ~~ Ts))))
    2.22 -              end) (prfx, cs')
    2.23 +                   (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U,
    2.24 +                      Pretty.brk 1, x]]) args Ts)), "  | ")
    2.25 +              end) cs' prfx
    2.26            in eqs @ rest end;
    2.27  
    2.28      fun mk_gen_of_def gr prfx [] = []
     3.1 --- a/src/HOL/Tools/datatype_realizer.ML	Thu Jun 04 16:11:03 2009 +0200
     3.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Thu Jun 04 16:11:04 2009 +0200
     3.3 @@ -56,17 +56,17 @@
     3.4      fun mk_all i s T t =
     3.5        if i mem is then list_all_free ([(s, T)], t) else t;
     3.6  
     3.7 -    val (prems, rec_fns) = split_list (List.concat (snd (Library.foldl_map
     3.8 -      (fn (j, ((i, (_, _, constrs)), T)) => Library.foldl_map (fn (j, (cname, cargs)) =>
     3.9 +    val (prems, rec_fns) = split_list (flat (fst (fold_map
    3.10 +      (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    3.11          let
    3.12            val Ts = map (typ_of_dtyp descr sorts) cargs;
    3.13            val tnames = Name.variant_list pnames (DatatypeProp.make_tnames Ts);
    3.14 -          val recs = List.filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    3.15 +          val recs = filter (is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
    3.16            val frees = tnames ~~ Ts;
    3.17  
    3.18            fun mk_prems vs [] = 
    3.19                  let
    3.20 -                  val rT = List.nth (rec_result_Ts, i);
    3.21 +                  val rT = nth (rec_result_Ts) i;
    3.22                    val vs' = filter_out is_unit vs;
    3.23                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
    3.24                    val f' = Envir.eta_contract (list_abs_free
    3.25 @@ -80,7 +80,7 @@
    3.26                    val k = body_index dt;
    3.27                    val (Us, U) = strip_type T;
    3.28                    val i = length Us;
    3.29 -                  val rT = List.nth (rec_result_Ts, k);
    3.30 +                  val rT = nth (rec_result_Ts) k;
    3.31                    val r = Free ("r" ^ s, Us ---> rT);
    3.32                    val (p, f) = mk_prems (vs @ [r]) ds
    3.33                  in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
    3.34 @@ -89,9 +89,8 @@
    3.35                        (app_bnds (Free (s, T)) i))), p)), f)
    3.36                  end
    3.37  
    3.38 -        in (j + 1,
    3.39 -          apfst (curry list_all_free frees) (mk_prems (map Free frees) recs))
    3.40 -        end) (j, constrs)) (1, descr ~~ recTs))));
    3.41 +        in (apfst (curry list_all_free frees) (mk_prems (map Free frees) recs), j + 1) end)
    3.42 +          constrs) (descr ~~ recTs) 1)));
    3.43   
    3.44      fun mk_proj j [] t = t
    3.45        | mk_proj j (i :: is) t = if null is then t else
     4.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 04 16:11:03 2009 +0200
     4.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 04 16:11:04 2009 +0200
     4.3 @@ -315,16 +315,16 @@
     4.4      fun get f = (these oo Option.map) f;
     4.5      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
     4.6        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
     4.7 -    val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) =>
     4.8 -      if s mem rsets then
     4.9 +    val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
    4.10 +      if member (op =) rsets s then
    4.11          let
    4.12            val (d :: dummies') = dummies;
    4.13            val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
    4.14 -        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
    4.15 -          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
    4.16 +        in (map (head_of o hd o rev o snd o strip_comb o fst o
    4.17 +          HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
    4.18          end
    4.19 -      else ((recs, dummies), replicate (length rs) Extraction.nullt))
    4.20 -        ((get #rec_thms dt_info, dummies), rss);
    4.21 +      else (replicate (length rs) Extraction.nullt, (recs, dummies)))
    4.22 +        rss (get #rec_thms dt_info, dummies);
    4.23      val rintrs = map (fn (intr, c) => Envir.eta_contract
    4.24        (Extraction.realizes_of thy2 vs
    4.25          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    4.26 @@ -360,7 +360,7 @@
    4.27  
    4.28      (** realizer for induction rule **)
    4.29  
    4.30 -    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
    4.31 +    val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
    4.32        SOME (fst (fst (dest_Var (head_of P)))) else NONE)
    4.33          (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
    4.34