diff -r 6f43714517ee -r 08c8dad8e399 src/Pure/meta_simplifier.ML --- a/src/Pure/meta_simplifier.ML Fri Feb 11 18:51:00 2005 +0100 +++ b/src/Pure/meta_simplifier.ML Sun Feb 13 17:15:14 2005 +0100 @@ -303,8 +303,8 @@ val basic_mk_rews: mk_rews = {mk = fn th => if can Logic.dest_equals (Thm.concl_of th) then [th] else [], mk_cong = I, - mk_sym = Some o Drule.symmetric_fun, - mk_eq_True = K None}; + mk_sym = SOME o Drule.symmetric_fun, + mk_eq_True = K NONE}; in @@ -445,8 +445,8 @@ fun mk_eq_True (Simpset (_, {mk_rews = {mk_eq_True, ...}, ...})) (thm, name) = (case mk_eq_True thm of - None => [] - | Some eq_True => + NONE => [] + | SOME eq_True => let val (_, _, lhs, elhs, _, _) = decomp_simp eq_True in [{thm = eq_True, name = name, lhs = lhs, elhs = elhs, perm = false}] end); @@ -478,8 +478,8 @@ else let val Simpset (_, {mk_rews = {mk_sym, ...}, ...}) = ss in (case mk_sym thm of - None => [] - | Some thm' => + NONE => [] + | SOME thm' => let val (_, _, lhs', elhs', rhs', _) = decomp_simp thm' in rrule_eq_True (thm', name, lhs', elhs', rhs', ss, thm) end) end @@ -516,9 +516,9 @@ (* congs *) -fun cong_name (Const (a, _)) = Some a - | cong_name (Free (a, _)) = Some ("Free: " ^ a) - | cong_name _ = None; +fun cong_name (Const (a, _)) = SOME a + | cong_name (Free (a, _)) = SOME ("Free: " ^ a) + | cong_name _ = NONE; local @@ -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 Library.OPTION => + val a = the (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,12 +565,12 @@ 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 Library.OPTION => + val a = the (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, ...}) => - if is_full_cong thm then None else Some a); + if is_full_cong thm then NONE else SOME a); in ((alist2, weak2), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end); fun mk_cong (Simpset (_, {mk_rews = {mk_cong = f, ...}, ...})) = f; @@ -710,12 +710,12 @@ let val thm'' = transitive thm (transitive (symmetric (Drule.beta_eta_conversion (lhs_of thm'))) thm') - in if msg then trace_thm "SUCCEEDED" thm' else (); Some thm'' end + in if msg then trace_thm "SUCCEEDED" thm' else (); SOME thm'' end handle THM _ => let val {sign, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in trace_thm "Proved wrong thm (Check subgoaler?)" thm'; trace_term false "Should have proved:" sign prop0; - None + NONE end; @@ -764,12 +764,12 @@ val Simpset ({depth = depth', ...}, _) = ss'; in if depth' > ! simp_depth_limit - then (warning "simp_depth_limit exceeded - giving up"; None) + then (warning "simp_depth_limit exceeded - giving up"; NONE) else (if depth' mod 10 = 0 then warning ("Simplification depth " ^ string_of_int depth') else (); - Some ss') + SOME ss') end; (* @@ -803,34 +803,34 @@ in if perm andalso not (termless (rhs', lhs')) then (trace_named_thm "Cannot apply permutative rewrite rule" (thm, name); - trace_thm "Term does not become smaller:" thm'; None) + trace_thm "Term does not become smaller:" thm'; NONE) else (trace_named_thm "Applying instance of rewrite rule" (thm, name); if unconditional then (trace_thm "Rewriting:" thm'; let val lr = Logic.dest_equals prop; - val Some thm'' = check_conv false eta_thm thm' - in Some (thm'', uncond_skel (congs, lr)) end) + val SOME thm'' = check_conv false eta_thm thm' + in SOME (thm'', uncond_skel (congs, lr)) end) else (trace_thm "Trying to rewrite:" thm'; case incr_depth ss of - None => (trace_thm "FAILED - reached depth limit" thm'; None) - | Some ss' => + NONE => (trace_thm "FAILED - reached depth limit" thm'; NONE) + | SOME ss' => (case prover ss' thm' of - None => (trace_thm "FAILED" thm'; None) - | Some thm2 => + NONE => (trace_thm "FAILED" thm'; NONE) + | SOME thm2 => (case check_conv true eta_thm thm2 of - None => None | - Some thm2' => + NONE => NONE | + SOME thm2' => let val concl = Logic.strip_imp_concl prop val lr = Logic.dest_equals concl - in Some (thm2', cond_skel (congs, lr)) end)))) + in SOME (thm2', cond_skel (congs, lr)) end)))) end - fun rews [] = None + fun rews [] = NONE | rews (rrule :: rrules) = - let val opt = rew rrule handle Pattern.MATCH => None - in case opt of None => rews rrules | some => some end; + let val opt = rew rrule handle Pattern.MATCH => NONE + in case opt of NONE => rews rrules | some => some end; fun sort_rrules rrs = let fun is_simple({thm, ...}:rrule) = case Thm.prop_of thm of @@ -842,25 +842,25 @@ else sort rrs (re1,rr::re2) in sort rrs ([],[]) end - fun proc_rews [] = None + fun proc_rews [] = NONE | proc_rews (Proc {name, proc, lhs, ...} :: ps) = if Pattern.matches tsigt (Thm.term_of lhs, Thm.term_of t) then (debug_term false ("Trying procedure " ^ quote name ^ " on:") signt eta_t; case transform_failure (curry SIMPROC_FAIL name) (fn () => proc signt ss eta_t) () of - None => (debug false "FAILED"; proc_rews ps) - | Some raw_thm => + NONE => (debug false "FAILED"; proc_rews ps) + | SOME raw_thm => (trace_thm ("Procedure " ^ quote name ^ " produced rewrite rule:") raw_thm; (case rews (mk_procrule raw_thm) of - None => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^ + NONE => (trace_cterm true ("IGNORED result of simproc " ^ quote name ^ " -- does not match") t; proc_rews ps) | some => some))) else proc_rews ps; in case eta_t of - Abs _ $ _ => Some (transitive eta_thm + Abs _ $ _ => SOME (transitive eta_thm (beta_conversion false eta_t'), skel0) | _ => (case rews (sort_rrules (Net.match_term rules eta_t)) of - None => proc_rews (Net.match_term procs eta_t) + NONE => proc_rews (Net.match_term procs eta_t) | some => some) end; @@ -876,67 +876,67 @@ is handled when congc is called *) val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm); val unit = trace_thm "Applying congruence rule:" thm'; - fun err (msg, thm) = (trace_thm msg thm; None) + fun err (msg, thm) = (trace_thm msg thm; NONE) in case prover thm' of - None => err ("Congruence proof failed. Could not prove", thm') - | Some thm2 => (case check_conv true (Drule.beta_eta_conversion t) thm2 of - None => err ("Congruence proof failed. Should not have proved", thm2) - | Some thm2' => + NONE => err ("Congruence proof failed. Could not prove", thm') + | SOME thm2 => (case check_conv true (Drule.beta_eta_conversion t) thm2 of + NONE => err ("Congruence proof failed. Should not have proved", thm2) + | SOME thm2' => if op aconv (pairself term_of (dest_equals (cprop_of thm2'))) - then None else Some thm2') + then NONE else SOME thm2') end; val (cA, (cB, cC)) = apsnd dest_equals (dest_implies (hd (cprems_of Drule.imp_cong))); -fun transitive1 None None = None - | transitive1 (Some thm1) None = Some thm1 - | transitive1 None (Some thm2) = Some thm2 - | transitive1 (Some thm1) (Some thm2) = Some (transitive thm1 thm2) +fun transitive1 NONE NONE = NONE + | transitive1 (SOME thm1) NONE = SOME thm1 + | transitive1 NONE (SOME thm2) = SOME thm2 + | transitive1 (SOME thm1) (SOME thm2) = SOME (transitive thm1 thm2) -fun transitive2 thm = transitive1 (Some thm); -fun transitive3 thm = transitive1 thm o Some; +fun transitive2 thm = transitive1 (SOME thm); +fun transitive3 thm = transitive1 thm o SOME; fun bottomc ((simprem, useprem, mutsimp), prover, sign, maxidx) = let fun botc skel ss t = - if is_Var skel then None + if is_Var skel then NONE else (case subc skel ss t of - some as Some thm1 => + some as SOME thm1 => (case rewritec (prover, sign, maxidx) ss (rhs_of thm1) of - Some (thm2, skel2) => + SOME (thm2, skel2) => transitive2 (transitive thm1 thm2) (botc skel2 ss (rhs_of thm2)) - | None => some) - | None => + | NONE => some) + | NONE => (case rewritec (prover, sign, maxidx) ss t of - Some (thm2, skel2) => transitive2 thm2 + SOME (thm2, skel2) => transitive2 thm2 (botc skel2 ss (rhs_of thm2)) - | None => None)) + | NONE => NONE)) and try_botc ss t = (case botc skel0 ss t of - Some trec1 => trec1 | None => (reflexive t)) + SOME trec1 => trec1 | NONE => (reflexive t)) and subc skel (ss as Simpset ({bounds, ...}, {congs, ...})) t0 = (case term_of t0 of Abs (a, T, t) => let - val (v, t') = Thm.dest_abs (Some ("." ^ a ^ "." ^ string_of_int bounds)) t0; + val (v, t') = Thm.dest_abs (SOME ("." ^ a ^ "." ^ string_of_int bounds)) t0; val ss' = incr_bounds ss; val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0; in case botc skel' ss' t' of - Some thm => Some (abstract_rule a v thm) - | None => None + SOME thm => SOME (abstract_rule a v thm) + | NONE => NONE end | t $ _ => (case t of Const ("==>", _) $ _ => impc t0 ss | Abs _ => let val thm = beta_conversion false t0 in case subc skel0 ss (rhs_of thm) of - None => Some thm - | Some thm' => Some (transitive thm thm') + NONE => SOME thm + | SOME thm' => SOME (transitive thm thm') end | _ => let fun appc () = @@ -947,21 +947,21 @@ val (ct, cu) = Thm.dest_comb t0 in (case botc tskel ss ct of - Some thm1 => + SOME thm1 => (case botc uskel ss cu of - Some thm2 => Some (combination thm1 thm2) - | None => Some (combination thm1 (reflexive cu))) - | None => + SOME thm2 => SOME (combination thm1 thm2) + | NONE => SOME (combination thm1 (reflexive cu))) + | NONE => (case botc uskel ss cu of - Some thm1 => Some (combination (reflexive ct) thm1) - | None => None)) + SOME thm1 => SOME (combination (reflexive ct) thm1) + | NONE => NONE)) end val (h, ts) = strip_comb t in case cong_name h of - Some a => + SOME a => (case assoc_string (fst congs, a) of - None => appc () - | Some cong => + NONE => appc () + | SOME cong => (*post processing: some partial applications h t1 ... tj, j <= length ts, may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*) (let @@ -972,14 +972,14 @@ val skel = list_comb (h, replicate (length ts) dVar) in case botc skel ss cl of - None => thm - | Some thm' => transitive3 thm + NONE => thm + | SOME thm' => transitive3 thm (combination thm' (reflexive cr)) end handle TERM _ => error "congc result" | Pattern.MATCH => appc ())) | _ => appc () end) - | _ => None) + | _ => NONE) and impc ct ss = if mutsimp then mut_impc0 [] ct [] [] ss else nonmut_impc ct ss @@ -987,10 +987,10 @@ and rules_of_prem ss prem = if maxidx_of_term (term_of prem) <> ~1 then (trace_cterm true - "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], None)) + "Cannot add premise as rewrite rule because it contains (type) unknowns:" prem; ([], NONE)) else let val asm = assume prem - in (extract_safe_rrules (ss, asm), Some asm) end + 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) @@ -1021,8 +1021,8 @@ Drule.mk_implies (prem, if_none (apsome rhs_of eq) concl); val dprem = apsome (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) + NONE => rebuild prems concl' rrss asms ss (dprem eq) + | SOME (eq', _) => transitive2 (foldl (disch false o swap) (the (transitive3 (dprem eq) eq'), prems)) (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss) end @@ -1037,7 +1037,7 @@ 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')) + (apsome (curry (disch false) prem) eq2)) (NONE, eqns ~~ prems')) (if changed > 0 then mut_impc (rev prems') concl (rev rrss') (rev asms') [] [] [] [] ss ~1 changed @@ -1046,12 +1046,12 @@ | mut_impc (prem :: prems) concl (rrs :: rrss) (asm :: asms) prems' rrss' asms' eqns ss changed k = - case (if k = 0 then None else botc skel0 (add_rrules + case (if k = 0 then NONE else botc skel0 (add_rrules (rev rrss' @ rrss, rev asms' @ asms) ss) prem) of - None => mut_impc prems concl rrss asms (prem :: prems') - (rrs :: rrss') (asm :: asms') (None :: eqns) ss changed + NONE => mut_impc prems concl rrss asms (prem :: prems') + (rrs :: rrss') (asm :: asms') (NONE :: eqns) ss changed (if k = 0 then 0 else k - 1) - | Some eqn => + | SOME eqn => let val prem' = rhs_of eqn; val tprems = map term_of prems; @@ -1059,7 +1059,7 @@ 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) + (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 end @@ -1067,20 +1067,20 @@ (*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 thm1 = if simprem then botc skel0 ss prem else NONE; val prem1 = if_none (apsome 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 - None => (case thm1 of - None => None - | Some thm1' => Some (Drule.imp_cong' thm1' (reflexive conc))) - | Some thm2 => + NONE => (case thm1 of + NONE => NONE + | SOME thm1' => SOME (Drule.imp_cong' thm1' (reflexive conc))) + | SOME thm2 => let val thm2' = disch false (prem1, thm2) in (case thm1 of - None => Some thm2' - | Some thm1' => - Some (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2')) + NONE => SOME thm2' + | SOME thm1' => + SOME (transitive (Drule.imp_cong' thm1' (reflexive conc)) thm2')) end) end