--- a/src/Provers/classical.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Provers/classical.ML Thu May 31 23:47:36 2007 +0200
@@ -326,7 +326,7 @@
fun tag_brls' _ _ [] = []
| tag_brls' w k (brl::brls) = ((w, k), brl) :: tag_brls' w (k + 1) brls;
-fun insert_tagged_list kbrls netpr = foldr Tactic.insert_tagged_brl netpr kbrls;
+fun insert_tagged_list rls = fold_rev Tactic.insert_tagged_brl rls;
(*Insert into netpair that already has nI intr rules and nE elim rules.
Count the intr rules double (to account for swapify). Negate to give the
@@ -334,7 +334,7 @@
fun insert (nI, nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
fun insert' w (nI, nE) = insert_tagged_list o tag_brls' w (~(nI + nE)) o joinrules';
-fun delete_tagged_list brls netpr = foldr Tactic.delete_tagged_brl netpr brls;
+fun delete_tagged_list rls = fold_rev Tactic.delete_tagged_brl rls;
fun delete x = delete_tagged_list (joinrules x);
fun delete' x = delete_tagged_list (joinrules' x);
--- a/src/Pure/General/seq.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/General/seq.ML Thu May 31 23:47:36 2007 +0200
@@ -202,8 +202,8 @@
fun op APPEND (f, g) x =
append (f x) (make (fn () => pull (g x)));
-fun EVERY fs = foldr THEN succeed fs;
-fun FIRST fs = foldr ORELSE fail fs;
+fun EVERY fs = fold_rev (curry op THEN) fs succeed;
+fun FIRST fs = fold_rev (curry op ORELSE) fs fail;
fun TRY f = ORELSE (f, succeed);
--- a/src/Pure/Isar/context_rules.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Isar/context_rules.ML Thu May 31 23:47:36 2007 +0200
@@ -80,13 +80,13 @@
fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
make_rules (next - 1) ((w, ((i, b), th)) :: rules)
- (nth_map i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
+ (nth_map i (insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
end;
fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
let
fun eq_th (_, (_, th')) = Thm.eq_thm_prop (th, th');
- fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair;
+ fun del b netpair = delete_tagged_brl (b, th) netpair handle Net.DELETE => netpair;
in
if not (exists eq_th rules) then rs
else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
@@ -107,7 +107,7 @@
k1 = k2 andalso Thm.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
val netpairs = fold (fn (n, (w, ((i, b), th))) =>
- nth_map i (curry insert_tagged_brl ((w, n), (b, th))))
+ nth_map i (insert_tagged_brl ((w, n), (b, th))))
(next upto ~1 ~~ rules) empty_netpairs;
in make_rules (next - 1) rules netpairs wrappers end
);
--- a/src/Pure/Isar/locale.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Isar/locale.ML Thu May 31 23:47:36 2007 +0200
@@ -664,7 +664,7 @@
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
fun inst_parms (i, ps) =
- foldr Term.add_typ_tfrees [] (map_filter snd ps)
+ List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
|> map_filter (fn (a, S) =>
let val T = Envir.norm_type unifier' (TVar ((a, i), S))
in if T = TFree (a, S) then NONE else SOME (a, T) end)
@@ -1707,7 +1707,7 @@
val env = Term.add_term_free_names (body, []);
val xs = filter (member (op =) env o #1) parms;
val Ts = map #2 xs;
- val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees [] Ts)
+ val extraTs = (Term.term_tfrees body \\ List.foldr Term.add_typ_tfrees [] Ts)
|> Library.sort_wrt #1 |> map TFree;
val predT = map Term.itselfT extraTs ---> Ts ---> bodyT;
@@ -1855,8 +1855,8 @@
map_filter (fn ((id, Assumed axs), elems) => SOME (id, elems) | _ => NONE);
val imports = prep_expr thy raw_imports;
- val extraTs = foldr Term.add_term_tfrees [] exts' \\
- foldr Term.add_typ_tfrees [] (map snd parms);
+ val extraTs = List.foldr Term.add_term_tfrees [] exts' \\
+ List.foldr Term.add_typ_tfrees [] (map snd parms);
val _ = if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^ quote bname);
--- a/src/Pure/Isar/method.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Isar/method.ML Thu May 31 23:47:36 2007 +0200
@@ -216,7 +216,8 @@
local
fun asm_tac ths =
- foldr (op APPEND') (K no_tac) (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths);
+ fold_rev (curry op APPEND')
+ (map (fn th => Tactic.rtac th THEN_ALL_NEW assume_tac) ths) (K no_tac);
fun cond_rtac cond rule = SUBGOAL (fn (prop, i) =>
if cond (Logic.strip_assums_concl prop)
--- a/src/Pure/Proof/extraction.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Proof/extraction.ML Thu May 31 23:47:36 2007 +0200
@@ -84,7 +84,7 @@
fun merge_rules
({next, rs = rs1, net} : rules) ({next = next2, rs = rs2, ...} : rules) =
- foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
+ List.foldr add_rule {next = next, rs = rs1, net = net} (subtract (op =) rs1 rs2);
fun condrew thy rules procs =
let
@@ -136,7 +136,7 @@
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, prf_abstract_over t prf) end;
-val mkabs = foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
+val mkabs = List.foldr (fn (v, t) => Abs ("x", fastype_of v, abstract_over (v, t)));
fun strip_abs 0 t = t
| strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
@@ -145,7 +145,7 @@
fun prf_subst_TVars tye =
map_proof_terms (subst_TVars tye) (typ_subst_TVars tye);
-fun relevant_vars types prop = foldr (fn
+fun relevant_vars types prop = List.foldr (fn
(Var ((a, i), T), vs) => (case strip_type T of
(_, Type (s, _)) => if member (op =) types s then a :: vs else vs
| _ => vs)
@@ -237,7 +237,7 @@
defs, expand, prep} = ExtractionData.get thy;
in
ExtractionData.put
- {realizes_eqns = foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
+ {realizes_eqns = List.foldr add_rule realizes_eqns (map (prep_eq thy) eqns),
typeof_eqns = typeof_eqns, types = types, realizers = realizers,
defs = defs, expand = expand, prep = prep} thy
end
@@ -255,7 +255,7 @@
in
ExtractionData.put
{realizes_eqns = realizes_eqns, realizers = realizers,
- typeof_eqns = foldr add_rule typeof_eqns eqns',
+ typeof_eqns = List.foldr add_rule typeof_eqns eqns',
types = types, defs = defs, expand = expand, prep = prep} thy
end
@@ -324,7 +324,7 @@
(procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
(Const ("realizes", T --> propT --> propT) $
(if T = nullT then t else list_comb (t, vars')) $ prop);
- val r = foldr forall_intr r' (map (get_var_type r') vars);
+ val r = List.foldr forall_intr r' (map (get_var_type r') vars);
val prf = Reconstruct.reconstruct_proof thy' r (rd s2);
in (name, (vs, (t, prf))) end
end;
@@ -474,7 +474,7 @@
end
else (vs', tye)
- in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
+ in List.foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
fun find' s = map snd o List.filter (equal s o fst)
@@ -569,7 +569,7 @@
val (defs'', corr_prf) =
corr (d + 1) defs' vs' [] [] [] prf' prf' NONE;
val corr_prop = Reconstruct.prop_of corr_prf;
- val corr_prf' = foldr forall_intr_prf
+ val corr_prf' = List.foldr forall_intr_prf
(proof_combt
(PThm (corr_name name vs', corr_prf, corr_prop,
SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
@@ -678,7 +678,7 @@
PAxm (cname ^ "_def", eqn,
SOME (map TVar (term_tvars eqn))))) %% corr_prf;
val corr_prop = Reconstruct.prop_of corr_prf';
- val corr_prf'' = foldr forall_intr_prf
+ val corr_prf'' = List.foldr forall_intr_prf
(proof_combt
(PThm (corr_name s vs', corr_prf', corr_prop,
SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu May 31 23:47:36 2007 +0200
@@ -231,7 +231,7 @@
val tvars = term_tvars prop;
val (_, rhs) = Logic.dest_equals prop;
val rhs' = Term.betapplys (subst_TVars (map fst tvars ~~ Ts)
- (foldr (fn p => Abs ("", dummyT, abstract_over p)) rhs vs),
+ (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
map the ts);
in
change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs'
--- a/src/Pure/Proof/reconstruct.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Proof/reconstruct.ML Thu May 31 23:47:36 2007 +0200
@@ -26,19 +26,19 @@
fun vars_of t = rev (fold_aterms
(fn v as Var _ => insert (op =) v | _ => I) t []);
-fun forall_intr (t, prop) =
+fun forall_intr t prop =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in all T $ Abs (a, T, abstract_over (t, prop)) end;
-fun forall_intr_vfs prop = foldr forall_intr prop
- (vars_of prop @ sort Term.term_ord (term_frees prop));
+fun forall_intr_vfs prop = fold_rev forall_intr
+ (vars_of prop @ sort Term.term_ord (term_frees prop)) prop;
-fun forall_intr_prf (t, prf) =
+fun forall_intr_prf t prf =
let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
in Abst (a, SOME T, prf_abstract_over t prf) end;
-fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf prf
- (vars_of prop @ sort Term.term_ord (term_frees prop));
+fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_prf
+ (vars_of prop @ sort Term.term_ord (term_frees prop)) prf;
fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
(Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
@@ -49,7 +49,7 @@
(**** generate constraints for proof term ****)
-fun mk_var env Ts T =
+fun mk_var env Ts T =
let val (env', v) = Envir.genvar "a" (env, rev Ts ---> T)
in (env', list_comb (v, map Bound (length Ts - 1 downto 0))) end;
@@ -74,7 +74,7 @@
fun infer_type thy (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs
(t as Const (s, T)) = if T = dummyT then (case Sign.const_type thy s of
NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
- | SOME T =>
+ | SOME T =>
let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T)
in (Const (s, T'), T', vTs,
Envir.Envir {maxidx = maxidx + 1, asol = asol, iTs = iTs})
@@ -156,7 +156,7 @@
fun head_norm (prop, prf, cnstrts, env, vTs) =
(Envir.head_norm env prop, prf, cnstrts, env, vTs);
-
+
fun mk_cnstrts env _ Hs vTs (PBound i) = (List.nth (Hs, i), PBound i, [], env, vTs)
| mk_cnstrts env Ts Hs vTs (Abst (s, opT, cprf)) =
let
@@ -338,10 +338,10 @@
fun expand_proof thy thms prf =
let
- fun expand maxidx prfs (AbsP (s, t, prf)) =
+ fun expand maxidx prfs (AbsP (s, t, prf)) =
let val (maxidx', prfs', prf') = expand maxidx prfs prf
in (maxidx', prfs', AbsP (s, t, prf')) end
- | expand maxidx prfs (Abst (s, T, prf)) =
+ | expand maxidx prfs (Abst (s, T, prf)) =
let val (maxidx', prfs', prf') = expand maxidx prfs prf
in (maxidx', prfs', Abst (s, T, prf')) end
| expand maxidx prfs (prf1 %% prf2) =
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu May 31 23:47:36 2007 +0200
@@ -594,7 +594,7 @@
x::_::_ => SOME x (* String.find? *)
| _ => NONE
fun subthys_of_thy s =
- foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
+ List.foldl (fn (NONE,xs) => xs | (SOME x,xs) => insert op= x xs) []
(map thy_prefix (thms_of_thy s))
fun subthms_of_thy thy =
(case thy_prefix thy of
--- a/src/Pure/Tools/nbe_eval.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/Tools/nbe_eval.ML Thu May 31 23:47:36 2007 +0200
@@ -56,7 +56,7 @@
| string_of_nterm(AbsN(n,t)) =
"(Abs " ^ string_of_int n ^ " " ^ string_of_nterm t ^ ")";
-fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
+fun apps t args = fold_rev (fn y => fn x => A(x,y)) args t;
(* ------------------------------ The semantical universe --------------------- *)
--- a/src/Pure/codegen.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/codegen.ML Thu May 31 23:47:36 2007 +0200
@@ -359,7 +359,7 @@
fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p;
val code_attr =
- Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser
+ Attrib.syntax (Scan.peek (fn context => List.foldr op || Scan.fail (map mk_parser
(#attrs (CodegenData.get (Context.theory_of context))))));
val _ = Context.add_setup
@@ -542,7 +542,7 @@
fun rename_terms ts =
let
- val names = foldr add_term_names
+ val names = List.foldr add_term_names
(map (fst o fst) (rev (fold Term.add_vars ts []))) ts;
val reserved = filter ML_Syntax.is_reserved names;
val (illegal, alt_names) = split_list (map_filter (fn s =>
@@ -684,7 +684,7 @@
val (Ts, _) = strip_type (fastype_of t);
val j = i - length ts
in
- foldr (fn (T, t) => Abs ("x", T, t))
+ List.foldr (fn (T, t) => Abs ("x", T, t))
(list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
end;
@@ -862,15 +862,15 @@
if module = "" then
let
val modules = distinct (op =) (map (#2 o snd) code);
- val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
- (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
+ val mod_gr = fold_rev Graph.add_edge_acyclic
(maps (fn (s, (_, module, _)) => map (pair module)
(filter_out (equal module) (map (#2 o Graph.get_node gr)
- (Graph.imm_succs gr s)))) code);
+ (Graph.imm_succs gr s)))) code)
+ (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
val modules' =
rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
in
- foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
+ List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms)
(map (rpair "") modules') code
end handle Graph.CYCLES (cs :: _) =>
error ("Cyclic dependency of modules:\n" ^ commas cs ^
@@ -887,7 +887,7 @@
val graphs = get_modules thy;
val defs = mk_deftab thy;
val gr = new_node ("<Top>", (NONE, module, ""))
- (foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
+ (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) =>
(Graph.merge (fn ((_, module, _), (_, module', _)) =>
module = module') (gr, gr'),
(merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr
--- a/src/Pure/drule.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/drule.ML Thu May 31 23:47:36 2007 +0200
@@ -401,7 +401,7 @@
let val fth = Thm.freezeT th
val {prop, tpairs, thy, ...} = rep_thm fth
in
- case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+ case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
[] => (fth, fn i => fn x => x) (*No vars: nothing to do!*)
| vars =>
let fun newName (Var(ix,_)) = (ix, gensym (string_of_indexname ix))
@@ -423,13 +423,13 @@
let val fth = Thm.freezeT th
val {prop, tpairs, thy, ...} = rep_thm fth
in
- case foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
+ case List.foldr add_term_vars [] (prop :: Thm.terms_of_tpairs tpairs) of
[] => (fth, fn x => x)
| vars =>
let fun newName (Var(ix,_), (pairs,used)) =
let val v = Name.variant used (string_of_indexname ix)
in ((ix,v)::pairs, v::used) end;
- val (alist, _) = foldr newName ([], Library.foldr add_term_names
+ val (alist, _) = List.foldr newName ([], Library.foldr add_term_names
(prop :: Thm.terms_of_tpairs tpairs, [])) vars
fun mk_inst (Var(v,T)) =
(cterm_of thy (Var(v,T)),
@@ -810,7 +810,7 @@
in
fun cterm_instantiate [] th = th
| cterm_instantiate ctpairs0 th =
- let val (thy,tye,_) = foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
+ let val (thy,tye,_) = List.foldr add_types (Thm.theory_of_thm th, Vartab.empty, 0) ctpairs0
fun instT(ct,cu) =
let val inst = cterm_of thy o Term.map_types (Envir.norm_type tye) o term_of
in (inst ct, inst cu) end
--- a/src/Pure/meta_simplifier.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/meta_simplifier.ML Thu May 31 23:47:36 2007 +0200
@@ -1107,7 +1107,7 @@
and add_rrules (rrss, asms) ss =
(fold o fold) insert_rrule rrss ss |> add_prems (map_filter I asms)
- and disch r (prem, eq) =
+ and disch r prem eq =
let
val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of eq);
val eq' = implies_elim (Thm.instantiate
@@ -1131,11 +1131,11 @@
val ss' = add_rrules (rev rrss, rev asms) ss;
val concl' =
Drule.mk_implies (prem, the_default concl (Option.map Thm.rhs_of eq));
- val dprem = Option.map (curry (disch false) prem)
+ val dprem = Option.map (disch false prem)
in case rewritec (prover, thy, maxidx) ss' concl' of
NONE => rebuild prems concl' rrss asms ss (dprem eq)
- | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
- (the (transitive3 (dprem eq) eq'), prems))
+ | SOME (eq', _) => transitive2 (fold (disch false)
+ prems (the (transitive3 (dprem eq) eq')))
(mut_impc0 (rev prems) (Thm.rhs_of eq') (rev rrss) (rev asms) ss)
end
@@ -1149,7 +1149,7 @@
and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k =
transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1
- (Option.map (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems'))
+ (Option.map (disch false prem) eq2)) (NONE, eqns ~~ prems'))
(if changed > 0 then
mut_impc (rev prems') concl (rev rrss') (rev asms')
[] [] [] [] ss ~1 changed
@@ -1171,9 +1171,10 @@
find_index (fn q => q aconv p) tprems) (#hyps (rep_thm eqn)));
val (rrs', asm') = rules_of_prem ss prem'
in mut_impc prems concl rrss asms (prem' :: prems')
- (rrs' :: rrss') (asm' :: asms') (SOME (foldr (disch true)
+ (rrs' :: rrss') (asm' :: asms') (SOME (fold_rev (disch true)
+ (Library.take (i, prems))
(Drule.imp_cong_rule eqn (reflexive (Drule.list_implies
- (Library.drop (i, prems), concl)))) (Library.take (i, prems))) :: eqns)
+ (Library.drop (i, prems), concl))))) :: eqns)
ss (length prems') ~1
end
@@ -1189,7 +1190,7 @@
NONE => NONE
| SOME thm1' => SOME (Drule.imp_cong_rule thm1' (reflexive conc)))
| SOME thm2 =>
- let val thm2' = disch false (prem1, thm2)
+ let val thm2' = disch false prem1 thm2
in (case thm1 of
NONE => SOME thm2'
| SOME thm1' =>
--- a/src/Pure/net.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/net.ML Thu May 31 23:47:36 2007 +0200
@@ -158,9 +158,9 @@
(*Skipping a term in a net. Recursively skip 2 levels if a combination*)
-fun net_skip (Leaf _, nets) = nets
- | net_skip (Net{comb,var,atoms}, nets) =
- foldr net_skip (Symtab.fold (cons o #2) atoms (var::nets)) (net_skip (comb,[]));
+fun net_skip (Leaf _) nets = nets
+ | net_skip (Net{comb,var,atoms}) nets =
+ fold_rev net_skip (net_skip comb []) (Symtab.fold (cons o #2) atoms (var::nets));
(** Matching and Unification **)
@@ -175,11 +175,11 @@
Abs or Var in object: if "unif", regarded as wildcard,
else matches only a variable in net.
*)
-fun matching unif t (net,nets) =
+fun matching unif t net nets =
let fun rands _ (Leaf _, nets) = nets
| rands t (Net{comb,atoms,...}, nets) =
case t of
- f$t => foldr (matching unif t) nets (rands f (comb,[]))
+ f$t => fold_rev (matching unif t) (rands f (comb,[])) nets
| Const(c,_) => look1 (atoms, c) nets
| Free(c,_) => look1 (atoms, c) nets
| Bound i => look1 (atoms, Name.bound i) nets
@@ -189,11 +189,11 @@
Leaf _ => nets
| Net{var,...} =>
case head_of t of
- Var _ => if unif then net_skip (net,nets)
+ Var _ => if unif then net_skip net nets
else var::nets (*only matches Var in net*)
(*If "unif" then a var instantiation in the abstraction could allow
an eta-reduction, so regard the abstraction as a wildcard.*)
- | Abs _ => if unif then net_skip (net,nets)
+ | Abs _ => if unif then net_skip net nets
else var::nets (*only a Var can match*)
| _ => rands t (net, var::nets) (*var could match also*)
end;
@@ -202,11 +202,11 @@
(*return items whose key could match t, WHICH MUST BE BETA-ETA NORMAL*)
fun match_term net t =
- extract_leaves (matching false t (net,[]));
+ extract_leaves (matching false t net []);
(*return items whose key could unify with t*)
fun unify_term net t =
- extract_leaves (matching true t (net,[]));
+ extract_leaves (matching true t net []);
(** operations on nets **)
--- a/src/Pure/proofterm.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/proofterm.ML Thu May 31 23:47:36 2007 +0200
@@ -250,7 +250,7 @@
(PThm (_, prf', _, _), _) => prf'
| _ => prf);
-val mk_Abst = foldr (fn ((s, T:typ), prf) => Abst (s, NONE, prf));
+val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
fun mk_AbsP (i, prf) = funpow i (fn prf => AbsP ("H", NONE, prf)) prf;
fun apsome f NONE = raise SAME
@@ -621,7 +621,7 @@
let
val used = it_term_types add_typ_tfree_names (t, [])
and tvars = map #1 (it_term_types add_typ_tvars (t, []));
- val (alist, _) = foldr new_name ([], used) tvars;
+ val (alist, _) = List.foldr new_name ([], used) tvars;
in
(case alist of
[] => prf (*nothing to do!*)
@@ -643,9 +643,9 @@
val j = length Bs;
in
mk_AbsP (j+1, proof_combP (prf, map PBound
- (j downto 1) @ [mk_Abst (mk_AbsP (i,
+ (j downto 1) @ [mk_Abst params (mk_AbsP (i,
proof_combP (proof_combt (PBound i, map Bound ((length params - 1) downto 0)),
- map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m)))))) params]))
+ map PBound (((i-m-1) downto 0) @ ((i-1) downto (i-m))))))]))
end;
@@ -700,7 +700,7 @@
val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
val k = length ps;
- fun mk_app (b, (i, j, prf)) =
+ fun mk_app b (i, j, prf) =
if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
fun lift Us bs i j (Const ("==>", _) $ A $ B) =
@@ -708,7 +708,7 @@
| lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
| lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
- map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
+ map (fn k => (#3 (fold_rev mk_app bs (i-1, j-1, PBound k))))
(i + k - 1 downto i));
in
mk_AbsP (k, lift [] [] 0 0 Bi)
@@ -1200,7 +1200,7 @@
map SOME (sort Term.term_ord (term_frees prop));
val opt_prf = if ! proofs = 2 then
#4 (shrink_proof thy [] 0 (rewrite_prf fst (ProofData.get thy)
- (foldr (uncurry implies_intr_proof) prf hyps)))
+ (fold_rev implies_intr_proof hyps prf)))
else MinProof (mk_min_proof prf ([], [], []));
val head = (case strip_combt (fst (strip_combP prf)) of
(PThm (old_name, prf', prop', NONE), args') =>
--- a/src/Pure/search.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/search.ML Thu May 31 23:47:36 2007 +0200
@@ -1,6 +1,6 @@
-(* Title: Pure/search.ML
+(* Title: Pure/search.ML
ID: $Id$
- Author: Lawrence C Paulson and Norbert Voelker
+ Author: Lawrence C Paulson and Norbert Voelker
Search tacticals.
*)
@@ -9,33 +9,33 @@
signature SEARCH =
sig
- val DEEPEN : int*int -> (int->int->tactic) -> int -> int -> tactic
+ val DEEPEN : int*int -> (int->int->tactic) -> int -> int -> tactic
- val THEN_MAYBE : tactic * tactic -> tactic
- val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
+ val THEN_MAYBE : tactic * tactic -> tactic
+ val THEN_MAYBE' : ('a -> tactic) * ('a -> tactic) -> ('a -> tactic)
- val trace_DEPTH_FIRST : bool ref
- val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
- val DEPTH_SOLVE : tactic -> tactic
- val DEPTH_SOLVE_1 : tactic -> tactic
- val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic
- val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic
+ val trace_DEPTH_FIRST : bool ref
+ val DEPTH_FIRST : (thm -> bool) -> tactic -> tactic
+ val DEPTH_SOLVE : tactic -> tactic
+ val DEPTH_SOLVE_1 : tactic -> tactic
+ val ITER_DEEPEN : (thm->bool) -> (int->tactic) -> tactic
+ val THEN_ITER_DEEPEN : tactic -> (thm->bool) -> (int->tactic) -> tactic
val iter_deepen_limit : int ref
- val has_fewer_prems : int -> thm -> bool
- val IF_UNSOLVED : tactic -> tactic
- val SOLVE : tactic -> tactic
+ val has_fewer_prems : int -> thm -> bool
+ val IF_UNSOLVED : tactic -> tactic
+ val SOLVE : tactic -> tactic
val DETERM_UNTIL_SOLVED: tactic -> tactic
- val trace_BEST_FIRST : bool ref
- val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
- val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
- -> tactic
- val trace_ASTAR : bool ref
- val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic
- val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic
- -> tactic
- val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
- val QUIET_BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
+ val trace_BEST_FIRST : bool ref
+ val BEST_FIRST : (thm -> bool) * (thm -> int) -> tactic -> tactic
+ val THEN_BEST_FIRST : tactic -> (thm->bool) * (thm->int) -> tactic
+ -> tactic
+ val trace_ASTAR : bool ref
+ val ASTAR : (thm -> bool) * (int->thm->int) -> tactic -> tactic
+ val THEN_ASTAR : tactic -> (thm->bool) * (int->thm->int) -> tactic
+ -> tactic
+ val BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
+ val QUIET_BREADTH_FIRST : (thm -> bool) -> tactic -> tactic
end;
@@ -48,7 +48,7 @@
(Term.term_ord o Library.pairself (#prop o Thm.rep_thm)));
-structure Search : SEARCH =
+structure Search : SEARCH =
struct
(**** Depth-first search ****)
@@ -57,17 +57,17 @@
(*Searches until "satp" reports proof tree as satisfied.
Suppresses duplicate solutions to minimize search space.*)
-fun DEPTH_FIRST satp tac =
+fun DEPTH_FIRST satp tac =
let val tac = tracify trace_DEPTH_FIRST tac
fun depth used [] = NONE
| depth used (q::qs) =
- case Seq.pull q of
- NONE => depth used qs
- | SOME(st,stq) =>
- if satp st andalso not (member Thm.eq_thm used st)
- then SOME(st, Seq.make
- (fn()=> depth (st::used) (stq::qs)))
- else depth used (tac st :: stq :: qs)
+ case Seq.pull q of
+ NONE => depth used qs
+ | SOME(st,stq) =>
+ if satp st andalso not (member Thm.eq_thm used st)
+ then SOME(st, Seq.make
+ (fn()=> depth (st::used) (stq::qs)))
+ else depth used (tac st :: stq :: qs)
in traced_tac (fn st => depth [] [Seq.single st]) end;
@@ -86,7 +86,7 @@
(*Execute tac1, but only execute tac2 if there are at least as many subgoals
as before. This ensures that tac2 is only applied to an outcome of tac1.*)
-fun (tac1 THEN_MAYBE tac2) st =
+fun (tac1 THEN_MAYBE tac2) st =
(tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st;
fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x;
@@ -95,7 +95,7 @@
If no subgoals then it must fail! *)
fun DEPTH_SOLVE_1 tac st = st |>
(case nprems_of st of
- 0 => no_tac
+ 0 => no_tac
| n => DEPTH_FIRST (has_fewer_prems n) tac);
(*Uses depth-first search to solve ALL subgoals*)
@@ -114,21 +114,21 @@
may perform >1 inference*)
(*Pruning of rigid ancestor to prevent backtracking*)
-fun prune (new as (k', np':int, rgd', stq), qs) =
+fun prune (new as (k', np':int, rgd', stq), qs) =
let fun prune_aux (qs, []) = new::qs
| prune_aux (qs, (k,np,rgd,q)::rqs) =
- if np'+1 = np andalso rgd then
- (if !trace_DEPTH_FIRST then
- tracing ("Pruning " ^
- string_of_int (1+length rqs) ^ " levels")
- else ();
- (*Use OLD k: zero-cost solution; see Stickel, p 365*)
- (k, np', rgd', stq) :: qs)
- else prune_aux ((k,np,rgd,q)::qs, rqs)
+ if np'+1 = np andalso rgd then
+ (if !trace_DEPTH_FIRST then
+ tracing ("Pruning " ^
+ string_of_int (1+length rqs) ^ " levels")
+ else ();
+ (*Use OLD k: zero-cost solution; see Stickel, p 365*)
+ (k, np', rgd', stq) :: qs)
+ else prune_aux ((k,np,rgd,q)::qs, rqs)
fun take ([], rqs) = ([], rqs)
- | take (arg as ((k,np,rgd,stq)::qs, rqs)) =
- if np' < np then take (qs, (k,np,rgd,stq)::rqs)
- else arg
+ | take (arg as ((k,np,rgd,stq)::qs, rqs)) =
+ if np' < np then take (qs, (k,np,rgd,stq)::rqs)
+ else arg
in prune_aux (take (qs, [])) end;
@@ -140,49 +140,49 @@
The solution sequence is redundant: the cutoff heuristic makes it impossible
to suppress solutions arising from earlier searches, as the accumulated cost
(k) can be wrong.*)
-fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
+fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
let val countr = ref 0
and tf = tracify trace_DEPTH_FIRST (tac1 1)
and qs0 = tac0 st
(*bnd = depth bound; inc = estimate of increment required next*)
- fun depth (bnd,inc) [] =
+ fun depth (bnd,inc) [] =
if bnd > !iter_deepen_limit then
- (tracing (string_of_int (!countr) ^
- " inferences so far. Giving up at " ^ string_of_int bnd);
- NONE)
+ (tracing (string_of_int (!countr) ^
+ " inferences so far. Giving up at " ^ string_of_int bnd);
+ NONE)
else
- (tracing (string_of_int (!countr) ^
- " inferences so far. Searching to depth " ^
- string_of_int bnd);
- (*larger increments make it run slower for the hard problems*)
- depth (bnd+inc, 10)) [(0, 1, false, qs0)]
+ (tracing (string_of_int (!countr) ^
+ " inferences so far. Searching to depth " ^
+ string_of_int bnd);
+ (*larger increments make it run slower for the hard problems*)
+ depth (bnd+inc, 10)) [(0, 1, false, qs0)]
| depth (bnd,inc) ((k,np,rgd,q)::qs) =
- if k>=bnd then depth (bnd,inc) qs
+ if k>=bnd then depth (bnd,inc) qs
else
- case (countr := !countr+1;
- if !trace_DEPTH_FIRST then
- tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
- else ();
- Seq.pull q) of
- NONE => depth (bnd,inc) qs
- | SOME(st,stq) =>
- if satp st (*solution!*)
- then SOME(st, Seq.make
- (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
+ case (countr := !countr+1;
+ if !trace_DEPTH_FIRST then
+ tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
+ else ();
+ Seq.pull q) of
+ NONE => depth (bnd,inc) qs
+ | SOME(st,stq) =>
+ if satp st (*solution!*)
+ then SOME(st, Seq.make
+ (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs)))
- else
+ else
let val np' = nprems_of st
- (*rgd' calculation assumes tactic operates on subgoal 1*)
+ (*rgd' calculation assumes tactic operates on subgoal 1*)
val rgd' = not (has_vars (hd (prems_of st)))
val k' = k+np'-np+1 (*difference in # of subgoals, +1*)
- in if k'+np' >= bnd
- then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
- else if np' < np (*solved a subgoal; prune rigid ancestors*)
- then depth (bnd,inc)
- (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
- else depth (bnd,inc) ((k', np', rgd', tf st) ::
- (k,np,rgd,stq) :: qs)
- end
+ in if k'+np' >= bnd
+ then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs
+ else if np' < np (*solved a subgoal; prune rigid ancestors*)
+ then depth (bnd,inc)
+ (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs))
+ else depth (bnd,inc) ((k', np', rgd', tf st) ::
+ (k,np,rgd,stq) :: qs)
+ end
in depth (0,5) [] end);
val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
@@ -190,16 +190,16 @@
(*Simple iterative deepening tactical. It merely "deepens" any search tactic
using increment "inc" up to limit "lim". *)
-fun DEEPEN (inc,lim) tacf m i =
- let fun dpn m st =
+fun DEEPEN (inc,lim) tacf m i =
+ let fun dpn m st =
st |> (if has_fewer_prems i st then no_tac
- else if m>lim then
- (warning "Search depth limit exceeded: giving up";
- no_tac)
- else (warning ("Search depth = " ^ string_of_int m);
- tacf m i ORELSE dpn (m+inc)))
+ else if m>lim then
+ (warning "Search depth limit exceeded: giving up";
+ no_tac)
+ else (warning ("Search depth = " ^ string_of_int m);
+ tacf m i ORELSE dpn (m+inc)))
in dpn m end;
-
+
(*** Best-first search ***)
val trace_BEST_FIRST = ref false;
@@ -209,7 +209,7 @@
| some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
(*Check for and delete duplicate proof states*)
-fun deleteAllMin prf heap =
+fun deleteAllMin prf heap =
if ThmHeap.is_empty heap then heap
else if Thm.eq_thm (prf, #2 (ThmHeap.min heap))
then deleteAllMin prf (ThmHeap.delete_min heap)
@@ -218,23 +218,22 @@
(*Best-first search for a state that satisfies satp (incl initial state)
Function sizef estimates size of problem remaining (smaller means better).
tactic tac0 sets up the initial priority queue, while tac1 searches it. *)
-fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
+fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 =
let val tac = tracify trace_BEST_FIRST tac1
fun pairsize th = (sizef th, th);
fun bfs (news,nprf_heap) =
- (case List.partition satp news of
- ([],nonsats) => next(foldr ThmHeap.insert
- nprf_heap (map pairsize nonsats))
- | (sats,_) => some_of_list sats)
+ (case List.partition satp news of
+ ([],nonsats) => next(fold_rev ThmHeap.insert (map pairsize nonsats) nprf_heap)
+ | (sats,_) => some_of_list sats)
and next nprf_heap =
if ThmHeap.is_empty nprf_heap then NONE
- else
- let val (n,prf) = ThmHeap.min nprf_heap
- in if !trace_BEST_FIRST
- then tracing("state size = " ^ string_of_int n)
+ else
+ let val (n,prf) = ThmHeap.min nprf_heap
+ in if !trace_BEST_FIRST
+ then tracing("state size = " ^ string_of_int n)
else ();
- bfs (Seq.list_of (tac prf),
- deleteAllMin prf (ThmHeap.delete_min nprf_heap))
+ bfs (Seq.list_of (tac prf),
+ deleteAllMin prf (ThmHeap.delete_min nprf_heap))
end
fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty)
in traced_tac btac end;
@@ -242,32 +241,32 @@
(*Ordinary best-first search, with no initial tactic*)
val BEST_FIRST = THEN_BEST_FIRST all_tac;
-(*Breadth-first search to satisfy satpred (including initial state)
+(*Breadth-first search to satisfy satpred (including initial state)
SLOW -- SHOULD NOT USE APPEND!*)
-fun gen_BREADTH_FIRST message satpred (tac:tactic) =
+fun gen_BREADTH_FIRST message satpred (tac:tactic) =
let val tacf = Seq.list_of o tac;
fun bfs prfs =
- (case List.partition satpred prfs of
- ([],[]) => []
- | ([],nonsats) =>
- (message("breadth=" ^ string_of_int(length nonsats));
- bfs (maps tacf nonsats))
- | (sats,_) => sats)
+ (case List.partition satpred prfs of
+ ([],[]) => []
+ | ([],nonsats) =>
+ (message("breadth=" ^ string_of_int(length nonsats));
+ bfs (maps tacf nonsats))
+ | (sats,_) => sats)
in (fn st => Seq.of_list (bfs [st])) end;
val BREADTH_FIRST = gen_BREADTH_FIRST tracing;
val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ());
-(* Author: Norbert Voelker, FernUniversitaet Hagen
+(* Author: Norbert Voelker, FernUniversitaet Hagen
Remarks: Implementation of A*-like proof procedure by modification
- of the existing code for BEST_FIRST and best_tac so that the
- current level of search is taken into account.
-*)
+ of the existing code for BEST_FIRST and best_tac so that the
+ current level of search is taken into account.
+*)
(*Insertion into priority queue of states, marked with level *)
fun insert_with_level (lnth: int*int*thm, []) = [lnth]
- | insert_with_level ((l,m,th), (l',n,th')::nths) =
+ | insert_with_level ((l,m,th), (l',n,th')::nths) =
if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths)
else if n=m andalso Thm.eq_thm(th,th')
then (l',n,th')::nths
@@ -277,23 +276,23 @@
fun some_of_list [] = NONE
| some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l));
-val trace_ASTAR = ref false;
+val trace_ASTAR = ref false;
-fun THEN_ASTAR tac0 (satp, costf) tac1 =
- let val tf = tracify trace_ASTAR tac1;
+fun THEN_ASTAR tac0 (satp, costf) tac1 =
+ let val tf = tracify trace_ASTAR tac1;
fun bfs (news,nprfs,level) =
let fun cost thm = (level, costf level thm, thm)
in (case List.partition satp news of
- ([],nonsats)
- => next (foldr insert_with_level nprfs (map cost nonsats))
+ ([],nonsats)
+ => next (List.foldr insert_with_level nprfs (map cost nonsats))
| (sats,_) => some_of_list sats)
- end and
+ end and
next [] = NONE
| next ((level,n,prf)::nprfs) =
- (if !trace_ASTAR
+ (if !trace_ASTAR
then tracing("level = " ^ string_of_int level ^
- " cost = " ^ string_of_int n ^
- " queue length =" ^ string_of_int (length nprfs))
+ " cost = " ^ string_of_int n ^
+ " queue length =" ^ string_of_int (length nprfs))
else ();
bfs (Seq.list_of (tf prf), nprfs,level+1))
fun tf st = bfs (Seq.list_of (tac0 st), [], 0)
--- a/src/Pure/tactic.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/tactic.ML Thu May 31 23:47:36 2007 +0200
@@ -51,11 +51,11 @@
val forward_tac : thm list -> int -> tactic
val forw_inst_tac : (string*string)list -> thm -> int -> tactic
val ftac : thm -> int ->tactic
- val insert_tagged_brl : ('a * (bool * thm)) *
- (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
+ val insert_tagged_brl : 'a * (bool * thm) ->
+ ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
- val delete_tagged_brl : (bool * thm) *
- (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
+ val delete_tagged_brl : bool * thm ->
+ ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
val lessb : (bool * thm) * (bool * thm) -> bool
val lift_inst_rule : thm * int * (string*string)list * thm -> thm
@@ -410,7 +410,7 @@
fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
(*insert one tagged brl into the pair of nets*)
-fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
+fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
if eres then
(case try Thm.major_prem_of th of
SOME prem => (inet, Net.insert_term (K false) (prem, kbrl) enet)
@@ -419,12 +419,12 @@
(*build a pair of nets for biresolution*)
fun build_netpair netpair brls =
- foldr insert_tagged_brl netpair (taglist 1 brls);
+ fold_rev insert_tagged_brl (taglist 1 brls) netpair;
(*delete one kbrl from the pair of nets*)
fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
-fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
+fun delete_tagged_brl (brl as (eres, th)) (inet, enet) =
(if eres then
(case try Thm.major_prem_of th of
SOME prem => (inet, Net.delete_term eq_kbrl (prem, ((), brl)) enet)
@@ -458,12 +458,12 @@
(*** Simpler version for resolve_tac -- only one net, and no hyps ***)
(*insert one tagged rl into the net*)
-fun insert_krl (krl as (k,th), net) =
- Net.insert_term (K false) (concl_of th, krl) net;
+fun insert_krl (krl as (k,th)) =
+ Net.insert_term (K false) (concl_of th, krl);
(*build a net of rules for resolution*)
fun build_net rls =
- foldr insert_krl Net.empty (taglist 1 rls);
+ fold_rev insert_krl (taglist 1 rls) Net.empty;
(*resolution using a net rather than rules; pred supports filt_resolve_tac*)
fun filt_resolution_from_net_tac match pred net =
--- a/src/Pure/tctical.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/tctical.ML Thu May 31 23:47:36 2007 +0200
@@ -177,10 +177,10 @@
fun EVERY1 tacs = EVERY' tacs 1;
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *)
-fun FIRST tacs = foldr (op ORELSE) no_tac tacs;
+fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *)
-fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs;
+fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);
(*Apply first tactic to 1*)
fun FIRST1 tacs = FIRST' tacs 1;
@@ -413,7 +413,7 @@
(*Common code for METAHYPS and metahyps_thms*)
fun metahyps_split_prem prem =
let (*find all vars in the hyps -- should find tvars also!*)
- val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem)
+ val hyps_vars = List.foldr add_term_vars [] (Logic.strip_assums_hyp prem)
val insts = map mk_inst hyps_vars
(*replace the hyps_vars by Frees*)
val prem' = subst_atomic insts prem
@@ -453,7 +453,7 @@
fun relift st =
let val prop = Thm.prop_of st
val subgoal_vars = (*Vars introduced in the subgoals*)
- foldr add_term_vars [] (Logic.strip_imp_prems prop)
+ List.foldr add_term_vars [] (Logic.strip_imp_prems prop)
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, [])
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st
--- a/src/Pure/term.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/term.ML Thu May 31 23:47:36 2007 +0200
@@ -1112,20 +1112,20 @@
| add_term_names (_, bs) = bs;
(*Accumulates the TVars in a type, suppressing duplicates. *)
-fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
+fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
| add_typ_tvars(TFree(_),vs) = vs
| add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
(*Accumulates the TFrees in a type, suppressing duplicates. *)
-fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
+fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
| add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
| add_typ_tfree_names(TVar(_),fs) = fs;
-fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
+fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
| add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
| add_typ_tfrees(TVar(_),fs) = fs;
-fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
+fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
| add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
| add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
--- a/src/Pure/thm.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/thm.ML Thu May 31 23:47:36 2007 +0200
@@ -1150,7 +1150,7 @@
(* Replace all TFrees not fixed or in the hyps by new TVars *)
fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
let
- val tfrees = foldr add_term_tfrees fixed hyps;
+ val tfrees = List.foldr add_term_tfrees fixed hyps;
val prop1 = attach_tpairs tpairs prop;
val (al, prop2) = Type.varify tfrees prop1;
val (ts, prop3) = Logic.strip_prems (length tpairs, [], prop2);
@@ -1430,7 +1430,7 @@
(*Function to rename bounds/unknowns in the argument, lifted over B*)
fun rename_bvars(dpairs, tpairs, B) =
- rename_bvs(foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
+ rename_bvs(List.foldr Term.match_bvars [] dpairs, dpairs, tpairs, B);
(*** RESOLUTION ***)
--- a/src/Pure/type.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/type.ML Thu May 31 23:47:36 2007 +0200
@@ -264,7 +264,7 @@
let
val used = add_typ_tfree_names (T, [])
and tvars = map #1 (add_typ_tvars (T, []));
- val (alist, _) = foldr new_name ([], used) tvars;
+ val (alist, _) = List.foldr new_name ([], used) tvars;
in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
val freeze_type = #1 o freeze_thaw_type;
@@ -273,7 +273,7 @@
let
val used = it_term_types add_typ_tfree_names (t, [])
and tvars = map #1 (it_term_types add_typ_tvars (t, []));
- val (alist, _) = foldr new_name ([], used) tvars;
+ val (alist, _) = List.foldr new_name ([], used) tvars;
in
(case alist of
[] => (t, fn x => x) (*nothing to do!*)
--- a/src/Pure/unify.ML Thu May 31 23:02:16 2007 +0200
+++ b/src/Pure/unify.ML Thu May 31 23:47:36 2007 +0200
@@ -280,7 +280,7 @@
Clever would be to re-do just the affected dpairs*)
fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
let val all as (env',flexflex,flexrigid) =
- foldr (SIMPL0 thy) (env,[],[]) dpairs;
+ List.foldr (SIMPL0 thy) (env,[],[]) dpairs;
val dps = flexrigid@flexflex
in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
then SIMPL thy (env',dps) else all
@@ -471,7 +471,7 @@
val (Ts,U) = strip_type env T
and js = length ts - 1 downto 0
val args = sort (make_ord arg_less)
- (foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
+ (List.foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
val ts' = map (#t) args
in
if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
@@ -504,7 +504,7 @@
then (bnos, (a,T)::newbinder) (*needed by both: keep*)
else (j::bnos, newbinder); (*remove*)
val indices = 0 upto (length rbinder - 1);
- val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
+ val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
val (env', t') = clean_term banned (env, t);
val (env'',u') = clean_term banned (env',u)
in (ff_assign thy (env'', rbin', t', u'), tpairs)
@@ -558,7 +558,7 @@
then print_dpairs thy "Enter SIMPL" (env,dpairs) else ();
SIMPL thy (env,dpairs))
in case flexrigid of
- [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq)
+ [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
| dp::frigid' =>
if tdepth > !search_bound then
(warning "Unification bound exceeded"; Seq.pull reseq)
@@ -607,7 +607,7 @@
(*Smash all flex-flexpairs. Should allow selection of pairs by a predicate?*)
fun smash_flexflex (env,tpairs) : Envir.env =
- foldr smash_flexflex1 env tpairs;
+ List.foldr smash_flexflex1 env tpairs;
(*Returns unifiers with no remaining disagreement pairs*)
fun smash_unifiers thy tus env =