# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 4fbb1de05169c33ab8ce653a9e2393b29766a4c5
# Parent  59e0ca92bb0b201a090e5d43ae92480f1b3f4f17
fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings

diff -r 59e0ca92bb0b -r 4fbb1de05169 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun May 01 18:37:25 2011 +0200
@@ -12,10 +12,24 @@
   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
 
   datatype failure =
-    Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
-    CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
-    NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
-    Interrupted | Crashed | InternalError | UnknownError of string
+    Unprovable |
+    IncompleteUnprovable |
+    ProofMissing |
+    UnsoundProof of bool |
+    CantConnect |
+    TimedOut |
+    OutOfResources |
+    SpassTooOld |
+    VampireTooOld |
+    NoPerl |
+    NoLibwwwPerl |
+    NoRealZ3 |
+    MalformedInput |
+    MalformedOutput |
+    Interrupted |
+    Crashed |
+    InternalError |
+    UnknownError of string
 
   type step_name = string * string option
 
@@ -47,10 +61,24 @@
 open ATP_Problem
 
 datatype failure =
-  Unprovable | IncompleteUnprovable | ProofMissing | UnsoundProof |
-  CantConnect | TimedOut | OutOfResources | SpassTooOld | VampireTooOld |
-  NoPerl | NoLibwwwPerl | NoRealZ3 | MalformedInput | MalformedOutput |
-  Interrupted | Crashed | InternalError | UnknownError of string
+  Unprovable |
+  IncompleteUnprovable |
+  ProofMissing |
+  UnsoundProof of bool |
+  CantConnect |
+  TimedOut |
+  OutOfResources |
+  SpassTooOld |
+  VampireTooOld |
+  NoPerl |
+  NoLibwwwPerl |
+  NoRealZ3 |
+  MalformedInput |
+  MalformedOutput |
+  Interrupted |
+  Crashed |
+  InternalError |
+  UnknownError of string
 
 fun strip_spaces_in_list _ [] = []
   | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
@@ -95,9 +123,14 @@
     "The prover gave up."
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
-  | string_for_failure UnsoundProof =
-    "The prover found a type-unsound proof. (Or, very unlikely, your axioms \
-    \are inconsistent.)"
+  | string_for_failure (UnsoundProof false) =
+    "The prover found a type-unsound proof (or, very unlikely, your axioms \
+    \are inconsistent). Try passing the \"full_types\" option to Sledgehammer \
+    \to avoid such spurious proofs."
+  | string_for_failure (UnsoundProof true) =
+    "The prover found a type-unsound proof even though a supposedly type-sound \
+    \encoding was used (or, very unlikely, your axioms are inconsistent). You \
+    \might want to report this to the Isabelle developers."
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The prover ran out of resources."
diff -r 59e0ca92bb0b -r 4fbb1de05169 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:25 2011 +0200
@@ -20,8 +20,8 @@
   type text_result = string * (string * locality) list
 
   val repair_conjecture_shape_and_fact_names :
-    string -> int list list -> (string * locality) list vector
-    -> int list list * (string * locality) list vector
+    string -> int list list -> int -> (string * locality) list vector
+    -> int list list * int * (string * locality) list vector
   val used_facts_in_atp_proof :
     int -> (string * locality) list vector -> string proof
     -> (string * locality) list
@@ -78,8 +78,7 @@
 fun extract_clause_sequence output =
   let
     val tokens_of = String.tokens (not o Char.isAlphaNum)
-    fun extract_num ("clause" :: (ss as _ :: _)) =
-    Int.fromString (List.last ss)
+    fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss)
       | extract_num _ = NONE
   in output |> split_lines |> map_filter (extract_num o tokens_of) end
 
@@ -98,7 +97,8 @@
 
 val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
 
-fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_names =
+fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_offset
+                                           fact_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
     let
       val j0 = hd (hd conjecture_shape)
@@ -117,11 +117,11 @@
                      handle Option.Option =>
                             error ("No such fact: " ^ quote name ^ "."))
     in
-      (conjecture_shape |> map (maps renumber_conjecture),
+      (conjecture_shape |> map (maps renumber_conjecture), 0,
        seq |> map names_for_number |> Vector.fromList)
     end
   else
-    (conjecture_shape, fact_names)
+    (conjecture_shape, fact_offset, fact_names)
 
 val vampire_step_prefix = "f" (* grrr... *)
 
diff -r 59e0ca92bb0b -r 4fbb1de05169 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
@@ -495,20 +495,21 @@
                   extract_tstplike_proof_and_outcome debug verbose complete
                       res_code proof_delims known_failures output
                   |>> atp_proof_from_tstplike_proof
-                val (conjecture_shape, fact_names) =
+                val (conjecture_shape, facts_offset, fact_names) =
                   if is_none outcome then
                     repair_conjecture_shape_and_fact_names output
-                        conjecture_shape fact_names
+                        conjecture_shape facts_offset fact_names
                   else
-                    (conjecture_shape, fact_names) (* don't bother repairing *)
+                    (* don't bother repairing *)
+                    (conjecture_shape, facts_offset, fact_names)
                 val outcome =
                   case outcome of
-                    NONE => if level_of_type_sys type_sys <> Sound andalso
-                               is_unsound_proof conjecture_shape facts_offset
-                                                fact_names atp_proof then
-                              SOME UnsoundProof
-                            else
-                              NONE
+                    NONE =>
+                    if is_unsound_proof conjecture_shape facts_offset fact_names
+                                        atp_proof then
+                      SOME (UnsoundProof (level_of_type_sys type_sys = Sound))
+                    else
+                      NONE
                   | SOME Unprovable =>
                     if null blacklist then outcome
                     else SOME IncompleteUnprovable
@@ -534,7 +535,7 @@
               | maybe_run_slice _ _ result = result
             fun maybe_blacklist_facts_and_retry iter blacklist
                     (result as ((_, _, facts_offset, fact_names),
-                                (_, _, atp_proof, SOME UnsoundProof))) =
+                                (_, _, atp_proof, SOME (UnsoundProof false)))) =
                 (case used_facts_in_atp_proof facts_offset fact_names
                                               atp_proof of
                    [] => result