# HG changeset patch # User blanchet # Date 1261059747 -3600 # Node ID 7aac4d74bb76664535cd951c4bfdd5cd199609ec # Parent c4628a1dcf75e4059b94c656d444c5d33118054c# Parent 87cbdecaa87958281c6f2a0b79a9c03449b509a7 merged diff -r 87cbdecaa879 -r 7aac4d74bb76 doc-src/Nitpick/nitpick.tex --- 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: diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Nitpick.thy --- 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 \ bool) \ 'a" datatype ('a, 'b) pair_box = PairBox 'a 'b -datatype ('a, 'b) fun_box = FunBox "'a \ 'b" +datatype ('a, 'b) fun_box = FunBox "('a \ '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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 = diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Nitpick_Examples/Special_Nits.thy --- 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 "\a. g a = a \ \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\nat). b\<^isub>1 < b\<^isub>11 \ f5 g x = f5 (\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, diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Refute.thy --- 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. *) (* *) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/SAT.thy --- 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) *} diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/HISTORY --- 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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/kodkod.ML --- 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 ^ diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/minipick.ML --- 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" diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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\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) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- 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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 ("\", 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) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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 ^ " \ " ^ 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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- 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, diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_rep.ML --- 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])) = diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_tests.ML --- 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) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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 diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/refute.ML --- 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 (* ------------------------------------------------------------------------- *) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/Tools/refute_isar.ML --- 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 *) diff -r 87cbdecaa879 -r 7aac4d74bb76 src/HOL/ex/Refute_Examples.thy --- 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