# HG changeset patch
# User blanchet
# Date 1369048051 -7200
# Node ID 788b27dfaefaaac86d8eb18a818fc6ca0f51ad83
# Parent  bfa28e1cba77a226a44943ca84703c10d297cf5b
parse agsyHOL proofs (as unsat cores)

diff -r bfa28e1cba77 -r 788b27dfaefa src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 20 12:35:29 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 20 13:07:31 2013 +0200
@@ -473,6 +473,8 @@
 val satallax_coreN = "__satallax_core" (* arbitrary *)
 val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *)
 
+fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
+
 (* Syntax: core(<name>,[<name>,...,<name>]). *)
 fun parse_z3_tptp_line x =
   (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
@@ -481,8 +483,7 @@
 
 (* Syntax: <name> *)
 fun parse_satallax_line x =
-  (scan_general_id --| Scan.option ($$ " ")
-   >> (fn s => ((s, [s]), Unknown, dummy_phi, satallax_coreN, []))) x
+  (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_coreN) x
 
 fun parse_line problem =
   parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
@@ -495,11 +496,21 @@
                          (Scan.repeat1 (parse_line problem))))
   #> fst
 
+fun core_of_agsyhol_proof s =
+  case split_lines s of
+    "The transformed problem consists of the following conjectures:" :: conj ::
+    _ :: proof_term :: _ =>
+    SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term)
+  | _ => NONE
+
 fun atp_proof_of_tstplike_proof _ "" = []
   | atp_proof_of_tstplike_proof problem tstp =
-    tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
-    |> parse_proof problem
-    |> sort (step_name_ord o pairself #1)
+    case core_of_agsyhol_proof tstp of
+      SOME facts => facts |> map (core_inference agsyhol_coreN)
+    | NONE =>
+      tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
+      |> parse_proof problem
+      |> sort (step_name_ord o pairself #1)
 
 fun clean_up_dependencies _ [] = []
   | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
diff -r bfa28e1cba77 -r 788b27dfaefa src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Mon May 20 12:35:29 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Mon May 20 13:07:31 2013 +0200
@@ -14,6 +14,7 @@
   val strip_spaces : bool -> (char -> bool) -> string -> string
   val strip_spaces_except_between_idents : string -> string
   val elide_string : int -> string -> string
+  val find_enclosed : string -> string -> string -> string list
   val nat_subscript : int -> string
   val unquote_tvar : string -> string
   val unyxml : string -> string
@@ -121,6 +122,14 @@
   else
     s
 
+fun find_enclosed left right s =
+  case first_field left s of
+    SOME (_, s) =>
+    (case first_field right s of
+       SOME (enclosed, s) => enclosed :: find_enclosed left right s
+     | NONE => [])
+  | NONE => []
+
 val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
diff -r bfa28e1cba77 -r 788b27dfaefa src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon May 20 12:35:29 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon May 20 13:07:31 2013 +0200
@@ -162,10 +162,11 @@
         dependencies in the TSTP proof. Remove the next line once this is
         fixed. *)
      add_non_rec_defs fact_names
-   else if rule = satallax_coreN then
+   else if rule = agsyhol_coreN orelse rule = satallax_coreN then
      (fn [] =>
-         (* Satallax doesn't include definitions in its unsatisfiable cores, so
-            we assume the worst and include them all here. *)
+         (* agsyHOL and Satallax don't include definitions in their
+            unsatisfiable cores, so we assume the worst and include them all
+            here. *)
          [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names
        | facts => facts)
    else