equal
deleted
inserted
replaced
23 open Nitpick_Rep |
23 open Nitpick_Rep |
24 open Nitpick_Nut |
24 open Nitpick_Nut |
25 open Nitpick |
25 open Nitpick |
26 |
26 |
27 val auto = Unsynchronized.ref false |
27 val auto = Unsynchronized.ref false |
|
28 |
|
29 (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share |
|
30 its time slot with several other automatic tools. *) |
|
31 val max_auto_scopes = 6 |
28 |
32 |
29 val _ = |
33 val _ = |
30 ProofGeneralPgip.add_preference Preferences.category_tracing |
34 ProofGeneralPgip.add_preference Preferences.category_tracing |
31 (Preferences.bool_pref auto "auto-nitpick" |
35 (Preferences.bool_pref auto "auto-nitpick" |
32 "Run Nitpick automatically.") |
36 "Run Nitpick automatically.") |
221 Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) |
225 Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt) |
222 val lookup_term_list_polymorphic = |
226 val lookup_term_list_polymorphic = |
223 AList.lookup (op =) raw_params #> these #> map read_term_polymorphic |
227 AList.lookup (op =) raw_params #> these #> map read_term_polymorphic |
224 val read_const_polymorphic = read_term_polymorphic #> dest_Const |
228 val read_const_polymorphic = read_term_polymorphic #> dest_Const |
225 val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |
229 val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1 |
|
230 |> auto ? map (apsnd (take max_auto_scopes)) |
226 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 |
231 val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1 |
227 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 |
232 val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0 |
228 val bitss = lookup_int_seq "bits" 1 |
233 val bitss = lookup_int_seq "bits" 1 |
229 val bisim_depths = lookup_int_seq "bisim_depth" ~1 |
234 val bisim_depths = lookup_int_seq "bisim_depth" ~1 |
230 val boxes = lookup_bool_option_assigns read_type_polymorphic "box" |
235 val boxes = lookup_bool_option_assigns read_type_polymorphic "box" |