# HG changeset patch
# User sultana
# Date 1333573059 -3600
# Node ID f5a304ca037e920d647144eb0daa8514c65e213f
# Parent  7b09206bb74bd9029596c56f4108c5e808908b58
improved import_tptp to use standard TPTP directory structure; extended the TPTP testing theory to include an example of using the import_tptp command;

diff -r 7b09206bb74b -r f5a304ca037e src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 04 20:40:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 04 21:57:39 2012 +0100
@@ -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
diff -r 7b09206bb74b -r f5a304ca037e src/HOL/TPTP/TPTP_Parser_Example.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Wed Apr 04 21:57:39 2012 +0100
@@ -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
diff -r 7b09206bb74b -r f5a304ca037e src/HOL/TPTP/TPTP_Parser_Test.thy
--- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Apr 04 20:40:39 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Wed Apr 04 21:57:39 2012 +0100
@@ -7,7 +7,7 @@
 *)
 
 theory TPTP_Parser_Test
-imports TPTP_Parser
+imports TPTP_Parser TPTP_Parser_Example
 begin
 
 ML {*