src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 55890 bd7927cca152
parent 55889 6bfbec3dff62
child 56220 4c43a2881b25
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -367,7 +367,7 @@
     1.4  and reconstruct_term maybe_opt unfold pool
     1.5          (wacky_names as ((maybe_name, abs_name), _))
     1.6          (scope as {hol_ctxt as {thy, ctxt, ...}, binarize, card_assigns, bits,
     1.7 -                   datatypes, ofs, ...})
     1.8 +                   data_types, ofs, ...})
     1.9          atomss sel_names rel_table bounds =
    1.10    let
    1.11      val for_auto = (maybe_name = "")
    1.12 @@ -403,7 +403,7 @@
    1.13          val empty_const = Const (@{const_abbrev Set.empty}, set_T)
    1.14          val insert_const = Const (@{const_name insert}, T --> set_T --> set_T)
    1.15          fun aux [] =
    1.16 -            if maybe_opt andalso not (is_complete_type datatypes false T) then
    1.17 +            if maybe_opt andalso not (is_complete_type data_types false T) then
    1.18                insert_const $ Const (unrep (), T) $ empty_const
    1.19              else
    1.20                empty_const
    1.21 @@ -432,7 +432,7 @@
    1.22                 Const (@{const_name None}, _) => aux' tps
    1.23               | _ => update_const $ aux' tps $ t1 $ t2)
    1.24          fun aux tps =
    1.25 -          if maybe_opt andalso not (is_complete_type datatypes false T1) then
    1.26 +          if maybe_opt andalso not (is_complete_type data_types false T1) then
    1.27              update_const $ aux' tps $ Const (unrep (), T1)
    1.28              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
    1.29            else
    1.30 @@ -463,7 +463,7 @@
    1.31               | Const (s, Type (@{type_name fun}, [T1, T2])) =>
    1.32                 if s = opt_flag orelse s = non_opt_flag then
    1.33                   Abs ("x", T1,
    1.34 -                      Const (if is_complete_type datatypes false T1 then
    1.35 +                      Const (if is_complete_type data_types false T1 then
    1.36                                 irrelevant
    1.37                               else
    1.38                                 unknown, T2))
    1.39 @@ -525,7 +525,7 @@
    1.40            HOLogic.mk_number nat_T (k - j - 1)
    1.41          else if T = @{typ bisim_iterator} then
    1.42            HOLogic.mk_number nat_T j
    1.43 -        else case datatype_spec datatypes T of
    1.44 +        else case data_type_spec data_types T of
    1.45            NONE => nth_atom thy atomss pool for_auto T j
    1.46          | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
    1.47          | SOME {co, constrs, ...} =>
    1.48 @@ -888,7 +888,7 @@
    1.49                        simp_table, psimp_table, choice_spec_table, intro_table,
    1.50                        ground_thm_table, ersatz_table, skolems, special_funs,
    1.51                        unrolled_preds, wf_cache, constr_cache}, binarize,
    1.52 -                      card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
    1.53 +                      card_assigns, bits, bisim_depth, data_types, ofs} : scope)
    1.54          formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
    1.55          rel_table bounds =
    1.56    let
    1.57 @@ -910,15 +910,16 @@
    1.58         wf_cache = wf_cache, constr_cache = constr_cache}
    1.59      val scope =
    1.60        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    1.61 -       bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    1.62 +       bits = bits, bisim_depth = bisim_depth, data_types = data_types,
    1.63 +       ofs = ofs}
    1.64      fun term_for_rep maybe_opt unfold =
    1.65        reconstruct_term maybe_opt unfold pool wacky_names scope atomss
    1.66                         sel_names rel_table bounds
    1.67      val all_values =
    1.68        all_values_of_type pool wacky_names scope atomss sel_names rel_table
    1.69                           bounds
    1.70 -    fun is_codatatype_wellformed (cos : datatype_spec list)
    1.71 -                                 ({typ, card, ...} : datatype_spec) =
    1.72 +    fun is_codatatype_wellformed (cos : data_type_spec list)
    1.73 +                                 ({typ, card, ...} : data_type_spec) =
    1.74        let
    1.75          val ts = all_values card typ
    1.76          val max_depth = Integer.sum (map #card cos)
    1.77 @@ -950,7 +951,7 @@
    1.78              [Syntax.pretty_term ctxt t1, Pretty.str oper,
    1.79               Syntax.pretty_term ctxt t2])
    1.80        end
    1.81 -    fun pretty_for_datatype ({typ, card, complete, ...} : datatype_spec) =
    1.82 +    fun pretty_for_data_type ({typ, card, complete, ...} : data_type_spec) =
    1.83        Pretty.block (Pretty.breaks
    1.84            (pretty_for_type ctxt typ ::
    1.85             (case typ of
    1.86 @@ -962,24 +963,18 @@
    1.87                  (map (Syntax.pretty_term ctxt) (all_values card typ) @
    1.88                   (if fun_from_pair complete false then []
    1.89                    else [Pretty.str (unrep ())]))]))
    1.90 -    fun integer_datatype T =
    1.91 +    fun integer_data_type T =
    1.92        [{typ = T, card = card_of_type card_assigns T, co = false,
    1.93          self_rec = true, complete = (false, false), concrete = (true, true),
    1.94          deep = true, constrs = []}]
    1.95        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    1.96 -    val (codatatypes, datatypes) =
    1.97 -      datatypes |> filter #deep |> List.partition #co
    1.98 -                ||> append (integer_datatype nat_T @ integer_datatype int_T)
    1.99 -    val block_of_datatypes =
   1.100 -      if show_types andalso not (null datatypes) then
   1.101 -        [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":")
   1.102 -                         (map pretty_for_datatype datatypes)]
   1.103 -      else
   1.104 -        []
   1.105 -    val block_of_codatatypes =
   1.106 -      if show_types andalso not (null codatatypes) then
   1.107 -        [Pretty.big_list ("Codatatype" ^ plural_s_for_list codatatypes ^ ":")
   1.108 -                         (map pretty_for_datatype codatatypes)]
   1.109 +    val data_types =
   1.110 +      data_types |> filter #deep
   1.111 +                 |> append (maps integer_data_type [nat_T, int_T])
   1.112 +    val block_of_data_types =
   1.113 +      if show_types andalso not (null data_types) then
   1.114 +        [Pretty.big_list ("Type" ^ plural_s_for_list data_types ^ ":")
   1.115 +                         (map pretty_for_data_type data_types)]
   1.116        else
   1.117          []
   1.118      fun block_of_names show title names =
   1.119 @@ -1010,9 +1005,10 @@
   1.120      val chunks = block_of_names true "Free variable" real_free_names @
   1.121                   block_of_names show_skolems "Skolem constant" skolem_names @
   1.122                   block_of_names true "Evaluated term" eval_names @
   1.123 -                 block_of_datatypes @ block_of_codatatypes @
   1.124 +                 block_of_data_types @
   1.125                   block_of_names show_consts "Constant"
   1.126                                  noneval_nonskolem_nonsel_names
   1.127 +    val codatatypes = filter #co data_types;
   1.128    in
   1.129      (Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
   1.130                      else chunks),