--- 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
--- 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
--- /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
--- 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"
+ ];
--- /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;
--- 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"
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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;