src/HOL/Tools/Nitpick/nitpick_tptp.ML
changeset 46319 c248e4f1be74
parent 46113 dd112cd72c48
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tptp.ML	Mon Jan 23 17:40:31 2012 +0100
     1.3 @@ -0,0 +1,140 @@
     1.4 +(*  Title:      HOL/Tools/Nitpick/nitpick_tptp.ML
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2010, 2011
     1.7 +
     1.8 +Nitpick for TPTP.
     1.9 +*)
    1.10 +
    1.11 +signature NITPICK_TPTP =
    1.12 +sig
    1.13 +  val pick_nits_in_tptp_file : string -> string
    1.14 +end;
    1.15 +
    1.16 +structure Nitpick_TPTP : NITPICK_TPTP =
    1.17 +struct
    1.18 +
    1.19 +open ATP_Util
    1.20 +open ATP_Problem
    1.21 +open ATP_Proof
    1.22 +open Nitpick_Util
    1.23 +open Nitpick
    1.24 +open Nitpick_Isar
    1.25 +
    1.26 +exception SYNTAX of string
    1.27 +
    1.28 +val tptp_explode = raw_explode o strip_spaces_except_between_idents
    1.29 +
    1.30 +fun parse_file_path (c :: ss) =
    1.31 +    if c = "'" orelse c = "\"" then
    1.32 +      ss |> chop_while (curry (op <>) c) |>> implode ||> tl
    1.33 +    else
    1.34 +      raise SYNTAX "invalid file path"
    1.35 +  | parse_file_path [] = raise SYNTAX "invalid file path"
    1.36 +
    1.37 +fun parse_include x =
    1.38 +  let
    1.39 +    val (file_name, rest) =
    1.40 +      (Scan.this_string "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
    1.41 +       --| $$ ".") x
    1.42 +    val path = file_name |> Path.explode
    1.43 +    val path =
    1.44 +      path |> not (Path.is_absolute path) ? Path.append (Path.explode "$TPTP")
    1.45 +  in ((), (path |> File.read |> tptp_explode) @ rest) end
    1.46 +
    1.47 +val parse_cnf_or_fof =
    1.48 +  (Scan.this_string "cnf" || Scan.this_string "fof") |-- $$ "(" |--
    1.49 +  Scan.many (not_equal ",") |-- $$ "," |--
    1.50 +  (Scan.this_string "axiom" || Scan.this_string "definition"
    1.51 +   || Scan.this_string "theorem" || Scan.this_string "lemma"
    1.52 +   || Scan.this_string "hypothesis" || Scan.this_string "conjecture"
    1.53 +   || Scan.this_string "negated_conjecture") --| $$ "," -- parse_formula
    1.54 +      --| $$ ")" --| $$ "."
    1.55 +  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
    1.56 +
    1.57 +val parse_problem =
    1.58 +  Scan.repeat parse_include
    1.59 +  |-- Scan.repeat (parse_cnf_or_fof --| Scan.repeat parse_include)
    1.60 +
    1.61 +val parse_tptp_problem =
    1.62 +  Scan.finite Symbol.stopper
    1.63 +      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
    1.64 +                  parse_problem))
    1.65 +  o tptp_explode
    1.66 +
    1.67 +val iota_T = @{typ iota}
    1.68 +val quant_T = (iota_T --> bool_T) --> bool_T
    1.69 +
    1.70 +fun is_variable s = Char.isUpper (String.sub (s, 0))
    1.71 +
    1.72 +fun hol_term_from_fo_term res_T (ATerm (x, us)) =
    1.73 +  let val ts = map (hol_term_from_fo_term iota_T) us in
    1.74 +    list_comb ((case x of
    1.75 +                  "$true" => @{const_name True}
    1.76 +                | "$false" => @{const_name False}
    1.77 +                | "=" => @{const_name HOL.eq}
    1.78 +                | "equal" => @{const_name HOL.eq}
    1.79 +                | _ => x, map fastype_of ts ---> res_T)
    1.80 +               |> (if is_variable x then Free else Const), ts)
    1.81 +  end
    1.82 +
    1.83 +fun hol_prop_from_formula phi =
    1.84 +  case phi of
    1.85 +    AQuant (_, [], phi') => hol_prop_from_formula phi'
    1.86 +  | AQuant (q, (x, _) :: xs, phi') =>
    1.87 +    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
    1.88 +           quant_T)
    1.89 +    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
    1.90 +  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
    1.91 +  | AConn (c, [u1, u2]) =>
    1.92 +    pairself hol_prop_from_formula (u1, u2)
    1.93 +    |> (case c of
    1.94 +          AAnd => HOLogic.mk_conj
    1.95 +        | AOr => HOLogic.mk_disj
    1.96 +        | AImplies => HOLogic.mk_imp
    1.97 +        | AIff => HOLogic.mk_eq
    1.98 +        | ANot => raise Fail "binary \"ANot\"")
    1.99 +  | AConn _ => raise Fail "malformed AConn"
   1.100 +  | AAtom u => hol_term_from_fo_term bool_T u
   1.101 +
   1.102 +fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
   1.103 +
   1.104 +fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
   1.105 +
   1.106 +fun pick_nits_in_tptp_file file_name =
   1.107 +  case parse_tptp_problem (File.read (Path.explode file_name)) of
   1.108 +    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
   1.109 +  | (phis, []) =>
   1.110 +    let
   1.111 +      val ts = map (HOLogic.mk_Trueprop o close_hol_prop
   1.112 +                    o hol_prop_from_formula) phis
   1.113 +(*
   1.114 +      val _ = warning (PolyML.makestring phis)
   1.115 +      val _ = app (warning o Syntax.string_of_term @{context}) ts
   1.116 +*)
   1.117 +      val state = Proof.init @{context}
   1.118 +      val params =
   1.119 +        [("card iota", "1\<emdash>100"),
   1.120 +         ("card", "1\<emdash>8"),
   1.121 +         ("box", "false"),
   1.122 +         ("sat_solver", "smart"),
   1.123 +         ("max_threads", "1"),
   1.124 +         ("batch_size", "10"),
   1.125 +         (* ("debug", "true"), *)
   1.126 +         ("verbose", "true"),
   1.127 +         (* ("overlord", "true"), *)
   1.128 +         ("show_consts", "true"),
   1.129 +         ("format", "1000"),
   1.130 +         ("max_potential", "0"),
   1.131 +         ("timeout", "none"),
   1.132 +         ("expect", genuineN)]
   1.133 +        |> default_params @{theory}
   1.134 +      val i = 1
   1.135 +      val n = 1
   1.136 +      val step = 0
   1.137 +      val subst = []
   1.138 +    in
   1.139 +      pick_nits_in_term state params Normal i n step subst ts @{prop False}
   1.140 +      |> fst
   1.141 +    end
   1.142 +
   1.143 +end;