--- a/doc-src/Nitpick/nitpick.tex Mon Nov 23 15:30:32 2009 -0800
+++ b/doc-src/Nitpick/nitpick.tex Thu Dec 17 15:22:27 2009 +0100
@@ -436,12 +436,10 @@
\label{natural-numbers-and-integers}
Because of the axiom of infinity, the type \textit{nat} does not admit any
-finite models. To deal with this, Nitpick considers prefixes $\{0,\, 1,\,
-\ldots,\, K - 1\}$ of \textit{nat} (where $K = \textit{card}~\textit{nat}$) and
-maps all other numbers to the undefined value ($\unk$). The type \textit{int} is
-handled in a similar way: If $K = \textit{card}~\textit{int}$, the subset of
-\textit{int} known to Nitpick is $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor
-K/2 \rfloor\}$. Undefined values lead to a three-valued logic.
+finite models. To deal with this, Nitpick's approach is to consider finite
+subsets $N$ of \textit{nat} and maps all numbers $\notin N$ to the undefined
+value (displayed as `$\unk$'). The type \textit{int} is handled similarly.
+Internally, undefined values lead to a three-valued logic.
Here is an example involving \textit{int}:
@@ -456,15 +454,26 @@
\hbox{}\qquad\qquad $n = 0$
\postw
+Internally, Nitpick uses either a unary or a binary representation of numbers.
+The unary representation is more efficient but only suitable for numbers very
+close to zero. By default, Nitpick attempts to choose the more appropriate
+encoding by inspecting the formula at hand. This behavior can be overridden by
+passing either \textit{unary\_ints} or \textit{binary\_ints} as option. For
+binary notation, the number of bits to use can be specified using
+the \textit{bits} option. For example:
+
+\prew
+\textbf{nitpick} [\textit{binary\_ints}, \textit{bits}${} = 16$]
+\postw
+
With infinite types, we don't always have the luxury of a genuine counterexample
and must often content ourselves with a potential one. The tedious task of
finding out whether the potential counterexample is in fact genuine can be
-outsourced to \textit{auto} by passing the option \textit{check\_potential}. For
-example:
+outsourced to \textit{auto} by passing \textit{check\_potential}. For example:
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
-\textbf{nitpick} [\textit{card~nat}~= 100,\, \textit{check\_potential}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
@@ -482,7 +491,7 @@
Incidentally, if you distrust the so-called genuine counterexamples, you can
enable \textit{check\_\allowbreak genuine} to verify them as well. However, be
-aware that \textit{auto} will often fail to prove that the counterexample is
+aware that \textit{auto} will usually fail to prove that the counterexample is
genuine or spurious.
Some conjectures involving elementary number theory make Nitpick look like a
@@ -495,10 +504,11 @@
Nitpick found no counterexample.
\postw
-For any cardinality $k$, \textit{Suc} is the partial function $\{0 \mapsto 1,\,
-1 \mapsto 2,\, \ldots,\, k - 1 \mapsto \unk\}$, which evaluates to $\unk$ when
-it is passed as argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$.
-The next example is similar:
+On any finite set $N$, \textit{Suc} is a partial function; for example, if $N =
+\{0, 1, \ldots, k\}$, then \textit{Suc} is $\{0 \mapsto 1,\, 1 \mapsto 2,\,
+\ldots,\, k \mapsto \unk\}$, which evaluates to $\unk$ when passed as
+argument to $P$. As a result, $P~\textit{Suc}$ is always $\unk$. The next
+example is similar:
\prew
\textbf{lemma} ``$P~(\textit{op}~{+}\Colon
@@ -822,7 +832,7 @@
\prew
\textbf{lemma} ``$\textit{even}'~(n - 2) \,\Longrightarrow\, \textit{even}'~n$'' \\
-\textbf{nitpick} [\textit{card nat} = 10,\, \textit{show\_consts}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{card nat} = 10, \textit{show\_consts}] \\[2\smallskipamount]
\slshape Nitpick found a counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $n = 1$ \\
@@ -989,7 +999,7 @@
\prew
\textbf{lemma} ``$\lbrakk xs = \textit{LCons}~a~\textit{xs};\>\, \textit{ys} = \textit{LCons}~a~\textit{ys}\rbrakk
\,\Longrightarrow\, \textit{xs} = \textit{ys}$'' \\
-\textbf{nitpick} [\textit{bisim\_depth} = $-1$,\, \textit{show\_datatypes}] \\[2\smallskipamount]
+\textbf{nitpick} [\textit{bisim\_depth} = $-1$, \textit{show\_datatypes}] \\[2\smallskipamount]
\slshape Nitpick found a likely genuine counterexample for $\textit{card}~'a$ = 2: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $a = a_2$ \\
@@ -1687,23 +1697,7 @@
\begin{enum}
\opu{card}{type}{int\_seq}
-Specifies the sequence of cardinalities to use for a given type. For
-\textit{nat} and \textit{int}, the cardinality fully specifies the subset used
-to approximate the type. For example:
-%
-$$\hbox{\begin{tabular}{@{}rll@{}}%
-\textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
-\textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
-\textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
-\end{tabular}}$$
-%
-In general:
-%
-$$\hbox{\begin{tabular}{@{}rll@{}}%
-\textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
-\textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
-\end{tabular}}$$
-%
+Specifies the sequence of cardinalities to use for a given type.
For free types, and often also for \textbf{typedecl}'d types, it usually makes
sense to specify cardinalities as a range of the form \textit{$1$--$n$}.
Although function and product types are normally mapped directly to the
@@ -1731,6 +1725,44 @@
(co)in\-duc\-tive datatype constructors. This can be overridden on a per-constructor
basis using the \textit{max}~\qty{const} option described above.
+\opsmart{binary\_ints}{unary\_ints}
+Specifies whether natural numbers and integers should be encoded using a unary
+or binary notation. In unary mode, the cardinality fully specifies the subset
+used to approximate the type. For example:
+%
+$$\hbox{\begin{tabular}{@{}rll@{}}%
+\textit{card nat} = 4 & induces & $\{0,\, 1,\, 2,\, 3\}$ \\
+\textit{card int} = 4 & induces & $\{-1,\, 0,\, +1,\, +2\}$ \\
+\textit{card int} = 5 & induces & $\{-2,\, -1,\, 0,\, +1,\, +2\}.$%
+\end{tabular}}$$
+%
+In general:
+%
+$$\hbox{\begin{tabular}{@{}rll@{}}%
+\textit{card nat} = $K$ & induces & $\{0,\, \ldots,\, K - 1\}$ \\
+\textit{card int} = $K$ & induces & $\{-\lceil K/2 \rceil + 1,\, \ldots,\, +\lfloor K/2 \rfloor\}.$%
+\end{tabular}}$$
+%
+In binary mode, the cardinality specifies the number of distinct values that can
+be constructed. Each of these value is represented by a bit pattern whose length
+is specified by the \textit{bits} (\S\ref{scope-of-search}) option. By default,
+Nitpick attempts to choose the more appropriate encoding by inspecting the
+formula at hand, preferring the binary notation for problems involving
+multiplicative operators or large constants.
+
+\textbf{Warning:} For technical reasons, Nitpick always reverts to unary for
+problems that refer to the types \textit{rat} or \textit{real} or the constants
+\textit{gcd} or \textit{lcm}.
+
+{\small See also \textit{bits} (\S\ref{scope-of-search}) and
+\textit{show\_datatypes} (\S\ref{output-format}).}
+
+\opt{bits}{int\_seq}{$\mathbf{1},\mathbf{2},\mathbf{3},\mathbf{4},\mathbf{6},\mathbf{8},\mathbf{10},\mathbf{12}$}
+Specifies the number of bits to use to represent natural numbers and integers in
+binary, excluding the sign bit. The minimum is 1 and the maximum is 31.
+
+{\small See also \textit{binary\_ints} (\S\ref{scope-of-search}).}
+
\opusmart{wf}{const}{non\_wf}
Specifies whether the specified (co)in\-duc\-tively defined predicate is
well-founded. The option can take the following values:
--- a/src/HOL/Nitpick.thy Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Nitpick.thy Thu Dec 17 15:22:27 2009 +0100
@@ -36,7 +36,12 @@
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) pair_box = PairBox 'a 'b
-datatype ('a, 'b) fun_box = FunBox "'a \<Rightarrow> 'b"
+datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
+
+typedecl unsigned_bit
+typedecl signed_bit
+
+datatype 'a word = Word "('a set)"
text {*
Alternative definitions.
@@ -126,8 +131,6 @@
declare nat.cases [nitpick_simp del]
-lemmas [nitpick_def] = dvd_eq_mod_eq_0 [THEN eq_reflection]
-
lemma list_size_simp [nitpick_simp]:
"list_size f xs = (if xs = [] then 0
else Suc (f (hd xs) + list_size f (tl xs)))"
@@ -244,11 +247,11 @@
setup {* Nitpick_Isar.setup *}
hide (open) const unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Tha refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
- fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
- one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
- number_of_frac inverse_frac less_eq_frac of_frac
-hide (open) type bisim_iterator pair_box fun_box
+ bisim_iterator_max Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
+ wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
+ Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
+ times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
+hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Dec 17 15:22:27 2009 +0100
@@ -18,16 +18,16 @@
val def_table = Nitpick_HOL.const_def_table @{context} defs
val ext_ctxt : Nitpick_HOL.extended_context =
{thy = @{theory}, ctxt = @{context}, max_bisim_depth = ~1, boxes = [],
- user_axioms = NONE, debug = false, wfs = [], destroy_constrs = false,
- specialize = false, skolemize = false, star_linear_preds = false,
- uncurry = false, fast_descrs = false, tac_timeout = NONE, evals = [],
- case_names = [], def_table = def_table, nondef_table = Symtab.empty,
- user_nondefs = [], simp_table = Unsynchronized.ref Symtab.empty,
- psimp_table = Symtab.empty, intro_table = Symtab.empty,
- ground_thm_table = Inttab.empty, ersatz_table = [],
- skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
- unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
- constr_cache = Unsynchronized.ref []}
+ user_axioms = NONE, debug = false, wfs = [], binary_ints = SOME false,
+ destroy_constrs = false, specialize = false, skolemize = false,
+ star_linear_preds = false, uncurry = false, fast_descrs = false,
+ tac_timeout = NONE, evals = [], case_names = [], def_table = def_table,
+ nondef_table = Symtab.empty, user_nondefs = [],
+ simp_table = Unsynchronized.ref Symtab.empty, psimp_table = Symtab.empty,
+ intro_table = Symtab.empty, ground_thm_table = Inttab.empty,
+ ersatz_table = [], skolems = Unsynchronized.ref [],
+ special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
+ wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
(* term -> bool *)
val is_mono = Nitpick_Mono.formulas_monotonic ext_ctxt @{typ 'a} [] []
fun is_const t =
--- a/src/HOL/Nitpick_Examples/Special_Nits.thy Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Nitpick_Examples/Special_Nits.thy Thu Dec 17 15:22:27 2009 +0100
@@ -135,7 +135,7 @@
lemma "\<forall>a. g a = a
\<Longrightarrow> \<exists>b\<^isub>1 b\<^isub>2 b\<^isub>3 b\<^isub>4 b\<^isub>5 b\<^isub>6 b\<^isub>7 b\<^isub>8 b\<^isub>9 b\<^isub>10 (b\<^isub>11\<Colon>nat).
b\<^isub>1 < b\<^isub>11 \<and> f5 g x = f5 (\<lambda>a. if b\<^isub>1 < b\<^isub>11 then a else h b\<^isub>2) x"
-nitpick [expect = potential]
+nitpick [expect = none]
nitpick [dont_specialize, expect = none]
nitpick [dont_box, expect = none]
nitpick [dont_box, dont_specialize, expect = none]
@@ -163,7 +163,7 @@
else
h b\<^isub>2 + h b\<^isub>3 + h b\<^isub>4 + h b\<^isub>5 + h b\<^isub>6 + h b\<^isub>7 + h b\<^isub>8
+ h b\<^isub>9 + h b\<^isub>10) x"
-nitpick [card nat = 2, card 'a = 1, expect = none]
+nitpick [card nat = 2, card 'a = 1, expect = potential]
nitpick [card nat = 2, card 'a = 1, dont_box, expect = potential]
nitpick [card nat = 2, card 'a = 1, dont_specialize, expect = potential]
nitpick [card nat = 2, card 'a = 1, dont_box, dont_specialize,
--- a/src/HOL/Refute.thy Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Refute.thy Thu Dec 17 15:22:27 2009 +0100
@@ -61,7 +61,8 @@
(* ------------------------------------------------------------------------- *)
(* PARAMETERS *)
(* *)
-(* The following global parameters are currently supported (and required): *)
+(* The following global parameters are currently supported (and required, *)
+(* except for "expect"): *)
(* *)
(* Name Type Description *)
(* *)
@@ -75,6 +76,10 @@
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
(* This value is ignored under some ML compilers. *)
(* "satsolver" string Name of the SAT solver to be used. *)
+(* "no_assms" bool If "true", assumptions in structured proofs are *)
+(* not considered. *)
+(* "expect" string Expected result ("genuine", "potential", "none", or *)
+(* "unknown"). *)
(* *)
(* See 'HOL/SAT.thy' for default values. *)
(* *)
--- a/src/HOL/SAT.thy Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/SAT.thy Thu Dec 17 15:22:27 2009 +0100
@@ -23,7 +23,8 @@
maxsize=8,
maxvars=10000,
maxtime=60,
- satsolver="auto"]
+ satsolver="auto",
+ no_assms="false"]
ML {* structure sat = SATFunc(cnf) *}
--- a/src/HOL/Tools/Nitpick/HISTORY Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/HISTORY Thu Dec 17 15:22:27 2009 +0100
@@ -1,5 +1,6 @@
Version 2010
+ * Added and implemented "binary_ints" and "bits" options
* Fixed soundness bug in "destroy_constrs" optimization
Version 2009-1
--- a/src/HOL/Tools/Nitpick/kodkod.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Dec 17 15:22:27 2009 +0100
@@ -506,12 +506,13 @@
= filter (is_relevant_setting o fst) (#settings p2)
(* int -> string *)
-fun base_name j = if j < 0 then Int.toString (~j - 1) ^ "'" else Int.toString j
+fun base_name j =
+ if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
(* n_ary_index -> string -> string -> string -> string *)
fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
| n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
- | n_ary_name (n, j) _ _ prefix = prefix ^ Int.toString n ^ "_" ^ base_name j
+ | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j
(* int -> string *)
fun atom_name j = "A" ^ base_name j
@@ -574,7 +575,7 @@
sub ts1 prec ^ " - " ^ sub ts1 (prec + 1)
| TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts1 prec
| TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
- | TupleProject (ts, c) => sub ts prec ^ "[" ^ Int.toString c ^ "]"
+ | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
| TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
| TupleRange (t1, t2) =>
"{" ^ string_for_tuple t1 ^
@@ -602,7 +603,7 @@
(* int_bound -> string *)
fun int_string_for_bound (opt_n, tss) =
(case opt_n of
- SOME n => Int.toString n ^ ": "
+ SOME n => signed_string_of_int n ^ ": "
| NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"
val prec_All = 1
@@ -823,7 +824,7 @@
| Neg i => (out "-"; out_i i prec)
| Absolute i => (out "abs "; out_i i prec)
| Signum i => (out "sgn "; out_i i prec)
- | Num k => out (Int.toString k)
+ | Num k => out (signed_string_of_int k)
| IntReg j => out (int_reg_name j));
(if need_parens then out ")" else ())
end
@@ -996,7 +997,7 @@
(* bool -> Time.time option -> int -> int -> problem list -> outcome *)
fun solve_any_problem overlord deadline max_threads max_solutions problems =
let
- val j = find_index (equal True o #formula) problems
+ val j = find_index (curry (op =) True o #formula) problems
val indexed_problems = if j >= 0 then
[(j, nth problems j)]
else
@@ -1048,12 +1049,12 @@
\LD_LIBRARY_PATH=\"$KODKODI_JAVA_LIBRARY_PATH:\
\$LD_LIBRARY_PATH\" \
\\"$KODKODI\"/bin/kodkodi" ^
- (if ms >= 0 then " -max-msecs " ^ Int.toString ms
+ (if ms >= 0 then " -max-msecs " ^ string_of_int ms
else "") ^
(if max_solutions > 1 then " -solve-all" else "") ^
- " -max-solutions " ^ Int.toString max_solutions ^
+ " -max-solutions " ^ string_of_int max_solutions ^
(if max_threads > 0 then
- " -max-threads " ^ Int.toString max_threads
+ " -max-threads " ^ string_of_int max_threads
else
"") ^
" < " ^ Path.implode in_path ^
--- a/src/HOL/Tools/Nitpick/minipick.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/minipick.ML Thu Dec 17 15:22:27 2009 +0100
@@ -232,7 +232,7 @@
| Const (@{const_name snd}, _) => raise SAME ()
| Const (_, @{typ bool}) => atom_from_formula (to_F Ts t)
| Free (x as (_, T)) =>
- Rel (arity_of RRep card T, find_index (equal x) frees)
+ Rel (arity_of RRep card T, find_index (curry (op =) x) frees)
| Term.Var _ => raise NOT_SUPPORTED "schematic variables"
| Bound j => raise SAME ()
| Abs (_, T, t') =>
@@ -314,7 +314,8 @@
bounds = bounds, int_bounds = [], expr_assigns = [], formula = formula}
in
case solve_any_problem overlord NONE 0 1 [problem] of
- Normal ([], _) => "none"
+ NotInstalled => "unknown"
+ | Normal ([], _) => "none"
| Normal _ => "genuine"
| TimedOut _ => "unknown"
| Interrupted _ => "unknown"
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Dec 17 15:22:27 2009 +0100
@@ -12,6 +12,7 @@
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,
monos: (typ option * bool option) list,
@@ -25,6 +26,7 @@
user_axioms: bool option,
assms: bool,
merge_type_vars: bool,
+ binary_ints: bool option,
destroy_constrs: bool,
specialize: bool,
skolemize: bool,
@@ -77,6 +79,7 @@
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,
monos: (typ option * bool option) list,
@@ -90,6 +93,7 @@
user_axioms: bool option,
assms: bool,
merge_type_vars: bool,
+ binary_ints: bool option,
destroy_constrs: bool,
specialize: bool,
skolemize: bool,
@@ -133,7 +137,7 @@
[Pretty.str (s ^ plural_s_for_list ts ^ ":"),
Pretty.indent indent_size (Pretty.chunks
(map2 (fn j => fn t =>
- Pretty.block [t |> shorten_const_names_in_term
+ Pretty.block [t |> shorten_names_in_term
|> Syntax.pretty_term ctxt,
Pretty.str (if j = 1 then "." else ";")])
(length ts downto 1) ts))]
@@ -162,7 +166,7 @@
| passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
(* ('a * bool option) list -> bool *)
-fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
+fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
val syntactic_sorts =
@{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
@@ -186,20 +190,21 @@
val nitpick_thy = ThyInfo.get_theory "Nitpick"
val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy))
val thy = if nitpick_thy_missing then
- Theory.begin_theory "Nitpick_Internal" [nitpick_thy, user_thy]
+ Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY"
+ [nitpick_thy, user_thy]
|> Theory.checkpoint
else
user_thy
val ctxt = Proof.context_of state
|> nitpick_thy_missing ? Context.raw_transfer thy
- val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
- monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
- user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
- skolemize, star_linear_preds, uncurry, fast_descrs, peephole_optim,
- tac_timeout, sym_break, sharing_depth, flatten_props, max_threads,
- show_skolems, show_datatypes, show_consts, evals, formats,
- max_potential, max_genuine, check_potential, check_genuine, batch_size,
- ...} =
+ val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
+ boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
+ overlord, user_axioms, assms, merge_type_vars, binary_ints,
+ destroy_constrs, specialize, skolemize, star_linear_preds, uncurry,
+ fast_descrs, peephole_optim, tac_timeout, sym_break, sharing_depth,
+ flatten_props, max_threads, show_skolems, show_datatypes, show_consts,
+ evals, formats, max_potential, max_genuine, check_potential,
+ check_genuine, batch_size, ...} =
params
val state_ref = Unsynchronized.ref state
(* Pretty.T -> unit *)
@@ -260,10 +265,11 @@
val (ext_ctxt as {wf_cache, ...}) =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
user_axioms = user_axioms, debug = debug, wfs = wfs,
- destroy_constrs = destroy_constrs, specialize = specialize,
- skolemize = skolemize, star_linear_preds = star_linear_preds,
- uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout,
- evals = evals, case_names = case_names, def_table = def_table,
+ binary_ints = binary_ints, destroy_constrs = destroy_constrs,
+ specialize = specialize, skolemize = skolemize,
+ star_linear_preds = star_linear_preds, uncurry = uncurry,
+ fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
+ case_names = case_names, def_table = def_table,
nondef_table = nondef_table, user_nondefs = user_nondefs,
simp_table = simp_table, psimp_table = psimp_table,
intro_table = intro_table, ground_thm_table = ground_thm_table,
@@ -315,25 +321,33 @@
(core_u :: def_us @ nondef_us)
*)
- val unique_scope = forall (equal 1 o length o snd) cards_assigns
+ val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
(* typ -> bool *)
fun is_free_type_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
- | _ => formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+ | _ => is_bit_type T
+ orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
fun is_datatype_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
- | _ =>
- not (is_pure_typedef thy T) orelse is_univ_typedef thy T
- orelse is_number_type thy T
- orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
- fun is_datatype_shallow T =
- not (exists (equal T o domain_type o type_of) sel_names)
+ | _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T
+ orelse is_number_type thy T
+ orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+ fun is_datatype_deep T =
+ is_word_type T
+ orelse exists (curry (op =) T o domain_type o type_of) sel_names
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
+ val _ = if verbose andalso binary_ints = SOME true
+ andalso exists (member (op =) [nat_T, int_T]) Ts then
+ print_v (K "The option \"binary_ints\" will be ignored because \
+ \of the presence of rationals, reals, \"gcd\", or \
+ \\"lcm\" in the problem.")
+ else
+ ()
val (all_dataTs, all_free_Ts) =
List.partition (is_integer_type orf is_datatype thy) Ts
val (mono_dataTs, nonmono_dataTs) =
@@ -341,11 +355,13 @@
val (mono_free_Ts, nonmono_free_Ts) =
List.partition is_free_type_monotonic all_free_Ts
+ val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts
val _ =
- if not unique_scope andalso not (null mono_free_Ts) then
+ if not unique_scope andalso not (null interesting_mono_free_Ts) then
print_v (fn () =>
let
- val ss = map (quote o string_for_type ctxt) mono_free_Ts
+ val ss = map (quote o string_for_type ctxt)
+ interesting_mono_free_Ts
in
"The type" ^ plural_s_for_list ss ^ " " ^
space_implode " " (serial_commas "and" ss) ^ " " ^
@@ -360,7 +376,7 @@
()
val mono_Ts = mono_dataTs @ mono_free_Ts
val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
- val shallow_dataTs = filter is_datatype_shallow mono_dataTs
+ val shallow_dataTs = filter_out is_datatype_deep mono_dataTs
(*
val _ = priority "Monotonic datatypes:"
val _ = List.app (priority o string_for_type ctxt) mono_dataTs
@@ -375,8 +391,9 @@
val need_incremental = Int.max (max_potential, max_genuine) >= 2
val effective_sat_solver =
if sat_solver <> "smart" then
- if need_incremental andalso
- not (sat_solver mem Kodkod_SAT.configured_sat_solvers true) then
+ if need_incremental
+ andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
+ sat_solver) then
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
\be used instead of " ^ quote sat_solver ^ "."));
"SAT4J")
@@ -399,12 +416,12 @@
(* bool -> scope -> rich_problem option *)
fun problem_for_scope liberal
- (scope as {card_assigns, bisim_depth, datatypes, ofs, ...}) =
+ (scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
let
val _ = not (exists (fn other => scope_less_eq other scope)
(!too_big_scopes))
- orelse raise LIMIT ("Nitpick.pick_them_nits_in_term.\
- \problem_for_scope", "too big scope")
+ orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
+ \problem_for_scope", "too large scope")
(*
val _ = priority "Offsets:"
val _ = List.app (fn (T, j0) =>
@@ -412,13 +429,13 @@
string_of_int j0))
(Typtab.dest ofs)
*)
- val all_precise = forall (is_precise_type datatypes) Ts
+ val all_exact = forall (is_exact_type datatypes) Ts
(* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
- val repify_consts = choose_reps_for_consts scope all_precise
+ val repify_consts = choose_reps_for_consts scope all_exact
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
- val _ = forall (equal main_j0) [nat_j0, int_j0]
+ val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0)
orelse raise BAD ("Nitpick.pick_them_nits_in_term.\
\problem_for_scope", "bad offsets")
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
@@ -453,7 +470,7 @@
val def_us = map (rename_vars_in_nut pool rel_table) def_us
val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
(* nut -> Kodkod.formula *)
- val to_f = kodkod_formula_from_nut ofs liberal kk
+ val to_f = kodkod_formula_from_nut bits ofs liberal kk
val core_f = to_f core_u
val def_fs = map to_f def_us
val nondef_fs = map to_f nondef_us
@@ -462,6 +479,7 @@
PrintMode.setmp [] multiline_string_for_scope scope
val kodkod_sat_solver = Kodkod_SAT.sat_solver_spec effective_sat_solver
|> snd
+ val bit_width = if bits = 0 then 16 else bits + 1
val delay = if liberal then
Option.map (fn time => Time.- (time, Time.now ()))
deadline
@@ -470,7 +488,7 @@
0
val settings = [("solver", commas (map quote kodkod_sat_solver)),
("skolem_depth", "-1"),
- ("bit_width", "16"),
+ ("bit_width", string_of_int bit_width),
("symmetry_breaking", signed_string_of_int sym_break),
("sharing", signed_string_of_int sharing_depth),
("flatten", Bool.toString flatten_props),
@@ -479,7 +497,7 @@
val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels
val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels
val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels
- val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt ofs kk
+ val dtype_axioms = declarative_axioms_for_datatypes ext_ctxt bits ofs kk
rel_table datatypes
val declarative_axioms = plain_axioms @ dtype_axioms
val univ_card = univ_card nat_card int_card main_j0
@@ -491,35 +509,44 @@
val highest_arity =
fold Integer.max (map (fst o fst) (maps fst bounds)) 0
val formula = fold_rev s_and declarative_axioms formula
+ val _ = if bits = 0 then () else check_bits bits formula
val _ = if formula = Kodkod.False then ()
else check_arity univ_card highest_arity
in
SOME ({comment = comment, settings = settings, univ_card = univ_card,
tuple_assigns = [], bounds = bounds,
- int_bounds = sequential_int_bounds univ_card,
+ int_bounds =
+ if bits = 0 then sequential_int_bounds univ_card
+ else pow_of_two_int_bounds bits main_j0 univ_card,
expr_assigns = [], formula = formula},
{free_names = free_names, sel_names = sel_names,
nonsel_names = nonsel_names, rel_table = rel_table,
liberal = liberal, scope = scope, core = core_f,
defs = nondef_fs @ def_fs @ declarative_axioms})
end
- handle LIMIT (loc, msg) =>
+ handle TOO_LARGE (loc, msg) =>
if loc = "Nitpick_Kodkod.check_arity"
andalso not (Typtab.is_empty ofs) then
problem_for_scope liberal
{ext_ctxt = ext_ctxt, card_assigns = card_assigns,
- bisim_depth = bisim_depth, datatypes = datatypes,
- ofs = Typtab.empty}
+ bits = bits, bisim_depth = bisim_depth,
+ datatypes = datatypes, ofs = Typtab.empty}
else if loc = "Nitpick.pick_them_nits_in_term.\
\problem_for_scope" then
NONE
else
(Unsynchronized.change too_big_scopes (cons scope);
print_v (fn () => ("Limit reached: " ^ msg ^
- ". Dropping " ^ (if liberal then "potential"
+ ". Skipping " ^ (if liberal then "potential"
else "genuine") ^
" component of scope."));
NONE)
+ | TOO_SMALL (loc, msg) =>
+ (print_v (fn () => ("Limit reached: " ^ msg ^
+ ". Skipping " ^ (if liberal then "potential"
+ else "genuine") ^
+ " component of scope."));
+ NONE)
(* int -> (''a * int list list) list -> ''a -> Kodkod.tuple_set *)
fun tuple_set_for_rel univ_card =
@@ -663,7 +690,8 @@
let
val num_genuine = take max_potential lib_ps
|> map (print_and_check false)
- |> filter (equal (SOME true)) |> length
+ |> filter (curry (op =) (SOME true))
+ |> length
val max_genuine = max_genuine - num_genuine
val max_potential = max_potential
- (length lib_ps - num_genuine)
@@ -807,7 +835,7 @@
(* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
fun run_batches _ _ [] (max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "ran out of juice"); "unknown")
+ (print_m (fn () => excipit "ran out of some resource"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
@@ -825,9 +853,9 @@
val (skipped, the_scopes) =
all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns
- bisim_depths mono_Ts nonmono_Ts shallow_dataTs
+ bitss bisim_depths mono_Ts nonmono_Ts shallow_dataTs
val _ = if skipped > 0 then
- print_m (fn () => "Too many scopes. Dropping " ^
+ print_m (fn () => "Too many scopes. Skipping " ^
string_of_int skipped ^ " scope" ^
plural_s skipped ^
". (Consider using \"mono\" or \
@@ -859,8 +887,8 @@
error "Nitpick was interrupted."
(* Proof.state -> params -> bool -> term -> string * Proof.state *)
-fun pick_nits_in_term state (params as {debug, timeout, expect, ...})
- auto orig_assm_ts orig_t =
+fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto
+ orig_assm_ts orig_t =
if getenv "KODKODI" = "" then
(if auto then ()
else warning (Pretty.string_of (plazy install_kodkodi_message));
@@ -878,7 +906,7 @@
end
(* Proof.state -> params -> thm -> int -> string * Proof.state *)
-fun pick_nits_in_subgoal state params auto subgoal =
+fun pick_nits_in_subgoal state params auto i =
let
val ctxt = Proof.context_of state
val t = state |> Proof.raw_goal |> #goal |> prop_of
@@ -888,7 +916,7 @@
else
let
val assms = map term_of (Assumption.all_assms_of ctxt)
- val (t, frees) = Logic.goal_params t subgoal
+ val (t, frees) = Logic.goal_params t i
in pick_nits_in_term state params auto assms (subst_bounds (frees, t)) end
end
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Dec 17 15:22:27 2009 +0100
@@ -21,6 +21,7 @@
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
+ binary_ints: bool option,
destroy_constrs: bool,
specialize: bool,
skolemize: bool,
@@ -49,12 +50,12 @@
val skolem_prefix : string
val eval_prefix : string
val original_name : string -> string
- val unbox_type : typ -> typ
+ val unbit_and_unbox_type : typ -> typ
val string_for_type : Proof.context -> typ -> string
val prefix_name : string -> string -> string
+ val shortest_name : string -> string
val short_name : string -> string
- val short_const_name : string -> string
- val shorten_const_names_in_term : term -> term
+ val shorten_names_in_term : term -> term
val type_match : theory -> typ * typ -> bool
val const_match : theory -> styp * styp -> bool
val term_match : theory -> term * term -> bool
@@ -68,6 +69,8 @@
val is_fp_iterator_type : typ -> bool
val is_boolean_type : typ -> bool
val is_integer_type : typ -> bool
+ val is_bit_type : typ -> bool
+ val is_word_type : typ -> bool
val is_record_type : typ -> bool
val is_number_type : theory -> typ -> bool
val const_for_iterator_type : typ -> styp
@@ -91,6 +94,7 @@
val is_constr : theory -> styp -> bool
val is_stale_constr : theory -> styp -> bool
val is_sel : string -> bool
+ val is_sel_like_and_no_discr : string -> bool
val discr_for_constr : styp -> styp
val num_sels_for_constr_type : typ -> int
val nth_sel_name_for_constr_name : string -> int -> string
@@ -111,7 +115,7 @@
val boxed_constr_for_sel : extended_context -> styp -> styp
val card_of_type : (typ * int) list -> typ -> int
val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
- val bounded_precise_card_of_type :
+ val bounded_exact_card_of_type :
extended_context -> int -> int -> (typ * int) list -> typ -> int
val is_finite_type : extended_context -> typ -> bool
val all_axioms_of : theory -> term list * term list * term list
@@ -161,6 +165,7 @@
wfs: (styp option * bool option) list,
user_axioms: bool option,
debug: bool,
+ binary_ints: bool option,
destroy_constrs: bool,
specialize: bool,
skolemize: bool,
@@ -197,12 +202,14 @@
(* term * term -> term *)
fun s_conj (t1, @{const True}) = t1
| s_conj (@{const True}, t2) = t2
- | s_conj (t1, t2) = if @{const False} mem [t1, t2] then @{const False}
- else HOLogic.mk_conj (t1, t2)
+ | s_conj (t1, t2) =
+ if t1 = @{const False} orelse t2 = @{const False} then @{const False}
+ else HOLogic.mk_conj (t1, t2)
fun s_disj (t1, @{const False}) = t1
| s_disj (@{const False}, t2) = t2
- | s_disj (t1, t2) = if @{const True} mem [t1, t2] then @{const True}
- else HOLogic.mk_disj (t1, t2)
+ | s_disj (t1, t2) =
+ if t1 = @{const True} orelse t2 = @{const True} then @{const True}
+ else HOLogic.mk_disj (t1, t2)
(* term -> term -> term *)
fun mk_exists v t =
HOLogic.exists_const (fastype_of v) $ lambda v (incr_boundvars 1 t)
@@ -213,7 +220,7 @@
| strip_connective _ t = [t]
(* term -> term list * term *)
fun strip_any_connective (t as (t0 $ t1 $ t2)) =
- if t0 mem [@{const "op &"}, @{const "op |"}] then
+ if t0 = @{const "op &"} orelse t0 = @{const "op |"} then
(strip_connective t0 t, t0)
else
([t], @{const Not})
@@ -305,7 +312,6 @@
(@{const_name minus_nat_inst.minus_nat}, 0),
(@{const_name times_nat_inst.times_nat}, 0),
(@{const_name div_nat_inst.div_nat}, 0),
- (@{const_name div_nat_inst.mod_nat}, 0),
(@{const_name ord_nat_inst.less_nat}, 2),
(@{const_name ord_nat_inst.less_eq_nat}, 2),
(@{const_name nat_gcd}, 0),
@@ -316,7 +322,6 @@
(@{const_name minus_int_inst.minus_int}, 0),
(@{const_name times_int_inst.times_int}, 0),
(@{const_name div_int_inst.div_int}, 0),
- (@{const_name div_int_inst.mod_int}, 0),
(@{const_name uminus_int_inst.uminus_int}, 0),
(@{const_name ord_int_inst.less_int}, 2),
(@{const_name ord_int_inst.less_eq_int}, 2),
@@ -327,7 +332,8 @@
[(@{const_name The}, 1),
(@{const_name Eps}, 1)]
val built_in_typed_consts =
- [((@{const_name of_nat}, nat_T --> int_T), 0)]
+ [((@{const_name of_nat}, nat_T --> int_T), 0),
+ ((@{const_name of_nat}, @{typ "unsigned_bit word => signed_bit word"}), 0)]
val built_in_set_consts =
[(@{const_name lower_semilattice_fun_inst.inf_fun}, 2),
(@{const_name upper_semilattice_fun_inst.sup_fun}, 2),
@@ -335,31 +341,45 @@
(@{const_name ord_fun_inst.less_eq_fun}, 2)]
(* typ -> typ *)
-fun unbox_type (Type (@{type_name fun_box}, Ts)) =
- Type ("fun", map unbox_type Ts)
- | unbox_type (Type (@{type_name pair_box}, Ts)) =
- Type ("*", map unbox_type Ts)
- | unbox_type (Type (s, Ts)) = Type (s, map unbox_type Ts)
- | unbox_type T = T
+fun unbit_type @{typ "unsigned_bit word"} = nat_T
+ | unbit_type @{typ "signed_bit word"} = int_T
+ | unbit_type @{typ bisim_iterator} = nat_T
+ | unbit_type (Type (s, Ts as _ :: _)) = Type (s, map unbit_type Ts)
+ | unbit_type T = T
+fun unbit_and_unbox_type (Type (@{type_name fun_box}, Ts)) =
+ unbit_and_unbox_type (Type ("fun", Ts))
+ | unbit_and_unbox_type (Type (@{type_name pair_box}, Ts)) =
+ Type ("*", map unbit_and_unbox_type Ts)
+ | unbit_and_unbox_type @{typ "unsigned_bit word"} = nat_T
+ | unbit_and_unbox_type @{typ "signed_bit word"} = int_T
+ | unbit_and_unbox_type @{typ bisim_iterator} = nat_T
+ | unbit_and_unbox_type (Type (s, Ts as _ :: _)) =
+ Type (s, map unbit_and_unbox_type Ts)
+ | unbit_and_unbox_type T = T
(* Proof.context -> typ -> string *)
-fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbox_type
+fun string_for_type ctxt = Syntax.string_of_typ ctxt o unbit_and_unbox_type
(* string -> string -> string *)
val prefix_name = Long_Name.qualify o Long_Name.base_name
(* string -> string *)
-fun short_name s = List.last (space_explode "." s) handle List.Empty => ""
+fun shortest_name s = List.last (space_explode "." s) handle List.Empty => ""
(* string -> term -> term *)
val prefix_abs_vars = Term.map_abs_vars o prefix_name
(* term -> term *)
-val shorten_abs_vars = Term.map_abs_vars short_name
+val shorten_abs_vars = Term.map_abs_vars shortest_name
(* string -> string *)
-fun short_const_name s =
+fun short_name s =
case space_explode name_sep s of
[_] => s |> String.isPrefix nitpick_prefix s ? unprefix nitpick_prefix
- | ss => map short_name ss |> space_implode "_"
+ | ss => map shortest_name ss |> space_implode "_"
+(* typ -> typ *)
+fun shorten_names_in_type (Type (s, Ts)) =
+ Type (short_name s, map shorten_names_in_type Ts)
+ | shorten_names_in_type T = T
(* term -> term *)
-val shorten_const_names_in_term =
- map_aterms (fn Const (s, T) => Const (short_const_name s, T) | t => t)
+val shorten_names_in_term =
+ map_aterms (fn Const (s, T) => Const (short_name s, T) | t => t)
+ #> map_types shorten_names_in_type
(* theory -> typ * typ -> bool *)
fun type_match thy (T1, T2) =
@@ -371,7 +391,7 @@
(* theory -> term * term -> bool *)
fun term_match thy (Const x1, Const x2) = const_match thy (x1, x2)
| term_match thy (Free (s1, T1), Free (s2, T2)) =
- const_match thy ((short_name s1, T1), (short_name s2, T2))
+ const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
| term_match thy (t1, t2) = t1 aconv t2
(* typ -> bool *)
@@ -391,9 +411,12 @@
fun is_gfp_iterator_type (Type (s, _)) = String.isPrefix gfp_iterator_prefix s
| is_gfp_iterator_type _ = false
val is_fp_iterator_type = is_lfp_iterator_type orf is_gfp_iterator_type
-val is_boolean_type = equal prop_T orf equal bool_T
+fun is_boolean_type T = (T = prop_T orelse T = bool_T)
val is_integer_type =
member (op =) [nat_T, int_T, @{typ bisim_iterator}] orf is_fp_iterator_type
+fun is_bit_type T = (T = @{typ unsigned_bit} orelse T = @{typ signed_bit})
+fun is_word_type (Type (@{type_name word}, _)) = true
+ | is_word_type _ = false
val is_record_type = not o null o Record.dest_recTs
(* theory -> typ -> bool *)
fun is_frac_type thy (Type (s, [])) =
@@ -447,16 +470,13 @@
| dest_n_tuple_type _ T =
raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], [])
-(* (typ * typ) list -> typ -> typ *)
-fun typ_subst [] T = T
- | typ_subst ps T =
- let
- (* typ -> typ *)
- fun subst T =
- case AList.lookup (op =) ps T of
- SOME T' => T'
- | NONE => case T of Type (s, Ts) => Type (s, map subst Ts) | _ => T
- in subst T end
+(* FIXME: Use antiquotation for "code_numeral" below or detect "rep_datatype",
+ e.g., by adding a field to "Datatype_Aux.info". *)
+(* string -> bool *)
+val is_basic_datatype =
+ member (op =) [@{type_name "*"}, @{type_name bool}, @{type_name unit},
+ @{type_name nat}, @{type_name int},
+ "Code_Numeral.code_numeral"]
(* theory -> typ -> typ -> typ -> typ *)
fun instantiate_type thy T1 T1' T2 =
@@ -486,8 +506,11 @@
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
val (co_s, co_Ts) = dest_Type co_T
val _ =
- if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) then ()
- else raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
+ if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
+ andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
+ ()
+ else
+ raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
codatatypes
in Data.put {frac_types = frac_types, codatatypes = codatatypes} thy end
@@ -516,12 +539,6 @@
Rep_inverse = SOME Rep_inverse}
| NONE => NONE
-(* FIXME: use antiquotation for "code_numeral" below or detect "rep_datatype",
- e.g., by adding a field to "Datatype_Aux.info". *)
-(* string -> bool *)
-fun is_basic_datatype s =
- s mem [@{type_name "*"}, @{type_name bool}, @{type_name unit},
- @{type_name nat}, @{type_name int}, "Code_Numeral.code_numeral"]
(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
@@ -568,14 +585,15 @@
val num_record_fields = Integer.add 1 o length o fst oo Record.get_extT_fields
(* theory -> string -> typ -> int *)
fun no_of_record_field thy s T1 =
- find_index (equal s o fst) (Record.get_extT_fields thy T1 ||> single |> op @)
+ find_index (curry (op =) s o fst)
+ (Record.get_extT_fields thy T1 ||> single |> op @)
(* theory -> styp -> bool *)
fun is_record_get thy (s, Type ("fun", [T1, _])) =
- exists (equal s o fst) (all_record_fields thy T1)
+ exists (curry (op =) s o fst) (all_record_fields thy T1)
| is_record_get _ _ = false
fun is_record_update thy (s, T) =
String.isSuffix Record.updateN s andalso
- exists (equal (unsuffix Record.updateN s) o fst)
+ exists (curry (op =) (unsuffix Record.updateN s) o fst)
(all_record_fields thy (body_type T))
handle TYPE _ => false
fun is_abs_fun thy (s, Type ("fun", [_, Type (s', _)])) =
@@ -608,11 +626,11 @@
end
handle TYPE ("dest_Type", _, _) => false
fun is_constr_like thy (s, T) =
- s mem [@{const_name FunBox}, @{const_name PairBox}] orelse
- let val (x as (s, T)) = (s, unbox_type T) in
+ s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
+ let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
Refute.is_IDT_constructor thy x orelse is_record_constr x
orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
- orelse s mem [@{const_name Zero_Rep}, @{const_name Suc_Rep}]
+ orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
orelse is_coconstr thy x
end
@@ -621,7 +639,7 @@
andalso not (is_coconstr thy x)
fun is_constr thy (x as (_, T)) =
is_constr_like thy x
- andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
+ andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T)))))
andalso not (is_stale_constr thy x)
(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
@@ -644,10 +662,11 @@
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
case T of
Type ("fun", _) =>
- boxy mem [InPair, InFunLHS] andalso not (is_boolean_type (body_type T))
+ (boxy = InPair orelse boxy = InFunLHS)
+ andalso not (is_boolean_type (body_type T))
| Type ("*", Ts) =>
- boxy mem [InPair, InFunRHS1, InFunRHS2]
- orelse (boxy mem [InExpr, InFunLHS]
+ boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2
+ orelse ((boxy = InExpr orelse boxy = InFunLHS)
andalso exists (is_boxing_worth_it ext_ctxt InPair)
(map (box_type ext_ctxt InPair) Ts))
| _ => false
@@ -660,7 +679,7 @@
and box_type ext_ctxt boxy T =
case T of
Type (z as ("fun", [T1, T2])) =>
- if not (boxy mem [InConstr, InSel])
+ if boxy <> InConstr andalso boxy <> InSel
andalso should_box_type ext_ctxt boxy z then
Type (@{type_name fun_box},
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
@@ -672,8 +691,8 @@
Type (@{type_name pair_box}, map (box_type ext_ctxt InSel) Ts)
else
Type ("*", map (box_type ext_ctxt
- (if boxy mem [InConstr, InSel] then boxy
- else InPair)) Ts)
+ (if boxy = InConstr orelse boxy = InSel then boxy
+ else InPair)) Ts)
| _ => T
(* styp -> styp *)
@@ -872,7 +891,7 @@
val x' as (_, T') =
if is_pair_type T then
let val (T1, T2) = HOLogic.dest_prodT T in
- (@{const_name Pair}, [T1, T2] ---> T)
+ (@{const_name Pair}, T1 --> T2 --> T)
end
else
datatype_constrs ext_ctxt T |> the_single
@@ -883,46 +902,46 @@
end
(* (typ * int) list -> typ -> int *)
-fun card_of_type asgns (Type ("fun", [T1, T2])) =
- reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)
- | card_of_type asgns (Type ("*", [T1, T2])) =
- card_of_type asgns T1 * card_of_type asgns T2
+fun card_of_type assigns (Type ("fun", [T1, T2])) =
+ reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
+ | card_of_type assigns (Type ("*", [T1, T2])) =
+ card_of_type assigns T1 * card_of_type assigns T2
| card_of_type _ (Type (@{type_name itself}, _)) = 1
| card_of_type _ @{typ prop} = 2
| card_of_type _ @{typ bool} = 2
| card_of_type _ @{typ unit} = 1
- | card_of_type asgns T =
- case AList.lookup (op =) asgns T of
+ | card_of_type assigns T =
+ case AList.lookup (op =) assigns T of
SOME k => k
| NONE => if T = @{typ bisim_iterator} then 0
else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
(* int -> (typ * int) list -> typ -> int *)
-fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
+fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
let
- val k1 = bounded_card_of_type max default_card asgns T1
- val k2 = bounded_card_of_type max default_card asgns T2
+ val k1 = bounded_card_of_type max default_card assigns T1
+ val k2 = bounded_card_of_type max default_card assigns T2
in
if k1 = max orelse k2 = max then max
else Int.min (max, reasonable_power k2 k1)
end
- | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =
+ | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
let
- val k1 = bounded_card_of_type max default_card asgns T1
- val k2 = bounded_card_of_type max default_card asgns T2
+ val k1 = bounded_card_of_type max default_card assigns T1
+ val k2 = bounded_card_of_type max default_card assigns T2
in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
- | bounded_card_of_type max default_card asgns T =
+ | bounded_card_of_type max default_card assigns T =
Int.min (max, if default_card = ~1 then
- card_of_type asgns T
+ card_of_type assigns T
else
- card_of_type asgns T
+ card_of_type assigns T
handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
default_card)
(* extended_context -> int -> (typ * int) list -> typ -> int *)
-fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
+fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
let
(* typ list -> typ -> int *)
fun aux avoid T =
- (if T mem avoid then
+ (if member (op =) avoid T then
0
else case T of
Type ("fun", [T1, T2]) =>
@@ -957,16 +976,17 @@
|> map (Integer.prod o map (aux (T :: avoid)) o binder_types
o snd)
in
- if exists (equal 0) constr_cards then 0
+ if exists (curry (op =) 0) constr_cards then 0
else Integer.sum constr_cards
end)
| _ => raise SAME ())
- handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
+ handle SAME () =>
+ AList.lookup (op =) assigns T |> the_default default_card
in Int.min (max, aux [] T) end
(* extended_context -> typ -> bool *)
fun is_finite_type ext_ctxt =
- not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
+ not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
(* term -> bool *)
fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
@@ -989,8 +1009,8 @@
(* theory -> string -> bool *)
fun is_funky_typedef_name thy s =
- s mem [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
- @{type_name int}]
+ member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
+ @{type_name int}] s
orelse is_frac_type thy (Type (s, []))
(* theory -> term -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
@@ -1063,10 +1083,11 @@
val (built_in_nondefs, user_nondefs) =
List.partition (is_typedef_axiom thy false) user_nondefs
|>> append built_in_nondefs
- val defs = (thy |> PureThy.all_thms_of
- |> filter (equal Thm.definitionK o Thm.get_kind o snd)
- |> map (prop_of o snd) |> filter is_plain_definition) @
- user_defs @ built_in_defs
+ val defs =
+ (thy |> PureThy.all_thms_of
+ |> filter (curry (op =) Thm.definitionK o Thm.get_kind o snd)
+ |> map (prop_of o snd) |> filter is_plain_definition) @
+ user_defs @ built_in_defs
in (defs, built_in_nondefs, user_nondefs) end
(* bool -> styp -> int option *)
@@ -1111,7 +1132,7 @@
else
these (Symtab.lookup table s)
|> map_filter (try (Refute.specialize_type thy x))
- |> filter (equal (Const x) o term_under_def)
+ |> filter (curry (op =) (Const x) o term_under_def)
(* theory -> term -> term option *)
fun normalized_rhs_of thy t =
@@ -1152,7 +1173,8 @@
(* term -> bool *)
fun is_good_arg (Bound _) = true
| is_good_arg (Const (s, _)) =
- s mem [@{const_name True}, @{const_name False}, @{const_name undefined}]
+ s = @{const_name True} orelse s = @{const_name False}
+ orelse s = @{const_name undefined}
| is_good_arg _ = false
in
case t |> strip_abs_body |> strip_comb of
@@ -1198,7 +1220,7 @@
(* Proof.context -> term list -> const_table *)
fun const_def_table ctxt ts =
- table_for (map prop_of o Nitpick_Defs.get) ctxt
+ table_for (rev o map prop_of o Nitpick_Defs.get) ctxt
|> fold (fn (s, t) => Symtab.map_default (s, []) (cons t))
(map pair_for_prop ts)
(* term list -> const_table *)
@@ -1307,7 +1329,7 @@
end
(* extended_context -> typ -> int * styp -> term -> term *)
fun add_constr_case (ext_ctxt as {thy, ...}) res_T (j, x) res_t =
- Const (@{const_name If}, [bool_T, res_T, res_T] ---> res_T)
+ Const (@{const_name If}, bool_T --> res_T --> res_T --> res_T)
$ discriminate_value ext_ctxt x (Bound 0) $ constr_case_body thy (j, x)
$ res_t
(* extended_context -> typ -> typ -> term *)
@@ -1538,10 +1560,10 @@
else case def_of_const thy def_table x of
SOME def =>
if depth > unfold_max_depth then
- raise LIMIT ("Nitpick_HOL.unfold_defs_in_term",
- "too many nested definitions (" ^
- string_of_int depth ^ ") while expanding " ^
- quote s)
+ raise TOO_LARGE ("Nitpick_HOL.unfold_defs_in_term",
+ "too many nested definitions (" ^
+ string_of_int depth ^ ") while expanding " ^
+ quote s)
else if s = @{const_name wfrec'} then
(do_term (depth + 1) Ts (betapplys (def, ts)), [])
else
@@ -1556,7 +1578,7 @@
val xs = datatype_constrs ext_ctxt T
val set_T = T --> bool_T
val iter_T = @{typ bisim_iterator}
- val bisim_const = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
+ val bisim_const = Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
val bisim_max = @{const bisim_iterator_max}
val n_var = Var (("n", 0), iter_T)
val n_var_minus_1 =
@@ -1586,7 +1608,7 @@
$ (betapplys (optimized_case_def ext_ctxt T bool_T,
map case_func xs @ [x_var]))),
HOLogic.eq_const set_T $ (bisim_const $ bisim_max $ x_var)
- $ (Const (@{const_name insert}, [T, set_T] ---> set_T)
+ $ (Const (@{const_name insert}, T --> set_T --> set_T)
$ x_var $ Const (@{const_name bot_fun_inst.bot_fun}, set_T))]
|> map HOLogic.mk_Trueprop
end
@@ -1598,9 +1620,9 @@
let
val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
- val (main, side) = List.partition (exists_Const (equal x)) prems
+ val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
(* term -> bool *)
- val is_good_head = equal (Const x) o head_of
+ val is_good_head = curry (op =) (Const x) o head_of
in
if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE ()
end
@@ -1693,7 +1715,7 @@
(x as (s, _)) =
case triple_lookup (const_match thy) wfs x of
SOME (SOME b) => b
- | _ => s mem [@{const_name Nats}, @{const_name fold_graph'}]
+ | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
orelse case AList.lookup (op =) (!wf_cache) x of
SOME (_, wf) => wf
| NONE =>
@@ -1730,7 +1752,7 @@
| do_disjunct j t =
case num_occs_of_bound_in_term j t of
0 => true
- | 1 => exists (equal (Bound j) o head_of) (conjuncts t)
+ | 1 => exists (curry (op =) (Bound j) o head_of) (conjuncts t)
| _ => false
(* term -> bool *)
fun do_lfp_def (Const (@{const_name lfp}, _) $ t2) =
@@ -1774,7 +1796,7 @@
t
end
val (nonrecs, recs) =
- List.partition (equal 0 o num_occs_of_bound_in_term j)
+ List.partition (curry (op =) 0 o num_occs_of_bound_in_term j)
(disjuncts body)
val base_body = nonrecs |> List.foldl s_disj @{const False}
val step_body = recs |> map (repair_rec j)
@@ -1923,7 +1945,7 @@
| Type ("*", Ts) => fold (add_ground_types ext_ctxt) Ts accum
| Type (@{type_name itself}, [T1]) => add_ground_types ext_ctxt T1 accum
| Type (_, Ts) =>
- if T mem @{typ prop} :: @{typ bool} :: @{typ unit} :: accum then
+ if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
accum
else
T :: accum
@@ -1962,7 +1984,7 @@
andalso has_heavy_bounds_or_vars Ts level t_comb
andalso not (loose_bvar (t_comb, level)) then
let
- val (j, seen) = case find_index (equal t_comb) seen of
+ val (j, seen) = case find_index (curry (op =) t_comb) seen of
~1 => (0, t_comb :: seen)
| j => (j, seen)
in (fresh_value_var Ts k (length seen) j t_comb, seen) end
@@ -2046,8 +2068,8 @@
(Const (x as (s, T)), args) =>
let val arg_Ts = binder_types T in
if length arg_Ts = length args
- andalso (is_constr thy x orelse s mem [@{const_name Pair}]
- orelse x = dest_Const @{const Suc})
+ andalso (is_constr thy x orelse s = @{const_name Pair}
+ orelse x = (@{const_name Suc}, nat_T --> nat_T))
andalso (not careful orelse not (is_Var t1)
orelse String.isPrefix val_var_prefix
(fst (fst (dest_Var t1)))) then
@@ -2141,7 +2163,8 @@
(* term list -> (indexname * typ) list -> indexname * typ -> term -> term
-> term -> term *)
and aux_eq prems zs z t' t1 t2 =
- if not (z mem zs) andalso not (exists_subterm (equal (Var z)) t') then
+ if not (member (op =) zs z)
+ andalso not (exists_subterm (curry (op =) (Var z)) t') then
aux prems zs (subst_free [(Var z, t')] t2)
else
aux (t1 :: prems) (Term.add_vars t1 zs) t2
@@ -2299,8 +2322,8 @@
(t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
aux s0 (s1 :: ss) (T1 :: Ts) t1
- else if quant_s = ""
- andalso s0 mem [@{const_name All}, @{const_name Ex}] then
+ else if quant_s = "" andalso (s0 = @{const_name All}
+ orelse s0 = @{const_name Ex}) then
aux s0 [s1] [T1] t1
else
raise SAME ()
@@ -2330,7 +2353,8 @@
| cost boundss_cum_costs (j :: js) =
let
val (yeas, nays) =
- List.partition (fn (bounds, _) => j mem bounds)
+ List.partition (fn (bounds, _) =>
+ member (op =) bounds j)
boundss_cum_costs
val yeas_bounds = big_union fst yeas
val yeas_cost = Integer.sum (map snd yeas)
@@ -2339,7 +2363,7 @@
val js = all_permutations (index_seq 0 num_Ts)
|> map (`(cost (t_boundss ~~ t_costs)))
|> sort (int_ord o pairself fst) |> hd |> snd
- val back_js = map (fn j => find_index (equal j) js)
+ val back_js = map (fn j => find_index (curry (op =) j) js)
(index_seq 0 num_Ts)
val ts = map (renumber_bounds 0 num_Ts (nth back_js o flip))
ts
@@ -2355,7 +2379,8 @@
| build ts_cum_bounds (j :: js) =
let
val (yeas, nays) =
- List.partition (fn (_, bounds) => j mem bounds)
+ List.partition (fn (_, bounds) =>
+ member (op =) bounds j)
ts_cum_bounds
||> map (apfst (incr_boundvars ~1))
in
@@ -2476,7 +2501,7 @@
map Bound (length trunk_arg_Ts - 1 downto 0))
in
List.foldr absdummy
- (Const (set_oper, [set_T, set_T] ---> set_T)
+ (Const (set_oper, set_T --> set_T --> set_T)
$ app pos $ app neg) trunk_arg_Ts
end
else
@@ -2548,7 +2573,7 @@
if t = Const x then
list_comb (Const x', extra_args @ filter_out_indices fixed_js args)
else
- let val j = find_index (equal t) fixed_params in
+ let val j = find_index (curry (op =) t) fixed_params in
list_comb (if j >= 0 then nth fixed_args j else t, args)
end
in aux [] t end
@@ -2582,7 +2607,7 @@
else case term_under_def t of Const x => [x] | _ => []
(* term list -> typ list -> term -> term *)
fun aux args Ts (Const (x as (s, T))) =
- ((if not (x mem blacklist) andalso not (null args)
+ ((if not (member (op =) blacklist x) andalso not (null args)
andalso not (String.isPrefix special_prefix s)
andalso is_equational_fun ext_ctxt x then
let
@@ -2607,7 +2632,8 @@
(* int -> term *)
fun var_for_bound_no j =
Var ((bound_var_prefix ^
- nat_subscript (find_index (equal j) bound_js + 1), k),
+ nat_subscript (find_index (curry (op =) j) bound_js
+ + 1), k),
nth Ts j)
val fixed_args_in_axiom =
map (curry subst_bounds
@@ -2739,7 +2765,8 @@
\coerce_term", [t']))
| (Type (new_s, new_Ts as [new_T1, new_T2]),
Type (old_s, old_Ts as [old_T1, old_T2])) =>
- if old_s mem [@{type_name fun_box}, @{type_name pair_box}, "*"] then
+ if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box}
+ orelse old_s = "*" then
case constr_expand ext_ctxt old_T t of
Const (@{const_name FunBox}, _) $ t1 =>
if new_s = "fun" then
@@ -2770,13 +2797,13 @@
fold (add_boxed_types_for_var z) [(T1, t1), (T2, t2)]
| _ => raise TYPE ("Nitpick_HOL.box_fun_and_pair_in_term.\
\add_boxed_types_for_var", [T'], []))
- | _ => exists_subterm (equal (Var z)) t' ? insert (op =) T
+ | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
(* typ list -> typ list -> term -> indexname * typ -> typ *)
fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
case t of
@{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
| Const (s0, _) $ t1 $ _ =>
- if s0 mem [@{const_name "=="}, @{const_name "op ="}] then
+ if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
let
val (t', args) = strip_comb t1
val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
@@ -2811,7 +2838,7 @@
val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
in
- list_comb (Const (s0, [T, T] ---> body_type T0),
+ list_comb (Const (s0, T --> T --> body_type T0),
map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
end
(* string -> typ -> term *)
@@ -2855,7 +2882,8 @@
| Const (s as @{const_name Eps}, T) => do_description_operator s T
| Const (s as @{const_name Tha}, T) => do_description_operator s T
| Const (x as (s, T)) =>
- Const (s, if s mem [@{const_name converse}, @{const_name trancl}] then
+ Const (s, if s = @{const_name converse}
+ orelse s = @{const_name trancl} then
box_relational_operator_type T
else if is_built_in_const fast_descrs x
orelse s = @{const_name Sigma} then
@@ -2954,7 +2982,7 @@
|> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
|> AList.group (op =)
|> filter_out (is_equational_fun_surely_complete ext_ctxt o fst)
- |> map (fn (x, zs) => (x, zs |> (x mem xs) ? cons ([], [], x)))
+ |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
(* special -> int *)
fun generality (js, _, _) = ~(length js)
(* special -> special -> bool *)
@@ -3022,14 +3050,15 @@
case t of
t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
| Const (x as (s, T)) =>
- (if x mem xs orelse is_built_in_const fast_descrs x then
+ (if member (op =) xs x orelse is_built_in_const fast_descrs x then
accum
else
let val accum as (xs, _) = (x :: xs, axs) in
if depth > axioms_max_depth then
- raise LIMIT ("Nitpick_HOL.axioms_for_term.add_axioms_for_term",
- "too many nested axioms (" ^ string_of_int depth ^
- ")")
+ raise TOO_LARGE ("Nitpick_HOL.axioms_for_term.\
+ \add_axioms_for_term",
+ "too many nested axioms (" ^
+ string_of_int depth ^ ")")
else if Refute.is_const_of_class thy x then
let
val class = Logic.class_of_const s
@@ -3172,10 +3201,10 @@
(* int list -> int list -> typ -> typ *)
fun format_type default_format format T =
let
- val T = unbox_type T
+ val T = unbit_and_unbox_type T
val format = format |> filter (curry (op <) 0)
in
- if forall (equal 1) format then
+ if forall (curry (op =) 1) format then
T
else
let
@@ -3211,7 +3240,8 @@
(* term -> term *)
val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t')
val (x' as (_, T'), js, ts) =
- AList.find (op =) (!special_funs) (s, unbox_type T) |> the_single
+ AList.find (op =) (!special_funs) (s, unbit_and_unbox_type T)
+ |> the_single
val max_j = List.last js
val Ts = List.take (binder_types T', max_j + 1)
val missing_js = filter_out (member (op =) js) (0 upto max_j)
@@ -3226,7 +3256,8 @@
SOME t => do_term t
| NONE =>
Var (nth missing_vars
- (find_index (equal j) missing_js)))
+ (find_index (curry (op =) j)
+ missing_js)))
Ts (0 upto max_j)
val t = do_const x' |> fst
val format =
@@ -3299,8 +3330,8 @@
let val t = Const (original_name s, T) in
(t, format_term_type thy def_table formats t)
end)
- |>> map_types (typ_subst [(@{typ bisim_iterator}, nat_T)] o unbox_type)
- |>> shorten_const_names_in_term |>> shorten_abs_vars
+ |>> map_types unbit_and_unbox_type
+ |>> shorten_names_in_term |>> shorten_abs_vars
in do_const end
(* styp -> string *)
@@ -3314,10 +3345,45 @@
else
"="
+val binary_int_threshold = 4
+
+(* term -> bool *)
+fun may_use_binary_ints (t1 $ t2) =
+ may_use_binary_ints t1 andalso may_use_binary_ints t2
+ | may_use_binary_ints (Const (s, _)) =
+ not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac},
+ @{const_name Frac}, @{const_name norm_frac},
+ @{const_name nat_gcd}, @{const_name nat_lcm}] s)
+ | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t'
+ | may_use_binary_ints _ = true
+
+fun should_use_binary_ints (t1 $ t2) =
+ should_use_binary_ints t1 orelse should_use_binary_ints t2
+ | should_use_binary_ints (Const (s, _)) =
+ member (op =) [@{const_name times_nat_inst.times_nat},
+ @{const_name div_nat_inst.div_nat},
+ @{const_name times_int_inst.times_int},
+ @{const_name div_int_inst.div_int}] s
+ orelse (String.isPrefix numeral_prefix s andalso
+ let val n = the (Int.fromString (unprefix numeral_prefix s)) in
+ n <= ~ binary_int_threshold orelse n >= binary_int_threshold
+ end)
+ | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
+ | should_use_binary_ints _ = false
+
+(* typ -> typ *)
+fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
+ | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
+ | binarize_nat_and_int_in_type (Type (s, Ts)) =
+ Type (s, map binarize_nat_and_int_in_type Ts)
+ | binarize_nat_and_int_in_type T = T
+(* term -> term *)
+val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
+
(* extended_context -> term
-> ((term list * term list) * (bool * bool)) * term *)
-fun preprocess_term (ext_ctxt as {thy, destroy_constrs, boxes, skolemize,
- uncurry, ...}) t =
+fun preprocess_term (ext_ctxt as {thy, binary_ints, destroy_constrs, boxes,
+ skolemize, uncurry, ...}) t =
let
val skolem_depth = if skolemize then 4 else ~1
val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
@@ -3326,14 +3392,22 @@
|> skolemize_term_and_more ext_ctxt skolem_depth
|> specialize_consts_in_term ext_ctxt 0
|> `(axioms_for_term ext_ctxt)
- val maybe_box = exists (not_equal (SOME false) o snd) boxes
+ val binarize =
+ case binary_ints of
+ SOME false => false
+ | _ =>
+ forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+ (binary_ints = SOME true
+ orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ val box = exists (not_equal (SOME false) o snd) boxes
val table =
Termtab.empty |> uncurry
? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
(* bool -> bool -> term -> term *)
fun do_rest def core =
- uncurry ? uncurry_term table
- #> maybe_box ? box_fun_and_pair_in_term ext_ctxt def
+ binarize ? binarize_nat_and_int_in_term
+ #> uncurry ? uncurry_term table
+ #> box ? box_fun_and_pair_in_term ext_ctxt def
#> destroy_constrs ? (pull_out_universal_constrs thy def
#> pull_out_existential_constrs thy
#> destroy_pulled_out_constrs ext_ctxt def)
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Thu Dec 17 15:22:27 2009 +0100
@@ -37,6 +37,7 @@
val default_default_params =
[("card", ["1\<midarrow>8"]),
("iter", ["0,1,2,4,8,12,16,24"]),
+ ("bits", ["1,2,3,4,6,8,10,12"]),
("bisim_depth", ["7"]),
("box", ["smart"]),
("mono", ["smart"]),
@@ -48,6 +49,7 @@
("user_axioms", ["smart"]),
("assms", ["true"]),
("merge_type_vars", ["false"]),
+ ("binary_ints", ["smart"]),
("destroy_constrs", ["true"]),
("specialize", ["true"]),
("skolemize", ["true"]),
@@ -83,6 +85,7 @@
("no_user_axioms", "user_axioms"),
("no_assms", "assms"),
("dont_merge_type_vars", "merge_type_vars"),
+ ("unary_ints", "binary_ints"),
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_skolemize", "skolemize"),
@@ -105,7 +108,7 @@
fun is_known_raw_param s =
AList.defined (op =) default_default_params s
orelse AList.defined (op =) negated_params s
- orelse s mem ["max", "eval", "expect"]
+ orelse s = "max" orelse s = "eval" orelse s = "expect"
orelse exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
"wf", "non_wf", "format"]
@@ -283,6 +286,7 @@
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
+ val bitss = lookup_int_seq "bits" 1
val bisim_depths = lookup_int_seq "bisim_depth" ~1
val boxes =
lookup_bool_option_assigns read_type_polymorphic "box" @
@@ -303,6 +307,7 @@
val user_axioms = lookup_bool_option "user_axioms"
val assms = lookup_bool "assms"
val merge_type_vars = lookup_bool "merge_type_vars"
+ val binary_ints = lookup_bool_option "binary_ints"
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val skolemize = lookup_bool "skolemize"
@@ -333,15 +338,16 @@
val expect = lookup_string "expect"
in
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
- iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes,
- monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
- falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
- user_axioms = user_axioms, assms = assms,
- merge_type_vars = merge_type_vars, destroy_constrs = destroy_constrs,
- specialize = specialize, skolemize = skolemize,
- star_linear_preds = star_linear_preds, uncurry = uncurry,
- fast_descrs = fast_descrs, peephole_optim = peephole_optim,
- timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break,
+ iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
+ boxes = boxes, monos = monos, wfs = wfs, sat_solver = sat_solver,
+ blocking = blocking, falsify = falsify, debug = debug, verbose = verbose,
+ overlord = overlord, user_axioms = user_axioms, assms = assms,
+ merge_type_vars = merge_type_vars, binary_ints = binary_ints,
+ destroy_constrs = destroy_constrs, specialize = specialize,
+ skolemize = skolemize, star_linear_preds = star_linear_preds,
+ uncurry = uncurry, fast_descrs = fast_descrs,
+ peephole_optim = peephole_optim, timeout = timeout,
+ tac_timeout = tac_timeout, sym_break = sym_break,
sharing_depth = sharing_depth, flatten_props = flatten_props,
max_threads = max_threads, show_skolems = show_skolems,
show_datatypes = show_datatypes, show_consts = show_consts,
@@ -379,8 +385,6 @@
error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
| BAD (loc, details) =>
error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
- | LIMIT (_, details) =>
- (warning ("Limit reached: " ^ details ^ "."); x)
| NOT_SUPPORTED details =>
(warning ("Unsupported case: " ^ details ^ "."); x)
| NUT (loc, us) =>
@@ -394,6 +398,10 @@
error ("Invalid term" ^ plural_s_for_list ts ^
" (" ^ quote loc ^ "): " ^
commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
+ | TOO_LARGE (_, details) =>
+ (warning ("Limit reached: " ^ details ^ "."); x)
+ | TOO_SMALL (_, details) =>
+ (warning ("Limit reached: " ^ details ^ "."); x)
| TYPE (loc, Ts, ts) =>
error ("Invalid type" ^ plural_s_for_list Ts ^
(if null ts then
@@ -409,7 +417,7 @@
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
(* raw_param list -> bool -> int -> Proof.state -> bool * Proof.state *)
-fun pick_nits override_params auto subgoal state =
+fun pick_nits override_params auto i state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
@@ -423,26 +431,25 @@
|> (if auto then perhaps o try
else if debug then fn f => fn x => f x
else handle_exceptions ctxt)
- (fn (_, state) => pick_nits_in_subgoal state params auto subgoal
- |>> equal "genuine")
+ (fn (_, state) => pick_nits_in_subgoal state params auto i
+ |>> curry (op =) "genuine")
in
if auto orelse blocking then go ()
else (Toplevel.thread true (fn () => (go (); ())); (false, state))
end
-(* (TableFun().key * string list) list option * int option
- -> Toplevel.transition -> Toplevel.transition *)
-fun nitpick_trans (opt_params, opt_subgoal) =
+(* raw_param list option * int option -> Toplevel.transition
+ -> Toplevel.transition *)
+fun nitpick_trans (opt_params, opt_i) =
Toplevel.keep (K ()
- o snd o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
+ o snd o pick_nits (these opt_params) false (the_default 1 opt_i)
o Toplevel.proof_of)
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
-(* (TableFun().key * string) list option -> Toplevel.transition
- -> Toplevel.transition *)
+(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
fun nitpick_params_trans opt_params =
Toplevel.theory
(fold set_default_raw_param (these opt_params)
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Dec 17 15:22:27 2009 +0100
@@ -19,10 +19,12 @@
val univ_card :
int -> int -> int -> Kodkod.bound list -> Kodkod.formula -> int
+ val check_bits : int -> Kodkod.formula -> unit
val check_arity : int -> int -> unit
val kk_tuple : bool -> int -> int list -> Kodkod.tuple
val tuple_set_from_atom_schema : (int * int) list -> Kodkod.tuple_set
val sequential_int_bounds : int -> Kodkod.int_bound list
+ val pow_of_two_int_bounds : int -> int -> int -> Kodkod.int_bound list
val bounds_for_built_in_rels_in_formula :
bool -> int -> int -> int -> int -> Kodkod.formula -> Kodkod.bound list
val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
@@ -31,10 +33,10 @@
val merge_bounds : Kodkod.bound list -> Kodkod.bound list
val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
val declarative_axioms_for_datatypes :
- extended_context -> int Typtab.table -> kodkod_constrs
+ extended_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
- int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
+ int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
end;
structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -80,18 +82,28 @@
|> Kodkod.fold_formula expr_F formula
in Int.max (main_j0 + fold Integer.max [2, nat_card, int_card] 0, card) end
-(* Proof.context -> bool -> string -> typ -> rep -> string *)
-fun bound_comment ctxt debug nick T R =
- short_const_name nick ^
- (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
- else "") ^ " : " ^ string_for_rep R
+(* int -> Kodkod.formula -> unit *)
+fun check_bits bits formula =
+ let
+ (* Kodkod.int_expr -> unit -> unit *)
+ fun int_expr_func (Kodkod.Num k) () =
+ if is_twos_complement_representable bits k then
+ ()
+ else
+ raise TOO_SMALL ("Nitpick_Kodkod.check_bits",
+ "\"bits\" value " ^ string_of_int bits ^
+ " too small for problem")
+ | int_expr_func _ () = ()
+ val expr_F = {formula_func = K I, rel_expr_func = K I,
+ int_expr_func = int_expr_func}
+ in Kodkod.fold_formula expr_F formula () end
(* int -> int -> unit *)
fun check_arity univ_card n =
if n > Kodkod.max_arity univ_card then
- raise LIMIT ("Nitpick_Kodkod.check_arity",
- "arity " ^ string_of_int n ^ " too large for universe of \
- \cardinality " ^ string_of_int univ_card)
+ raise TOO_LARGE ("Nitpick_Kodkod.check_arity",
+ "arity " ^ string_of_int n ^ " too large for universe of \
+ \cardinality " ^ string_of_int univ_card)
else
()
@@ -109,20 +121,34 @@
(* rep -> Kodkod.tuple_set *)
val upper_bound_for_rep = tuple_set_from_atom_schema o atom_schema_of_rep
+(* int -> Kodkod.tuple_set *)
+val single_atom = Kodkod.TupleSet o single o Kodkod.Tuple o single
(* int -> Kodkod.int_bound list *)
-fun sequential_int_bounds n =
- [(NONE, map (Kodkod.TupleSet o single o Kodkod.Tuple o single)
- (index_seq 0 n))]
+fun sequential_int_bounds n = [(NONE, map single_atom (index_seq 0 n))]
+(* int -> int -> Kodkod.int_bound list *)
+fun pow_of_two_int_bounds bits j0 univ_card =
+ let
+ (* int -> int -> int -> Kodkod.int_bound list *)
+ fun aux 0 _ _ = []
+ | aux 1 pow_of_two j =
+ if j < univ_card then [(SOME (~ pow_of_two), [single_atom j])] else []
+ | aux iter pow_of_two j =
+ (SOME pow_of_two, [single_atom j]) ::
+ aux (iter - 1) (2 * pow_of_two) (j + 1)
+ in aux (bits + 1) 1 j0 end
(* Kodkod.formula -> Kodkod.n_ary_index list *)
fun built_in_rels_in_formula formula =
let
(* Kodkod.rel_expr -> Kodkod.n_ary_index list -> Kodkod.n_ary_index list *)
- fun rel_expr_func (Kodkod.Rel (n, j)) rels =
- (case AList.lookup (op =) (#rels initial_pool) n of
- SOME k => (j < k ? insert (op =) (n, j)) rels
- | NONE => rels)
- | rel_expr_func _ rels = rels
+ fun rel_expr_func (r as Kodkod.Rel (x as (n, j))) =
+ if x = unsigned_bit_word_sel_rel orelse x = signed_bit_word_sel_rel then
+ I
+ else
+ (case AList.lookup (op =) (#rels initial_pool) n of
+ SOME k => j < k ? insert (op =) x
+ | NONE => I)
+ | rel_expr_func _ = I
val expr_F = {formula_func = K I, rel_expr_func = rel_expr_func,
int_expr_func = K I}
in Kodkod.fold_formula expr_F formula [] end
@@ -132,8 +158,8 @@
(* int -> unit *)
fun check_table_size k =
if k > max_table_size then
- raise LIMIT ("Nitpick_Kodkod.check_table_size",
- "precomputed table too large (" ^ string_of_int k ^ ")")
+ raise TOO_LARGE ("Nitpick_Kodkod.check_table_size",
+ "precomputed table too large (" ^ string_of_int k ^ ")")
else
()
@@ -205,43 +231,39 @@
-> string * bool * Kodkod.tuple list *)
fun tabulate_built_in_rel debug univ_card nat_card int_card j0 (x as (n, _)) =
(check_arity univ_card n;
- if Kodkod.Rel x = not3_rel then
+ if x = not3_rel then
("not3", tabulate_func1 debug univ_card (2, j0) (curry (op -) 1))
- else if Kodkod.Rel x = suc_rel then
+ else if x = suc_rel then
("suc", tabulate_func1 debug univ_card (univ_card - j0 - 1, j0)
(Integer.add 1))
- else if Kodkod.Rel x = nat_add_rel then
+ else if x = nat_add_rel then
("nat_add", tabulate_nat_op2 debug univ_card (nat_card, j0) (op +))
- else if Kodkod.Rel x = int_add_rel then
+ else if x = int_add_rel then
("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +))
- else if Kodkod.Rel x = nat_subtract_rel then
+ else if x = nat_subtract_rel then
("nat_subtract",
tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus))
- else if Kodkod.Rel x = int_subtract_rel then
+ else if x = int_subtract_rel then
("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -))
- else if Kodkod.Rel x = nat_multiply_rel then
+ else if x = nat_multiply_rel then
("nat_multiply", tabulate_nat_op2 debug univ_card (nat_card, j0) (op * ))
- else if Kodkod.Rel x = int_multiply_rel then
+ else if x = int_multiply_rel then
("int_multiply", tabulate_int_op2 debug univ_card (int_card, j0) (op * ))
- else if Kodkod.Rel x = nat_divide_rel then
+ else if x = nat_divide_rel then
("nat_divide", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_div)
- else if Kodkod.Rel x = int_divide_rel then
+ else if x = int_divide_rel then
("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
- else if Kodkod.Rel x = nat_modulo_rel then
- ("nat_modulo", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_mod)
- else if Kodkod.Rel x = int_modulo_rel then
- ("int_modulo", tabulate_int_op2 debug univ_card (int_card, j0) isa_mod)
- else if Kodkod.Rel x = nat_less_rel then
+ else if x = nat_less_rel then
("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
(int_for_bool o op <))
- else if Kodkod.Rel x = int_less_rel then
+ else if x = int_less_rel then
("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
(int_for_bool o op <))
- else if Kodkod.Rel x = gcd_rel then
+ else if x = gcd_rel then
("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
- else if Kodkod.Rel x = lcm_rel then
+ else if x = lcm_rel then
("lcm", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_lcm)
- else if Kodkod.Rel x = norm_frac_rel then
+ else if x = norm_frac_rel then
("norm_frac", tabulate_int_op2_2 debug univ_card (int_card, j0)
isa_norm_frac)
else
@@ -260,12 +282,18 @@
map (bound_for_built_in_rel debug univ_card nat_card int_card j0)
o built_in_rels_in_formula
+(* Proof.context -> bool -> string -> typ -> rep -> string *)
+fun bound_comment ctxt debug nick T R =
+ short_name nick ^
+ (if debug then " :: " ^ plain_string_from_yxml (Syntax.string_of_typ ctxt T)
+ else "") ^ " : " ^ string_for_rep R
+
(* Proof.context -> bool -> nut -> Kodkod.bound *)
fun bound_for_plain_rel ctxt debug (u as FreeRel (x, T, R, nick)) =
([(x, bound_comment ctxt debug nick T R)],
if nick = @{const_name bisim_iterator_max} then
case R of
- Atom (k, j0) => [Kodkod.TupleSet [Kodkod.Tuple [k - 1 + j0]]]
+ Atom (k, j0) => [single_atom (k - 1 + j0)]
| _ => raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
else
[Kodkod.TupleSet [], upper_bound_for_rep R])
@@ -369,17 +397,17 @@
else
Kodkod.True
end
-fun kk_n_ary_function kk R (r as Kodkod.Rel _) =
+fun kk_n_ary_function kk R (r as Kodkod.Rel x) =
if not (is_opt_rep R) then
- if r = suc_rel then
+ if x = suc_rel then
Kodkod.False
- else if r = nat_add_rel then
+ else if x = nat_add_rel then
formula_for_bool (card_of_rep (body_rep R) = 1)
- else if r = nat_multiply_rel then
+ else if x = nat_multiply_rel then
formula_for_bool (card_of_rep (body_rep R) <= 2)
else
d_n_ary_function kk R r
- else if r = nat_subtract_rel then
+ else if x = nat_subtract_rel then
Kodkod.True
else
d_n_ary_function kk R r
@@ -393,27 +421,27 @@
(* int -> kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr)
-> Kodkod.rel_expr -> Kodkod.rel_expr *)
-fun basic_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
+fun basic_rel_rel_let j ({kk_rel_let, ...} : kodkod_constrs) f r =
if inline_rel_expr r then
f r
else
let val x = (Kodkod.arity_of_rel_expr r, j) in
kk_rel_let [Kodkod.AssignRelReg (x, r)] (f (Kodkod.RelReg x))
end
-
(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr) -> Kodkod.rel_expr
-> Kodkod.rel_expr *)
-val single_rel_let = basic_rel_let 0
+val single_rel_rel_let = basic_rel_rel_let 0
(* kodkod_constrs -> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
-> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
-fun double_rel_let kk f r1 r2 =
- single_rel_let kk (fn r1 => basic_rel_let 1 kk (f r1) r2) r1
+fun double_rel_rel_let kk f r1 r2 =
+ single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
(* kodkod_constrs
-> (Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr)
-> Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr
-> Kodkod.rel_expr *)
-fun triple_rel_let kk f r1 r2 r3 =
- double_rel_let kk (fn r1 => fn r2 => basic_rel_let 2 kk (f r1 r2) r3) r1 r2
+fun tripl_rel_rel_let kk f r1 r2 r3 =
+ double_rel_rel_let kk
+ (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
(* kodkod_constrs -> int -> Kodkod.formula -> Kodkod.rel_expr *)
fun atom_from_formula ({kk_rel_if, ...} : kodkod_constrs) j0 f =
@@ -469,8 +497,8 @@
if is_lone_rep old_R andalso is_lone_rep new_R
andalso card = card_of_rep new_R then
if card >= lone_rep_fallback_max_card then
- raise LIMIT ("Nitpick_Kodkod.lone_rep_fallback",
- "too high cardinality (" ^ string_of_int card ^ ")")
+ raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
+ "too high cardinality (" ^ string_of_int card ^ ")")
else
kk_case_switch kk old_R new_R r (all_singletons_for_rep old_R)
(all_singletons_for_rep new_R)
@@ -672,6 +700,21 @@
(* kodkod_constrs -> rep -> rep -> rep -> Kodkod.rel_expr -> Kodkod.rel_expr *)
and rel_expr_to_func kk R1 R2 = rel_expr_from_rel_expr kk (Func (R1, R2))
+(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.rel_expr *)
+fun bit_set_from_atom ({kk_join, ...} : kodkod_constrs) T r =
+ kk_join r (Kodkod.Rel (if T = @{typ "unsigned_bit word"} then
+ unsigned_bit_word_sel_rel
+ else
+ signed_bit_word_sel_rel))
+(* kodkod_constrs -> typ -> Kodkod.rel_expr -> Kodkod.int_expr *)
+val int_expr_from_atom = Kodkod.SetSum ooo bit_set_from_atom
+(* kodkod_constrs -> typ -> rep -> Kodkod.int_expr -> Kodkod.rel_expr *)
+fun atom_from_int_expr (kk as {kk_rel_eq, kk_comprehension, ...}
+ : kodkod_constrs) T R i =
+ kk_comprehension (decls_for_atom_schema ~1 (atom_schema_of_rep R))
+ (kk_rel_eq (bit_set_from_atom kk T (Kodkod.Var (1, ~1)))
+ (Kodkod.Bits i))
+
(* kodkod_constrs -> nut -> Kodkod.formula *)
fun declarative_axiom_for_plain_rel kk (FreeRel (x, _, R as Func _, nick)) =
kk_n_ary_function kk (R |> nick = @{const_name List.set} ? unopt_rep)
@@ -725,7 +768,7 @@
(* nfa_table -> typ -> typ -> Kodkod.rel_expr list *)
fun direct_path_rel_exprs nfa start final =
case AList.lookup (op =) nfa final of
- SOME trans => map fst (filter (equal start o snd) trans)
+ SOME trans => map fst (filter (curry (op =) start o snd) trans)
| NONE => []
(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> Kodkod.rel_expr *)
and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
@@ -804,9 +847,9 @@
(kk_no r'))
end
end
-(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
+(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
-> constr_spec -> Kodkod.formula list *)
-fun sel_axioms_for_constr ext_ctxt j0 kk rel_table
+fun sel_axioms_for_constr ext_ctxt bits j0 kk rel_table
(constr as {const, delta, epsilon, explicit_max, ...}) =
let
val honors_explicit_max =
@@ -818,19 +861,25 @@
let
val ran_r = discr_rel_expr rel_table const
val max_axiom =
- if honors_explicit_max then Kodkod.True
- else Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
+ if honors_explicit_max then
+ Kodkod.True
+ else if is_twos_complement_representable bits (epsilon - delta) then
+ Kodkod.LE (Kodkod.Cardinality ran_r, Kodkod.Num explicit_max)
+ else
+ raise TOO_SMALL ("Nitpick_Kodkod.sel_axioms_for_constr",
+ "\"bits\" value " ^ string_of_int bits ^
+ " too small for \"max\"")
in
max_axiom ::
map (sel_axiom_for_sel ext_ctxt j0 kk rel_table ran_r constr)
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
-(* extended_context -> int -> kodkod_constrs -> nut NameTable.table
+(* extended_context -> int -> int -> kodkod_constrs -> nut NameTable.table
-> dtype_spec -> Kodkod.formula list *)
-fun sel_axioms_for_datatype ext_ctxt j0 kk rel_table
+fun sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table
({constrs, ...} : dtype_spec) =
- maps (sel_axioms_for_constr ext_ctxt j0 kk rel_table) constrs
+ maps (sel_axioms_for_constr ext_ctxt bits j0 kk rel_table) constrs
(* extended_context -> kodkod_constrs -> nut NameTable.table -> constr_spec
-> Kodkod.formula list *)
@@ -881,24 +930,25 @@
kk_disjoint_sets kk rs]
end
-(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec -> Kodkod.formula list *)
-fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = []
- | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) =
+(* extended_context -> int -> int Typtab.table -> kodkod_constrs
+ -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *)
+fun other_axioms_for_datatype _ _ _ _ _ {shallow = true, ...} = []
+ | other_axioms_for_datatype ext_ctxt bits ofs kk rel_table
+ (dtype as {typ, ...}) =
let val j0 = offset_of_type ofs typ in
- sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @
+ sel_axioms_for_datatype ext_ctxt bits j0 kk rel_table dtype @
uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @
partition_axioms_for_datatype j0 kk rel_table dtype
end
-(* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
- -> dtype_spec list -> Kodkod.formula list *)
-fun declarative_axioms_for_datatypes ext_ctxt ofs kk rel_table dtypes =
+(* extended_context -> int -> int Typtab.table -> kodkod_constrs
+ -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *)
+fun declarative_axioms_for_datatypes ext_ctxt bits ofs kk rel_table dtypes =
acyclicity_axioms_for_datatypes ext_ctxt kk rel_table dtypes @
- maps (other_axioms_for_datatype ext_ctxt ofs kk rel_table) dtypes
+ maps (other_axioms_for_datatype ext_ctxt bits ofs kk rel_table) dtypes
-(* int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
-fun kodkod_formula_from_nut ofs liberal
+(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula *)
+fun kodkod_formula_from_nut bits ofs liberal
(kk as {kk_all, kk_exist, kk_formula_let, kk_formula_if, kk_or, kk_not,
kk_iff, kk_implies, kk_and, kk_subset, kk_rel_eq, kk_no, kk_one,
kk_some, kk_rel_let, kk_rel_if, kk_union, kk_difference,
@@ -924,12 +974,12 @@
fun kk_notimplies f1 f2 = kk_and f1 (kk_not f2)
(* Kodkod.rel_expr -> Kodkod.rel_expr -> Kodkod.rel_expr *)
val kk_or3 =
- double_rel_let kk
+ double_rel_rel_let kk
(fn r1 => fn r2 =>
kk_rel_if (kk_subset true_atom (kk_union r1 r2)) true_atom
(kk_intersect r1 r2))
val kk_and3 =
- double_rel_let kk
+ double_rel_rel_let kk
(fn r1 => fn r2 =>
kk_rel_if (kk_subset false_atom (kk_union r1 r2)) false_atom
(kk_intersect r1 r2))
@@ -1031,7 +1081,7 @@
fold (kk_or o (kk_no o to_r)) opt_arg_us
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
else
- kk_no (kk_difference (to_rep min_R u1) (to_rep min_R u2))
+ kk_subset (to_rep min_R u1) (to_rep min_R u2)
end)
| Op2 (Eq, T, R, u1, u2) =>
(case min_rep (rep_of u1) (rep_of u2) of
@@ -1067,7 +1117,7 @@
kk_subset (kk_product r1 r2) Kodkod.Iden
else if not both_opt then
(r1, r2) |> is_opt_rep (rep_of u2) ? swap
- |> uncurry kk_difference |> kk_no
+ |-> kk_subset
else
raise SAME ()
else
@@ -1153,38 +1203,98 @@
| Cst (Iden, T, Func (Atom (1, j0), Formula Neut)) => Kodkod.Atom j0
| Cst (Iden, T as Type ("fun", [T1, _]), R as Func (R1, _)) =>
to_rep R (Cst (Iden, T, Func (one_rep ofs T1 R1, Formula Neut)))
- | Cst (Num j, @{typ int}, R) =>
- (case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
+ | Cst (Num j, T, R) =>
+ if is_word_type T then
+ atom_from_int_expr kk T R (Kodkod.Num j)
+ else if T = int_T then
+ case atom_for_int (card_of_rep R, offset_of_type ofs int_T) j of
~1 => if is_opt_rep R then Kodkod.None
else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
- | j' => Kodkod.Atom j')
- | Cst (Num j, T, R) =>
- if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
- else if is_opt_rep R then Kodkod.None
- else raise NUT ("Nitpick_Kodkod.to_r", [u])
+ | j' => Kodkod.Atom j'
+ else
+ if j < card_of_rep R then Kodkod.Atom (j + offset_of_type ofs T)
+ else if is_opt_rep R then Kodkod.None
+ else raise NUT ("Nitpick_Kodkod.to_r (Num)", [u])
| Cst (Unknown, _, R) => empty_rel_for_rep R
| Cst (Unrep, _, R) => empty_rel_for_rep R
| Cst (Suc, T, Func (Atom x, _)) =>
- if domain_type T <> nat_T then suc_rel
- else kk_intersect suc_rel (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
- | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => nat_add_rel
- | Cst (Add, Type ("fun", [@{typ int}, _]), _) => int_add_rel
- | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) => nat_subtract_rel
- | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) => int_subtract_rel
- | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) => nat_multiply_rel
- | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) => int_multiply_rel
- | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) => nat_divide_rel
- | Cst (Divide, Type ("fun", [@{typ int}, _]), _) => int_divide_rel
- | Cst (Modulo, Type ("fun", [@{typ nat}, _]), _) => nat_modulo_rel
- | Cst (Modulo, Type ("fun", [@{typ int}, _]), _) => int_modulo_rel
- | Cst (Gcd, _, _) => gcd_rel
- | Cst (Lcm, _, _) => lcm_rel
+ if domain_type T <> nat_T then
+ Kodkod.Rel suc_rel
+ else
+ kk_intersect (Kodkod.Rel suc_rel)
+ (kk_product Kodkod.Univ (Kodkod.AtomSeq x))
+ | Cst (Add, Type ("fun", [@{typ nat}, _]), _) => Kodkod.Rel nat_add_rel
+ | Cst (Add, Type ("fun", [@{typ int}, _]), _) => Kodkod.Rel int_add_rel
+ | Cst (Add, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ to_bit_word_binary_op T R NONE (SOME (curry Kodkod.Add))
+ | Cst (Add, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ to_bit_word_binary_op T R
+ (SOME (fn i1 => fn i2 => fn i3 =>
+ kk_implies (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i1, i2)))
+ (Kodkod.LE (Kodkod.Num 0, Kodkod.BitXor (i2, i3)))))
+ (SOME (curry Kodkod.Add))
+ | Cst (Subtract, Type ("fun", [@{typ nat}, _]), _) =>
+ Kodkod.Rel nat_subtract_rel
+ | Cst (Subtract, Type ("fun", [@{typ int}, _]), _) =>
+ Kodkod.Rel int_subtract_rel
+ | Cst (Subtract, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ to_bit_word_binary_op T R NONE
+ (SOME (fn i1 => fn i2 =>
+ Kodkod.IntIf (Kodkod.LE (i1, i2), Kodkod.Num 0,
+ Kodkod.Sub (i1, i2))))
+ | Cst (Subtract, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ to_bit_word_binary_op T R
+ (SOME (fn i1 => fn i2 => fn i3 =>
+ kk_implies (Kodkod.LT (Kodkod.BitXor (i1, i2), Kodkod.Num 0))
+ (Kodkod.LT (Kodkod.BitXor (i2, i3), Kodkod.Num 0))))
+ (SOME (curry Kodkod.Sub))
+ | Cst (Multiply, Type ("fun", [@{typ nat}, _]), _) =>
+ Kodkod.Rel nat_multiply_rel
+ | Cst (Multiply, Type ("fun", [@{typ int}, _]), _) =>
+ Kodkod.Rel int_multiply_rel
+ | Cst (Multiply,
+ T as Type ("fun", [Type (@{type_name word}, [bit_T]), _]), R) =>
+ to_bit_word_binary_op T R
+ (SOME (fn i1 => fn i2 => fn i3 =>
+ kk_or (Kodkod.IntEq (i2, Kodkod.Num 0))
+ (Kodkod.IntEq (Kodkod.Div (i3, i2), i1)
+ |> bit_T = @{typ signed_bit}
+ ? kk_and (Kodkod.LE (Kodkod.Num 0,
+ foldl1 Kodkod.BitAnd [i1, i2, i3])))))
+ (SOME (curry Kodkod.Mult))
+ | Cst (Divide, Type ("fun", [@{typ nat}, _]), _) =>
+ Kodkod.Rel nat_divide_rel
+ | Cst (Divide, Type ("fun", [@{typ int}, _]), _) =>
+ Kodkod.Rel int_divide_rel
+ | Cst (Divide, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ to_bit_word_binary_op T R NONE
+ (SOME (fn i1 => fn i2 =>
+ Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
+ Kodkod.Num 0, Kodkod.Div (i1, i2))))
+ | Cst (Divide, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ to_bit_word_binary_op T R
+ (SOME (fn i1 => fn i2 => fn i3 =>
+ Kodkod.LE (Kodkod.Num 0, foldl1 Kodkod.BitAnd [i1, i2, i3])))
+ (SOME (fn i1 => fn i2 =>
+ Kodkod.IntIf (kk_and (Kodkod.LT (i1, Kodkod.Num 0))
+ (Kodkod.LT (Kodkod.Num 0, i2)),
+ Kodkod.Sub (Kodkod.Div (Kodkod.Add (i1, Kodkod.Num 1), i2),
+ Kodkod.Num 1),
+ Kodkod.IntIf (kk_and (Kodkod.LT (Kodkod.Num 0, i1))
+ (Kodkod.LT (i2, Kodkod.Num 0)),
+ Kodkod.Sub (Kodkod.Div (Kodkod.Sub (i1, Kodkod.Num 1),
+ i2), Kodkod.Num 1),
+ Kodkod.IntIf (Kodkod.IntEq (i2, Kodkod.Num 0),
+ Kodkod.Num 0, Kodkod.Div (i1, i2))))))
+ | Cst (Gcd, _, _) => Kodkod.Rel gcd_rel
+ | Cst (Lcm, _, _) => Kodkod.Rel lcm_rel
| Cst (Fracs, _, Func (Atom (1, _), _)) => Kodkod.None
| Cst (Fracs, _, Func (Struct _, _)) =>
- kk_project_seq norm_frac_rel 2 2
- | Cst (NormFrac, _, _) => norm_frac_rel
- | Cst (NatToInt, _, Func (Atom _, Atom _)) => Kodkod.Iden
- | Cst (NatToInt, _,
+ kk_project_seq (Kodkod.Rel norm_frac_rel) 2 2
+ | Cst (NormFrac, _, _) => Kodkod.Rel norm_frac_rel
+ | Cst (NatToInt, Type ("fun", [@{typ nat}, _]), Func (Atom _, Atom _)) =>
+ Kodkod.Iden
+ | Cst (NatToInt, Type ("fun", [@{typ nat}, _]),
Func (Atom (nat_k, nat_j0), Opt (Atom (int_k, int_j0)))) =>
if nat_j0 = int_j0 then
kk_intersect Kodkod.Iden
@@ -1192,7 +1302,10 @@
Kodkod.Univ)
else
raise BAD ("Nitpick_Kodkod.to_r (NatToInt)", "\"nat_j0 <> int_j0\"")
- | Cst (IntToNat, _, Func (Atom (int_k, int_j0), nat_R)) =>
+ | Cst (NatToInt, T as Type ("fun", [@{typ "unsigned_bit word"}, _]), R) =>
+ to_bit_word_unary_op T R I
+ | Cst (IntToNat, Type ("fun", [@{typ int}, _]),
+ Func (Atom (int_k, int_j0), nat_R)) =>
let
val abs_card = max_int_for_card int_k + 1
val (nat_k, nat_j0) = the_single (atom_schema_of_rep nat_R)
@@ -1208,6 +1321,10 @@
else
raise BAD ("Nitpick_Kodkod.to_r (IntToNat)", "\"nat_j0 <> int_j0\"")
end
+ | Cst (IntToNat, T as Type ("fun", [@{typ "signed_bit word"}, _]), R) =>
+ to_bit_word_unary_op T R
+ (fn i => Kodkod.IntIf (Kodkod.LE (i, Kodkod.Num 0),
+ Kodkod.Num 0, i))
| Op1 (Not, _, R, u1) => kk_not3 (to_rep R u1)
| Op1 (Finite, _, Opt (Atom _), _) => Kodkod.None
| Op1 (Converse, T, R, u1) =>
@@ -1241,7 +1358,7 @@
val R' = rep_to_binary_rel_rep ofs T1 (unopt_rep (rep_of u1))
val R'' = opt_rep ofs T1 R'
in
- single_rel_let kk
+ single_rel_rel_let kk
(fn r =>
let
val true_r = kk_closure (kk_join r true_atom)
@@ -1266,7 +1383,7 @@
Func (R1, Formula Neut) => to_rep R1 u1
| Func (Unit, Opt R) => to_guard [u1] R true_atom
| Func (R1, R2 as Opt _) =>
- single_rel_let kk
+ single_rel_rel_let kk
(fn r => kk_rel_if (kk_no r) (empty_rel_for_rep R)
(rel_expr_to_func kk R1 bool_atom_R
(Func (R1, Formula Neut)) r))
@@ -1309,12 +1426,22 @@
if is_opt_rep (rep_of u1) then kk_rel_if (to_f u2) (to_r u1) false_atom
else kk_rel_if (to_f u1) (to_r u2) false_atom
| Op2 (Less, _, _, u1, u2) =>
- if type_of u1 = nat_T then
- if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
- else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
- else kk_nat_less (to_integer u1) (to_integer u2)
- else
- kk_int_less (to_integer u1) (to_integer u2)
+ (case type_of u1 of
+ @{typ nat} =>
+ if is_Cst Unrep u1 then to_compare_with_unrep u2 false_atom
+ else if is_Cst Unrep u2 then to_compare_with_unrep u1 true_atom
+ else kk_nat_less (to_integer u1) (to_integer u2)
+ | @{typ int} => kk_int_less (to_integer u1) (to_integer u2)
+ | _ => double_rel_rel_let kk
+ (fn r1 => fn r2 =>
+ kk_rel_if
+ (fold kk_and (map_filter (fn (u, r) =>
+ if is_opt_rep (rep_of u) then SOME (kk_some r)
+ else NONE) [(u1, r1), (u2, r2)]) Kodkod.True)
+ (atom_from_formula kk bool_j0 (Kodkod.LT (pairself
+ (int_expr_from_atom kk (type_of u1)) (r1, r2))))
+ Kodkod.None)
+ (to_r u1) (to_r u2))
| Op2 (The, T, R, u1, u2) =>
if is_opt_rep R then
let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
@@ -1468,7 +1595,7 @@
if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
Kodkod.Atom (offset_of_type ofs nat_T)
else
- fold kk_join [to_integer u1, to_integer u2] nat_subtract_rel
+ fold kk_join (map to_integer [u1, u2]) (Kodkod.Rel nat_subtract_rel)
| Op2 (Apply, _, R, u1, u2) =>
if is_Cst Unrep u2 andalso is_set_type (type_of u1)
andalso is_FreeName u1 then
@@ -1494,7 +1621,7 @@
kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
| Op3 (If, _, R, u1, u2, u3) =>
if is_opt_rep (rep_of u1) then
- triple_rel_let kk
+ tripl_rel_rel_let kk
(fn r1 => fn r2 => fn r3 =>
let val empty_r = empty_rel_for_rep R in
fold1 kk_union
@@ -1686,7 +1813,7 @@
| Func (_, Formula Neut) => set_oper r1 r2
| Func (Unit, _) => connective3 r1 r2
| Func (R1, _) =>
- double_rel_let kk
+ double_rel_rel_let kk
(fn r1 => fn r2 =>
kk_union
(kk_product
@@ -1702,6 +1829,43 @@
r1 r2
| _ => raise REP ("Nitpick_Kodkod.to_set_op", [min_R]))
end
+ (* typ -> rep -> (Kodkod.int_expr -> Kodkod.int_expr) -> Kodkod.rel_expr *)
+ and to_bit_word_unary_op T R oper =
+ let
+ val Ts = strip_type T ||> single |> op @
+ (* int -> Kodkod.int_expr *)
+ fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
+ in
+ kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
+ (Kodkod.FormulaLet
+ (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 1),
+ Kodkod.IntEq (Kodkod.IntReg 1, oper (Kodkod.IntReg 0))))
+ end
+ (* typ -> rep
+ -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr -> bool) option
+ -> (Kodkod.int_expr -> Kodkod.int_expr -> Kodkod.int_expr) option
+ -> Kodkod.rel_expr *)
+ and to_bit_word_binary_op T R opt_guard opt_oper =
+ let
+ val Ts = strip_type T ||> single |> op @
+ (* int -> Kodkod.int_expr *)
+ fun int_arg j = int_expr_from_atom kk (nth Ts j) (Kodkod.Var (1, j))
+ in
+ kk_comprehension (decls_for_atom_schema 0 (atom_schema_of_rep R))
+ (Kodkod.FormulaLet
+ (map (fn j => Kodkod.AssignIntReg (j, int_arg j)) (0 upto 2),
+ fold1 kk_and
+ ((case opt_guard of
+ NONE => []
+ | SOME guard =>
+ [guard (Kodkod.IntReg 0) (Kodkod.IntReg 1)
+ (Kodkod.IntReg 2)]) @
+ (case opt_oper of
+ NONE => []
+ | SOME oper =>
+ [Kodkod.IntEq (Kodkod.IntReg 2,
+ oper (Kodkod.IntReg 0) (Kodkod.IntReg 1))]))))
+ end
(* rep -> rep -> Kodkod.rel_expr -> nut -> Kodkod.rel_expr *)
and to_apply res_R func_u arg_u =
case unopt_rep (rep_of func_u) of
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Dec 17 15:22:27 2009 +0100
@@ -60,7 +60,7 @@
? prefix "\<^isub>,"
(* string -> typ -> int -> string *)
fun atom_name prefix (T as Type (s, _)) j =
- prefix ^ substring (short_name s, 0, 1) ^ atom_suffix s j
+ prefix ^ substring (shortest_name s, 0, 1) ^ atom_suffix s j
| atom_name prefix (T as TFree (s, _)) j =
prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s j
| atom_name _ T _ = raise TYPE ("Nitpick_Model.atom_name", [T], [])
@@ -71,24 +71,40 @@
else
Const (atom_name "" T j, T)
+(* term * term -> order *)
+fun nice_term_ord (Abs (_, _, t1), Abs (_, _, t2)) = nice_term_ord (t1, t2)
+ | nice_term_ord (t1, t2) =
+ int_ord (snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
+ handle TERM ("dest_number", _) =>
+ case (t1, t2) of
+ (t11 $ t12, t21 $ t22) =>
+ (case nice_term_ord (t11, t21) of
+ EQUAL => nice_term_ord (t12, t22)
+ | ord => ord)
+ | _ => TermOrd.term_ord (t1, t2)
+
(* nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list *)
fun tuple_list_for_name rel_table bounds name =
the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
(* term -> term *)
-fun unbox_term (Const (@{const_name FunBox}, _) $ t1) = unbox_term t1
- | unbox_term (Const (@{const_name PairBox},
- Type ("fun", [T1, Type ("fun", [T2, T3])])) $ t1 $ t2) =
- let val Ts = map unbox_type [T1, T2] in
+fun unbit_and_unbox_term (Const (@{const_name FunBox}, _) $ t1) =
+ unbit_and_unbox_term t1
+ | unbit_and_unbox_term (Const (@{const_name PairBox},
+ Type ("fun", [T1, Type ("fun", [T2, T3])]))
+ $ t1 $ t2) =
+ let val Ts = map unbit_and_unbox_type [T1, T2] in
Const (@{const_name Pair}, Ts ---> Type ("*", Ts))
- $ unbox_term t1 $ unbox_term t2
+ $ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
end
- | unbox_term (Const (s, T)) = Const (s, unbox_type T)
- | unbox_term (t1 $ t2) = unbox_term t1 $ unbox_term t2
- | unbox_term (Free (s, T)) = Free (s, unbox_type T)
- | unbox_term (Var (x, T)) = Var (x, unbox_type T)
- | unbox_term (Bound j) = Bound j
- | unbox_term (Abs (s, T, t')) = Abs (s, unbox_type T, unbox_term t')
+ | unbit_and_unbox_term (Const (s, T)) = Const (s, unbit_and_unbox_type T)
+ | unbit_and_unbox_term (t1 $ t2) =
+ unbit_and_unbox_term t1 $ unbit_and_unbox_term t2
+ | unbit_and_unbox_term (Free (s, T)) = Free (s, unbit_and_unbox_type T)
+ | unbit_and_unbox_term (Var (x, T)) = Var (x, unbit_and_unbox_type T)
+ | unbit_and_unbox_term (Bound j) = Bound j
+ | unbit_and_unbox_term (Abs (s, T, t')) =
+ Abs (s, unbit_and_unbox_type T, unbit_and_unbox_term t')
(* typ -> typ -> (typ * typ) * (typ * typ) *)
fun factor_out_types (T1 as Type ("*", [T11, T12]))
@@ -121,11 +137,12 @@
Const (if maybe_opt orelse T2 <> bool_T then @{const_name undefined}
else non_opt_name, T1 --> T2)
| aux T1 T2 ((t1, t2) :: ps) =
- Const (@{const_name fun_upd}, [T1 --> T2, T1, T2] ---> T1 --> T2)
+ Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
$ aux T1 T2 ps $ t1 $ t2
in aux T1 T2 o rev end
(* term -> bool *)
-fun is_plain_fun (Const (s, _)) = s mem [@{const_name undefined}, non_opt_name]
+fun is_plain_fun (Const (s, _)) =
+ (s = @{const_name undefined} orelse s = non_opt_name)
| is_plain_fun (Const (@{const_name fun_upd}, _) $ t0 $ _ $ _) =
is_plain_fun t0
| is_plain_fun _ = false
@@ -185,7 +202,7 @@
| do_arrow T1' T2' T1 T2
(Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) =
Const (@{const_name fun_upd},
- [T1' --> T2', T1', T2'] ---> T1' --> T2')
+ (T1' --> T2') --> T1' --> T2' --> T1' --> T2')
$ do_arrow T1' T2' T1 T2 t0 $ do_term T1' T1 t1 $ do_term T2' T2 t2
| do_arrow _ _ _ _ t =
raise TERM ("Nitpick_Model.typecast_fun.do_arrow", [t])
@@ -220,24 +237,34 @@
HOLogic.mk_prod (mk_tuple T1 ts,
mk_tuple T2 (List.drop (ts, length (HOLogic.flatten_tupleT T1))))
| mk_tuple _ (t :: _) = t
+ | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
(* string * string * string * string -> scope -> nut list -> nut list
-> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> typ -> typ
-> rep -> int list list -> term *)
fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
- ({ext_ctxt as {thy, ctxt, ...}, card_assigns, datatypes, ofs, ...}
+ ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
: scope) sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
+ (* int list list -> int *)
+ fun value_of_bits jss =
+ let
+ val j0 = offset_of_type ofs @{typ unsigned_bit}
+ val js = map (Integer.add (~ j0) o the_single) jss
+ in
+ fold (fn j => Integer.add (reasonable_power 2 j |> j = bits ? op ~))
+ js 0
+ end
(* bool -> typ -> typ -> (term * term) list -> term *)
fun make_set maybe_opt T1 T2 =
let
val empty_const = Const (@{const_name Set.empty}, T1 --> T2)
val insert_const = Const (@{const_name insert},
- [T1, T1 --> T2] ---> T1 --> T2)
+ T1 --> (T1 --> T2) --> T1 --> T2)
(* (term * term) list -> term *)
fun aux [] =
- if maybe_opt andalso not (is_precise_type datatypes T1) then
+ if maybe_opt andalso not (is_complete_type datatypes T1) then
insert_const $ Const (unrep, T1) $ empty_const
else
empty_const
@@ -253,7 +280,7 @@
fun make_map T1 T2 T2' =
let
val update_const = Const (@{const_name fun_upd},
- [T1 --> T2, T1, T2] ---> T1 --> T2)
+ (T1 --> T2) --> T1 --> T2 --> T1 --> T2)
(* (term * term) list -> term *)
fun aux' [] = Const (@{const_name Map.empty}, T1 --> T2)
| aux' ((t1, t2) :: ps) =
@@ -261,7 +288,7 @@
Const (@{const_name None}, _) => aux' ps
| _ => update_const $ aux' ps $ t1 $ t2)
fun aux ps =
- if not (is_precise_type datatypes T1) then
+ if not (is_complete_type datatypes T1) then
update_const $ aux' ps $ Const (unrep, T1)
$ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
else
@@ -299,8 +326,10 @@
fun make_fun maybe_opt T1 T2 T' ts1 ts2 =
ts1 ~~ ts2 |> T1 = @{typ bisim_iterator} ? rev
|> make_plain_fun (maybe_opt andalso not for_auto) T1 T2
- |> unbox_term
- |> typecast_fun (unbox_type T') (unbox_type T1) (unbox_type T2)
+ |> unbit_and_unbox_term
+ |> typecast_fun (unbit_and_unbox_type T')
+ (unbit_and_unbox_type T1)
+ (unbit_and_unbox_type T2)
(* (typ * int) list -> typ -> typ -> int -> term *)
fun term_for_atom seen (T as Type ("fun", [T1, T2])) T' j =
let
@@ -350,7 +379,8 @@
val real_j = j + offset_of_type ofs T
val constr_x as (constr_s, constr_T) =
get_first (fn (jss, {const, ...}) =>
- if [real_j] mem jss then SOME const else NONE)
+ if member (op =) jss [real_j] then SOME const
+ else NONE)
(discr_jsss ~~ constrs) |> the
val arg_Ts = curried_binder_types constr_T
val sel_xs = map (boxed_nth_sel_for_constr ext_ctxt constr_x)
@@ -369,8 +399,12 @@
else NONE)) sel_jsss
val uncur_arg_Ts = binder_types constr_T
in
- if co andalso (T, j) mem seen then
+ if co andalso member (op =) seen (T, j) then
Var (var ())
+ else if constr_s = @{const_name Word} then
+ HOLogic.mk_number
+ (if T = @{typ "unsigned_bit word"} then nat_T else int_T)
+ (value_of_bits (the_single arg_jsss))
else
let
val seen = seen |> co ? cons (T, j)
@@ -396,7 +430,7 @@
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
| n2 => Const (@{const_name HOL.divide},
- [num_T, num_T] ---> num_T)
+ num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
\for_atom (Abs_Frac)", ts)
@@ -408,10 +442,10 @@
in
if co then
let val var = var () in
- if exists_subterm (equal (Var var)) t then
+ if exists_subterm (curry (op =) (Var var)) t then
Const (@{const_name The}, (T --> bool_T) --> T)
$ Abs ("\<omega>", T,
- Const (@{const_name "op ="}, [T, T] ---> bool_T)
+ Const (@{const_name "op ="}, T --> T --> bool_T)
$ Bound 0 $ abstract_over (Var var, t))
else
t
@@ -449,7 +483,8 @@
val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
val ts2 =
map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
- [[int_for_bool (js mem jss)]]) jss1
+ [[int_for_bool (member (op =) jss js)]])
+ jss1
in make_fun false T1 T2 T' ts1 ts2 end
| term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
let
@@ -467,7 +502,8 @@
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
in
- (not for_auto ? setify_mapify_funs []) o unbox_term oooo term_for_rep []
+ (not for_auto ? setify_mapify_funs []) o unbit_and_unbox_term
+ oooo term_for_rep []
end
(* scope -> nut list -> nut NameTable.table -> Kodkod.raw_bound list -> nut
@@ -517,7 +553,7 @@
let
val ((head1, args1), (head2, args2)) =
pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
- val max_depth = max_depth - (if T mem coTs then 1 else 0)
+ val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
in
head1 = head2
andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
@@ -530,25 +566,26 @@
-> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
-> Pretty.T * bool *)
fun reconstruct_hol_model {show_skolems, show_datatypes, show_consts}
- ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, user_axioms, debug,
- wfs, destroy_constrs, specialize, skolemize,
- star_linear_preds, uncurry, fast_descrs, tac_timeout,
- evals, case_names, def_table, nondef_table, user_nondefs,
- simp_table, psimp_table, intro_table, ground_thm_table,
- ersatz_table, skolems, special_funs, unrolled_preds,
- wf_cache, constr_cache},
- card_assigns, bisim_depth, datatypes, ofs} : scope) formats all_frees
- free_names sel_names nonsel_names rel_table bounds =
+ ({ext_ctxt as {thy, ctxt, max_bisim_depth, boxes, wfs, user_axioms,
+ debug, binary_ints, destroy_constrs, specialize,
+ skolemize, star_linear_preds, uncurry, fast_descrs,
+ tac_timeout, evals, case_names, def_table, nondef_table,
+ user_nondefs, simp_table, psimp_table, intro_table,
+ ground_thm_table, ersatz_table, skolems, special_funs,
+ unrolled_preds, wf_cache, constr_cache},
+ card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
+ formats all_frees free_names sel_names nonsel_names rel_table bounds =
let
val (wacky_names as (_, base_name, step_name, _), ctxt) =
add_wacky_syntax ctxt
val ext_ctxt =
{thy = thy, ctxt = ctxt, max_bisim_depth = max_bisim_depth, boxes = boxes,
wfs = wfs, user_axioms = user_axioms, debug = debug,
- destroy_constrs = destroy_constrs, specialize = specialize,
- skolemize = skolemize, star_linear_preds = star_linear_preds,
- uncurry = uncurry, fast_descrs = fast_descrs, tac_timeout = tac_timeout,
- evals = evals, case_names = case_names, def_table = def_table,
+ binary_ints = binary_ints, destroy_constrs = destroy_constrs,
+ specialize = specialize, skolemize = skolemize,
+ star_linear_preds = star_linear_preds, uncurry = uncurry,
+ fast_descrs = fast_descrs, tac_timeout = tac_timeout, evals = evals,
+ case_names = case_names, def_table = def_table,
nondef_table = nondef_table, user_nondefs = user_nondefs,
simp_table = simp_table, psimp_table = psimp_table,
intro_table = intro_table, ground_thm_table = ground_thm_table,
@@ -556,17 +593,21 @@
special_funs = special_funs, unrolled_preds = unrolled_preds,
wf_cache = wf_cache, constr_cache = constr_cache}
val scope = {ext_ctxt = ext_ctxt, card_assigns = card_assigns,
- bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
+ bits = bits, bisim_depth = bisim_depth, datatypes = datatypes,
+ ofs = ofs}
(* typ -> typ -> rep -> int list list -> term *)
val term_for_rep = reconstruct_term wacky_names scope sel_names rel_table
bounds
- (* typ -> typ -> typ *)
- fun nth_value_of_type T card n = term_for_rep T T (Atom (card, 0)) [[n]]
+ (* nat -> typ -> nat -> typ *)
+ fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
+ (* nat -> typ -> typ list *)
+ fun all_values_of_type card T =
+ index_seq 0 card |> map (nth_value_of_type card T) |> sort nice_term_ord
(* dtype_spec list -> dtype_spec -> bool *)
fun is_codatatype_wellformed (cos : dtype_spec list)
({typ, card, ...} : dtype_spec) =
let
- val ts = map (nth_value_of_type typ card) (index_seq 0 card)
+ val ts = all_values_of_type card typ
val max_depth = Integer.sum (map #card cos)
in
forall (not o bisimilar_values (map #typ cos) max_depth)
@@ -578,7 +619,7 @@
val (oper, (t1, T'), T) =
case name of
FreeName (s, T, _) =>
- let val t = Free (s, unbox_type T) in
+ let val t = Free (s, unbit_and_unbox_type T) in
("=", (t, format_term_type thy def_table formats t), T)
end
| ConstName (s, T, _) =>
@@ -598,17 +639,16 @@
Pretty.str oper, Syntax.pretty_term ctxt t2])
end
(* dtype_spec -> Pretty.T *)
- fun pretty_for_datatype ({typ, card, precise, ...} : dtype_spec) =
+ fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
Pretty.block (Pretty.breaks
- [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=",
+ [Syntax.pretty_typ ctxt (unbit_and_unbox_type typ), Pretty.str "=",
Pretty.enum "," "{" "}"
- (map (Syntax.pretty_term ctxt o nth_value_of_type typ card)
- (index_seq 0 card) @
- (if precise then [] else [Pretty.str unrep]))])
+ (map (Syntax.pretty_term ctxt) (all_values_of_type card typ)
+ @ (if complete then [] else [Pretty.str unrep]))])
(* typ -> dtype_spec list *)
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
- precise = false, shallow = false, constrs = []}]
+ complete = false, concrete = true, shallow = false, constrs = []}]
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
datatypes |> filter_out #shallow
@@ -639,10 +679,12 @@
val (eval_names, noneval_nonskolem_nonsel_names) =
List.partition (String.isPrefix eval_prefix o nickname_of)
nonskolem_nonsel_names
- ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of)
+ ||> filter_out (curry (op =) @{const_name bisim_iterator_max}
+ o nickname_of)
val free_names =
map (fn x as (s, T) =>
- case filter (equal x o pairf nickname_of (unbox_type o type_of))
+ case filter (curry (op =) x
+ o pairf nickname_of (unbit_and_unbox_type o type_of))
free_names of
[name] => name
| [] => FreeName (s, T, Any)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Dec 17 15:22:27 2009 +0100
@@ -101,7 +101,7 @@
string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
| CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
| CType (s, []) =>
- if s mem [@{type_name prop}, @{type_name bool}] then "o" else s
+ if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
| CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
| CRec (s, _) => "[" ^ s ^ "]") ^
(if need_parens then ")" else "")
@@ -125,9 +125,10 @@
andalso exists (could_exist_alpha_subtype alpha_T) Ts)
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
(* theory -> typ -> typ -> bool *)
-fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) =
- could_exist_alpha_subtype alpha_T
- | could_exist_alpha_sub_ctype thy alpha_T = equal alpha_T orf is_datatype thy
+fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
+ could_exist_alpha_subtype alpha_T T
+ | could_exist_alpha_sub_ctype thy alpha_T T =
+ (T = alpha_T orelse is_datatype thy T)
(* ctype -> bool *)
fun exists_alpha_sub_ctype CAlpha = true
@@ -164,7 +165,7 @@
| repair_ctype cache seen (CRec (z as (s, _))) =
case AList.lookup (op =) cache z |> the of
CRec _ => CType (s, [])
- | C => if C mem seen then CType (s, [])
+ | C => if member (op =) seen C then CType (s, [])
else repair_ctype cache (C :: seen) C
(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
@@ -465,11 +466,11 @@
PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))
(* var -> (int -> bool option) -> literal list -> literal list *)
-fun literals_from_assignments max_var asgns lits =
+fun literals_from_assignments max_var assigns lits =
fold (fn x => fn accum =>
if AList.defined (op =) lits x then
accum
- else case asgns x of
+ else case assigns x of
SOME b => (x, sign_from_bool b) :: accum
| NONE => accum) (max_var downto 1) lits
@@ -490,7 +491,7 @@
(* literal list -> unit *)
fun print_solution lits =
- let val (pos, neg) = List.partition (equal Pos o snd) lits in
+ let val (pos, neg) = List.partition (curry (op =) Pos o snd) lits in
print_g ("*** Solution:\n" ^
"+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
"-: " ^ commas (map (string_for_var o fst) neg))
@@ -504,10 +505,13 @@
val prop = PropLogic.all (map prop_for_literal lits @
map prop_for_comp comps @
map prop_for_sign_expr sexps)
+ (* use the first ML solver (to avoid startup overhead) *)
+ val solvers = !SatSolver.solvers
+ |> filter (member (op =) ["dptsat", "dpll"] o fst)
in
- case SatSolver.invoke_solver "dpll" prop of
- SatSolver.SATISFIABLE asgns =>
- SOME (literals_from_assignments max_var asgns lits
+ case snd (hd solvers) prop of
+ SatSolver.SATISFIABLE assigns =>
+ SOME (literals_from_assignments max_var assigns lits
|> tap print_solution)
| _ => NONE
end
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Thu Dec 17 15:22:27 2009 +0100
@@ -26,7 +26,6 @@
Subtract |
Multiply |
Divide |
- Modulo |
Gcd |
Lcm |
Fracs |
@@ -144,7 +143,6 @@
Subtract |
Multiply |
Divide |
- Modulo |
Gcd |
Lcm |
Fracs |
@@ -218,7 +216,6 @@
| string_for_cst Subtract = "Subtract"
| string_for_cst Multiply = "Multiply"
| string_for_cst Divide = "Divide"
- | string_for_cst Modulo = "Modulo"
| string_for_cst Gcd = "Gcd"
| string_for_cst Lcm = "Lcm"
| string_for_cst Fracs = "Fracs"
@@ -614,8 +611,6 @@
Cst (Multiply, T, Any)
| (Const (@{const_name div_nat_inst.div_nat}, T), []) =>
Cst (Divide, T, Any)
- | (Const (@{const_name div_nat_inst.mod_nat}, T), []) =>
- Cst (Modulo, T, Any)
| (Const (@{const_name ord_nat_inst.less_nat}, T), [t1, t2]) =>
Op2 (Less, bool_T, Any, sub t1, sub t2)
| (Const (@{const_name ord_nat_inst.less_eq_nat}, T), [t1, t2]) =>
@@ -634,12 +629,12 @@
Cst (Multiply, T, Any)
| (Const (@{const_name div_int_inst.div_int}, T), []) =>
Cst (Divide, T, Any)
- | (Const (@{const_name div_int_inst.mod_int}, T), []) =>
- Cst (Modulo, T, Any)
| (Const (@{const_name uminus_int_inst.uminus_int}, T), []) =>
- Op2 (Apply, int_T --> int_T, Any,
- Cst (Subtract, [int_T, int_T] ---> int_T, Any),
- Cst (Num 0, int_T, Any))
+ let val num_T = domain_type T in
+ Op2 (Apply, num_T --> num_T, Any,
+ Cst (Subtract, num_T --> num_T --> num_T, Any),
+ Cst (Num 0, num_T, Any))
+ end
| (Const (@{const_name ord_int_inst.less_int}, T), [t1, t2]) =>
Op2 (Less, bool_T, Any, sub t1, sub t2)
| (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
@@ -650,6 +645,9 @@
| (Const (@{const_name norm_frac}, T), []) => Cst (NormFrac, T, Any)
| (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
Cst (NatToInt, T, Any)
+ | (Const (@{const_name of_nat},
+ T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
+ Cst (NatToInt, T, Any)
| (Const (@{const_name lower_semilattice_fun_inst.inf_fun}, T),
[t1, t2]) =>
Op2 (Intersect, nth_range_type 2 T, Any, sub t1, sub t2)
@@ -708,24 +706,24 @@
(* scope -> bool -> nut -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
- ofs, ...}) all_precise v (vs, table) =
+ ofs, ...}) all_exact v (vs, table) =
let
val x as (s, T) = (nickname_of v, type_of v)
val R = (if is_abs_fun thy x then
rep_for_abs_fun
else if is_rep_fun thy x then
Func oo best_non_opt_symmetric_reps_for_fun_type
- else if all_precise orelse is_skolem_name v
- orelse original_name s
- mem [@{const_name undefined_fast_The},
- @{const_name undefined_fast_Eps},
- @{const_name bisim},
- @{const_name bisim_iterator_max}] then
+ else if all_exact orelse is_skolem_name v
+ orelse member (op =) [@{const_name undefined_fast_The},
+ @{const_name undefined_fast_Eps},
+ @{const_name bisim},
+ @{const_name bisim_iterator_max}]
+ (original_name s) then
best_non_opt_set_rep_for_type
- else if original_name s
- mem [@{const_name set}, @{const_name distinct},
- @{const_name ord_class.less},
- @{const_name ord_class.less_eq}] then
+ else if member (op =) [@{const_name set}, @{const_name distinct},
+ @{const_name ord_class.less},
+ @{const_name ord_class.less_eq}]
+ (original_name s) then
best_set_rep_for_type
else
best_opt_set_rep_for_type) scope T
@@ -737,17 +735,19 @@
fold (choose_rep_for_free_var scope) vs ([], table)
(* scope -> bool -> nut list -> rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_reps_for_consts scope all_precise vs table =
- fold (choose_rep_for_const scope all_precise) vs ([], table)
+fun choose_reps_for_consts scope all_exact vs table =
+ fold (choose_rep_for_const scope all_exact) vs ([], table)
(* scope -> styp -> int -> nut list * rep NameTable.table
-> nut list * rep NameTable.table *)
-fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) x n
+fun choose_rep_for_nth_sel_for_constr (scope as {ext_ctxt, ...}) (x as (_, T)) n
(vs, table) =
let
val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
- val R' = if n = ~1 then best_non_opt_set_rep_for_type scope T'
- else best_opt_set_rep_for_type scope T' |> unopt_rep
+ val R' = if n = ~1 orelse is_word_type (body_type T) then
+ best_non_opt_set_rep_for_type scope T'
+ else
+ best_opt_set_rep_for_type scope T' |> unopt_rep
val v = ConstName (s', T', R')
in (v :: vs, NameTable.update (v, R') table) end
(* scope -> styp -> nut list * rep NameTable.table
@@ -780,7 +780,8 @@
(not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
case u of
Cst (Num _, _, _) => true
- | Cst (cst, T, _) => cst = Suc orelse (body_type T = nat_T andalso cst = Add)
+ | Cst (cst, T, _) =>
+ cst = Suc orelse (body_type T = nat_T andalso cst = Add)
| Op2 (Apply, _, _, u1, u2) => forall is_constructive [u1, u2]
| Op3 (If, _, _, u1, u2, u3) =>
not (is_opt_rep (rep_of u1)) andalso forall is_constructive [u2, u3]
@@ -883,7 +884,8 @@
(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
fun choose_reps_in_nut (scope as {ext_ctxt as {thy, ctxt, ...}, card_assigns,
- datatypes, ofs, ...}) liberal table def =
+ bits, datatypes, ofs, ...})
+ liberal table def =
let
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
(* polarity -> bool -> rep *)
@@ -912,17 +914,23 @@
Cst (False, T, _) => Cst (False, T, Formula Neut)
| Cst (True, T, _) => Cst (True, T, Formula Neut)
| Cst (Num j, T, _) =>
- (case spec_of_type scope T of
- (1, j0) => if j = 0 then Cst (Unity, T, Unit)
- else Cst (Unrep, T, Opt (Atom (1, j0)))
- | (k, j0) =>
- let
- val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
- else j < k)
- in
- if ok then Cst (Num j, T, Atom (k, j0))
- else Cst (Unrep, T, Opt (Atom (k, j0)))
- end)
+ if is_word_type T then
+ if is_twos_complement_representable bits j then
+ Cst (Num j, T, best_non_opt_set_rep_for_type scope T)
+ else
+ Cst (Unrep, T, best_opt_set_rep_for_type scope T)
+ else
+ (case spec_of_type scope T of
+ (1, j0) => if j = 0 then Cst (Unity, T, Unit)
+ else Cst (Unrep, T, Opt (Atom (1, j0)))
+ | (k, j0) =>
+ let
+ val ok = (if T = int_T then atom_for_int (k, j0) j <> ~1
+ else j < k)
+ in
+ if ok then Cst (Num j, T, Atom (k, j0))
+ else Cst (Unrep, T, Opt (Atom (k, j0)))
+ end)
| Cst (Suc, T as Type ("fun", [T1, _]), _) =>
let val R = Atom (spec_of_type scope T1) in
Cst (Suc, T, Func (R, Opt R))
@@ -934,35 +942,32 @@
Cst (NormFrac, T, Func (R1, Func (R1, Opt (Struct [R1, R1]))))
end
| Cst (cst, T, _) =>
- if cst mem [Unknown, Unrep] then
+ if cst = Unknown orelse cst = Unrep then
case (is_boolean_type T, polar) of
(true, Pos) => Cst (False, T, Formula Pos)
| (true, Neg) => Cst (True, T, Formula Neg)
| _ => Cst (cst, T, best_opt_set_rep_for_type scope T)
- else if cst mem [Add, Subtract, Multiply, Divide, Modulo, Gcd,
- Lcm] then
+ else if member (op =) [Add, Subtract, Multiply, Divide, Gcd, Lcm]
+ cst then
let
val T1 = domain_type T
val R1 = Atom (spec_of_type scope T1)
- val total =
- T1 = nat_T andalso cst mem [Subtract, Divide, Modulo, Gcd]
+ val total = T1 = nat_T
+ andalso (cst = Subtract orelse cst = Divide
+ orelse cst = Gcd)
in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
- else if cst mem [NatToInt, IntToNat] then
+ else if cst = NatToInt orelse cst = IntToNat then
let
- val (nat_card, nat_j0) = spec_of_type scope nat_T
- val (int_card, int_j0) = spec_of_type scope int_T
+ val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
+ val (ran_card, ran_j0) = spec_of_type scope (range_type T)
+ val total = not (is_word_type (domain_type T))
+ andalso (if cst = NatToInt then
+ max_int_for_card ran_card >= dom_card + 1
+ else
+ max_int_for_card dom_card < ran_card)
in
- if cst = NatToInt then
- let val total = (max_int_for_card int_card >= nat_card + 1) in
- Cst (cst, T,
- Func (Atom (nat_card, nat_j0),
- (not total ? Opt) (Atom (int_card, int_j0))))
- end
- else
- let val total = (max_int_for_card int_card < nat_card) in
- Cst (cst, T, Func (Atom (int_card, int_j0),
- Atom (nat_card, nat_j0)) |> not total ? Opt)
- end
+ Cst (cst, T, Func (Atom (dom_card, dom_j0),
+ Atom (ran_card, ran_j0) |> not total ? Opt))
end
else
Cst (cst, T, best_set_rep_for_type scope T)
@@ -997,7 +1002,7 @@
if is_opt_rep R then
triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
else if opt andalso polar = Pos andalso
- not (is_fully_comparable_type datatypes (type_of u1)) then
+ not (is_concrete_type datatypes (type_of u1)) then
Cst (False, T, Formula Pos)
else
s_op2 Subset T R u1 u2
@@ -1023,7 +1028,7 @@
else opt_opt_case ()
in
if liberal orelse polar = Neg
- orelse is_fully_comparable_type datatypes (type_of u1) then
+ orelse is_concrete_type datatypes (type_of u1) then
case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
(true, true) => opt_opt_case ()
| (true, false) => hybrid_case u1'
@@ -1113,7 +1118,7 @@
in s_op2 Lambda T R u1' u2' end
| R => raise NUT ("Nitpick_Nut.aux.choose_reps_in_nut", [u]))
| Op2 (oper, T, _, u1, u2) =>
- if oper mem [All, Exist] then
+ if oper = All orelse oper = Exist then
let
val table' = fold (choose_rep_for_bound_var scope) (untuple I u1)
table
@@ -1126,7 +1131,7 @@
let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
if def
orelse (liberal andalso (polar = Pos) = (oper = All))
- orelse is_precise_type datatypes (type_of u1) then
+ orelse is_complete_type datatypes (type_of u1) then
quant_u
else
let
@@ -1140,7 +1145,7 @@
end
end
end
- else if oper mem [Or, And] then
+ else if oper = Or orelse oper = And then
let
val u1' = gsub def polar u1
val u2' = gsub def polar u2
@@ -1159,7 +1164,7 @@
raise SAME ())
handle SAME () => s_op2 oper T (Formula polar) u1' u2'
end
- else if oper mem [The, Eps] then
+ else if oper = The orelse oper = Eps then
let
val u1' = sub u1
val opt1 = is_opt_rep (rep_of u1')
@@ -1169,7 +1174,7 @@
else unopt_R |> opt ? opt_rep ofs T
val u = Op2 (oper, T, R, u1', sub u2)
in
- if is_precise_type datatypes T orelse not opt1 then
+ if is_complete_type datatypes T orelse not opt1 then
u
else
let
@@ -1210,7 +1215,7 @@
let
val Rs = map (best_one_rep_for_type scope o type_of) us
val us = map sub us
- val R = if forall (equal Unit) Rs then Unit else Struct Rs
+ val R = if forall (curry (op =) Unit) Rs then Unit else Struct Rs
val R' = (exists (is_opt_rep o rep_of) us ? opt_rep ofs T) R
in s_tuple T R' us end
| Construct (us', T, _, us) =>
@@ -1312,7 +1317,18 @@
in (ws' @ ws, pool, NameTable.update (v, shape_tuple T R ws') table) end
else
let
- val (j, pool) = fresh arity pool
+ val (j, pool) =
+ case v of
+ ConstName _ =>
+ if is_sel_like_and_no_discr nick then
+ case domain_type T of
+ @{typ "unsigned_bit word"} =>
+ (snd unsigned_bit_word_sel_rel, pool)
+ | @{typ "signed_bit word"} => (snd signed_bit_word_sel_rel, pool)
+ | _ => fresh arity pool
+ else
+ fresh arity pool
+ | _ => fresh arity pool
val w = constr ((arity, j), T, R, nick)
in (w :: ws, pool, NameTable.update (v, w) table) end
end
@@ -1331,7 +1347,7 @@
Cst _ => u
| Op1 (oper, T, R, u1) => Op1 (oper, T, R, rename_vars_in_nut pool table u1)
| Op2 (oper, T, R, u1, u2) =>
- if oper mem [All, Exist, Lambda] then
+ if oper = All orelse oper = Exist orelse oper = Lambda then
let
val (_, pool, table) = fold (rename_n_ary_var false) (untuple I u1)
([], pool, table)
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Thu Dec 17 15:22:27 2009 +0100
@@ -7,6 +7,7 @@
signature NITPICK_PEEPHOLE =
sig
+ type n_ary_index = Kodkod.n_ary_index
type formula = Kodkod.formula
type int_expr = Kodkod.int_expr
type rel_expr = Kodkod.rel_expr
@@ -14,29 +15,29 @@
type expr_assign = Kodkod.expr_assign
type name_pool = {
- rels: Kodkod.n_ary_index list,
- vars: Kodkod.n_ary_index list,
+ rels: n_ary_index list,
+ vars: n_ary_index list,
formula_reg: int,
rel_reg: int}
val initial_pool : name_pool
- val not3_rel : rel_expr
- val suc_rel : rel_expr
- val nat_add_rel : rel_expr
- val int_add_rel : rel_expr
- val nat_subtract_rel : rel_expr
- val int_subtract_rel : rel_expr
- val nat_multiply_rel : rel_expr
- val int_multiply_rel : rel_expr
- val nat_divide_rel : rel_expr
- val int_divide_rel : rel_expr
- val nat_modulo_rel : rel_expr
- val int_modulo_rel : rel_expr
- val nat_less_rel : rel_expr
- val int_less_rel : rel_expr
- val gcd_rel : rel_expr
- val lcm_rel : rel_expr
- val norm_frac_rel : rel_expr
+ val not3_rel : n_ary_index
+ val suc_rel : n_ary_index
+ val unsigned_bit_word_sel_rel : n_ary_index
+ val signed_bit_word_sel_rel : n_ary_index
+ val nat_add_rel : n_ary_index
+ val int_add_rel : n_ary_index
+ val nat_subtract_rel : n_ary_index
+ val int_subtract_rel : n_ary_index
+ val nat_multiply_rel : n_ary_index
+ val int_multiply_rel : n_ary_index
+ val nat_divide_rel : n_ary_index
+ val int_divide_rel : n_ary_index
+ val nat_less_rel : n_ary_index
+ val int_less_rel : n_ary_index
+ val gcd_rel : n_ary_index
+ val lcm_rel : n_ary_index
+ val norm_frac_rel : n_ary_index
val atom_for_bool : int -> bool -> rel_expr
val formula_for_bool : bool -> formula
val atom_for_nat : int * int -> int -> int
@@ -44,6 +45,7 @@
val max_int_for_card : int -> int
val int_for_atom : int * int -> int -> int
val atom_for_int : int * int -> int -> int
+ val is_twos_complement_representable : int -> int -> bool
val inline_rel_expr : rel_expr -> bool
val empty_n_ary_rel : int -> rel_expr
val num_seq : int -> int -> int_expr list
@@ -105,23 +107,23 @@
{rels = [(2, 10), (3, 20), (4, 10)], vars = [], formula_reg = 10,
rel_reg = 10}
-val not3_rel = Rel (2, 0)
-val suc_rel = Rel (2, 1)
-val nat_add_rel = Rel (3, 0)
-val int_add_rel = Rel (3, 1)
-val nat_subtract_rel = Rel (3, 2)
-val int_subtract_rel = Rel (3, 3)
-val nat_multiply_rel = Rel (3, 4)
-val int_multiply_rel = Rel (3, 5)
-val nat_divide_rel = Rel (3, 6)
-val int_divide_rel = Rel (3, 7)
-val nat_modulo_rel = Rel (3, 8)
-val int_modulo_rel = Rel (3, 9)
-val nat_less_rel = Rel (3, 10)
-val int_less_rel = Rel (3, 11)
-val gcd_rel = Rel (3, 12)
-val lcm_rel = Rel (3, 13)
-val norm_frac_rel = Rel (4, 0)
+val not3_rel = (2, 0)
+val suc_rel = (2, 1)
+val unsigned_bit_word_sel_rel = (2, 2)
+val signed_bit_word_sel_rel = (2, 3)
+val nat_add_rel = (3, 0)
+val int_add_rel = (3, 1)
+val nat_subtract_rel = (3, 2)
+val int_subtract_rel = (3, 3)
+val nat_multiply_rel = (3, 4)
+val int_multiply_rel = (3, 5)
+val nat_divide_rel = (3, 6)
+val int_divide_rel = (3, 7)
+val nat_less_rel = (3, 8)
+val int_less_rel = (3, 9)
+val gcd_rel = (3, 10)
+val lcm_rel = (3, 11)
+val norm_frac_rel = (4, 0)
(* int -> bool -> rel_expr *)
fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
@@ -140,6 +142,9 @@
if n < min_int_for_card k orelse n > max_int_for_card k then ~1
else if n < 0 then n + k + j0
else n + j0
+(* int -> int -> bool *)
+fun is_twos_complement_representable bits n =
+ let val max = reasonable_power 2 bits in n >= ~ max andalso n < max end
(* rel_expr -> bool *)
fun is_none_product (Product (r1, r2)) =
@@ -365,16 +370,28 @@
(* rel_expr -> rel_expr *)
fun s_not3 (Atom j) = Atom (if j = main_j0 then j + 1 else j - 1)
| s_not3 (r as Join (r1, r2)) =
- if r2 = not3_rel then r1 else Join (r, not3_rel)
- | s_not3 r = Join (r, not3_rel)
+ if r2 = Rel not3_rel then r1 else Join (r, Rel not3_rel)
+ | s_not3 r = Join (r, Rel not3_rel)
(* rel_expr -> rel_expr -> formula *)
fun s_rel_eq r1 r2 =
(case (r1, r2) of
- (Join (r11, r12), _) =>
- if r12 = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
- | (_, Join (r21, r22)) =>
- if r22 = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
+ (Join (r11, Rel x), _) =>
+ if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
+ | (_, Join (r21, Rel x)) =>
+ if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
+ | (RelIf (f, r11, r12), _) =>
+ if inline_rel_expr r2 then
+ s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
+ else
+ raise SAME ()
+ | (_, RelIf (f, r21, r22)) =>
+ if inline_rel_expr r1 then
+ s_formula_if f (s_rel_eq r1 r21) (s_rel_eq r1 r22)
+ else
+ raise SAME ()
+ | (RelLet (bs, r1'), Atom _) => s_formula_let bs (s_rel_eq r1' r2)
+ | (Atom _, RelLet (bs, r2')) => s_formula_let bs (s_rel_eq r1 r2')
| _ => raise SAME ())
handle SAME () =>
case rel_expr_equal r1 r2 of
@@ -499,8 +516,8 @@
| s_join (r1 as RelIf (f, r11, r12)) r2 =
if inline_rel_expr r2 then s_rel_if f (s_join r11 r2) (s_join r12 r2)
else Join (r1, r2)
- | s_join (r1 as Atom j1) (r2 as Rel (2, j2)) =
- if r2 = suc_rel then
+ | s_join (r1 as Atom j1) (r2 as Rel (x as (2, j2))) =
+ if x = suc_rel then
let val n = to_nat j1 + 1 in
if n < nat_card then from_nat n else None
end
@@ -511,8 +528,8 @@
s_project (s_join r21 r1) is
else
Join (r1, r2)
- | s_join r1 (Join (r21, r22 as Rel (3, j22))) =
- ((if r22 = nat_add_rel then
+ | s_join r1 (Join (r21, r22 as Rel (x as (3, j22)))) =
+ ((if x = nat_add_rel then
case (r21, r1) of
(Atom j1, Atom j2) =>
let val n = to_nat j1 + to_nat j2 in
@@ -521,19 +538,19 @@
| (Atom j, r) =>
(case to_nat j of
0 => r
- | 1 => s_join r suc_rel
+ | 1 => s_join r (Rel suc_rel)
| _ => raise SAME ())
| (r, Atom j) =>
(case to_nat j of
0 => r
- | 1 => s_join r suc_rel
+ | 1 => s_join r (Rel suc_rel)
| _ => raise SAME ())
| _ => raise SAME ()
- else if r22 = nat_subtract_rel then
+ else if x = nat_subtract_rel then
case (r21, r1) of
(Atom j1, Atom j2) => from_nat (nat_minus (to_nat j1) (to_nat j2))
| _ => raise SAME ()
- else if r22 = nat_multiply_rel then
+ else if x = nat_multiply_rel then
case (r21, r1) of
(Atom j1, Atom j2) =>
let val n = to_nat j1 * to_nat j2 in
@@ -596,20 +613,20 @@
in aux (arity_of_rel_expr r) r end
(* rel_expr -> rel_expr -> rel_expr *)
- fun s_nat_subtract r1 r2 = fold s_join [r1, r2] nat_subtract_rel
+ fun s_nat_subtract r1 r2 = fold s_join [r1, r2] (Rel nat_subtract_rel)
fun s_nat_less (Atom j1) (Atom j2) = from_bool (j1 < j2)
- | s_nat_less r1 r2 = fold s_join [r1, r2] nat_less_rel
+ | s_nat_less r1 r2 = fold s_join [r1, r2] (Rel nat_less_rel)
fun s_int_less (Atom j1) (Atom j2) = from_bool (to_int j1 < to_int j2)
- | s_int_less r1 r2 = fold s_join [r1, r2] int_less_rel
+ | s_int_less r1 r2 = fold s_join [r1, r2] (Rel int_less_rel)
(* rel_expr -> int -> int -> rel_expr *)
fun d_project_seq r j0 n = Project (r, num_seq j0 n)
(* rel_expr -> rel_expr *)
- fun d_not3 r = Join (r, not3_rel)
+ fun d_not3 r = Join (r, Rel not3_rel)
(* rel_expr -> rel_expr -> rel_expr *)
- fun d_nat_subtract r1 r2 = List.foldl Join nat_subtract_rel [r1, r2]
- fun d_nat_less r1 r2 = List.foldl Join nat_less_rel [r1, r2]
- fun d_int_less r1 r2 = List.foldl Join int_less_rel [r1, r2]
+ fun d_nat_subtract r1 r2 = List.foldl Join (Rel nat_subtract_rel) [r1, r2]
+ fun d_nat_less r1 r2 = List.foldl Join (Rel nat_less_rel) [r1, r2]
+ fun d_int_less r1 r2 = List.foldl Join (Rel int_less_rel) [r1, r2]
in
if optim then
{kk_all = s_all, kk_exist = s_exist, kk_formula_let = s_formula_let,
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Thu Dec 17 15:22:27 2009 +0100
@@ -299,7 +299,7 @@
| z => Func z)
| best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
fun best_set_rep_for_type (scope as {datatypes, ...}) T =
- (if is_precise_type datatypes T then best_non_opt_set_rep_for_type
+ (if is_exact_type datatypes T then best_non_opt_set_rep_for_type
else best_opt_set_rep_for_type) scope T
fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
(Type ("fun", [T1, T2])) =
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Dec 17 15:22:27 2009 +0100
@@ -22,21 +22,24 @@
typ: typ,
card: int,
co: bool,
- precise: bool,
+ complete: bool,
+ concrete: bool,
shallow: bool,
constrs: constr_spec list}
type scope = {
ext_ctxt: extended_context,
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
- val is_precise_type : dtype_spec list -> typ -> bool
- val is_fully_comparable_type : dtype_spec list -> typ -> bool
+ val is_complete_type : dtype_spec list -> typ -> bool
+ val is_concrete_type : dtype_spec list -> typ -> bool
+ val is_exact_type : dtype_spec list -> typ -> bool
val offset_of_type : int Typtab.table -> typ -> int
val spec_of_type : scope -> typ -> int * int
val pretties_for_scope : scope -> bool -> Pretty.T list
@@ -46,7 +49,8 @@
val all_scopes :
extended_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list
- -> int list -> typ list -> typ list -> typ list -> int * scope list
+ -> int list -> int list -> typ list -> typ list -> typ list
+ -> int * scope list
end;
structure Nitpick_Scope : NITPICK_SCOPE =
@@ -67,13 +71,15 @@
typ: typ,
card: int,
co: bool,
- precise: bool,
+ complete: bool,
+ concrete: bool,
shallow: bool,
constrs: constr_spec list}
type scope = {
ext_ctxt: extended_context,
card_assigns: (typ * int) list,
+ bits: int,
bisim_depth: int,
datatypes: dtype_spec list,
ofs: int Typtab.table}
@@ -85,28 +91,32 @@
(* dtype_spec list -> typ -> dtype_spec option *)
fun datatype_spec (dtypes : dtype_spec list) T =
- List.find (equal T o #typ) dtypes
+ List.find (curry (op =) T o #typ) dtypes
(* dtype_spec list -> styp -> constr_spec *)
fun constr_spec [] x = raise TERM ("Nitpick_Scope.constr_spec", [Const x])
| constr_spec ({constrs, ...} :: dtypes : dtype_spec list) (x as (s, T)) =
- case List.find (equal (s, body_type T) o (apsnd body_type o #const))
+ case List.find (curry (op =) (s, body_type T) o (apsnd body_type o #const))
constrs of
SOME c => c
| NONE => constr_spec dtypes x
(* dtype_spec list -> typ -> bool *)
-fun is_precise_type dtypes (Type ("fun", Ts)) =
- forall (is_precise_type dtypes) Ts
- | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts
- | is_precise_type dtypes T =
- not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T))
+fun is_complete_type dtypes (Type ("fun", [T1, T2])) =
+ is_concrete_type dtypes T1 andalso is_complete_type dtypes T2
+ | is_complete_type dtypes (Type ("*", Ts)) =
+ forall (is_complete_type dtypes) Ts
+ | is_complete_type dtypes T =
+ not (is_integer_type T) andalso not (is_bit_type T)
+ andalso #complete (the (datatype_spec dtypes T))
handle Option.Option => true
-fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) =
- is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2
- | is_fully_comparable_type dtypes (Type ("*", Ts)) =
- forall (is_fully_comparable_type dtypes) Ts
- | is_fully_comparable_type _ _ = true
+and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
+ is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
+ | is_concrete_type dtypes (Type ("*", Ts)) =
+ forall (is_concrete_type dtypes) Ts
+ | is_concrete_type dtypes T =
+ #concrete (the (datatype_spec dtypes T)) handle Option.Option => true
+fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes
(* int Typtab.table -> typ -> int *)
fun offset_of_type ofs T =
@@ -122,13 +132,16 @@
(* (string -> string) -> scope
-> string list * string list * string list * string list * string list *)
fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
- bisim_depth, datatypes, ...} : scope) =
+ bits, bisim_depth, datatypes, ...} : scope) =
let
- val (iter_asgns, card_asgns) =
- card_assigns |> filter_out (equal @{typ bisim_iterator} o fst)
+ val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
+ @{typ bisim_iterator}]
+ val (iter_assigns, card_assigns) =
+ card_assigns |> filter_out (member (op =) boring_Ts o fst)
|> List.partition (is_fp_iterator_type o fst)
- val (unimportant_card_asgns, important_card_asgns) =
- card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
+ val (secondary_card_assigns, primary_card_assigns) =
+ card_assigns |> List.partition ((is_integer_type orf is_datatype thy)
+ o fst)
val cards =
map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
string_of_int k)
@@ -145,24 +158,25 @@
map (fn (T, k) =>
quote (Syntax.string_of_term ctxt
(Const (const_for_iterator_type T))) ^ " = " ^
- string_of_int (k - 1)) iter_asgns
- fun bisims () =
- if bisim_depth < 0 andalso forall (not o #co) datatypes then []
- else ["bisim_depth = " ^ string_of_int bisim_depth]
+ string_of_int (k - 1)) iter_assigns
+ fun miscs () =
+ (if bits = 0 then [] else ["bits = " ^ string_of_int bits]) @
+ (if bisim_depth < 0 andalso forall (not o #co) datatypes then []
+ else ["bisim_depth = " ^ string_of_int bisim_depth])
in
setmp_show_all_types
- (fn () => (cards important_card_asgns, cards unimportant_card_asgns,
- maxes (), iters (), bisims ())) ()
+ (fn () => (cards primary_card_assigns, cards secondary_card_assigns,
+ maxes (), iters (), miscs ())) ()
end
(* scope -> bool -> Pretty.T list *)
fun pretties_for_scope scope verbose =
let
- val (important_cards, unimportant_cards, maxes, iters, bisim_depths) =
+ val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
quintuple_for_scope maybe_quote scope
- val ss = map (prefix "card ") important_cards @
+ val ss = map (prefix "card ") primary_cards @
(if verbose then
- map (prefix "card ") unimportant_cards @
+ map (prefix "card ") secondary_cards @
map (prefix "max ") maxes @
map (prefix "iter ") iters @
bisim_depths
@@ -176,9 +190,9 @@
(* scope -> string *)
fun multiline_string_for_scope scope =
let
- val (important_cards, unimportant_cards, maxes, iters, bisim_depths) =
+ val (primary_cards, secondary_cards, maxes, iters, bisim_depths) =
quintuple_for_scope I scope
- val cards = important_cards @ unimportant_cards
+ val cards = primary_cards @ secondary_cards
in
case (if null cards then [] else ["card: " ^ commas cards]) @
(if null maxes then [] else ["max: " ^ commas maxes]) @
@@ -204,52 +218,58 @@
fun project_block (column, block) = map (project_row column) block
(* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *)
-fun lookup_ints_assign eq asgns key =
- case triple_lookup eq asgns key of
+fun lookup_ints_assign eq assigns key =
+ case triple_lookup eq assigns key of
SOME ks => ks
| NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
(* theory -> (typ option * int list) list -> typ -> int list *)
-fun lookup_type_ints_assign thy asgns T =
- map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T)
+fun lookup_type_ints_assign thy assigns T =
+ map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T)
handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
(* theory -> (styp option * int list) list -> styp -> int list *)
-fun lookup_const_ints_assign thy asgns x =
- lookup_ints_assign (const_match thy) asgns x
+fun lookup_const_ints_assign thy assigns x =
+ lookup_ints_assign (const_match thy) assigns x
handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
(* theory -> (styp option * int list) list -> styp -> row option *)
-fun row_for_constr thy maxes_asgns constr =
- SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr)
+fun row_for_constr thy maxes_assigns constr =
+ SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr)
handle TERM ("lookup_const_ints_assign", _) => NONE
+val max_bits = 31 (* Kodkod limit *)
+
(* extended_context -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
- -> typ -> block *)
-fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns
- bisim_depths T =
- if T = @{typ bisim_iterator} then
- [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
+ -> int list -> typ -> block *)
+fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
+ iters_assigns bitss bisim_depths T =
+ if T = @{typ unsigned_bit} then
+ [(Card T, map (Integer.min max_bits o Integer.max 1) bitss)]
+ else if T = @{typ signed_bit} then
+ [(Card T, map (Integer.add 1 o Integer.min max_bits o Integer.max 1) bitss)]
+ else if T = @{typ bisim_iterator} then
+ [(Card T, map (Integer.add 1 o Integer.max 0) bisim_depths)]
else if is_fp_iterator_type T then
- [(Card T, map (fn k => Int.max (0, k) + 1)
- (lookup_const_ints_assign thy iters_asgns
+ [(Card T, map (Integer.add 1 o Integer.max 0)
+ (lookup_const_ints_assign thy iters_assigns
(const_for_iterator_type T)))]
else
- (Card T, lookup_type_ints_assign thy cards_asgns T) ::
+ (Card T, lookup_type_ints_assign thy cards_assigns T) ::
(case datatype_constrs ext_ctxt T of
[_] => []
- | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
+ | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
(* extended_context -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
- -> typ list -> typ list -> block list *)
-fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
- mono_Ts nonmono_Ts =
+ -> int list -> typ list -> typ list -> block list *)
+fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns bitss
+ bisim_depths mono_Ts nonmono_Ts =
let
(* typ -> block *)
- val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns
- bisim_depths
+ val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
+ iters_assigns bitss bisim_depths
val mono_block = maps block_for mono_Ts
val nonmono_blocks = map block_for nonmono_Ts
in mono_block :: nonmono_blocks end
@@ -262,14 +282,14 @@
(* int list -> int *)
fun cost_with_monos [] = 0
| cost_with_monos (k :: ks) =
- if k < sync_threshold andalso forall (equal k) ks then
+ if k < sync_threshold andalso forall (curry (op =) k) ks then
k - sync_threshold
else
k * (k + 1) div 2 + Integer.sum ks
fun cost_without_monos [] = 0
| cost_without_monos [k] = k
| cost_without_monos (_ :: k :: ks) =
- if k < sync_threshold andalso forall (equal k) ks then
+ if k < sync_threshold andalso forall (curry (op =) k) ks then
k - sync_threshold
else
Integer.sum (k :: ks)
@@ -282,7 +302,7 @@
(* typ -> bool *)
fun is_self_recursive_constr_type T =
- exists (exists_subtype (equal (body_type T))) (binder_types T)
+ exists (exists_subtype (curry (op =) (body_type T))) (binder_types T)
(* (styp * int) list -> styp -> int *)
fun constr_max maxes x = the_default ~1 (AList.lookup (op =) maxes x)
@@ -290,117 +310,121 @@
type scope_desc = (typ * int) list * (styp * int) list
(* extended_context -> scope_desc -> typ * int -> bool *)
-fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) =
+fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
+ (T, k) =
case datatype_constrs ext_ctxt T of
[] => false
| xs =>
let
- val precise_cards =
+ val exact_cards =
map (Integer.prod
- o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns)
+ o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns)
o binder_types o snd) xs
- val maxes = map (constr_max max_asgns) xs
+ val maxes = map (constr_max max_assigns) xs
(* int -> int -> int *)
fun effective_max 0 ~1 = k
| effective_max 0 max = max
| effective_max card ~1 = card
| effective_max card max = Int.min (card, max)
- val max = map2 effective_max precise_cards maxes |> Integer.sum
+ val max = map2 effective_max exact_cards maxes |> Integer.sum
(* unit -> int *)
fun doms_card () =
- xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_asgns)
+ xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
o binder_types o snd)
|> Integer.sum
in
max < k
- orelse (forall (not_equal 0) precise_cards andalso doms_card () < k)
+ orelse (forall (not_equal 0) exact_cards andalso doms_card () < k)
end
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
(* extended_context -> scope_desc -> bool *)
fun is_surely_inconsistent_scope_description ext_ctxt
- (desc as (card_asgns, _)) =
- exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns
+ (desc as (card_assigns, _)) =
+ exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns
(* extended_context -> scope_desc -> (typ * int) list option *)
-fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) =
+fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
let
(* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
fun aux seen [] = SOME seen
| aux seen ((T, 0) :: _) = NONE
- | aux seen ((T, k) :: asgns) =
+ | aux seen ((T, k) :: assigns) =
(if is_surely_inconsistent_scope_description ext_ctxt
- ((T, k) :: seen, max_asgns) then
+ ((T, k) :: seen, max_assigns) then
raise SAME ()
else
- case aux ((T, k) :: seen) asgns of
- SOME asgns => SOME asgns
+ case aux ((T, k) :: seen) assigns of
+ SOME assigns => SOME assigns
| NONE => raise SAME ())
- handle SAME () => aux seen ((T, k - 1) :: asgns)
- in aux [] (rev card_asgns) end
+ handle SAME () => aux seen ((T, k - 1) :: assigns)
+ in aux [] (rev card_assigns) end
(* theory -> (typ * int) list -> typ * int -> typ * int *)
-fun repair_iterator_assign thy asgns (T as Type (s, Ts), k) =
+fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) =
(T, if T = @{typ bisim_iterator} then
- let val co_cards = map snd (filter (is_codatatype thy o fst) asgns) in
- Int.min (k, Integer.sum co_cards)
- end
+ let
+ val co_cards = map snd (filter (is_codatatype thy o fst) assigns)
+ in Int.min (k, Integer.sum co_cards) end
else if is_fp_iterator_type T then
case Ts of
[] => 1
- | _ => bounded_card_of_type k ~1 asgns (foldr1 HOLogic.mk_prodT Ts)
+ | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts)
else
k)
- | repair_iterator_assign _ _ asgn = asgn
+ | repair_iterator_assign _ _ assign = assign
(* row -> scope_desc -> scope_desc *)
-fun add_row_to_scope_descriptor (kind, ks) (card_asgns, max_asgns) =
+fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) =
case kind of
- Card T => ((T, the_single ks) :: card_asgns, max_asgns)
- | Max x => (card_asgns, (x, the_single ks) :: max_asgns)
+ Card T => ((T, the_single ks) :: card_assigns, max_assigns)
+ | Max x => (card_assigns, (x, the_single ks) :: max_assigns)
(* block -> scope_desc *)
fun scope_descriptor_from_block block =
fold_rev add_row_to_scope_descriptor block ([], [])
(* extended_context -> block list -> int list -> scope_desc option *)
fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
let
- val (card_asgns, max_asgns) =
+ val (card_assigns, max_assigns) =
maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
- val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the
+ val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
+ |> the
in
- SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns)
+ SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
+ max_assigns)
end
handle Option.Option => NONE
(* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *)
-fun offset_table_for_card_assigns thy asgns dtypes =
+fun offset_table_for_card_assigns thy assigns dtypes =
let
(* int -> (int * int) list -> (typ * int) list -> int Typtab.table
-> int Typtab.table *)
fun aux next _ [] = Typtab.update_new (dummyT, next)
- | aux next reusable ((T, k) :: asgns) =
- if k = 1 orelse is_integer_type T then
- aux next reusable asgns
+ | aux next reusable ((T, k) :: assigns) =
+ if k = 1 orelse is_integer_type T orelse is_bit_type T then
+ aux next reusable assigns
else if length (these (Option.map #constrs (datatype_spec dtypes T)))
> 1 then
- Typtab.update_new (T, next) #> aux (next + k) reusable asgns
+ Typtab.update_new (T, next) #> aux (next + k) reusable assigns
else
case AList.lookup (op =) reusable k of
- SOME j0 => Typtab.update_new (T, j0) #> aux next reusable asgns
+ SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns
| NONE => Typtab.update_new (T, next)
- #> aux (next + k) ((k, next) :: reusable) asgns
- in aux 0 [] asgns Typtab.empty end
+ #> aux (next + k) ((k, next) :: reusable) assigns
+ in aux 0 [] assigns Typtab.empty end
(* int -> (typ * int) list -> typ -> int *)
-fun domain_card max card_asgns =
- Integer.prod o map (bounded_card_of_type max max card_asgns) o binder_types
+fun domain_card max card_assigns =
+ Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
(* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
-> constr_spec list -> constr_spec list *)
-fun add_constr_spec (card_asgns, max_asgns) co card sum_dom_cards num_self_recs
- num_non_self_recs (self_rec, x as (s, T)) constrs =
+fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
+ num_self_recs num_non_self_recs (self_rec, x as (s, T))
+ constrs =
let
- val max = constr_max max_asgns x
+ val max = constr_max max_assigns x
(* int -> int *)
fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k)
(* unit -> int *)
@@ -412,7 +436,7 @@
end
else if not co andalso num_self_recs > 0 then
if not self_rec andalso num_non_self_recs = 1
- andalso domain_card 2 card_asgns T = 1 then
+ andalso domain_card 2 card_assigns T = 1 then
{delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}),
total = true}
else if s = @{const_name Cons} then
@@ -421,7 +445,7 @@
{delta = 0, epsilon = card, exclusive = false, total = false}
else if card = sum_dom_cards (card + 1) then
let val delta = next_delta () in
- {delta = delta, epsilon = delta + domain_card card card_asgns T,
+ {delta = delta, epsilon = delta + domain_card card card_assigns T,
exclusive = true, total = true}
end
else
@@ -432,55 +456,74 @@
explicit_max = max, total = total} :: constrs
end
+(* extended_context -> (typ * int) list -> typ -> bool *)
+fun has_exact_card ext_ctxt card_assigns T =
+ let val card = card_of_type card_assigns T in
+ card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
+ end
+
(* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
- (desc as (card_asgns, _)) (T, card) =
+ (desc as (card_assigns, _)) (T, card) =
let
- val shallow = T mem shallow_dataTs
+ val shallow = member (op =) shallow_dataTs T
val co = is_codatatype thy T
val xs = boxed_datatype_constrs ext_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
- List.partition (equal true) self_recs |> pairself length
- val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
- card_asgns T)
+ List.partition I self_recs |> pairself length
+ val complete = has_exact_card ext_ctxt card_assigns T
+ val concrete = xs |> maps (binder_types o snd) |> maps binder_types
+ |> forall (has_exact_card ext_ctxt card_assigns)
(* int -> int *)
fun sum_dom_cards max =
- map (domain_card max card_asgns o snd) xs |> Integer.sum
+ map (domain_card max card_assigns o snd) xs |> Integer.sum
val constrs =
fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
num_non_self_recs) (self_recs ~~ xs) []
in
- {typ = T, card = card, co = co, precise = precise, shallow = shallow,
- constrs = constrs}
+ {typ = T, card = card, co = co, complete = complete, concrete = concrete,
+ shallow = shallow, constrs = constrs}
end
+(* int -> int *)
+fun min_bits_for_nat_value n = if n <= 0 then 0 else IntInf.log2 n + 1
+(* scope_desc -> int *)
+fun min_bits_for_max_assigns (_, []) = 0
+ | min_bits_for_max_assigns (card_assigns, max_assigns) =
+ min_bits_for_nat_value (fold Integer.max
+ (map snd card_assigns @ map snd max_assigns) 0)
+
(* extended_context -> int -> typ list -> scope_desc -> scope *)
fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
- (desc as (card_asgns, _)) =
+ (desc as (card_assigns, _)) =
let
val datatypes =
map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
- (filter (is_datatype thy o fst) card_asgns)
- val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
+ (filter (is_datatype thy o fst) card_assigns)
+ val bits = card_of_type card_assigns @{typ signed_bit} - 1
+ handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
+ card_of_type card_assigns @{typ unsigned_bit}
+ handle TYPE ("Nitpick_HOL.card_of_type", _, _) => 0
+ val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
in
- {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
- bisim_depth = bisim_depth,
+ {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
+ bits = bits, bisim_depth = bisim_depth,
ofs = if sym_break <= 0 then Typtab.empty
- else offset_table_for_card_assigns thy card_asgns datatypes}
+ else offset_table_for_card_assigns thy card_assigns datatypes}
end
(* theory -> typ list -> (typ option * int list) list
-> (typ option * int list) list *)
-fun fix_cards_assigns_wrt_boxing _ _ [] = []
- | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_asgns) =
+fun repair_cards_assigns_wrt_boxing _ _ [] = []
+ | repair_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
(if is_fun_type T orelse is_pair_type T then
- Ts |> filter (curry (type_match thy o swap) T o unbox_type)
+ Ts |> filter (curry (type_match thy o swap) T o unbit_and_unbox_type)
|> map (rpair ks o SOME)
else
- [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_asgns
- | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) =
- (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns
+ [(SOME T, ks)]) @ repair_cards_assigns_wrt_boxing thy Ts cards_assigns
+ | repair_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
+ (NONE, ks) :: repair_cards_assigns_wrt_boxing thy Ts cards_assigns
val max_scopes = 4096
val distinct_threshold = 512
@@ -488,12 +531,15 @@
(* extended_context -> int -> (typ option * int list) list
-> (styp option * int list) list -> (styp option * int list) list -> int list
-> typ list -> typ list -> typ list -> int * scope list *)
-fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns
- iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
+fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
+ iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
+ shallow_dataTs =
let
- val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
- val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns
- bisim_depths mono_Ts nonmono_Ts
+ val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
+ cards_assigns
+ val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
+ iters_assigns bitss bisim_depths mono_Ts
+ nonmono_Ts
val ranks = map rank_of_block blocks
val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
val head = take max_scopes all
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Thu Dec 17 15:22:27 2009 +0100
@@ -300,6 +300,7 @@
val peephole_optim = true
val nat_card = 4
val int_card = 9
+ val bits = 8
val j0 = 0
val constrs = kodkod_constrs peephole_optim nat_card int_card j0
val (free_rels, pool, table) =
@@ -307,7 +308,7 @@
NameTable.empty
val u = Op1 (Not, type_of u, rep_of u, u)
|> rename_vars_in_nut pool table
- val formula = kodkod_formula_from_nut Typtab.empty false constrs u
+ val formula = kodkod_formula_from_nut bits Typtab.empty false constrs u
val bounds = map (bound_for_plain_rel ctxt debug) free_rels
val univ_card = univ_card nat_card int_card j0 bounds formula
val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu Dec 17 15:22:27 2009 +0100
@@ -12,7 +12,8 @@
exception ARG of string * string
exception BAD of string * string
- exception LIMIT of string * string
+ exception TOO_SMALL of string * string
+ exception TOO_LARGE of string * string
exception NOT_SUPPORTED of string
exception SAME of unit
@@ -51,7 +52,6 @@
val bool_T : typ
val nat_T : typ
val int_T : typ
- val subscript : string -> string
val nat_subscript : int -> string
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -71,7 +71,8 @@
exception ARG of string * string
exception BAD of string * string
-exception LIMIT of string * string
+exception TOO_SMALL of string * string
+exception TOO_LARGE of string * string
exception NOT_SUPPORTED of string
exception SAME of unit
@@ -96,14 +97,16 @@
| reasonable_power 0 _ = 0
| reasonable_power 1 _ = 1
| reasonable_power a b =
- if b < 0 orelse b > max_exponent then
- raise LIMIT ("Nitpick_Util.reasonable_power",
- "too large exponent (" ^ signed_string_of_int b ^ ")")
+ if b < 0 then
+ raise ARG ("Nitpick_Util.reasonable_power",
+ "negative exponent (" ^ signed_string_of_int b ^ ")")
+ else if b > max_exponent then
+ raise TOO_LARGE ("Nitpick_Util.reasonable_power",
+ "too large exponent (" ^ signed_string_of_int b ^ ")")
else
- let
- val c = reasonable_power a (b div 2) in
- c * c * reasonable_power a (b mod 2)
- end
+ let val c = reasonable_power a (b div 2) in
+ c * c * reasonable_power a (b mod 2)
+ end
(* int -> int -> int *)
fun exact_log m n =
@@ -247,7 +250,11 @@
(* string -> string *)
val subscript = implode o map (prefix "\<^isub>") o explode
(* int -> string *)
-val nat_subscript = subscript o signed_string_of_int
+fun nat_subscript n =
+ (* cheap trick to ensure proper alphanumeric ordering for one- and two-digit
+ numbers *)
+ if n <= 9 then "\<^bsub>" ^ signed_string_of_int n ^ "\<^esub>"
+ else subscript (string_of_int n)
(* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
fun time_limit NONE = I
--- a/src/HOL/Tools/refute.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/refute.ML Thu Dec 17 15:22:27 2009 +0100
@@ -45,13 +45,16 @@
val get_default_params : theory -> (string * string) list
val actual_params : theory -> (string * string) list -> params
- val find_model : theory -> params -> term -> bool -> unit
+ val find_model : theory -> params -> term list -> term -> bool -> unit
(* tries to find a model for a formula: *)
- val satisfy_term : theory -> (string * string) list -> term -> unit
+ val satisfy_term :
+ theory -> (string * string) list -> term list -> term -> unit
(* tries to find a model that refutes a formula: *)
- val refute_term : theory -> (string * string) list -> term -> unit
- val refute_goal : theory -> (string * string) list -> thm -> int -> unit
+ val refute_term :
+ theory -> (string * string) list -> term list -> term -> unit
+ val refute_goal :
+ Proof.context -> (string * string) list -> thm -> int -> unit
val setup : theory -> theory
@@ -153,8 +156,10 @@
(* formula. *)
(* "maxtime" int If >0, terminate after at most 'maxtime' seconds. *)
(* "satsolver" string SAT solver to be used. *)
+(* "no_assms" bool If "true", assumptions in structured proofs are *)
+(* not considered. *)
(* "expect" string Expected result ("genuine", "potential", "none", or *)
-(* "unknown") *)
+(* "unknown"). *)
(* ------------------------------------------------------------------------- *)
type params =
@@ -165,6 +170,7 @@
maxvars : int,
maxtime : int,
satsolver: string,
+ no_assms : bool,
expect : string
};
@@ -360,6 +366,15 @@
fun actual_params thy override =
let
+ (* (string * string) list * string -> bool *)
+ fun read_bool (parms, name) =
+ case AList.lookup (op =) parms name of
+ SOME "true" => true
+ | SOME "false" => false
+ | SOME s => error ("parameter " ^ quote name ^
+ " (value is " ^ quote s ^ ") must be \"true\" or \"false\"")
+ | NONE => error ("parameter " ^ quote name ^
+ " must be assigned a value")
(* (string * string) list * string -> int *)
fun read_int (parms, name) =
case AList.lookup (op =) parms name of
@@ -385,6 +400,7 @@
val maxtime = read_int (allparams, "maxtime")
(* string *)
val satsolver = read_string (allparams, "satsolver")
+ val no_assms = read_bool (allparams, "no_assms")
val expect = the_default "" (AList.lookup (op =) allparams "expect")
(* all remaining parameters of the form "string=int" are collected in *)
(* 'sizes' *)
@@ -395,10 +411,10 @@
(fn (name, value) => Option.map (pair name) (Int.fromString value))
(filter (fn (name, _) => name<>"minsize" andalso name<>"maxsize"
andalso name<>"maxvars" andalso name<>"maxtime"
- andalso name<>"satsolver") allparams)
+ andalso name<>"satsolver" andalso name<>"no_assms") allparams)
in
{sizes=sizes, minsize=minsize, maxsize=maxsize, maxvars=maxvars,
- maxtime=maxtime, satsolver=satsolver, expect=expect}
+ maxtime=maxtime, satsolver=satsolver, no_assms=no_assms, expect=expect}
end;
@@ -1118,6 +1134,7 @@
(* the model to the user by calling 'print_model' *)
(* thy : the current theory *)
(* {...} : parameters that control the translation/model generation *)
+(* assm_ts : assumptions to be considered unless "no_assms" is specified *)
(* t : term to be translated into a propositional formula *)
(* negate : if true, find a model that makes 't' false (rather than true) *)
(* ------------------------------------------------------------------------- *)
@@ -1125,7 +1142,7 @@
(* theory -> params -> Term.term -> bool -> unit *)
fun find_model thy {sizes, minsize, maxsize, maxvars, maxtime, satsolver,
- expect} t negate =
+ no_assms, expect} assm_ts t negate =
let
(* string -> unit *)
fun check_expect outcome_code =
@@ -1135,6 +1152,9 @@
fun wrapper () =
let
val timer = Timer.startRealTimer ()
+ val t = if no_assms then t
+ else if negate then Logic.list_implies (assm_ts, t)
+ else Logic.mk_conjunction_list (t :: assm_ts)
val u = unfold_defs thy t
val _ = tracing ("Unfolded term: " ^ Syntax.string_of_term_global thy u)
val axioms = collect_axioms thy u
@@ -1270,10 +1290,10 @@
(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Term.term -> unit *)
+ (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
- fun satisfy_term thy params t =
- find_model thy (actual_params thy params) t false;
+ fun satisfy_term thy params assm_ts t =
+ find_model thy (actual_params thy params) assm_ts t false;
(* ------------------------------------------------------------------------- *)
(* refute_term: calls 'find_model' to find a model that refutes 't' *)
@@ -1281,9 +1301,9 @@
(* parameters *)
(* ------------------------------------------------------------------------- *)
- (* theory -> (string * string) list -> Term.term -> unit *)
+ (* theory -> (string * string) list -> Term.term list -> Term.term -> unit *)
- fun refute_term thy params t =
+ fun refute_term thy params assm_ts t =
let
(* disallow schematic type variables, since we cannot properly negate *)
(* terms containing them (their logical meaning is that there EXISTS a *)
@@ -1332,15 +1352,29 @@
val frees = Term.rename_wrt_term strip_t (strip_all_vars ex_closure)
val subst_t = Term.subst_bounds (map Free frees, strip_t)
in
- find_model thy (actual_params thy params) subst_t true
+ find_model thy (actual_params thy params) assm_ts subst_t true
+ handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
end;
(* ------------------------------------------------------------------------- *)
(* refute_goal *)
(* ------------------------------------------------------------------------- *)
- fun refute_goal thy params st i =
- refute_term thy params (Logic.get_goal (Thm.prop_of st) i);
+ fun refute_goal ctxt params th i =
+ let
+ val t = th |> prop_of
+ in
+ if Logic.count_prems t = 0 then
+ priority "No subgoal!"
+ else
+ let
+ val assms = map term_of (Assumption.all_assms_of ctxt)
+ val (t, frees) = Logic.goal_params t i
+ in
+ refute_term (ProofContext.theory_of ctxt) params assms
+ (subst_bounds (frees, t))
+ end
+ end
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/refute_isar.ML Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/Tools/refute_isar.ML Thu Dec 17 15:22:27 2009 +0100
@@ -12,8 +12,9 @@
(*optional list of arguments of the form [name1=value1, name2=value2, ...]*)
-val scan_parm = OuterParse.name -- (OuterParse.$$$ "=" |-- OuterParse.name);
-
+val scan_parm =
+ OuterParse.name
+ -- (Scan.optional (OuterParse.$$$ "=" |-- OuterParse.name) "true")
val scan_parms = Scan.optional
(OuterParse.$$$ "[" |-- OuterParse.list scan_parm --| OuterParse.$$$ "]") [];
@@ -27,9 +28,9 @@
(fn (parms, i) =>
Toplevel.keep (fn state =>
let
- val thy = Toplevel.theory_of state;
+ val ctxt = Toplevel.context_of state;
val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
- in Refute.refute_goal thy parms st i end)));
+ in Refute.refute_goal ctxt parms st i end)));
(* 'refute_params' command *)
--- a/src/HOL/ex/Refute_Examples.thy Mon Nov 23 15:30:32 2009 -0800
+++ b/src/HOL/ex/Refute_Examples.thy Thu Dec 17 15:22:27 2009 +0100
@@ -1516,6 +1516,17 @@
refute
oops
+text {* Structured proofs *}
+
+lemma "x = y"
+proof cases
+ assume "x = y"
+ show ?thesis
+ refute
+ refute [no_assms]
+ refute [no_assms = false]
+oops
+
refute_params [satsolver="auto"]
end