# HG changeset patch
# User sultana
# Date 1334036715 -3600
# Node ID 7df9a4f320a5d88560f7db6d9c38f57562bf5f0c
# Parent  33f2f968c0a1c323f3faf67439f005bc1b858ff7
moved non-interpret-specific code to different module

diff -r 33f2f968c0a1 -r 7df9a4f320a5 src/HOL/TPTP/TPTP_Parser.thy
--- a/src/HOL/TPTP/TPTP_Parser.thy	Mon Apr 09 23:06:14 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser.thy	Tue Apr 10 06:45:15 2012 +0100
@@ -17,6 +17,7 @@
   "TPTP_Parser/tptp_lexyacc.ML" (*generated from tptp.lex and tptp.yacc*)
   "TPTP_Parser/tptp_parser.ML"
   "TPTP_Parser/tptp_problem_name.ML"
+  "TPTP_Parser/tptp_proof.ML"
   "TPTP_Parser/tptp_interpret.ML"
 
 begin
diff -r 33f2f968c0a1 -r 7df9a4f320a5 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Mon Apr 09 23:06:14 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 10 06:45:15 2012 +0100
@@ -133,9 +133,6 @@
 
   val import_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
     theory -> theory
-
-  val extract_inference_info : (TPTP_Syntax.general_term * 'a list) option ->
-                               (string * string list) option
 end
 
 structure TPTP_Interpret : TPTP_INTERPRET =
@@ -681,32 +678,6 @@
         interpret_formula config language
          const_map var_types type_map tptp_formula thy
 
-
-(*Extract name of inference rule, and the inferences it relies on*)
-(*This is tuned to work with LEO-II, and is brittle to upstream
-  changes of the proof protocol.*)
-fun extract_inference_info annot =
-  let
-    fun get_line_id (General_Data (Number (Int_num, num))) = [num]
-      | get_line_id (General_Data (Atomic_Word name)) = [name]
-      | get_line_id (General_Term (Number (Int_num, num), _ (*e.g. a bind*))) = [num]
-      | get_line_id _ = []
-        (*e.g. General_Data (Application ("theory", [General_Data
-          (Atomic_Word "equality")])) -- which would come from E through LEO-II*)
-  in
-    case annot of
-      NONE => NONE
-    | SOME annot =>
-      (case annot of
-        (General_Data (Application ("inference",
-        [General_Data (Atomic_Word inference_name),
-         _,
-         General_List related_lines])), _) =>
-          (SOME (inference_name, map get_line_id related_lines |> List.concat))
-      | _ => NONE)
-  end
-
-
 (*Extract the type from a typing*)
 local
   fun extract_type tptp_type =
@@ -824,7 +795,7 @@
             ((type_map, const_map,
               [(label, role, tptp_formula,
                 Syntax.check_term (Proof_Context.init_global thy') t,
-                extract_inference_info annotation_opt)]), thy')
+                TPTP_Proof.extract_inference_info annotation_opt)]), thy')
            end
 
 and interpret_problem new_basic_types config path_prefix lines type_map const_map thy =
diff -r 33f2f968c0a1 -r 7df9a4f320a5 src/HOL/TPTP/TPTP_Parser/tptp_proof.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Apr 10 06:45:15 2012 +0100
@@ -0,0 +1,43 @@
+(*  Title:      HOL/TPTP/TPTP_Parser/tptp_proof.ML
+    Author:     Nik Sultana, Cambridge University Computer Laboratory
+
+Collection of functions for handling TPTP proofs.
+*)
+
+signature TPTP_PROOF =
+sig
+  val extract_inference_info : (TPTP_Syntax.general_term * 'a list) option ->
+                               (string * string list) option
+end
+
+
+structure TPTP_Proof : TPTP_PROOF =
+struct
+
+open TPTP_Syntax
+
+(*Extract name of inference rule, and the inferences it relies on*)
+(*This is tuned to work with LEO-II, and is brittle wrt upstream
+  changes of the proof protocol.*)
+fun extract_inference_info annot =
+  let
+    fun get_line_id (General_Data (Number (Int_num, num))) = [num]
+      | get_line_id (General_Data (Atomic_Word name)) = [name]
+      | get_line_id (General_Term (Number (Int_num, num), _ (*e.g. a bind*))) = [num]
+      | get_line_id _ = []
+        (*e.g. General_Data (Application ("theory", [General_Data
+          (Atomic_Word "equality")])) -- which would come from E through LEO-II*)
+  in
+    case annot of
+      NONE => NONE
+    | SOME annot =>
+      (case annot of
+        (General_Data (Application ("inference",
+        [General_Data (Atomic_Word inference_name),
+         _,
+         General_List related_lines])), _) =>
+          (SOME (inference_name, map get_line_id related_lines |> List.concat))
+      | _ => NONE)
+  end
+
+end