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