# HG changeset patch # User wenzelm # Date 1180648056 -7200 # Node ID 07ba6b58b3d2f75a84191df181721f3a835bed3c # Parent 3004310c95b153298b63dc7e1b4240aa22b86c80 simplified/unified list fold; diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Provers/classical.ML --- 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); diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/General/seq.ML --- 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); diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Isar/context_rules.ML --- 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 ); diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Isar/locale.ML --- 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); diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Isar/method.ML --- 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) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Proof/extraction.ML --- 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)) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Proof/proof_rewrite_rules.ML --- 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' diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Proof/reconstruct.ML --- 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) = diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/Tools/nbe_eval.ML --- 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 --------------------- *) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/codegen.ML --- 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 ("", (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 diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/drule.ML --- 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 diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/meta_simplifier.ML --- 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' => diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/net.ML --- 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 **) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/proofterm.ML --- 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') => diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/search.ML --- 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 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) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/tactic.ML --- 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 = diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/tctical.ML --- 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 diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/term.ML --- 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; diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/thm.ML --- 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 ***) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/type.ML --- 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!*) diff -r 3004310c95b1 -r 07ba6b58b3d2 src/Pure/unify.ML --- 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 =