author | blanchet |
Fri, 08 Sep 2017 00:03:06 +0200 | |
changeset 66635 | dbe1dc1f0016 |
parent 66634 | 56456f388867 |
child 66646 | 383d8e388d1b |
permissions | -rw-r--r-- |
64389 | 1 |
(* Title: HOL/Nunchaku/Tools/nunchaku_collect.ML |
66614
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
65458
diff
changeset
|
2 |
Author: Jasmin Blanchette, VU Amsterdam |
1f1c5d85d232
moved Nunchaku to Main; the goal is to move Nitpick out in the next 1-2 years
blanchet
parents:
65458
diff
changeset
|
3 |
Copyright 2015, 2016, 2017 |
64389 | 4 |
|
5 |
Collecting of Isabelle/HOL definitions etc. for Nunchaku. |
|
6 |
*) |
|
7 |
||
8 |
signature NUNCHAKU_COLLECT = |
|
9 |
sig |
|
10 |
val dest_co_datatype_case: Proof.context -> string * typ -> (string * typ) list |
|
11 |
||
12 |
type isa_type_spec = |
|
13 |
{abs_typ: typ, |
|
14 |
rep_typ: typ, |
|
15 |
wrt: term, |
|
16 |
abs: term, |
|
17 |
rep: term} |
|
18 |
||
19 |
type isa_co_data_spec = |
|
20 |
{typ: typ, |
|
21 |
ctrs: term list} |
|
22 |
||
23 |
type isa_const_spec = |
|
24 |
{const: term, |
|
25 |
props: term list} |
|
26 |
||
27 |
type isa_rec_spec = |
|
28 |
{const: term, |
|
29 |
props: term list, |
|
30 |
pat_complete: bool} |
|
31 |
||
32 |
type isa_consts_spec = |
|
33 |
{consts: term list, |
|
34 |
props: term list} |
|
35 |
||
36 |
datatype isa_command = |
|
37 |
ITVal of typ * (int option * int option) |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
38 |
| ITypedef of isa_type_spec |
64389 | 39 |
| IQuotient of isa_type_spec |
40 |
| ICoData of BNF_Util.fp_kind * isa_co_data_spec list |
|
41 |
| IVal of term |
|
42 |
| ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list |
|
43 |
| IRec of isa_rec_spec list |
|
44 |
| ISpec of isa_consts_spec |
|
45 |
| IAxiom of term |
|
46 |
| IGoal of term |
|
47 |
| IEval of term |
|
48 |
||
49 |
type isa_problem = |
|
50 |
{commandss: isa_command list list, |
|
51 |
sound: bool, |
|
52 |
complete: bool} |
|
53 |
||
54 |
exception CYCLIC_DEPS of unit |
|
55 |
exception TOO_DEEP_DEPS of unit |
|
56 |
exception TOO_META of term |
|
57 |
exception UNEXPECTED_POLYMORPHISM of term |
|
58 |
exception UNEXPECTED_VAR of term |
|
59 |
exception UNSUPPORTED_FUNC of term |
|
60 |
||
61 |
val isa_problem_of_subgoal: Proof.context -> bool -> ((string * typ) option * bool option) list -> |
|
62 |
(term option * bool) list -> (typ option * (int option * int option)) list -> bool -> |
|
63 |
Time.time -> term list -> term list -> term -> term list * isa_problem |
|
64 |
val pat_completes_of_isa_problem: isa_problem -> term list |
|
65 |
val str_of_isa_problem: Proof.context -> isa_problem -> string |
|
66 |
end; |
|
67 |
||
68 |
structure Nunchaku_Collect : NUNCHAKU_COLLECT = |
|
69 |
struct |
|
70 |
||
71 |
open Nunchaku_Util; |
|
72 |
||
73 |
type isa_type_spec = |
|
74 |
{abs_typ: typ, |
|
75 |
rep_typ: typ, |
|
76 |
wrt: term, |
|
77 |
abs: term, |
|
78 |
rep: term}; |
|
79 |
||
80 |
type isa_co_data_spec = |
|
81 |
{typ: typ, |
|
82 |
ctrs: term list}; |
|
83 |
||
84 |
type isa_const_spec = |
|
85 |
{const: term, |
|
86 |
props: term list}; |
|
87 |
||
88 |
type isa_rec_spec = |
|
89 |
{const: term, |
|
90 |
props: term list, |
|
91 |
pat_complete: bool}; |
|
92 |
||
93 |
type isa_consts_spec = |
|
94 |
{consts: term list, |
|
95 |
props: term list}; |
|
96 |
||
97 |
datatype isa_command = |
|
98 |
ITVal of typ * (int option * int option) |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
99 |
| ITypedef of isa_type_spec |
64389 | 100 |
| IQuotient of isa_type_spec |
101 |
| ICoData of BNF_Util.fp_kind * isa_co_data_spec list |
|
102 |
| IVal of term |
|
103 |
| ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list |
|
104 |
| IRec of isa_rec_spec list |
|
105 |
| ISpec of isa_consts_spec |
|
106 |
| IAxiom of term |
|
107 |
| IGoal of term |
|
108 |
| IEval of term; |
|
109 |
||
110 |
type isa_problem = |
|
111 |
{commandss: isa_command list list, |
|
112 |
sound: bool, |
|
113 |
complete: bool}; |
|
114 |
||
115 |
exception CYCLIC_DEPS of unit; |
|
116 |
exception TOO_DEEP_DEPS of unit; |
|
117 |
exception TOO_META of term; |
|
118 |
exception UNEXPECTED_POLYMORPHISM of term; |
|
119 |
exception UNEXPECTED_VAR of term; |
|
120 |
exception UNSUPPORTED_FUNC of term; |
|
121 |
||
122 |
fun str_of_and_list str_of_elem = |
|
123 |
map str_of_elem #> space_implode ("\nand "); |
|
124 |
||
125 |
val key_of_typ = |
|
126 |
let |
|
127 |
fun key_of (Type (s, [])) = s |
|
128 |
| key_of (Type (s, Ts)) = s ^ "(" ^ commas (map key_of Ts) ^ ")" |
|
129 |
| key_of (TFree (s, _)) = s; |
|
130 |
in |
|
131 |
prefix "y" o key_of |
|
132 |
end; |
|
133 |
||
134 |
fun key_of_const ctxt = |
|
135 |
let |
|
136 |
val thy = Proof_Context.theory_of ctxt; |
|
137 |
||
138 |
fun key_of (Const (x as (s, _))) = |
|
139 |
(case Sign.const_typargs thy x of |
|
140 |
[] => s |
|
141 |
| Ts => s ^ "(" ^ commas (map key_of_typ Ts) ^ ")") |
|
142 |
| key_of (Free (s, _)) = s; |
|
143 |
in |
|
144 |
prefix "t" o key_of |
|
145 |
end; |
|
146 |
||
147 |
val add_type_keys = fold_subtypes (insert (op =) o key_of_typ); |
|
148 |
||
149 |
fun add_aterm_keys ctxt t = |
|
150 |
if is_Const t orelse is_Free t then insert (op =) (key_of_const ctxt t) else I; |
|
151 |
||
152 |
fun add_keys ctxt t = |
|
153 |
fold_aterms (add_aterm_keys ctxt) t |
|
154 |
#> fold_types add_type_keys t; |
|
155 |
||
156 |
fun close_form except t = |
|
157 |
fold (fn ((s, i), T) => fn t' => |
|
158 |
HOLogic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
|
159 |
(Term.add_vars t [] |> subtract (op =) except) t; |
|
160 |
||
161 |
(* "imp_conjL[symmetric]" is important for inductive predicates with multiple assumptions. *) |
|
162 |
val basic_defs = |
|
163 |
@{thms Ball_def[abs_def] Bex_def[abs_def] case_bool_if Ex1_def[abs_def] |
|
164 |
imp_conjL[symmetric, abs_def] Let_def[abs_def] rmember_def[symmetric, abs_def]}; |
|
165 |
||
166 |
fun unfold_basic_def ctxt = |
|
167 |
let val thy = Proof_Context.theory_of ctxt in |
|
168 |
Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) basic_defs) [] |
|
169 |
end; |
|
170 |
||
171 |
val has_polymorphism = exists_type (exists_subtype is_TVar); |
|
172 |
||
173 |
fun whack_term thy whacks = |
|
174 |
let |
|
175 |
fun whk t = |
|
176 |
if triple_lookup (term_match thy o swap) whacks t = SOME true then |
|
177 |
Const (@{const_name unreachable}, fastype_of t) |
|
178 |
else |
|
179 |
(case t of |
|
180 |
u $ v => whk u $ whk v |
|
181 |
| Abs (s, T, u) => Abs (s, T, whk u) |
|
182 |
| _ => t); |
|
183 |
in |
|
184 |
whk |
|
185 |
end; |
|
186 |
||
187 |
fun preprocess_term_basic falsify ctxt whacks t = |
|
188 |
let val thy = Proof_Context.theory_of ctxt in |
|
189 |
if has_polymorphism t then |
|
190 |
raise UNEXPECTED_POLYMORPHISM t |
|
191 |
else |
|
192 |
t |
|
193 |
|> attach_typeS |
|
194 |
|> whack_term thy whacks |
|
195 |
|> Object_Logic.atomize_term ctxt |
|
196 |
|> tap (fn t' => fastype_of t' <> @{typ prop} orelse raise TOO_META t) |
|
197 |
|> falsify ? HOLogic.mk_not |
|
198 |
|> unfold_basic_def ctxt |
|
199 |
end; |
|
200 |
||
201 |
val check_closed = tap (fn t => null (Term.add_vars t []) orelse raise UNEXPECTED_VAR t); |
|
202 |
||
203 |
val preprocess_prop = close_form [] oooo preprocess_term_basic; |
|
204 |
val preprocess_closed_term = check_closed ooo preprocess_term_basic false; |
|
205 |
||
206 |
val is_type_builtin = member (op =) [@{type_name bool}, @{type_name fun}]; |
|
207 |
||
208 |
val is_const_builtin = |
|
209 |
member (op =) [@{const_name All}, @{const_name conj}, @{const_name disj}, @{const_name Eps}, |
|
210 |
@{const_name HOL.eq}, @{const_name Ex}, @{const_name False}, @{const_name If}, |
|
211 |
@{const_name implies}, @{const_name Not}, @{const_name The}, @{const_name The_unsafe}, |
|
212 |
@{const_name True}]; |
|
213 |
||
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
214 |
datatype type_classification = Builtin | TVal | Typedef | Quotient | Co_Datatype; |
64389 | 215 |
|
216 |
fun classify_type_name ctxt T_name = |
|
217 |
if is_type_builtin T_name then |
|
218 |
Builtin |
|
219 |
else if T_name = @{type_name itself} then |
|
220 |
Co_Datatype |
|
221 |
else |
|
222 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of |
|
223 |
SOME _ => Co_Datatype |
|
224 |
| NONE => |
|
225 |
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of |
|
226 |
SOME _ => Co_Datatype |
|
227 |
| NONE => |
|
228 |
(case Quotient_Info.lookup_quotients ctxt T_name of |
|
229 |
SOME _ => Quotient |
|
230 |
| NONE => |
|
231 |
if T_name = @{type_name set} then |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
232 |
Typedef |
64389 | 233 |
else |
234 |
(case Typedef.get_info ctxt T_name of |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
235 |
_ :: _ => Typedef |
64389 | 236 |
| [] => TVal)))); |
237 |
||
238 |
fun fp_kind_of_ctr_sugar_kind Ctr_Sugar.Codatatype = BNF_Util.Greatest_FP |
|
239 |
| fp_kind_of_ctr_sugar_kind _ = BNF_Util.Least_FP; |
|
240 |
||
241 |
fun mutual_co_datatypes_of ctxt (T_name, Ts) = |
|
242 |
(if T_name = @{type_name itself} then |
|
243 |
(BNF_Util.Least_FP, [@{typ "'a itself"}], [[@{const Pure.type ('a)}]]) |
|
244 |
else |
|
245 |
let |
|
246 |
val (fp, ctr_sugars) = |
|
247 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of |
|
248 |
SOME (fp_sugar as {fp, fp_res = {Ts, ...}, ...}) => |
|
249 |
(fp, |
|
250 |
(case Ts of |
|
251 |
[_] => [fp_sugar] |
|
252 |
| _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o fst o dest_Type) Ts) |
|
253 |
|> map (#ctr_sugar o #fp_ctr_sugar)) |
|
254 |
| NONE => |
|
255 |
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of |
|
256 |
SOME (ctr_sugar as {kind, ...}) => |
|
257 |
(* Any freely constructed type that is not a codatatype is considered a datatype. This |
|
258 |
is sound (but incomplete) for model finding. *) |
|
259 |
(fp_kind_of_ctr_sugar_kind kind, [ctr_sugar]))); |
|
260 |
in |
|
261 |
(fp, map #T ctr_sugars, map #ctrs ctr_sugars) |
|
262 |
end) |
|
263 |
|> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts)))) |
|
264 |
|> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts))); |
|
265 |
||
66624 | 266 |
fun typedef_of ctxt T_name = |
64389 | 267 |
if T_name = @{type_name set} then |
268 |
let |
|
269 |
val A = Logic.varifyT_global @{typ 'a}; |
|
270 |
val absT = Type (@{type_name set}, [A]); |
|
271 |
val repT = A --> HOLogic.boolT; |
|
66624 | 272 |
val pred = Abs (Name.uu, repT, @{const True}); |
64389 | 273 |
val abs = Const (@{const_name Collect}, repT --> absT); |
274 |
val rep = Const (@{const_name rmember}, absT --> repT); |
|
275 |
in |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
276 |
(absT, repT, pred, abs, rep) |
64389 | 277 |
end |
278 |
else |
|
279 |
(case Typedef.get_info ctxt T_name of |
|
280 |
(* When several entries are returned, it shouldn't matter much which one we take (according to |
|
281 |
Florian Haftmann). The "Logic.varifyT_global" calls are a workaround because these types' |
|
282 |
variables sometimes clash with locally fixed type variables. *) |
|
283 |
({abs_type, rep_type, Abs_name, Rep_name, ...}, {Rep, ...}) :: _ => |
|
284 |
let |
|
285 |
val absT = Logic.varifyT_global abs_type; |
|
286 |
val repT = Logic.varifyT_global rep_type; |
|
66624 | 287 |
val set = Thm.prop_of Rep |
64389 | 288 |
|> HOLogic.dest_Trueprop |
289 |
|> HOLogic.dest_mem |
|
290 |
|> snd; |
|
66624 | 291 |
val pred = Abs (Name.uu, repT, HOLogic.mk_mem (Bound 0, set)); |
64389 | 292 |
val abs = Const (Abs_name, repT --> absT); |
293 |
val rep = Const (Rep_name, absT --> repT); |
|
294 |
in |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
295 |
(absT, repT, pred, abs, rep) |
64389 | 296 |
end); |
297 |
||
66624 | 298 |
fun quotient_of ctxt T_name = |
64412 | 299 |
(case Quotient_Info.lookup_quotients ctxt T_name of |
66624 | 300 |
SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} => |
301 |
let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in |
|
64412 | 302 |
(qtyp, rtyp, equiv_rel, abs, rep) |
303 |
end); |
|
304 |
||
64389 | 305 |
fun is_co_datatype_ctr ctxt (s, T) = |
306 |
(case body_type T of |
|
307 |
Type (fpT_name, Ts) => |
|
308 |
classify_type_name ctxt fpT_name = Co_Datatype andalso |
|
309 |
let |
|
310 |
val ctrs = |
|
311 |
if fpT_name = @{type_name itself} then |
|
312 |
[Const (@{const_name Pure.type}, @{typ "'a itself"})] |
|
313 |
else |
|
314 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of |
|
315 |
SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} => ctrs |
|
316 |
| NONE => |
|
317 |
(case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of |
|
318 |
SOME {ctrs, ...} => ctrs |
|
319 |
| _ => [])); |
|
320 |
||
321 |
fun is_right_ctr (t' as Const (s', _)) = |
|
322 |
s = s' andalso fastype_of (Ctr_Sugar.mk_ctr Ts t') = T; |
|
323 |
in |
|
324 |
exists is_right_ctr ctrs |
|
325 |
end |
|
326 |
| _ => false); |
|
327 |
||
328 |
fun dest_co_datatype_case ctxt (s, T) = |
|
329 |
let val thy = Proof_Context.theory_of ctxt in |
|
330 |
(case strip_fun_type (Sign.the_const_type thy s) of |
|
331 |
(gen_branch_Ts, gen_body_fun_T) => |
|
332 |
(case gen_body_fun_T of |
|
333 |
Type (@{type_name fun}, [Type (fpT_name, _), _]) => |
|
334 |
if classify_type_name ctxt fpT_name = Co_Datatype then |
|
335 |
let |
|
336 |
val Type (_, fpTs) = domain_type (funpow (length gen_branch_Ts) range_type T); |
|
337 |
val (ctrs0, Const (case_name, _)) = |
|
338 |
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of |
|
339 |
SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, casex, ...}, ...}, ...} => (ctrs, casex) |
|
340 |
| NONE => |
|
341 |
(case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of |
|
342 |
SOME {ctrs, casex, ...} => (ctrs, casex))); |
|
343 |
in |
|
344 |
if s = case_name then map (dest_Const o Ctr_Sugar.mk_ctr fpTs) ctrs0 |
|
345 |
else raise Fail "non-case" |
|
346 |
end |
|
347 |
else |
|
348 |
raise Fail "non-case")) |
|
349 |
end; |
|
350 |
||
351 |
val is_co_datatype_case = can o dest_co_datatype_case; |
|
352 |
||
66624 | 353 |
fun is_quotient_abs ctxt (s, T) = |
64389 | 354 |
(case T of |
355 |
Type (@{type_name fun}, [_, Type (absT_name, _)]) => |
|
356 |
classify_type_name ctxt absT_name = Quotient andalso |
|
66624 | 357 |
(case quotient_of ctxt absT_name of |
64389 | 358 |
(_, _, _, Const (s', _), _) => s' = s) |
359 |
| _ => false); |
|
360 |
||
66624 | 361 |
fun is_quotient_rep ctxt (s, T) = |
64389 | 362 |
(case T of |
363 |
Type (@{type_name fun}, [Type (absT_name, _), _]) => |
|
364 |
classify_type_name ctxt absT_name = Quotient andalso |
|
66624 | 365 |
(case quotient_of ctxt absT_name of |
64389 | 366 |
(_, _, _, _, Const (s', _)) => s' = s) |
367 |
| _ => false); |
|
368 |
||
66624 | 369 |
fun is_maybe_typedef_abs ctxt absT_name s = |
64389 | 370 |
if absT_name = @{type_name set} then |
371 |
s = @{const_name Collect} |
|
372 |
else |
|
66624 | 373 |
(case try (typedef_of ctxt) absT_name of |
64389 | 374 |
SOME (_, _, _, Const (s', _), _) => s' = s |
375 |
| NONE => false); |
|
376 |
||
66624 | 377 |
fun is_maybe_typedef_rep ctxt absT_name s = |
64389 | 378 |
if absT_name = @{type_name set} then |
379 |
s = @{const_name rmember} |
|
380 |
else |
|
66624 | 381 |
(case try (typedef_of ctxt) absT_name of |
64389 | 382 |
SOME (_, _, _, _, Const (s', _)) => s' = s |
383 |
| NONE => false); |
|
384 |
||
66624 | 385 |
fun is_typedef_abs ctxt (s, T) = |
64389 | 386 |
(case T of |
387 |
Type (@{type_name fun}, [_, Type (absT_name, _)]) => |
|
66624 | 388 |
classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_abs ctxt absT_name s |
64389 | 389 |
| _ => false); |
390 |
||
66624 | 391 |
fun is_typedef_rep ctxt (s, T) = |
64389 | 392 |
(case T of |
393 |
Type (@{type_name fun}, [Type (absT_name, _), _]) => |
|
66624 | 394 |
classify_type_name ctxt absT_name = Typedef andalso is_maybe_typedef_rep ctxt absT_name s |
64389 | 395 |
| _ => false); |
396 |
||
66624 | 397 |
fun is_stale_typedef_abs ctxt (s, T) = |
64389 | 398 |
(case T of |
399 |
Type (@{type_name fun}, [_, Type (absT_name, _)]) => |
|
66624 | 400 |
classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_abs ctxt absT_name s |
64389 | 401 |
| _ => false); |
402 |
||
66624 | 403 |
fun is_stale_typedef_rep ctxt (s, T) = |
64389 | 404 |
(case T of |
405 |
Type (@{type_name fun}, [Type (absT_name, _), _]) => |
|
66624 | 406 |
classify_type_name ctxt absT_name <> Typedef andalso is_maybe_typedef_rep ctxt absT_name s |
64389 | 407 |
| _ => false); |
408 |
||
409 |
fun instantiate_constant_types_in_term ctxt csts target = |
|
410 |
let |
|
411 |
val thy = Proof_Context.theory_of ctxt; |
|
412 |
||
413 |
fun try_const _ _ (res as SOME _) = res |
|
414 |
| try_const (s', T') cst NONE = |
|
415 |
(case cst of |
|
416 |
Const (s, T) => |
|
417 |
if s = s' then |
|
418 |
SOME (Sign.typ_match thy (T', T) Vartab.empty) |
|
419 |
handle Type.TYPE_MATCH => NONE |
|
420 |
else |
|
421 |
NONE |
|
422 |
| _ => NONE); |
|
423 |
||
424 |
fun subst_for (Const x) = fold (try_const x) csts NONE |
|
425 |
| subst_for (t as Free _) = if member (op aconv) csts t then SOME Vartab.empty else NONE |
|
426 |
| subst_for (t1 $ t2) = (case subst_for t1 of SOME subst => SOME subst | NONE => subst_for t2) |
|
427 |
| subst_for (Abs (_, _, t')) = subst_for t' |
|
428 |
| subst_for _ = NONE; |
|
429 |
in |
|
430 |
(case subst_for target of |
|
431 |
SOME subst => Envir.subst_term_types subst target |
|
432 |
| NONE => raise Type.TYPE_MATCH) |
|
433 |
end; |
|
434 |
||
435 |
datatype card = One | Fin | Fin_or_Inf | Inf |
|
436 |
||
437 |
(* Similar to "ATP_Util.tiny_card_of_type". *) |
|
438 |
fun card_of_type ctxt = |
|
439 |
let |
|
440 |
fun max_card Inf _ = Inf |
|
441 |
| max_card _ Inf = Inf |
|
442 |
| max_card Fin_or_Inf _ = Fin_or_Inf |
|
443 |
| max_card _ Fin_or_Inf = Fin_or_Inf |
|
444 |
| max_card Fin _ = Fin |
|
445 |
| max_card _ Fin = Fin |
|
446 |
| max_card One One = One; |
|
447 |
||
448 |
fun card_of avoid T = |
|
449 |
if member (op =) avoid T then |
|
450 |
Inf |
|
451 |
else |
|
452 |
(case T of |
|
453 |
TFree _ => Fin_or_Inf |
|
454 |
| TVar _ => Inf |
|
455 |
| Type (@{type_name fun}, [T1, T2]) => |
|
456 |
(case (card_of avoid T1, card_of avoid T2) of |
|
457 |
(_, One) => One |
|
458 |
| (k1, k2) => max_card k1 k2) |
|
459 |
| Type (@{type_name prod}, [T1, T2]) => |
|
460 |
(case (card_of avoid T1, card_of avoid T2) of |
|
461 |
(k1, k2) => max_card k1 k2) |
|
462 |
| Type (@{type_name set}, [T']) => card_of avoid (T' --> HOLogic.boolT) |
|
463 |
| Type (T_name, Ts) => |
|
464 |
(case try (mutual_co_datatypes_of ctxt) (T_name, Ts) of |
|
465 |
NONE => Inf |
|
466 |
| SOME (_, fpTs, ctrss) => |
|
467 |
(case ctrss of [[_]] => One | _ => Fin) |
|
468 |
|> fold (fold (fold (max_card o card_of (fpTs @ avoid)) o binder_types o fastype_of)) |
|
469 |
ctrss)); |
|
470 |
in |
|
471 |
card_of [] |
|
472 |
end; |
|
473 |
||
474 |
fun int_of_classif Spec_Rules.Equational = 1 |
|
475 |
| int_of_classif Spec_Rules.Inductive = 2 |
|
476 |
| int_of_classif Spec_Rules.Co_Inductive = 3 |
|
477 |
| int_of_classif Spec_Rules.Unknown = 4; |
|
478 |
||
479 |
val classif_ord = int_ord o apply2 int_of_classif; |
|
480 |
||
481 |
fun spec_rules_of ctxt (x as (s, T)) = |
|
482 |
let |
|
483 |
val thy = Proof_Context.theory_of ctxt; |
|
484 |
||
485 |
fun subst_of t0 = |
|
486 |
try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty; |
|
487 |
||
488 |
fun process_spec _ (res as SOME _) = res |
|
489 |
| process_spec (classif, (ts0, ths as _ :: _)) NONE = |
|
490 |
(case get_first subst_of ts0 of |
|
491 |
SOME subst => |
|
492 |
(let |
|
493 |
val ts = map (Envir.subst_term_types subst) ts0; |
|
494 |
val poly_props = map Thm.prop_of ths; |
|
495 |
val props = map (instantiate_constant_types_in_term ctxt ts) poly_props; |
|
496 |
in |
|
497 |
if exists (exists (exists_type (exists_subtype is_TVar))) [ts, props] then NONE |
|
498 |
else SOME (classif, ts, props, poly_props) |
|
499 |
end |
|
500 |
handle Type.TYPE_MATCH => NONE) |
|
501 |
| NONE => NONE) |
|
502 |
| process_spec _ NONE = NONE; |
|
503 |
||
504 |
fun spec_rules () = |
|
505 |
Spec_Rules.retrieve ctxt (Const x) |
|
506 |
|> sort (classif_ord o apply2 fst); |
|
507 |
||
508 |
val specs = |
|
509 |
if s = @{const_name The} then |
|
510 |
[(Spec_Rules.Unknown, ([Logic.varify_global @{term The}], [@{thm theI_unique}]))] |
|
511 |
else if s = @{const_name finite} then |
|
512 |
let val card = card_of_type ctxt T in |
|
513 |
if card = Inf orelse card = Fin_or_Inf then |
|
514 |
spec_rules () |
|
515 |
else |
|
516 |
[(Spec_Rules.Equational, ([Logic.varify_global @{term finite}], |
|
517 |
[Skip_Proof.make_thm thy (Logic.varify_global @{prop "finite A = True"})]))] |
|
518 |
end |
|
519 |
else |
|
520 |
spec_rules (); |
|
521 |
in |
|
522 |
fold process_spec specs NONE |
|
523 |
end; |
|
524 |
||
525 |
fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t |
|
526 |
| lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t; |
|
527 |
||
528 |
fun specialize_definition_type thy x def0 = |
|
529 |
let |
|
530 |
val def = specialize_type thy x def0; |
|
531 |
val lhs = lhs_of_equation def; |
|
532 |
in |
|
533 |
if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize" |
|
534 |
end; |
|
535 |
||
536 |
fun definition_of thy (x as (s, _)) = |
|
537 |
Defs.specifications_of (Theory.defs_of thy) (Defs.Const, s) |
|
538 |
|> map_filter #def |
|
539 |
|> map_filter (try (specialize_definition_type thy x o Thm.prop_of o Thm.axiom thy)) |
|
540 |
|> try hd; |
|
541 |
||
542 |
fun is_builtin_theory thy_id = |
|
543 |
Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice}); |
|
544 |
||
545 |
val orphan_axioms_of = |
|
546 |
Spec_Rules.get |
|
547 |
#> filter (curry (op =) Spec_Rules.Unknown o fst) |
|
548 |
#> map snd |
|
549 |
#> filter (null o fst) |
|
550 |
#> maps snd |
|
65458 | 551 |
#> filter_out (is_builtin_theory o Thm.theory_id) |
64389 | 552 |
#> map Thm.prop_of; |
553 |
||
554 |
fun keys_of _ (ITVal (T, _)) = [key_of_typ T] |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
555 |
| keys_of _ (ITypedef {abs_typ, ...}) = [key_of_typ abs_typ] |
64389 | 556 |
| keys_of _ (IQuotient {abs_typ, ...}) = [key_of_typ abs_typ] |
557 |
| keys_of _ (ICoData (_, specs)) = map (key_of_typ o #typ) specs |
|
558 |
| keys_of ctxt (IVal const) = [key_of_const ctxt const] |
|
559 |
| keys_of ctxt (ICoPred (_, _, specs)) = map (key_of_const ctxt o #const) specs |
|
560 |
| keys_of ctxt (IRec specs) = map (key_of_const ctxt o #const) specs |
|
561 |
| keys_of ctxt (ISpec {consts, ...}) = map (key_of_const ctxt) consts |
|
562 |
| keys_of _ (IAxiom _) = [] |
|
563 |
| keys_of _ (IGoal _) = [] |
|
564 |
| keys_of _ (IEval _) = []; |
|
565 |
||
566 |
fun co_data_spec_deps_of ctxt ({ctrs, ...} : isa_co_data_spec) = |
|
567 |
fold (add_keys ctxt) ctrs []; |
|
568 |
fun const_spec_deps_of ctxt consts props = |
|
569 |
fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts); |
|
570 |
fun consts_spec_deps_of ctxt {consts, props} = |
|
571 |
fold (add_keys ctxt) props [] |> subtract (op =) (map (key_of_const ctxt) consts); |
|
572 |
||
573 |
fun deps_of _ (ITVal _) = [] |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
574 |
| deps_of ctxt (ITypedef {wrt, ...}) = add_keys ctxt wrt [] |
64389 | 575 |
| deps_of ctxt (IQuotient {wrt, ...}) = add_keys ctxt wrt [] |
576 |
| deps_of ctxt (ICoData (_, specs)) = maps (co_data_spec_deps_of ctxt) specs |
|
577 |
| deps_of _ (IVal const) = add_type_keys (fastype_of const) [] |
|
578 |
| deps_of ctxt (ICoPred (_, _, specs)) = |
|
579 |
maps (const_spec_deps_of ctxt (map #const specs) o #props) specs |
|
580 |
| deps_of ctxt (IRec specs) = maps (const_spec_deps_of ctxt (map #const specs) o #props) specs |
|
581 |
| deps_of ctxt (ISpec spec) = consts_spec_deps_of ctxt spec |
|
582 |
| deps_of ctxt (IAxiom prop) = add_keys ctxt prop [] |
|
583 |
| deps_of ctxt (IGoal prop) = add_keys ctxt prop [] |
|
584 |
| deps_of ctxt (IEval t) = add_keys ctxt t []; |
|
585 |
||
586 |
fun consts_of_rec_or_spec (IRec specs) = map #const specs |
|
587 |
| consts_of_rec_or_spec (ISpec {consts, ...}) = consts; |
|
588 |
||
589 |
fun props_of_rec_or_spec (IRec specs) = maps #props specs |
|
590 |
| props_of_rec_or_spec (ISpec {props, ...}) = props; |
|
591 |
||
592 |
fun merge_two_rec_or_spec cmd cmd' = |
|
593 |
ISpec {consts = consts_of_rec_or_spec cmd @ consts_of_rec_or_spec cmd', |
|
594 |
props = props_of_rec_or_spec cmd @ props_of_rec_or_spec cmd'}; |
|
595 |
||
596 |
fun merge_two (ICoData (fp, specs)) (ICoData (fp', specs'), complete) = |
|
597 |
(ICoData (BNF_Util.case_fp fp fp fp', specs @ specs'), complete andalso fp = fp') |
|
598 |
| merge_two (IRec specs) (IRec specs', complete) = (IRec (specs @ specs'), complete) |
|
599 |
| merge_two (cmd as IRec _) (cmd' as ISpec _, complete) = |
|
600 |
(merge_two_rec_or_spec cmd cmd', complete) |
|
601 |
| merge_two (cmd as ISpec _) (cmd' as IRec _, complete) = |
|
602 |
(merge_two_rec_or_spec cmd cmd', complete) |
|
603 |
| merge_two (cmd as ISpec _) (cmd' as ISpec _, complete) = |
|
604 |
(merge_two_rec_or_spec cmd cmd', complete) |
|
605 |
| merge_two _ _ = raise CYCLIC_DEPS (); |
|
606 |
||
607 |
fun sort_isa_commands_topologically ctxt cmds = |
|
608 |
let |
|
609 |
fun normal_pairs [] = [] |
|
610 |
| normal_pairs (all as normal :: _) = map (rpair normal) all; |
|
611 |
||
612 |
fun add_node [] _ = I |
|
613 |
| add_node (normal :: _) cmd = Graph.new_node (normal, cmd); |
|
614 |
||
615 |
fun merge_scc (cmd :: cmds) complete = fold merge_two cmds (cmd, complete); |
|
616 |
||
617 |
fun sort_problem (cmds, complete) = |
|
618 |
let |
|
619 |
val keyss = map (keys_of ctxt) cmds; |
|
620 |
val normal_keys = Symtab.make (maps normal_pairs keyss); |
|
621 |
val normalize = Symtab.lookup normal_keys; |
|
622 |
||
623 |
fun add_deps [] _ = I |
|
624 |
| add_deps (normal :: _) cmd = |
|
625 |
let |
|
626 |
val deps = deps_of ctxt cmd |
|
627 |
|> map_filter normalize |
|
628 |
|> remove (op =) normal; |
|
629 |
in |
|
630 |
fold (fn dep => Graph.add_edge (dep, normal)) deps |
|
631 |
end; |
|
632 |
||
633 |
val cmd_of_key = the o AList.lookup (op =) (map hd keyss ~~ cmds); |
|
634 |
||
635 |
val G = Graph.empty |
|
636 |
|> fold2 add_node keyss cmds |
|
637 |
|> fold2 add_deps keyss cmds; |
|
638 |
||
639 |
val cmd_sccs = rev (Graph.strong_conn G) |
|
640 |
|> map (map cmd_of_key); |
|
641 |
in |
|
642 |
if exists (can (fn _ :: _ :: _ => ())) cmd_sccs then |
|
643 |
sort_problem (fold_map merge_scc cmd_sccs complete) |
|
644 |
else |
|
645 |
(Graph.schedule (K snd) G, complete) |
|
646 |
end; |
|
647 |
||
648 |
val typedecls = filter (can (fn ITVal _ => ())) cmds; |
|
649 |
val (mixed, complete) = |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
650 |
(filter (can (fn ITypedef _ => () | IQuotient _ => () | ICoData _ => () | IVal _ => () |
64389 | 651 |
| ICoPred _ => () | IRec _ => () | ISpec _ => ())) cmds, true) |
652 |
|> sort_problem; |
|
653 |
val axioms = filter (can (fn IAxiom _ => ())) cmds; |
|
654 |
val goals = filter (can (fn IGoal _ => ())) cmds; |
|
655 |
val evals = filter (can (fn IEval _ => ())) cmds; |
|
656 |
in |
|
657 |
(typedecls @ mixed @ axioms @ goals @ evals, complete) |
|
658 |
end; |
|
659 |
||
660 |
fun group_of (ITVal _) = 1 |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
661 |
| group_of (ITypedef _) = 2 |
64389 | 662 |
| group_of (IQuotient _) = 3 |
663 |
| group_of (ICoData _) = 4 |
|
664 |
| group_of (IVal _) = 5 |
|
665 |
| group_of (ICoPred _) = 6 |
|
666 |
| group_of (IRec _) = 7 |
|
667 |
| group_of (ISpec _) = 8 |
|
668 |
| group_of (IAxiom _) = 9 |
|
669 |
| group_of (IGoal _) = 10 |
|
670 |
| group_of (IEval _) = 11; |
|
671 |
||
672 |
fun group_isa_commands [] = [] |
|
673 |
| group_isa_commands [cmd] = [[cmd]] |
|
674 |
| group_isa_commands (cmd :: cmd' :: cmds) = |
|
675 |
let val (group :: groups) = group_isa_commands (cmd' :: cmds) in |
|
676 |
if group_of cmd = group_of cmd' then |
|
677 |
(cmd :: group) :: groups |
|
678 |
else |
|
679 |
[cmd] :: (group :: groups) |
|
680 |
end; |
|
681 |
||
682 |
fun defined_by (Const (@{const_name All}, _) $ t) = defined_by t |
|
683 |
| defined_by (Abs (_, _, t)) = defined_by t |
|
684 |
| defined_by (@{const implies} $ _ $ u) = defined_by u |
|
685 |
| defined_by (Const (@{const_name HOL.eq}, _) $ t $ _) = head_of t |
|
686 |
| defined_by t = head_of t; |
|
687 |
||
688 |
fun partition_props [_] props = SOME [props] |
|
689 |
| partition_props consts props = |
|
690 |
let |
|
691 |
val propss = map (fn const => filter (fn prop => defined_by prop aconv const) props) consts; |
|
692 |
in |
|
693 |
if eq_set (op aconv) (props, flat propss) andalso forall (not o null) propss then SOME propss |
|
694 |
else NONE |
|
695 |
end; |
|
696 |
||
697 |
fun hol_concl_head (Const (@{const_name All}, _) $ Abs (_, _, t)) = hol_concl_head t |
|
698 |
| hol_concl_head (Const (@{const_name implies}, _) $ _ $ t) = hol_concl_head t |
|
699 |
| hol_concl_head (t $ _) = hol_concl_head t |
|
700 |
| hol_concl_head t = t; |
|
701 |
||
702 |
fun is_inductive_set_intro t = |
|
703 |
(case hol_concl_head t of |
|
704 |
Const (@{const_name rmember}, _) => true |
|
705 |
| _ => false); |
|
706 |
||
707 |
exception NO_TRIPLE of unit; |
|
708 |
||
709 |
fun triple_for_intro_rule ctxt x rule = |
|
710 |
let |
|
711 |
val (prems, concl) = Logic.strip_horn rule |
|
712 |
|>> map (Object_Logic.atomize_term ctxt) |
|
713 |
||> Object_Logic.atomize_term ctxt; |
|
714 |
||
715 |
val (mains, sides) = List.partition (exists_Const (curry (op =) x)) prems; |
|
716 |
||
717 |
val is_right_head = curry (op aconv) (Const x) o head_of; |
|
718 |
in |
|
719 |
if forall is_right_head mains then (sides, mains, concl) else raise NO_TRIPLE () |
|
720 |
end; |
|
721 |
||
722 |
val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb; |
|
723 |
||
724 |
fun wf_constraint_for rel sides concl mains = |
|
725 |
HOLogic.mk_mem (HOLogic.mk_prod (apply2 tuple_for_args (mains, concl)), Var rel) |
|
726 |
|> fold (curry HOLogic.mk_imp) sides |
|
727 |
|> close_form [rel]; |
|
728 |
||
729 |
fun wf_constraint_for_triple rel (sides, mains, concl) = |
|
730 |
map (wf_constraint_for rel sides concl) mains |
|
731 |
|> foldr1 HOLogic.mk_conj; |
|
732 |
||
733 |
fun terminates_by ctxt timeout goal tac = |
|
734 |
can (SINGLE (Classical.safe_tac ctxt) #> the |
|
735 |
#> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) #> the |
|
736 |
#> Goal.finish ctxt) goal; |
|
737 |
||
738 |
val max_cached_wfs = 50; |
|
739 |
val cached_timeout = Synchronized.var "Nunchaku_Collect.cached_timeout" Time.zeroTime; |
|
740 |
val cached_wf_props = Synchronized.var "Nunchaku_Collect.cached_wf_props" ([] : (term * bool) list); |
|
741 |
||
742 |
val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac]; |
|
743 |
||
744 |
fun is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout const intros = |
|
745 |
let |
|
746 |
val thy = Proof_Context.theory_of ctxt; |
|
747 |
||
748 |
val Const (x as (_, T)) = head_of (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd intros))); |
|
749 |
in |
|
750 |
(case triple_lookup (const_match thy o swap) wfs (dest_Const const) of |
|
751 |
SOME (SOME wf) => wf |
|
752 |
| _ => |
|
753 |
(case map (triple_for_intro_rule ctxt x) intros |> filter_out (null o #2) of |
|
754 |
[] => true |
|
755 |
| triples => |
|
756 |
let |
|
757 |
val binders_T = HOLogic.mk_tupleT (binder_types T); |
|
758 |
val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T)); |
|
759 |
val j = fold (Integer.max o maxidx_of_term) intros 0 + 1; |
|
760 |
val rel = (("R", j), rel_T); |
|
761 |
val prop = |
|
762 |
Const (@{const_name wf}, rel_T --> HOLogic.boolT) $ Var rel :: |
|
763 |
map (wf_constraint_for_triple rel) triples |
|
764 |
|> foldr1 HOLogic.mk_conj |
|
765 |
|> HOLogic.mk_Trueprop; |
|
766 |
in |
|
767 |
if debug then writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop) |
|
768 |
else (); |
|
769 |
if wf_timeout = Synchronized.value cached_timeout andalso |
|
770 |
length (Synchronized.value cached_wf_props) < max_cached_wfs then |
|
771 |
() |
|
772 |
else |
|
773 |
(Synchronized.change cached_wf_props (K []); |
|
774 |
Synchronized.change cached_timeout (K wf_timeout)); |
|
775 |
(case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of |
|
776 |
SOME wf => wf |
|
777 |
| NONE => |
|
778 |
let |
|
779 |
val goal = Goal.init (Thm.cterm_of ctxt prop); |
|
780 |
val wf = exists (terminates_by ctxt wf_timeout goal) termination_tacs; |
|
781 |
in |
|
782 |
Synchronized.change cached_wf_props (cons (prop, wf)); wf |
|
783 |
end) |
|
784 |
end) |
|
785 |
handle |
|
786 |
List.Empty => false |
|
787 |
| NO_TRIPLE () => false) |
|
788 |
end; |
|
789 |
||
790 |
datatype lhs_pat = |
|
791 |
Only_Vars |
|
792 |
| Prim_Pattern of string |
|
793 |
| Any_Pattern; |
|
794 |
||
66634
56456f388867
eliminate artifact of translation in printed Nunchaku model
blanchet
parents:
66624
diff
changeset
|
795 |
fun is_apparently_pat_complete ctxt props = |
64389 | 796 |
let |
797 |
val is_Var_or_Bound = is_Var orf is_Bound; |
|
798 |
||
799 |
fun lhs_pat_of t = |
|
800 |
(case t of |
|
801 |
Const (@{const_name All}, _) $ Abs (_, _, t) => lhs_pat_of t |
|
802 |
| Const (@{const_name HOL.eq}, _) $ u $ _ => |
|
803 |
(case filter_out is_Var_or_Bound (snd (strip_comb u)) of |
|
804 |
[] => Only_Vars |
|
805 |
| [v] => |
|
806 |
(case strip_comb v of |
|
807 |
(cst as Const (_, T), args) => |
|
808 |
(case body_type T of |
|
809 |
Type (T_name, _) => |
|
810 |
if can (Ctr_Sugar.dest_ctr ctxt T_name) cst andalso forall is_Var_or_Bound args then |
|
811 |
Prim_Pattern T_name |
|
812 |
else |
|
813 |
Any_Pattern |
|
814 |
| _ => Any_Pattern) |
|
815 |
| _ => Any_Pattern) |
|
816 |
| _ => Any_Pattern) |
|
817 |
| _ => Any_Pattern); |
|
818 |
in |
|
819 |
(case map lhs_pat_of props of |
|
820 |
[] => false |
|
821 |
| pats as Prim_Pattern T_name :: _ => |
|
822 |
forall (can (fn Prim_Pattern _ => ())) pats andalso |
|
823 |
length pats = length (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt T_name))) |
|
824 |
| pats => forall (curry (op =) Only_Vars) pats) |
|
825 |
end; |
|
826 |
||
827 |
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *) |
|
828 |
val axioms_max_depth = 255 |
|
829 |
||
830 |
fun isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals0 some_assms0 |
|
831 |
subgoal0 = |
|
832 |
let |
|
833 |
val thy = Proof_Context.theory_of ctxt; |
|
834 |
||
835 |
fun card_of T = |
|
836 |
(case triple_lookup (typ_match thy o swap) cards T of |
|
837 |
NONE => (NONE, NONE) |
|
838 |
| SOME (c1, c2) => (if c1 = SOME 1 then NONE else c1, c2)); |
|
839 |
||
840 |
fun axioms_of_class class = |
|
841 |
#axioms (Axclass.get_info thy class) |
|
842 |
handle ERROR _ => []; |
|
843 |
||
844 |
fun monomorphize_class_axiom T t = |
|
845 |
(case Term.add_tvars t [] of |
|
846 |
[] => t |
|
847 |
| [(x, S)] => Envir.subst_term_types (Vartab.make [(x, (S, T))]) t); |
|
848 |
||
849 |
fun consider_sort depth T S (seens as (seenS, seenT, seen), problem) = |
|
850 |
if member (op =) seenS S then |
|
851 |
(seens, problem) |
|
852 |
else if depth > axioms_max_depth then |
|
853 |
raise TOO_DEEP_DEPS () |
|
854 |
else |
|
855 |
let |
|
856 |
val seenS = S :: seenS; |
|
857 |
val seens = (seenS, seenT, seen); |
|
858 |
||
859 |
val supers = Sign.complete_sort thy S; |
|
860 |
val axioms0 = maps (map Thm.prop_of o axioms_of_class) supers; |
|
861 |
val axioms = map (preprocess_prop false ctxt whacks o monomorphize_class_axiom T) axioms0; |
|
862 |
in |
|
863 |
(seens, map IAxiom axioms @ problem) |
|
864 |
|> fold (consider_term (depth + 1)) axioms |
|
865 |
end |
|
866 |
and consider_type depth T = |
|
867 |
(case T of |
|
868 |
Type (s, Ts) => |
|
869 |
if is_type_builtin s then fold (consider_type depth) Ts |
|
870 |
else consider_non_builtin_type depth T |
|
871 |
| _ => consider_non_builtin_type depth T) |
|
872 |
and consider_non_builtin_type depth T (seens as (seenS, seenT, seen), problem) = |
|
873 |
if member (op =) seenT T then |
|
874 |
(seens, problem) |
|
875 |
else |
|
876 |
let |
|
877 |
val seenT = T :: seenT; |
|
878 |
val seens = (seenS, seenT, seen); |
|
879 |
||
64412 | 880 |
fun consider_typedef_or_quotient itypedef_or_quotient tuple_of s = |
64389 | 881 |
let |
66624 | 882 |
val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s; |
64389 | 883 |
val tyenv = Sign.typ_match thy (T0, T) Vartab.empty; |
884 |
val substT = Envir.subst_type tyenv; |
|
885 |
val subst = Envir.subst_term_types tyenv; |
|
886 |
val repT = substT repT0; |
|
66624 | 887 |
val wrt = preprocess_prop false ctxt whacks (subst wrt0); |
64389 | 888 |
val abs = subst abs0; |
889 |
val rep = subst rep0; |
|
890 |
in |
|
64412 | 891 |
apsnd (cons (itypedef_or_quotient {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs, |
64389 | 892 |
rep = rep})) |
893 |
#> consider_term (depth + 1) wrt |
|
894 |
end; |
|
895 |
in |
|
896 |
(seens, problem) |
|
897 |
|> (case T of |
|
898 |
TFree (_, S) => |
|
899 |
apsnd (cons (ITVal (T, card_of T))) |
|
900 |
#> consider_sort depth T S |
|
901 |
| TVar (_, S) => consider_sort depth T S |
|
902 |
| Type (s, Ts) => |
|
903 |
fold (consider_type depth) Ts |
|
904 |
#> (case classify_type_name ctxt s of |
|
905 |
Co_Datatype => |
|
906 |
let |
|
907 |
val (fp, fpTs, ctrss) = mutual_co_datatypes_of ctxt (s, Ts); |
|
908 |
val specs = map2 (fn T => fn ctrs => {typ = T, ctrs = ctrs}) fpTs ctrss; |
|
909 |
in |
|
910 |
(fn ((seenS, seenT, seen), problem) => |
|
911 |
((seenS, union (op =) fpTs seenT, seen), ICoData (fp, specs) :: problem)) |
|
912 |
#> fold (fold (consider_type (depth + 1) o fastype_of)) ctrss |
|
913 |
end |
|
64412 | 914 |
| Typedef => consider_typedef_or_quotient ITypedef typedef_of s |
915 |
| Quotient => consider_typedef_or_quotient IQuotient quotient_of s |
|
64389 | 916 |
| TVal => apsnd (cons (ITVal (T, card_of T))))) |
917 |
end |
|
918 |
and consider_term depth t = |
|
919 |
(case t of |
|
920 |
t1 $ t2 => fold (consider_term depth) [t1, t2] |
|
921 |
| Var (_, T) => consider_type depth T |
|
922 |
| Bound _ => I |
|
923 |
| Abs (_, T, t') => |
|
924 |
consider_term depth t' |
|
925 |
#> consider_type depth T |
|
926 |
| _ => (fn (seens as (seenS, seenT, seen), problem) => |
|
927 |
if member (op aconv) seen t then |
|
928 |
(seens, problem) |
|
929 |
else if depth > axioms_max_depth then |
|
930 |
raise TOO_DEEP_DEPS () |
|
931 |
else |
|
932 |
let |
|
933 |
val seen = t :: seen; |
|
934 |
val seens = (seenS, seenT, seen); |
|
935 |
in |
|
936 |
(case t of |
|
937 |
Const (x as (s, T)) => |
|
938 |
(if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse |
|
66624 | 939 |
is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse |
940 |
is_quotient_rep ctxt x orelse is_typedef_abs ctxt x orelse |
|
941 |
is_typedef_rep ctxt x then |
|
64389 | 942 |
(seens, problem) |
66624 | 943 |
else if is_stale_typedef_abs ctxt x orelse is_stale_typedef_rep ctxt x then |
64389 | 944 |
raise UNSUPPORTED_FUNC t |
945 |
else |
|
946 |
(case spec_rules_of ctxt x of |
|
947 |
SOME (classif, consts, props0, poly_props) => |
|
948 |
let |
|
949 |
val props = map (preprocess_prop false ctxt whacks) props0; |
|
950 |
||
951 |
fun def_or_spec () = |
|
952 |
(case definition_of thy x of |
|
953 |
SOME eq0 => |
|
954 |
let val eq = preprocess_prop false ctxt whacks eq0 in |
|
955 |
([eq], [IRec [{const = t, props = [eq], pat_complete = true}]]) |
|
956 |
end |
|
957 |
| NONE => (props, [ISpec {consts = consts, props = props}])); |
|
958 |
||
959 |
val (props', cmds) = |
|
960 |
if null props then |
|
961 |
([], map IVal consts) |
|
962 |
else if classif = Spec_Rules.Equational then |
|
963 |
(case partition_props consts props of |
|
964 |
SOME propss => |
|
965 |
(props, |
|
966 |
[IRec (map2 (fn const => fn props => |
|
967 |
{const = const, props = props, |
|
66634
56456f388867
eliminate artifact of translation in printed Nunchaku model
blanchet
parents:
66624
diff
changeset
|
968 |
pat_complete = is_apparently_pat_complete ctxt props}) |
64389 | 969 |
consts propss)]) |
970 |
| NONE => def_or_spec ()) |
|
971 |
else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive] |
|
972 |
classif then |
|
973 |
if is_inductive_set_intro (hd props) then |
|
974 |
def_or_spec () |
|
975 |
else |
|
976 |
(case partition_props consts props of |
|
977 |
SOME propss => |
|
978 |
(props, |
|
979 |
[ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP |
|
980 |
else BNF_Util.Greatest_FP, |
|
981 |
length consts = 1 andalso |
|
982 |
is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout |
|
983 |
(the_single consts) poly_props, |
|
984 |
map2 (fn const => fn props => {const = const, props = props}) |
|
985 |
consts propss)]) |
|
986 |
| NONE => def_or_spec ()) |
|
987 |
else |
|
988 |
def_or_spec (); |
|
989 |
in |
|
990 |
((seenS, seenT, union (op aconv) consts seen), cmds @ problem) |
|
991 |
|> fold (consider_term (depth + 1)) props' |
|
992 |
end |
|
993 |
| NONE => |
|
994 |
(case definition_of thy x of |
|
995 |
SOME eq0 => |
|
996 |
let val eq = preprocess_prop false ctxt whacks eq0 in |
|
997 |
(seens, IRec [{const = t, props = [eq], pat_complete = true}] :: problem) |
|
998 |
|> consider_term (depth + 1) eq |
|
999 |
end |
|
1000 |
| NONE => (seens, IVal t :: problem)))) |
|
1001 |
|> consider_type depth T |
|
1002 |
| Free (_, T) => |
|
1003 |
(seens, IVal t :: problem) |
|
1004 |
|> consider_type depth T) |
|
1005 |
end)); |
|
1006 |
||
1007 |
val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt |
|
1008 |
|> List.partition has_polymorphism; |
|
1009 |
||
1010 |
fun implicit_evals_of pol (@{const Not} $ t) = implicit_evals_of (not pol) t |
|
1011 |
| implicit_evals_of pol (@{const implies} $ t $ u) = |
|
1012 |
(case implicit_evals_of pol u of |
|
1013 |
[] => implicit_evals_of (not pol) t |
|
1014 |
| ts => ts) |
|
1015 |
| implicit_evals_of pol (@{const conj} $ t $ u) = |
|
1016 |
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u) |
|
1017 |
| implicit_evals_of pol (@{const disj} $ t $ u) = |
|
1018 |
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u) |
|
1019 |
| implicit_evals_of false (Const (@{const_name HOL.eq}, _) $ t $ u) = |
|
1020 |
distinct (op aconv) [t, u] |
|
1021 |
| implicit_evals_of true (Const (@{const_name HOL.eq}, _) $ t $ _) = [t] |
|
1022 |
| implicit_evals_of _ _ = []; |
|
1023 |
||
1024 |
val mono_axioms_and_some_assms = |
|
1025 |
map (preprocess_prop false ctxt whacks) (mono_axioms0 @ some_assms0); |
|
1026 |
val subgoal = preprocess_prop falsify ctxt whacks subgoal0; |
|
1027 |
val implicit_evals = implicit_evals_of true subgoal; |
|
1028 |
val evals = map (preprocess_closed_term ctxt whacks) evals0; |
|
1029 |
val seens = ([], [], []); |
|
1030 |
||
1031 |
val (commandss, complete) = |
|
1032 |
(seens, |
|
1033 |
map IAxiom mono_axioms_and_some_assms @ [IGoal subgoal] @ map IEval (implicit_evals @ evals)) |
|
1034 |
|> fold (consider_term 0) (subgoal :: evals @ mono_axioms_and_some_assms) |
|
1035 |
|> snd |
|
1036 |
|> rev (* prettier *) |
|
1037 |
|> sort_isa_commands_topologically ctxt |
|
1038 |
|>> group_isa_commands; |
|
1039 |
in |
|
1040 |
(poly_axioms, {commandss = commandss, sound = true, complete = complete}) |
|
1041 |
end; |
|
1042 |
||
1043 |
fun add_pat_complete_of_command cmd = |
|
1044 |
(case cmd of |
|
1045 |
ICoPred (_, _, specs) => union (op =) (map #const specs) |
|
1046 |
| IRec specs => |
|
1047 |
union (op =) (map_filter (try (fn {const, pat_complete = true, ...} => const)) specs) |
|
1048 |
| _ => I); |
|
1049 |
||
1050 |
fun pat_completes_of_isa_problem {commandss, ...} = |
|
1051 |
fold (fold add_pat_complete_of_command) commandss []; |
|
1052 |
||
1053 |
fun str_of_isa_term_with_type ctxt t = |
|
1054 |
Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t); |
|
1055 |
||
1056 |
fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body |
|
1057 |
| is_triv_wrt @{const True} = true |
|
1058 |
| is_triv_wrt _ = false; |
|
1059 |
||
1060 |
fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} = |
|
1061 |
Syntax.string_of_typ ctxt abs_typ ^ " := " ^ Syntax.string_of_typ ctxt rep_typ ^ |
|
1062 |
(if is_triv_wrt wrt then "" else "\n wrt " ^ Syntax.string_of_term ctxt wrt) ^ |
|
1063 |
"\n abstract " ^ Syntax.string_of_term ctxt abs ^ |
|
1064 |
"\n concrete " ^ Syntax.string_of_term ctxt rep; |
|
1065 |
||
1066 |
fun str_of_isa_co_data_spec ctxt {typ, ctrs} = |
|
1067 |
Syntax.string_of_typ ctxt typ ^ " :=\n " ^ |
|
1068 |
space_implode "\n| " (map (str_of_isa_term_with_type ctxt) ctrs); |
|
1069 |
||
1070 |
fun str_of_isa_const_spec ctxt {const, props} = |
|
1071 |
str_of_isa_term_with_type ctxt const ^ " :=\n " ^ |
|
1072 |
space_implode ";\n " (map (Syntax.string_of_term ctxt) props); |
|
1073 |
||
1074 |
fun str_of_isa_rec_spec ctxt {const, props, pat_complete} = |
|
1075 |
str_of_isa_term_with_type ctxt const ^ (if pat_complete then " [pat_complete]" else "") ^ |
|
66635 | 1076 |
" :=\n " ^ space_implode ";\n " (map (Syntax.string_of_term ctxt) props); |
64389 | 1077 |
|
1078 |
fun str_of_isa_consts_spec ctxt {consts, props} = |
|
1079 |
space_implode " and\n " (map (str_of_isa_term_with_type ctxt) consts) ^ " :=\n " ^ |
|
1080 |
space_implode ";\n " (map (Syntax.string_of_term ctxt) props); |
|
1081 |
||
1082 |
fun str_of_isa_card NONE = "" |
|
1083 |
| str_of_isa_card (SOME k) = signed_string_of_int k; |
|
1084 |
||
1085 |
fun str_of_isa_cards_suffix (NONE, NONE) = "" |
|
1086 |
| str_of_isa_cards_suffix (c1, c2) = " " ^ str_of_isa_card c1 ^ "-" ^ str_of_isa_card c2; |
|
1087 |
||
1088 |
fun str_of_isa_command ctxt (ITVal (T, cards)) = |
|
1089 |
"type " ^ Syntax.string_of_typ ctxt T ^ str_of_isa_cards_suffix cards |
|
64411
0af9926e1303
adapted Nunchaku's input syntax to new design decisions
blanchet
parents:
64389
diff
changeset
|
1090 |
| str_of_isa_command ctxt (ITypedef spec) = "typedef " ^ str_of_isa_type_spec ctxt spec |
64389 | 1091 |
| str_of_isa_command ctxt (IQuotient spec) = "quotient " ^ str_of_isa_type_spec ctxt spec |
1092 |
| str_of_isa_command ctxt (ICoData (fp, specs)) = |
|
1093 |
BNF_Util.case_fp fp "data" "codata" ^ " " ^ str_of_and_list (str_of_isa_co_data_spec ctxt) specs |
|
1094 |
| str_of_isa_command ctxt (IVal t) = "val " ^ str_of_isa_term_with_type ctxt t |
|
1095 |
| str_of_isa_command ctxt (ICoPred (fp, wf, specs)) = |
|
1096 |
BNF_Util.case_fp fp "pred" "copred" ^ " " ^ (if wf then "[wf] " else "") ^ |
|
1097 |
str_of_and_list (str_of_isa_const_spec ctxt) specs |
|
1098 |
| str_of_isa_command ctxt (IRec specs) = "rec " ^ str_of_and_list (str_of_isa_rec_spec ctxt) specs |
|
1099 |
| str_of_isa_command ctxt (ISpec spec) = "spec " ^ str_of_isa_consts_spec ctxt spec |
|
1100 |
| str_of_isa_command ctxt (IAxiom prop) = "axiom " ^ Syntax.string_of_term ctxt prop |
|
1101 |
| str_of_isa_command ctxt (IGoal prop) = "goal " ^ Syntax.string_of_term ctxt prop |
|
1102 |
| str_of_isa_command ctxt (IEval t) = "eval " ^ Syntax.string_of_term ctxt t; |
|
1103 |
||
1104 |
fun str_of_isa_problem ctxt {commandss, sound, complete} = |
|
1105 |
map (cat_lines o map (suffix "." o str_of_isa_command ctxt)) commandss |
|
1106 |
|> space_implode "\n\n" |> suffix "\n" |
|
1107 |
|> prefix ("# " ^ (if sound then "sound" else "unsound") ^ "\n") |
|
1108 |
|> prefix ("# " ^ (if complete then "complete" else "incomplete") ^ "\n"); |
|
1109 |
||
1110 |
end; |