--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Wed Apr 04 20:45:19 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Thu Apr 05 08:13:40 2012 +0200
@@ -896,7 +896,11 @@
val _ =
Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
(Parse.path >> (fn path =>
- Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
+ Toplevel.theory (fn thy =>
+ (*NOTE: assumes Axioms directory is on same level as the Problems one
+ (which is how TPTP is currently organised)*)
+ import_file true (Path.appends [Path.dir path, Path.parent, Path.parent])
+ path [] [] thy)))
(*Used for debugging. Returns all files contained within a directory or its
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy Thu Apr 05 08:13:40 2012 +0200
@@ -0,0 +1,69 @@
+(* Title: HOL/TPTP/TPTP_Parser_Example.thy
+ Author: Nik Sultana, Cambridge University Computer Laboratory
+
+Example of importing a TPTP problem and trying to prove it in Isabelle/HOL.
+*)
+
+theory TPTP_Parser_Example
+imports TPTP_Parser
+uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
+begin
+
+import_tptp "$TPTP_PROBLEMS_PATH/ALG/ALG001^5.p" (*FIXME multiple imports*)
+(*import_tptp "$TPTP_PROBLEMS_PATH/NUM/NUM021^1.p"*)
+
+ML {*
+val an_fmlas =
+ TPTP_Interpret.get_manifests @{theory}
+ |> hd (*FIXME use named lookup*)
+ |> #2 (*get problem contents*)
+ |> #3 (*get formulas*)
+*}
+
+(*Display nicely.*)
+ML {*
+List.app (fn (n, role, _, fmla, _) =>
+ Pretty.writeln
+ (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
+ TPTP_Syntax.role_to_string role ^ "): "), Syntax.pretty_term @{context} fmla])
+ ) (rev an_fmlas)
+*}
+
+ML {*
+(*Extract the (name, term) pairs of formulas having roles belonging to a
+ user-supplied set*)
+fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
+ (string * term) list =
+ let
+ fun role_predicate (_, role, _, _, _) =
+ fold (fn r1 => fn b => role = r1 orelse b) roles false
+ in filter role_predicate #> map (fn (n, _, _, t, _) => (n, t)) end
+*}
+
+ML {*
+(*Use a given tactic on a goal*)
+fun prove_conjectures tactic ctxt an_fmlas =
+ let
+ val assumptions =
+ extract_terms
+ [TPTP_Syntax.Role_Definition (*FIXME include axioms, etc here*)]
+ an_fmlas
+ |> map snd
+ val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
+ fun driver (n, goal) =
+ (n, Goal.prove ctxt [] assumptions goal (fn _ => tactic ctxt))
+ in map driver goals end
+
+val auto_prove = prove_conjectures auto_tac
+val sh_prove = prove_conjectures (fn ctxt =>
+ Sledgehammer_Tactics.sledgehammer_with_metis_tac ctxt []
+ (*FIXME use relevance_override*)
+ {add = [], del = [], only = false} 1)
+*}
+
+ML "auto_prove @{context} an_fmlas"
+
+sledgehammer_params [provers = z3_tptp leo2, debug]
+ML "sh_prove @{context} an_fmlas"
+
+end
\ No newline at end of file
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy Wed Apr 04 20:45:19 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy Thu Apr 05 08:13:40 2012 +0200
@@ -7,7 +7,7 @@
*)
theory TPTP_Parser_Test
-imports TPTP_Parser
+imports TPTP_Parser TPTP_Parser_Example
begin
ML {*
@@ -69,12 +69,12 @@
section "Source problems"
ML {*
(*problem source*)
- val thf_probs_dir =
+ val tptp_probs_dir =
Path.explode "$TPTP_PROBLEMS_PATH"
|> Path.expand;
(*list of files to under test*)
- val files = TPTP_Syntax.get_file_list thf_probs_dir;
+ val files = TPTP_Syntax.get_file_list tptp_probs_dir;
(* (*test problem-name parsing and mangling*)
val problem_names =
@@ -140,7 +140,7 @@
subsection "More parser tests"
ML {*
- fun situate file_name = Path.append thf_probs_dir (Path.explode file_name);
+ fun situate file_name = Path.append tptp_probs_dir (Path.explode file_name);
fun parser_test ctxt = (*FIXME argument order*)
test_fn ctxt
(fn file_name =>
@@ -184,8 +184,8 @@
Timing.timing
(TPTP_Interpret.interpret_file
false
- (Path.dir thf_probs_dir)
- (Path.append thf_probs_dir (Path.explode "LCL/LCL825-1.p"))
+ (Path.dir tptp_probs_dir)
+ (Path.append tptp_probs_dir (Path.explode "LCL/LCL825-1.p"))
[]
[])
@{theory}
@@ -228,7 +228,7 @@
TimeLimit.timeLimit (Time.fromSeconds timeout)
(TPTP_Interpret.interpret_file
false
- (Path.dir thf_probs_dir)
+ (Path.dir tptp_probs_dir)
file
[]
[])