distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
authorblanchet
Mon Dec 14 16:48:49 2009 +0100 (2009-12-14)
changeset 34123c4988215a691
parent 34122 9e6326db46b4
child 34124 c4628a1dcf75
distinguish better between "complete" (vs. incomplete) types and "concrete" (vs. abstract) types in Nitpick;
this improves Nitpick's precision in some cases (e.g. higher-order constructors) and reflects a better understanding of what's going on
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 14 12:31:00 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 14 16:48:49 2009 +0100
     1.3 @@ -162,7 +162,7 @@
     1.4    | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS
     1.5  
     1.6  (* ('a * bool option) list -> bool *)
     1.7 -fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
     1.8 +fun none_true assigns = forall (not_equal (SOME true) o snd) assigns
     1.9  
    1.10  val syntactic_sorts =
    1.11    @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
    1.12 @@ -413,9 +413,9 @@
    1.13                                         string_of_int j0))
    1.14                           (Typtab.dest ofs)
    1.15  *)
    1.16 -        val all_precise = forall (is_precise_type datatypes) Ts
    1.17 +        val all_exact = forall (is_exact_type datatypes) Ts
    1.18          (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
    1.19 -        val repify_consts = choose_reps_for_consts scope all_precise
    1.20 +        val repify_consts = choose_reps_for_consts scope all_exact
    1.21          val main_j0 = offset_of_type ofs bool_T
    1.22          val (nat_card, nat_j0) = spec_of_type scope nat_T
    1.23          val (int_card, int_j0) = spec_of_type scope int_T
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Dec 14 12:31:00 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Dec 14 16:48:49 2009 +0100
     2.3 @@ -111,7 +111,7 @@
     2.4    val boxed_constr_for_sel : extended_context -> styp -> styp
     2.5    val card_of_type : (typ * int) list -> typ -> int
     2.6    val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
     2.7 -  val bounded_precise_card_of_type :
     2.8 +  val bounded_exact_card_of_type :
     2.9      extended_context -> int -> int -> (typ * int) list -> typ -> int
    2.10    val is_finite_type : extended_context -> typ -> bool
    2.11    val all_axioms_of : theory -> term list * term list * term list
    2.12 @@ -897,42 +897,42 @@
    2.13           end
    2.14  
    2.15  (* (typ * int) list -> typ -> int *)
    2.16 -fun card_of_type asgns (Type ("fun", [T1, T2])) =
    2.17 -    reasonable_power (card_of_type asgns T2) (card_of_type asgns T1)
    2.18 -  | card_of_type asgns (Type ("*", [T1, T2])) =
    2.19 -    card_of_type asgns T1 * card_of_type asgns T2
    2.20 +fun card_of_type assigns (Type ("fun", [T1, T2])) =
    2.21 +    reasonable_power (card_of_type assigns T2) (card_of_type assigns T1)
    2.22 +  | card_of_type assigns (Type ("*", [T1, T2])) =
    2.23 +    card_of_type assigns T1 * card_of_type assigns T2
    2.24    | card_of_type _ (Type (@{type_name itself}, _)) = 1
    2.25    | card_of_type _ @{typ prop} = 2
    2.26    | card_of_type _ @{typ bool} = 2
    2.27    | card_of_type _ @{typ unit} = 1
    2.28 -  | card_of_type asgns T =
    2.29 -    case AList.lookup (op =) asgns T of
    2.30 +  | card_of_type assigns T =
    2.31 +    case AList.lookup (op =) assigns T of
    2.32        SOME k => k
    2.33      | NONE => if T = @{typ bisim_iterator} then 0
    2.34                else raise TYPE ("Nitpick_HOL.card_of_type", [T], [])
    2.35  (* int -> (typ * int) list -> typ -> int *)
    2.36 -fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) =
    2.37 +fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) =
    2.38      let
    2.39 -      val k1 = bounded_card_of_type max default_card asgns T1
    2.40 -      val k2 = bounded_card_of_type max default_card asgns T2
    2.41 +      val k1 = bounded_card_of_type max default_card assigns T1
    2.42 +      val k2 = bounded_card_of_type max default_card assigns T2
    2.43      in
    2.44        if k1 = max orelse k2 = max then max
    2.45        else Int.min (max, reasonable_power k2 k1)
    2.46      end
    2.47 -  | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) =
    2.48 +  | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) =
    2.49      let
    2.50 -      val k1 = bounded_card_of_type max default_card asgns T1
    2.51 -      val k2 = bounded_card_of_type max default_card asgns T2
    2.52 +      val k1 = bounded_card_of_type max default_card assigns T1
    2.53 +      val k2 = bounded_card_of_type max default_card assigns T2
    2.54      in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end
    2.55 -  | bounded_card_of_type max default_card asgns T =
    2.56 +  | bounded_card_of_type max default_card assigns T =
    2.57      Int.min (max, if default_card = ~1 then
    2.58 -                    card_of_type asgns T
    2.59 +                    card_of_type assigns T
    2.60                    else
    2.61 -                    card_of_type asgns T
    2.62 +                    card_of_type assigns T
    2.63                      handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
    2.64                             default_card)
    2.65  (* extended_context -> int -> (typ * int) list -> typ -> int *)
    2.66 -fun bounded_precise_card_of_type ext_ctxt max default_card asgns T =
    2.67 +fun bounded_exact_card_of_type ext_ctxt max default_card assigns T =
    2.68    let
    2.69      (* typ list -> typ -> int *)
    2.70      fun aux avoid T =
    2.71 @@ -975,12 +975,13 @@
    2.72                else Integer.sum constr_cards
    2.73              end)
    2.74         | _ => raise SAME ())
    2.75 -      handle SAME () => AList.lookup (op =) asgns T |> the_default default_card
    2.76 +      handle SAME () =>
    2.77 +             AList.lookup (op =) assigns T |> the_default default_card
    2.78    in Int.min (max, aux [] T) end
    2.79  
    2.80  (* extended_context -> typ -> bool *)
    2.81  fun is_finite_type ext_ctxt =
    2.82 -  not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 []
    2.83 +  not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 []
    2.84  
    2.85  (* term -> bool *)
    2.86  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 12:31:00 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Dec 14 16:48:49 2009 +0100
     3.3 @@ -238,7 +238,7 @@
     3.4                                    [T1, T1 --> T2] ---> T1 --> T2)
     3.5          (* (term * term) list -> term *)
     3.6          fun aux [] =
     3.7 -            if maybe_opt andalso not (is_precise_type datatypes T1) then
     3.8 +            if maybe_opt andalso not (is_complete_type datatypes T1) then
     3.9                insert_const $ Const (unrep, T1) $ empty_const
    3.10              else
    3.11                empty_const
    3.12 @@ -262,7 +262,7 @@
    3.13                 Const (@{const_name None}, _) => aux' ps
    3.14               | _ => update_const $ aux' ps $ t1 $ t2)
    3.15          fun aux ps =
    3.16 -          if not (is_precise_type datatypes T1) then
    3.17 +          if not (is_complete_type datatypes T1) then
    3.18              update_const $ aux' ps $ Const (unrep, T1)
    3.19              $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
    3.20            else
    3.21 @@ -601,17 +601,17 @@
    3.22               Pretty.str oper, Syntax.pretty_term ctxt t2])
    3.23        end
    3.24      (* dtype_spec -> Pretty.T *)
    3.25 -    fun pretty_for_datatype ({typ, card, precise, ...} : dtype_spec) =
    3.26 +    fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) =
    3.27        Pretty.block (Pretty.breaks
    3.28            [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=",
    3.29             Pretty.enum "," "{" "}"
    3.30                 (map (Syntax.pretty_term ctxt o nth_value_of_type typ card)
    3.31                      (index_seq 0 card) @
    3.32 -                (if precise then [] else [Pretty.str unrep]))])
    3.33 +                (if complete then [] else [Pretty.str unrep]))])
    3.34      (* typ -> dtype_spec list *)
    3.35      fun integer_datatype T =
    3.36        [{typ = T, card = card_of_type card_assigns T, co = false,
    3.37 -        precise = false, shallow = false, constrs = []}]
    3.38 +        complete = false, concrete = true, shallow = false, constrs = []}]
    3.39        handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
    3.40      val (codatatypes, datatypes) =
    3.41        datatypes |> filter_out #shallow
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 14 12:31:00 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 14 16:48:49 2009 +0100
     4.3 @@ -466,11 +466,11 @@
     4.4      PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, []))
     4.5  
     4.6  (* var -> (int -> bool option) -> literal list -> literal list *)
     4.7 -fun literals_from_assignments max_var asgns lits =
     4.8 +fun literals_from_assignments max_var assigns lits =
     4.9    fold (fn x => fn accum =>
    4.10             if AList.defined (op =) lits x then
    4.11               accum
    4.12 -           else case asgns x of
    4.13 +           else case assigns x of
    4.14               SOME b => (x, sign_from_bool b) :: accum
    4.15             | NONE => accum) (max_var downto 1) lits
    4.16  
    4.17 @@ -505,10 +505,13 @@
    4.18        val prop = PropLogic.all (map prop_for_literal lits @
    4.19                                  map prop_for_comp comps @
    4.20                                  map prop_for_sign_expr sexps)
    4.21 +      (* use the first ML solver (to avoid startup overhead) *)
    4.22 +      val solvers = !SatSolver.solvers
    4.23 +                    |> filter (member (op =) ["dptsat", "dpll"] o fst)
    4.24      in
    4.25 -      case SatSolver.invoke_solver "dpll" prop of
    4.26 -        SatSolver.SATISFIABLE asgns =>
    4.27 -        SOME (literals_from_assignments max_var asgns lits
    4.28 +      case snd (hd solvers) prop of
    4.29 +        SatSolver.SATISFIABLE assigns =>
    4.30 +        SOME (literals_from_assignments max_var assigns lits
    4.31                |> tap print_solution)
    4.32        | _ => NONE
    4.33      end
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Dec 14 12:31:00 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Dec 14 16:48:49 2009 +0100
     5.3 @@ -708,14 +708,14 @@
     5.4  (* scope -> bool -> nut -> nut list * rep NameTable.table
     5.5     -> nut list * rep NameTable.table *)
     5.6  fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes,
     5.7 -                                    ofs, ...}) all_precise v (vs, table) =
     5.8 +                                    ofs, ...}) all_exact v (vs, table) =
     5.9    let
    5.10      val x as (s, T) = (nickname_of v, type_of v)
    5.11      val R = (if is_abs_fun thy x then
    5.12                 rep_for_abs_fun
    5.13               else if is_rep_fun thy x then
    5.14                 Func oo best_non_opt_symmetric_reps_for_fun_type
    5.15 -             else if all_precise orelse is_skolem_name v
    5.16 +             else if all_exact orelse is_skolem_name v
    5.17                       orelse member (op =) [@{const_name undefined_fast_The},
    5.18                                             @{const_name undefined_fast_Eps},
    5.19                                             @{const_name bisim},
    5.20 @@ -737,8 +737,8 @@
    5.21    fold (choose_rep_for_free_var scope) vs ([], table)
    5.22  (* scope -> bool -> nut list -> rep NameTable.table
    5.23     -> nut list * rep NameTable.table *)
    5.24 -fun choose_reps_for_consts scope all_precise vs table =
    5.25 -  fold (choose_rep_for_const scope all_precise) vs ([], table)
    5.26 +fun choose_reps_for_consts scope all_exact vs table =
    5.27 +  fold (choose_rep_for_const scope all_exact) vs ([], table)
    5.28  
    5.29  (* scope -> styp -> int -> nut list * rep NameTable.table
    5.30     -> nut list * rep NameTable.table *)
    5.31 @@ -998,7 +998,7 @@
    5.32              if is_opt_rep R then
    5.33                triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
    5.34              else if opt andalso polar = Pos andalso
    5.35 -                    not (is_fully_comparable_type datatypes (type_of u1)) then
    5.36 +                    not (is_concrete_type datatypes (type_of u1)) then
    5.37                Cst (False, T, Formula Pos)
    5.38              else
    5.39                s_op2 Subset T R u1 u2
    5.40 @@ -1024,7 +1024,7 @@
    5.41                else opt_opt_case ()
    5.42            in
    5.43              if liberal orelse polar = Neg
    5.44 -               orelse is_fully_comparable_type datatypes (type_of u1) then
    5.45 +               orelse is_concrete_type datatypes (type_of u1) then
    5.46                case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
    5.47                  (true, true) => opt_opt_case ()
    5.48                | (true, false) => hybrid_case u1'
    5.49 @@ -1127,7 +1127,7 @@
    5.50                  let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
    5.51                    if def
    5.52                       orelse (liberal andalso (polar = Pos) = (oper = All))
    5.53 -                     orelse is_precise_type datatypes (type_of u1) then
    5.54 +                     orelse is_complete_type datatypes (type_of u1) then
    5.55                      quant_u
    5.56                    else
    5.57                      let
    5.58 @@ -1170,7 +1170,7 @@
    5.59                        else unopt_R |> opt ? opt_rep ofs T
    5.60                val u = Op2 (oper, T, R, u1', sub u2)
    5.61              in
    5.62 -              if is_precise_type datatypes T orelse not opt1 then
    5.63 +              if is_complete_type datatypes T orelse not opt1 then
    5.64                  u
    5.65                else
    5.66                  let
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Dec 14 12:31:00 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Mon Dec 14 16:48:49 2009 +0100
     6.3 @@ -299,7 +299,7 @@
     6.4       | z => Func z)
     6.5    | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
     6.6  fun best_set_rep_for_type (scope as {datatypes, ...}) T =
     6.7 -  (if is_precise_type datatypes T then best_non_opt_set_rep_for_type
     6.8 +  (if is_exact_type datatypes T then best_non_opt_set_rep_for_type
     6.9     else best_opt_set_rep_for_type) scope T
    6.10  fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
    6.11                                               (Type ("fun", [T1, T2])) =
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Dec 14 12:31:00 2009 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Dec 14 16:48:49 2009 +0100
     7.3 @@ -22,7 +22,8 @@
     7.4      typ: typ,
     7.5      card: int,
     7.6      co: bool,
     7.7 -    precise: bool,
     7.8 +    complete: bool,
     7.9 +    concrete: bool,
    7.10      shallow: bool,
    7.11      constrs: constr_spec list}
    7.12  
    7.13 @@ -35,8 +36,9 @@
    7.14  
    7.15    val datatype_spec : dtype_spec list -> typ -> dtype_spec option
    7.16    val constr_spec : dtype_spec list -> styp -> constr_spec
    7.17 -  val is_precise_type : dtype_spec list -> typ -> bool
    7.18 -  val is_fully_comparable_type : dtype_spec list -> typ -> bool
    7.19 +  val is_complete_type : dtype_spec list -> typ -> bool
    7.20 +  val is_concrete_type : dtype_spec list -> typ -> bool
    7.21 +  val is_exact_type : dtype_spec list -> typ -> bool
    7.22    val offset_of_type : int Typtab.table -> typ -> int
    7.23    val spec_of_type : scope -> typ -> int * int
    7.24    val pretties_for_scope : scope -> bool -> Pretty.T list
    7.25 @@ -67,7 +69,8 @@
    7.26    typ: typ,
    7.27    card: int,
    7.28    co: bool,
    7.29 -  precise: bool,
    7.30 +  complete: bool,
    7.31 +  concrete: bool,
    7.32    shallow: bool,
    7.33    constrs: constr_spec list}
    7.34  
    7.35 @@ -96,17 +99,20 @@
    7.36      | NONE => constr_spec dtypes x
    7.37  
    7.38  (* dtype_spec list -> typ -> bool *)
    7.39 -fun is_precise_type dtypes (Type ("fun", Ts)) =
    7.40 -    forall (is_precise_type dtypes) Ts
    7.41 -  | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts
    7.42 -  | is_precise_type dtypes T =
    7.43 -    not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T))
    7.44 +fun is_complete_type dtypes (Type ("fun", [T1, T2])) =
    7.45 +    is_concrete_type dtypes T1 andalso is_complete_type dtypes T2
    7.46 +  | is_complete_type dtypes (Type ("*", Ts)) =
    7.47 +    forall (is_complete_type dtypes) Ts
    7.48 +  | is_complete_type dtypes T =
    7.49 +    not (is_integer_type T) andalso #complete (the (datatype_spec dtypes T))
    7.50      handle Option.Option => true
    7.51 -fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) =
    7.52 -    is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2
    7.53 -  | is_fully_comparable_type dtypes (Type ("*", Ts)) =
    7.54 -    forall (is_fully_comparable_type dtypes) Ts
    7.55 -  | is_fully_comparable_type _ _ = true
    7.56 +and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
    7.57 +    is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
    7.58 +  | is_concrete_type dtypes (Type ("*", Ts)) =
    7.59 +    forall (is_concrete_type dtypes) Ts
    7.60 +  | is_concrete_type dtypes T =
    7.61 +    #concrete (the (datatype_spec dtypes T)) handle Option.Option => true
    7.62 +fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes
    7.63  
    7.64  (* int Typtab.table -> typ -> int *)
    7.65  fun offset_of_type ofs T =
    7.66 @@ -124,11 +130,11 @@
    7.67  fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns,
    7.68                                  bisim_depth, datatypes, ...} : scope) =
    7.69    let
    7.70 -    val (iter_asgns, card_asgns) =
    7.71 +    val (iter_assigns, card_assigns) =
    7.72        card_assigns |> filter_out (curry (op =) @{typ bisim_iterator} o fst)
    7.73                     |> List.partition (is_fp_iterator_type o fst)
    7.74 -    val (unimportant_card_asgns, important_card_asgns) =
    7.75 -      card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
    7.76 +    val (unimportant_card_assigns, important_card_assigns) =
    7.77 +      card_assigns |> List.partition ((is_integer_type orf is_datatype thy) o fst)
    7.78      val cards =
    7.79        map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^
    7.80                          string_of_int k)
    7.81 @@ -145,13 +151,13 @@
    7.82        map (fn (T, k) =>
    7.83                quote (Syntax.string_of_term ctxt
    7.84                           (Const (const_for_iterator_type T))) ^ " = " ^
    7.85 -              string_of_int (k - 1)) iter_asgns
    7.86 +              string_of_int (k - 1)) iter_assigns
    7.87      fun bisims () =
    7.88        if bisim_depth < 0 andalso forall (not o #co) datatypes then []
    7.89        else ["bisim_depth = " ^ string_of_int bisim_depth]
    7.90    in
    7.91      setmp_show_all_types
    7.92 -        (fn () => (cards important_card_asgns, cards unimportant_card_asgns,
    7.93 +        (fn () => (cards important_card_assigns, cards unimportant_card_assigns,
    7.94                     maxes (), iters (), bisims ())) ()
    7.95    end
    7.96  
    7.97 @@ -204,52 +210,52 @@
    7.98  fun project_block (column, block) = map (project_row column) block
    7.99  
   7.100  (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *)
   7.101 -fun lookup_ints_assign eq asgns key =
   7.102 -  case triple_lookup eq asgns key of
   7.103 +fun lookup_ints_assign eq assigns key =
   7.104 +  case triple_lookup eq assigns key of
   7.105      SOME ks => ks
   7.106    | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "")
   7.107  (* theory -> (typ option * int list) list -> typ -> int list *)
   7.108 -fun lookup_type_ints_assign thy asgns T =
   7.109 -  map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T)
   7.110 +fun lookup_type_ints_assign thy assigns T =
   7.111 +  map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T)
   7.112    handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
   7.113           raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], [])
   7.114  (* theory -> (styp option * int list) list -> styp -> int list *)
   7.115 -fun lookup_const_ints_assign thy asgns x =
   7.116 -  lookup_ints_assign (const_match thy) asgns x
   7.117 +fun lookup_const_ints_assign thy assigns x =
   7.118 +  lookup_ints_assign (const_match thy) assigns x
   7.119    handle ARG ("Nitpick_Scope.lookup_ints_assign", _) =>
   7.120           raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x])
   7.121  
   7.122  (* theory -> (styp option * int list) list -> styp -> row option *)
   7.123 -fun row_for_constr thy maxes_asgns constr =
   7.124 -  SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr)
   7.125 +fun row_for_constr thy maxes_assigns constr =
   7.126 +  SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr)
   7.127    handle TERM ("lookup_const_ints_assign", _) => NONE
   7.128  
   7.129  (* extended_context -> (typ option * int list) list
   7.130     -> (styp option * int list) list -> (styp option * int list) list -> int list
   7.131     -> typ -> block *)
   7.132 -fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns
   7.133 -                   bisim_depths T =
   7.134 +fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns
   7.135 +                   iters_assigns bisim_depths T =
   7.136    if T = @{typ bisim_iterator} then
   7.137      [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)]
   7.138    else if is_fp_iterator_type T then
   7.139      [(Card T, map (fn k => Int.max (0, k) + 1)
   7.140 -                  (lookup_const_ints_assign thy iters_asgns
   7.141 +                  (lookup_const_ints_assign thy iters_assigns
   7.142                                              (const_for_iterator_type T)))]
   7.143    else
   7.144 -    (Card T, lookup_type_ints_assign thy cards_asgns T) ::
   7.145 +    (Card T, lookup_type_ints_assign thy cards_assigns T) ::
   7.146      (case datatype_constrs ext_ctxt T of
   7.147         [_] => []
   7.148 -     | constrs => map_filter (row_for_constr thy maxes_asgns) constrs)
   7.149 +     | constrs => map_filter (row_for_constr thy maxes_assigns) constrs)
   7.150  
   7.151  (* extended_context -> (typ option * int list) list
   7.152     -> (styp option * int list) list -> (styp option * int list) list -> int list
   7.153     -> typ list -> typ list -> block list *)
   7.154 -fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths
   7.155 -                     mono_Ts nonmono_Ts =
   7.156 +fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns
   7.157 +                     bisim_depths mono_Ts nonmono_Ts =
   7.158    let
   7.159      (* typ -> block *)
   7.160 -    val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns
   7.161 -                                   bisim_depths
   7.162 +    val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns
   7.163 +                                   iters_assigns bisim_depths
   7.164      val mono_block = maps block_for mono_Ts
   7.165      val nonmono_blocks = map block_for nonmono_Ts
   7.166    in mono_block :: nonmono_blocks end
   7.167 @@ -290,117 +296,121 @@
   7.168  type scope_desc = (typ * int) list * (styp * int) list
   7.169  
   7.170  (* extended_context -> scope_desc -> typ * int -> bool *)
   7.171 -fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) =
   7.172 +fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns)
   7.173 +                                       (T, k) =
   7.174    case datatype_constrs ext_ctxt T of
   7.175      [] => false
   7.176    | xs =>
   7.177      let
   7.178 -      val precise_cards =
   7.179 +      val exact_cards =
   7.180          map (Integer.prod
   7.181 -             o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns)
   7.182 +             o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns)
   7.183               o binder_types o snd) xs
   7.184 -      val maxes = map (constr_max max_asgns) xs
   7.185 +      val maxes = map (constr_max max_assigns) xs
   7.186        (* int -> int -> int *)
   7.187        fun effective_max 0 ~1 = k
   7.188          | effective_max 0 max = max
   7.189          | effective_max card ~1 = card
   7.190          | effective_max card max = Int.min (card, max)
   7.191 -      val max = map2 effective_max precise_cards maxes |> Integer.sum
   7.192 +      val max = map2 effective_max exact_cards maxes |> Integer.sum
   7.193        (* unit -> int *)
   7.194        fun doms_card () =
   7.195 -        xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_asgns)
   7.196 +        xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns)
   7.197                     o binder_types o snd)
   7.198             |> Integer.sum
   7.199      in
   7.200        max < k
   7.201 -      orelse (forall (not_equal 0) precise_cards andalso doms_card () < k)
   7.202 +      orelse (forall (not_equal 0) exact_cards andalso doms_card () < k)
   7.203      end
   7.204      handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false
   7.205  
   7.206  (* extended_context -> scope_desc -> bool *)
   7.207  fun is_surely_inconsistent_scope_description ext_ctxt
   7.208 -                                             (desc as (card_asgns, _)) =
   7.209 -  exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns
   7.210 +                                             (desc as (card_assigns, _)) =
   7.211 +  exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns
   7.212  
   7.213  (* extended_context -> scope_desc -> (typ * int) list option *)
   7.214 -fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) =
   7.215 +fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) =
   7.216    let
   7.217      (* (typ * int) list -> (typ * int) list -> (typ * int) list option *)
   7.218      fun aux seen [] = SOME seen
   7.219        | aux seen ((T, 0) :: _) = NONE
   7.220 -      | aux seen ((T, k) :: asgns) =
   7.221 +      | aux seen ((T, k) :: assigns) =
   7.222          (if is_surely_inconsistent_scope_description ext_ctxt
   7.223 -                ((T, k) :: seen, max_asgns) then
   7.224 +                ((T, k) :: seen, max_assigns) then
   7.225             raise SAME ()
   7.226           else
   7.227 -           case aux ((T, k) :: seen) asgns of
   7.228 -             SOME asgns => SOME asgns
   7.229 +           case aux ((T, k) :: seen) assigns of
   7.230 +             SOME assigns => SOME assigns
   7.231             | NONE => raise SAME ())
   7.232 -        handle SAME () => aux seen ((T, k - 1) :: asgns)
   7.233 -  in aux [] (rev card_asgns) end
   7.234 +        handle SAME () => aux seen ((T, k - 1) :: assigns)
   7.235 +  in aux [] (rev card_assigns) end
   7.236  
   7.237  (* theory -> (typ * int) list -> typ * int -> typ * int *)
   7.238 -fun repair_iterator_assign thy asgns (T as Type (s, Ts), k) =
   7.239 +fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) =
   7.240      (T, if T = @{typ bisim_iterator} then
   7.241 -          let val co_cards = map snd (filter (is_codatatype thy o fst) asgns) in
   7.242 -            Int.min (k, Integer.sum co_cards)
   7.243 -          end
   7.244 +          let
   7.245 +            val co_cards = map snd (filter (is_codatatype thy o fst) assigns)
   7.246 +          in Int.min (k, Integer.sum co_cards) end
   7.247          else if is_fp_iterator_type T then
   7.248            case Ts of
   7.249              [] => 1
   7.250 -          | _ => bounded_card_of_type k ~1 asgns (foldr1 HOLogic.mk_prodT Ts)
   7.251 +          | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts)
   7.252          else
   7.253            k)
   7.254 -  | repair_iterator_assign _ _ asgn = asgn
   7.255 +  | repair_iterator_assign _ _ assign = assign
   7.256  
   7.257  (* row -> scope_desc -> scope_desc *)
   7.258 -fun add_row_to_scope_descriptor (kind, ks) (card_asgns, max_asgns) =
   7.259 +fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) =
   7.260    case kind of
   7.261 -    Card T => ((T, the_single ks) :: card_asgns, max_asgns)
   7.262 -  | Max x => (card_asgns, (x, the_single ks) :: max_asgns)
   7.263 +    Card T => ((T, the_single ks) :: card_assigns, max_assigns)
   7.264 +  | Max x => (card_assigns, (x, the_single ks) :: max_assigns)
   7.265  (* block -> scope_desc *)
   7.266  fun scope_descriptor_from_block block =
   7.267    fold_rev add_row_to_scope_descriptor block ([], [])
   7.268  (* extended_context -> block list -> int list -> scope_desc option *)
   7.269  fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns =
   7.270    let
   7.271 -    val (card_asgns, max_asgns) =
   7.272 +    val (card_assigns, max_assigns) =
   7.273        maps project_block (columns ~~ blocks) |> scope_descriptor_from_block
   7.274 -    val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the
   7.275 +    val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns)
   7.276 +                       |> the
   7.277    in
   7.278 -    SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns)
   7.279 +    SOME (map (repair_iterator_assign thy card_assigns) card_assigns,
   7.280 +          max_assigns)
   7.281    end
   7.282    handle Option.Option => NONE
   7.283  
   7.284  (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *)
   7.285 -fun offset_table_for_card_assigns thy asgns dtypes =
   7.286 +fun offset_table_for_card_assigns thy assigns dtypes =
   7.287    let
   7.288      (* int -> (int * int) list -> (typ * int) list -> int Typtab.table
   7.289         -> int Typtab.table *)
   7.290      fun aux next _ [] = Typtab.update_new (dummyT, next)
   7.291 -      | aux next reusable ((T, k) :: asgns) =
   7.292 +      | aux next reusable ((T, k) :: assigns) =
   7.293          if k = 1 orelse is_integer_type T then
   7.294 -          aux next reusable asgns
   7.295 +          aux next reusable assigns
   7.296          else if length (these (Option.map #constrs (datatype_spec dtypes T)))
   7.297                  > 1 then
   7.298 -          Typtab.update_new (T, next) #> aux (next + k) reusable asgns
   7.299 +          Typtab.update_new (T, next) #> aux (next + k) reusable assigns
   7.300          else
   7.301            case AList.lookup (op =) reusable k of
   7.302 -            SOME j0 => Typtab.update_new (T, j0) #> aux next reusable asgns
   7.303 +            SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns
   7.304            | NONE => Typtab.update_new (T, next)
   7.305 -                    #> aux (next + k) ((k, next) :: reusable) asgns
   7.306 -  in aux 0 [] asgns Typtab.empty end
   7.307 +                    #> aux (next + k) ((k, next) :: reusable) assigns
   7.308 +  in aux 0 [] assigns Typtab.empty end
   7.309  
   7.310  (* int -> (typ * int) list -> typ -> int *)
   7.311 -fun domain_card max card_asgns =
   7.312 -  Integer.prod o map (bounded_card_of_type max max card_asgns) o binder_types
   7.313 +fun domain_card max card_assigns =
   7.314 +  Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types
   7.315  
   7.316  (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp
   7.317     -> constr_spec list -> constr_spec list *)
   7.318 -fun add_constr_spec (card_asgns, max_asgns) co card sum_dom_cards num_self_recs
   7.319 -                    num_non_self_recs (self_rec, x as (s, T)) constrs =
   7.320 +fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards
   7.321 +                    num_self_recs num_non_self_recs (self_rec, x as (s, T))
   7.322 +                    constrs =
   7.323    let
   7.324 -    val max = constr_max max_asgns x
   7.325 +    val max = constr_max max_assigns x
   7.326      (* int -> int *)
   7.327      fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k)
   7.328      (* unit -> int *)
   7.329 @@ -412,7 +422,7 @@
   7.330          end
   7.331        else if not co andalso num_self_recs > 0 then
   7.332          if not self_rec andalso num_non_self_recs = 1
   7.333 -           andalso domain_card 2 card_asgns T = 1 then
   7.334 +           andalso domain_card 2 card_assigns T = 1 then
   7.335            {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}),
   7.336             total = true}
   7.337          else if s = @{const_name Cons} then
   7.338 @@ -421,7 +431,7 @@
   7.339            {delta = 0, epsilon = card, exclusive = false, total = false}
   7.340        else if card = sum_dom_cards (card + 1) then
   7.341          let val delta = next_delta () in
   7.342 -          {delta = delta, epsilon = delta + domain_card card card_asgns T,
   7.343 +          {delta = delta, epsilon = delta + domain_card card card_assigns T,
   7.344             exclusive = true, total = true}
   7.345          end
   7.346        else
   7.347 @@ -432,55 +442,62 @@
   7.348       explicit_max = max, total = total} :: constrs
   7.349    end
   7.350  
   7.351 +(* extended_context -> (typ * int) list -> typ -> bool *)
   7.352 +fun has_exact_card ext_ctxt card_assigns T =
   7.353 +  let val card = card_of_type card_assigns T in
   7.354 +    card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T
   7.355 +  end
   7.356 +
   7.357  (* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *)
   7.358  fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs
   7.359 -                                        (desc as (card_asgns, _)) (T, card) =
   7.360 +                                        (desc as (card_assigns, _)) (T, card) =
   7.361    let
   7.362      val shallow = member (op =) shallow_dataTs T
   7.363      val co = is_codatatype thy T
   7.364      val xs = boxed_datatype_constrs ext_ctxt T
   7.365      val self_recs = map (is_self_recursive_constr_type o snd) xs
   7.366      val (num_self_recs, num_non_self_recs) =
   7.367 -      List.partition (curry (op =) true) self_recs |> pairself length
   7.368 -    val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0
   7.369 -                                                       card_asgns T)
   7.370 +      List.partition I self_recs |> pairself length
   7.371 +    val complete = has_exact_card ext_ctxt card_assigns T
   7.372 +    val concrete = xs |> maps (binder_types o snd) |> maps binder_types
   7.373 +                      |> forall (has_exact_card ext_ctxt card_assigns)
   7.374      (* int -> int *)
   7.375      fun sum_dom_cards max =
   7.376 -      map (domain_card max card_asgns o snd) xs |> Integer.sum
   7.377 +      map (domain_card max card_assigns o snd) xs |> Integer.sum
   7.378      val constrs =
   7.379        fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs
   7.380                                  num_non_self_recs) (self_recs ~~ xs) []
   7.381    in
   7.382 -    {typ = T, card = card, co = co, precise = precise, shallow = shallow,
   7.383 -     constrs = constrs}
   7.384 +    {typ = T, card = card, co = co, complete = complete, concrete = concrete,
   7.385 +     shallow = shallow, constrs = constrs}
   7.386    end
   7.387  
   7.388  (* extended_context -> int -> typ list -> scope_desc -> scope *)
   7.389  fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs
   7.390 -                          (desc as (card_asgns, _)) =
   7.391 +                          (desc as (card_assigns, _)) =
   7.392    let
   7.393      val datatypes =
   7.394        map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc)
   7.395 -          (filter (is_datatype thy o fst) card_asgns)
   7.396 -    val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1
   7.397 +          (filter (is_datatype thy o fst) card_assigns)
   7.398 +    val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1
   7.399    in
   7.400 -    {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes,
   7.401 +    {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes,
   7.402       bisim_depth = bisim_depth,
   7.403       ofs = if sym_break <= 0 then Typtab.empty
   7.404 -           else offset_table_for_card_assigns thy card_asgns datatypes}
   7.405 +           else offset_table_for_card_assigns thy card_assigns datatypes}
   7.406    end
   7.407  
   7.408  (* theory -> typ list -> (typ option * int list) list
   7.409     -> (typ option * int list) list *)
   7.410  fun fix_cards_assigns_wrt_boxing _ _ [] = []
   7.411 -  | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_asgns) =
   7.412 +  | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) =
   7.413      (if is_fun_type T orelse is_pair_type T then
   7.414         Ts |> filter (curry (type_match thy o swap) T o unbox_type)
   7.415            |> map (rpair ks o SOME)
   7.416       else
   7.417 -       [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_asgns
   7.418 -  | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) =
   7.419 -    (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns
   7.420 +       [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_assigns
   7.421 +  | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) =
   7.422 +    (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_assigns
   7.423  
   7.424  val max_scopes = 4096
   7.425  val distinct_threshold = 512
   7.426 @@ -488,12 +505,12 @@
   7.427  (* extended_context -> int -> (typ option * int list) list
   7.428     -> (styp option * int list) list -> (styp option * int list) list -> int list
   7.429     -> typ list -> typ list -> typ list -> int * scope list *)
   7.430 -fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns
   7.431 -               iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
   7.432 +fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns
   7.433 +               iters_assigns bisim_depths mono_Ts nonmono_Ts shallow_dataTs =
   7.434    let
   7.435 -    val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns
   7.436 -    val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns
   7.437 -                                  bisim_depths mono_Ts nonmono_Ts
   7.438 +    val cards_assigns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_assigns
   7.439 +    val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns
   7.440 +                                  iters_assigns bisim_depths mono_Ts nonmono_Ts
   7.441      val ranks = map rank_of_block blocks
   7.442      val all = all_combinations_ordered_smartly (map (rpair 0) ranks)
   7.443      val head = take max_scopes all