1.1 --- a/doc-src/Nitpick/nitpick.tex Sun Apr 25 00:10:30 2010 +0200
1.2 +++ b/doc-src/Nitpick/nitpick.tex Sun Apr 25 00:25:44 2010 +0200
1.3 @@ -2190,12 +2190,6 @@
1.4 {\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
1.5 \textit{batch\_size} (\S\ref{optimizations}).}
1.6
1.7 -\optrue{show\_skolems}{hide\_skolem}
1.8 -Specifies whether the values of Skolem constants should be displayed as part of
1.9 -counterexamples. Skolem constants correspond to bound variables in the original
1.10 -formula and usually help us to understand why the counterexample falsifies the
1.11 -formula.
1.12 -
1.13 \opfalse{show\_datatypes}{hide\_datatypes}
1.14 Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
1.15 be displayed as part of counterexamples. Such subsets are sometimes helpful when
1.16 @@ -2209,8 +2203,8 @@
1.17 genuine, but they can clutter the output.
1.18
1.19 \opfalse{show\_all}{dont\_show\_all}
1.20 -Enabling this option effectively enables \textit{show\_skolems},
1.21 -\textit{show\_datatypes}, and \textit{show\_consts}.
1.22 +Enabling this option effectively enables \textit{show\_datatypes} and
1.23 +\textit{show\_consts}.
1.24
1.25 \opdefault{max\_potential}{int}{$\mathbf{1}$}
1.26 Specifies the maximum number of potential counterexamples to display. Setting
2.1 --- a/src/HOL/Tools/Nitpick/HISTORY Sun Apr 25 00:10:30 2010 +0200
2.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Sun Apr 25 00:25:44 2010 +0200
2.3 @@ -17,8 +17,8 @@
2.4 * Added cache to speed up repeated Kodkod invocations on the same problems
2.5 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
2.6 "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
2.7 - * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and
2.8 - "sharing_depth" options
2.9 + * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
2.10 + "sharing_depth", and "show_skolems" options
2.11
2.12 Version 2009-1
2.13
3.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML Sun Apr 25 00:10:30 2010 +0200
3.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Sun Apr 25 00:25:44 2010 +0200
3.3 @@ -120,11 +120,10 @@
3.4 AssignRelReg of n_ary_index * rel_expr |
3.5 AssignIntReg of int * int_expr
3.6
3.7 - type 'a fold_expr_funcs = {
3.8 - formula_func: formula -> 'a -> 'a,
3.9 - rel_expr_func: rel_expr -> 'a -> 'a,
3.10 - int_expr_func: int_expr -> 'a -> 'a
3.11 - }
3.12 + type 'a fold_expr_funcs =
3.13 + {formula_func: formula -> 'a -> 'a,
3.14 + rel_expr_func: rel_expr -> 'a -> 'a,
3.15 + int_expr_func: int_expr -> 'a -> 'a}
3.16
3.17 val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
3.18 val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
3.19 @@ -132,10 +131,9 @@
3.20 val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
3.21 val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
3.22
3.23 - type 'a fold_tuple_funcs = {
3.24 - tuple_func: tuple -> 'a -> 'a,
3.25 - tuple_set_func: tuple_set -> 'a -> 'a
3.26 - }
3.27 + type 'a fold_tuple_funcs =
3.28 + {tuple_func: tuple -> 'a -> 'a,
3.29 + tuple_set_func: tuple_set -> 'a -> 'a}
3.30
3.31 val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
3.32 val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
3.33 @@ -144,15 +142,15 @@
3.34 'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
3.35 val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
3.36
3.37 - type problem = {
3.38 - comment: string,
3.39 - settings: setting list,
3.40 - univ_card: int,
3.41 - tuple_assigns: tuple_assign list,
3.42 - bounds: bound list,
3.43 - int_bounds: int_bound list,
3.44 - expr_assigns: expr_assign list,
3.45 - formula: formula}
3.46 + type problem =
3.47 + {comment: string,
3.48 + settings: setting list,
3.49 + univ_card: int,
3.50 + tuple_assigns: tuple_assign list,
3.51 + bounds: bound list,
3.52 + int_bounds: int_bound list,
3.53 + expr_assigns: expr_assign list,
3.54 + formula: formula}
3.55
3.56 type raw_bound = n_ary_index * int list list
3.57
3.58 @@ -291,15 +289,15 @@
3.59 AssignRelReg of n_ary_index * rel_expr |
3.60 AssignIntReg of int * int_expr
3.61
3.62 -type problem = {
3.63 - comment: string,
3.64 - settings: setting list,
3.65 - univ_card: int,
3.66 - tuple_assigns: tuple_assign list,
3.67 - bounds: bound list,
3.68 - int_bounds: int_bound list,
3.69 - expr_assigns: expr_assign list,
3.70 - formula: formula}
3.71 +type problem =
3.72 + {comment: string,
3.73 + settings: setting list,
3.74 + univ_card: int,
3.75 + tuple_assigns: tuple_assign list,
3.76 + bounds: bound list,
3.77 + int_bounds: int_bound list,
3.78 + expr_assigns: expr_assign list,
3.79 + formula: formula}
3.80
3.81 type raw_bound = n_ary_index * int list list
3.82
3.83 @@ -313,11 +311,10 @@
3.84
3.85 exception SYNTAX of string * string
3.86
3.87 -type 'a fold_expr_funcs = {
3.88 - formula_func: formula -> 'a -> 'a,
3.89 - rel_expr_func: rel_expr -> 'a -> 'a,
3.90 - int_expr_func: int_expr -> 'a -> 'a
3.91 -}
3.92 +type 'a fold_expr_funcs =
3.93 + {formula_func: formula -> 'a -> 'a,
3.94 + rel_expr_func: rel_expr -> 'a -> 'a,
3.95 + int_expr_func: int_expr -> 'a -> 'a}
3.96
3.97 (** Auxiliary functions on ML representation of Kodkod problems **)
3.98
3.99 @@ -419,10 +416,9 @@
3.100 | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
3.101 | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
3.102
3.103 -type 'a fold_tuple_funcs = {
3.104 - tuple_func: tuple -> 'a -> 'a,
3.105 - tuple_set_func: tuple_set -> 'a -> 'a
3.106 -}
3.107 +type 'a fold_tuple_funcs =
3.108 + {tuple_func: tuple -> 'a -> 'a,
3.109 + tuple_set_func: tuple_set -> 'a -> 'a}
3.110
3.111 fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
3.112 fun fold_tuple_set F tuple_set =
4.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 00:10:30 2010 +0200
4.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 00:25:44 2010 +0200
4.3 @@ -9,46 +9,45 @@
4.4 sig
4.5 type styp = Nitpick_Util.styp
4.6 type term_postprocessor = Nitpick_Model.term_postprocessor
4.7 - type params = {
4.8 - cards_assigns: (typ option * int list) list,
4.9 - maxes_assigns: (styp option * int list) list,
4.10 - iters_assigns: (styp option * int list) list,
4.11 - bitss: int list,
4.12 - bisim_depths: int list,
4.13 - boxes: (typ option * bool option) list,
4.14 - finitizes: (typ option * bool option) list,
4.15 - monos: (typ option * bool option) list,
4.16 - stds: (typ option * bool) list,
4.17 - wfs: (styp option * bool option) list,
4.18 - sat_solver: string,
4.19 - blocking: bool,
4.20 - falsify: bool,
4.21 - debug: bool,
4.22 - verbose: bool,
4.23 - overlord: bool,
4.24 - user_axioms: bool option,
4.25 - assms: bool,
4.26 - merge_type_vars: bool,
4.27 - binary_ints: bool option,
4.28 - destroy_constrs: bool,
4.29 - specialize: bool,
4.30 - star_linear_preds: bool,
4.31 - fast_descrs: bool,
4.32 - peephole_optim: bool,
4.33 - timeout: Time.time option,
4.34 - tac_timeout: Time.time option,
4.35 - max_threads: int,
4.36 - show_skolems: bool,
4.37 - show_datatypes: bool,
4.38 - show_consts: bool,
4.39 - evals: term list,
4.40 - formats: (term option * int list) list,
4.41 - max_potential: int,
4.42 - max_genuine: int,
4.43 - check_potential: bool,
4.44 - check_genuine: bool,
4.45 - batch_size: int,
4.46 - expect: string}
4.47 + type params =
4.48 + {cards_assigns: (typ option * int list) list,
4.49 + maxes_assigns: (styp option * int list) list,
4.50 + iters_assigns: (styp option * int list) list,
4.51 + bitss: int list,
4.52 + bisim_depths: int list,
4.53 + boxes: (typ option * bool option) list,
4.54 + finitizes: (typ option * bool option) list,
4.55 + monos: (typ option * bool option) list,
4.56 + stds: (typ option * bool) list,
4.57 + wfs: (styp option * bool option) list,
4.58 + sat_solver: string,
4.59 + blocking: bool,
4.60 + falsify: bool,
4.61 + debug: bool,
4.62 + verbose: bool,
4.63 + overlord: bool,
4.64 + user_axioms: bool option,
4.65 + assms: bool,
4.66 + merge_type_vars: bool,
4.67 + binary_ints: bool option,
4.68 + destroy_constrs: bool,
4.69 + specialize: bool,
4.70 + star_linear_preds: bool,
4.71 + fast_descrs: bool,
4.72 + peephole_optim: bool,
4.73 + timeout: Time.time option,
4.74 + tac_timeout: Time.time option,
4.75 + max_threads: int,
4.76 + show_datatypes: bool,
4.77 + show_consts: bool,
4.78 + evals: term list,
4.79 + formats: (term option * int list) list,
4.80 + max_potential: int,
4.81 + max_genuine: int,
4.82 + check_potential: bool,
4.83 + check_genuine: bool,
4.84 + batch_size: int,
4.85 + expect: string}
4.86
4.87 val register_frac_type : string -> (string * string) list -> theory -> theory
4.88 val unregister_frac_type : string -> theory -> theory
4.89 @@ -80,55 +79,54 @@
4.90
4.91 structure KK = Kodkod
4.92
4.93 -type params = {
4.94 - cards_assigns: (typ option * int list) list,
4.95 - maxes_assigns: (styp option * int list) list,
4.96 - iters_assigns: (styp option * int list) list,
4.97 - bitss: int list,
4.98 - bisim_depths: int list,
4.99 - boxes: (typ option * bool option) list,
4.100 - finitizes: (typ option * bool option) list,
4.101 - monos: (typ option * bool option) list,
4.102 - stds: (typ option * bool) list,
4.103 - wfs: (styp option * bool option) list,
4.104 - sat_solver: string,
4.105 - blocking: bool,
4.106 - falsify: bool,
4.107 - debug: bool,
4.108 - verbose: bool,
4.109 - overlord: bool,
4.110 - user_axioms: bool option,
4.111 - assms: bool,
4.112 - merge_type_vars: bool,
4.113 - binary_ints: bool option,
4.114 - destroy_constrs: bool,
4.115 - specialize: bool,
4.116 - star_linear_preds: bool,
4.117 - fast_descrs: bool,
4.118 - peephole_optim: bool,
4.119 - timeout: Time.time option,
4.120 - tac_timeout: Time.time option,
4.121 - max_threads: int,
4.122 - show_skolems: bool,
4.123 - show_datatypes: bool,
4.124 - show_consts: bool,
4.125 - evals: term list,
4.126 - formats: (term option * int list) list,
4.127 - max_potential: int,
4.128 - max_genuine: int,
4.129 - check_potential: bool,
4.130 - check_genuine: bool,
4.131 - batch_size: int,
4.132 - expect: string}
4.133 +type params =
4.134 + {cards_assigns: (typ option * int list) list,
4.135 + maxes_assigns: (styp option * int list) list,
4.136 + iters_assigns: (styp option * int list) list,
4.137 + bitss: int list,
4.138 + bisim_depths: int list,
4.139 + boxes: (typ option * bool option) list,
4.140 + finitizes: (typ option * bool option) list,
4.141 + monos: (typ option * bool option) list,
4.142 + stds: (typ option * bool) list,
4.143 + wfs: (styp option * bool option) list,
4.144 + sat_solver: string,
4.145 + blocking: bool,
4.146 + falsify: bool,
4.147 + debug: bool,
4.148 + verbose: bool,
4.149 + overlord: bool,
4.150 + user_axioms: bool option,
4.151 + assms: bool,
4.152 + merge_type_vars: bool,
4.153 + binary_ints: bool option,
4.154 + destroy_constrs: bool,
4.155 + specialize: bool,
4.156 + star_linear_preds: bool,
4.157 + fast_descrs: bool,
4.158 + peephole_optim: bool,
4.159 + timeout: Time.time option,
4.160 + tac_timeout: Time.time option,
4.161 + max_threads: int,
4.162 + show_datatypes: bool,
4.163 + show_consts: bool,
4.164 + evals: term list,
4.165 + formats: (term option * int list) list,
4.166 + max_potential: int,
4.167 + max_genuine: int,
4.168 + check_potential: bool,
4.169 + check_genuine: bool,
4.170 + batch_size: int,
4.171 + expect: string}
4.172
4.173 -type problem_extension = {
4.174 - free_names: nut list,
4.175 - sel_names: nut list,
4.176 - nonsel_names: nut list,
4.177 - rel_table: nut NameTable.table,
4.178 - unsound: bool,
4.179 - scope: scope}
4.180 -
4.181 +type problem_extension =
4.182 + {free_names: nut list,
4.183 + sel_names: nut list,
4.184 + nonsel_names: nut list,
4.185 + rel_table: nut NameTable.table,
4.186 + unsound: bool,
4.187 + scope: scope}
4.188 +
4.189 type rich_problem = KK.problem * problem_extension
4.190
4.191 fun pretties_for_formulas _ _ [] = []
4.192 @@ -191,10 +189,9 @@
4.193 boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
4.194 verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
4.195 destroy_constrs, specialize, star_linear_preds, fast_descrs,
4.196 - peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
4.197 - show_consts, evals, formats, max_potential, max_genuine,
4.198 - check_potential, check_genuine, batch_size, ...} =
4.199 - params
4.200 + peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
4.201 + evals, formats, max_potential, max_genuine, check_potential,
4.202 + check_genuine, batch_size, ...} = params
4.203 val state_ref = Unsynchronized.ref state
4.204 val pprint =
4.205 if auto then
4.206 @@ -580,8 +577,7 @@
4.207 : problem_extension) =
4.208 let
4.209 val (reconstructed_model, codatatypes_ok) =
4.210 - reconstruct_hol_model {show_skolems = show_skolems,
4.211 - show_datatypes = show_datatypes,
4.212 + reconstruct_hol_model {show_datatypes = show_datatypes,
4.213 show_consts = show_consts}
4.214 scope formats frees free_names sel_names nonsel_names rel_table
4.215 bounds
5.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 25 00:10:30 2010 +0200
5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 25 00:25:44 2010 +0200
5.3 @@ -13,37 +13,37 @@
5.4 type unrolled = styp * styp
5.5 type wf_cache = (styp * (bool * bool)) list
5.6
5.7 - type hol_context = {
5.8 - thy: theory,
5.9 - ctxt: Proof.context,
5.10 - max_bisim_depth: int,
5.11 - boxes: (typ option * bool option) list,
5.12 - stds: (typ option * bool) list,
5.13 - wfs: (styp option * bool option) list,
5.14 - user_axioms: bool option,
5.15 - debug: bool,
5.16 - binary_ints: bool option,
5.17 - destroy_constrs: bool,
5.18 - specialize: bool,
5.19 - star_linear_preds: bool,
5.20 - fast_descrs: bool,
5.21 - tac_timeout: Time.time option,
5.22 - evals: term list,
5.23 - case_names: (string * int) list,
5.24 - def_table: const_table,
5.25 - nondef_table: const_table,
5.26 - user_nondefs: term list,
5.27 - simp_table: const_table Unsynchronized.ref,
5.28 - psimp_table: const_table,
5.29 - choice_spec_table: const_table,
5.30 - intro_table: const_table,
5.31 - ground_thm_table: term list Inttab.table,
5.32 - ersatz_table: (string * string) list,
5.33 - skolems: (string * string list) list Unsynchronized.ref,
5.34 - special_funs: special_fun list Unsynchronized.ref,
5.35 - unrolled_preds: unrolled list Unsynchronized.ref,
5.36 - wf_cache: wf_cache Unsynchronized.ref,
5.37 - constr_cache: (typ * styp list) list Unsynchronized.ref}
5.38 + type hol_context =
5.39 + {thy: theory,
5.40 + ctxt: Proof.context,
5.41 + max_bisim_depth: int,
5.42 + boxes: (typ option * bool option) list,
5.43 + stds: (typ option * bool) list,
5.44 + wfs: (styp option * bool option) list,
5.45 + user_axioms: bool option,
5.46 + debug: bool,
5.47 + binary_ints: bool option,
5.48 + destroy_constrs: bool,
5.49 + specialize: bool,
5.50 + star_linear_preds: bool,
5.51 + fast_descrs: bool,
5.52 + tac_timeout: Time.time option,
5.53 + evals: term list,
5.54 + case_names: (string * int) list,
5.55 + def_table: const_table,
5.56 + nondef_table: const_table,
5.57 + user_nondefs: term list,
5.58 + simp_table: const_table Unsynchronized.ref,
5.59 + psimp_table: const_table,
5.60 + choice_spec_table: const_table,
5.61 + intro_table: const_table,
5.62 + ground_thm_table: term list Inttab.table,
5.63 + ersatz_table: (string * string) list,
5.64 + skolems: (string * string list) list Unsynchronized.ref,
5.65 + special_funs: special_fun list Unsynchronized.ref,
5.66 + unrolled_preds: unrolled list Unsynchronized.ref,
5.67 + wf_cache: wf_cache Unsynchronized.ref,
5.68 + constr_cache: (typ * styp list) list Unsynchronized.ref}
5.69
5.70 datatype fixpoint_kind = Lfp | Gfp | NoFp
5.71 datatype boxability =
5.72 @@ -222,37 +222,37 @@
5.73 type unrolled = styp * styp
5.74 type wf_cache = (styp * (bool * bool)) list
5.75
5.76 -type hol_context = {
5.77 - thy: theory,
5.78 - ctxt: Proof.context,
5.79 - max_bisim_depth: int,
5.80 - boxes: (typ option * bool option) list,
5.81 - stds: (typ option * bool) list,
5.82 - wfs: (styp option * bool option) list,
5.83 - user_axioms: bool option,
5.84 - debug: bool,
5.85 - binary_ints: bool option,
5.86 - destroy_constrs: bool,
5.87 - specialize: bool,
5.88 - star_linear_preds: bool,
5.89 - fast_descrs: bool,
5.90 - tac_timeout: Time.time option,
5.91 - evals: term list,
5.92 - case_names: (string * int) list,
5.93 - def_table: const_table,
5.94 - nondef_table: const_table,
5.95 - user_nondefs: term list,
5.96 - simp_table: const_table Unsynchronized.ref,
5.97 - psimp_table: const_table,
5.98 - choice_spec_table: const_table,
5.99 - intro_table: const_table,
5.100 - ground_thm_table: term list Inttab.table,
5.101 - ersatz_table: (string * string) list,
5.102 - skolems: (string * string list) list Unsynchronized.ref,
5.103 - special_funs: special_fun list Unsynchronized.ref,
5.104 - unrolled_preds: unrolled list Unsynchronized.ref,
5.105 - wf_cache: wf_cache Unsynchronized.ref,
5.106 - constr_cache: (typ * styp list) list Unsynchronized.ref}
5.107 +type hol_context =
5.108 + {thy: theory,
5.109 + ctxt: Proof.context,
5.110 + max_bisim_depth: int,
5.111 + boxes: (typ option * bool option) list,
5.112 + stds: (typ option * bool) list,
5.113 + wfs: (styp option * bool option) list,
5.114 + user_axioms: bool option,
5.115 + debug: bool,
5.116 + binary_ints: bool option,
5.117 + destroy_constrs: bool,
5.118 + specialize: bool,
5.119 + star_linear_preds: bool,
5.120 + fast_descrs: bool,
5.121 + tac_timeout: Time.time option,
5.122 + evals: term list,
5.123 + case_names: (string * int) list,
5.124 + def_table: const_table,
5.125 + nondef_table: const_table,
5.126 + user_nondefs: term list,
5.127 + simp_table: const_table Unsynchronized.ref,
5.128 + psimp_table: const_table,
5.129 + choice_spec_table: const_table,
5.130 + intro_table: const_table,
5.131 + ground_thm_table: term list Inttab.table,
5.132 + ersatz_table: (string * string) list,
5.133 + skolems: (string * string list) list Unsynchronized.ref,
5.134 + special_funs: special_fun list Unsynchronized.ref,
5.135 + unrolled_preds: unrolled list Unsynchronized.ref,
5.136 + wf_cache: wf_cache Unsynchronized.ref,
5.137 + constr_cache: (typ * styp list) list Unsynchronized.ref}
5.138
5.139 datatype fixpoint_kind = Lfp | Gfp | NoFp
5.140 datatype boxability =
6.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Apr 25 00:10:30 2010 +0200
6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Apr 25 00:25:44 2010 +0200
6.3 @@ -65,7 +65,6 @@
6.4 ("verbose", "false"),
6.5 ("overlord", "false"),
6.6 ("show_all", "false"),
6.7 - ("show_skolems", "true"),
6.8 ("show_datatypes", "false"),
6.9 ("show_consts", "false"),
6.10 ("format", "1"),
6.11 @@ -95,7 +94,6 @@
6.12 ("quiet", "verbose"),
6.13 ("no_overlord", "overlord"),
6.14 ("dont_show_all", "show_all"),
6.15 - ("hide_skolems", "show_skolems"),
6.16 ("hide_datatypes", "show_datatypes"),
6.17 ("hide_consts", "show_consts"),
6.18 ("trust_potential", "check_potential"),
6.19 @@ -255,7 +253,6 @@
6.20 val tac_timeout = lookup_time "tac_timeout"
6.21 val max_threads = Int.max (0, lookup_int "max_threads")
6.22 val show_all = debug orelse lookup_bool "show_all"
6.23 - val show_skolems = show_all orelse lookup_bool "show_skolems"
6.24 val show_datatypes = show_all orelse lookup_bool "show_datatypes"
6.25 val show_consts = show_all orelse lookup_bool "show_consts"
6.26 val formats = lookup_ints_assigns read_term_polymorphic "format" 0
6.27 @@ -265,9 +262,10 @@
6.28 val max_genuine = Int.max (0, lookup_int "max_genuine")
6.29 val check_potential = lookup_bool "check_potential"
6.30 val check_genuine = lookup_bool "check_genuine"
6.31 - val batch_size = case lookup_int_option "batch_size" of
6.32 - SOME n => Int.max (1, n)
6.33 - | NONE => if debug then 1 else 64
6.34 + val batch_size =
6.35 + case lookup_int_option "batch_size" of
6.36 + SOME n => Int.max (1, n)
6.37 + | NONE => if debug then 1 else 64
6.38 val expect = lookup_string "expect"
6.39 in
6.40 {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
6.41 @@ -281,11 +279,10 @@
6.42 star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
6.43 peephole_optim = peephole_optim, timeout = timeout,
6.44 tac_timeout = tac_timeout, max_threads = max_threads,
6.45 - show_skolems = show_skolems, show_datatypes = show_datatypes,
6.46 - show_consts = show_consts, formats = formats, evals = evals,
6.47 - max_potential = max_potential, max_genuine = max_genuine,
6.48 - check_potential = check_potential, check_genuine = check_genuine,
6.49 - batch_size = batch_size, expect = expect}
6.50 + show_datatypes = show_datatypes, show_consts = show_consts,
6.51 + formats = formats, evals = evals, max_potential = max_potential,
6.52 + max_genuine = max_genuine, check_potential = check_potential,
6.53 + check_genuine = check_genuine, batch_size = batch_size, expect = expect}
6.54 end
6.55
6.56 fun default_params thy =
6.57 @@ -382,7 +379,7 @@
6.58 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
6.59
6.60 val _ = OuterSyntax.improper_command "nitpick"
6.61 - "try to find a counterexample for a given subgoal using Kodkod"
6.62 + "try to find a counterexample for a given subgoal using Nitpick"
6.63 K.diag parse_nitpick_command
6.64 val _ = OuterSyntax.command "nitpick_params"
6.65 "set and display the default parameters for Nitpick"
7.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Apr 25 00:10:30 2010 +0200
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Apr 25 00:25:44 2010 +0200
7.3 @@ -12,10 +12,10 @@
7.4 type rep = Nitpick_Rep.rep
7.5 type nut = Nitpick_Nut.nut
7.6
7.7 - type params = {
7.8 - show_skolems: bool,
7.9 - show_datatypes: bool,
7.10 - show_consts: bool}
7.11 + type params =
7.12 + {show_datatypes: bool,
7.13 + show_consts: bool}
7.14 +
7.15 type term_postprocessor =
7.16 Proof.context -> string -> (typ -> term list) -> typ -> term -> term
7.17
7.18 @@ -51,10 +51,9 @@
7.19
7.20 structure KK = Kodkod
7.21
7.22 -type params = {
7.23 - show_skolems: bool,
7.24 - show_datatypes: bool,
7.25 - show_consts: bool}
7.26 +type params =
7.27 + {show_datatypes: bool,
7.28 + show_consts: bool}
7.29
7.30 type term_postprocessor =
7.31 Proof.context -> string -> (typ -> term list) -> typ -> term -> term
7.32 @@ -840,7 +839,7 @@
7.33 t1 = t2
7.34 end
7.35
7.36 -fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
7.37 +fun reconstruct_hol_model {show_datatypes, show_consts}
7.38 ({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
7.39 debug, binary_ints, destroy_constrs, specialize,
7.40 star_linear_preds, fast_descrs, tac_timeout, evals,
7.41 @@ -980,7 +979,7 @@
7.42 | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
7.43 [Const x])) all_frees
7.44 val chunks = block_of_names true "Free variable" free_names @
7.45 - block_of_names show_skolems "Skolem constant" skolem_names @
7.46 + block_of_names true "Skolem constant" skolem_names @
7.47 block_of_names true "Evaluated term" eval_names @
7.48 block_of_datatypes @ block_of_codatatypes @
7.49 block_of_names show_consts "Constant"
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sun Apr 25 00:10:30 2010 +0200
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sun Apr 25 00:25:44 2010 +0200
8.3 @@ -14,11 +14,11 @@
8.4 type decl = Kodkod.decl
8.5 type expr_assign = Kodkod.expr_assign
8.6
8.7 - type name_pool = {
8.8 - rels: n_ary_index list,
8.9 - vars: n_ary_index list,
8.10 - formula_reg: int,
8.11 - rel_reg: int}
8.12 + type name_pool =
8.13 + {rels: n_ary_index list,
8.14 + vars: n_ary_index list,
8.15 + formula_reg: int,
8.16 + rel_reg: int}
8.17
8.18 val initial_pool : name_pool
8.19 val not3_rel : n_ary_index
8.20 @@ -51,39 +51,38 @@
8.21 val num_seq : int -> int -> int_expr list
8.22 val s_and : formula -> formula -> formula
8.23
8.24 - type kodkod_constrs = {
8.25 - kk_all: decl list -> formula -> formula,
8.26 - kk_exist: decl list -> formula -> formula,
8.27 - kk_formula_let: expr_assign list -> formula -> formula,
8.28 - kk_formula_if: formula -> formula -> formula -> formula,
8.29 - kk_or: formula -> formula -> formula,
8.30 - kk_not: formula -> formula,
8.31 - kk_iff: formula -> formula -> formula,
8.32 - kk_implies: formula -> formula -> formula,
8.33 - kk_and: formula -> formula -> formula,
8.34 - kk_subset: rel_expr -> rel_expr -> formula,
8.35 - kk_rel_eq: rel_expr -> rel_expr -> formula,
8.36 - kk_no: rel_expr -> formula,
8.37 - kk_lone: rel_expr -> formula,
8.38 - kk_one: rel_expr -> formula,
8.39 - kk_some: rel_expr -> formula,
8.40 - kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
8.41 - kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
8.42 - kk_union: rel_expr -> rel_expr -> rel_expr,
8.43 - kk_difference: rel_expr -> rel_expr -> rel_expr,
8.44 - kk_override: rel_expr -> rel_expr -> rel_expr,
8.45 - kk_intersect: rel_expr -> rel_expr -> rel_expr,
8.46 - kk_product: rel_expr -> rel_expr -> rel_expr,
8.47 - kk_join: rel_expr -> rel_expr -> rel_expr,
8.48 - kk_closure: rel_expr -> rel_expr,
8.49 - kk_reflexive_closure: rel_expr -> rel_expr,
8.50 - kk_comprehension: decl list -> formula -> rel_expr,
8.51 - kk_project: rel_expr -> int_expr list -> rel_expr,
8.52 - kk_project_seq: rel_expr -> int -> int -> rel_expr,
8.53 - kk_not3: rel_expr -> rel_expr,
8.54 - kk_nat_less: rel_expr -> rel_expr -> rel_expr,
8.55 - kk_int_less: rel_expr -> rel_expr -> rel_expr
8.56 - }
8.57 + type kodkod_constrs =
8.58 + {kk_all: decl list -> formula -> formula,
8.59 + kk_exist: decl list -> formula -> formula,
8.60 + kk_formula_let: expr_assign list -> formula -> formula,
8.61 + kk_formula_if: formula -> formula -> formula -> formula,
8.62 + kk_or: formula -> formula -> formula,
8.63 + kk_not: formula -> formula,
8.64 + kk_iff: formula -> formula -> formula,
8.65 + kk_implies: formula -> formula -> formula,
8.66 + kk_and: formula -> formula -> formula,
8.67 + kk_subset: rel_expr -> rel_expr -> formula,
8.68 + kk_rel_eq: rel_expr -> rel_expr -> formula,
8.69 + kk_no: rel_expr -> formula,
8.70 + kk_lone: rel_expr -> formula,
8.71 + kk_one: rel_expr -> formula,
8.72 + kk_some: rel_expr -> formula,
8.73 + kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
8.74 + kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
8.75 + kk_union: rel_expr -> rel_expr -> rel_expr,
8.76 + kk_difference: rel_expr -> rel_expr -> rel_expr,
8.77 + kk_override: rel_expr -> rel_expr -> rel_expr,
8.78 + kk_intersect: rel_expr -> rel_expr -> rel_expr,
8.79 + kk_product: rel_expr -> rel_expr -> rel_expr,
8.80 + kk_join: rel_expr -> rel_expr -> rel_expr,
8.81 + kk_closure: rel_expr -> rel_expr,
8.82 + kk_reflexive_closure: rel_expr -> rel_expr,
8.83 + kk_comprehension: decl list -> formula -> rel_expr,
8.84 + kk_project: rel_expr -> int_expr list -> rel_expr,
8.85 + kk_project_seq: rel_expr -> int -> int -> rel_expr,
8.86 + kk_not3: rel_expr -> rel_expr,
8.87 + kk_nat_less: rel_expr -> rel_expr -> rel_expr,
8.88 + kk_int_less: rel_expr -> rel_expr -> rel_expr}
8.89
8.90 val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
8.91 end;
8.92 @@ -94,11 +93,11 @@
8.93 open Kodkod
8.94 open Nitpick_Util
8.95
8.96 -type name_pool = {
8.97 - rels: n_ary_index list,
8.98 - vars: n_ary_index list,
8.99 - formula_reg: int,
8.100 - rel_reg: int}
8.101 +type name_pool =
8.102 + {rels: n_ary_index list,
8.103 + vars: n_ary_index list,
8.104 + formula_reg: int,
8.105 + rel_reg: int}
8.106
8.107 (* If you add new built-in relations, make sure to increment the counters here
8.108 as well to avoid name clashes (which fortunately would be detected by
8.109 @@ -204,39 +203,38 @@
8.110 | s_and _ False = False
8.111 | s_and f1 f2 = And (f1, f2)
8.112
8.113 -type kodkod_constrs = {
8.114 - kk_all: decl list -> formula -> formula,
8.115 - kk_exist: decl list -> formula -> formula,
8.116 - kk_formula_let: expr_assign list -> formula -> formula,
8.117 - kk_formula_if: formula -> formula -> formula -> formula,
8.118 - kk_or: formula -> formula -> formula,
8.119 - kk_not: formula -> formula,
8.120 - kk_iff: formula -> formula -> formula,
8.121 - kk_implies: formula -> formula -> formula,
8.122 - kk_and: formula -> formula -> formula,
8.123 - kk_subset: rel_expr -> rel_expr -> formula,
8.124 - kk_rel_eq: rel_expr -> rel_expr -> formula,
8.125 - kk_no: rel_expr -> formula,
8.126 - kk_lone: rel_expr -> formula,
8.127 - kk_one: rel_expr -> formula,
8.128 - kk_some: rel_expr -> formula,
8.129 - kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
8.130 - kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
8.131 - kk_union: rel_expr -> rel_expr -> rel_expr,
8.132 - kk_difference: rel_expr -> rel_expr -> rel_expr,
8.133 - kk_override: rel_expr -> rel_expr -> rel_expr,
8.134 - kk_intersect: rel_expr -> rel_expr -> rel_expr,
8.135 - kk_product: rel_expr -> rel_expr -> rel_expr,
8.136 - kk_join: rel_expr -> rel_expr -> rel_expr,
8.137 - kk_closure: rel_expr -> rel_expr,
8.138 - kk_reflexive_closure: rel_expr -> rel_expr,
8.139 - kk_comprehension: decl list -> formula -> rel_expr,
8.140 - kk_project: rel_expr -> int_expr list -> rel_expr,
8.141 - kk_project_seq: rel_expr -> int -> int -> rel_expr,
8.142 - kk_not3: rel_expr -> rel_expr,
8.143 - kk_nat_less: rel_expr -> rel_expr -> rel_expr,
8.144 - kk_int_less: rel_expr -> rel_expr -> rel_expr
8.145 -}
8.146 +type kodkod_constrs =
8.147 + {kk_all: decl list -> formula -> formula,
8.148 + kk_exist: decl list -> formula -> formula,
8.149 + kk_formula_let: expr_assign list -> formula -> formula,
8.150 + kk_formula_if: formula -> formula -> formula -> formula,
8.151 + kk_or: formula -> formula -> formula,
8.152 + kk_not: formula -> formula,
8.153 + kk_iff: formula -> formula -> formula,
8.154 + kk_implies: formula -> formula -> formula,
8.155 + kk_and: formula -> formula -> formula,
8.156 + kk_subset: rel_expr -> rel_expr -> formula,
8.157 + kk_rel_eq: rel_expr -> rel_expr -> formula,
8.158 + kk_no: rel_expr -> formula,
8.159 + kk_lone: rel_expr -> formula,
8.160 + kk_one: rel_expr -> formula,
8.161 + kk_some: rel_expr -> formula,
8.162 + kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
8.163 + kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
8.164 + kk_union: rel_expr -> rel_expr -> rel_expr,
8.165 + kk_difference: rel_expr -> rel_expr -> rel_expr,
8.166 + kk_override: rel_expr -> rel_expr -> rel_expr,
8.167 + kk_intersect: rel_expr -> rel_expr -> rel_expr,
8.168 + kk_product: rel_expr -> rel_expr -> rel_expr,
8.169 + kk_join: rel_expr -> rel_expr -> rel_expr,
8.170 + kk_closure: rel_expr -> rel_expr,
8.171 + kk_reflexive_closure: rel_expr -> rel_expr,
8.172 + kk_comprehension: decl list -> formula -> rel_expr,
8.173 + kk_project: rel_expr -> int_expr list -> rel_expr,
8.174 + kk_project_seq: rel_expr -> int -> int -> rel_expr,
8.175 + kk_not3: rel_expr -> rel_expr,
8.176 + kk_nat_less: rel_expr -> rel_expr -> rel_expr,
8.177 + kk_int_less: rel_expr -> rel_expr -> rel_expr}
8.178
8.179 (* We assume throughout that Kodkod variables have a "one" constraint. This is
8.180 always the case if Kodkod's skolemization is disabled. *)
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Apr 25 00:10:30 2010 +0200
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Apr 25 00:25:44 2010 +0200
9.3 @@ -10,32 +10,32 @@
9.4 type styp = Nitpick_Util.styp
9.5 type hol_context = Nitpick_HOL.hol_context
9.6
9.7 - type constr_spec = {
9.8 - const: styp,
9.9 - delta: int,
9.10 - epsilon: int,
9.11 - exclusive: bool,
9.12 - explicit_max: int,
9.13 - total: bool}
9.14 + type constr_spec =
9.15 + {const: styp,
9.16 + delta: int,
9.17 + epsilon: int,
9.18 + exclusive: bool,
9.19 + explicit_max: int,
9.20 + total: bool}
9.21
9.22 - type dtype_spec = {
9.23 - typ: typ,
9.24 - card: int,
9.25 - co: bool,
9.26 - standard: bool,
9.27 - complete: bool * bool,
9.28 - concrete: bool * bool,
9.29 - deep: bool,
9.30 - constrs: constr_spec list}
9.31 + type dtype_spec =
9.32 + {typ: typ,
9.33 + card: int,
9.34 + co: bool,
9.35 + standard: bool,
9.36 + complete: bool * bool,
9.37 + concrete: bool * bool,
9.38 + deep: bool,
9.39 + constrs: constr_spec list}
9.40
9.41 - type scope = {
9.42 - hol_ctxt: hol_context,
9.43 - binarize: bool,
9.44 - card_assigns: (typ * int) list,
9.45 - bits: int,
9.46 - bisim_depth: int,
9.47 - datatypes: dtype_spec list,
9.48 - ofs: int Typtab.table}
9.49 + type scope =
9.50 + {hol_ctxt: hol_context,
9.51 + binarize: bool,
9.52 + card_assigns: (typ * int) list,
9.53 + bits: int,
9.54 + bisim_depth: int,
9.55 + datatypes: dtype_spec list,
9.56 + ofs: int Typtab.table}
9.57
9.58 val datatype_spec : dtype_spec list -> typ -> dtype_spec option
9.59 val constr_spec : dtype_spec list -> styp -> constr_spec
9.60 @@ -61,32 +61,32 @@
9.61 open Nitpick_Util
9.62 open Nitpick_HOL
9.63
9.64 -type constr_spec = {
9.65 - const: styp,
9.66 - delta: int,
9.67 - epsilon: int,
9.68 - exclusive: bool,
9.69 - explicit_max: int,
9.70 - total: bool}
9.71 +type constr_spec =
9.72 + {const: styp,
9.73 + delta: int,
9.74 + epsilon: int,
9.75 + exclusive: bool,
9.76 + explicit_max: int,
9.77 + total: bool}
9.78
9.79 -type dtype_spec = {
9.80 - typ: typ,
9.81 - card: int,
9.82 - co: bool,
9.83 - standard: bool,
9.84 - complete: bool * bool,
9.85 - concrete: bool * bool,
9.86 - deep: bool,
9.87 - constrs: constr_spec list}
9.88 +type dtype_spec =
9.89 + {typ: typ,
9.90 + card: int,
9.91 + co: bool,
9.92 + standard: bool,
9.93 + complete: bool * bool,
9.94 + concrete: bool * bool,
9.95 + deep: bool,
9.96 + constrs: constr_spec list}
9.97
9.98 -type scope = {
9.99 - hol_ctxt: hol_context,
9.100 - binarize: bool,
9.101 - card_assigns: (typ * int) list,
9.102 - bits: int,
9.103 - bisim_depth: int,
9.104 - datatypes: dtype_spec list,
9.105 - ofs: int Typtab.table}
9.106 +type scope =
9.107 + {hol_ctxt: hol_context,
9.108 + binarize: bool,
9.109 + card_assigns: (typ * int) list,
9.110 + bits: int,
9.111 + bisim_depth: int,
9.112 + datatypes: dtype_spec list,
9.113 + ofs: int Typtab.table}
9.114
9.115 datatype row_kind = Card of typ | Max of styp
9.116