1.1 --- a/doc-src/Nitpick/nitpick.tex Thu Nov 05 17:03:22 2009 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Thu Nov 05 19:06:35 2009 +0100
1.3 @@ -2420,6 +2420,11 @@
1.4 \kern1pt'a~\textit{list}\textrm{''}\}\ \,{*}\}$
1.5 \postw
1.6
1.7 +Inductive datatypes can be registered as coinductive datatypes, given
1.8 +appropriate coinductive constructors. However, doing so precludes
1.9 +the use of the inductive constructors---Nitpick will generate an error if they
1.10 +are needed.
1.11 +
1.12 \section{Known Bugs and Limitations}
1.13 \label{known-bugs-and-limitations}
1.14
1.15 @@ -2460,8 +2465,7 @@
1.16 \textit{Nitpick.register\_} functions can cause havoc if used improperly.
1.17
1.18 \item[$\bullet$] Although this has never been observed, arbitrary theorem
1.19 -morphisms could possibly confuse Nitpick and lead it to generate spurious
1.20 -counterexamples.
1.21 +morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
1.22
1.23 \item[$\bullet$] Local definitions are not supported and result in an error.
1.24
2.1 --- a/src/HOL/Tools/Nitpick/HISTORY Thu Nov 05 17:03:22 2009 +0100
2.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Thu Nov 05 19:06:35 2009 +0100
2.3 @@ -9,8 +9,10 @@
2.4 * Renamed "coalesce_type_vars" to "merge_type_vars"
2.5 * Optimized Kodkod encoding of datatypes whose constructors don't appear in
2.6 the formula to falsify
2.7 + * Added support for codatatype view of datatypes
2.8 * Fixed monotonicity check
2.9 * Fixed error in display of uncurried constants
2.10 + * Speeded up scope enumeration
2.11
2.12 Version 1.2.2 (16 Oct 2009)
2.13
3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Nov 05 17:03:22 2009 +0100
3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Nov 05 19:06:35 2009 +0100
3.3 @@ -87,6 +87,7 @@
3.4 val is_abs_fun : theory -> styp -> bool
3.5 val is_rep_fun : theory -> styp -> bool
3.6 val is_constr : theory -> styp -> bool
3.7 + val is_stale_constr : theory -> styp -> bool
3.8 val is_sel : string -> bool
3.9 val discr_for_constr : styp -> styp
3.10 val num_sels_for_constr_type : typ -> int
3.11 @@ -612,9 +613,13 @@
3.12 orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
3.13 orelse is_coconstr thy x
3.14 end
3.15 +fun is_stale_constr thy (x as (_, T)) =
3.16 + is_codatatype thy (body_type T) andalso is_constr_like thy x
3.17 + andalso not (is_coconstr thy x)
3.18 fun is_constr thy (x as (_, T)) =
3.19 is_constr_like thy x
3.20 andalso not (is_basic_datatype (fst (dest_Type (body_type T))))
3.21 + andalso not (is_stale_constr thy x)
3.22 (* string -> bool *)
3.23 val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
3.24 val is_sel_like_and_no_discr =
3.25 @@ -730,35 +735,37 @@
3.26
3.27 (* theory -> typ -> styp list *)
3.28 fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
3.29 - if is_datatype thy T then
3.30 - case Datatype.get_info thy s of
3.31 - SOME {index, descr, ...} =>
3.32 - let val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the in
3.33 - map (fn (s', Us) =>
3.34 - (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
3.35 - constrs
3.36 - end
3.37 - | NONE =>
3.38 - case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
3.39 - SOME (_, xs' as (_ :: _)) =>
3.40 - map (apsnd (repair_constr_type thy T)) xs'
3.41 - | _ =>
3.42 - if is_record_type T then
3.43 - let
3.44 - val s' = unsuffix Record.ext_typeN s ^ Record.extN
3.45 - val T' = (Record.get_extT_fields thy T
3.46 - |> apsnd single |> uncurry append |> map snd) ---> T
3.47 - in [(s', T')] end
3.48 - else case typedef_info thy s of
3.49 - SOME {abs_type, rep_type, Abs_name, ...} =>
3.50 - [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
3.51 - | NONE =>
3.52 - if T = @{typ ind} then
3.53 - [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
3.54 - else
3.55 - []
3.56 - else
3.57 - []
3.58 + (case AList.lookup (op =) (#codatatypes (TheoryData.get thy)) s of
3.59 + SOME (_, xs' as (_ :: _)) =>
3.60 + map (apsnd (repair_constr_type thy T)) xs'
3.61 + | _ =>
3.62 + if is_datatype thy T then
3.63 + case Datatype.get_info thy s of
3.64 + SOME {index, descr, ...} =>
3.65 + let
3.66 + val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
3.67 + in
3.68 + map (fn (s', Us) =>
3.69 + (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
3.70 + ---> T)) constrs
3.71 + end
3.72 + | NONE =>
3.73 + if is_record_type T then
3.74 + let
3.75 + val s' = unsuffix Record.ext_typeN s ^ Record.extN
3.76 + val T' = (Record.get_extT_fields thy T
3.77 + |> apsnd single |> uncurry append |> map snd) ---> T
3.78 + in [(s', T')] end
3.79 + else case typedef_info thy s of
3.80 + SOME {abs_type, rep_type, Abs_name, ...} =>
3.81 + [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
3.82 + | NONE =>
3.83 + if T = @{typ ind} then
3.84 + [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
3.85 + else
3.86 + []
3.87 + else
3.88 + [])
3.89 | uncached_datatype_constrs _ _ = []
3.90 (* extended_context -> typ -> styp list *)
3.91 fun datatype_constrs (ext_ctxt as {thy, constr_cache, ...} : extended_context)
3.92 @@ -1502,6 +1509,9 @@
3.93 | _ =>
3.94 if is_constr thy x then
3.95 (Const x, ts)
3.96 + else if is_stale_constr thy x then
3.97 + raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
3.98 + \(\"" ^ s ^ "\")")
3.99 else if is_record_get thy x then
3.100 case length ts of
3.101 0 => (do_term depth Ts (eta_expand Ts t 1), [])