superficial tuning;
authorwenzelm
Tue Mar 31 20:40:25 2009 +0200 (2009-03-31)
changeset 308228aac4b974280
parent 30821 7d6d1f9a0b41
child 30823 eb99b9134f2e
superficial tuning;
src/Pure/Tools/find_theorems.ML
src/Tools/auto_solve.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Tue Mar 31 14:10:46 2009 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Mar 31 20:40:25 2009 +0200
     1.3 @@ -271,15 +271,17 @@
     1.4        prod_ord int_ord int_ord ((p1, s1), (p0, s0));
     1.5    in map_filter eval_filters thms |> sort thm_ord |> map #2 end;
     1.6  
     1.7 -fun lazy_filter filters = let
     1.8 +fun lazy_filter filters =
     1.9 +  let
    1.10      fun lazy_match thms = Seq.make (fn () => first_match thms)
    1.11  
    1.12      and first_match [] = NONE
    1.13 -      | first_match (thm::thms) =
    1.14 -          case app_filters thm (SOME (0, 0), NONE, filters) of
    1.15 +      | first_match (thm :: thms) =
    1.16 +          (case app_filters thm (SOME (0, 0), NONE, filters) of
    1.17              NONE => first_match thms
    1.18 -          | SOME (_, t) => SOME (t, lazy_match thms);
    1.19 +          | SOME (_, t) => SOME (t, lazy_match thms));
    1.20    in lazy_match end;
    1.21 +
    1.22  end;
    1.23  
    1.24  
    1.25 @@ -304,9 +306,9 @@
    1.26      fun rem_c rev_seen [] = rev rev_seen
    1.27        | rem_c rev_seen [x] = rem_c (x :: rev_seen) []
    1.28        | rem_c rev_seen ((x as ((n, t), _)) :: (y as ((n', t'), _)) :: xs) =
    1.29 -        if Thm.eq_thm_prop (t, t')
    1.30 -        then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
    1.31 -        else rem_c (x :: rev_seen) (y :: xs)
    1.32 +          if Thm.eq_thm_prop (t, t')
    1.33 +          then rem_c rev_seen ((if nicer n n' then x else y) :: xs)
    1.34 +          else rem_c (x :: rev_seen) (y :: xs)
    1.35    in rem_c [] xs end;
    1.36  
    1.37  in
    1.38 @@ -346,9 +348,10 @@
    1.39  
    1.40  fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.41    let
    1.42 -    val assms = ProofContext.get_fact ctxt (Facts.named "local.assms")
    1.43 -                handle ERROR _ => [];
    1.44 -    val add_prems = Seq.hd o (TRY (Method.insert_tac assms 1));
    1.45 +    val assms =
    1.46 +      ProofContext.get_fact ctxt (Facts.named "local.assms")
    1.47 +        handle ERROR _ => [];
    1.48 +    val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
    1.49      val opt_goal' = Option.map add_prems opt_goal;
    1.50  
    1.51      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.52 @@ -370,7 +373,7 @@
    1.53      val find =
    1.54        if rem_dups orelse is_none opt_limit
    1.55        then find_all
    1.56 -      else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters
    1.57 +      else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
    1.58  
    1.59    in find (all_facts_of ctxt) end;
    1.60  
    1.61 @@ -388,12 +391,13 @@
    1.62      val returned = length thms;
    1.63      
    1.64      val tally_msg =
    1.65 -      case foundo of
    1.66 +      (case foundo of
    1.67          NONE => "displaying " ^ string_of_int returned ^ " theorems"
    1.68 -      | SOME found => "found " ^ string_of_int found ^ " theorems" ^
    1.69 -                      (if returned < found
    1.70 -                       then " (" ^ string_of_int returned ^ " displayed)"
    1.71 -                       else "");
    1.72 +      | SOME found =>
    1.73 +          "found " ^ string_of_int found ^ " theorems" ^
    1.74 +            (if returned < found
    1.75 +             then " (" ^ string_of_int returned ^ " displayed)"
    1.76 +             else ""));
    1.77  
    1.78      val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
    1.79    in
    1.80 @@ -411,11 +415,11 @@
    1.81  
    1.82  fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
    1.83    Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.84 -  let
    1.85 -    val proof_state = Toplevel.enter_proof_body state;
    1.86 -    val ctxt = Proof.context_of proof_state;
    1.87 -    val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
    1.88 -  in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    1.89 +    let
    1.90 +      val proof_state = Toplevel.enter_proof_body state;
    1.91 +      val ctxt = Proof.context_of proof_state;
    1.92 +      val opt_goal = try Proof.get_goal proof_state |> Option.map (#2 o #2);
    1.93 +    in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
    1.94  
    1.95  local
    1.96  
     2.1 --- a/src/Tools/auto_solve.ML	Tue Mar 31 14:10:46 2009 +0200
     2.2 +++ b/src/Tools/auto_solve.ML	Tue Mar 31 20:40:25 2009 +0200
     2.3 @@ -36,51 +36,55 @@
     2.4          handle TERM _ => t::conj_to_list ts;
     2.5  
     2.6      val crits = [(true, FindTheorems.Solves)];
     2.7 -    fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (!limit)) false crits));
     2.8 -    fun find_cterm g = (SOME g, snd (FindTheorems.find_theorems ctxt
     2.9 -                                      (SOME (Goal.init g)) (SOME (!limit)) false crits));
    2.10 +    fun find g = (NONE, snd (FindTheorems.find_theorems ctxt g (SOME (! limit)) false crits));
    2.11 +    fun find_cterm g =
    2.12 +      (SOME g, snd (FindTheorems.find_theorems ctxt
    2.13 +          (SOME (Goal.init g)) (SOME (! limit)) false crits));
    2.14  
    2.15      fun prt_result (goal, results) =
    2.16        let
    2.17 -        val msg = case goal of
    2.18 -                    NONE => "The current goal"
    2.19 -                  | SOME g => Syntax.string_of_term ctxt (term_of g);
    2.20 +        val msg =
    2.21 +          (case goal of
    2.22 +            NONE => "The current goal"
    2.23 +          | SOME g => Syntax.string_of_term ctxt (Thm.term_of g));
    2.24        in
    2.25 -        Pretty.big_list (msg ^ " could be solved directly with:")
    2.26 -                        (map (FindTheorems.pretty_thm ctxt) results)
    2.27 +        Pretty.big_list
    2.28 +          (msg ^ " could be solved directly with:")
    2.29 +          (map (FindTheorems.pretty_thm ctxt) results)
    2.30        end;
    2.31  
    2.32      fun seek_against_goal () =
    2.33        let
    2.34          val goal = try Proof.get_goal state
    2.35 -                   |> Option.map (#2 o #2);
    2.36 +          |> Option.map (#2 o #2);
    2.37  
    2.38          val goals = goal
    2.39 -                    |> Option.map (fn g => cprem_of g 1)
    2.40 -                    |> the_list
    2.41 -                    |> conj_to_list;
    2.42 +          |> Option.map (fn g => cprem_of g 1)
    2.43 +          |> the_list
    2.44 +          |> conj_to_list;
    2.45  
    2.46 -        val rs = if length goals = 1
    2.47 -                 then [find goal]
    2.48 -                 else map find_cterm goals;
    2.49 -        val frs = filter_out (null o snd) rs;
    2.50 +        val rs =
    2.51 +          if length goals = 1
    2.52 +          then [find goal]
    2.53 +          else map find_cterm goals;
    2.54 +        val results = filter_out (null o snd) rs;
    2.55  
    2.56 -      in if null frs then NONE else SOME frs end;
    2.57 +      in if null results then NONE else SOME results end;
    2.58  
    2.59      fun go () =
    2.60        let
    2.61 -        val res = TimeLimit.timeLimit
    2.62 -                    (Time.fromMilliseconds (! auto_time_limit))
    2.63 -                    (try seek_against_goal) ();
    2.64 +        val res =
    2.65 +          TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    2.66 +            (try seek_against_goal) ();
    2.67        in
    2.68 -        case Option.join res of
    2.69 -          NONE => state
    2.70 -        | SOME results => (Proof.goal_message
    2.71 -                            (fn () => Pretty.chunks [Pretty.str "",
    2.72 -                              Pretty.markup Markup.hilite
    2.73 -                              (Library.separate (Pretty.brk 0)
    2.74 -                                                (map prt_result results))])
    2.75 -                              state)
    2.76 +        (case res of
    2.77 +          SOME (SOME results) =>
    2.78 +            state |> Proof.goal_message
    2.79 +              (fn () => Pretty.chunks
    2.80 +                [Pretty.str "",
    2.81 +                  Pretty.markup Markup.hilite
    2.82 +                    (separate (Pretty.brk 0) (map prt_result results))])
    2.83 +        | NONE => state)
    2.84        end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    2.85    in
    2.86      if int andalso ! auto andalso not (! Toplevel.quiet)