(* Title: HOL/TPTP/TPTP_Parser/tptp_proof.ML
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
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_source_info annot =
let
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 => 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