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