(*  Title:      HOL/Tools/Nitpick/nitrox.ML

    Author:     Jasmin Blanchette, TU Muenchen

    Copyright   2010, 2011

Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.

*)

signature NITROX =

sig

  val pick_nits_in_fof_file : string -> string

end;

structure Nitrox : NITROX =

struct

open ATP_Util

open ATP_Problem

open ATP_Proof

open Nitpick

open Nitpick_Isar

exception SYNTAX of string

val parse_keyword = Scan.this_string

fun parse_file_path (c :: ss) =

    if c = "'" orelse c = "\"" then

      ss |> chop_while (curry (op <>) c) |>> implode ||> tl

    else

      raise SYNTAX "invalid file path"

  | parse_file_path [] = raise SYNTAX "invalid file path"

fun parse_include x =

  let

    val (file_name, rest) =

      (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"

       --| $$ ".") x

  in

    ((), (file_name |> Path.explode |> File.read

                    |> strip_spaces true (K true)

                    |> raw_explode) @ rest)

  end

val parse_fof_or_cnf =

  (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--

  Scan.many (not_equal ",") |-- $$ "," |--

  (parse_keyword "axiom" || parse_keyword "definition"

   || parse_keyword "theorem" || parse_keyword "lemma"

   || parse_keyword "hypothesis" || parse_keyword "conjecture"

   || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula

      --| $$ ")" --| $$ "."

  >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)

val parse_problem =

  Scan.repeat parse_include

  |-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include)

val parse_tptp_problem =

  Scan.finite Symbol.stopper

      (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")

                  parse_problem))

  o raw_explode o strip_spaces true (K true)

val boolT = @{typ bool}

val iotaT = @{typ iota}

val quantT = (iotaT --> boolT) --> boolT

fun is_variable s = Char.isUpper (String.sub (s, 0))

fun hol_term_from_fo_term res_T (ATerm (x, us)) =

  let val ts = map (hol_term_from_fo_term iotaT) us in

    list_comb ((case x of

                  "$true" => @{const_name True}

                | "$false" => @{const_name False}

                | "=" => @{const_name HOL.eq}

                | _ => x, map fastype_of ts ---> res_T)

               |> (if is_variable x then Free else Const), ts)

  end

fun hol_prop_from_formula phi =

  case phi of

    AQuant (_, [], phi') => hol_prop_from_formula phi'

  | AQuant (q, (x, _) :: xs, phi') =>

    Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},

           quantT)

    $ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi')))

  | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')

  | AConn (c, [u1, u2]) =>

    pairself hol_prop_from_formula (u1, u2)

    |> (case c of

          AAnd => HOLogic.mk_conj

        | AOr => HOLogic.mk_disj

        | AImplies => HOLogic.mk_imp

        | AIf => HOLogic.mk_imp o swap

        | AIff => HOLogic.mk_eq

        | ANotIff => HOLogic.mk_not o HOLogic.mk_eq

        | ANot => raise Fail "binary \"ANot\"")

  | AConn _ => raise Fail "malformed AConn"

  | AAtom u => hol_term_from_fo_term boolT u

fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t

fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t

fun pick_nits_in_fof_file file_name =

  case parse_tptp_problem (File.read (Path.explode file_name)) of

    (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))

  | (phis, []) =>

    let

      val ts = map (HOLogic.mk_Trueprop o close_hol_prop

                    o hol_prop_from_formula) phis

(*

      val _ = warning (PolyML.makestring phis)

      val _ = app (warning o Syntax.string_of_term @{context}) ts

*)

      val state = Proof.init @{context}

      val params =

        [("card", "1\<emdash>8"),

         ("box", "false"),

         ("sat_solver", "smart"),

         ("max_threads", "1"),

         ("batch_size", "10"),

         (* ("debug", "true"), *)

         ("verbose", "true"),

         (* ("overlord", "true"), *)

         ("show_consts", "true"),

         ("format", "1000"),

         ("max_potential", "0"),

         (* ("timeout", "240 s"), *)

         ("expect", genuineN)]

        |> default_params @{theory}

      val i = 1

      val n = 1

      val step = 0

      val subst = []

    in

      pick_nits_in_term state params Normal i n step subst ts @{prop False}

      |> fst

    end

end;