fold_index replacing foldln
authorhaftmann
Mon Oct 31 16:00:15 2005 +0100 (2005-10-31)
changeset 18050652c95961a8b
parent 18049 156bba334c12
child 18051 dba086ed50cb
fold_index replacing foldln
TFL/casesplit.ML
src/HOL/Tools/split_rule.ML
src/Pure/Isar/rule_cases.ML
src/Pure/library.ML
     1.1 --- a/TFL/casesplit.ML	Mon Oct 31 01:43:22 2005 +0100
     1.2 +++ b/TFL/casesplit.ML	Mon Oct 31 16:00:15 2005 +0100
     1.3 @@ -336,31 +336,24 @@
     1.4  
     1.5  (* derive eqs, assuming strict, ie the rules have no assumptions = all
     1.6     the well-foundness conditions have been solved. *)
     1.7 -local
     1.8 -  fun get_related_thms i =
     1.9 -      List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
    1.10 -
    1.11 -  fun solve_eq (th, [], i) =
    1.12 -      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
    1.13 -    | solve_eq (th, [a], i) = (a, i)
    1.14 -    | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i);
    1.15 -in
    1.16  fun derive_init_eqs sgn rules eqs =
    1.17 -    let
    1.18 -      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop)
    1.19 -                      eqs
    1.20 -    in
    1.21 -      (rev o map solve_eq)
    1.22 -        (Library.foldln
    1.23 -           (fn (e,i) =>
    1.24 -               (curry (op ::)) (e, (get_related_thms (i - 1) rules), i - 1))
    1.25 -           eqths [])
    1.26 -    end;
    1.27 -end;
    1.28 -(*
    1.29 -    val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules)
    1.30 -    (map2 (op |>) (ths, expfs))
    1.31 -*)
    1.32 +  let
    1.33 +    fun get_related_thms i =
    1.34 +      List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
    1.35 +    fun add_eq (i, e) xs =
    1.36 +      (e, (get_related_thms i rules), i) :: xs
    1.37 +    fun solve_eq (th, [], i) =
    1.38 +          raise ERROR_MESSAGE "derive_init_eqs: missing rules"
    1.39 +      | solve_eq (th, [a], i) = (a, i)
    1.40 +      | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
    1.41 +    val eqths =
    1.42 +      map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs;
    1.43 +  in
    1.44 +    []
    1.45 +    |> fold_index add_eq eqths 
    1.46 +    |> map solve_eq
    1.47 +    |> rev
    1.48 +  end;
    1.49  
    1.50  end;
    1.51  
     2.1 --- a/src/HOL/Tools/split_rule.ML	Mon Oct 31 01:43:22 2005 +0100
     2.2 +++ b/src/HOL/Tools/split_rule.ML	Mon Oct 31 16:00:15 2005 +0100
     2.3 @@ -120,14 +120,16 @@
     2.4  
     2.5  fun split_rule_goal xss rl =
     2.6    let
     2.7 -    fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
     2.8 -    fun one_goal (xs, i) th = Library.foldl (one_split i) (th, xs);
     2.9 +    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
    2.10 +    fun one_goal (i, xs) = fold (one_split (i+1)) xs;
    2.11    in
    2.12 -    Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
    2.13 +    rl
    2.14 +    |> Library.fold_index one_goal xss
    2.15 +    |> Simplifier.full_simplify split_rule_ss
    2.16 +    |> Drule.standard 
    2.17      |> RuleCases.save rl
    2.18    end;
    2.19  
    2.20 -
    2.21  (* attribute syntax *)
    2.22  
    2.23  (* FIXME dynamically scoped due to Args.name/pair_tac *)
     3.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Oct 31 01:43:22 2005 +0100
     3.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Oct 31 16:00:15 2005 +0100
     3.3 @@ -142,7 +142,9 @@
     3.4  
     3.5  (* params *)
     3.6  
     3.7 -fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
     3.8 +fun rename_params xss thm =
     3.9 +  thm
    3.10 +  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i+1)) xss
    3.11    |> save thm;
    3.12  
    3.13  fun params xss = Drule.rule_attribute (K (rename_params xss));
     4.1 --- a/src/Pure/library.ML	Mon Oct 31 01:43:22 2005 +0100
     4.2 +++ b/src/Pure/library.ML	Mon Oct 31 16:00:15 2005 +0100
     4.3 @@ -99,7 +99,7 @@
     4.4    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
     4.5    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     4.6    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     4.7 -  val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
     4.8 +  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
     4.9    val unflat: 'a list list -> 'b list -> 'b list list
    4.10    val splitAt: int * 'a list -> 'a list * 'a list
    4.11    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    4.12 @@ -504,7 +504,11 @@
    4.13          | itr (x::l) = f(x, itr l)
    4.14    in  itr l  end;
    4.15  
    4.16 -fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
    4.17 +fun fold_index f =
    4.18 +  let
    4.19 +    fun fold_aux _  [] y = y
    4.20 +      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
    4.21 +  in fold_aux 0 end;
    4.22  
    4.23  fun foldl_map f =
    4.24    let