# HG changeset patch
# User blanchet
# Date 1327336832 -3600
# Node ID e4bccf5ec61eb9efe5ce8b4a40b545b5f55d1c6b
# Parent  588c81d08a7c21cc2408bd172ae11c4315e92efc
added problem importer

diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/IsaMakefile	Mon Jan 23 17:40:32 2012 +0100
@@ -334,7 +334,6 @@
   Tools/Nitpick/nitpick_rep.ML \
   Tools/Nitpick/nitpick_scope.ML \
   Tools/Nitpick/nitpick_tests.ML \
-  Tools/Nitpick/nitpick_tptp.ML \
   Tools/Nitpick/nitpick_util.ML \
   Tools/numeral.ML \
   Tools/numeral_simprocs.ML \
@@ -1169,6 +1168,8 @@
 $(LOG)/HOL-TPTP.gz: \
   $(OUT)/HOL \
   TPTP/ROOT.ML \
+  TPTP/atp_problem_import.ML \
+  TPTP/ATP_Problem_Import.thy \
   TPTP/atp_theory_export.ML \
   TPTP/ATP_Theory_Export.thy \
   TPTP/CASC_Setup.thy
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/Nitpick.thy	Mon Jan 23 17:40:32 2012 +0100
@@ -23,11 +23,9 @@
      ("Tools/Nitpick/nitpick_model.ML")
      ("Tools/Nitpick/nitpick.ML")
      ("Tools/Nitpick/nitpick_isar.ML")
-     ("Tools/Nitpick/nitpick_tptp.ML")
      ("Tools/Nitpick/nitpick_tests.ML")
 begin
 
-typedecl iota (* for TPTP *)
 typedecl bisim_iterator
 
 axiomatization unknown :: 'a
@@ -223,7 +221,6 @@
 use "Tools/Nitpick/nitpick_model.ML"
 use "Tools/Nitpick/nitpick.ML"
 use "Tools/Nitpick/nitpick_isar.ML"
-use "Tools/Nitpick/nitpick_tptp.ML"
 use "Tools/Nitpick/nitpick_tests.ML"
 
 setup {*
@@ -240,8 +237,7 @@
     fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
     one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
     number_of_frac inverse_frac less_frac less_eq_frac of_frac
-hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
-    word
+hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
 hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
     prod_def refl'_def wf'_def card'_def setsum'_def
     fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/ATP_Problem_Import.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Mon Jan 23 17:40:32 2012 +0100
@@ -0,0 +1,16 @@
+(*  Title:      HOL/TPTP/ATP_Problem_Import.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+*)
+
+header {* ATP Problem Importer *}
+
+theory ATP_Problem_Import
+imports Complex_Main
+uses ("atp_problem_import.ML")
+begin
+
+typedecl iota (* for TPTP *)
+
+use "atp_problem_import.ML"
+
+end
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/ROOT.ML
--- a/src/HOL/TPTP/ROOT.ML	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/ROOT.ML	Mon Jan 23 17:40:32 2012 +0100
@@ -11,4 +11,7 @@
 ];
 
 Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
