45035
|
1 |
(* Title: HOL/Nitpick_Examples/minipick.ML
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
Copyright 2009-2010
|
|
4 |
|
|
5 |
Finite model generation for HOL formulas using Kodkod, minimalistic version.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature MINIPICK =
|
|
9 |
sig
|
|
10 |
datatype rep = S_Rep | R_Rep
|
|
11 |
type styp = Nitpick_Util.styp
|
|
12 |
|
|
13 |
val vars_for_bound_var :
|
|
14 |
(typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr list
|
|
15 |
val rel_expr_for_bound_var :
|
|
16 |
(typ -> int) -> rep -> typ list -> int -> Kodkod.rel_expr
|
|
17 |
val decls_for : rep -> (typ -> int) -> typ list -> typ -> Kodkod.decl list
|
|
18 |
val false_atom : Kodkod.rel_expr
|
|
19 |
val true_atom : Kodkod.rel_expr
|
|
20 |
val formula_from_atom : Kodkod.rel_expr -> Kodkod.formula
|
|
21 |
val atom_from_formula : Kodkod.formula -> Kodkod.rel_expr
|
|
22 |
val kodkod_problem_from_term :
|
|
23 |
Proof.context -> (typ -> int) -> term -> Kodkod.problem
|
|
24 |
val solve_any_kodkod_problem : theory -> Kodkod.problem list -> string
|
|
25 |
end;
|
|
26 |
|
|
27 |
structure Minipick : MINIPICK =
|
|
28 |
struct
|
|
29 |
|
|
30 |
open Kodkod
|
|
31 |
open Nitpick_Util
|
|
32 |
open Nitpick_HOL
|
|
33 |
open Nitpick_Peephole
|
|
34 |
open Nitpick_Kodkod
|
|
35 |
|
|
36 |
datatype rep = S_Rep | R_Rep
|
|
37 |
|
|
38 |
fun check_type ctxt (Type (@{type_name fun}, Ts)) =
|
|
39 |
List.app (check_type ctxt) Ts
|
|
40 |
| check_type ctxt (Type (@{type_name prod}, Ts)) =
|
|
41 |
List.app (check_type ctxt) Ts
|
|
42 |
| check_type _ @{typ bool} = ()
|
|
43 |
| check_type _ (TFree (_, @{sort "{}"})) = ()
|
|
44 |
| check_type _ (TFree (_, @{sort HOL.type})) = ()
|
|
45 |
| check_type ctxt T =
|
|
46 |
raise NOT_SUPPORTED ("type " ^ quote (Syntax.string_of_typ ctxt T))
|
|
47 |
|
|
48 |
fun atom_schema_of S_Rep card (Type (@{type_name fun}, [T1, T2])) =
|
|
49 |
replicate_list (card T1) (atom_schema_of S_Rep card T2)
|
|
50 |
| atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, @{typ bool}])) =
|
|
51 |
atom_schema_of S_Rep card T1
|
|
52 |
| atom_schema_of R_Rep card (Type (@{type_name fun}, [T1, T2])) =
|
|
53 |
atom_schema_of S_Rep card T1 @ atom_schema_of R_Rep card T2
|
|
54 |
| atom_schema_of _ card (Type (@{type_name prod}, Ts)) =
|
|
55 |
maps (atom_schema_of S_Rep card) Ts
|
|
56 |
| atom_schema_of _ card T = [card T]
|
|
57 |
val arity_of = length ooo atom_schema_of
|
|
58 |
|
|
59 |
fun index_for_bound_var _ [_] 0 = 0
|
|
60 |
| index_for_bound_var card (_ :: Ts) 0 =
|
|
61 |
index_for_bound_var card Ts 0 + arity_of S_Rep card (hd Ts)
|
|
62 |
| index_for_bound_var card Ts n = index_for_bound_var card (tl Ts) (n - 1)
|
|
63 |
fun vars_for_bound_var card R Ts j =
|
|
64 |
map (curry Var 1) (index_seq (index_for_bound_var card Ts j)
|
|
65 |
(arity_of R card (nth Ts j)))
|
|
66 |
val rel_expr_for_bound_var = foldl1 Product oooo vars_for_bound_var
|
|
67 |
fun decls_for R card Ts T =
|
|
68 |
map2 (curry DeclOne o pair 1)
|
|
69 |
(index_seq (index_for_bound_var card (T :: Ts) 0)
|
|
70 |
(arity_of R card (nth (T :: Ts) 0)))
|
|
71 |
(map (AtomSeq o rpair 0) (atom_schema_of R card T))
|
|
72 |
|
|
73 |
val atom_product = foldl1 Product o map Atom
|
|
74 |
|
|
75 |
val false_atom = Atom 0
|
|
76 |
val true_atom = Atom 1
|
|
77 |
|
|
78 |
fun formula_from_atom r = RelEq (r, true_atom)
|
|
79 |
fun atom_from_formula f = RelIf (f, true_atom, false_atom)
|
|
80 |
|
|
81 |
fun kodkod_formula_from_term ctxt card frees =
|
|
82 |
let
|
|
83 |
fun R_rep_from_S_rep (Type (@{type_name fun}, [T1, @{typ bool}])) r =
|
|
84 |
let
|
|
85 |
val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
|
|
86 |
|> all_combinations
|
|
87 |
in
|
|
88 |
map2 (fn i => fn js =>
|
|
89 |
RelIf (formula_from_atom (Project (r, [Num i])),
|
|
90 |
atom_product js, empty_n_ary_rel (length js)))
|
|
91 |
(index_seq 0 (length jss)) jss
|
|
92 |
|> foldl1 Union
|
|
93 |
end
|
|
94 |
| R_rep_from_S_rep (Type (@{type_name fun}, [T1, T2])) r =
|
|
95 |
let
|
|
96 |
val jss = atom_schema_of S_Rep card T1 |> map (rpair 0)
|
|
97 |
|> all_combinations
|
|
98 |
val arity2 = arity_of S_Rep card T2
|
|
99 |
in
|
|
100 |
map2 (fn i => fn js =>
|
|
101 |
Product (atom_product js,
|
|
102 |
Project (r, num_seq (i * arity2) arity2)
|
|
103 |
|> R_rep_from_S_rep T2))
|
|
104 |
(index_seq 0 (length jss)) jss
|
|
105 |
|> foldl1 Union
|
|
106 |
end
|
|
107 |
| R_rep_from_S_rep _ r = r
|
|
108 |
fun S_rep_from_R_rep Ts (T as Type (@{type_name fun}, _)) r =
|
|
109 |
Comprehension (decls_for S_Rep card Ts T,
|
|
110 |
RelEq (R_rep_from_S_rep T
|
|
111 |
(rel_expr_for_bound_var card S_Rep (T :: Ts) 0), r))
|
|
112 |
| S_rep_from_R_rep _ _ r = r
|
|
113 |
fun to_F Ts t =
|
|
114 |
(case t of
|
|
115 |
@{const Not} $ t1 => Not (to_F Ts t1)
|
|
116 |
| @{const False} => False
|
|
117 |
| @{const True} => True
|
|
118 |
| Const (@{const_name All}, _) $ Abs (_, T, t') =>
|
|
119 |
All (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
|
|
120 |
| (t0 as Const (@{const_name All}, _)) $ t1 =>
|
|
121 |
to_F Ts (t0 $ eta_expand Ts t1 1)
|
|
122 |
| Const (@{const_name Ex}, _) $ Abs (_, T, t') =>
|
|
123 |
Exist (decls_for S_Rep card Ts T, to_F (T :: Ts) t')
|
|
124 |
| (t0 as Const (@{const_name Ex}, _)) $ t1 =>
|
|
125 |
to_F Ts (t0 $ eta_expand Ts t1 1)
|
|
126 |
| Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
|
|
127 |
RelEq (to_R_rep Ts t1, to_R_rep Ts t2)
|
|
128 |
| Const (@{const_name ord_class.less_eq},
|
|
129 |
Type (@{type_name fun},
|
|
130 |
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
|
|
131 |
$ t1 $ t2 =>
|
|
132 |
Subset (to_R_rep Ts t1, to_R_rep Ts t2)
|
|
133 |
| @{const HOL.conj} $ t1 $ t2 => And (to_F Ts t1, to_F Ts t2)
|
|
134 |
| @{const HOL.disj} $ t1 $ t2 => Or (to_F Ts t1, to_F Ts t2)
|
|
135 |
| @{const HOL.implies} $ t1 $ t2 => Implies (to_F Ts t1, to_F Ts t2)
|
|
136 |
| t1 $ t2 => Subset (to_S_rep Ts t2, to_R_rep Ts t1)
|
|
137 |
| Free _ => raise SAME ()
|
|
138 |
| Term.Var _ => raise SAME ()
|
|
139 |
| Bound _ => raise SAME ()
|
|
140 |
| Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
|
|
141 |
| _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
|
|
142 |
handle SAME () => formula_from_atom (to_R_rep Ts t)
|
|
143 |
and to_S_rep Ts t =
|
|
144 |
case t of
|
|
145 |
Const (@{const_name Pair}, _) $ t1 $ t2 =>
|
|
146 |
Product (to_S_rep Ts t1, to_S_rep Ts t2)
|
|
147 |
| Const (@{const_name Pair}, _) $ _ => to_S_rep Ts (eta_expand Ts t 1)
|
|
148 |
| Const (@{const_name Pair}, _) => to_S_rep Ts (eta_expand Ts t 2)
|
|
149 |
| Const (@{const_name fst}, _) $ t1 =>
|
|
150 |
let val fst_arity = arity_of S_Rep card (fastype_of1 (Ts, t)) in
|
|
151 |
Project (to_S_rep Ts t1, num_seq 0 fst_arity)
|
|
152 |
end
|
|
153 |
| Const (@{const_name fst}, _) => to_S_rep Ts (eta_expand Ts t 1)
|
|
154 |
| Const (@{const_name snd}, _) $ t1 =>
|
|
155 |
let
|
|
156 |
val pair_arity = arity_of S_Rep card (fastype_of1 (Ts, t1))
|
|
157 |
val snd_arity = arity_of S_Rep card (fastype_of1 (Ts, t))
|
|
158 |
val fst_arity = pair_arity - snd_arity
|
|
159 |
in Project (to_S_rep Ts t1, num_seq fst_arity snd_arity) end
|
|
160 |
| Const (@{const_name snd}, _) => to_S_rep Ts (eta_expand Ts t 1)
|
|
161 |
| Bound j => rel_expr_for_bound_var card S_Rep Ts j
|
|
162 |
| _ => S_rep_from_R_rep Ts (fastype_of1 (Ts, t)) (to_R_rep Ts t)
|
|
163 |
and to_R_rep Ts t =
|
|
164 |
(case t of
|
|
165 |
@{const Not} => to_R_rep Ts (eta_expand Ts t 1)
|
|
166 |
| Const (@{const_name All}, _) => to_R_rep Ts (eta_expand Ts t 1)
|
|
167 |
| Const (@{const_name Ex}, _) => to_R_rep Ts (eta_expand Ts t 1)
|
|
168 |
| Const (@{const_name HOL.eq}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
|
|
169 |
| Const (@{const_name HOL.eq}, _) => to_R_rep Ts (eta_expand Ts t 2)
|
|
170 |
| Const (@{const_name ord_class.less_eq},
|
|
171 |
Type (@{type_name fun},
|
|
172 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
|
|
173 |
to_R_rep Ts (eta_expand Ts t 1)
|
|
174 |
| Const (@{const_name ord_class.less_eq}, _) =>
|
|
175 |
to_R_rep Ts (eta_expand Ts t 2)
|
|
176 |
| @{const HOL.conj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
|
|
177 |
| @{const HOL.conj} => to_R_rep Ts (eta_expand Ts t 2)
|
|
178 |
| @{const HOL.disj} $ _ => to_R_rep Ts (eta_expand Ts t 1)
|
|
179 |
| @{const HOL.disj} => to_R_rep Ts (eta_expand Ts t 2)
|
|
180 |
| @{const HOL.implies} $ _ => to_R_rep Ts (eta_expand Ts t 1)
|
|
181 |
| @{const HOL.implies} => to_R_rep Ts (eta_expand Ts t 2)
|
|
182 |
| Const (@{const_name bot_class.bot},
|
|
183 |
T as Type (@{type_name fun}, [_, @{typ bool}])) =>
|
|
184 |
empty_n_ary_rel (arity_of R_Rep card T)
|
|
185 |
| Const (@{const_name insert}, _) $ t1 $ t2 =>
|
|
186 |
Union (to_S_rep Ts t1, to_R_rep Ts t2)
|
|
187 |
| Const (@{const_name insert}, _) $ _ => to_R_rep Ts (eta_expand Ts t 1)
|
|
188 |
| Const (@{const_name insert}, _) => to_R_rep Ts (eta_expand Ts t 2)
|
|
189 |
| Const (@{const_name trancl}, _) $ t1 =>
|
|
190 |
if arity_of R_Rep card (fastype_of1 (Ts, t1)) = 2 then
|
|
191 |
Closure (to_R_rep Ts t1)
|
|
192 |
else
|
|
193 |
raise NOT_SUPPORTED "transitive closure for function or pair type"
|
|
194 |
| Const (@{const_name trancl}, _) => to_R_rep Ts (eta_expand Ts t 1)
|
|
195 |
| Const (@{const_name inf_class.inf},
|
|
196 |
Type (@{type_name fun},
|
|
197 |
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
|
|
198 |
$ t1 $ t2 =>
|
|
199 |
Intersect (to_R_rep Ts t1, to_R_rep Ts t2)
|
|
200 |
| Const (@{const_name inf_class.inf}, _) $ _ =>
|
|
201 |
to_R_rep Ts (eta_expand Ts t 1)
|
|
202 |
| Const (@{const_name inf_class.inf}, _) =>
|
|
203 |
to_R_rep Ts (eta_expand Ts t 2)
|
|
204 |
| Const (@{const_name sup_class.sup},
|
|
205 |
Type (@{type_name fun},
|
|
206 |
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
|
|
207 |
$ t1 $ t2 =>
|
|
208 |
Union (to_R_rep Ts t1, to_R_rep Ts t2)
|
|
209 |
| Const (@{const_name sup_class.sup}, _) $ _ =>
|
|
210 |
to_R_rep Ts (eta_expand Ts t 1)
|
|
211 |
| Const (@{const_name sup_class.sup}, _) =>
|
|
212 |
to_R_rep Ts (eta_expand Ts t 2)
|
|
213 |
| Const (@{const_name minus_class.minus},
|
|
214 |
Type (@{type_name fun},
|
|
215 |
[Type (@{type_name fun}, [_, @{typ bool}]), _]))
|
|
216 |
$ t1 $ t2 =>
|
|
217 |
Difference (to_R_rep Ts t1, to_R_rep Ts t2)
|
|
218 |
| Const (@{const_name minus_class.minus},
|
|
219 |
Type (@{type_name fun},
|
|
220 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) $ _ =>
|
|
221 |
to_R_rep Ts (eta_expand Ts t 1)
|
|
222 |
| Const (@{const_name minus_class.minus},
|
|
223 |
Type (@{type_name fun},
|
|
224 |
[Type (@{type_name fun}, [_, @{typ bool}]), _])) =>
|
|
225 |
to_R_rep Ts (eta_expand Ts t 2)
|
|
226 |
| Const (@{const_name Pair}, _) $ _ $ _ => raise SAME ()
|
|
227 |
| Const (@{const_name Pair}, _) $ _ => raise SAME ()
|
|
228 |
| Const (@{const_name Pair}, _) => raise SAME ()
|
|
229 |
| Const (@{const_name fst}, _) $ _ => raise SAME ()
|
|
230 |
| Const (@{const_name fst}, _) => raise SAME ()
|
|
231 |
| Const (@{const_name snd}, _) $ _ => raise SAME ()
|
|
232 |
| Const (@{const_name snd}, _) => raise SAME ()
|
|
233 |
| Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
|
|
234 |
| Free (x as (_, T)) =>
|
|
235 |
Rel (arity_of R_Rep card T, find_index (curry (op =) x) frees)
|
|
236 |
| Term.Var _ => raise NOT_SUPPORTED "schematic variables"
|
|
237 |
| Bound _ => raise SAME ()
|
|
238 |
| Abs (_, T, t') =>
|
|
239 |
(case fastype_of1 (T :: Ts, t') of
|
|
240 |
@{typ bool} => Comprehension (decls_for S_Rep card Ts T,
|
|
241 |
to_F (T :: Ts) t')
|
|
242 |
| T' => Comprehension (decls_for S_Rep card Ts T @
|
|
243 |
decls_for R_Rep card (T :: Ts) T',
|
|
244 |
Subset (rel_expr_for_bound_var card R_Rep
|
|
245 |
(T' :: T :: Ts) 0,
|
|
246 |
to_R_rep (T :: Ts) t')))
|
|
247 |
| t1 $ t2 =>
|
|
248 |
(case fastype_of1 (Ts, t) of
|
|
249 |
@{typ bool} => atom_from_formula (to_F Ts t)
|
|
250 |
| T =>
|
|
251 |
let val T2 = fastype_of1 (Ts, t2) in
|
|
252 |
case arity_of S_Rep card T2 of
|
|
253 |
1 => Join (to_S_rep Ts t2, to_R_rep Ts t1)
|
|
254 |
| arity2 =>
|
|
255 |
let val res_arity = arity_of R_Rep card T in
|
|
256 |
Project (Intersect
|
|
257 |
(Product (to_S_rep Ts t2,
|
|
258 |
atom_schema_of R_Rep card T
|
|
259 |
|> map (AtomSeq o rpair 0) |> foldl1 Product),
|
|
260 |
to_R_rep Ts t1),
|
|
261 |
num_seq arity2 res_arity)
|
|
262 |
end
|
|
263 |
end)
|
|
264 |
| _ => raise NOT_SUPPORTED ("term " ^
|
|
265 |
quote (Syntax.string_of_term ctxt t)))
|
|
266 |
handle SAME () => R_rep_from_S_rep (fastype_of1 (Ts, t)) (to_S_rep Ts t)
|
|
267 |
in to_F [] end
|
|
268 |
|
|
269 |
fun bound_for_free card i (s, T) =
|
|
270 |
let val js = atom_schema_of R_Rep card T in
|
|
271 |
([((length js, i), s)],
|
|
272 |
[TupleSet [], atom_schema_of R_Rep card T |> map (rpair 0)
|
|
273 |
|> tuple_set_from_atom_schema])
|
|
274 |
end
|
|
275 |
|
|
276 |
fun declarative_axiom_for_rel_expr card Ts (Type (@{type_name fun}, [T1, T2]))
|
|
277 |
r =
|
|
278 |
if body_type T2 = bool_T then
|
|
279 |
True
|
|
280 |
else
|
|
281 |
All (decls_for S_Rep card Ts T1,
|
|
282 |
declarative_axiom_for_rel_expr card (T1 :: Ts) T2
|
|
283 |
(List.foldl Join r (vars_for_bound_var card S_Rep (T1 :: Ts) 0)))
|
|
284 |
| declarative_axiom_for_rel_expr _ _ _ r = One r
|
|
285 |
fun declarative_axiom_for_free card i (_, T) =
|
|
286 |
declarative_axiom_for_rel_expr card [] T (Rel (arity_of R_Rep card T, i))
|
|
287 |
|
|
288 |
fun kodkod_problem_from_term ctxt raw_card t =
|
|
289 |
let
|
|
290 |
val thy = ProofContext.theory_of ctxt
|
|
291 |
fun card (Type (@{type_name fun}, [T1, T2])) =
|
|
292 |
reasonable_power (card T2) (card T1)
|
|
293 |
| card (Type (@{type_name prod}, [T1, T2])) = card T1 * card T2
|
|
294 |
| card @{typ bool} = 2
|
|
295 |
| card T = Int.max (1, raw_card T)
|
|
296 |
val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
|
|
297 |
val _ = fold_types (K o check_type ctxt) neg_t ()
|
|
298 |
val frees = Term.add_frees neg_t []
|
|
299 |
val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
|
|
300 |
val declarative_axioms =
|
|
301 |
map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
|
|
302 |
val formula = kodkod_formula_from_term ctxt card frees neg_t
|
|
303 |
|> fold_rev (curry And) declarative_axioms
|
|
304 |
val univ_card = univ_card 0 0 0 bounds formula
|
|
305 |
in
|
|
306 |
{comment = "", settings = [], univ_card = univ_card, tuple_assigns = [],
|
|
307 |
bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
|
|
308 |
end
|
|
309 |
|
|
310 |
fun solve_any_kodkod_problem thy problems =
|
|
311 |
let
|
|
312 |
val {debug, overlord, ...} = Nitpick_Isar.default_params thy []
|
|
313 |
val max_threads = 1
|
|
314 |
val max_solutions = 1
|
|
315 |
in
|
|
316 |
case solve_any_problem debug overlord NONE max_threads max_solutions
|
|
317 |
problems of
|
|
318 |
JavaNotInstalled => "unknown"
|
|
319 |
| JavaTooOld => "unknown"
|
|
320 |
| KodkodiNotInstalled => "unknown"
|
|
321 |
| Normal ([], _, _) => "none"
|
|
322 |
| Normal _ => "genuine"
|
|
323 |
| TimedOut _ => "unknown"
|
|
324 |
| Error (s, _) => error ("Kodkod error: " ^ s)
|
|
325 |
end
|
|
326 |
|
|
327 |
end;
|