src/HOL/Tools/Nitpick/nitpick_tptp.ML
author blanchet
Mon Jan 23 17:40:31 2012 +0100 (2012-01-23)
changeset 46319 c248e4f1be74
parent 46113 src/HOL/Tools/Nitpick/nitrox.ML@dd112cd72c48
permissions -rw-r--r--
rebranded Nitrox, for more uniformity
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_tptp.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2010, 2011
     4 
     5 Nitpick for TPTP.
     6 *)
     7 
     8 signature NITPICK_TPTP =
     9 sig
    10   val pick_nits_in_tptp_file : string -> string
    11 end;
    12 
    13 structure Nitpick_TPTP : NITPICK_TPTP =
    14 struct
    15 
    16 open ATP_Util
    17 open ATP_Problem
    18 open ATP_Proof
    19 open Nitpick_Util
    20 open Nitpick
    21 open Nitpick_Isar
    22 
    23 exception SYNTAX of string
    24 
    25 val tptp_explode = raw_explode o strip_spaces_except_between_idents
    26 
    27 fun parse_file_path (c :: ss) =
    28     if c = "'" orelse c = "\"" then
    29       ss |> chop_while (curry (op <>) c) |>> implode ||> tl
    30     else
    31       raise SYNTAX "invalid file path"
    32   | parse_file_path [] = raise SYNTAX "invalid file path"
    33 
    34 fun parse_include x =
    35   let
    36     val (file_name, rest) =
    37       (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
    38        --| $$ ".") x
    39     val path = file_name |> Path.explode
    40     val path =
    41       path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
    42   in ((), (path |> File.read |> tptp_explode) @ rest) end
    43 
    44 val parse_cnf_or_fof =
    45   (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
    46   Scan.many (not_equal ",") |-- $$ "," |--
    47   (Scan.this_string "axiom" || Scan.this_string "definition"
    48    || Scan.this_string "theorem" || Scan.this_string "lemma"
    49    || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    50    || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
    51       --| $$ ")" --| $$ "."
    52   >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
    53 
    54 val parse_problem =
    55   Scan.repeat parse_include
    56   |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
    57 
    58 val parse_tptp_problem =
    59   Scan.finite Symbol.stopper
    60       (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
    61                   parse_problem))
    62   o tptp_explode
    63 
    64 val iota_T = @{typ iota}
    65 val quant_T = (iota_T --> bool_T) --> bool_T
    66 
    67 fun is_variable s = Char.isUpper (String.sub (s, 0))
    68 
    69 fun hol_term_from_fo_term res_T (ATerm (x, us)) =
    70   let val ts = map (hol_term_from_fo_term iota_T) us in
    71     list_comb ((case x of
    72                   "$true" => @{const_name True}
    73                 | "$false" => @{const_name False}
    74                 | "=" => @{const_name HOL.eq}
    75                 | "equal" => @{const_name HOL.eq}
    76                 | _ => x, map fastype_of ts ---> res_T)
    77                |> (if is_variable x then Free else Const), ts)
    78   end
    79 
    80 fun hol_prop_from_formula phi =
    81   case phi of
    82     AQuant (_, [], phi') => hol_prop_from_formula phi'
    83   | AQuant (q, (x, _) :: xs, phi') =>
    84     Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
    85            quant_T)
    86     $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
    87   | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
    88   | AConn (c, [u1, u2]) =>
    89     pairself hol_prop_from_formula (u1, u2)
    90     |> (case c of
    91           AAnd => HOLogic.mk_conj
    92         | AOr => HOLogic.mk_disj
    93         | AImplies => HOLogic.mk_imp
    94         | AIff => HOLogic.mk_eq
    95         | ANot => raise Fail "binary \"ANot\"")
    96   | AConn _ => raise Fail "malformed AConn"
    97   | AAtom u => hol_term_from_fo_term bool_T u
    98 
    99 fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
   100 
   101 fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
   102 
   103 fun pick_nits_in_tptp_file file_name =
   104   case parse_tptp_problem (File.read (Path.explode file_name)) of
   105     (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
   106   | (phis, []) =>
   107     let
   108       val ts = map (HOLogic.mk_Trueprop o close_hol_prop
   109                     o hol_prop_from_formula) phis
   110 (*
   111       val _ = warning (PolyML.makestring phis)
   112       val _ = app (warning o Syntax.string_of_term @{context}) ts
   113 *)
   114       val state = Proof.init @{context}
   115       val params =
   116         [("card iota", "1\<emdash>100"),
   117          ("card", "1\<emdash>8"),
   118          ("box", "false"),
   119          ("sat_solver", "smart"),
   120          ("max_threads", "1"),
   121          ("batch_size", "10"),
   122          (* ("debug", "true"), *)
   123          ("verbose", "true"),
   124          (* ("overlord", "true"), *)
   125          ("show_consts", "true"),
   126          ("format", "1000"),
   127          ("max_potential", "0"),
   128          ("timeout", "none"),
   129          ("expect", genuineN)]
   130         |> default_params @{theory}
   131       val i = 1
   132       val n = 1
   133       val step = 0
   134       val subst = []
   135     in
   136       pick_nits_in_term state params Normal i n step subst ts @{prop False}
   137       |> fst
   138     end
   139 
   140 end;