src/Tools/auto_solve.ML
author huffman
Mon Apr 27 07:26:17 2009 -0700 (2009-04-27)
changeset 31007 7c871a9cf6f4
parent 30825 14d24e1fe594
parent 30980 fe0855471964
child 32740 9dd0a2f83429
permissions -rw-r--r--
merged
     1 (*  Title:      Tools/auto_solve.ML
     2     Author:     Timothy Bourke and Gerwin Klein, NICTA
     3 
     4 Check whether a newly stated theorem can be solved directly by an
     5 existing theorem.  Duplicate lemmas can be detected in this way.
     6 
     7 The implementation is based in part on Berghofer and Haftmann's
     8 quickcheck.ML.  It relies critically on the FindTheorems solves
     9 feature.
    10 *)
    11 
    12 signature AUTO_SOLVE =
    13 sig
    14   val auto : bool ref
    15   val auto_time_limit : int ref
    16   val limit : int ref
    17 end;
    18 
    19 structure AutoSolve : AUTO_SOLVE =
    20 struct
    21 
    22 (* preferences *)
    23 
    24 val auto = ref false;
    25 val auto_time_limit = ref 2500;
    26 val limit = ref 5;
    27 
    28 val _ =
    29   ProofGeneralPgip.add_preference Preferences.category_tracing
    30   (setmp auto true (fn () =>
    31     Preferences.bool_pref auto
    32       "auto-solve"
    33       "Try to solve newly declared lemmas with existing theorems.") ());
    34 
    35 val _ =
    36   ProofGeneralPgip.add_preference Preferences.category_tracing
    37     (Preferences.nat_pref auto_time_limit
    38       "auto-solve-time-limit"
    39       "Time limit for seeking automatic solutions (in milliseconds).");
    40 
    41 
    42 (* hook *)
    43 
    44 val _ = Context.>> (Specification.add_theorem_hook (fn int => fn state =>
    45   let
    46     val ctxt = Proof.context_of state;
    47 
    48     val crits = [(true, FindTheorems.Solves)];
    49     fun find g = snd (FindTheorems.find_theorems ctxt (SOME g) (SOME (! limit)) false crits);
    50 
    51     fun prt_result (goal, results) =
    52       let
    53         val msg =
    54           (case goal of
    55             NONE => "The current goal"
    56           | SOME sg => Syntax.string_of_term ctxt (Thm.term_of sg));
    57       in
    58         Pretty.big_list
    59           (msg ^ " could be solved directly with:")
    60           (map (FindTheorems.pretty_thm ctxt) results)
    61       end;
    62 
    63     fun seek_against_goal () =
    64       (case try Proof.get_goal state of
    65         NONE => NONE
    66       | SOME (_, (_, goal)) =>
    67           let
    68             val subgoals = Conjunction.dest_conjunctions (Thm.cprem_of goal 1);
    69             val rs =
    70               if length subgoals = 1
    71               then [(NONE, find goal)]
    72               else map (fn sg => (SOME sg, find (Goal.init sg))) subgoals;
    73             val results = filter_out (null o snd) rs;
    74           in if null results then NONE else SOME results end);
    75 
    76     fun go () =
    77       let
    78         val res =
    79           TimeLimit.timeLimit (Time.fromMilliseconds (! auto_time_limit))
    80             (try seek_against_goal) ();
    81       in
    82         (case res of
    83           SOME (SOME results) =>
    84             state |> Proof.goal_message
    85               (fn () => Pretty.chunks
    86                 [Pretty.str "",
    87                   Pretty.markup Markup.hilite
    88                     (separate (Pretty.brk 0) (map prt_result results))])
    89         | _ => state)
    90       end handle TimeLimit.TimeOut => (warning "AutoSolve: timeout."; state);
    91   in
    92     if int andalso ! auto andalso not (! Toplevel.quiet)
    93     then go ()
    94     else state
    95   end));
    96 
    97 end;
    98 
    99 val auto_solve = AutoSolve.auto;
   100 val auto_solve_time_limit = AutoSolve.auto_time_limit;
   101