1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Feb 12 21:27:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sat Feb 13 11:56:06 2010 +0100
     1.3 @@ -97,6 +97,7 @@
     1.4    val dest_n_tuple : int -> term -> term list
     1.5    val instantiate_type : theory -> typ -> typ -> typ -> typ
     1.6    val is_real_datatype : theory -> string -> bool
     1.7 +  val is_standard_datatype : hol_context -> typ -> bool
     1.8    val is_quot_type : theory -> typ -> bool
     1.9    val is_codatatype : theory -> typ -> bool
    1.10    val is_pure_typedef : theory -> typ -> bool
    1.11 @@ -574,6 +575,10 @@
    1.12  (* theory -> string -> bool *)
    1.13  val is_typedef = is_some oo typedef_info
    1.14  val is_real_datatype = is_some oo Datatype.get_info
    1.15 +(* hol_context -> typ -> bool *)
    1.16 +fun is_standard_datatype ({thy, stds, ...} : hol_context) =
    1.17 +  the o triple_lookup (type_match thy) stds
    1.18 +
    1.19  (* theory -> typ -> bool *)
    1.20  fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* FIXME *)
    1.21    | is_quot_type _ (Type ("FSet.fset", _)) = true
    1.22 @@ -828,9 +833,8 @@
    1.23  fun zero_const T = Const (@{const_name zero_nat_inst.zero_nat}, T)
    1.24  fun suc_const T = Const (@{const_name Suc}, T --> T)
    1.25  
    1.26 -(* hol_context -> typ -> styp list *)
    1.27 -fun uncached_datatype_constrs ({thy, stds, ...} : hol_context)
    1.28 -                              (T as Type (s, Ts)) =
    1.29 +(* theory -> typ -> styp list *)
    1.30 +fun uncached_datatype_constrs thy (T as Type (s, Ts)) =
    1.31      (case AList.lookup (op =) (#codatatypes (Data.get thy)) s of
    1.32         SOME (_, xs' as (_ :: _)) => map (apsnd (repair_constr_type thy T)) xs'
    1.33       | _ =>
    1.34 @@ -843,8 +847,6 @@
    1.35               map (fn (s', Us) =>
    1.36                       (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
    1.37                            ---> T)) constrs
    1.38 -             |> (triple_lookup (type_match thy) stds T |> the |> not) ?
    1.39 -                cons (@{const_name Silly}, @{typ \<xi>} --> T)
    1.40             end
    1.41           | NONE =>
    1.42             if is_record_type T then
    1.43 @@ -867,11 +869,11 @@
    1.44           [])
    1.45    | uncached_datatype_constrs _ _ = []
    1.46  (* hol_context -> typ -> styp list *)
    1.47 -fun datatype_constrs (hol_ctxt as {constr_cache, ...}) T =
    1.48 +fun datatype_constrs ({thy, constr_cache, ...} : hol_context) T =
    1.49    case AList.lookup (op =) (!constr_cache) T of
    1.50      SOME xs => xs
    1.51    | NONE =>
    1.52 -    let val xs = uncached_datatype_constrs hol_ctxt T in
    1.53 +    let val xs = uncached_datatype_constrs thy T in
    1.54        (Unsynchronized.change constr_cache (cons (T, xs)); xs)
    1.55      end
    1.56  fun boxed_datatype_constrs hol_ctxt =
    1.57 @@ -957,10 +959,6 @@
    1.58        | _ => list_comb (Const x, args)
    1.59      end
    1.60  
    1.61 -(* The higher this number is, the more nonstandard models can be generated. It's
    1.62 -   not important enough to be a user option, though. *)
    1.63 -val xi_card = 8
    1.64 -
    1.65  (* (typ * int) list -> typ -> int *)
    1.66  fun card_of_type assigns (Type ("fun", [T1, T2])) =
    1.67      reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
    1.68 @@ -970,7 +968,6 @@
    1.69    | card_of_type _ @{typ prop} = 2
    1.70    | card_of_type _ @{typ bool} = 2
    1.71    | card_of_type _ @{typ unit} = 1
    1.72 -  | card_of_type _ @{typ \<xi>} = xi_card
    1.73    | card_of_type assigns T =
    1.74      case AList.lookup (op =) assigns T of
    1.75        SOME k => k
    1.76 @@ -1027,7 +1024,6 @@
    1.77         | @{typ prop} => 2
    1.78         | @{typ bool} => 2
    1.79         | @{typ unit} => 1
    1.80 -       | @{typ \<xi>} => xi_card
    1.81         | Type _ =>
    1.82           (case datatype_constrs hol_ctxt T of
    1.83              [] => if is_integer_type T orelse is_bit_type T then 0
    1.84 @@ -1393,21 +1389,11 @@
    1.85  fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
    1.86    let
    1.87      val xs = datatype_constrs hol_ctxt dataT
    1.88 -    val xs' = filter_out (curry (op =) @{const_name Silly} o fst) xs
    1.89 -    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
    1.90 +    val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs
    1.91 +    val (xs', x) = split_last xs
    1.92    in
    1.93 -    (if length xs = length xs' then
    1.94 -       let
    1.95 -         val (xs'', x) = split_last xs'
    1.96 -       in
    1.97 -         constr_case_body thy (1, x)
    1.98 -         |> fold_rev (add_constr_case hol_ctxt res_T)
    1.99 -                     (length xs' downto 2 ~~ xs'')
   1.100 -       end
   1.101 -     else
   1.102 -       Const (@{const_name undefined}, dataT --> res_T) $ Bound 0
   1.103 -       |> fold_rev (add_constr_case hol_ctxt res_T)
   1.104 -                   (length xs' downto 1 ~~ xs'))
   1.105 +    constr_case_body thy (1, x)
   1.106 +    |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs')
   1.107      |> fold_rev (curry absdummy) (func_Ts @ [dataT])
   1.108    end
   1.109  
   1.110 @@ -2032,8 +2018,7 @@
   1.111    | Type ("*", Ts) => fold (add_ground_types hol_ctxt) Ts accum
   1.112    | Type (@{type_name itself}, [T1]) => add_ground_types hol_ctxt T1 accum
   1.113    | Type (_, Ts) =>
   1.114 -    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} ::
   1.115 -                      @{typ \<xi>} :: accum) T then
   1.116 +    if member (op =) (@{typ prop} :: @{typ bool} :: @{typ unit} :: accum) T then
   1.117        accum
   1.118      else
   1.119        T :: accum

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Feb 12 21:27:06 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Sat Feb 13 11:56:06 2010 +0100
     2.3 @@ -318,7 +318,8 @@
     2.4             else
     2.5               [KK.TupleSet [],
     2.6                if T1 = T2 andalso epsilon > delta andalso
     2.7 -                 not (datatype_spec dtypes T1 |> the |> #co) then
     2.8 +                 (datatype_spec dtypes T1 |> the |> pairf #co #standard)
     2.9 +                 = (false, true) then
    2.10                  index_seq delta (epsilon - delta)
    2.11                  |> map (fn j =>
    2.12                             KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
    2.13 @@ -763,6 +764,7 @@
    2.14  (* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
    2.15     -> dtype_spec -> nfa_entry option *)
    2.16  fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE
    2.17 +  | nfa_entry_for_datatype _ _ _ _ {standard = false, ...} = NONE
    2.18    | nfa_entry_for_datatype _ _ _ _ {deep = false, ...} = NONE
    2.19    | nfa_entry_for_datatype hol_ctxt kk rel_table dtypes {typ, constrs, ...} =
    2.20      SOME (typ, maps (nfa_transitions_for_constr hol_ctxt kk rel_table dtypes

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Feb 12 21:27:06 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sat Feb 13 11:56:06 2010 +0100
     3.3 @@ -53,6 +53,8 @@
     3.4  val base_mixfix = "_\<^bsub>base\<^esub>"
     3.5  val step_mixfix = "_\<^bsub>step\<^esub>"
     3.6  val abs_mixfix = "\<guillemotleft>_\<guillemotright>"
     3.7 +val cyclic_co_val_name = "\<omega>"
     3.8 +val cyclic_non_std_type_name = "\<xi>"
     3.9  val opt_flag = nitpick_prefix ^ "opt"
    3.10  val non_opt_flag = nitpick_prefix ^ "non_opt"
    3.11  
    3.12 @@ -397,7 +399,7 @@
    3.13          else case datatype_spec datatypes T of
    3.14            NONE => nth_atom pool for_auto T j k
    3.15          | SOME {deep = false, ...} => nth_atom pool for_auto T j k
    3.16 -        | SOME {co, constrs, ...} =>
    3.17 +        | SOME {co, standard, constrs, ...} =>
    3.18            let
    3.19              (* styp -> int list *)
    3.20              fun tuples_for_const (s, T) =
    3.21 @@ -428,8 +430,9 @@
    3.22                map (map_filter (fn js => if hd js = real_j then SOME (tl js)
    3.23                                          else NONE)) sel_jsss
    3.24              val uncur_arg_Ts = binder_types constr_T
    3.25 +            val maybe_cyclic = co orelse not standard
    3.26            in
    3.27 -            if co andalso member (op =) seen (T, j) then
    3.28 +            if maybe_cyclic andalso member (op =) seen (T, j) then
    3.29                Var (var ())
    3.30              else if constr_s = @{const_name Word} then
    3.31                HOLogic.mk_number
    3.32 @@ -437,7 +440,7 @@
    3.33                    (value_of_bits (the_single arg_jsss))
    3.34              else
    3.35                let
    3.36 -                val seen = seen |> co ? cons (T, j)
    3.37 +                val seen = seen |> maybe_cyclic ? cons (T, j)
    3.38                  val ts =
    3.39                    if length arg_Ts = 0 then
    3.40                      []
    3.41 @@ -469,19 +472,20 @@
    3.42                            (is_abs_fun thy constr_x orelse
    3.43                             constr_s = @{const_name Quot}) then
    3.44                      Const (abs_name, constr_T) $ the_single ts
    3.45 -                  else if not for_auto andalso
    3.46 -                          constr_s = @{const_name Silly} then
    3.47 -                    Const (fst (dest_Const (the_single ts)), T)
    3.48                    else
    3.49                      list_comb (Const constr_x, ts)
    3.50                in
    3.51 -                if co then
    3.52 +                if maybe_cyclic then
    3.53                    let val var = var () in
    3.54                      if exists_subterm (curry (op =) (Var var)) t then
    3.55 -                      Const (@{const_name The}, (T --> bool_T) --> T)
    3.56 -                      $ Abs ("\<omega>", T,
    3.57 -                             Const (@{const_name "op ="}, T --> T --> bool_T)
    3.58 -                             $ Bound 0 $ abstract_over (Var var, t))
    3.59 +                      if co then
    3.60 +                        Const (@{const_name The}, (T --> bool_T) --> T)
    3.61 +                        $ Abs (cyclic_co_val_name, T,
    3.62 +                               Const (@{const_name "op ="}, T --> T --> bool_T)
    3.63 +                               $ Bound 0 $ abstract_over (Var var, t))
    3.64 +                      else
    3.65 +                        nth_atom pool for_auto
    3.66 +                                 (Type (cyclic_non_std_type_name, [])) j k
    3.67                      else
    3.68                        t
    3.69                    end
    3.70 @@ -682,7 +686,8 @@
    3.71      (* typ -> dtype_spec list *)
    3.72      fun integer_datatype T =
    3.73        [{typ = T, card = card_of_type card_assigns T, co = false,
    3.74 -        complete = false, concrete = true, deep = true, constrs = []}]
    3.75 +        standard = true, complete = false, concrete = true, deep = true,
    3.76 +        constrs = []}]
    3.77        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    3.78      val (codatatypes, datatypes) =
    3.79        datatypes |> filter #deep |> List.partition #co

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Fri Feb 12 21:27:06 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Sat Feb 13 11:56:06 2010 +0100
     4.3 @@ -22,6 +22,7 @@
     4.4      typ: typ,
     4.5      card: int,
     4.6      co: bool,
     4.7 +    standard: bool,
     4.8      complete: bool,
     4.9      concrete: bool,
    4.10      deep: bool,
    4.11 @@ -71,6 +72,7 @@
    4.12    typ: typ,
    4.13    card: int,
    4.14    co: bool,
    4.15 +  standard: bool,
    4.16    complete: bool,
    4.17    concrete: bool,
    4.18    deep: bool,
    4.19 @@ -466,6 +468,7 @@
    4.20    let
    4.21      val deep = member (op =) deep_dataTs T
    4.22      val co = is_codatatype thy T
    4.23 +    val standard = is_standard_datatype hol_ctxt T
    4.24      val xs = boxed_datatype_constrs hol_ctxt T
    4.25      val self_recs = map (is_self_recursive_constr_type o snd) xs
    4.26      val (num_self_recs, num_non_self_recs) =
    4.27 @@ -481,8 +484,8 @@
    4.28                                  num_non_self_recs)
    4.29                 (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
    4.30    in
    4.31 -    {typ = T, card = card, co = co, complete = complete, concrete = concrete,
    4.32 -     deep = deep, constrs = constrs}
    4.33 +    {typ = T, card = card, co = co, standard = standard, complete = complete,
    4.34 +     concrete = concrete, deep = deep, constrs = constrs}
    4.35    end
    4.36  
    4.37  (* int -> int *)