# HG changeset patch # User wenzelm # Date 1238524825 -7200 # Node ID 8aac4b9742804b5221034c700a8770d801c3c379 # Parent 7d6d1f9a0b41cb6f71792cfee07b73b5d0b0eb82 superficial tuning; diff -r 7d6d1f9a0b41 -r 8aac4b974280 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Tue Mar 31 14:10:46 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Tue Mar 31 20:40:25 2009 +0200 @@ -271,15 +271,17 @@ prod_ord int_ord int_ord ((p1, s1), (p0, s0)); in map_filter eval_filters thms |> sort thm_ord |> map #2 end; -fun lazy_filter filters = let +fun lazy_filter filters = + let fun lazy_match thms = Seq.make (fn () => first_match thms) and first_match [] = NONE - | first_match (thm::thms) = - case app_filters thm (SOME (0, 0), NONE, filters) of + | first_match (thm :: thms) = + (case app_filters thm (SOME (0, 0), NONE, filters) of NONE => first_match thms - | SOME (_, t) => SOME (t, lazy_match thms); + | SOME (_, t) => SOME (t, lazy_match thms)); in lazy_match end; + end; @@ -304,9 +306,9 @@ fun rem_c rev_seen [] = rev rev_seen | rem_c rev_seen [x] = rem_c (x :: rev_seen) [] | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) = - if Thm.eq_thm_prop (t, t') - then rem_c rev_seen ((if nicer n n' then x else y) :: xs) - else rem_c (x :: rev_seen) (y :: xs) + if Thm.eq_thm_prop (t, t') + then rem_c rev_seen ((if nicer n n' then x else y) :: xs) + else rem_c (x :: rev_seen) (y :: xs) in rem_c [] xs end; in @@ -346,9 +348,10 @@ fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria = let - val assms = ProofContext.get_fact ctxt (Facts.named "local.assms") - handle ERROR _ => []; - val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1)); + val assms = + ProofContext.get_fact ctxt (Facts.named "local.assms") + handle ERROR _ => []; + val add_prems = Seq.hd o TRY (Method.insert_tac assms 1); val opt_goal' = Option.map add_prems opt_goal; val criteria = map (apsnd (read_criterion ctxt)) raw_criteria; @@ -370,7 +373,7 @@ val find = if rem_dups orelse is_none opt_limit then find_all - else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters + else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters; in find (all_facts_of ctxt) end; @@ -388,12 +391,13 @@ val returned = length thms; val tally_msg = - case foundo of + (case foundo of NONE => "displaying " ^ string_of_int returned ^ " theorems" - | SOME found => "found " ^ string_of_int found ^ " theorems" ^ - (if returned < found - then " (" ^ string_of_int returned ^ " displayed)" - else ""); + | SOME found => + "found " ^ string_of_int found ^ " theorems" ^ + (if returned < found + then " (" ^ string_of_int returned ^ " displayed)" + else "")); val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs"; in @@ -411,11 +415,11 @@ fun find_theorems_cmd ((opt_lim, rem_dups), spec) = Toplevel.unknown_theory o Toplevel.keep (fn state => - let - val proof_state = Toplevel.enter_proof_body state; - val ctxt = Proof.context_of proof_state; - val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2); - in print_theorems ctxt opt_goal opt_lim rem_dups spec end); + let + val proof_state = Toplevel.enter_proof_body state; + val ctxt = Proof.context_of proof_state; + val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2); + in print_theorems ctxt opt_goal opt_lim rem_dups spec end); local diff -r 7d6d1f9a0b41 -r 8aac4b974280 src/Tools/auto_solve.ML --- a/src/Tools/auto_solve.ML Tue Mar 31 14:10:46 2009 +0200 +++ b/src/Tools/auto_solve.ML Tue Mar 31 20:40:25 2009 +0200 @@ -36,51 +36,55 @@ handle TERM _ => t::conj_to_list ts; val crits = [(true, FindTheorems.Solves)]; - fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits)); - fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt - (SOME (Goal.init g)) (SOME (!limit)) false crits)); + fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (! limit)) false crits)); + fun find_cterm g = + (SOME g, snd (FindTheorems.find_theorems ctxt + (SOME (Goal.init g)) (SOME (! limit)) false crits)); fun prt_result (goal, results) = let - val msg = case goal of - NONE => "The current goal" - | SOME g => Syntax.string_of_term ctxt (term_of g); + val msg = + (case goal of + NONE => "The current goal" + | SOME g => Syntax.string_of_term ctxt (Thm.term_of g)); in - Pretty.big_list (msg ^ " could be solved directly with:") - (map (FindTheorems.pretty_thm ctxt) results) + Pretty.big_list + (msg ^ " could be solved directly with:") + (map (FindTheorems.pretty_thm ctxt) results) end; fun seek_against_goal () = let val goal = try Proof.get_goal state - |> Option.map (#2 o #2); + |> Option.map (#2 o #2); val goals = goal - |> Option.map (fn g => cprem_of g 1) - |> the_list - |> conj_to_list; + |> Option.map (fn g => cprem_of g 1) + |> the_list + |> conj_to_list; - val rs = if length goals = 1 - then [find goal] - else map find_cterm goals; - val frs = filter_out (null o snd) rs; + val rs = + if length goals = 1 + then [find goal] + else map find_cterm goals; + val results = filter_out (null o snd) rs; - in if null frs then NONE else SOME frs end; + in if null results then NONE else SOME results end; fun go () = let - val res = TimeLimit.timeLimit - (Time.fromMilliseconds (! auto_time_limit)) - (try seek_against_goal) (); + val res = + TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit)) + (try seek_against_goal) (); in - case Option.join res of - NONE => state - | SOME results => (Proof.goal_message - (fn () => Pretty.chunks [Pretty.str "", - Pretty.markup Markup.hilite - (Library.separate (Pretty.brk 0) - (map prt_result results))]) - state) + (case res of + SOME (SOME results) => + state |> Proof.goal_message + (fn () => Pretty.chunks + [Pretty.str "", + Pretty.markup Markup.hilite + (separate (Pretty.brk 0) (map prt_result results))]) + | NONE => state) end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state); in if int andalso ! auto andalso not (! Toplevel.quiet)