rebranded Nitrox, for more uniformity
authorblanchet
Mon Jan 23 17:40:31 2012 +0100 (2012-01-23)
changeset 46319c248e4f1be74
parent 46318 8038d050ff15
child 46320 0b8b73b49848
rebranded Nitrox, for more uniformity
src/HOL/IsaMakefile
src/HOL/Nitpick.thy
src/HOL/TPTP/lib/Tools/nitrox
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
src/HOL/Tools/Nitpick/nitrox.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Mon Jan 23 17:40:31 2012 +0100
     1.3 @@ -334,8 +334,8 @@
     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/Nitpick/nitrox.ML \
    1.10    Tools/numeral.ML \
    1.11    Tools/numeral_simprocs.ML \
    1.12    Tools/numeral_syntax.ML \
     2.1 --- a/src/HOL/Nitpick.thy	Mon Jan 23 17:40:31 2012 +0100
     2.2 +++ b/src/HOL/Nitpick.thy	Mon Jan 23 17:40:31 2012 +0100
     2.3 @@ -23,11 +23,11 @@
     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 -     ("Tools/Nitpick/nitrox.ML")
    2.10  begin
    2.11  
    2.12 -typedecl iota (* for Nitrox *)
    2.13 +typedecl iota (* for TPTP *)
    2.14  typedecl bisim_iterator
    2.15  
    2.16  axiomatization unknown :: 'a
    2.17 @@ -223,8 +223,8 @@
    2.18  use "Tools/Nitpick/nitpick_model.ML"
    2.19  use "Tools/Nitpick/nitpick.ML"
    2.20  use "Tools/Nitpick/nitpick_isar.ML"
    2.21 +use "Tools/Nitpick/nitpick_tptp.ML"
    2.22  use "Tools/Nitpick/nitpick_tests.ML"
    2.23 -use "Tools/Nitpick/nitrox.ML"
    2.24  
    2.25  setup {*
    2.26    Nitpick_Isar.setup #>
     3.1 --- a/src/HOL/TPTP/lib/Tools/nitrox	Mon Jan 23 17:40:31 2012 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,28 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Author: Jasmin Blanchette
     3.7 -#
     3.8 -# DESCRIPTION: TPTP FOF version of Nitpick
     3.9 -
    3.10 -
    3.11 -PRG="$(basename "$0")"
    3.12 -
    3.13 -function usage() {
    3.14 -  echo
    3.15 -  echo "Usage: isabelle $PRG FILES"
    3.16 -  echo
    3.17 -  echo "  Runs Nitrox on a CNF or FOF TPTP problem."
    3.18 -  echo
    3.19 -  exit 1
    3.20 -}
    3.21 -
    3.22 -[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    3.23 -
    3.24 -SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    3.25 -
    3.26 -for FILE in "$@"
    3.27 -do
    3.28 -  echo "theory $SCRATCH imports \"Nitpick\" begin ML {* Nitrox.pick_nits_in_fof_file \"$FILE\" *} end;" \
    3.29 -    > /tmp/$SCRATCH.thy
    3.30 -  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    3.31 -done
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_isabelle	Mon Jan 23 17:40:31 2012 +0100
     4.3 @@ -0,0 +1,28 @@
     4.4 +#!/usr/bin/env bash
     4.5 +#
     4.6 +# Author: Jasmin Blanchette
     4.7 +#
     4.8 +# DESCRIPTION: Isabelle tactics for TPTP
     4.9 +
    4.10 +
    4.11 +PRG="$(basename "$0")"
    4.12 +
    4.13 +function usage() {
    4.14 +  echo
    4.15 +  echo "Usage: isabelle $PRG FILES"
    4.16 +  echo
    4.17 +  echo "  Runs a combination of Isabelle tactics on TPTP problems."
    4.18 +  echo
    4.19 +  exit 1
    4.20 +}
    4.21 +
    4.22 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    4.23 +
    4.24 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    4.25 +
    4.26 +for FILE in "$@"
    4.27 +do
    4.28 +  echo "theory $SCRATCH imports \"CASC\_Setup\" begin ML {* FIXME \"$FILE\" *} end;" \
    4.29 +    > /tmp/$SCRATCH.thy
    4.30 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    4.31 +done
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_nitpick	Mon Jan 23 17:40:31 2012 +0100
     5.3 @@ -0,0 +1,28 @@
     5.4 +#!/usr/bin/env bash
     5.5 +#
     5.6 +# Author: Jasmin Blanchette
     5.7 +#
     5.8 +# DESCRIPTION: Nitpick for TPTP
     5.9 +
    5.10 +
    5.11 +PRG="$(basename "$0")"
    5.12 +
    5.13 +function usage() {
    5.14 +  echo
    5.15 +  echo "Usage: isabelle $PRG FILES"
    5.16 +  echo
    5.17 +  echo "  Runs Nitpick on TPTP problems."
    5.18 +  echo
    5.19 +  exit 1
    5.20 +}
    5.21 +
    5.22 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    5.23 +
    5.24 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    5.25 +
    5.26 +for FILE in "$@"
    5.27 +do
    5.28 +  echo "theory $SCRATCH imports \"Main\" begin ML {* Nitpick_TPTP.pick_nits_in_tptp_file \"$FILE\" *} end;" \
    5.29 +    > /tmp/$SCRATCH.thy
    5.30 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    5.31 +done
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_refute	Mon Jan 23 17:40:31 2012 +0100
     6.3 @@ -0,0 +1,28 @@
     6.4 +#!/usr/bin/env bash
     6.5 +#
     6.6 +# Author: Jasmin Blanchette
     6.7 +#
     6.8 +# DESCRIPTION: Refute for TPTP
     6.9 +
    6.10 +
    6.11 +PRG="$(basename "$0")"
    6.12 +
    6.13 +function usage() {
    6.14 +  echo
    6.15 +  echo "Usage: isabelle $PRG FILES"
    6.16 +  echo
    6.17 +  echo "  Runs Refute on TPTP problems."
    6.18 +  echo
    6.19 +  exit 1
    6.20 +}
    6.21 +
    6.22 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    6.23 +
    6.24 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    6.25 +
    6.26 +for FILE in "$@"
    6.27 +do
    6.28 +  echo "theory $SCRATCH imports \"Main\" begin ML {* Refute.refute_tptp_file \"$FILE\" *} end;" \
    6.29 +    > /tmp/$SCRATCH.thy
    6.30 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    6.31 +done
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_sledgehammer	Mon Jan 23 17:40:31 2012 +0100
     7.3 @@ -0,0 +1,28 @@
     7.4 +#!/usr/bin/env bash
     7.5 +#
     7.6 +# Author: Jasmin Blanchette
     7.7 +#
     7.8 +# DESCRIPTION: Sledgehammer for TPTP
     7.9 +
    7.10 +
    7.11 +PRG="$(basename "$0")"
    7.12 +
    7.13 +function usage() {
    7.14 +  echo
    7.15 +  echo "Usage: isabelle $PRG FILES"
    7.16 +  echo
    7.17 +  echo "  Runs Sledgehammer on TPTP problems."
    7.18 +  echo
    7.19 +  exit 1
    7.20 +}
    7.21 +
    7.22 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    7.23 +
    7.24 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    7.25 +
    7.26 +for FILE in "$@"
    7.27 +do
    7.28 +  echo "theory $SCRATCH imports \"Main\" begin ML {* Sledgehammer_Isar.run_sledgehammer_on_tptp_file \"$FILE\" *} end;" \
    7.29 +    > /tmp/$SCRATCH.thy
    7.30 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    7.31 +done
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/TPTP/lib/Tools/tptp_translate	Mon Jan 23 17:40:31 2012 +0100
     8.3 @@ -0,0 +1,28 @@
     8.4 +#!/usr/bin/env bash
     8.5 +#
     8.6 +# Author: Jasmin Blanchette
     8.7 +#
     8.8 +# DESCRIPTION: Translation tool for TPTP formats
     8.9 +
    8.10 +
    8.11 +PRG="$(basename "$0")"
    8.12 +
    8.13 +function usage() {
    8.14 +  echo
    8.15 +  echo "Usage: isabelle $PRG FORMAT FILE"
    8.16 +  echo
    8.17 +  echo "  Translates TPTP file to specified TPTP format (\"CNF\", \"FOF\", \"TFF0\", \"TFF1\", or \"THF0\")."
    8.18 +  echo
    8.19 +  exit 1
    8.20 +}
    8.21 +
    8.22 +[ "$#" -eq 0 -o "$1" = "-?" ] && usage
    8.23 +
    8.24 +SCRATCH="Scratch_${PRG}_$$_${RANDOM}"
    8.25 +
    8.26 +for FILE in "$@"
    8.27 +do
    8.28 +  echo "theory $SCRATCH imports \"Main\" begin ML {* ATP_Translate.translate_tptp_file \"$FILE\" *} end;" \
    8.29 +    > /tmp/$SCRATCH.thy
    8.30 +  "$ISABELLE_PROCESS" -e "use_thy \"/tmp/$SCRATCH\"; exit 1;"
    8.31 +done
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tptp.ML	Mon Jan 23 17:40:31 2012 +0100
     9.3 @@ -0,0 +1,140 @@
     9.4 +(*  Title:      HOL/Tools/Nitpick/nitpick_tptp.ML
     9.5 +    Author:     Jasmin Blanchette, TU Muenchen
     9.6 +    Copyright   2010, 2011
     9.7 +
     9.8 +Nitpick for TPTP.
     9.9 +*)
    9.10 +
    9.11 +signature NITPICK_TPTP =
    9.12 +sig
    9.13 +  val pick_nits_in_tptp_file : string -> string
    9.14 +end;
    9.15 +
    9.16 +structure Nitpick_TPTP : NITPICK_TPTP =
    9.17 +struct
    9.18 +
    9.19 +open ATP_Util
    9.20 +open ATP_Problem
    9.21 +open ATP_Proof
    9.22 +open Nitpick_Util
    9.23 +open Nitpick
    9.24 +open Nitpick_Isar
    9.25 +
    9.26 +exception SYNTAX of string
    9.27 +
    9.28 +val tptp_explode = raw_explode o strip_spaces_except_between_idents
    9.29 +
    9.30 +fun parse_file_path (c :: ss) =
    9.31 +    if c = "'" orelse c = "\"" then
    9.32 +      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
    9.33 +    else
    9.34 +      raise SYNTAX "invalid file path"
    9.35 +  | parse_file_path [] = raise SYNTAX "invalid file path"
    9.36 +
    9.37 +fun parse_include x =
    9.38 +  let
    9.39 +    val (file_name, rest) =
    9.40 +      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
    9.41 +       --| $$ ".") x
    9.42 +    val path = file_name |> Path.explode
    9.43 +    val path =
    9.44 +      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
    9.45 +  in ((), (path |> File.read |> tptp_explode) @ rest) end
    9.46 +
    9.47 +val parse_cnf_or_fof =
    9.48 +  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
    9.49 +  Scan.many (not_equal ",") |-- $$ "," |--
    9.50 +  (Scan.this_string "axiom" || Scan.this_string "definition"
    9.51 +   || Scan.this_string "theorem" || Scan.this_string "lemma"
    9.52 +   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    9.53 +   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
    9.54 +      --| $$ ")" --| $$ "."
    9.55 +  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
    9.56 +
    9.57 +val parse_problem =
    9.58 +  Scan.repeat parse_include
    9.59 +  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
    9.60 +
    9.61 +val parse_tptp_problem =
    9.62 +  Scan.finite Symbol.stopper
    9.63 +      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
    9.64 +                  parse_problem))
    9.65 +  o tptp_explode
    9.66 +
    9.67 +val iota_T = @{typ iota}
    9.68 +val quant_T = (iota_T --> bool_T) --> bool_T
    9.69 +
    9.70 +fun is_variable s = Char.isUpper (String.sub (s, 0))
    9.71 +
    9.72 +fun hol_term_from_fo_term res_T (ATerm (x, us)) =
    9.73 +  let val ts = map (hol_term_from_fo_term iota_T) us in
    9.74 +    list_comb ((case x of
    9.75 +                  "$true" => @{const_name True}
    9.76 +                | "$false" => @{const_name False}
    9.77 +                | "=" => @{const_name HOL.eq}
    9.78 +                | "equal" => @{const_name HOL.eq}
    9.79 +                | _ => x, map fastype_of ts ---> res_T)
    9.80 +               |> (if is_variable x then Free else Const), ts)
    9.81 +  end
    9.82 +
    9.83 +fun hol_prop_from_formula phi =
    9.84 +  case phi of
    9.85 +    AQuant (_, [], phi') => hol_prop_from_formula phi'
    9.86 +  | AQuant (q, (x, _) :: xs, phi') =>
    9.87 +    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
    9.88 +           quant_T)
    9.89 +    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
    9.90 +  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
    9.91 +  | AConn (c, [u1, u2]) =>
    9.92 +    pairself hol_prop_from_formula (u1, u2)
    9.93 +    |> (case c of
    9.94 +          AAnd => HOLogic.mk_conj
    9.95 +        | AOr => HOLogic.mk_disj
    9.96 +        | AImplies => HOLogic.mk_imp
    9.97 +        | AIff => HOLogic.mk_eq
    9.98 +        | ANot => raise Fail "binary \"ANot\"")
    9.99 +  | AConn _ => raise Fail "malformed AConn"
   9.100 +  | AAtom u => hol_term_from_fo_term bool_T u
   9.101 +
   9.102 +fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
   9.103 +
   9.104 +fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
   9.105 +
   9.106 +fun pick_nits_in_tptp_file file_name =
   9.107 +  case parse_tptp_problem (File.read (Path.explode file_name)) of
   9.108 +    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
   9.109 +  | (phis, []) =>
   9.110 +    let
   9.111 +      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
   9.112 +                    o hol_prop_from_formula) phis
   9.113 +(*
   9.114 +      val _ = warning (PolyML.makestring phis)
   9.115 +      val _ = app (warning o Syntax.string_of_term @{context}) ts
   9.116 +*)
   9.117 +      val state = Proof.init @{context}
   9.118 +      val params =
   9.119 +        [("card iota", "1\<emdash>100"),
   9.120 +         ("card", "1\<emdash>8"),
   9.121 +         ("box", "false"),
   9.122 +         ("sat_solver", "smart"),
   9.123 +         ("max_threads", "1"),
   9.124 +         ("batch_size", "10"),
   9.125 +         (* ("debug", "true"), *)
   9.126 +         ("verbose", "true"),
   9.127 +         (* ("overlord", "true"), *)
   9.128 +         ("show_consts", "true"),
   9.129 +         ("format", "1000"),
   9.130 +         ("max_potential", "0"),
   9.131 +         ("timeout", "none"),
   9.132 +         ("expect", genuineN)]
   9.133 +        |> default_params @{theory}
   9.134 +      val i = 1
   9.135 +      val n = 1
   9.136 +      val step = 0
   9.137 +      val subst = []
   9.138 +    in
   9.139 +      pick_nits_in_term state params Normal i n step subst ts @{prop False}
   9.140 +      |> fst
   9.141 +    end
   9.142 +
   9.143 +end;
    10.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML	Mon Jan 23 17:40:31 2012 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,140 +0,0 @@
    10.4 -(*  Title:      HOL/Tools/Nitpick/nitrox.ML
    10.5 -    Author:     Jasmin Blanchette, TU Muenchen
    10.6 -    Copyright   2010, 2011
    10.7 -
    10.8 -Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.
    10.9 -*)
   10.10 -
   10.11 -signature NITROX =
   10.12 -sig
   10.13 -  val pick_nits_in_fof_file : string -> string
   10.14 -end;
   10.15 -
   10.16 -structure Nitrox : NITROX =
   10.17 -struct
   10.18 -
   10.19 -open ATP_Util
   10.20 -open ATP_Problem
   10.21 -open ATP_Proof
   10.22 -open Nitpick_Util
   10.23 -open Nitpick
   10.24 -open Nitpick_Isar
   10.25 -
   10.26 -exception SYNTAX of string
   10.27 -
   10.28 -val tptp_explode = raw_explode o strip_spaces_except_between_idents
   10.29 -
   10.30 -fun parse_file_path (c :: ss) =
   10.31 -    if c = "'" orelse c = "\"" then
   10.32 -      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
   10.33 -    else
   10.34 -      raise SYNTAX "invalid file path"
   10.35 -  | parse_file_path [] = raise SYNTAX "invalid file path"
   10.36 -
   10.37 -fun parse_include x =
   10.38 -  let
   10.39 -    val (file_name, rest) =
   10.40 -      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
   10.41 -       --| $$ ".") x
   10.42 -    val path = file_name |> Path.explode
   10.43 -    val path =
   10.44 -      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
   10.45 -  in ((), (path |> File.read |> tptp_explode) @ rest) end
   10.46 -
   10.47 -val parse_fof_or_cnf =
   10.48 -  (Scan.this_string "fof" || Scan.this_string "cnf") |-- $$ "(" |--
   10.49 -  Scan.many (not_equal ",") |-- $$ "," |--
   10.50 -  (Scan.this_string "axiom" || Scan.this_string "definition"
   10.51 -   || Scan.this_string "theorem" || Scan.this_string "lemma"
   10.52 -   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
   10.53 -   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
   10.54 -      --| $$ ")" --| $$ "."
   10.55 -  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
   10.56 -
   10.57 -val parse_problem =
   10.58 -  Scan.repeat parse_include
   10.59 -  |-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include)
   10.60 -
   10.61 -val parse_tptp_problem =
   10.62 -  Scan.finite Symbol.stopper
   10.63 -      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
   10.64 -                  parse_problem))
   10.65 -  o tptp_explode
   10.66 -
   10.67 -val iota_T = @{typ iota}
   10.68 -val quant_T = (iota_T --> bool_T) --> bool_T
   10.69 -
   10.70 -fun is_variable s = Char.isUpper (String.sub (s, 0))
   10.71 -
   10.72 -fun hol_term_from_fo_term res_T (ATerm (x, us)) =
   10.73 -  let val ts = map (hol_term_from_fo_term iota_T) us in
   10.74 -    list_comb ((case x of
   10.75 -                  "$true" => @{const_name True}
   10.76 -                | "$false" => @{const_name False}
   10.77 -                | "=" => @{const_name HOL.eq}
   10.78 -                | "equal" => @{const_name HOL.eq}
   10.79 -                | _ => x, map fastype_of ts ---> res_T)
   10.80 -               |> (if is_variable x then Free else Const), ts)
   10.81 -  end
   10.82 -
   10.83 -fun hol_prop_from_formula phi =
   10.84 -  case phi of
   10.85 -    AQuant (_, [], phi') => hol_prop_from_formula phi'
   10.86 -  | AQuant (q, (x, _) :: xs, phi') =>
   10.87 -    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
   10.88 -           quant_T)
   10.89 -    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
   10.90 -  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
   10.91 -  | AConn (c, [u1, u2]) =>
   10.92 -    pairself hol_prop_from_formula (u1, u2)
   10.93 -    |> (case c of
   10.94 -          AAnd => HOLogic.mk_conj
   10.95 -        | AOr => HOLogic.mk_disj
   10.96 -        | AImplies => HOLogic.mk_imp
   10.97 -        | AIff => HOLogic.mk_eq
   10.98 -        | ANot => raise Fail "binary \"ANot\"")
   10.99 -  | AConn _ => raise Fail "malformed AConn"
  10.100 -  | AAtom u => hol_term_from_fo_term bool_T u
  10.101 -
  10.102 -fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
  10.103 -
  10.104 -fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
  10.105 -
  10.106 -fun pick_nits_in_fof_file file_name =
  10.107 -  case parse_tptp_problem (File.read (Path.explode file_name)) of
  10.108 -    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
  10.109 -  | (phis, []) =>
  10.110 -    let
  10.111 -      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
  10.112 -                    o hol_prop_from_formula) phis
  10.113 -(*
  10.114 -      val _ = warning (PolyML.makestring phis)
  10.115 -      val _ = app (warning o Syntax.string_of_term @{context}) ts
  10.116 -*)
  10.117 -      val state = Proof.init @{context}
  10.118 -      val params =
  10.119 -        [("card iota", "1\<emdash>100"),
  10.120 -         ("card", "1\<emdash>8"),
  10.121 -         ("box", "false"),
  10.122 -         ("sat_solver", "smart"),
  10.123 -         ("max_threads", "1"),
  10.124 -         ("batch_size", "10"),
  10.125 -         (* ("debug", "true"), *)
  10.126 -         ("verbose", "true"),
  10.127 -         (* ("overlord", "true"), *)
  10.128 -         ("show_consts", "true"),
  10.129 -         ("format", "1000"),
  10.130 -         ("max_potential", "0"),
  10.131 -         ("timeout", "none"),
  10.132 -         ("expect", genuineN)]
  10.133 -        |> default_params @{theory}
  10.134 -      val i = 1
  10.135 -      val n = 1
  10.136 -      val step = 0
  10.137 -      val subst = []
  10.138 -    in
  10.139 -      pick_nits_in_term state params Normal i n step subst ts @{prop False}
  10.140 -      |> fst
  10.141 -    end
  10.142 -
  10.143 -end;