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