diff -r 1b3115d1a8df -r 8d8c70b41bab src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Thu Mar 03 09:22:35 2005 +0100 +++ b/src/Pure/meta_simplifier.ML Thu Mar 03 12:43:01 2005 +0100 @@ -402,7 +402,7 @@ all its Vars? Better: a dynamic check each time a rule is applied. *) fun rewrite_rule_extra_vars prems elhs erhs = - not (term_varnames erhs subset foldl add_term_varnames (term_varnames elhs, prems)) + not (term_varnames erhs subset Library.foldl add_term_varnames (term_varnames elhs, prems)) orelse not (term_tvars erhs subset (term_tvars elhs union List.concat (map term_tvars prems))); @@ -487,16 +487,16 @@ end; fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) = - flat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms); + List.concat (map (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms); fun orient_comb_simps comb mk_rrule (ss, thms) = let val rews = extract_rews (ss, thms); - val rrules = flat (map mk_rrule rews); - in foldl comb (ss, rrules) end; + val rrules = List.concat (map mk_rrule rews); + in Library.foldl comb (ss, rrules) end; fun extract_safe_rrules (ss, thm) = - flat (map (orient_rrule ss) (extract_rews (ss, [thm]))); + List.concat (map (orient_rrule ss) (extract_rews (ss, [thm]))); (*add rewrite rules explicitly; do not reorient!*) fun ss addsimps thms = @@ -551,7 +551,7 @@ val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm)) handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); (*val lhs = Pattern.eta_contract lhs;*) - val a = the (cong_name (head_of (term_of lhs))) handle Option => + val a = valOf (cong_name (head_of (term_of lhs))) handle Option => raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm); val (alist, weak) = congs; val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm})) @@ -565,11 +565,11 @@ val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm); (*val lhs = Pattern.eta_contract lhs;*) - val a = the (cong_name (head_of lhs)) handle Option => + val a = valOf (cong_name (head_of lhs)) handle Option => raise SIMPLIFIER ("Congruence must start with a constant", thm); val (alist, _) = congs; - val alist2 = filter (fn (x, _) => x <> a) alist; - val weak2 = alist2 |> mapfilter (fn (a, {thm, ...}) => + val alist2 = List.filter (fn (x, _) => x <> a) alist; + val weak2 = alist2 |> List.mapPartial (fn (a, {thm, ...}) => if is_full_cong thm then NONE else SOME a); in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); @@ -577,8 +577,8 @@ in -val (op addeqcongs) = foldl add_cong; -val (op deleqcongs) = foldl del_cong; +val (op addeqcongs) = Library.foldl add_cong; +val (op deleqcongs) = Library.foldl del_cong; fun ss addcongs congs = ss addeqcongs map (mk_cong ss) congs; fun ss delcongs congs = ss deleqcongs map (mk_cong ss) congs; @@ -607,8 +607,8 @@ in -val (op addsimprocs) = foldl (fn (ss, Simproc procs) => foldl add_proc (ss, procs)); -val (op delsimprocs) = foldl (fn (ss, Simproc procs) => foldl del_proc (ss, procs)); +val (op addsimprocs) = Library.foldl (fn (ss, Simproc procs) => Library.foldl add_proc (ss, procs)); +val (op delsimprocs) = Library.foldl (fn (ss, Simproc procs) => Library.foldl del_proc (ss, procs)); end; @@ -966,7 +966,7 @@ may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) (let val thm = congc (prover ss, sign, maxidx) cong t0; - val t = if_none (apsome rhs_of thm) t0; + val t = getOpt (Option.map rhs_of thm, t0); val (cl, cr) = Thm.dest_comb t val dVar = Var(("", 0), dummyT) val skel = @@ -993,7 +993,7 @@ in (extract_safe_rrules (ss, asm), SOME asm) end and add_rrules (rrss, asms) ss = - foldl (insert_rrule true) (ss, flat rrss) |> add_prems (mapfilter I asms) + Library.foldl (insert_rrule true) (ss, List.concat rrss) |> add_prems (List.mapPartial I asms) and disch r (prem, eq) = let @@ -1018,12 +1018,12 @@ let val ss' = add_rrules (rev rrss, rev asms) ss; val concl' = - Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl); - val dprem = apsome (curry (disch false) prem) + Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl)); + val dprem = Option.map (curry (disch false) prem) in case rewritec (prover, sign, maxidx) ss' concl' of NONE => rebuild prems concl' rrss asms ss (dprem eq) - | SOME (eq', _) => transitive2 (foldl (disch false o swap) - (the (transitive3 (dprem eq) eq'), prems)) + | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap) + (valOf (transitive3 (dprem eq) eq'), prems)) (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss) end @@ -1036,8 +1036,8 @@ end and mut_impc [] concl [] [] prems' rrss' asms' eqns ss changed k = - transitive1 (foldl (fn (eq2, (eq1, prem)) => transitive1 eq1 - (apsome (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems')) + transitive1 (Library.foldl (fn (eq2, (eq1, prem)) => transitive1 eq1 + (Option.map (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems')) (if changed > 0 then mut_impc (rev prems') concl (rev rrss') (rev asms') [] [] [] [] ss ~1 changed @@ -1055,20 +1055,20 @@ let val prem' = rhs_of eqn; val tprems = map term_of prems; - val i = 1 + foldl Int.max (~1, map (fn p => + val i = 1 + Library.foldl Int.max (~1, map (fn p => find_index_eq 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) - (take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies - (drop (i, prems), concl))))) :: eqns) ss (length prems') ~1 + (rrs' :: rrss') (asm' :: asms') (SOME (Library.foldr (disch true) + (Library.take (i, prems), Drule.imp_cong' eqn (reflexive (Drule.list_implies + (Library.drop (i, prems), concl))))) :: eqns) ss (length prems') ~1 end (*legacy code - only for backwards compatibility*) and nonmut_impc ct ss = let val (prem, conc) = dest_implies ct; val thm1 = if simprem then botc skel0 ss prem else NONE; - val prem1 = if_none (apsome rhs_of thm1) prem; + val prem1 = getOpt (Option.map rhs_of thm1, prem); val ss1 = if not useprem then ss else add_rrules (apsnd single (apfst single (rules_of_prem ss prem1))) ss in (case botc skel0 ss1 conc of @@ -1169,7 +1169,7 @@ let val Simpset (_, {solvers = (unsafe_solvers, _), ...}) = ss; val tacf = solve_all_tac unsafe_solvers; - fun prover s th = apsome #1 (Seq.pull (tacf s th)); + fun prover s th = Option.map #1 (Seq.pull (tacf s th)); in rew mode prover ss thm end; val simp_thm = simp rewrite_thm;