-  use_thy "CASC_Setup";
+  use_thys [
+    "ATP_Problem_Import",
+    "CASC_Setup"
+  ];
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/atp_problem_import.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Jan 23 17:40:32 2012 +0100
@@ -0,0 +1,170 @@
+(*  Title:      HOL/TPTP/atp_problem_import.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Import TPTP problems as Isabelle terms or goals.
+*)
+
+signature ATP_PROBLEM_IMPORT =
+sig
+  val isabelle_tptp_file : string -> unit
+  val nitpick_tptp_file : string -> unit
+  val refute_tptp_file : string -> unit
+  val sledgehammer_tptp_file : string -> unit
+  val translate_tptp_file : string -> unit
+end;
+
+structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
+struct
+
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+open Nitpick_Util
+open Nitpick
+open Nitpick_Isar
+
+
+(** General TPTP parsing **)
+
+exception SYNTAX of string
+
+val tptp_explode = raw_explode o strip_spaces_except_between_idents
+
+fun parse_file_path (c :: ss) =
+    if c = "'" orelse c = "\"" then
+      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
+    else
+      raise SYNTAX "invalid file path"
+  | parse_file_path [] = raise SYNTAX "invalid file path"
+
+fun parse_include x =
+  let
+    val (file_name, rest) =
+      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
+       --| $$ ".") x
+    val path = file_name |> Path.explode
+    val path =
+      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
+  in ((), (path |> File.read |> tptp_explode) @ rest) end
+
+val parse_cnf_or_fof =
+  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
+  Scan.many (not_equal ",") |-- $$ "," |--
+  (Scan.this_string "axiom" || Scan.this_string "definition"
+   || Scan.this_string "theorem" || Scan.this_string "lemma"
+   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
+   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
+      --| $$ ")" --| $$ "."
+  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
+
+val parse_problem =
+  Scan.repeat parse_include
+  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
+
+val parse_tptp_problem =
+  Scan.finite Symbol.stopper
+      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
+                  parse_problem))
+  o tptp_explode
+
+val iota_T = @{typ iota}
+val quant_T = (iota_T --> bool_T) --> bool_T
+
+fun is_variable s = Char.isUpper (String.sub (s, 0))
+
+fun hol_term_from_fo_term res_T (ATerm (x, us)) =
+  let val ts = map (hol_term_from_fo_term iota_T) us in
+    list_comb ((case x of
+                  "$true" => @{const_name True}
+                | "$false" => @{const_name False}
+                | "=" => @{const_name HOL.eq}
+                | "equal" => @{const_name HOL.eq}
+                | _ => x, map fastype_of ts ---> res_T)
+               |> (if is_variable x then Free else Const), ts)
+  end
+
+fun hol_prop_from_formula phi =
+  case phi of
+    AQuant (_, [], phi') => hol_prop_from_formula phi'
+  | AQuant (q, (x, _) :: xs, phi') =>
+    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
+           quant_T)
+    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
+  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
+  | AConn (c, [u1, u2]) =>
+    pairself hol_prop_from_formula (u1, u2)
+    |> (case c of
+          AAnd => HOLogic.mk_conj
+        | AOr => HOLogic.mk_disj
+        | AImplies => HOLogic.mk_imp
+        | AIff => HOLogic.mk_eq
+        | ANot => raise Fail "binary \"ANot\"")
+  | AConn _ => raise Fail "malformed AConn"
+  | AAtom u => hol_term_from_fo_term bool_T u
+
+fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
+
+fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
+
+
+(** Isabelle (combination of provers) **)
+
+fun isabelle_tptp_file file_name = ()
+
+
+(** Nitpick (alias Nitrox) **)
+
+fun nitpick_tptp_file file_name =
+  case parse_tptp_problem (File.read (Path.explode file_name)) of
+    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
+  | (phis, []) =>
+    let
+      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
+                    o hol_prop_from_formula) phis
+(*
+      val _ = warning (PolyML.makestring phis)
+      val _ = app (warning o Syntax.string_of_term @{context}) ts
+*)
+      val state = Proof.init @{context}
+      val params =
+        [("card iota", "1\<emdash>100"),
+         ("card", "1\<emdash>8"),
+         ("box", "false"),
+         ("sat_solver", "smart"),
+         ("max_threads", "1"),
+         ("batch_size", "10"),
+         (* ("debug", "true"), *)
+         ("verbose", "true"),
+         (* ("overlord", "true"), *)
+         ("show_consts", "true"),
+         ("format", "1000"),
+         ("max_potential", "0"),
+         ("timeout", "none"),
+         ("expect", genuineN)]
+        |> default_params @{theory}
+      val i = 1
+      val n = 1
+      val step = 0
+      val subst = []
+    in
+      pick_nits_in_term state params Normal i n step subst ts @{prop False};
+      ()
+    end
+
+
+(** Refute **)
+
+fun refute_tptp_file file_name = ()
+
+
+(** Sledgehammer **)
+
+fun sledgehammer_tptp_file file_name = ()
+
+
+(** Translator between TPTP(-like) file formats **)
+
+fun translate_tptp_file file_name = ()
+
+end;
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/etc/settings
--- a/src/HOL/TPTP/etc/settings	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/etc/settings	Mon Jan 23 17:40:32 2012 +0100
@@ -1,3 +1,5 @@
 # -*- shell-script -*- :mode=shellscript:
 
+TPTP_HOME="$COMPONENT"
+
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/lib/Tools/tptp_isabelle
--- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Mon Jan 23 17:40:32 2012 +0100
@@ -22,7 +22,8 @@
 
 for FILE in "$@"
 do
-  echo "theory $SCRATCH imports \"CASC\_Setup\" begin ML {* FIXME \"$FILE\" *} end;" \
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.isabelle_tptp_file \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/lib/Tools/tptp_nitpick
--- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Mon Jan 23 17:40:32 2012 +0100
@@ -22,7 +22,8 @@
 
 for FILE in "$@"
 do
-  echo "theory $SCRATCH imports \"Main\" begin ML {* Nitpick_TPTP.pick_nits_in_tptp_file \"$FILE\" *} end;" \
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.nitpick_tptp_file \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/lib/Tools/tptp_refute
--- a/src/HOL/TPTP/lib/Tools/tptp_refute	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Mon Jan 23 17:40:32 2012 +0100
@@ -22,7 +22,8 @@
 
 for FILE in "$@"
 do
-  echo "theory $SCRATCH imports \"Main\" begin ML {* Refute.refute_tptp_file \"$FILE\" *} end;" \
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.refute_tptp_file \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/lib/Tools/tptp_sledgehammer
--- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Mon Jan 23 17:40:32 2012 +0100
@@ -22,7 +22,8 @@
 
 for FILE in "$@"
 do
