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
```