--- a/doc-src/Nitpick/nitpick.tex Sun Apr 25 00:10:30 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Sun Apr 25 00:25:44 2010 +0200
@@ -2190,12 +2190,6 @@
{\small See also \textit{overlord} (\S\ref{mode-of-operation}) and
\textit{batch\_size} (\S\ref{optimizations}).}
-\optrue{show\_skolems}{hide\_skolem}
-Specifies whether the values of Skolem constants should be displayed as part of
-counterexamples. Skolem constants correspond to bound variables in the original
-formula and usually help us to understand why the counterexample falsifies the
-formula.
-
\opfalse{show\_datatypes}{hide\_datatypes}
Specifies whether the subsets used to approximate (co)in\-duc\-tive datatypes should
be displayed as part of counterexamples. Such subsets are sometimes helpful when
@@ -2209,8 +2203,8 @@
genuine, but they can clutter the output.
\opfalse{show\_all}{dont\_show\_all}
-Enabling this option effectively enables \textit{show\_skolems},
-\textit{show\_datatypes}, and \textit{show\_consts}.
+Enabling this option effectively enables \textit{show\_datatypes} and
+\textit{show\_consts}.
\opdefault{max\_potential}{int}{$\mathbf{1}$}
Specifies the maximum number of potential counterexamples to display. Setting
--- a/src/HOL/Tools/Nitpick/HISTORY Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/HISTORY Sun Apr 25 00:25:44 2010 +0200
@@ -17,8 +17,8 @@
* Added cache to speed up repeated Kodkod invocations on the same problems
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
- * Removed "skolemize", "uncurry", "sym_break", "flatten_prop", and
- "sharing_depth" options
+ * Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
+ "sharing_depth", and "show_skolems" options
Version 2009-1
--- a/src/HOL/Tools/Nitpick/kodkod.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Sun Apr 25 00:25:44 2010 +0200
@@ -120,11 +120,10 @@
AssignRelReg of n_ary_index * rel_expr |
AssignIntReg of int * int_expr
- type 'a fold_expr_funcs = {
- formula_func: formula -> 'a -> 'a,
- rel_expr_func: rel_expr -> 'a -> 'a,
- int_expr_func: int_expr -> 'a -> 'a
- }
+ type 'a fold_expr_funcs =
+ {formula_func: formula -> 'a -> 'a,
+ rel_expr_func: rel_expr -> 'a -> 'a,
+ int_expr_func: int_expr -> 'a -> 'a}
val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
@@ -132,10 +131,9 @@
val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
- type 'a fold_tuple_funcs = {
- tuple_func: tuple -> 'a -> 'a,
- tuple_set_func: tuple_set -> 'a -> 'a
- }
+ type 'a fold_tuple_funcs =
+ {tuple_func: tuple -> 'a -> 'a,
+ tuple_set_func: tuple_set -> 'a -> 'a}
val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
@@ -144,15 +142,15 @@
'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
- type problem = {
- comment: string,
- settings: setting list,
- univ_card: int,
- tuple_assigns: tuple_assign list,
- bounds: bound list,
- int_bounds: int_bound list,
- expr_assigns: expr_assign list,
- formula: formula}
+ type problem =
+ {comment: string,
+ settings: setting list,
+ univ_card: int,
+ tuple_assigns: tuple_assign list,
+ bounds: bound list,
+ int_bounds: int_bound list,
+ expr_assigns: expr_assign list,
+ formula: formula}
type raw_bound = n_ary_index * int list list
@@ -291,15 +289,15 @@
AssignRelReg of n_ary_index * rel_expr |
AssignIntReg of int * int_expr
-type problem = {
- comment: string,
- settings: setting list,
- univ_card: int,
- tuple_assigns: tuple_assign list,
- bounds: bound list,
- int_bounds: int_bound list,
- expr_assigns: expr_assign list,
- formula: formula}
+type problem =
+ {comment: string,
+ settings: setting list,
+ univ_card: int,
+ tuple_assigns: tuple_assign list,
+ bounds: bound list,
+ int_bounds: int_bound list,
+ expr_assigns: expr_assign list,
+ formula: formula}
type raw_bound = n_ary_index * int list list
@@ -313,11 +311,10 @@
exception SYNTAX of string * string
-type 'a fold_expr_funcs = {
- formula_func: formula -> 'a -> 'a,
- rel_expr_func: rel_expr -> 'a -> 'a,
- int_expr_func: int_expr -> 'a -> 'a
-}
+type 'a fold_expr_funcs =
+ {formula_func: formula -> 'a -> 'a,
+ rel_expr_func: rel_expr -> 'a -> 'a,
+ int_expr_func: int_expr -> 'a -> 'a}
(** Auxiliary functions on ML representation of Kodkod problems **)
@@ -419,10 +416,9 @@
| AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
| AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
-type 'a fold_tuple_funcs = {
- tuple_func: tuple -> 'a -> 'a,
- tuple_set_func: tuple_set -> 'a -> 'a
-}
+type 'a fold_tuple_funcs =
+ {tuple_func: tuple -> 'a -> 'a,
+ tuple_set_func: tuple_set -> 'a -> 'a}
fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
fun fold_tuple_set F tuple_set =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 00:25:44 2010 +0200
@@ -9,46 +9,45 @@
sig
type styp = Nitpick_Util.styp
type term_postprocessor = Nitpick_Model.term_postprocessor
- type params = {
- cards_assigns: (typ option * int list) list,
- maxes_assigns: (styp option * int list) list,
- iters_assigns: (styp option * int list) list,
- bitss: int list,
- bisim_depths: int list,
- boxes: (typ option * bool option) list,
- finitizes: (typ option * bool option) list,
- monos: (typ option * bool option) list,
- stds: (typ option * bool) list,
- wfs: (styp option * bool option) list,
- sat_solver: string,
- blocking: bool,
- falsify: bool,
- debug: bool,
- verbose: bool,
- overlord: bool,
- user_axioms: bool option,
- assms: bool,
- merge_type_vars: bool,
- binary_ints: bool option,
- destroy_constrs: bool,
- specialize: bool,
- star_linear_preds: bool,
- fast_descrs: bool,
- peephole_optim: bool,
- timeout: Time.time option,
- tac_timeout: Time.time option,
- max_threads: int,
- show_skolems: bool,
- show_datatypes: bool,
- show_consts: bool,
- evals: term list,
- formats: (term option * int list) list,
- max_potential: int,
- max_genuine: int,
- check_potential: bool,
- check_genuine: bool,
- batch_size: int,
- expect: string}
+ type params =
+ {cards_assigns: (typ option * int list) list,
+ maxes_assigns: (styp option * int list) list,
+ iters_assigns: (styp option * int list) list,
+ bitss: int list,
+ bisim_depths: int list,
+ boxes: (typ option * bool option) list,
+ finitizes: (typ option * bool option) list,
+ monos: (typ option * bool option) list,
+ stds: (typ option * bool) list,
+ wfs: (styp option * bool option) list,
+ sat_solver: string,
+ blocking: bool,
+ falsify: bool,
+ debug: bool,
+ verbose: bool,
+ overlord: bool,
+ user_axioms: bool option,
+ assms: bool,
+ merge_type_vars: bool,
+ binary_ints: bool option,
+ destroy_constrs: bool,
+ specialize: bool,
+ star_linear_preds: bool,
+ fast_descrs: bool,
+ peephole_optim: bool,
+ timeout: Time.time option,
+ tac_timeout: Time.time option,
+ max_threads: int,
+ show_datatypes: bool,
+ show_consts: bool,
+ evals: term list,
+ formats: (term option * int list) list,
+ max_potential: int,
+ max_genuine: int,
+ check_potential: bool,
+ check_genuine: bool,
+ batch_size: int,
+ expect: string}
val register_frac_type : string -> (string * string) list -> theory -> theory
val unregister_frac_type : string -> theory -> theory
@@ -80,55 +79,54 @@
structure KK = Kodkod
-type params = {
- cards_assigns: (typ option * int list) list,
- maxes_assigns: (styp option * int list) list,
- iters_assigns: (styp option * int list) list,
- bitss: int list,
- bisim_depths: int list,
- boxes: (typ option * bool option) list,
- finitizes: (typ option * bool option) list,
- monos: (typ option * bool option) list,
- stds: (typ option * bool) list,
- wfs: (styp option * bool option) list,
- sat_solver: string,
- blocking: bool,
- falsify: bool,
- debug: bool,
- verbose: bool,
- overlord: bool,
- user_axioms: bool option,
- assms: bool,
- merge_type_vars: bool,
- binary_ints: bool option,
- destroy_constrs: bool,
- specialize: bool,
- star_linear_preds: bool,
- fast_descrs: bool,
- peephole_optim: bool,
- timeout: Time.time option,
- tac_timeout: Time.time option,
- max_threads: int,
- show_skolems: bool,
- show_datatypes: bool,
- show_consts: bool,
- evals: term list,
- formats: (term option * int list) list,
- max_potential: int,
- max_genuine: int,
- check_potential: bool,
- check_genuine: bool,
- batch_size: int,
- expect: string}
+type params =
+ {cards_assigns: (typ option * int list) list,
+ maxes_assigns: (styp option * int list) list,
+ iters_assigns: (styp option * int list) list,
+ bitss: int list,
+ bisim_depths: int list,
+ boxes: (typ option * bool option) list,
+ finitizes: (typ option * bool option) list,
+ monos: (typ option * bool option) list,
+ stds: (typ option * bool) list,
+ wfs: (styp option * bool option) list,
+ sat_solver: string,
+ blocking: bool,
+ falsify: bool,
+ debug: bool,
+ verbose: bool,
+ overlord: bool,
+ user_axioms: bool option,
+ assms: bool,
+ merge_type_vars: bool,
+ binary_ints: bool option,
+ destroy_constrs: bool,
+ specialize: bool,
+ star_linear_preds: bool,
+ fast_descrs: bool,
+ peephole_optim: bool,
+ timeout: Time.time option,
+ tac_timeout: Time.time option,
+ max_threads: int,
+ show_datatypes: bool,
+ show_consts: bool,
+ evals: term list,
+ formats: (term option * int list) list,
+ max_potential: int,
+ max_genuine: int,
+ check_potential: bool,
+ check_genuine: bool,
+ batch_size: int,
+ expect: string}
-type problem_extension = {
- free_names: nut list,
- sel_names: nut list,
- nonsel_names: nut list,
- rel_table: nut NameTable.table,
- unsound: bool,
- scope: scope}
-
+type problem_extension =
+ {free_names: nut list,
+ sel_names: nut list,
+ nonsel_names: nut list,
+ rel_table: nut NameTable.table,
+ unsound: bool,
+ scope: scope}
+
type rich_problem = KK.problem * problem_extension
fun pretties_for_formulas _ _ [] = []
@@ -191,10 +189,9 @@
boxes, finitizes, monos, stds, wfs, sat_solver, falsify, debug,
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
destroy_constrs, specialize, star_linear_preds, fast_descrs,
- peephole_optim, tac_timeout, max_threads, show_skolems, show_datatypes,
- show_consts, evals, formats, max_potential, max_genuine,
- check_potential, check_genuine, batch_size, ...} =
- params
+ peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
+ evals, formats, max_potential, max_genuine, check_potential,
+ check_genuine, batch_size, ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
if auto then
@@ -580,8 +577,7 @@
: problem_extension) =
let
val (reconstructed_model, codatatypes_ok) =
- reconstruct_hol_model {show_skolems = show_skolems,
- show_datatypes = show_datatypes,
+ reconstruct_hol_model {show_datatypes = show_datatypes,
show_consts = show_consts}
scope formats frees free_names sel_names nonsel_names rel_table
bounds
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Apr 25 00:25:44 2010 +0200
@@ -13,37 +13,37 @@
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list
- type hol_context = {
- thy: theory,
- ctxt: Proof.context,
- max_bisim_depth: int,
- boxes: (typ option * bool option) list,
- stds: (typ option * bool) list,
- wfs: (styp option * bool option) list,
- user_axioms: bool option,
- debug: bool,
- binary_ints: bool option,
- destroy_constrs: bool,
- specialize: bool,
- star_linear_preds: bool,
- fast_descrs: bool,
- tac_timeout: Time.time option,
- evals: term list,
- case_names: (string * int) list,
- def_table: const_table,
- nondef_table: const_table,
- user_nondefs: term list,
- simp_table: const_table Unsynchronized.ref,
- psimp_table: const_table,
- choice_spec_table: const_table,
- intro_table: const_table,
- ground_thm_table: term list Inttab.table,
- ersatz_table: (string * string) list,
- skolems: (string * string list) list Unsynchronized.ref,
- special_funs: special_fun list Unsynchronized.ref,
- unrolled_preds: unrolled list Unsynchronized.ref,
- wf_cache: wf_cache Unsynchronized.ref,
- constr_cache: (typ * styp list) list Unsynchronized.ref}
+ type hol_context =
+ {thy: theory,
+ ctxt: Proof.context,
+ max_bisim_depth: int,
+ boxes: (typ option * bool option) list,
+ stds: (typ option * bool) list,
+ wfs: (styp option * bool option) list,
+ user_axioms: bool option,
+ debug: bool,
+ binary_ints: bool option,
+ destroy_constrs: bool,
+ specialize: bool,
+ star_linear_preds: bool,
+ fast_descrs: bool,
+ tac_timeout: Time.time option,
+ evals: term list,
+ case_names: (string * int) list,
+ def_table: const_table,
+ nondef_table: const_table,
+ user_nondefs: term list,
+ simp_table: const_table Unsynchronized.ref,
+ psimp_table: const_table,
+ choice_spec_table: const_table,
+ intro_table: const_table,
+ ground_thm_table: term list Inttab.table,
+ ersatz_table: (string * string) list,
+ skolems: (string * string list) list Unsynchronized.ref,
+ special_funs: special_fun list Unsynchronized.ref,
+ unrolled_preds: unrolled list Unsynchronized.ref,
+ wf_cache: wf_cache Unsynchronized.ref,
+ constr_cache: (typ * styp list) list Unsynchronized.ref}
datatype fixpoint_kind = Lfp | Gfp | NoFp
datatype boxability =
@@ -222,37 +222,37 @@
type unrolled = styp * styp
type wf_cache = (styp * (bool * bool)) list
-type hol_context = {
- thy: theory,
- ctxt: Proof.context,
- max_bisim_depth: int,
- boxes: (typ option * bool option) list,
- stds: (typ option * bool) list,
- wfs: (styp option * bool option) list,
- user_axioms: bool option,
- debug: bool,
- binary_ints: bool option,
- destroy_constrs: bool,
- specialize: bool,
- star_linear_preds: bool,
- fast_descrs: bool,
- tac_timeout: Time.time option,
- evals: term list,
- case_names: (string * int) list,
- def_table: const_table,
- nondef_table: const_table,
- user_nondefs: term list,
- simp_table: const_table Unsynchronized.ref,
- psimp_table: const_table,
- choice_spec_table: const_table,
- intro_table: const_table,
- ground_thm_table: term list Inttab.table,
- ersatz_table: (string * string) list,
- skolems: (string * string list) list Unsynchronized.ref,
- special_funs: special_fun list Unsynchronized.ref,
- unrolled_preds: unrolled list Unsynchronized.ref,
- wf_cache: wf_cache Unsynchronized.ref,
- constr_cache: (typ * styp list) list Unsynchronized.ref}
+type hol_context =
+ {thy: theory,
+ ctxt: Proof.context,
+ max_bisim_depth: int,
+ boxes: (typ option * bool option) list,
+ stds: (typ option * bool) list,
+ wfs: (styp option * bool option) list,
+ user_axioms: bool option,
+ debug: bool,
+ binary_ints: bool option,
+ destroy_constrs: bool,
+ specialize: bool,
+ star_linear_preds: bool,
+ fast_descrs: bool,
+ tac_timeout: Time.time option,
+ evals: term list,
+ case_names: (string * int) list,
+ def_table: const_table,
+ nondef_table: const_table,
+ user_nondefs: term list,
+ simp_table: const_table Unsynchronized.ref,
+ psimp_table: const_table,
+ choice_spec_table: const_table,
+ intro_table: const_table,
+ ground_thm_table: term list Inttab.table,
+ ersatz_table: (string * string) list,
+ skolems: (string * string list) list Unsynchronized.ref,
+ special_funs: special_fun list Unsynchronized.ref,
+ unrolled_preds: unrolled list Unsynchronized.ref,
+ wf_cache: wf_cache Unsynchronized.ref,
+ constr_cache: (typ * styp list) list Unsynchronized.ref}
datatype fixpoint_kind = Lfp | Gfp | NoFp
datatype boxability =
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Apr 25 00:25:44 2010 +0200
@@ -65,7 +65,6 @@
("verbose", "false"),
("overlord", "false"),
("show_all", "false"),
- ("show_skolems", "true"),
("show_datatypes", "false"),
("show_consts", "false"),
("format", "1"),
@@ -95,7 +94,6 @@
("quiet", "verbose"),
("no_overlord", "overlord"),
("dont_show_all", "show_all"),
- ("hide_skolems", "show_skolems"),
("hide_datatypes", "show_datatypes"),
("hide_consts", "show_consts"),
("trust_potential", "check_potential"),
@@ -255,7 +253,6 @@
val tac_timeout = lookup_time "tac_timeout"
val max_threads = Int.max (0, lookup_int "max_threads")
val show_all = debug orelse lookup_bool "show_all"
- val show_skolems = show_all orelse lookup_bool "show_skolems"
val show_datatypes = show_all orelse lookup_bool "show_datatypes"
val show_consts = show_all orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
@@ -265,9 +262,10 @@
val max_genuine = Int.max (0, lookup_int "max_genuine")
val check_potential = lookup_bool "check_potential"
val check_genuine = lookup_bool "check_genuine"
- val batch_size = case lookup_int_option "batch_size" of
- SOME n => Int.max (1, n)
- | NONE => if debug then 1 else 64
+ val batch_size =
+ case lookup_int_option "batch_size" of
+ SOME n => Int.max (1, n)
+ | NONE => if debug then 1 else 64
val expect = lookup_string "expect"
in
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
@@ -281,11 +279,10 @@
star_linear_preds = star_linear_preds, fast_descrs = fast_descrs,
peephole_optim = peephole_optim, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
- show_skolems = show_skolems, show_datatypes = show_datatypes,
- show_consts = show_consts, formats = formats, evals = evals,
- max_potential = max_potential, max_genuine = max_genuine,
- check_potential = check_potential, check_genuine = check_genuine,
- batch_size = batch_size, expect = expect}
+ show_datatypes = show_datatypes, show_consts = show_consts,
+ formats = formats, evals = evals, max_potential = max_potential,
+ max_genuine = max_genuine, check_potential = check_potential,
+ check_genuine = check_genuine, batch_size = batch_size, expect = expect}
end
fun default_params thy =
@@ -382,7 +379,7 @@
val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
val _ = OuterSyntax.improper_command "nitpick"
- "try to find a counterexample for a given subgoal using Kodkod"
+ "try to find a counterexample for a given subgoal using Nitpick"
K.diag parse_nitpick_command
val _ = OuterSyntax.command "nitpick_params"
"set and display the default parameters for Nitpick"
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Apr 25 00:25:44 2010 +0200
@@ -12,10 +12,10 @@
type rep = Nitpick_Rep.rep
type nut = Nitpick_Nut.nut
- type params = {
- show_skolems: bool,
- show_datatypes: bool,
- show_consts: bool}
+ type params =
+ {show_datatypes: bool,
+ show_consts: bool}
+
type term_postprocessor =
Proof.context -> string -> (typ -> term list) -> typ -> term -> term
@@ -51,10 +51,9 @@
structure KK = Kodkod
-type params = {
- show_skolems: bool,
- show_datatypes: bool,
- show_consts: bool}
+type params =
+ {show_datatypes: bool,
+ show_consts: bool}
type term_postprocessor =
Proof.context -> string -> (typ -> term list) -> typ -> term -> term
@@ -840,7 +839,7 @@
t1 = t2
end
-fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
+fun reconstruct_hol_model {show_datatypes, show_consts}
({hol_ctxt = {thy, ctxt, max_bisim_depth, boxes, stds, wfs, user_axioms,
debug, binary_ints, destroy_constrs, specialize,
star_linear_preds, fast_descrs, tac_timeout, evals,
@@ -980,7 +979,7 @@
| _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
[Const x])) all_frees
val chunks = block_of_names true "Free variable" free_names @
- block_of_names show_skolems "Skolem constant" skolem_names @
+ block_of_names true "Skolem constant" skolem_names @
block_of_names true "Evaluated term" eval_names @
block_of_datatypes @ block_of_codatatypes @
block_of_names show_consts "Constant"
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Sun Apr 25 00:25:44 2010 +0200
@@ -14,11 +14,11 @@
type decl = Kodkod.decl
type expr_assign = Kodkod.expr_assign
- type name_pool = {
- rels: n_ary_index list,
- vars: n_ary_index list,
- formula_reg: int,
- rel_reg: int}
+ type name_pool =
+ {rels: n_ary_index list,
+ vars: n_ary_index list,
+ formula_reg: int,
+ rel_reg: int}
val initial_pool : name_pool
val not3_rel : n_ary_index
@@ -51,39 +51,38 @@
val num_seq : int -> int -> int_expr list
val s_and : formula -> formula -> formula
- type kodkod_constrs = {
- kk_all: decl list -> formula -> formula,
- kk_exist: decl list -> formula -> formula,
- kk_formula_let: expr_assign list -> formula -> formula,
- kk_formula_if: formula -> formula -> formula -> formula,
- kk_or: formula -> formula -> formula,
- kk_not: formula -> formula,
- kk_iff: formula -> formula -> formula,
- kk_implies: formula -> formula -> formula,
- kk_and: formula -> formula -> formula,
- kk_subset: rel_expr -> rel_expr -> formula,
- kk_rel_eq: rel_expr -> rel_expr -> formula,
- kk_no: rel_expr -> formula,
- kk_lone: rel_expr -> formula,
- kk_one: rel_expr -> formula,
- kk_some: rel_expr -> formula,
- kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
- kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
- kk_union: rel_expr -> rel_expr -> rel_expr,
- kk_difference: rel_expr -> rel_expr -> rel_expr,
- kk_override: rel_expr -> rel_expr -> rel_expr,
- kk_intersect: rel_expr -> rel_expr -> rel_expr,
- kk_product: rel_expr -> rel_expr -> rel_expr,
- kk_join: rel_expr -> rel_expr -> rel_expr,
- kk_closure: rel_expr -> rel_expr,
- kk_reflexive_closure: rel_expr -> rel_expr,
- kk_comprehension: decl list -> formula -> rel_expr,
- kk_project: rel_expr -> int_expr list -> rel_expr,
- kk_project_seq: rel_expr -> int -> int -> rel_expr,
- kk_not3: rel_expr -> rel_expr,
- kk_nat_less: rel_expr -> rel_expr -> rel_expr,
- kk_int_less: rel_expr -> rel_expr -> rel_expr
- }
+ type kodkod_constrs =
+ {kk_all: decl list -> formula -> formula,
+ kk_exist: decl list -> formula -> formula,
+ kk_formula_let: expr_assign list -> formula -> formula,
+ kk_formula_if: formula -> formula -> formula -> formula,
+ kk_or: formula -> formula -> formula,
+ kk_not: formula -> formula,
+ kk_iff: formula -> formula -> formula,
+ kk_implies: formula -> formula -> formula,
+ kk_and: formula -> formula -> formula,
+ kk_subset: rel_expr -> rel_expr -> formula,
+ kk_rel_eq: rel_expr -> rel_expr -> formula,
+ kk_no: rel_expr -> formula,
+ kk_lone: rel_expr -> formula,
+ kk_one: rel_expr -> formula,
+ kk_some: rel_expr -> formula,
+ kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
+ kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
+ kk_union: rel_expr -> rel_expr -> rel_expr,
+ kk_difference: rel_expr -> rel_expr -> rel_expr,
+ kk_override: rel_expr -> rel_expr -> rel_expr,
+ kk_intersect: rel_expr -> rel_expr -> rel_expr,
+ kk_product: rel_expr -> rel_expr -> rel_expr,
+ kk_join: rel_expr -> rel_expr -> rel_expr,
+ kk_closure: rel_expr -> rel_expr,
+ kk_reflexive_closure: rel_expr -> rel_expr,
+ kk_comprehension: decl list -> formula -> rel_expr,
+ kk_project: rel_expr -> int_expr list -> rel_expr,
+ kk_project_seq: rel_expr -> int -> int -> rel_expr,
+ kk_not3: rel_expr -> rel_expr,
+ kk_nat_less: rel_expr -> rel_expr -> rel_expr,
+ kk_int_less: rel_expr -> rel_expr -> rel_expr}
val kodkod_constrs : bool -> int -> int -> int -> kodkod_constrs
end;
@@ -94,11 +93,11 @@
open Kodkod
open Nitpick_Util
-type name_pool = {
- rels: n_ary_index list,
- vars: n_ary_index list,
- formula_reg: int,
- rel_reg: int}
+type name_pool =
+ {rels: n_ary_index list,
+ vars: n_ary_index list,
+ formula_reg: int,
+ rel_reg: int}
(* If you add new built-in relations, make sure to increment the counters here
as well to avoid name clashes (which fortunately would be detected by
@@ -204,39 +203,38 @@
| s_and _ False = False
| s_and f1 f2 = And (f1, f2)
-type kodkod_constrs = {
- kk_all: decl list -> formula -> formula,
- kk_exist: decl list -> formula -> formula,
- kk_formula_let: expr_assign list -> formula -> formula,
- kk_formula_if: formula -> formula -> formula -> formula,
- kk_or: formula -> formula -> formula,
- kk_not: formula -> formula,
- kk_iff: formula -> formula -> formula,
- kk_implies: formula -> formula -> formula,
- kk_and: formula -> formula -> formula,
- kk_subset: rel_expr -> rel_expr -> formula,
- kk_rel_eq: rel_expr -> rel_expr -> formula,
- kk_no: rel_expr -> formula,
- kk_lone: rel_expr -> formula,
- kk_one: rel_expr -> formula,
- kk_some: rel_expr -> formula,
- kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
- kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
- kk_union: rel_expr -> rel_expr -> rel_expr,
- kk_difference: rel_expr -> rel_expr -> rel_expr,
- kk_override: rel_expr -> rel_expr -> rel_expr,
- kk_intersect: rel_expr -> rel_expr -> rel_expr,
- kk_product: rel_expr -> rel_expr -> rel_expr,
- kk_join: rel_expr -> rel_expr -> rel_expr,
- kk_closure: rel_expr -> rel_expr,
- kk_reflexive_closure: rel_expr -> rel_expr,
- kk_comprehension: decl list -> formula -> rel_expr,
- kk_project: rel_expr -> int_expr list -> rel_expr,
- kk_project_seq: rel_expr -> int -> int -> rel_expr,
- kk_not3: rel_expr -> rel_expr,
- kk_nat_less: rel_expr -> rel_expr -> rel_expr,
- kk_int_less: rel_expr -> rel_expr -> rel_expr
-}
+type kodkod_constrs =
+ {kk_all: decl list -> formula -> formula,
+ kk_exist: decl list -> formula -> formula,
+ kk_formula_let: expr_assign list -> formula -> formula,
+ kk_formula_if: formula -> formula -> formula -> formula,
+ kk_or: formula -> formula -> formula,
+ kk_not: formula -> formula,
+ kk_iff: formula -> formula -> formula,
+ kk_implies: formula -> formula -> formula,
+ kk_and: formula -> formula -> formula,
+ kk_subset: rel_expr -> rel_expr -> formula,
+ kk_rel_eq: rel_expr -> rel_expr -> formula,
+ kk_no: rel_expr -> formula,
+ kk_lone: rel_expr -> formula,
+ kk_one: rel_expr -> formula,
+ kk_some: rel_expr -> formula,
+ kk_rel_let: expr_assign list -> rel_expr -> rel_expr,
+ kk_rel_if: formula -> rel_expr -> rel_expr -> rel_expr,
+ kk_union: rel_expr -> rel_expr -> rel_expr,
+ kk_difference: rel_expr -> rel_expr -> rel_expr,
+ kk_override: rel_expr -> rel_expr -> rel_expr,
+ kk_intersect: rel_expr -> rel_expr -> rel_expr,
+ kk_product: rel_expr -> rel_expr -> rel_expr,
+ kk_join: rel_expr -> rel_expr -> rel_expr,
+ kk_closure: rel_expr -> rel_expr,
+ kk_reflexive_closure: rel_expr -> rel_expr,
+ kk_comprehension: decl list -> formula -> rel_expr,
+ kk_project: rel_expr -> int_expr list -> rel_expr,
+ kk_project_seq: rel_expr -> int -> int -> rel_expr,
+ kk_not3: rel_expr -> rel_expr,
+ kk_nat_less: rel_expr -> rel_expr -> rel_expr,
+ kk_int_less: rel_expr -> rel_expr -> rel_expr}
(* We assume throughout that Kodkod variables have a "one" constraint. This is
always the case if Kodkod's skolemization is disabled. *)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Apr 25 00:10:30 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sun Apr 25 00:25:44 2010 +0200
@@ -10,32 +10,32 @@
type styp = Nitpick_Util.styp
type hol_context = Nitpick_HOL.hol_context
- type constr_spec = {
- const: styp,
- delta: int,
- epsilon: int,
- exclusive: bool,
- explicit_max: int,
- total: bool}
+ type constr_spec =
+ {const: styp,
+ delta: int,
+ epsilon: int,
+ exclusive: bool,
+ explicit_max: int,
+ total: bool}
- type dtype_spec = {
- typ: typ,
- card: int,
- co: bool,
- standard: bool,
- complete: bool * bool,
- concrete: bool * bool,
- deep: bool,
- constrs: constr_spec list}
+ type dtype_spec =
+ {typ: typ,
+ card: int,
+ co: bool,
+ standard: bool,
+ complete: bool * bool,
+ concrete: bool * bool,
+ deep: bool,
+ constrs: constr_spec list}
- type scope = {
- hol_ctxt: hol_context,
- binarize: bool,
- card_assigns: (typ * int) list,
- bits: int,
- bisim_depth: int,
- datatypes: dtype_spec list,
- ofs: int Typtab.table}
+ type scope =
+ {hol_ctxt: hol_context,
+ binarize: bool,
+ card_assigns: (typ * int) list,
+ bits: int,
+ bisim_depth: int,
+ datatypes: dtype_spec list,
+ ofs: int Typtab.table}
val datatype_spec : dtype_spec list -> typ -> dtype_spec option
val constr_spec : dtype_spec list -> styp -> constr_spec
@@ -61,32 +61,32 @@
open Nitpick_Util
open Nitpick_HOL
-type constr_spec = {
- const: styp,
- delta: int,
- epsilon: int,
- exclusive: bool,
- explicit_max: int,
- total: bool}
+type constr_spec =
+ {const: styp,
+ delta: int,
+ epsilon: int,
+ exclusive: bool,
+ explicit_max: int,
+ total: bool}
-type dtype_spec = {
- typ: typ,
- card: int,
- co: bool,
- standard: bool,
- complete: bool * bool,
- concrete: bool * bool,
- deep: bool,
- constrs: constr_spec list}
+type dtype_spec =
+ {typ: typ,
+ card: int,
+ co: bool,
+ standard: bool,
+ complete: bool * bool,
+ concrete: bool * bool,
+ deep: bool,
+ constrs: constr_spec list}
-type scope = {
- hol_ctxt: hol_context,
- binarize: bool,
- card_assigns: (typ * int) list,
- bits: int,
- bisim_depth: int,
- datatypes: dtype_spec list,
- ofs: int Typtab.table}
+type scope =
+ {hol_ctxt: hol_context,
+ binarize: bool,
+ card_assigns: (typ * int) list,
+ bits: int,
+ bisim_depth: int,
+ datatypes: dtype_spec list,
+ ofs: int Typtab.table}
datatype row_kind = Card of typ | Max of styp