--- a/doc-src/Nitpick/nitpick.tex Wed Feb 17 11:21:59 2010 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Feb 17 12:14:21 2010 +0100
@@ -472,7 +472,9 @@
\prew
\textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
\textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
-\slshape Nitpick found a potential counterexample: \\[2\smallskipamount]
+\slshape Warning: The conjecture either trivially holds or (more likely) lies outside Nitpick's supported
+fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
+Nitpick found a potential counterexample: \\[2\smallskipamount]
\hbox{}\qquad Free variable: \nopagebreak \\
\hbox{}\qquad\qquad $P = \textit{False}$ \\[2\smallskipamount]
Confirmation by ``\textit{auto}'': The above counterexample is genuine.
@@ -1331,7 +1333,7 @@
and this time \textit{arith} can finish off the subgoals.
A similar technique can be employed for structural induction. The
-following mini-formalization of full binary trees will serve as illustration:
+following mini formalization of full binary trees will serve as illustration:
\prew
\textbf{datatype} $\kern1pt'a$~\textit{bin\_tree} = $\textit{Leaf}~{\kern1pt'a}$ $\mid$ $\textit{Branch}$ ``\kern1pt$'a$ \textit{bin\_tree}'' ``\kern1pt$'a$ \textit{bin\_tree}'' \\[2\smallskipamount]
@@ -1350,8 +1352,7 @@
obtained by swapping $a$ and $b$:
\prew
-\textbf{lemma} $``\lbrakk a \in \textit{labels}~t;\, b \in \textit{labels}~t;\, a \not= b\rbrakk {}$ \\
-\phantom{\textbf{lemma} ``}$\,{\Longrightarrow}{\;\,} \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
+\textbf{lemma} $``\{a, b\} \subseteq \textit{labels}~t \,\Longrightarrow\, \textit{labels}~(\textit{swap}~t~a~b) = \textit{labels}~t$''
\postw
Nitpick can't find any counterexample, so we proceed with induction
@@ -1369,48 +1370,47 @@
\prew
\slshape
-Hint: To check that the induction hypothesis is general enough, try the following command:
-\textbf{nitpick}~[\textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$'', \textit{show\_consts}].
+Hint: To check that the induction hypothesis is general enough, try this command:
+\textbf{nitpick}~[\textit{non\_std}, \textit{show\_all}].
\postw
If we follow the hint, we get a ``nonstandard'' counterexample for the step:
\prew
-\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 4: \\[2\smallskipamount]
+\slshape Nitpick found a nonstandard counterexample for \textit{card} $'a$ = 3: \\[2\smallskipamount]
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $a = a_1$ \\
\hbox{}\qquad\qquad $b = a_2$ \\
\hbox{}\qquad\qquad $t = \xi_1$ \\
\hbox{}\qquad\qquad $u = \xi_2$ \\
+\hbox{}\qquad Datatype: \nopagebreak \\
+\hbox{}\qquad\qquad $\alpha~\textit{btree} = \{\xi_1 \mathbin{=} \textit{Branch}~\xi_1~\xi_1,\> \xi_2 \mathbin{=} \textit{Branch}~\xi_2~\xi_2,\> \textit{Branch}~\xi_1~\xi_2\}$ \\
\hbox{}\qquad {\slshape Constants:} \nopagebreak \\
\hbox{}\qquad\qquad $\textit{labels} = \undef
(\!\begin{aligned}[t]%
- & \xi_1 := \{a_1, a_4, a_3^\Q\},\> \xi_2 := \{a_2, a_3^\Q\}, \\[-2pt] %% TYPESETTING
- & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_4, a_3^\Q\}, \\[-2pt]
- & \textit{Branch}~\xi_2~\xi_2 := \{a_2, a_3^\Q\})\end{aligned}$ \\
+ & \xi_1 := \{a_2, a_3\},\> \xi_2 := \{a_1\},\> \\[-2pt]
+ & \textit{Branch}~\xi_1~\xi_2 := \{a_1, a_2, a_3\})\end{aligned}$ \\
\hbox{}\qquad\qquad $\lambda x_1.\> \textit{swap}~x_1~a~b = \undef
(\!\begin{aligned}[t]%
& \xi_1 := \xi_2,\> \xi_2 := \xi_2, \\[-2pt]
- & \textit{Branch}~\xi_1~\xi_2 := \textit{Branch}~\xi_2~\xi_2, \\[-2pt]
- & \textit{Branch}~\xi_2~\xi_2 := \textit{Branch}~\xi_2~\xi_2)\end{aligned}$ \\[2\smallskipamount]
+ & \textit{Branch}~\xi_1~\xi_2 := \xi_2)\end{aligned}$ \\[2\smallskipamount]
The existence of a nonstandard model suggests that the induction hypothesis is not general enough or perhaps
even wrong. See the ``Inductive Properties'' section of the Nitpick manual for details (``\textit{isabelle doc nitpick}'').
\postw
Reading the Nitpick manual is a most excellent idea.
-But what's going on? The \textit{non\_std} ``${\kern1pt'a}~\textit{bin\_tree}$''
-option told the tool to look for nonstandard models of binary trees, which
-means that new ``nonstandard'' trees $\xi_1, \xi_2, \ldots$, are now allowed in
-addition to the standard trees generated by the \textit{Leaf} and
-\textit{Branch} constructors.%
+But what's going on? The \textit{non\_std} option told the tool to look for
+nonstandard models of binary trees, which means that new ``nonstandard'' trees
+$\xi_1, \xi_2, \ldots$, are now allowed in addition to the standard trees
+generated by the \textit{Leaf} and \textit{Branch} constructors.%
\footnote{Notice the similarity between allowing nonstandard trees here and
allowing unreachable states in the preceding example (by removing the ``$n \in
\textit{reach\/}$'' assumption). In both cases, we effectively enlarge the
set of objects over which the induction is performed while doing the step
in order to test the induction hypothesis's strength.}
-The new trees are so nonstandard that we know nothing about them, except what
-the induction hypothesis states and what can be proved about all trees without
-relying on induction or case distinction. The key observation is,
+Unlike standard trees, these new trees contain cycles. We will see later that
+every property of acyclic trees that can be proved without using induction also
+holds for cyclic trees. Hence,
%
\begin{quote}
\textsl{If the induction
@@ -1418,9 +1418,9 @@
objects, and Nitpick won't find any nonstandard counterexample.}
\end{quote}
%
-But here, Nitpick did find some nonstandard trees $t = \xi_1$
-and $u = \xi_2$ such that $a \in \textit{labels}~t$, $b \notin
-\textit{labels}~t$, $a \notin \textit{labels}~u$, and $b \in \textit{labels}~u$.
+But here the tool find some nonstandard trees $t = \xi_1$
+and $u = \xi_2$ such that $a \notin \textit{labels}~t$, $b \in
+\textit{labels}~t$, $a \in \textit{labels}~u$, and $b \notin \textit{labels}~u$.
Because neither tree contains both $a$ and $b$, the induction hypothesis tells
us nothing about the labels of $\textit{swap}~t~a~b$ and $\textit{swap}~u~a~b$,
and as a result we know nothing about the labels of the tree
--- a/src/HOL/Nitpick.thy Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Nitpick.thy Wed Feb 17 12:14:21 2010 +0100
@@ -37,7 +37,6 @@
and bisim_iterator_max :: bisim_iterator
and Quot :: "'a \<Rightarrow> 'b"
and quot_normal :: "'a \<Rightarrow> 'a"
- and NonStd :: "'a \<Rightarrow> 'b"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -45,7 +44,6 @@
typedecl unsigned_bit
typedecl signed_bit
-typedecl \<xi>
datatype 'a word = Word "('a set)"
@@ -254,12 +252,12 @@
setup {* Nitpick_Isar.setup *}
hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
+ bisim_iterator_max Quot quot_normal 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 \<xi> word
+hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
The_psimp Eps_psimp unit_case_def nat_case_def list_size_simp nat_gcd_def
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Wed Feb 17 12:14:21 2010 +0100
@@ -259,14 +259,14 @@
(if c = a then Leaf b else if c = b then Leaf a else Leaf c)" |
"swap (Branch t u) a b = Branch (swap t a b) (swap u a b)"
-lemma "\<lbrakk>a \<in> labels t; b \<in> labels t; a \<noteq> b\<rbrakk> \<Longrightarrow> labels (swap t a b) = labels t"
+lemma "{a, b} \<subseteq> labels t \<Longrightarrow> labels (swap t a b) = labels t"
nitpick
proof (induct t)
case Leaf thus ?case by simp
next
case (Branch t u) thus ?case
nitpick
- nitpick [non_std "'a bin_tree", show_consts]
+ nitpick [non_std, show_all]
oops
lemma "labels (swap t a b) =
--- a/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Feb 17 12:14:21 2010 +0100
@@ -167,6 +167,7 @@
val max_arity : int -> int
val arity_of_rel_expr : rel_expr -> int
+ val is_problem_trivially_false : problem -> bool
val problems_equivalent : problem -> problem -> bool
val solve_any_problem :
bool -> Time.time option -> int -> int -> problem list -> outcome
@@ -491,6 +492,10 @@
| arity_of_decl (DeclSome ((n, _), _)) = n
| arity_of_decl (DeclSet ((n, _), _)) = n
+(* problem -> bool *)
+fun is_problem_trivially_false ({formula = False, ...} : problem) = true
+ | is_problem_trivially_false _ = false
+
(* string -> bool *)
val is_relevant_setting = not o member (op =) ["solver", "delay"]
@@ -1014,7 +1019,7 @@
val indexed_problems = if j >= 0 then
[(j, nth problems j)]
else
- filter (not_equal False o #formula o snd)
+ filter (is_problem_trivially_false o snd)
(0 upto length problems - 1 ~~ problems)
val triv_js = filter_out (AList.defined (op =) indexed_problems)
(0 upto length problems - 1)
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Feb 17 12:14:21 2010 +0100
@@ -9,7 +9,7 @@
sig
val configured_sat_solvers : bool -> string list
val smart_sat_solver_name : bool -> string
- val sat_solver_spec : bool -> string -> string * string list
+ val sat_solver_spec : string -> string * string list
end;
structure Kodkod_SAT : KODKOD_SAT =
@@ -51,15 +51,15 @@
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
-(* bool -> string -> sink -> string -> string -> string list -> string list
+(* string -> sink -> string -> string -> string list -> string list
-> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_external overlord name dev home exec args markers =
+fun dynamic_entry_for_external name dev home exec args markers =
case getenv home of
"" => NONE
| dir =>
SOME (name, fn () =>
let
- val serial_str = if overlord then "" else serial_string ()
+ val serial_str = serial_string ()
val base = name ^ serial_str
val out_file = base ^ ".out"
val dir_sep =
@@ -76,9 +76,9 @@
end)
(* bool -> bool -> string * sat_solver_info
-> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) =
+fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
- | dynamic_entry_for_info _ incremental (name, Internal (JNI, mode, ss)) =
+ | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
if incremental andalso mode = Batch then
NONE
else
@@ -92,26 +92,25 @@
else
NONE
end
- | dynamic_entry_for_info overlord false
- (name, External (dev, home, exec, args)) =
- dynamic_entry_for_external overlord name dev home exec args []
- | dynamic_entry_for_info overlord false
+ | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
+ dynamic_entry_for_external name dev home exec args []
+ | dynamic_entry_for_info false
(name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
- dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3]
- | dynamic_entry_for_info _ true _ = NONE
-(* bool -> bool -> (string * (unit -> string list)) list *)
-fun dynamic_list overlord incremental =
- map_filter (dynamic_entry_for_info overlord incremental) static_list
+ dynamic_entry_for_external name dev home exec args [m1, m2, m3]
+ | dynamic_entry_for_info true _ = NONE
+(* bool -> (string * (unit -> string list)) list *)
+fun dynamic_list incremental =
+ map_filter (dynamic_entry_for_info incremental) static_list
(* bool -> string list *)
-val configured_sat_solvers = map fst o dynamic_list false
+val configured_sat_solvers = map fst o dynamic_list
(* bool -> string *)
-val smart_sat_solver_name = fst o hd o dynamic_list false
+val smart_sat_solver_name = fst o hd o dynamic_list
-(* bool -> string -> string * string list *)
-fun sat_solver_spec overlord name =
+(* string -> string * string list *)
+fun sat_solver_spec name =
let
- val dyn_list = dynamic_list overlord false
+ val dyn_list = dynamic_list false
(* (string * 'a) list -> string *)
fun enum_solvers solvers =
commas (distinct (op =) (map (quote o fst) solvers))
--- a/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Wed Feb 17 12:14:21 2010 +0100
@@ -84,7 +84,7 @@
fun atom_from_formula f = RelIf (f, true_atom, false_atom)
(* Proof.context -> (typ -> int) -> styp list -> term -> formula *)
-fun kodkod_formula_for_term ctxt card frees =
+fun kodkod_formula_from_term ctxt card frees =
let
(* typ -> rel_expr -> rel_expr *)
fun R_rep_from_S_rep (T as Type ("fun", [T1, @{typ bool}])) r =
@@ -145,7 +145,7 @@
| Term.Var _ => raise SAME ()
| Bound _ => raise SAME ()
| Const (s, _) => raise NOT_SUPPORTED ("constant " ^ quote s)
- | _ => raise TERM ("Minipick.kodkod_formula_for_term.to_F", [t]))
+ | _ => raise TERM ("Minipick.kodkod_formula_from_term.to_F", [t]))
handle SAME () => formula_from_atom (to_R_rep Ts t)
(* typ list -> term -> rel_expr *)
and to_S_rep Ts t =
@@ -306,7 +306,7 @@
val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
val declarative_axioms =
map2 (declarative_axiom_for_free card) (index_seq 0 (length frees)) frees
- val formula = kodkod_formula_for_term ctxt card frees neg_t
+ val formula = kodkod_formula_from_term ctxt card frees neg_t
|> fold_rev (curry And) declarative_axioms
val univ_card = univ_card 0 0 0 bounds formula
val problem =
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 17 12:14:21 2010 +0100
@@ -130,7 +130,7 @@
sel_names: nut list,
nonsel_names: nut list,
rel_table: nut NameTable.table,
- liberal: bool,
+ unsound: bool,
scope: scope,
core: KK.formula,
defs: KK.formula list}
@@ -157,15 +157,15 @@
(Path.variable "ISABELLE_HOME_USER" ::
map Path.basic ["etc", "components"]))) ^ "\"."
-val max_liberal_delay_ms = 200
-val max_liberal_delay_percent = 2
+val max_unsound_delay_ms = 200
+val max_unsound_delay_percent = 2
(* Time.time option -> int *)
-fun liberal_delay_for_timeout NONE = max_liberal_delay_ms
- | liberal_delay_for_timeout (SOME timeout) =
- Int.max (0, Int.min (max_liberal_delay_ms,
+fun unsound_delay_for_timeout NONE = max_unsound_delay_ms
+ | unsound_delay_for_timeout (SOME timeout) =
+ Int.max (0, Int.min (max_unsound_delay_ms,
Time.toMilliseconds timeout
- * max_liberal_delay_percent div 100))
+ * max_unsound_delay_percent div 100))
(* Time.time option -> bool *)
fun passed_deadline NONE = false
@@ -247,7 +247,7 @@
(if i <> 1 orelse n <> 1 then
"subgoal " ^ string_of_int i ^ " of " ^ string_of_int n
else
- "goal")) [orig_t]))
+ "goal")) [Logic.list_implies (orig_assm_ts, orig_t)]))
val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
else orig_t
val assms_t = if assms orelse auto then
@@ -382,29 +382,22 @@
else
()
val deep_dataTs = filter is_deep_datatype all_Ts
- (* FIXME: Implement proper detection of induction datatypes. *)
+ (* This detection code is an ugly hack. Fortunately, it is used only to
+ provide a hint to the user. *)
(* string * (Rule_Cases.T * bool) -> bool *)
- fun is_inductive_case (_, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
- false
-(*
- not (null fixes) andalso exists (String.isSuffix ".hyps" o fst) assumes
-*)
- (* unit -> typ list *)
- val induct_dataTs =
- if exists is_inductive_case (ProofContext.cases_of ctxt) then
- filter (is_datatype thy) all_Ts
- else
- []
- val _ = if standard andalso not (null induct_dataTs) then
+ fun is_struct_induct_step (name, (Rule_Cases.Case {fixes, assumes, ...}, _)) =
+ not (null fixes) andalso
+ exists (String.isSuffix ".hyps" o fst) assumes andalso
+ exists (exists (curry (op =) name o shortest_name o fst)
+ o datatype_constrs hol_ctxt) deep_dataTs
+ val likely_in_struct_induct_step =
+ exists is_struct_induct_step (ProofContext.cases_of ctxt)
+ val _ = if standard andalso likely_in_struct_induct_step then
pprint_m (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
- \general enough, try the following command: " @
+ \general enough, try this command: " @
[Pretty.mark Markup.sendback (Pretty.blk (0,
- pstrs ("nitpick [" ^
- commas (map (prefix "non_std " o maybe_quote
- o unyxml o string_for_type ctxt)
- induct_dataTs) ^
- ", show_consts]")))] @ pstrs "."))
+ pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
()
(*
@@ -441,7 +434,7 @@
val too_big_scopes = Unsynchronized.ref []
(* bool -> scope -> rich_problem option *)
- fun problem_for_scope liberal
+ fun problem_for_scope unsound
(scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
let
val _ = not (exists (fn other => scope_less_eq other scope)
@@ -476,10 +469,10 @@
(univ_card nat_card int_card main_j0 [] KK.True)
val _ = check_arity min_univ_card min_highest_arity
- val core_u = choose_reps_in_nut scope liberal rep_table false core_u
- val def_us = map (choose_reps_in_nut scope liberal rep_table true)
+ val core_u = choose_reps_in_nut scope unsound rep_table false core_u
+ val def_us = map (choose_reps_in_nut scope unsound rep_table true)
def_us
- val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
+ val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
nondef_us
(*
val _ = List.app (priority o string_for_nut ctxt)
@@ -495,21 +488,19 @@
val core_u = rename_vars_in_nut pool rel_table core_u
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 -> KK.formula *)
- 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
+ val core_f = kodkod_formula_from_nut bits ofs kk core_u
+ val def_fs = map (kodkod_formula_from_nut bits ofs kk) def_us
+ val nondef_fs = map (kodkod_formula_from_nut bits ofs kk) nondef_us
val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
- val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
+ val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
PrintMode.setmp [] multiline_string_for_scope scope
val kodkod_sat_solver =
- Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd
+ 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
+ val delay = if unsound then
Option.map (fn time => Time.- (time, Time.now ()))
deadline
- |> liberal_delay_for_timeout
+ |> unsound_delay_for_timeout
else
0
val settings = [("solver", commas (map quote kodkod_sat_solver)),
@@ -547,13 +538,13 @@
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,
+ unsound = unsound, scope = scope, core = core_f,
defs = nondef_fs @ def_fs @ declarative_axioms})
end
handle TOO_LARGE (loc, msg) =>
if loc = "Nitpick_Kodkod.check_arity" andalso
not (Typtab.is_empty ofs) then
- problem_for_scope liberal
+ problem_for_scope unsound
{hol_ctxt = hol_ctxt, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth,
datatypes = datatypes, ofs = Typtab.empty}
@@ -563,13 +554,13 @@
else
(Unsynchronized.change too_big_scopes (cons scope);
print_v (fn () => ("Limit reached: " ^ msg ^
- ". Skipping " ^ (if liberal then "potential"
+ ". Skipping " ^ (if unsound then "potential"
else "genuine") ^
" component of scope."));
NONE)
| TOO_SMALL (loc, msg) =>
(print_v (fn () => ("Limit reached: " ^ msg ^
- ". Skipping " ^ (if liberal then "potential"
+ ". Skipping " ^ (if unsound then "potential"
else "genuine") ^
" component of scope."));
NONE)
@@ -584,7 +575,7 @@
val scopes = Unsynchronized.ref []
val generated_scopes = Unsynchronized.ref []
- val generated_problems = Unsynchronized.ref []
+ val generated_problems = Unsynchronized.ref ([] : rich_problem list)
val checked_problems = Unsynchronized.ref (SOME [])
val met_potential = Unsynchronized.ref 0
@@ -635,7 +626,7 @@
| NONE => print "No confirmation by \"auto\".")
else
();
- if not standard andalso not (null induct_dataTs) then
+ if not standard andalso likely_in_struct_induct_step then
print "The existence of a nonstandard model suggests that the \
\induction hypothesis is not general enough or perhaps even \
\wrong. See the \"Inductive Properties\" section of the \
@@ -718,7 +709,7 @@
| KK.Normal (sat_ps, unsat_js) =>
let
val (lib_ps, con_ps) =
- List.partition (#liberal o snd o nth problems o fst) sat_ps
+ List.partition (#unsound o snd o nth problems o fst) sat_ps
in
update_checked_problems problems (unsat_js @ map fst lib_ps);
if null con_ps then
@@ -735,9 +726,9 @@
(0, 0, donno)
else
let
- (* "co_js" is the list of conservative problems whose
- liberal pendants couldn't be satisfied and hence that
- most probably can't be satisfied themselves. *)
+ (* "co_js" is the list of sound problems whose unsound
+ pendants couldn't be satisfied and hence that most
+ probably can't be satisfied themselves. *)
val co_js =
map (fn j => j - 1) unsat_js
|> filter (fn j =>
@@ -750,7 +741,7 @@
val problems =
problems |> filter_out_indices bye_js
|> max_potential <= 0
- ? filter_out (#liberal o snd)
+ ? filter_out (#unsound o snd)
in
solve_any_problem max_potential max_genuine donno false
problems
@@ -770,7 +761,7 @@
(map fst sat_ps @ unsat_js)
val problems =
problems |> filter_out_indices bye_js
- |> filter_out (#liberal o snd)
+ |> filter_out (#unsound o snd)
in solve_any_problem 0 max_genuine donno false problems end
end
end
@@ -814,10 +805,10 @@
()
(* scope * bool -> rich_problem list * bool
-> rich_problem list * bool *)
- fun add_problem_for_scope (scope as {datatypes, ...}, liberal)
+ fun add_problem_for_scope (scope as {datatypes, ...}, unsound)
(problems, donno) =
(check_deadline ();
- case problem_for_scope liberal scope of
+ case problem_for_scope unsound scope of
SOME problem =>
(problems
|> (null problems orelse
@@ -833,6 +824,28 @@
([], donno)
val _ = Unsynchronized.change generated_problems (append problems)
val _ = Unsynchronized.change generated_scopes (append scopes)
+ val _ =
+ if j + 1 = n then
+ let
+ val (unsound_problems, sound_problems) =
+ List.partition (#unsound o snd) (!generated_problems)
+ in
+ if not (null sound_problems) andalso
+ forall (KK.is_problem_trivially_false o fst)
+ sound_problems then
+ print_m (fn () =>
+ "Warning: The conjecture either trivially holds or (more \
+ \likely) lies outside Nitpick's supported fragment." ^
+ (if exists (not o KK.is_problem_trivially_false o fst)
+ unsound_problems then
+ " Only potential counterexamples may be found."
+ else
+ ""))
+ else
+ ()
+ end
+ else
+ ()
in
solve_any_problem max_potential max_genuine donno true (rev problems)
end
@@ -845,7 +858,7 @@
let
(* rich_problem list -> rich_problem list *)
val do_filter =
- if !met_potential = max_potential then filter_out (#liberal o snd)
+ if !met_potential = max_potential then filter_out (#unsound o snd)
else I
val total = length (!scopes)
val unsat =
@@ -874,7 +887,7 @@
if max_potential = original_max_potential then
(print_m (fn () =>
"Nitpick found no " ^ das_wort_model ^ "." ^
- (if not standard andalso not (null induct_dataTs) then
+ (if not standard andalso likely_in_struct_induct_step then
" This suggests that the induction hypothesis might be \
\general enough to prove this subgoal."
else
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 17 12:14:21 2010 +0100
@@ -97,6 +97,7 @@
val dest_n_tuple : int -> term -> term list
val instantiate_type : theory -> typ -> typ -> typ -> typ
val is_real_datatype : theory -> string -> bool
+ val is_standard_datatype : hol_context -> typ -> bool
val is_quot_type : theory -> typ -> bool
val is_codatatype : theory -> typ -> bool
val is_pure_typedef : theory -> typ -> bool
@@ -574,6 +575,10 @@
(* theory -> string -> bool *)
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
+(* hol_context -> typ -> bool *)
+fun is_standard_datatype ({thy, stds, ...} : hol_context) =
+ the o triple_lookup (type_match thy) stds
+
(* theory -> typ -> bool *)
fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
| is_quot_type _ (Type ("FSet.fset", _)) = true
@@ -828,9 +833,8 @@
fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
fun suc_const T = Const (@{const_name Suc}, T --> T)
-(* hol_context -> typ -> styp list *)
-fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
- (T as Type (s, Ts)) =
+(* theory -> typ -> styp list *)
+fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
(case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
| _ =>
@@ -843,8 +847,6 @@
map (fn (s', Us) =>
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
---> T)) constrs
- |> (triple_lookup (type_match thy) stds T |> the |> not) ?
- cons (@{const_name NonStd}, @{typ \<xi>} --> T)
end
| NONE =>
if is_record_type T then
@@ -867,11 +869,11 @@
[])
| uncached_datatype_constrs _ _ = []
(* hol_context -> typ -> styp list *)
-fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
+fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
case AList.lookup (op =) (!constr_cache) T of
SOME xs => xs
| NONE =>
- let val xs = uncached_datatype_constrs hol_ctxt T in
+ let val xs = uncached_datatype_constrs thy T in
(Unsynchronized.change constr_cache (cons (T, xs)); xs)
end
fun boxed_datatype_constrs hol_ctxt =
@@ -957,10 +959,6 @@
| _ => list_comb (Const x, args)
end
-(* The higher this number is, the more nonstandard models can be generated. It's
- not important enough to be a user option, though. *)
-val xi_card = 8
-
(* (typ * int) list -> typ -> int *)
fun card_of_type assigns (Type ("fun", [T1, T2])) =
reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
@@ -970,7 +968,6 @@
| card_of_type _ @{typ prop} = 2
| card_of_type _ @{typ bool} = 2
| card_of_type _ @{typ unit} = 1
- | card_of_type _ @{typ \<xi>} = xi_card
| card_of_type assigns T =
case AList.lookup (op =) assigns T of
SOME k => k
@@ -1027,7 +1024,6 @@
| @{typ prop} => 2
| @{typ bool} => 2
| @{typ unit} => 1
- | @{typ \<xi>} => xi_card
| Type _ =>
(case datatype_constrs hol_ctxt T of
[] => if is_integer_type T orelse is_bit_type T then 0
@@ -1393,21 +1389,11 @@
fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
let
val xs = datatype_constrs hol_ctxt dataT
- val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
- val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
+ val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
+ val (xs', x) = split_last xs
in
- (if length xs = length xs' then
- let
- val (xs'', x) = split_last xs'
- in
- constr_case_body thy (1, x)
- |> fold_rev (add_constr_case hol_ctxt res_T)
- (length xs' downto 2 ~~ xs'')
- end
- else
- Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
- |> fold_rev (add_constr_case hol_ctxt res_T)
- (length xs' downto 1 ~~ xs'))
+ constr_case_body thy (1, x)
+ |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
|> fold_rev (curry absdummy) (func_Ts @ [dataT])
end
@@ -1738,10 +1724,11 @@
(tac ctxt (auto_tac (clasimpset_of ctxt))))
#> the #> Goal.finish ctxt) goal
-val max_cached_wfs = 100
-val cached_timeout = Unsynchronized.ref (SOME Time.zeroTime)
-val cached_wf_props : (term * bool) list Unsynchronized.ref =
- Unsynchronized.ref []
+val max_cached_wfs = 50
+val cached_timeout =
+ Synchronized.var "Nitpick_HOL.cached_timeout" (SOME Time.zeroTime)
+val cached_wf_props =
+ Synchronized.var "Nitpick_HOL.cached_wf_props" ([] : (term * bool) list)
val termination_tacs = [Lexicographic_Order.lex_order_tac true,
ScnpReconstruct.sizechange_tac]
@@ -1772,19 +1759,20 @@
else
()
in
- if tac_timeout = (!cached_timeout) andalso
- length (!cached_wf_props) < max_cached_wfs then
+ if tac_timeout = Synchronized.value cached_timeout andalso
+ length (Synchronized.value cached_wf_props) < max_cached_wfs then
()
else
- (cached_wf_props := []; cached_timeout := tac_timeout);
- case AList.lookup (op =) (!cached_wf_props) prop of
+ (Synchronized.change cached_wf_props (K []);
+ Synchronized.change cached_timeout (K tac_timeout));
+ case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of
SOME wf => wf
| NONE =>
let
val goal = prop |> cterm_of thy |> Goal.init
val wf = exists (terminates_by ctxt tac_timeout goal)
termination_tacs
- in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end
+ in Synchronized.change cached_wf_props (cons (prop, wf)); wf end
end)
handle List.Empty => false
| NO_TRIPLE () => false
@@ -1799,14 +1787,14 @@
SOME (SOME b) => b
| _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
case AList.lookup (op =) (!wf_cache) x of
- SOME (_, wf) => wf
- | NONE =>
- let
- val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
- val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
- in
- Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
- end
+ SOME (_, wf) => wf
+ | NONE =>
+ let
+ val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
+ val wf = uncached_is_well_founded_inductive_pred hol_ctxt x
+ in
+ Unsynchronized.change wf_cache (cons (x, (gfp, wf))); wf
+ end
(* typ list -> typ -> typ -> term -> term *)
fun ap_curry [_] _ _ t = t
@@ -2032,8 +2020,7 @@
| Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
| Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
| Type (_, Ts) =>
- if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
- @{typ \<xi>} :: accum) T then
+ if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
accum
else
T :: accum
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 17 12:14:21 2010 +0100
@@ -36,7 +36,7 @@
hol_context -> int -> int Typtab.table -> kodkod_constrs
-> nut NameTable.table -> dtype_spec list -> Kodkod.formula list
val kodkod_formula_from_nut :
- int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> Kodkod.formula
+ int -> int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
end;
structure Nitpick_Kodkod : NITPICK_KODKOD =
@@ -317,7 +317,9 @@
[ts] |> not exclusive ? cons (KK.TupleSet [])
else
[KK.TupleSet [],
- if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
+ if T1 = T2 andalso epsilon > delta andalso
+ (datatype_spec dtypes T1 |> the |> pairf #co #standard)
+ = (false, true) then
index_seq delta (epsilon - delta)
|> map (fn j =>
KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
@@ -762,6 +764,7 @@
(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> dtype_spec -> nfa_entry option *)
fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
+ | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
| nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
| nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes
@@ -770,45 +773,47 @@
val empty_rel = KK.Product (KK.None, KK.None)
(* nfa_table -> typ -> typ -> KK.rel_expr list *)
-fun direct_path_rel_exprs nfa start final =
- case AList.lookup (op =) nfa final of
- SOME trans => map fst (filter (curry (op =) start o snd) trans)
+fun direct_path_rel_exprs nfa start_T final_T =
+ case AList.lookup (op =) nfa final_T of
+ SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
| NONE => []
(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
-and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
- fold kk_union (direct_path_rel_exprs nfa start final)
- (if start = final then KK.Iden else empty_rel)
- | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final =
- kk_union (any_path_rel_expr kk nfa qs start final)
- (knot_path_rel_expr kk nfa qs start q final)
+and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
+ final_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T final_T)
+ (if start_T = final_T then KK.Iden else empty_rel)
+ | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
+ kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
+ (knot_path_rel_expr kk nfa Ts start_T T final_T)
(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
-> KK.rel_expr *)
-and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start
- knot final =
- kk_join (kk_join (any_path_rel_expr kk nfa qs knot final)
- (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot)))
- (any_path_rel_expr kk nfa qs start knot)
+and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
+ start_T knot_T final_T =
+ kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
+ (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
+ (any_path_rel_expr kk nfa Ts start_T knot_T)
(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
-and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start =
- fold kk_union (direct_path_rel_exprs nfa start start) empty_rel
- | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start =
- if start = q then
- kk_closure (loop_path_rel_expr kk nfa qs start)
+and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
+ | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
+ start_T =
+ if start_T = T then
+ kk_closure (loop_path_rel_expr kk nfa Ts start_T)
else
- kk_union (loop_path_rel_expr kk nfa qs start)
- (knot_path_rel_expr kk nfa qs start q start)
+ kk_union (loop_path_rel_expr kk nfa Ts start_T)
+ (knot_path_rel_expr kk nfa Ts start_T T start_T)
(* nfa_table -> unit NfaGraph.T *)
fun graph_for_nfa nfa =
let
(* typ -> unit NfaGraph.T -> unit NfaGraph.T *)
- fun new_node q = perhaps (try (NfaGraph.new_node (q, ())))
+ fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
(* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *)
fun add_nfa [] = I
| add_nfa ((_, []) :: nfa) = add_nfa nfa
- | add_nfa ((q, ((_, q') :: transitions)) :: nfa) =
- add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o
- new_node q' o new_node q
+ | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
+ add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o
+ new_node T' o new_node T
in add_nfa nfa NfaGraph.empty end
(* nfa_table -> nfa_table list *)
@@ -816,22 +821,22 @@
nfa |> graph_for_nfa |> NfaGraph.strong_conn
|> map (fn keys => filter (member (op =) keys o fst) nfa)
-(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *)
-fun acyclicity_axiom_for_datatype dtypes kk nfa start =
+(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
+fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
#kk_no kk (#kk_intersect kk
- (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
+ (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> KK.formula list *)
fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
|> strongly_connected_sub_nfas
- |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
- nfa)
+ |> maps (fn nfa =>
+ map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
-> constr_spec -> int -> KK.formula *)
fun sel_axiom_for_sel hol_ctxt j0
- (kk as {kk_all, kk_implies, kk_formula_if, kk_subset, kk_rel_eq, kk_no,
+ (kk as {kk_all, kk_formula_if, kk_implies, kk_subset, kk_rel_eq, kk_no,
kk_join, ...}) rel_table dom_r
({const, delta, epsilon, exclusive, explicit_max, ...} : constr_spec)
n =
@@ -862,19 +867,19 @@
[formula_for_bool honors_explicit_max]
else
let
- val ran_r = discr_rel_expr rel_table const
+ val dom_r = discr_rel_expr rel_table const
val max_axiom =
if honors_explicit_max then
KK.True
else if is_twos_complement_representable bits (epsilon - delta) then
- KK.LE (KK.Cardinality ran_r, KK.Num explicit_max)
+ KK.LE (KK.Cardinality dom_r, KK.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 hol_ctxt j0 kk rel_table ran_r constr)
+ map (sel_axiom_for_sel hol_ctxt j0 kk rel_table dom_r constr)
(index_seq 0 (num_sels_for_constr_type (snd const)))
end
end
@@ -949,8 +954,8 @@
acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes @
maps (other_axioms_for_datatype hol_ctxt bits ofs kk rel_table) dtypes
-(* int -> int Typtab.table -> bool -> kodkod_constrs -> nut -> KK.formula *)
-fun kodkod_formula_from_nut bits ofs liberal
+(* int -> int Typtab.table -> kodkod_constrs -> nut -> KK.formula *)
+fun kodkod_formula_from_nut bits ofs
(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_lone, kk_one, kk_some, kk_rel_let, kk_rel_if, kk_union,
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 17 12:14:21 2010 +0100
@@ -53,6 +53,8 @@
val base_mixfix = "_\<^bsub>base\<^esub>"
val step_mixfix = "_\<^bsub>step\<^esub>"
val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
+val cyclic_co_val_name = "\<omega>"
+val cyclic_type_name = "\<xi>"
val opt_flag = nitpick_prefix ^ "opt"
val non_opt_flag = nitpick_prefix ^ "non_opt"
@@ -88,7 +90,7 @@
Const (nth_atom_name pool "" T j k, T)
(* term -> real *)
-fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
(* term * term -> order *)
@@ -257,14 +259,13 @@
| 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 -> KK.raw_bound list -> typ -> typ -> rep
- -> int list list -> term *)
-fun reconstruct_term (maybe_name, base_name, step_name, abs_name)
+(* bool -> atom_pool -> string * string * string * string -> scope -> nut list
+ -> nut list -> nut list -> nut NameTable.table -> KK.raw_bound list -> typ
+ -> typ -> rep -> int list list -> term *)
+fun reconstruct_term elaborate pool (maybe_name, base_name, step_name, abs_name)
({hol_ctxt as {thy, ctxt, ...}, card_assigns, bits, datatypes, ofs, ...}
: scope) sel_names rel_table bounds =
let
- val pool = Unsynchronized.ref []
val for_auto = (maybe_name = "")
(* int list list -> int *)
fun value_of_bits jss =
@@ -397,13 +398,16 @@
else case datatype_spec datatypes T of
NONE => nth_atom pool for_auto T j k
| SOME {deep = false, ...} => nth_atom pool for_auto T j k
- | SOME {co, constrs, ...} =>
+ | SOME {co, standard, constrs, ...} =>
let
(* styp -> int list *)
fun tuples_for_const (s, T) =
tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
- (* unit -> indexname * typ *)
- fun var () = ((nth_atom_name pool "" T j k, 0), T)
+ (* unit -> term *)
+ fun cyclic_atom () =
+ nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
+ fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
+
val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
constrs
val real_j = j + offset_of_type ofs T
@@ -428,16 +432,18 @@
map (map_filter (fn js => if hd js = real_j then SOME (tl js)
else NONE)) sel_jsss
val uncur_arg_Ts = binder_types constr_T
+ val maybe_cyclic = co orelse not standard
in
- if co andalso member (op =) seen (T, j) then
- Var (var ())
+ if maybe_cyclic andalso not (null seen) andalso
+ member (op =) (seen |> elaborate ? (fst o split_last)) (T, j) then
+ cyclic_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)
+ val seen = seen |> maybe_cyclic ? cons (T, j)
val ts =
if length arg_Ts = 0 then
[]
@@ -459,7 +465,7 @@
0 => mk_num 0
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
- | n2 => Const (@{const_name Rings.divide},
+ | n2 => Const (@{const_name divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
@@ -469,19 +475,27 @@
(is_abs_fun thy constr_x orelse
constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
- else if not for_auto andalso
- constr_s = @{const_name NonStd} then
- Const (fst (dest_Const (the_single ts)), T)
else
list_comb (Const constr_x, ts)
in
- if co then
- let val var = var () in
- if exists_subterm (curry (op =) (Var var)) t then
- Const (@{const_name The}, (T --> bool_T) --> T)
- $ Abs ("\<omega>", T,
- Const (@{const_name "op ="}, T --> T --> bool_T)
- $ Bound 0 $ abstract_over (Var var, t))
+ if maybe_cyclic then
+ let val var = cyclic_var () in
+ if elaborate andalso not standard andalso
+ length seen = 1 andalso
+ exists_subterm (fn Const (s, _) =>
+ String.isPrefix cyclic_type_name s
+ | t' => t' = var) t then
+ let val atom = cyclic_atom () in
+ HOLogic.mk_eq (atom, subst_atomic [(var, atom)] t)
+ end
+ else if exists_subterm (curry (op =) var) t then
+ if co then
+ Const (@{const_name The}, (T --> bool_T) --> T)
+ $ Abs (cyclic_co_val_name, T,
+ Const (@{const_name "op ="}, T --> T --> bool_T)
+ $ Bound 0 $ abstract_over (var, t))
+ else
+ cyclic_atom ()
else
t
end
@@ -537,17 +551,15 @@
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
- in
- polish_funs [] o unbit_and_unbox_term oooo term_for_rep []
- end
+ in polish_funs [] o unbit_and_unbox_term oooo term_for_rep [] end
-(* scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut
- -> term *)
-fun term_for_name scope sel_names rel_table bounds name =
+(* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list
+ -> nut -> term *)
+fun term_for_name pool scope sel_names rel_table bounds name =
let val T = type_of name in
tuple_list_for_name rel_table bounds name
- |> reconstruct_term ("", "", "", "") scope sel_names rel_table bounds T T
- (rep_of name)
+ |> reconstruct_term false pool ("", "", "", "") scope sel_names rel_table
+ bounds T T (rep_of name)
end
(* Proof.context -> (string * string * string * string) * Proof.context *)
@@ -610,6 +622,7 @@
card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
formats all_frees free_names sel_names nonsel_names rel_table bounds =
let
+ val pool = Unsynchronized.ref []
val (wacky_names as (_, base_name, step_name, _), ctxt) =
add_wacky_syntax ctxt
val hol_ctxt =
@@ -629,11 +642,13 @@
val scope = {hol_ctxt = hol_ctxt, card_assigns = card_assigns,
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
+ (* bool -> typ -> typ -> rep -> int list list -> term *)
+ fun term_for_rep elaborate =
+ reconstruct_term elaborate pool wacky_names scope sel_names rel_table
+ bounds
(* nat -> typ -> nat -> typ *)
- fun nth_value_of_type card T n = term_for_rep T T (Atom (card, 0)) [[n]]
+ fun nth_value_of_type card T n =
+ term_for_rep true 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
@@ -666,7 +681,7 @@
Const (@{const_name undefined}, T')
else
tuple_list_for_name rel_table bounds name
- |> term_for_rep T T' (rep_of name)
+ |> term_for_rep false T T' (rep_of name)
in
Pretty.block (Pretty.breaks
[setmp_show_all_types (Syntax.pretty_term ctxt) t1,
@@ -682,7 +697,8 @@
(* typ -> dtype_spec list *)
fun integer_datatype T =
[{typ = T, card = card_of_type card_assigns T, co = false,
- complete = false, concrete = true, deep = true, constrs = []}]
+ standard = true, complete = false, concrete = true, deep = true,
+ constrs = []}]
handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
val (codatatypes, datatypes) =
datatypes |> filter #deep |> List.partition #co
@@ -758,7 +774,7 @@
(* nut -> term *)
fun free_name_assm name =
HOLogic.mk_eq (Free (nickname_of name, type_of name),
- term_for_name scope sel_names rel_table bounds name)
+ term_for_name pool scope sel_names rel_table bounds name)
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
val model_assms = map free_name_assm free_names
val assm = foldr1 s_conj (freeT_assms @ model_assms)
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Feb 17 12:14:21 2010 +0100
@@ -892,7 +892,7 @@
(* scope -> bool -> rep NameTable.table -> bool -> nut -> nut *)
fun choose_reps_in_nut (scope as {hol_ctxt as {thy, ctxt, ...}, card_assigns,
bits, datatypes, ofs, ...})
- liberal table def =
+ unsound table def =
let
val bool_atom_R = Atom (2, offset_of_type ofs bool_T)
(* polarity -> bool -> rep *)
@@ -1036,7 +1036,7 @@
if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
else opt_opt_case ()
in
- if liberal orelse polar = Neg orelse
+ if unsound orelse polar = Neg 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 ()
@@ -1138,7 +1138,7 @@
else
let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
if def orelse
- (liberal andalso (polar = Pos) = (oper = All)) orelse
+ (unsound andalso (polar = Pos) = (oper = All)) orelse
is_complete_type datatypes (type_of u1) then
quant_u
else
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Feb 17 12:14:21 2010 +0100
@@ -22,6 +22,7 @@
typ: typ,
card: int,
co: bool,
+ standard: bool,
complete: bool,
concrete: bool,
deep: bool,
@@ -71,6 +72,7 @@
typ: typ,
card: int,
co: bool,
+ standard: bool,
complete: bool,
concrete: bool,
deep: bool,
@@ -162,7 +164,7 @@
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])
+ else ["bisim_depth = " ^ signed_string_of_int bisim_depth])
in
setmp_show_all_types
(fn () => (cards primary_card_assigns, cards secondary_card_assigns,
@@ -466,6 +468,7 @@
let
val deep = member (op =) deep_dataTs T
val co = is_codatatype thy T
+ val standard = is_standard_datatype hol_ctxt T
val xs = boxed_datatype_constrs hol_ctxt T
val self_recs = map (is_self_recursive_constr_type o snd) xs
val (num_self_recs, num_non_self_recs) =
@@ -481,8 +484,8 @@
num_non_self_recs)
(sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
in
- {typ = T, card = card, co = co, complete = complete, concrete = concrete,
- deep = deep, constrs = constrs}
+ {typ = T, card = card, co = co, standard = standard, complete = complete,
+ concrete = concrete, deep = deep, constrs = constrs}
end
(* int -> int *)
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 17 11:21:59 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Wed Feb 17 12:14:21 2010 +0100
@@ -308,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 bits Typtab.empty false constrs u
+ val formula = kodkod_formula_from_nut bits Typtab.empty 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)