# HG changeset patch
# User blanchet
# Date 1283291003 -7200
# Node ID 162bbbea4e4d690c63539372e6751d518e560d9d
# Parent  ca7ac998bb36ed09063b74e45d59df40ba2d0717
added "expect" feature of Nitpick to Sledgehammer, for regression testing

diff -r ca7ac998bb36 -r 162bbbea4e4d src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 23:42:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Aug 31 23:43:23 2010 +0200
@@ -25,7 +25,8 @@
      theory_relevant: bool option,
      isar_proof: bool,
      isar_shrink_factor: int,
-     timeout: Time.time}
+     timeout: Time.time,
+     expect: string}
   type problem =
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
@@ -93,7 +94,8 @@
    theory_relevant: bool option,
    isar_proof: bool,
    isar_shrink_factor: int,
-   timeout: Time.time}
+   timeout: Time.time,
+   expect: string}
 
 type problem =
   {subgoal: int,
@@ -365,7 +367,7 @@
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
 fun start_prover_thread (params as {blocking, verbose, full_types, timeout,
-                                    ...})
+                                    expect, ...})
                         i n relevance_override minimize_command proof_state
                         atp_name =
   let
@@ -375,23 +377,35 @@
     val prover = get_prover_fun thy atp_name
     val {context = ctxt, facts, goal} = Proof.goal proof_state;
     val desc =
-      "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
-      Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
+      "ATP " ^ quote atp_name ^ " for subgoal " ^ string_of_int i ^ ":" ^
+      (if blocking then
+         ""
+       else
+         "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
     fun run () =
       let
         val problem =
           {subgoal = i, goal = (ctxt, (facts, goal)),
            relevance_override = relevance_override, axioms = NONE}
+        val (outcome_code, message) =
+          prover params (minimize_command atp_name) problem
+          |> (fn {outcome, message, ...} =>
+                 (if is_some outcome then "none" else "some", message))
+          handle ERROR message => ("unknown", "Error: " ^ message ^ "\n")
+               | exn => ("unknown", "Internal error:\n" ^
+                                    ML_Compiler.exn_message exn ^ "\n")
       in
-        prover params (minimize_command atp_name) problem |> #message
-        handle ERROR message => "Error: " ^ message ^ "\n"
-             | exn => "Internal error:\n" ^ ML_Compiler.exn_message exn ^ "\n"
+        if expect = "" orelse outcome_code = expect then
+          ()
+        else if blocking then
+          error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+        else
+          warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
+        message
       end
   in
-    if blocking then
-      priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
-    else
-      Async_Manager.launch das_Tool verbose birth_time death_time desc run
+    if blocking then priority (desc ^ "\n" ^ TimeLimit.timeLimit timeout run ())
+    else Async_Manager.launch das_Tool verbose birth_time death_time desc run
   end
 
 fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
diff -r ca7ac998bb36 -r 162bbbea4e4d src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 31 23:42:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML	Tue Aug 31 23:43:23 2010 +0200
@@ -53,7 +53,7 @@
        atps = atps, full_types = full_types, explicit_apply = explicit_apply,
        relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
        theory_relevant = NONE, isar_proof = isar_proof,
-       isar_shrink_factor = isar_shrink_factor, timeout = timeout}
+       isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
     val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
diff -r ca7ac998bb36 -r 162bbbea4e4d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 23:42:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Aug 31 23:43:23 2010 +0200
@@ -96,7 +96,7 @@
   AList.defined (op =) default_default_params s orelse
   AList.defined (op =) alias_params s orelse
   AList.defined (op =) negated_alias_params s orelse
-  member (op =) property_dependent_params s
+  member (op =) property_dependent_params s orelse s = "expect"
 
 fun check_raw_param (s, _) =
   if is_known_raw_param s then ()
@@ -184,12 +184,14 @@
     val isar_proof = lookup_bool "isar_proof"
     val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
     val timeout = lookup_time "timeout"
+    val expect = lookup_string "expect"
   in
     {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
      atps = atps, full_types = full_types, explicit_apply = explicit_apply,
      relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
      theory_relevant = theory_relevant, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, timeout = timeout}
+     isar_shrink_factor = isar_shrink_factor, timeout = timeout,
+     expect = expect}
   end
 
 fun get_params thy = extract_params (default_raw_params thy)