blanchet@42919: (*  Title:      HOL/Tools/Nitpick/nitrox.ML
blanchet@42919:     Author:     Jasmin Blanchette, TU Muenchen
blanchet@42919:     Copyright   2010, 2011
blanchet@42919: 
blanchet@43800: Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.
blanchet@42919: *)
blanchet@42919: 
blanchet@42919: signature NITROX =
blanchet@42919: sig
blanchet@42919:   val pick_nits_in_fof_file : string -> string
blanchet@42919: end;
blanchet@42919: 
blanchet@42919: structure Nitrox : NITROX =
blanchet@42919: struct
blanchet@42919: 
blanchet@43801: open ATP_Problem
blanchet@43802: open ATP_Proof
blanchet@43863: open Nitpick
blanchet@43863: open Nitpick_Isar
blanchet@42919: 
blanchet@42919: exception SYNTAX of string
blanchet@42919: 
blanchet@42919: val parse_keyword = Scan.this_string
blanchet@42919: 
blanchet@43802: fun parse_file_path (c :: ss) =
blanchet@43802:     if c = "'" orelse c = "\"" then
blanchet@43802:       ss |> chop_while (curry (op <>) c) |>> implode ||> tl
blanchet@43802:     else
blanchet@43802:       raise SYNTAX "invalid file path"
blanchet@43802:   | parse_file_path [] = raise SYNTAX "invalid file path"
blanchet@42919: 
blanchet@42919: fun parse_include x =
blanchet@42919:   let
blanchet@42919:     val (file_name, rest) =
blanchet@42919:       (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
blanchet@42919:        --| $$ ".") x
blanchet@42919:   in
blanchet@43802:     ((), (file_name |> Path.explode |> File.read
blanchet@43802:                     |> strip_spaces true (K true)
blanchet@43802:                     |> raw_explode) @ rest)
blanchet@42919:   end
blanchet@42919: 
blanchet@42919: val parse_fof_or_cnf =
blanchet@42919:   (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
blanchet@42919:   Scan.many (not_equal ",") |-- $$ "," |--
blanchet@42919:   (parse_keyword "axiom" || parse_keyword "definition"
blanchet@42919:    || parse_keyword "theorem" || parse_keyword "lemma"
blanchet@42919:    || parse_keyword "hypothesis" || parse_keyword "conjecture"
blanchet@42919:    || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula
blanchet@42919:       --| $$ ")" --| $$ "."
blanchet@42919:   >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi)
blanchet@42919: 
blanchet@42919: val parse_problem =
blanchet@42919:   Scan.repeat parse_include
blanchet@42919:   |-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include)
blanchet@42919: 
blanchet@42919: val parse_tptp_problem =
blanchet@42919:   Scan.finite Symbol.stopper
blanchet@42919:       (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
blanchet@42919:                   parse_problem))
blanchet@43802:   o raw_explode o strip_spaces true (K true)
blanchet@42919: 
blanchet@42919: val boolT = @{typ bool}
blanchet@42919: val iotaT = @{typ iota}
blanchet@42919: val quantT = (iotaT --> boolT) --> boolT
blanchet@42919: 
blanchet@42919: fun is_variable s = Char.isUpper (String.sub (s, 0))
blanchet@42919: 
blanchet@42919: fun hol_term_from_fo_term res_T (ATerm (x, us)) =
blanchet@42919:   let val ts = map (hol_term_from_fo_term iotaT) us in
blanchet@42919:     list_comb ((case x of
blanchet@42919:                   "$true" => @{const_name True}
blanchet@42919:                 | "$false" => @{const_name False}
blanchet@42919:                 | "=" => @{const_name HOL.eq}
blanchet@42919:                 | _ => x, map fastype_of ts ---> res_T)
blanchet@42919:                |> (if is_variable x then Free else Const), ts)
blanchet@42919:   end
blanchet@42919: 
blanchet@42919: fun hol_prop_from_formula phi =
blanchet@42919:   case phi of
blanchet@42919:     AQuant (_, [], phi') => hol_prop_from_formula phi'
blanchet@43801:   | AQuant (q, (x, _) :: xs, phi') =>
blanchet@42919:     Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
blanchet@42919:            quantT)
blanchet@42919:     $ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi')))
blanchet@42919:   | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
blanchet@42919:   | AConn (c, [u1, u2]) =>
blanchet@42919:     pairself hol_prop_from_formula (u1, u2)
blanchet@42919:     |> (case c of
blanchet@42919:           AAnd => HOLogic.mk_conj
blanchet@42919:         | AOr => HOLogic.mk_disj
blanchet@42919:         | AImplies => HOLogic.mk_imp
blanchet@42919:         | AIf => HOLogic.mk_imp o swap
blanchet@42919:         | AIff => HOLogic.mk_eq
blanchet@42919:         | ANotIff => HOLogic.mk_not o HOLogic.mk_eq
blanchet@42919:         | ANot => raise Fail "binary \"ANot\"")
blanchet@42919:   | AConn _ => raise Fail "malformed AConn"
blanchet@43801:   | AAtom u => hol_term_from_fo_term boolT u
blanchet@42919: 
blanchet@42919: fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t
blanchet@42919: 
blanchet@42919: fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t
blanchet@42919: 
blanchet@42919: fun pick_nits_in_fof_file file_name =
blanchet@42919:   case parse_tptp_problem (File.read (Path.explode file_name)) of
blanchet@42919:     (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss)))
blanchet@42919:   | (phis, []) =>
blanchet@42919:     let
blanchet@42919:       val ts = map (HOLogic.mk_Trueprop o close_hol_prop
blanchet@42919:                     o hol_prop_from_formula) phis
blanchet@42919: (*
blanchet@42919:       val _ = warning (PolyML.makestring phis)
blanchet@42919:       val _ = app (warning o Syntax.string_of_term @{context}) ts
blanchet@42919: *)
blanchet@42919:       val state = Proof.init @{context}
blanchet@42919:       val params =
blanchet@43800:         [("card", "1\<emdash>8"),
blanchet@42919:          ("box", "false"),
blanchet@42919:          ("sat_solver", "smart"),
blanchet@42919:          ("max_threads", "1"),
blanchet@42919:          ("batch_size", "10"),
blanchet@42919:          (* ("debug", "true"), *)
blanchet@42919:          ("verbose", "true"),
blanchet@42919:          (* ("overlord", "true"), *)
blanchet@42919:          ("show_consts", "true"),
blanchet@42919:          ("format", "1000"),
blanchet@42919:          ("max_potential", "0"),
blanchet@42919:          (* ("timeout", "240 s"), *)
blanchet@43863:          ("expect", genuineN)]
blanchet@43863:         |> default_params @{theory}
blanchet@42919:       val i = 1
blanchet@42919:       val n = 1
blanchet@42919:       val step = 0
blanchet@42919:       val subst = []
blanchet@42919:     in
blanchet@43863:       pick_nits_in_term state params Normal i n step subst ts @{prop False}
blanchet@43863:       |> fst
blanchet@42919:     end
blanchet@42919: 
blanchet@42919: end;