-  echo "theory $SCRATCH imports \"Main\" begin ML {* Sledgehammer_Isar.run_sledgehammer_on_tptp_file \"$FILE\" *} end;" \
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.sledgehammer_tptp_file \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/TPTP/lib/Tools/tptp_translate
--- a/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
+++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
@@ -22,7 +22,8 @@
 
 for FILE in "$@"
 do
-  echo "theory $SCRATCH imports \"Main\" begin ML {* ATP_Problem_Generate.translate_tptp_file \"$FILE\" *} end;" \
+  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
+ML {* ATP_Problem_Import.translate_tptp_file \"$FILE\" *} end;" \
     > /tmp/$SCRATCH.thy
   "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
 done
diff -r 588c81d08a7c -r e4bccf5ec61e src/HOL/Tools/Nitpick/nitpick_tptp.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tptp.ML	Mon Jan 23 17:40:32 2012 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,140 +0,0 @@
-(*  Title:      HOL/Tools/Nitpick/nitpick_tptp.ML
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2010, 2011
-
-Nitpick for TPTP.
-*)
-
-signature NITPICK_TPTP =
-sig
-  val pick_nits_in_tptp_file : string -> string
-end;
-
-structure Nitpick_TPTP : NITPICK_TPTP =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open Nitpick_Util
-open Nitpick
-open Nitpick_Isar
-
-exception SYNTAX of string
-
-val tptp_explode = raw_explode o strip_spaces_except_between_idents
-
-fun parse_file_path (c :: ss) =
-    if c = "'" orelse c = "\"" then
-      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
-    else
-      raise SYNTAX "invalid file path"
-  | parse_file_path [] = raise SYNTAX "invalid file path"
-
-fun parse_include x =
-  let
-    val (file_name, rest) =
-      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
-       --| $$ ".") x
-    val path = file_name |> Path.explode
-    val path =
-      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
-  in ((), (path |> File.read |> tptp_explode) @ rest) end
-
-val parse_cnf_or_fof =
-  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
-  Scan.many (not_equal ",") |-- $$ "," |--
-  (Scan.this_string "axiom" || Scan.this_string "definition"
-   || Scan.this_string "theorem" || Scan.this_string "lemma"
-   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
-   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
-      --| $$ ")" --| $$ "."
-  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
-
-val parse_problem =
-  Scan.repeat parse_include
-  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
-
-val parse_tptp_problem =
-  Scan.finite Symbol.stopper
-      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
-                  parse_problem))
-  o tptp_explode
-
-val iota_T = @{typ iota}
-val quant_T = (iota_T --> bool_T) --> bool_T
-
-fun is_variable s = Char.isUpper (String.sub (s, 0))
-
-fun hol_term_from_fo_term res_T (ATerm (x, us)) =
-  let val ts = map (hol_term_from_fo_term iota_T) us in
-    list_comb ((case x of
-                  "$true" => @{const_name True}
-                | "$false" => @{const_name False}
-                | "=" => @{const_name HOL.eq}
-                | "equal" => @{const_name HOL.eq}
-                | _ => x, map fastype_of ts ---> res_T)
-               |> (if is_variable x then Free else Const), ts)
-  end
-
-fun hol_prop_from_formula phi =
-  case phi of
-    AQuant (_, [], phi') => hol_prop_from_formula phi'
-  | AQuant (q, (x, _) :: xs, phi') =>
-    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
-           quant_T)
-    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
-  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
-  | AConn (c, [u1, u2]) =>
-    pairself hol_prop_from_formula (u1, u2)
-    |> (case c of
-          AAnd => HOLogic.mk_conj
-        | AOr => HOLogic.mk_disj
-        | AImplies => HOLogic.mk_imp
-        | AIff => HOLogic.mk_eq
-        | ANot => raise Fail "binary \"ANot\"")
-  | AConn _ => raise Fail "malformed AConn"
-  | AAtom u => hol_term_from_fo_term bool_T u
-
-fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
-
-fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
-
-fun pick_nits_in_tptp_file file_name =
-  case parse_tptp_problem (File.read (Path.explode file_name)) of
-    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
-  | (phis, []) =>
-    let
-      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
-                    o hol_prop_from_formula) phis
-(*
-      val _ = warning (PolyML.makestring phis)
-      val _ = app (warning o Syntax.string_of_term @{context}) ts
-*)
-      val state = Proof.init @{context}
-      val params =
-        [("card iota", "1\<emdash>100"),
-         ("card", "1\<emdash>8"),
-         ("box", "false"),
-         ("sat_solver", "smart"),
-         ("max_threads", "1"),
-         ("batch_size", "10"),
-         (* ("debug", "true"), *)
-         ("verbose", "true"),
-         (* ("overlord", "true"), *)
-         ("show_consts", "true"),
-         ("format", "1000"),
-         ("max_potential", "0"),
-         ("timeout", "none"),
-         ("expect", genuineN)]
-        |> default_params @{theory}
-      val i = 1
-      val n = 1
-      val step = 0
-      val subst = []
-    in
-      pick_nits_in_term state params Normal i n step subst ts @{prop False}
-      |> fst
-    end
-
-end;