src/HOL/TPTP/TPTP_Parser/tptp_proof.ML

--- a/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Sep 03 21:46:40 2013 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_proof.ML	Tue Sep 03 21:46:40 2013 +0100
@@ -2,42 +2,135 @@
     Author:     Nik Sultana, Cambridge University Computer Laboratory
 
 Collection of functions for handling TPTP proofs.
+Specialised for handling LEO-II proofs.
 *)
 
+(*FIXME actually this is more general than proofs*)
 signature TPTP_PROOF =
 sig
-  val extract_inference_info : (TPTP_Syntax.general_term * 'a list) option ->
-                               (string * string list) option
+  datatype parent_detail =
+    Bind of string(*variable name*) * TPTP_Syntax.tptp_formula
+  datatype parent_info_as =
+      Parent of string(*node name*)
+    | ParentWithDetails of string(*node name*) *
+        parent_detail list
+  datatype useful_info_as = Status of TPTP_Syntax.status_value
+  datatype source_info =
+      File of string * string
+    | Inference of
+       string *
+       useful_info_as list *
+       parent_info_as list
+  val extract_source_info : (TPTP_Syntax.general_term * 'a list) option ->
+                               source_info option
+
+  val is_inference_called : string -> source_info -> bool
+
+  val parent_name : parent_info_as -> string
 end
 
 
 structure TPTP_Proof : TPTP_PROOF =
 struct
 
+datatype parent_detail =
+  Bind of string(*variable name*) * TPTP_Syntax.tptp_formula
+datatype parent_info_as =
+    Parent of string(*node name*)
+  | ParentWithDetails of string(*node name*) *
+      parent_detail list
+datatype useful_info_as = Status of TPTP_Syntax.status_value
+datatype source_info =
+    File of string * string
+  | Inference of
+     string *
+     useful_info_as list *
+     parent_info_as list
+
 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 =
+fun extract_source_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*)
+      fun analyse_parent_details [] acc = acc
+        | analyse_parent_details (x :: xs) acc =
+            case x of
+                General_Data
+                 (Application
+                  ("bind",
+                   [General_Data (V var),
+                    General_Data (Formula_Data (THF, fmla))])) =>
+                  analyse_parent_details xs (Bind (var, fmla) :: acc)
+              (*FIXME incomplete*)
+            | _ => analyse_parent_details xs acc
+
+      fun analyse_parent_info [] acc = acc
+        | analyse_parent_info (x :: xs) acc =
+            case x of
+                General_Data (Number (Int_num, num)) =>
+                  analyse_parent_info
+                    xs (Parent num :: acc)
+              | General_Data (Atomic_Word name) =>
+                  analyse_parent_info
+                    xs (Parent name :: acc)
+              | General_Term
+                  (Number (Int_num, num),
+                   General_List
+                    parent_details) =>
+                  let
+                    val parent_details' = analyse_parent_details parent_details []
+                  in
+                    analyse_parent_info
+                      xs (ParentWithDetails
+                          (num, parent_details') :: acc)
+                  end
+              (*FIXME incomplete*)
+              | _ => analyse_parent_info xs acc
+
+      fun analyse_useful_info [] acc = acc
+        | analyse_useful_info (x :: xs) acc =
+          case x of
+            General_Data
+              (Application
+                 ("status", [General_Data (Atomic_Word status_str)])) =>
+              analyse_useful_info
+                xs (Status (read_status status_str) :: acc)
+            (*FIXME incomplete*)
+            | _ => analyse_useful_info xs acc
+
+    fun analyse_annot
+        (General_Data
+          (Application
+            ("inference",
+             [General_Data (Atomic_Word inference_name),
+              General_List useful_info,
+              General_List parent_info])), _) =
+                (SOME (Inference
+                       (inference_name,
+                        analyse_useful_info useful_info [],
+                        analyse_parent_info parent_info [])))
+      | analyse_annot
+         (General_Data
+          (Application
+            ("file",
+             [General_Data (Atomic_Word filename),
+              General_Data (Atomic_Word defname)])), _) =
+                (SOME (File (filename, defname)))
+
   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)
+    | SOME annot => analyse_annot annot
   end
 
+fun is_inference_called s src =
+  case src of
+      Inference (n, _, _) => s = n
+    | _ => false
+
+fun parent_name (Parent n) = n
+  | parent_name (ParentWithDetails (n, _)) = n
+
 end