(intermediate commit)
authorhaftmann
Wed Jul 13 11:16:34 2005 +0200 (2005-07-13)
changeset 16787b6b6e2faaa41
parent 16786 54b5df610651
child 16788 0c6f5fe30676
(intermediate commit)
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/Proof/reconstruct.ML
src/Pure/drule.ML
src/Pure/goals.ML
src/Pure/proofterm.ML
src/Pure/pure_thy.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/Isar/induct_attrib.ML	Wed Jul 13 10:48:21 2005 +0200
     1.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Jul 13 11:16:34 2005 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  local
     1.5  
     1.6  fun rev_vars_of tm =
     1.7 -  Term.foldl_aterms (fn (ts, t as Var _) => t :: ts | (ts, _) => ts) ([], tm)
     1.8 +  Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
     1.9    |> Library.distinct;
    1.10  
    1.11  val mk_var = encode_type o #2 o Term.dest_Var;
     2.1 --- a/src/Pure/Isar/locale.ML	Wed Jul 13 10:48:21 2005 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Wed Jul 13 11:16:34 2005 +0200
     2.3 @@ -705,7 +705,7 @@
     2.4  
     2.5  fun frozen_tvars ctxt Ts =
     2.6    let
     2.7 -    val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
     2.8 +    val tvars = rev (fold Term.add_tvarsT Ts []);
     2.9      val tfrees = map TFree
    2.10        (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
    2.11    in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;
     3.1 --- a/src/Pure/Isar/obtain.ML	Wed Jul 13 10:48:21 2005 +0200
     3.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jul 13 11:16:34 2005 +0200
     3.3 @@ -89,8 +89,8 @@
     3.4      val bound_thesis_raw as (bound_thesis_name, _) =
     3.5        Term.dest_Free (bind_thesis (Free (thesisN, propT)));
     3.6      val bound_thesis_var =
     3.7 -      foldl_aterms (fn (v, Free (x, T)) => if x = bound_thesis_name then (x, T) else v
     3.8 -        | (v, t) => v) (bound_thesis_raw, bound_thesis);
     3.9 +      fold_aterms (fn Free (x, T) => (fn v => if x = bound_thesis_name then (x, T) else v)
    3.10 +        | _ => I) bound_thesis bound_thesis_raw;
    3.11  
    3.12      fun occs_var x = Library.get_first (fn t =>
    3.13        ProofContext.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
     4.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jul 13 10:48:21 2005 +0200
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jul 13 11:16:34 2005 +0200
     4.3 @@ -565,22 +565,25 @@
     4.4  
     4.5  local
     4.6  
     4.7 -val ins_types = foldl_aterms
     4.8 -  (fn (types, Free (x, T)) => Vartab.update (((x, ~1), T), types)
     4.9 -    | (types, Var v) => Vartab.update (v, types)
    4.10 -    | (types, _) => types);
    4.11 +val ins_types = 
    4.12 +  let fun ins_types' (Free (x, T)) types = Vartab.update (((x, ~1), T), types)
    4.13 +         | ins_types' (Var v) types = Vartab.update (v, types)
    4.14 +         | ins_types' _ types = types
    4.15 +  in fold_aterms ins_types' end;
    4.16  
    4.17 -val ins_sorts = foldl_types (foldl_atyps
    4.18 -  (fn (sorts, TFree (x, S)) => Vartab.update (((x, ~1), S), sorts)
    4.19 -    | (sorts, TVar v) => Vartab.update (v, sorts)
    4.20 -    | (sorts, _) => sorts));
    4.21 +val ins_sorts =
    4.22 +  let fun ins_sorts' (TFree (x, S)) sorts = Vartab.update (((x, ~1), S), sorts)
    4.23 +         | ins_sorts' (TVar v) sorts = Vartab.update (v, sorts)
    4.24 +         | ins_sorts' _ sorts = sorts
    4.25 +  in fold_types ins_sorts' end;
    4.26  
    4.27 -val ins_used = foldl_term_types (fn t => foldl_atyps
    4.28 -  (fn (used, TFree (x, _)) => x ins_string used
    4.29 -    | (used, _) => used));
    4.30 +val ins_used = fold_term_types (fn t => fold_atyps
    4.31 +  (fn TFree (x, _) => curry (op ins_string) x
    4.32 +    | _ => I));
    4.33  
    4.34 -val ins_occs = foldl_term_types (fn t => foldl_atyps
    4.35 -  (fn (tab, TFree (x, _)) => Symtab.update_multi ((x, t), tab) | (tab, _) => tab));
    4.36 +val ins_occs = fold_term_types (fn t => fold_atyps
    4.37 +  (fn TFree (x, _) => curry Symtab.update_multi (x, t)
    4.38 +    | _ => I));
    4.39  
    4.40  fun ins_skolem def_ty = foldr
    4.41    (fn ((x, x'), types) =>
    4.42 @@ -595,14 +598,14 @@
    4.43  
    4.44  fun declare_term_syntax t ctxt =
    4.45    ctxt
    4.46 -  |> map_defaults (fn (types, sorts, used, occ) => (ins_types (types, t), sorts, used, occ))
    4.47 -  |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ))
    4.48 -  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ));
    4.49 +  |> map_defaults (fn (types, sorts, used, occ) => (ins_types t types, sorts, used, occ))
    4.50 +  |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts t sorts, used, occ))
    4.51 +  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used t used, occ));
    4.52  
    4.53  fun declare_term t ctxt =
    4.54    ctxt
    4.55    |> declare_term_syntax t
    4.56 -  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
    4.57 +  |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs t occ))
    4.58    |> map_defaults (fn (types, sorts, used, occ) =>
    4.59        (ins_skolem (fn x =>
    4.60          Vartab.lookup (types, (x, ~1))) types (fixes_of ctxt), sorts, used, occ));
    4.61 @@ -676,10 +679,10 @@
    4.62  
    4.63  (** export theorems **)
    4.64  
    4.65 -fun get_free x (NONE, t as Free (y, _)) = if x = y then SOME t else NONE
    4.66 -  | get_free _ (opt, _) = opt;
    4.67 -
    4.68 -fun find_free t x = foldl_aterms (get_free x) (NONE, t);
    4.69 +fun find_free t x =
    4.70 +  let fun get_free (t as Free (y, _)) NONE = if x = y then SOME t else NONE
    4.71 +         | get_free _ opt = opt
    4.72 +  in fold_aterms get_free t NONE end;
    4.73  
    4.74  fun export_view view is_goal inner outer =
    4.75    let
     5.1 --- a/src/Pure/Proof/extraction.ML	Wed Jul 13 10:48:21 2005 +0200
     5.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jul 13 11:16:34 2005 +0200
     5.3 @@ -128,8 +128,8 @@
     5.4  
     5.5  fun msg d s = priority (Symbol.spaces d ^ s);
     5.6  
     5.7 -fun vars_of t = rev (foldl_aterms
     5.8 -  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
     5.9 +fun vars_of t = rev (fold_aterms
    5.10 +  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
    5.11  
    5.12  fun vfs_of t = vars_of t @ sort (make_ord atless) (term_frees t);
    5.13  
     6.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 13 10:48:21 2005 +0200
     6.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Jul 13 11:16:34 2005 +0200
     6.3 @@ -210,8 +210,8 @@
     6.4  
     6.5  (**** eliminate definitions in proof ****)
     6.6  
     6.7 -fun vars_of t = rev (foldl_aterms
     6.8 -  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
     6.9 +fun vars_of t = rev (fold_aterms
    6.10 +  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
    6.11  
    6.12  fun insert_refl defs Ts (prf1 %% prf2) =
    6.13        insert_refl defs Ts prf1 %% insert_refl defs Ts prf2
     7.1 --- a/src/Pure/Proof/reconstruct.ML	Wed Jul 13 10:48:21 2005 +0200
     7.2 +++ b/src/Pure/Proof/reconstruct.ML	Wed Jul 13 11:16:34 2005 +0200
     7.3 @@ -23,8 +23,8 @@
     7.4  val quiet_mode = ref true;
     7.5  fun message s = if !quiet_mode then () else writeln s;
     7.6  
     7.7 -fun vars_of t = rev (foldl_aterms
     7.8 -  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
     7.9 +fun vars_of t = rev (fold_aterms
    7.10 +  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
    7.11  
    7.12  fun forall_intr (t, prop) =
    7.13    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
     8.1 --- a/src/Pure/drule.ML	Wed Jul 13 10:48:21 2005 +0200
     8.2 +++ b/src/Pure/drule.ML	Wed Jul 13 11:16:34 2005 +0200
     8.3 @@ -958,7 +958,7 @@
     8.4  
     8.5  (* vars in left-to-right order *)
     8.6  
     8.7 -fun tvars_of_terms ts = rev (Library.foldl Term.add_tvars ([], ts));
     8.8 +fun tvars_of_terms ts = rev (fold Term.add_tvars ts []);
     8.9  fun vars_of_terms ts = rev (Library.foldl Term.add_vars ([], ts));
    8.10  
    8.11  fun tvars_of thm = tvars_of_terms [Thm.full_prop_of thm];
     9.1 --- a/src/Pure/goals.ML	Wed Jul 13 10:48:21 2005 +0200
     9.2 +++ b/src/Pure/goals.ML	Wed Jul 13 11:16:34 2005 +0200
     9.3 @@ -350,10 +350,10 @@
     9.4  
     9.5  (* prepare props *)
     9.6  
     9.7 -val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
     9.8 +val add_frees = fold_aterms (fn Free v => (fn vs => v ins vs) | _ => I);
     9.9  
    9.10  fun enter_term t (envS, envT, used) =
    9.11 -  (Term.add_term_tfrees (t, envS), add_frees (envT, t), Term.add_term_tfree_names (t, used));
    9.12 +  (Term.add_term_tfrees (t, envS), add_frees t envT, Term.add_term_tfree_names (t, used));
    9.13  
    9.14  fun read_axm thy ((envS, envT, used), (name, s)) =
    9.15    let
    10.1 --- a/src/Pure/proofterm.ML	Wed Jul 13 10:48:21 2005 +0200
    10.2 +++ b/src/Pure/proofterm.ML	Wed Jul 13 11:16:34 2005 +0200
    10.3 @@ -766,8 +766,8 @@
    10.4  
    10.5  (***** axioms and theorems *****)
    10.6  
    10.7 -fun vars_of t = rev (foldl_aterms
    10.8 -  (fn (vs, v as Var _) => v ins vs | (vs, _) => vs) ([], t));
    10.9 +fun vars_of t = rev (fold_aterms
   10.10 +  (fn v as Var _ => (fn vs => v ins vs) | _ => I) t []);
   10.11  
   10.12  fun test_args _ [] = true
   10.13    | test_args is (Bound i :: ts) =
    11.1 --- a/src/Pure/pure_thy.ML	Wed Jul 13 10:48:21 2005 +0200
    11.2 +++ b/src/Pure/pure_thy.ML	Wed Jul 13 11:16:34 2005 +0200
    11.3 @@ -394,8 +394,8 @@
    11.4  fun forall_elim_vars_aux strip_vars i th =
    11.5    let
    11.6      val {thy, tpairs, prop, ...} = Thm.rep_thm th;
    11.7 -    fun add_used t used = (used, t) |> Term.foldl_aterms
    11.8 -      (fn (xs, Var ((x, j), _)) => if i = j then x ins_string xs else xs | (xs, _) => xs);
    11.9 +    val add_used = Term.fold_aterms
   11.10 +      (fn Var ((x, j), _) => if i = j then curry (op ins_string) x else I | _ => I);
   11.11      val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
   11.12      val vars = strip_vars prop;
   11.13      val cvars = (Term.variantlist (map #1 vars, used), vars)
    12.1 --- a/src/Pure/term.ML	Wed Jul 13 10:48:21 2005 +0200
    12.2 +++ b/src/Pure/term.ML	Wed Jul 13 11:16:34 2005 +0200
    12.3 @@ -157,10 +157,10 @@
    12.4    val term_frees: term -> term list
    12.5    val variant_abs: string * typ * term -> string * term
    12.6    val rename_wrt_term: term -> (string * typ) list -> (string * typ) list
    12.7 -  val foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a
    12.8 -  val foldl_aterms: ('a * term -> 'a) -> 'a * term -> 'a
    12.9 -  val foldl_term_types: (term -> 'a * typ -> 'a) -> 'a * term -> 'a
   12.10 -  val foldl_types: ('a * typ -> 'a) -> 'a * term -> 'a
   12.11 +  val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   12.12 +  val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   12.13 +  val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   12.14 +  val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
   12.15    val add_term_names: term * string list -> string list
   12.16    val add_term_varnames: indexname list * term -> indexname list
   12.17    val term_varnames: term -> indexname list
   12.18 @@ -191,8 +191,8 @@
   12.19    val map_typ: (string -> string) -> (string -> string) -> typ -> typ
   12.20    val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
   12.21    val dest_abs: string * typ * term -> string * term
   12.22 -  val add_tvarsT: (indexname * sort) list * typ -> (indexname * sort) list
   12.23 -  val add_tvars: (indexname * sort) list * term -> (indexname * sort) list
   12.24 +  val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   12.25 +  val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   12.26    val add_vars: (indexname * typ) list * term -> (indexname * typ) list
   12.27    val add_frees: (string * typ) list * term -> (string * typ) list
   12.28    val dummy_patternN: string
   12.29 @@ -1188,32 +1188,45 @@
   12.30  (* left-ro-right traversal *)
   12.31  
   12.32  (*foldl atoms of type*)
   12.33 -fun foldl_atyps f (x, Type (_, Ts)) = Library.foldl (foldl_atyps f) (x, Ts)
   12.34 -  | foldl_atyps f x_atom = f x_atom;
   12.35 +fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   12.36 +  | fold_atyps f T = f T
   12.37  
   12.38  (*foldl atoms of term*)
   12.39 -fun foldl_aterms f (x, t $ u) = foldl_aterms f (foldl_aterms f (x, t), u)
   12.40 -  | foldl_aterms f (x, Abs (_, _, t)) = foldl_aterms f (x, t)
   12.41 -  | foldl_aterms f x_atom = f x_atom;
   12.42 +fun fold_aterms f (t $ u) = (fold_aterms f u) o (fold_aterms f t)
   12.43 +  | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   12.44 +  | fold_aterms f t = f t;
   12.45  
   12.46  (*foldl types of term*)
   12.47 -fun foldl_term_types f (x, t as Const (_, T)) = f t (x, T)
   12.48 -  | foldl_term_types f (x, t as Free (_, T)) = f t (x, T)
   12.49 -  | foldl_term_types f (x, t as Var (_, T)) = f t (x, T)
   12.50 -  | foldl_term_types f (x, Bound _) = x
   12.51 -  | foldl_term_types f (x, t as Abs (_, T, b)) = foldl_term_types f (f t (x, T), b)
   12.52 -  | foldl_term_types f (x, t $ u) = foldl_term_types f (foldl_term_types f (x, t), u);
   12.53 +fun fold_term_types f (t as Const (_, T)) = f t T
   12.54 +  | fold_term_types f (t as Free (_, T)) = f t T
   12.55 +  | fold_term_types f (t as Var (_, T)) = f t T
   12.56 +  | fold_term_types f (Bound _) = I
   12.57 +  | fold_term_types f (t as Abs (_, T, b)) = (fold_term_types f b) o (f t T)
   12.58 +  | fold_term_types f (t $ u) = (fold_term_types f u) o (fold_term_types f t);
   12.59  
   12.60 -fun foldl_types f = foldl_term_types (fn _ => f);
   12.61 +fun fold_types f = fold_term_types (fn _ => f);
   12.62  
   12.63  (*collect variables*)
   12.64 -val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
   12.65 -val add_tvars = foldl_types add_tvarsT;
   12.66 -val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
   12.67 -val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
   12.68 +val add_tvarsT =
   12.69 +  let fun add_tvarsT' (TVar v) = insert (op =) v
   12.70 +         | add_tvarsT' _ = I
   12.71 +  in fold_atyps add_tvarsT' end;
   12.72 +val add_tvars = fold_types add_tvarsT;
   12.73 +val add_vars =
   12.74 +  let fun add_vars' (Var v) = insert (op =) v
   12.75 +         | add_vars' _ = I
   12.76 +  in uncurry (fold_aterms add_vars') o swap end;
   12.77 +val add_frees =
   12.78 +  let fun add_frees' (Free v) = insert (op =) v
   12.79 +         | add_frees' _ = I
   12.80 +  in uncurry (fold_aterms add_frees') o swap end;
   12.81  
   12.82  (*collect variable names*)
   12.83 -val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);
   12.84 +val add_term_varnames =
   12.85 +  let fun add_term_varnames' (Var (x, _)) xs = ins_ix (x, xs)
   12.86 +         | add_term_varnames' _ xs = xs
   12.87 +  in uncurry (fold_aterms add_term_varnames') o swap end;
   12.88 +  
   12.89  fun term_varnames t = add_term_varnames ([], t);
   12.90  
   12.91  
   12.92 @@ -1258,7 +1271,7 @@
   12.93    | is_dummy_pattern _ = false;
   12.94  
   12.95  fun no_dummy_patterns tm =
   12.96 -  if not (foldl_aterms (fn (b, t) => b orelse is_dummy_pattern t) (false, tm)) then tm
   12.97 +  if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   12.98    else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
   12.99  
  12.100  fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =