added problem importer
authorblanchet
Mon Jan 23 17:40:32 2012 +0100 (2012-01-23)
changeset 46324e4bccf5ec61e
parent 46323 588c81d08a7c
child 46325 b170ab46513a
added problem importer
src/HOL/IsaMakefile
src/HOL/Nitpick.thy
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/ROOT.ML
src/HOL/TPTP/atp_problem_import.ML
src/HOL/TPTP/etc/settings
src/HOL/TPTP/lib/Tools/tptp_isabelle
src/HOL/TPTP/lib/Tools/tptp_nitpick
src/HOL/TPTP/lib/Tools/tptp_refute
src/HOL/TPTP/lib/Tools/tptp_sledgehammer
src/HOL/TPTP/lib/Tools/tptp_translate
src/HOL/Tools/Nitpick/nitpick_tptp.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Jan 23 17:40:32 2012 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -334,7 +334,6 @@
     1.4    Tools/Nitpick/nitpick_rep.ML \
     1.5    Tools/Nitpick/nitpick_scope.ML \
     1.6    Tools/Nitpick/nitpick_tests.ML \
     1.7 -  Tools/Nitpick/nitpick_tptp.ML \
     1.8    Tools/Nitpick/nitpick_util.ML \
     1.9    Tools/numeral.ML \
    1.10    Tools/numeral_simprocs.ML \
    1.11 @@ -1169,6 +1168,8 @@
    1.12  $(LOG)/HOL-TPTP.gz: \
    1.13    $(OUT)/HOL \
    1.14    TPTP/ROOT.ML \
    1.15 +  TPTP/atp_problem_import.ML \
    1.16 +  TPTP/ATP_Problem_Import.thy \
    1.17    TPTP/atp_theory_export.ML \
    1.18    TPTP/ATP_Theory_Export.thy \
    1.19    TPTP/CASC_Setup.thy
     2.1 --- a/src/HOL/Nitpick.thy	Mon Jan 23 17:40:32 2012 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Mon Jan 23 17:40:32 2012 +0100
     2.3 @@ -23,11 +23,9 @@
     2.4       ("Tools/Nitpick/nitpick_model.ML")
     2.5       ("Tools/Nitpick/nitpick.ML")
     2.6       ("Tools/Nitpick/nitpick_isar.ML")
     2.7 -     ("Tools/Nitpick/nitpick_tptp.ML")
     2.8       ("Tools/Nitpick/nitpick_tests.ML")
     2.9  begin
    2.10  
    2.11 -typedecl iota (* for TPTP *)
    2.12  typedecl bisim_iterator
    2.13  
    2.14  axiomatization unknown :: 'a
    2.15 @@ -223,7 +221,6 @@
    2.16  use "Tools/Nitpick/nitpick_model.ML"
    2.17  use "Tools/Nitpick/nitpick.ML"
    2.18  use "Tools/Nitpick/nitpick_isar.ML"
    2.19 -use "Tools/Nitpick/nitpick_tptp.ML"
    2.20  use "Tools/Nitpick/nitpick_tests.ML"
    2.21  
    2.22  setup {*
    2.23 @@ -240,8 +237,7 @@
    2.24      fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    2.25      one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    2.26      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    2.27 -hide_type (open) iota bisim_iterator fun_box pair_box unsigned_bit signed_bit
    2.28 -    word
    2.29 +hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    2.30  hide_fact (open) Ex1_unfold rtrancl_unfold rtranclp_unfold tranclp_unfold
    2.31      prod_def refl'_def wf'_def card'_def setsum'_def
    2.32      fold_graph'_def The_psimp Eps_psimp unit_case_unfold nat_case_unfold
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Mon Jan 23 17:40:32 2012 +0100
     3.3 @@ -0,0 +1,16 @@
     3.4 +(*  Title:      HOL/TPTP/ATP_Problem_Import.thy
     3.5 +    Author:     Jasmin Blanchette, TU Muenchen
     3.6 +*)
     3.7 +
     3.8 +header {* ATP Problem Importer *}
     3.9 +
    3.10 +theory ATP_Problem_Import
    3.11 +imports Complex_Main
    3.12 +uses ("atp_problem_import.ML")
    3.13 +begin
    3.14 +
    3.15 +typedecl iota (* for TPTP *)
    3.16 +
    3.17 +use "atp_problem_import.ML"
    3.18 +
    3.19 +end
     4.1 --- a/src/HOL/TPTP/ROOT.ML	Mon Jan 23 17:40:32 2012 +0100
     4.2 +++ b/src/HOL/TPTP/ROOT.ML	Mon Jan 23 17:40:32 2012 +0100
     4.3 @@ -11,4 +11,7 @@
     4.4  ];
     4.5  
     4.6  Unsynchronized.setmp Proofterm.proofs (!Proofterm.proofs)
     4.7 -  use_thy "CASC_Setup";
     4.8 +  use_thys [
     4.9 +    "ATP_Problem_Import",
    4.10 +    "CASC_Setup"
    4.11 +  ];
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Mon Jan 23 17:40:32 2012 +0100
     5.3 @@ -0,0 +1,170 @@
     5.4 +(*  Title:      HOL/TPTP/atp_problem_import.ML
     5.5 +    Author:     Jasmin Blanchette, TU Muenchen
     5.6 +    Copyright   2012
     5.7 +
     5.8 +Import TPTP problems as Isabelle terms or goals.
     5.9 +*)
    5.10 +
    5.11 +signature ATP_PROBLEM_IMPORT =
    5.12 +sig
    5.13 +  val isabelle_tptp_file : string -> unit
    5.14 +  val nitpick_tptp_file : string -> unit
    5.15 +  val refute_tptp_file : string -> unit
    5.16 +  val sledgehammer_tptp_file : string -> unit
    5.17 +  val translate_tptp_file : string -> unit
    5.18 +end;
    5.19 +
    5.20 +structure ATP_Problem_Import : ATP_PROBLEM_IMPORT =
    5.21 +struct
    5.22 +
    5.23 +open ATP_Util
    5.24 +open ATP_Problem
    5.25 +open ATP_Proof
    5.26 +open Nitpick_Util
    5.27 +open Nitpick
    5.28 +open Nitpick_Isar
    5.29 +
    5.30 +
    5.31 +(** General TPTP parsing **)
    5.32 +
    5.33 +exception SYNTAX of string
    5.34 +
    5.35 +val tptp_explode = raw_explode o strip_spaces_except_between_idents
    5.36 +
    5.37 +fun parse_file_path (c :: ss) =
    5.38 +    if c = "'" orelse c = "\"" then
    5.39 +      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
    5.40 +    else
    5.41 +      raise SYNTAX "invalid file path"
    5.42 +  | parse_file_path [] = raise SYNTAX "invalid file path"
    5.43 +
    5.44 +fun parse_include x =
    5.45 +  let
    5.46 +    val (file_name, rest) =
    5.47 +      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
    5.48 +       --| $$ ".") x
    5.49 +    val path = file_name |> Path.explode
    5.50 +    val path =
    5.51 +      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
    5.52 +  in ((), (path |> File.read |> tptp_explode) @ rest) end
    5.53 +
    5.54 +val parse_cnf_or_fof =
    5.55 +  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
    5.56 +  Scan.many (not_equal ",") |-- $$ "," |--
    5.57 +  (Scan.this_string "axiom" || Scan.this_string "definition"
    5.58 +   || Scan.this_string "theorem" || Scan.this_string "lemma"
    5.59 +   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    5.60 +   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
    5.61 +      --| $$ ")" --| $$ "."
    5.62 +  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
    5.63 +
    5.64 +val parse_problem =
    5.65 +  Scan.repeat parse_include
    5.66 +  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
    5.67 +
    5.68 +val parse_tptp_problem =
    5.69 +  Scan.finite Symbol.stopper
    5.70 +      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
    5.71 +                  parse_problem))
    5.72 +  o tptp_explode
    5.73 +
    5.74 +val iota_T = @{typ iota}
    5.75 +val quant_T = (iota_T --> bool_T) --> bool_T
    5.76 +
    5.77 +fun is_variable s = Char.isUpper (String.sub (s, 0))
    5.78 +
    5.79 +fun hol_term_from_fo_term res_T (ATerm (x, us)) =
    5.80 +  let val ts = map (hol_term_from_fo_term iota_T) us in
    5.81 +    list_comb ((case x of
    5.82 +                  "$true" => @{const_name True}
    5.83 +                | "$false" => @{const_name False}
    5.84 +                | "=" => @{const_name HOL.eq}
    5.85 +                | "equal" => @{const_name HOL.eq}
    5.86 +                | _ => x, map fastype_of ts ---> res_T)
    5.87 +               |> (if is_variable x then Free else Const), ts)
    5.88 +  end
    5.89 +
    5.90 +fun hol_prop_from_formula phi =
    5.91 +  case phi of
    5.92 +    AQuant (_, [], phi') => hol_prop_from_formula phi'
    5.93 +  | AQuant (q, (x, _) :: xs, phi') =>
    5.94 +    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
    5.95 +           quant_T)
    5.96 +    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
    5.97 +  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
    5.98 +  | AConn (c, [u1, u2]) =>
    5.99 +    pairself hol_prop_from_formula (u1, u2)
   5.100 +    |> (case c of
   5.101 +          AAnd => HOLogic.mk_conj
   5.102 +        | AOr => HOLogic.mk_disj
   5.103 +        | AImplies => HOLogic.mk_imp
   5.104 +        | AIff => HOLogic.mk_eq
   5.105 +        | ANot => raise Fail "binary \"ANot\"")
   5.106 +  | AConn _ => raise Fail "malformed AConn"
   5.107 +  | AAtom u => hol_term_from_fo_term bool_T u
   5.108 +
   5.109 +fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
   5.110 +
   5.111 +fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
   5.112 +
   5.113 +
   5.114 +(** Isabelle (combination of provers) **)
   5.115 +
   5.116 +fun isabelle_tptp_file file_name = ()
   5.117 +
   5.118 +
   5.119 +(** Nitpick (alias Nitrox) **)
   5.120 +
   5.121 +fun nitpick_tptp_file file_name =
   5.122 +  case parse_tptp_problem (File.read (Path.explode file_name)) of
   5.123 +    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
   5.124 +  | (phis, []) =>
   5.125 +    let
   5.126 +      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
   5.127 +                    o hol_prop_from_formula) phis
   5.128 +(*
   5.129 +      val _ = warning (PolyML.makestring phis)
   5.130 +      val _ = app (warning o Syntax.string_of_term @{context}) ts
   5.131 +*)
   5.132 +      val state = Proof.init @{context}
   5.133 +      val params =
   5.134 +        [("card iota", "1\<emdash>100"),
   5.135 +         ("card", "1\<emdash>8"),
   5.136 +         ("box", "false"),
   5.137 +         ("sat_solver", "smart"),
   5.138 +         ("max_threads", "1"),
   5.139 +         ("batch_size", "10"),
   5.140 +         (* ("debug", "true"), *)
   5.141 +         ("verbose", "true"),
   5.142 +         (* ("overlord", "true"), *)
   5.143 +         ("show_consts", "true"),
   5.144 +         ("format", "1000"),
   5.145 +         ("max_potential", "0"),
   5.146 +         ("timeout", "none"),
   5.147 +         ("expect", genuineN)]
   5.148 +        |> default_params @{theory}
   5.149 +      val i = 1
   5.150 +      val n = 1
   5.151 +      val step = 0
   5.152 +      val subst = []
   5.153 +    in
   5.154 +      pick_nits_in_term state params Normal i n step subst ts @{prop False};
   5.155 +      ()
   5.156 +    end
   5.157 +
   5.158 +
   5.159 +(** Refute **)
   5.160 +
   5.161 +fun refute_tptp_file file_name = ()
   5.162 +
   5.163 +
   5.164 +(** Sledgehammer **)
   5.165 +
   5.166 +fun sledgehammer_tptp_file file_name = ()
   5.167 +
   5.168 +
   5.169 +(** Translator between TPTP(-like) file formats **)
   5.170 +
   5.171 +fun translate_tptp_file file_name = ()
   5.172 +
   5.173 +end;
     6.1 --- a/src/HOL/TPTP/etc/settings	Mon Jan 23 17:40:32 2012 +0100
     6.2 +++ b/src/HOL/TPTP/etc/settings	Mon Jan 23 17:40:32 2012 +0100
     6.3 @@ -1,3 +1,5 @@
     6.4  # -*- shell-script -*- :mode=shellscript:
     6.5  
     6.6 +TPTP_HOME="$COMPONENT"
     6.7 +
     6.8  ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     7.1 --- a/src/HOL/TPTP/lib/Tools/tptp_isabelle	Mon Jan 23 17:40:32 2012 +0100
     7.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Mon Jan 23 17:40:32 2012 +0100
     7.3 @@ -22,7 +22,8 @@
     7.4  
     7.5  for FILE in "$@"
     7.6  do
     7.7 -  echo "theory $SCRATCH imports \"CASC\_Setup\" begin ML {* FIXME \"$FILE\" *} end;" \
     7.8 +  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
     7.9 +ML {* ATP_Problem_Import.isabelle_tptp_file \"$FILE\" *} end;" \
    7.10      > /tmp/$SCRATCH.thy
    7.11    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    7.12  done
     8.1 --- a/src/HOL/TPTP/lib/Tools/tptp_nitpick	Mon Jan 23 17:40:32 2012 +0100
     8.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Mon Jan 23 17:40:32 2012 +0100
     8.3 @@ -22,7 +22,8 @@
     8.4  
     8.5  for FILE in "$@"
     8.6  do
     8.7 -  echo "theory $SCRATCH imports \"Main\" begin ML {* Nitpick_TPTP.pick_nits_in_tptp_file \"$FILE\" *} end;" \
     8.8 +  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
     8.9 +ML {* ATP_Problem_Import.nitpick_tptp_file \"$FILE\" *} end;" \
    8.10      > /tmp/$SCRATCH.thy
    8.11    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    8.12  done
     9.1 --- a/src/HOL/TPTP/lib/Tools/tptp_refute	Mon Jan 23 17:40:32 2012 +0100
     9.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Mon Jan 23 17:40:32 2012 +0100
     9.3 @@ -22,7 +22,8 @@
     9.4  
     9.5  for FILE in "$@"
     9.6  do
     9.7 -  echo "theory $SCRATCH imports \"Main\" begin ML {* Refute.refute_tptp_file \"$FILE\" *} end;" \
     9.8 +  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
     9.9 +ML {* ATP_Problem_Import.refute_tptp_file \"$FILE\" *} end;" \
    9.10      > /tmp/$SCRATCH.thy
    9.11    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    9.12  done
    10.1 --- a/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Mon Jan 23 17:40:32 2012 +0100
    10.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Mon Jan 23 17:40:32 2012 +0100
    10.3 @@ -22,7 +22,8 @@
    10.4  
    10.5  for FILE in "$@"
    10.6  do
    10.7 -  echo "theory $SCRATCH imports \"Main\" begin ML {* Sledgehammer_Isar.run_sledgehammer_on_tptp_file \"$FILE\" *} end;" \
    10.8 +  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    10.9 +ML {* ATP_Problem_Import.sledgehammer_tptp_file \"$FILE\" *} end;" \
   10.10      > /tmp/$SCRATCH.thy
   10.11    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
   10.12  done
    11.1 --- a/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
    11.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:32 2012 +0100
    11.3 @@ -22,7 +22,8 @@
    11.4  
    11.5  for FILE in "$@"
    11.6  do
    11.7 -  echo "theory $SCRATCH imports \"Main\" begin ML {* ATP_Problem_Generate.translate_tptp_file \"$FILE\" *} end;" \
    11.8 +  echo "theory $SCRATCH imports \"$TPTP_HOME/ATP_Problem_Import\" begin \
    11.9 +ML {* ATP_Problem_Import.translate_tptp_file \"$FILE\" *} end;" \
   11.10      > /tmp/$SCRATCH.thy
   11.11    "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
   11.12  done
    12.1 --- a/src/HOL/Tools/Nitpick/nitpick_tptp.ML	Mon Jan 23 17:40:32 2012 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,140 +0,0 @@
    12.4 -(*  Title:      HOL/Tools/Nitpick/nitpick_tptp.ML
    12.5 -    Author:     Jasmin Blanchette, TU Muenchen
    12.6 -    Copyright   2010, 2011
    12.7 -
    12.8 -Nitpick for TPTP.
    12.9 -*)
   12.10 -
   12.11 -signature NITPICK_TPTP =
   12.12 -sig
   12.13 -  val pick_nits_in_tptp_file : string -> string
   12.14 -end;
   12.15 -
   12.16 -structure Nitpick_TPTP : NITPICK_TPTP =
   12.17 -struct
   12.18 -
   12.19 -open ATP_Util
   12.20 -open ATP_Problem
   12.21 -open ATP_Proof
   12.22 -open Nitpick_Util
   12.23 -open Nitpick
   12.24 -open Nitpick_Isar
   12.25 -
   12.26 -exception SYNTAX of string
   12.27 -
   12.28 -val tptp_explode = raw_explode o strip_spaces_except_between_idents
   12.29 -
   12.30 -fun parse_file_path (c :: ss) =
   12.31 -    if c = "'" orelse c = "\"" then
   12.32 -      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
   12.33 -    else
   12.34 -      raise SYNTAX "invalid file path"
   12.35 -  | parse_file_path [] = raise SYNTAX "invalid file path"
   12.36 -
   12.37 -fun parse_include x =
   12.38 -  let
   12.39 -    val (file_name, rest) =
   12.40 -      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
   12.41 -       --| $$ ".") x
   12.42 -    val path = file_name |> Path.explode
   12.43 -    val path =
   12.44 -      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
   12.45 -  in ((), (path |> File.read |> tptp_explode) @ rest) end
   12.46 -
   12.47 -val parse_cnf_or_fof =
   12.48 -  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
   12.49 -  Scan.many (not_equal ",") |-- $$ "," |--
   12.50 -  (Scan.this_string "axiom" || Scan.this_string "definition"
   12.51 -   || Scan.this_string "theorem" || Scan.this_string "lemma"
   12.52 -   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
   12.53 -   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
   12.54 -      --| $$ ")" --| $$ "."
   12.55 -  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
   12.56 -
   12.57 -val parse_problem =
   12.58 -  Scan.repeat parse_include
   12.59 -  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
   12.60 -
   12.61 -val parse_tptp_problem =
   12.62 -  Scan.finite Symbol.stopper
   12.63 -      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
   12.64 -                  parse_problem))
   12.65 -  o tptp_explode
   12.66 -
   12.67 -val iota_T = @{typ iota}
   12.68 -val quant_T = (iota_T --> bool_T) --> bool_T
   12.69 -
   12.70 -fun is_variable s = Char.isUpper (String.sub (s, 0))
   12.71 -
   12.72 -fun hol_term_from_fo_term res_T (ATerm (x, us)) =
   12.73 -  let val ts = map (hol_term_from_fo_term iota_T) us in
   12.74 -    list_comb ((case x of
   12.75 -                  "$true" => @{const_name True}
   12.76 -                | "$false" => @{const_name False}
   12.77 -                | "=" => @{const_name HOL.eq}
   12.78 -                | "equal" => @{const_name HOL.eq}
   12.79 -                | _ => x, map fastype_of ts ---> res_T)
   12.80 -               |> (if is_variable x then Free else Const), ts)
   12.81 -  end
   12.82 -
   12.83 -fun hol_prop_from_formula phi =
   12.84 -  case phi of
   12.85 -    AQuant (_, [], phi') => hol_prop_from_formula phi'
   12.86 -  | AQuant (q, (x, _) :: xs, phi') =>
   12.87 -    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
   12.88 -           quant_T)
   12.89 -    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
   12.90 -  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
   12.91 -  | AConn (c, [u1, u2]) =>
   12.92 -    pairself hol_prop_from_formula (u1, u2)
   12.93 -    |> (case c of
   12.94 -          AAnd => HOLogic.mk_conj
   12.95 -        | AOr => HOLogic.mk_disj
   12.96 -        | AImplies => HOLogic.mk_imp
   12.97 -        | AIff => HOLogic.mk_eq
   12.98 -        | ANot => raise Fail "binary \"ANot\"")
   12.99 -  | AConn _ => raise Fail "malformed AConn"
  12.100 -  | AAtom u => hol_term_from_fo_term bool_T u
  12.101 -
  12.102 -fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
  12.103 -
  12.104 -fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
  12.105 -
  12.106 -fun pick_nits_in_tptp_file file_name =
  12.107 -  case parse_tptp_problem (File.read (Path.explode file_name)) of
  12.108 -    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
  12.109 -  | (phis, []) =>
  12.110 -    let
  12.111 -      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
  12.112 -                    o hol_prop_from_formula) phis
  12.113 -(*
  12.114 -      val _ = warning (PolyML.makestring phis)
  12.115 -      val _ = app (warning o Syntax.string_of_term @{context}) ts
  12.116 -*)
  12.117 -      val state = Proof.init @{context}
  12.118 -      val params =
  12.119 -        [("card iota", "1\<emdash>100"),
  12.120 -         ("card", "1\<emdash>8"),
  12.121 -         ("box", "false"),
  12.122 -         ("sat_solver", "smart"),
  12.123 -         ("max_threads", "1"),
  12.124 -         ("batch_size", "10"),
  12.125 -         (* ("debug", "true"), *)
  12.126 -         ("verbose", "true"),
  12.127 -         (* ("overlord", "true"), *)
  12.128 -         ("show_consts", "true"),
  12.129 -         ("format", "1000"),
  12.130 -         ("max_potential", "0"),
  12.131 -         ("timeout", "none"),
  12.132 -         ("expect", genuineN)]
  12.133 -        |> default_params @{theory}
  12.134 -      val i = 1
  12.135 -      val n = 1
  12.136 -      val step = 0
  12.137 -      val subst = []
  12.138 -    in
  12.139 -      pick_nits_in_term state params Normal i n step subst ts @{prop False}
  12.140 -      |> fst
  12.141 -    end
  12.142 -
  12.143 -end;