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