# HG changeset patch
# User huffman
# Date 1333606420 -7200
# Node ID eabfb53cfca809e43ea21fc32c07d80b2befa51c
# Parent  f483be2fecb9464db3b32642a25e1aba17148444# Parent  97097a58335d0d45afa9c0bb5dc780a84bb92131
merged

diff -r f483be2fecb9 -r eabfb53cfca8 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- 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
diff -r f483be2fecb9 -r eabfb53cfca8 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	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
diff -r f483be2fecb9 -r eabfb53cfca8 src/HOL/TPTP/TPTP_Parser_Test.thy
--- 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
          []
          [])