|
1 (* Title: HOL/Nitpick/Tools/nitpick_scope.ML |
|
2 Author: Jasmin Blanchette, TU Muenchen |
|
3 Copyright 2008, 2009 |
|
4 |
|
5 Scope enumerator for Nitpick. |
|
6 *) |
|
7 |
|
8 signature NITPICK_SCOPE = |
|
9 sig |
|
10 type extended_context = NitpickHOL.extended_context |
|
11 |
|
12 type constr_spec = { |
|
13 const: styp, |
|
14 delta: int, |
|
15 epsilon: int, |
|
16 exclusive: bool, |
|
17 explicit_max: int, |
|
18 total: bool} |
|
19 |
|
20 type dtype_spec = { |
|
21 typ: typ, |
|
22 card: int, |
|
23 co: bool, |
|
24 precise: bool, |
|
25 constrs: constr_spec list} |
|
26 |
|
27 type scope = { |
|
28 ext_ctxt: extended_context, |
|
29 card_assigns: (typ * int) list, |
|
30 bisim_depth: int, |
|
31 datatypes: dtype_spec list, |
|
32 ofs: int Typtab.table} |
|
33 |
|
34 val datatype_spec : dtype_spec list -> typ -> dtype_spec option |
|
35 val constr_spec : dtype_spec list -> styp -> constr_spec |
|
36 val is_precise_type : dtype_spec list -> typ -> bool |
|
37 val is_fully_comparable_type : dtype_spec list -> typ -> bool |
|
38 val offset_of_type : int Typtab.table -> typ -> int |
|
39 val spec_of_type : scope -> typ -> int * int |
|
40 val pretties_for_scope : scope -> bool -> Pretty.T list |
|
41 val multiline_string_for_scope : scope -> string |
|
42 val scopes_equivalent : scope -> scope -> bool |
|
43 val scope_less_eq : scope -> scope -> bool |
|
44 val all_scopes : |
|
45 extended_context -> int -> (typ option * int list) list |
|
46 -> (styp option * int list) list -> (styp option * int list) list |
|
47 -> int list -> typ list -> typ list -> scope list |
|
48 end; |
|
49 |
|
50 structure NitpickScope : NITPICK_SCOPE = |
|
51 struct |
|
52 |
|
53 open NitpickUtil |
|
54 open NitpickHOL |
|
55 |
|
56 type constr_spec = { |
|
57 const: styp, |
|
58 delta: int, |
|
59 epsilon: int, |
|
60 exclusive: bool, |
|
61 explicit_max: int, |
|
62 total: bool} |
|
63 |
|
64 type dtype_spec = { |
|
65 typ: typ, |
|
66 card: int, |
|
67 co: bool, |
|
68 precise: bool, |
|
69 constrs: constr_spec list} |
|
70 |
|
71 type scope = { |
|
72 ext_ctxt: extended_context, |
|
73 card_assigns: (typ * int) list, |
|
74 bisim_depth: int, |
|
75 datatypes: dtype_spec list, |
|
76 ofs: int Typtab.table} |
|
77 |
|
78 datatype row_kind = Card of typ | Max of styp |
|
79 |
|
80 type row = row_kind * int list |
|
81 type block = row list |
|
82 |
|
83 (* dtype_spec list -> typ -> dtype_spec option *) |
|
84 fun datatype_spec (dtypes : dtype_spec list) T = |
|
85 List.find (equal T o #typ) dtypes |
|
86 |
|
87 (* dtype_spec list -> styp -> constr_spec *) |
|
88 fun constr_spec [] x = raise TERM ("NitpickScope.constr_spec", [Const x]) |
|
89 | constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) = |
|
90 case List.find (equal (s, body_type T) o (apsnd body_type o #const)) |
|
91 constrs of |
|
92 SOME c => c |
|
93 | NONE => constr_spec dtypes x |
|
94 |
|
95 (* dtype_spec list -> typ -> bool *) |
|
96 fun is_precise_type dtypes (Type ("fun", Ts)) = |
|
97 forall (is_precise_type dtypes) Ts |
|
98 | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts |
|
99 | is_precise_type dtypes T = |
|
100 T <> nat_T andalso T <> int_T |
|
101 andalso #precise (the (datatype_spec dtypes T)) |
|
102 handle Option.Option => true |
|
103 fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) = |
|
104 is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2 |
|
105 | is_fully_comparable_type dtypes (Type ("*", Ts)) = |
|
106 forall (is_fully_comparable_type dtypes) Ts |
|
107 | is_fully_comparable_type _ _ = true |
|
108 |
|
109 (* int Typtab.table -> typ -> int *) |
|
110 fun offset_of_type ofs T = |
|
111 case Typtab.lookup ofs T of |
|
112 SOME j0 => j0 |
|
113 | NONE => Typtab.lookup ofs dummyT |> the_default 0 |
|
114 |
|
115 (* scope -> typ -> int * int *) |
|
116 fun spec_of_type ({card_assigns, ofs, ...} : scope) T = |
|
117 (card_of_type card_assigns T |
|
118 handle TYPE ("NitpickHOL.card_of_type", _, _) => ~1, offset_of_type ofs T) |
|
119 |
|
120 (* (string -> string) -> scope |
|
121 -> string list * string list * string list * string list * string list *) |
|
122 fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns, |
|
123 bisim_depth, datatypes, ...} : scope) = |
|
124 let |
|
125 val (iter_asgns, card_asgns) = |
|
126 card_assigns |> filter_out (equal @{typ bisim_iterator} o fst) |
|
127 |> List.partition (is_fp_iterator_type o fst) |
|
128 val (unimportant_card_asgns, important_card_asgns) = |
|
129 card_asgns |> List.partition ((is_datatype thy orf is_integer_type) o fst) |
|
130 val cards = |
|
131 map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^ |
|
132 string_of_int k) |
|
133 fun maxes () = |
|
134 maps (map_filter |
|
135 (fn {const, explicit_max, ...} => |
|
136 if explicit_max < 0 then |
|
137 NONE |
|
138 else |
|
139 SOME (Syntax.string_of_term ctxt (Const const) ^ " = " ^ |
|
140 string_of_int explicit_max)) |
|
141 o #constrs) datatypes |
|
142 fun iters () = |
|
143 map (fn (T, k) => |
|
144 quote (Syntax.string_of_term ctxt |
|
145 (Const (const_for_iterator_type T))) ^ " = " ^ |
|
146 string_of_int (k - 1)) iter_asgns |
|
147 fun bisims () = |
|
148 if bisim_depth < 0 andalso forall (not o #co) datatypes then [] |
|
149 else ["bisim_depth = " ^ string_of_int bisim_depth] |
|
150 in |
|
151 setmp_show_all_types |
|
152 (fn () => (cards important_card_asgns, cards unimportant_card_asgns, |
|
153 maxes (), iters (), bisims ())) () |
|
154 end |
|
155 |
|
156 (* scope -> bool -> Pretty.T list *) |
|
157 fun pretties_for_scope scope verbose = |
|
158 let |
|
159 val (important_cards, unimportant_cards, maxes, iters, bisim_depths) = |
|
160 quintuple_for_scope maybe_quote scope |
|
161 val ss = map (prefix "card ") important_cards @ |
|
162 (if verbose then |
|
163 map (prefix "card ") unimportant_cards @ |
|
164 map (prefix "max ") maxes @ |
|
165 map (prefix "iter ") iters @ |
|
166 bisim_depths |
|
167 else |
|
168 []) |
|
169 in |
|
170 if null ss then [] |
|
171 else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks |
|
172 end |
|
173 |
|
174 (* scope -> string *) |
|
175 fun multiline_string_for_scope scope = |
|
176 let |
|
177 val (important_cards, unimportant_cards, maxes, iters, bisim_depths) = |
|
178 quintuple_for_scope I scope |
|
179 val cards = important_cards @ unimportant_cards |
|
180 in |
|
181 case (if null cards then [] else ["card: " ^ commas cards]) @ |
|
182 (if null maxes then [] else ["max: " ^ commas maxes]) @ |
|
183 (if null iters then [] else ["iter: " ^ commas iters]) @ |
|
184 bisim_depths of |
|
185 [] => "empty" |
|
186 | lines => space_implode "\n" lines |
|
187 end |
|
188 |
|
189 (* scope -> scope -> bool *) |
|
190 fun scopes_equivalent (s1 : scope) (s2 : scope) = |
|
191 #datatypes s1 = #datatypes s2 andalso #card_assigns s1 = #card_assigns s2 |
|
192 fun scope_less_eq (s1 : scope) (s2 : scope) = |
|
193 (s1, s2) |> pairself (map snd o #card_assigns) |> op ~~ |> forall (op <=) |
|
194 |
|
195 (* row -> int *) |
|
196 fun rank_of_row (_, ks) = length ks |
|
197 (* block -> int *) |
|
198 fun rank_of_block block = fold Integer.max (map rank_of_row block) 1 |
|
199 (* int -> typ * int list -> typ * int list *) |
|
200 fun project_row column (y, ks) = (y, [nth ks (Int.min (column, length ks - 1))]) |
|
201 (* int -> block -> block *) |
|
202 fun project_block (column, block) = map (project_row column) block |
|
203 |
|
204 (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *) |
|
205 fun lookup_ints_assign eq asgns key = |
|
206 case triple_lookup eq asgns key of |
|
207 SOME ks => ks |
|
208 | NONE => raise ARG ("NitpickScope.lookup_ints_assign", "") |
|
209 (* theory -> (typ option * int list) list -> typ -> int list *) |
|
210 fun lookup_type_ints_assign thy asgns T = |
|
211 map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T) |
|
212 handle ARG ("NitpickScope.lookup_ints_assign", _) => |
|
213 raise TYPE ("NitpickScope.lookup_type_ints_assign", [T], []) |
|
214 (* theory -> (styp option * int list) list -> styp -> int list *) |
|
215 fun lookup_const_ints_assign thy asgns x = |
|
216 lookup_ints_assign (const_match thy) asgns x |
|
217 handle ARG ("NitpickScope.lookup_ints_assign", _) => |
|
218 raise TERM ("NitpickScope.lookup_const_ints_assign", [Const x]) |
|
219 |
|
220 (* theory -> (styp option * int list) list -> styp -> row option *) |
|
221 fun row_for_constr thy maxes_asgns constr = |
|
222 SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr) |
|
223 handle TERM ("lookup_const_ints_assign", _) => NONE |
|
224 |
|
225 (* Proof.context -> (typ option * int list) list |
|
226 -> (styp option * int list) list -> (styp option * int list) list -> int list |
|
227 -> typ -> block *) |
|
228 fun block_for_type ctxt cards_asgns maxes_asgns iters_asgns bisim_depths T = |
|
229 let val thy = ProofContext.theory_of ctxt in |
|
230 if T = @{typ bisim_iterator} then |
|
231 [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)] |
|
232 else if is_fp_iterator_type T then |
|
233 [(Card T, map (fn k => Int.max (0, k) + 1) |
|
234 (lookup_const_ints_assign thy iters_asgns |
|
235 (const_for_iterator_type T)))] |
|
236 else |
|
237 (Card T, lookup_type_ints_assign thy cards_asgns T) :: |
|
238 (case datatype_constrs thy T of |
|
239 [_] => [] |
|
240 | constrs => map_filter (row_for_constr thy maxes_asgns) constrs) |
|
241 end |
|
242 |
|
243 (* Proof.context -> (typ option * int list) list |
|
244 -> (styp option * int list) list -> (styp option * int list) list -> int list |
|
245 -> typ list -> typ list -> block list *) |
|
246 fun blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns bisim_depths |
|
247 mono_Ts nonmono_Ts = |
|
248 let |
|
249 val thy = ProofContext.theory_of ctxt |
|
250 (* typ -> block *) |
|
251 val block_for = block_for_type ctxt cards_asgns maxes_asgns iters_asgns |
|
252 bisim_depths |
|
253 val mono_block = maps block_for mono_Ts |
|
254 val nonmono_blocks = map block_for nonmono_Ts |
|
255 in mono_block :: nonmono_blocks end |
|
256 |
|
257 val sync_threshold = 5 |
|
258 |
|
259 (* int list -> int list list *) |
|
260 fun all_combinations_ordered_smartly ks = |
|
261 let |
|
262 (* int list -> int *) |
|
263 fun cost_with_monos [] = 0 |
|
264 | cost_with_monos (k :: ks) = |
|
265 if k < sync_threshold andalso forall (equal k) ks then |
|
266 k - sync_threshold |
|
267 else |
|
268 k * (k + 1) div 2 + Integer.sum ks |
|
269 fun cost_without_monos [] = 0 |
|
270 | cost_without_monos [k] = k |
|
271 | cost_without_monos (_ :: k :: ks) = |
|
272 if k < sync_threshold andalso forall (equal k) ks then |
|
273 k - sync_threshold |
|
274 else |
|
275 Integer.sum (k :: ks) |
|
276 in |
|
277 ks |> all_combinations |
|
278 |> map (`(if fst (hd ks) > 1 then cost_with_monos |
|
279 else cost_without_monos)) |
|
280 |> sort (int_ord o pairself fst) |> map snd |
|
281 end |
|
282 |
|
283 (* typ -> bool *) |
|
284 fun is_self_recursive_constr_type T = |
|
285 exists (exists_subtype (equal (body_type T))) (binder_types T) |
|
286 |
|
287 (* (styp * int) list -> styp -> int *) |
|
288 fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x) |
|
289 |
|
290 type scope_desc = (typ * int) list * (styp * int) list |
|
291 |
|
292 (* theory -> scope_desc -> typ * int -> bool *) |
|
293 fun is_surely_inconsistent_card_assign thy (card_asgns, max_asgns) (T, k) = |
|
294 case datatype_constrs thy T of |
|
295 [] => false |
|
296 | xs => |
|
297 let |
|
298 val precise_cards = |
|
299 map (Integer.prod |
|
300 o map (bounded_precise_card_of_type thy k 0 card_asgns) |
|
301 o binder_types o snd) xs |
|
302 val maxes = map (constr_max max_asgns) xs |
|
303 (* int -> int -> int *) |
|
304 fun effective_max 0 ~1 = k |
|
305 | effective_max 0 max = max |
|
306 | effective_max card ~1 = card |
|
307 | effective_max card max = Int.min (card, max) |
|
308 val max = map2 effective_max precise_cards maxes |> Integer.sum |
|
309 (* unit -> int *) |
|
310 fun doms_card () = |
|
311 xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_asgns) |
|
312 o binder_types o snd) |
|
313 |> Integer.sum |
|
314 in |
|
315 max < k |
|
316 orelse (forall (not_equal 0) precise_cards andalso doms_card () < k) |
|
317 end |
|
318 handle TYPE ("NitpickHOL.card_of_type", _, _) => false |
|
319 |
|
320 (* theory -> scope_desc -> bool *) |
|
321 fun is_surely_inconsistent_scope_description thy (desc as (card_asgns, _)) = |
|
322 exists (is_surely_inconsistent_card_assign thy desc) card_asgns |
|
323 |
|
324 (* theory -> scope_desc -> (typ * int) list option *) |
|
325 fun repair_card_assigns thy (card_asgns, max_asgns) = |
|
326 let |
|
327 (* (typ * int) list -> (typ * int) list -> (typ * int) list option *) |
|
328 fun aux seen [] = SOME seen |
|
329 | aux seen ((T, 0) :: _) = NONE |
|
330 | aux seen ((T, k) :: asgns) = |
|
331 (if is_surely_inconsistent_scope_description thy |
|
332 ((T, k) :: seen, max_asgns) then |
|
333 raise SAME () |
|
334 else |
|
335 case aux ((T, k) :: seen) asgns of |
|
336 SOME asgns => SOME asgns |
|
337 | NONE => raise SAME ()) |
|
338 handle SAME () => aux seen ((T, k - 1) :: asgns) |
|
339 in aux [] (rev card_asgns) end |
|
340 |
|
341 (* theory -> (typ * int) list -> typ * int -> typ * int *) |
|
342 fun repair_iterator_assign thy asgns (T as Type (s, Ts), k) = |
|
343 (T, if T = @{typ bisim_iterator} then |
|
344 let val co_cards = map snd (filter (is_codatatype thy o fst) asgns) in |
|
345 Int.min (k, Integer.sum co_cards) |
|
346 end |
|
347 else if is_fp_iterator_type T then |
|
348 case Ts of |
|
349 [] => 1 |
|
350 | _ => bounded_card_of_type k ~1 asgns (foldr1 HOLogic.mk_prodT Ts) |
|
351 else |
|
352 k) |
|
353 | repair_iterator_assign _ _ asgn = asgn |
|
354 |
|
355 (* row -> scope_desc -> scope_desc *) |
|
356 fun add_row_to_scope_descriptor (kind, ks) (card_asgns, max_asgns) = |
|
357 case kind of |
|
358 Card T => ((T, the_single ks) :: card_asgns, max_asgns) |
|
359 | Max x => (card_asgns, (x, the_single ks) :: max_asgns) |
|
360 (* block -> scope_desc *) |
|
361 fun scope_descriptor_from_block block = |
|
362 fold_rev add_row_to_scope_descriptor block ([], []) |
|
363 (* theory -> block list -> int list -> scope_desc option *) |
|
364 fun scope_descriptor_from_combination thy blocks columns = |
|
365 let |
|
366 val (card_asgns, max_asgns) = |
|
367 maps project_block (columns ~~ blocks) |> scope_descriptor_from_block |
|
368 val card_asgns = repair_card_assigns thy (card_asgns, max_asgns) |> the |
|
369 in |
|
370 SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns) |
|
371 end |
|
372 handle Option.Option => NONE |
|
373 |
|
374 (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *) |
|
375 fun offset_table_for_card_assigns thy asgns dtypes = |
|
376 let |
|
377 (* int -> (int * int) list -> (typ * int) list -> int Typtab.table |
|
378 -> int Typtab.table *) |
|
379 fun aux next _ [] = Typtab.update_new (dummyT, next) |
|
380 | aux next reusable ((T, k) :: asgns) = |
|
381 if k = 1 orelse is_integer_type T then |
|
382 aux next reusable asgns |
|
383 else if length (these (Option.map #constrs (datatype_spec dtypes T))) |
|
384 > 1 then |
|
385 Typtab.update_new (T, next) #> aux (next + k) reusable asgns |
|
386 else |
|
387 case AList.lookup (op =) reusable k of |
|
388 SOME j0 => Typtab.update_new (T, j0) #> aux next reusable asgns |
|
389 | NONE => Typtab.update_new (T, next) |
|
390 #> aux (next + k) ((k, next) :: reusable) asgns |
|
391 in aux 0 [] asgns Typtab.empty end |
|
392 |
|
393 (* int -> (typ * int) list -> typ -> int *) |
|
394 fun domain_card max card_asgns = |
|
395 Integer.prod o map (bounded_card_of_type max max card_asgns) o binder_types |
|
396 |
|
397 (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp |
|
398 -> constr_spec list -> constr_spec list *) |
|
399 fun add_constr_spec (card_asgns, max_asgns) co card sum_dom_cards num_self_recs |
|
400 num_non_self_recs (self_rec, x as (s, T)) constrs = |
|
401 let |
|
402 val max = constr_max max_asgns x |
|
403 (* int -> int *) |
|
404 fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k) |
|
405 (* unit -> int *) |
|
406 fun next_delta () = if null constrs then 0 else #epsilon (hd constrs) |
|
407 val {delta, epsilon, exclusive, total} = |
|
408 if max = 0 then |
|
409 let val delta = next_delta () in |
|
410 {delta = delta, epsilon = delta, exclusive = true, total = false} |
|
411 end |
|
412 else if not co andalso num_self_recs > 0 then |
|
413 if not self_rec andalso num_non_self_recs = 1 |
|
414 andalso domain_card 2 card_asgns T = 1 then |
|
415 {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}), |
|
416 total = true} |
|
417 else if s = @{const_name Cons} then |
|
418 {delta = 1, epsilon = card, exclusive = true, total = false} |
|
419 else |
|
420 {delta = 0, epsilon = card, exclusive = false, total = false} |
|
421 else if card = sum_dom_cards (card + 1) then |
|
422 let val delta = next_delta () in |
|
423 {delta = delta, epsilon = delta + domain_card card card_asgns T, |
|
424 exclusive = true, total = true} |
|
425 end |
|
426 else |
|
427 {delta = 0, epsilon = card, |
|
428 exclusive = (num_self_recs + num_non_self_recs = 1), total = false} |
|
429 in |
|
430 {const = x, delta = delta, epsilon = epsilon, exclusive = exclusive, |
|
431 explicit_max = max, total = total} :: constrs |
|
432 end |
|
433 |
|
434 (* extended_context -> scope_desc -> typ * int -> dtype_spec *) |
|
435 fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) |
|
436 (desc as (card_asgns, _)) (T, card) = |
|
437 let |
|
438 val co = is_codatatype thy T |
|
439 val xs = boxed_datatype_constrs ext_ctxt T |
|
440 val self_recs = map (is_self_recursive_constr_type o snd) xs |
|
441 val (num_self_recs, num_non_self_recs) = |
|
442 List.partition (equal true) self_recs |> pairself length |
|
443 val precise = (card = bounded_precise_card_of_type thy (card + 1) 0 |
|
444 card_asgns T) |
|
445 (* int -> int *) |
|
446 fun sum_dom_cards max = |
|
447 map (domain_card max card_asgns o snd) xs |> Integer.sum |
|
448 val constrs = |
|
449 fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs |
|
450 num_non_self_recs) (self_recs ~~ xs) [] |
|
451 in {typ = T, card = card, co = co, precise = precise, constrs = constrs} end |
|
452 |
|
453 (* extended_context -> int -> scope_desc -> scope *) |
|
454 fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break |
|
455 (desc as (card_asgns, _)) = |
|
456 let |
|
457 val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc) |
|
458 (filter (is_datatype thy o fst) card_asgns) |
|
459 val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1 |
|
460 in |
|
461 {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes, |
|
462 bisim_depth = bisim_depth, |
|
463 ofs = if sym_break <= 0 then Typtab.empty |
|
464 else offset_table_for_card_assigns thy card_asgns datatypes} |
|
465 end |
|
466 |
|
467 (* theory -> typ list -> (typ option * int list) list |
|
468 -> (typ option * int list) list *) |
|
469 fun fix_cards_assigns_wrt_boxing _ _ [] = [] |
|
470 | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_asgns) = |
|
471 (if is_fun_type T orelse is_pair_type T then |
|
472 Ts |> filter (curry (type_match thy o swap) T o unbox_type) |
|
473 |> map (rpair ks o SOME) |
|
474 else |
|
475 [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_asgns |
|
476 | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) = |
|
477 (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns |
|
478 |
|
479 val distinct_threshold = 512 |
|
480 |
|
481 (* extended_context -> int -> (typ option * int list) list |
|
482 -> (styp option * int list) list -> (styp option * int list) list -> int list |
|
483 -> typ list -> typ list -> scope list *) |
|
484 fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns |
|
485 iters_asgns bisim_depths mono_Ts nonmono_Ts = |
|
486 let |
|
487 val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns |
|
488 val blocks = blocks_for_types ctxt cards_asgns maxes_asgns iters_asgns |
|
489 bisim_depths mono_Ts nonmono_Ts |
|
490 val ranks = map rank_of_block blocks |
|
491 val descs = all_combinations_ordered_smartly (map (rpair 0) ranks) |
|
492 |> map_filter (scope_descriptor_from_combination thy blocks) |
|
493 in |
|
494 descs |> length descs <= distinct_threshold ? distinct (op =) |
|
495 |> map (scope_from_descriptor ext_ctxt sym_break) |
|
496 end |
|
497 |
|
498 end; |