--- 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