src/HOL/Tools/Nitpick/nitpick_scope.ML
changeset 55888 cac1add157e8
parent 55628 8103021024c1
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4      {typ: typ,
     1.5       card: int,
     1.6       co: bool,
     1.7 -     standard: bool,
     1.8       self_rec: bool,
     1.9       complete: bool * bool,
    1.10       concrete: bool * bool,
    1.11 @@ -76,7 +75,6 @@
    1.12    {typ: typ,
    1.13     card: int,
    1.14     co: bool,
    1.15 -   standard: bool,
    1.16     self_rec: bool,
    1.17     complete: bool * bool,
    1.18     concrete: bool * bool,
    1.19 @@ -142,7 +140,7 @@
    1.20     handle TYPE ("Nitpick_HOL.card_of_type", _, _) => ~1, offset_of_type ofs T)
    1.21  
    1.22  fun quintuple_for_scope code_type code_term code_string
    1.23 -        ({hol_ctxt = {ctxt, stds, ...}, card_assigns, bits, bisim_depth,
    1.24 +        ({hol_ctxt = {ctxt, ...}, card_assigns, bits, bisim_depth,
    1.25           datatypes, ...} : scope) =
    1.26    let
    1.27      val boring_Ts = [@{typ unsigned_bit}, @{typ signed_bit},
    1.28 @@ -152,7 +150,7 @@
    1.29                     |> List.partition (is_fp_iterator_type o fst)
    1.30      val (secondary_card_assigns, primary_card_assigns) =
    1.31        card_assigns
    1.32 -      |> List.partition ((is_integer_type orf is_datatype ctxt stds) o fst)
    1.33 +      |> List.partition ((is_integer_type orf is_datatype ctxt) o fst)
    1.34      val cards =
    1.35        map (fn (T, k) =>
    1.36                [code_type ctxt T, code_string (" = " ^ string_of_int k)])
    1.37 @@ -433,13 +431,12 @@
    1.38                 card_assigns T
    1.39    end
    1.40  
    1.41 -fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, ctxt, stds, ...})
    1.42 +fun datatype_spec_from_scope_descriptor (hol_ctxt as {ctxt, ...})
    1.43          binarize deep_dataTs finitizable_dataTs (desc as (card_assigns, _))
    1.44          (T, card) =
    1.45    let
    1.46      val deep = member (op =) deep_dataTs T
    1.47      val co = is_codatatype ctxt T
    1.48 -    val standard = is_standard_datatype thy stds T
    1.49      val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
    1.50      val self_recs = map (is_self_recursive_constr_type o snd) xs
    1.51      val (num_self_recs, num_non_self_recs) =
    1.52 @@ -459,21 +456,21 @@
    1.53      fun sum_dom_cards max =
    1.54        map (domain_card max card_assigns o snd) xs |> Integer.sum
    1.55      val constrs =
    1.56 -      fold_rev (add_constr_spec desc (not co andalso standard) card
    1.57 -                                sum_dom_cards num_self_recs num_non_self_recs)
    1.58 +      fold_rev (add_constr_spec desc (not co) card sum_dom_cards num_self_recs
    1.59 +                                num_non_self_recs)
    1.60                 (sort (bool_ord o swap o pairself fst) (self_recs ~~ xs)) []
    1.61    in
    1.62 -    {typ = T, card = card, co = co, standard = standard, self_rec = self_rec,
    1.63 -     complete = complete, concrete = concrete, deep = deep, constrs = constrs}
    1.64 +    {typ = T, card = card, co = co, self_rec = self_rec, complete = complete,
    1.65 +     concrete = concrete, deep = deep, constrs = constrs}
    1.66    end
    1.67  
    1.68 -fun scope_from_descriptor (hol_ctxt as {ctxt, stds, ...}) binarize deep_dataTs
    1.69 +fun scope_from_descriptor (hol_ctxt as {ctxt, ...}) binarize deep_dataTs
    1.70                            finitizable_dataTs (desc as (card_assigns, _)) =
    1.71    let
    1.72      val datatypes =
    1.73        map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
    1.74                                                 finitizable_dataTs desc)
    1.75 -          (filter (is_datatype ctxt stds o fst) card_assigns)
    1.76 +          (filter (is_datatype ctxt o fst) card_assigns)
    1.77      val bits = card_of_type card_assigns @{typ signed_bit} - 1
    1.78                 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
    1.79                        card_of_type card_assigns @{typ unsigned_bit}