redo Nitpick's nonstandard values as cyclic values (instead of additional constructors)

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 12 21:27:06 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Feb 13 11:56:06 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 Silly}, @{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 (curry (op =) @{const_name Silly} o fst) 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
 
@@ -2032,8 +2018,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	Fri Feb 12 21:27:06 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Feb 13 11:56:06 2010 +0100
@@ -318,7 +318,8 @@
            else
              [KK.TupleSet [],
               if T1 = T2 andalso epsilon > delta andalso
-                 not (datatype_spec dtypes T1 |> the |> #co) then
+                 (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]],
@@ -763,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

--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 12 21:27:06 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 11:56:06 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_non_std_type_name = "\<xi>"
 val opt_flag = nitpick_prefix ^ "opt"
 val non_opt_flag = nitpick_prefix ^ "non_opt"
 
@@ -397,7 +399,7 @@
         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) =
@@ -428,8 +430,9 @@
               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
+            if maybe_cyclic andalso member (op =) seen (T, j) then
               Var (var ())
             else if constr_s = @{const_name Word} then
               HOLogic.mk_number
@@ -437,7 +440,7 @@
                   (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
                     []
@@ -469,19 +472,20 @@
                           (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 Silly} then
-                    Const (fst (dest_Const (the_single ts)), T)
                   else
                     list_comb (Const constr_x, ts)
               in
-                if co then
+                if maybe_cyclic 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 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 var, t))
+                      else
+                        nth_atom pool for_auto
+                                 (Type (cyclic_non_std_type_name, [])) j k
                     else
                       t
                   end
@@ -682,7 +686,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

--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 12 21:27:06 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Feb 13 11:56:06 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,
@@ -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 *)