more standard fold/fold_rev;
authorwenzelm
Thu May 30 16:53:32 2013 +0200 (2013-05-30)
changeset 522422d634bfa1bbf
parent 52241 5f6e885382e9
child 52243 92bafa4235fa
more standard fold/fold_rev;
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu May 30 16:48:50 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 30 16:53:32 2013 +0200
     1.3 @@ -53,17 +53,15 @@
     1.4      let
     1.5        val premts = Thm.prems_of th;
     1.6  
     1.7 -      fun allify_prem_var (vt as (n,ty),t)  =
     1.8 +      fun allify_prem_var (vt as (n,ty)) t =
     1.9            (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    1.10  
    1.11 -      fun allify_prem Ts p = List.foldr allify_prem_var p Ts
    1.12 +      val allify_prem = fold_rev allify_prem_var
    1.13  
    1.14        val cTs = map (ctermify o Free) Ts
    1.15        val cterm_asms = map (ctermify o allify_prem Ts) premts
    1.16        val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    1.17 -    in
    1.18 -      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
    1.19 -    end;
    1.20 +    in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    1.21  
    1.22  (* make free vars into schematic vars with index zero *)
    1.23  fun unfix_frees frees =
     2.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 16:48:50 2013 +0200
     2.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 30 16:53:32 2013 +0200
     2.3 @@ -67,8 +67,8 @@
     2.4      (* using these names create lambda-abstracted version of the rule *)
     2.5      val abstractions = rev (Ts' ~~ tonames);
     2.6      val abstract_rule =
     2.7 -      Library.foldl (fn (th,((n,ty),ct)) => Thm.abstract_rule n ct th)
     2.8 -        (uncond_rule, abstractions);
     2.9 +      fold (fn ((n, ty), ct) => Thm.abstract_rule n ct)
    2.10 +        abstractions uncond_rule;
    2.11    in (cprems, abstract_rule) end;
    2.12  
    2.13  
    2.14 @@ -83,17 +83,16 @@
    2.15    let
    2.16      val rule_conds = Thm.prems_of rule_inst;
    2.17      val (_, cond_vs) =
    2.18 -      Library.foldl (fn ((tyvs, vs), t) =>
    2.19 -                (union (op =) (Misc_Legacy.term_tvars t) tyvs,
    2.20 -                 union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
    2.21 -            (([], []), rule_conds);
    2.22 +      fold (fn t => fn (tyvs, vs) =>
    2.23 +        (union (op =) (Misc_Legacy.term_tvars t) tyvs,
    2.24 +         union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs)) rule_conds ([], []);
    2.25      val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
    2.26      val vars_to_fix = union (op =) termvars cond_vs;
    2.27      val ys = IsaND.variant_names ctxt (tgt :: rule_conds) (map (fst o fst) vars_to_fix);
    2.28    in map2 (fn (xi, T) => fn y => ((xi, T), Free (y, T))) vars_to_fix ys end;
    2.29  
    2.30  (* make a new fresh typefree instantiation for the given tvar *)
    2.31 -fun new_tfree (tv as (ix,sort), (pairs,used)) =
    2.32 +fun new_tfree (tv as (ix,sort)) (pairs, used) =
    2.33    let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    2.34    in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
    2.35  
    2.36 @@ -104,11 +103,11 @@
    2.37    let
    2.38      val ignore_ixs = map fst ignore_insts;
    2.39      val (tvars, tfrees) =
    2.40 -      List.foldr (fn (t, (varixs, tfrees)) =>
    2.41 +      fold_rev (fn t => fn (varixs, tfrees) =>
    2.42          (Misc_Legacy.add_term_tvars (t,varixs),
    2.43 -         Misc_Legacy.add_term_tfrees (t,tfrees))) ([],[]) ts;
    2.44 +         Misc_Legacy.add_term_tfrees (t,tfrees))) ts ([], []);
    2.45      val unfixed_tvars = filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
    2.46 -    val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
    2.47 +    val (fixtyinsts, _) = fold_rev new_tfree unfixed_tvars ([], map fst tfrees)
    2.48    in (fixtyinsts, tfrees) end;
    2.49  
    2.50  
    2.51 @@ -176,10 +175,9 @@
    2.52  
    2.53      (* type-instantiate the var instantiations *)
    2.54      val insts_tyinst =
    2.55 -      List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
    2.56 +      fold_rev (fn (ix, (ty, t)) => fn insts_tyinst =>
    2.57          (ix, (Term.typ_subst_TVars term_typ_inst ty, Term.subst_TVars term_typ_inst t))
    2.58 -          :: insts_tyinst)
    2.59 -        [] unprepinsts;
    2.60 +          :: insts_tyinst) unprepinsts [];
    2.61  
    2.62      (* cross-instantiate *)
    2.63      val insts_tyinst_inst = cross_inst insts_tyinst;
     3.1 --- a/src/Tools/eqsubst.ML	Thu May 30 16:48:50 2013 +0200
     3.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 16:53:32 2013 +0200
     3.3 @@ -110,14 +110,14 @@
     3.4  fun mk_fake_bound_name n = ":b_" ^ n;
     3.5  fun fakefree_badbounds Ts t =
     3.6    let val (FakeTs, Ts, newnames) =
     3.7 -    List.foldr (fn ((n, ty), (FakeTs, Ts, usednames)) =>
     3.8 +    fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) =>
     3.9        let
    3.10          val newname = singleton (Name.variant_list usednames) n
    3.11        in
    3.12          ((mk_fake_bound_name newname, ty) :: FakeTs,
    3.13            (newname, ty) :: Ts,
    3.14            newname :: usednames)
    3.15 -      end) ([], [], []) Ts
    3.16 +      end) Ts ([], [], [])
    3.17    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
    3.18  
    3.19  (* before matching we need to fake the bound vars that are missing an