src/HOL/Tools/Nitpick/nitrox.ML
changeset 46319 c248e4f1be74
parent 46318 8038d050ff15
child 46320 0b8b73b49848
     1.1 --- a/src/HOL/Tools/Nitpick/nitrox.ML	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,140 +0,0 @@
     1.4 -(*  Title:      HOL/Tools/Nitpick/nitrox.ML
     1.5 -    Author:     Jasmin Blanchette, TU Muenchen
     1.6 -    Copyright   2010, 2011
     1.7 -
     1.8 -Finite model generation for TPTP first-order formulas (FOF and CNF) via Nitpick.
     1.9 -*)
    1.10 -
    1.11 -signature NITROX =
    1.12 -sig
    1.13 -  val pick_nits_in_fof_file : string -> string
    1.14 -end;
    1.15 -
    1.16 -structure Nitrox : NITROX =
    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_fof_or_cnf =
    1.48 -  (Scan.this_string "fof" || Scan.this_string "cnf") |-- $$ "(" |--
    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_fof_or_cnf --| 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_fof_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;