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