|
1 (* Title: HOL/Tools/Nitpick/nitrox.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2010, 2011 |
|
4 |
|
5 Finite model generation for TPTP first-order formulas via Nitpick. |
|
6 *) |
|
7 |
|
8 signature NITROX = |
|
9 sig |
|
10 val pick_nits_in_fof_file : string -> string |
|
11 end; |
|
12 |
|
13 structure Nitrox : NITROX = |
|
14 struct |
|
15 |
|
16 datatype 'a fo_term = ATerm of 'a * 'a fo_term list |
|
17 datatype quantifier = AForall | AExists |
|
18 datatype connective = ANot | AAnd | AOr | AImplies | AIf | AIff | ANotIff |
|
19 datatype 'a formula = |
|
20 AQuant of quantifier * 'a list * 'a formula | |
|
21 AConn of connective * 'a formula list | |
|
22 APred of 'a fo_term |
|
23 |
|
24 exception SYNTAX of string |
|
25 |
|
26 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
|
27 |
|
28 fun takewhile _ [] = [] |
|
29 | takewhile p (x :: xs) = if p x then x :: takewhile p xs else [] |
|
30 |
|
31 fun dropwhile _ [] = [] |
|
32 | dropwhile p (x :: xs) = if p x then dropwhile p xs else x :: xs |
|
33 |
|
34 fun strip_c_style_comment [] = "" |
|
35 | strip_c_style_comment (#"*" :: #"/" :: cs) = strip_spaces_in_list cs |
|
36 | strip_c_style_comment (_ :: cs) = strip_c_style_comment cs |
|
37 and strip_spaces_in_list [] = "" |
|
38 | strip_spaces_in_list (#"%" :: cs) = |
|
39 strip_spaces_in_list (dropwhile (not_equal #"\n") cs) |
|
40 | strip_spaces_in_list (#"/" :: #"*" :: cs) = strip_c_style_comment cs |
|
41 | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 |
|
42 | strip_spaces_in_list [c1, c2] = |
|
43 strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] |
|
44 | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = |
|
45 if Char.isSpace c1 then |
|
46 strip_spaces_in_list (c2 :: c3 :: cs) |
|
47 else if Char.isSpace c2 then |
|
48 if Char.isSpace c3 then |
|
49 strip_spaces_in_list (c1 :: c3 :: cs) |
|
50 else |
|
51 str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ |
|
52 strip_spaces_in_list (c3 :: cs) |
|
53 else |
|
54 str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) |
|
55 val strip_spaces = strip_spaces_in_list o String.explode |
|
56 |
|
57 val parse_keyword = Scan.this_string |
|
58 |
|
59 fun parse_file_path ("'" :: ss) = |
|
60 (takewhile (not_equal "'") ss |> implode, |
|
61 List.drop (dropwhile (not_equal "'") ss, 1)) |
|
62 | parse_file_path ("\"" :: ss) = |
|
63 (takewhile (not_equal "\"") ss |> implode, |
|
64 List.drop (dropwhile (not_equal "\"") ss, 1)) |
|
65 | parse_file_path _ = raise SYNTAX "invalid file path" |
|
66 |
|
67 fun parse_include x = |
|
68 let |
|
69 val (file_name, rest) = |
|
70 (parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")" |
|
71 --| $$ ".") x |
|
72 in |
|
73 ((), raw_explode (strip_spaces (File.read (Path.explode file_name))) @ rest) |
|
74 end |
|
75 |
|
76 fun mk_anot phi = AConn (ANot, [phi]) |
|
77 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) |
|
78 |
|
79 val parse_dollar_name = |
|
80 Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s) |
|
81 |
|
82 fun parse_term x = |
|
83 (parse_dollar_name |
|
84 -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> ATerm) x |
|
85 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x |
|
86 |
|
87 (* Apply equal or not-equal to a term. *) |
|
88 val parse_predicate_term = |
|
89 parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term) |
|
90 >> (fn (u, NONE) => APred u |
|
91 | (u1, SOME (NONE, u2)) => APred (ATerm ("=", [u1, u2])) |
|
92 | (u1, SOME (SOME _, u2)) => mk_anot (APred (ATerm ("=", [u1, u2])))) |
|
93 |
|
94 fun fo_term_head (ATerm (s, _)) = s |
|
95 |
|
96 fun parse_formula x = |
|
97 (($$ "(" |-- parse_formula --| $$ ")" |
|
98 || ($$ "!" >> K AForall || $$ "?" >> K AExists) |
|
99 --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula |
|
100 >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi)) |
|
101 || $$ "~" |-- parse_formula >> mk_anot |
|
102 || parse_predicate_term) |
|
103 -- Scan.option ((Scan.this_string "=>" >> K AImplies |
|
104 || Scan.this_string "<=>" >> K AIff |
|
105 || Scan.this_string "<~>" >> K ANotIff |
|
106 || Scan.this_string "<=" >> K AIf |
|
107 || $$ "|" >> K AOr || $$ "&" >> K AAnd) -- parse_formula) |
|
108 >> (fn (phi1, NONE) => phi1 |
|
109 | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x |
|
110 |
|
111 val parse_fof_or_cnf = |
|
112 (parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |-- |
|
113 Scan.many (not_equal ",") |-- $$ "," |-- |
|
114 (parse_keyword "axiom" || parse_keyword "definition" |
|
115 || parse_keyword "theorem" || parse_keyword "lemma" |
|
116 || parse_keyword "hypothesis" || parse_keyword "conjecture" |
|
117 || parse_keyword "negated_conjecture") --| $$ "," -- parse_formula |
|
118 --| $$ ")" --| $$ "." |
|
119 >> (fn ("conjecture", phi) => AConn (ANot, [phi]) | (_, phi) => phi) |
|
120 |
|
121 val parse_problem = |
|
122 Scan.repeat parse_include |
|
123 |-- Scan.repeat (parse_fof_or_cnf --| Scan.repeat parse_include) |
|
124 |
|
125 val parse_tptp_problem = |
|
126 Scan.finite Symbol.stopper |
|
127 (Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input") |
|
128 parse_problem)) |
|
129 o raw_explode o strip_spaces |
|
130 |
|
131 val boolT = @{typ bool} |
|
132 val iotaT = @{typ iota} |
|
133 val quantT = (iotaT --> boolT) --> boolT |
|
134 |
|
135 fun is_variable s = Char.isUpper (String.sub (s, 0)) |
|
136 |
|
137 fun hol_term_from_fo_term res_T (ATerm (x, us)) = |
|
138 let val ts = map (hol_term_from_fo_term iotaT) us in |
|
139 list_comb ((case x of |
|
140 "$true" => @{const_name True} |
|
141 | "$false" => @{const_name False} |
|
142 | "=" => @{const_name HOL.eq} |
|
143 | _ => x, map fastype_of ts ---> res_T) |
|
144 |> (if is_variable x then Free else Const), ts) |
|
145 end |
|
146 |
|
147 fun hol_prop_from_formula phi = |
|
148 case phi of |
|
149 AQuant (_, [], phi') => hol_prop_from_formula phi' |
|
150 | AQuant (q, x :: xs, phi') => |
|
151 Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex}, |
|
152 quantT) |
|
153 $ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi'))) |
|
154 | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u') |
|
155 | AConn (c, [u1, u2]) => |
|
156 pairself hol_prop_from_formula (u1, u2) |
|
157 |> (case c of |
|
158 AAnd => HOLogic.mk_conj |
|
159 | AOr => HOLogic.mk_disj |
|
160 | AImplies => HOLogic.mk_imp |
|
161 | AIf => HOLogic.mk_imp o swap |
|
162 | AIff => HOLogic.mk_eq |
|
163 | ANotIff => HOLogic.mk_not o HOLogic.mk_eq |
|
164 | ANot => raise Fail "binary \"ANot\"") |
|
165 | AConn _ => raise Fail "malformed AConn" |
|
166 | APred u => hol_term_from_fo_term boolT u |
|
167 |
|
168 fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t |
|
169 |
|
170 fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t |
|
171 |
|
172 fun pick_nits_in_fof_file file_name = |
|
173 case parse_tptp_problem (File.read (Path.explode file_name)) of |
|
174 (_, s :: ss) => raise SYNTAX ("cannot parse " ^ quote (implode (s :: ss))) |
|
175 | (phis, []) => |
|
176 let |
|
177 val ts = map (HOLogic.mk_Trueprop o close_hol_prop |
|
178 o hol_prop_from_formula) phis |
|
179 (* |
|
180 val _ = warning (PolyML.makestring phis) |
|
181 val _ = app (warning o Syntax.string_of_term @{context}) ts |
|
182 *) |
|
183 val state = Proof.init @{context} |
|
184 val params = |
|
185 [("card iota", "1\<midarrow>100"), |
|
186 ("card", "1\<midarrow>8"), |
|
187 ("box", "false"), |
|
188 ("sat_solver", "smart"), |
|
189 ("max_threads", "1"), |
|
190 ("batch_size", "10"), |
|
191 (* ("debug", "true"), *) |
|
192 ("verbose", "true"), |
|
193 (* ("overlord", "true"), *) |
|
194 ("show_consts", "true"), |
|
195 ("format", "1000"), |
|
196 ("max_potential", "0"), |
|
197 (* ("timeout", "240 s"), *) |
|
198 ("expect", "genuine")] |
|
199 |> Nitpick_Isar.default_params @{theory} |
|
200 val auto = false |
|
201 val i = 1 |
|
202 val n = 1 |
|
203 val step = 0 |
|
204 val subst = [] |
|
205 in |
|
206 Nitpick.pick_nits_in_term state params auto i n step subst ts |
|
207 @{prop False} |> fst |
|
208 end |
|
209 |
|
210 end; |