1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 16:54:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 17:38:40 2010 +0200
     1.3 @@ -10,6 +10,10 @@
     1.4  sig
     1.5    type minimize_command = string list -> string
     1.6  
     1.7 +  val axiom_prefix : string
     1.8 +  val conjecture_prefix : string
     1.9 +  val arity_clause_prefix : string
    1.10 +  val tfrees_name : string
    1.11    val metis_line: bool -> int -> int -> string list -> string
    1.12    val metis_proof_text:
    1.13      bool * minimize_command * string * string vector * thm * int
    1.14 @@ -34,6 +38,11 @@
    1.15  
    1.16  type minimize_command = string list -> string
    1.17  
    1.18 +val axiom_prefix = "ax_"
    1.19 +val conjecture_prefix = "conj_"
    1.20 +val arity_clause_prefix = "clsarity_"
    1.21 +val tfrees_name = "tfrees"
    1.22 +
    1.23  (* Simple simplifications to ensure that sort annotations don't leave a trail of
    1.24     spurious "True"s. *)
    1.25  fun s_not @{const False} = @{const True}
    1.26 @@ -548,15 +557,28 @@
    1.27     (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
    1.28     the first number (108) is extracted. For Vampire, we look for
    1.29     "108. ... [input]". *)
    1.30 -fun extract_formula_numbers_in_atp_proof atp_proof =
    1.31 +fun used_facts_in_atp_proof thm_names atp_proof =
    1.32    let
    1.33 -    val tokens_of = String.tokens (not o Char.isAlphaNum)
    1.34 -    fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
    1.35 -      | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
    1.36 -      | extract_num (num :: rest) =
    1.37 -        (case List.last rest of "input" => Int.fromString num | _ => NONE)
    1.38 -      | extract_num _ = NONE
    1.39 -  in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
    1.40 +    fun axiom_name num =
    1.41 +      let val j = Int.fromString num |> the_default ~1 in
    1.42 +        if is_axiom_clause_number thm_names j then
    1.43 +          SOME (Vector.sub (thm_names, j - 1))
    1.44 +        else
    1.45 +          NONE
    1.46 +      end
    1.47 +    val tokens_of =
    1.48 +      String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
    1.49 +    val thm_name_list = Vector.foldr (op ::) [] thm_names
    1.50 +    fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
    1.51 +        (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
    1.52 +           SOME name =>
    1.53 +           if member (op =) rest "file" then SOME name else axiom_name num
    1.54 +         | NONE => axiom_name num)
    1.55 +      | do_line (num :: "0" :: "Inp" :: _) = axiom_name num
    1.56 +      | do_line (num :: rest) =
    1.57 +        (case List.last rest of "input" => axiom_name num | _ => NONE)
    1.58 +      | do_line _ = NONE
    1.59 +  in atp_proof |> split_lines |> map_filter (do_line o tokens_of) end
    1.60  
    1.61  val indent_size = 2
    1.62  val no_label = ("", ~1)
    1.63 @@ -593,9 +615,7 @@
    1.64  val unprefix_chained = perhaps (try (unprefix chained_prefix))
    1.65  
    1.66  fun used_facts thm_names =
    1.67 -  extract_formula_numbers_in_atp_proof
    1.68 -  #> filter (is_axiom_clause_number thm_names)
    1.69 -  #> map (fn i => Vector.sub (thm_names, i - 1))
    1.70 +  used_facts_in_atp_proof thm_names
    1.71    #> List.partition (String.isPrefix chained_prefix)
    1.72    #>> map (unprefix chained_prefix)
    1.73    #> pairself (sort_distinct string_ord)