# HG changeset patch # User blanchet # Date 1260805729 -3600 # Node ID c4988215a691c9afb46429d27c503b8f04a55b86 # Parent 9e6326db46b413114f0077d8630ebf99680b5f2b 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 diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 14 16:48:49 2009 +0100 @@ -162,7 +162,7 @@ | passed_deadline (SOME time) = Time.compare (Time.now (), time) <> LESS (* ('a * bool option) list -> bool *) -fun none_true asgns = forall (not_equal (SOME true) o snd) asgns +fun none_true assigns = forall (not_equal (SOME true) o snd) assigns val syntactic_sorts = @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @ @@ -413,9 +413,9 @@ string_of_int j0)) (Typtab.dest ofs) *) - val all_precise = forall (is_precise_type datatypes) Ts + val all_exact = forall (is_exact_type datatypes) Ts (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *) - val repify_consts = choose_reps_for_consts scope all_precise + val repify_consts = choose_reps_for_consts scope all_exact val main_j0 = offset_of_type ofs bool_T val (nat_card, nat_j0) = spec_of_type scope nat_T val (int_card, int_j0) = spec_of_type scope int_T diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Dec 14 16:48:49 2009 +0100 @@ -111,7 +111,7 @@ val boxed_constr_for_sel : extended_context -> styp -> styp val card_of_type : (typ * int) list -> typ -> int val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int - val bounded_precise_card_of_type : + val bounded_exact_card_of_type : extended_context -> int -> int -> (typ * int) list -> typ -> int val is_finite_type : extended_context -> typ -> bool val all_axioms_of : theory -> term list * term list * term list @@ -897,42 +897,42 @@ end (* (typ * int) list -> typ -> int *) -fun card_of_type asgns (Type ("fun", [T1, T2])) = - reasonable_power (card_of_type asgns T2) (card_of_type asgns T1) - | card_of_type asgns (Type ("*", [T1, T2])) = - card_of_type asgns T1 * card_of_type asgns T2 +fun card_of_type assigns (Type ("fun", [T1, T2])) = + reasonable_power (card_of_type assigns T2) (card_of_type assigns T1) + | card_of_type assigns (Type ("*", [T1, T2])) = + card_of_type assigns T1 * card_of_type assigns T2 | card_of_type _ (Type (@{type_name itself}, _)) = 1 | card_of_type _ @{typ prop} = 2 | card_of_type _ @{typ bool} = 2 | card_of_type _ @{typ unit} = 1 - | card_of_type asgns T = - case AList.lookup (op =) asgns T of + | card_of_type assigns T = + case AList.lookup (op =) assigns T of SOME k => k | NONE => if T = @{typ bisim_iterator} then 0 else raise TYPE ("Nitpick_HOL.card_of_type", [T], []) (* int -> (typ * int) list -> typ -> int *) -fun bounded_card_of_type max default_card asgns (Type ("fun", [T1, T2])) = +fun bounded_card_of_type max default_card assigns (Type ("fun", [T1, T2])) = let - val k1 = bounded_card_of_type max default_card asgns T1 - val k2 = bounded_card_of_type max default_card asgns T2 + val k1 = bounded_card_of_type max default_card assigns T1 + val k2 = bounded_card_of_type max default_card assigns T2 in if k1 = max orelse k2 = max then max else Int.min (max, reasonable_power k2 k1) end - | bounded_card_of_type max default_card asgns (Type ("*", [T1, T2])) = + | bounded_card_of_type max default_card assigns (Type ("*", [T1, T2])) = let - val k1 = bounded_card_of_type max default_card asgns T1 - val k2 = bounded_card_of_type max default_card asgns T2 + val k1 = bounded_card_of_type max default_card assigns T1 + val k2 = bounded_card_of_type max default_card assigns T2 in if k1 = max orelse k2 = max then max else Int.min (max, k1 * k2) end - | bounded_card_of_type max default_card asgns T = + | bounded_card_of_type max default_card assigns T = Int.min (max, if default_card = ~1 then - card_of_type asgns T + card_of_type assigns T else - card_of_type asgns T + card_of_type assigns T handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) (* extended_context -> int -> (typ * int) list -> typ -> int *) -fun bounded_precise_card_of_type ext_ctxt max default_card asgns T = +fun bounded_exact_card_of_type ext_ctxt max default_card assigns T = let (* typ list -> typ -> int *) fun aux avoid T = @@ -975,12 +975,13 @@ else Integer.sum constr_cards end) | _ => raise SAME ()) - handle SAME () => AList.lookup (op =) asgns T |> the_default default_card + handle SAME () => + AList.lookup (op =) assigns T |> the_default default_card in Int.min (max, aux [] T) end (* extended_context -> typ -> bool *) fun is_finite_type ext_ctxt = - not_equal 0 o bounded_precise_card_of_type ext_ctxt 1 2 [] + not_equal 0 o bounded_exact_card_of_type ext_ctxt 1 2 [] (* term -> bool *) fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Mon Dec 14 16:48:49 2009 +0100 @@ -238,7 +238,7 @@ [T1, T1 --> T2] ---> T1 --> T2) (* (term * term) list -> term *) fun aux [] = - if maybe_opt andalso not (is_precise_type datatypes T1) then + if maybe_opt andalso not (is_complete_type datatypes T1) then insert_const $ Const (unrep, T1) $ empty_const else empty_const @@ -262,7 +262,7 @@ Const (@{const_name None}, _) => aux' ps | _ => update_const $ aux' ps $ t1 $ t2) fun aux ps = - if not (is_precise_type datatypes T1) then + if not (is_complete_type datatypes T1) then update_const $ aux' ps $ Const (unrep, T1) $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2')) else @@ -601,17 +601,17 @@ Pretty.str oper, Syntax.pretty_term ctxt t2]) end (* dtype_spec -> Pretty.T *) - fun pretty_for_datatype ({typ, card, precise, ...} : dtype_spec) = + fun pretty_for_datatype ({typ, card, complete, ...} : dtype_spec) = Pretty.block (Pretty.breaks [Syntax.pretty_typ ctxt (unbox_type typ), Pretty.str "=", Pretty.enum "," "{" "}" (map (Syntax.pretty_term ctxt o nth_value_of_type typ card) (index_seq 0 card) @ - (if precise then [] else [Pretty.str unrep]))]) + (if complete then [] else [Pretty.str unrep]))]) (* typ -> dtype_spec list *) fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, - precise = false, shallow = false, constrs = []}] + complete = false, concrete = true, shallow = false, constrs = []}] handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] val (codatatypes, datatypes) = datatypes |> filter_out #shallow diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 14 16:48:49 2009 +0100 @@ -466,11 +466,11 @@ PropLogic.SOr (prop_for_exists_eq xs Neg, prop_for_comp (a1, a2, cmp, [])) (* var -> (int -> bool option) -> literal list -> literal list *) -fun literals_from_assignments max_var asgns lits = +fun literals_from_assignments max_var assigns lits = fold (fn x => fn accum => if AList.defined (op =) lits x then accum - else case asgns x of + else case assigns x of SOME b => (x, sign_from_bool b) :: accum | NONE => accum) (max_var downto 1) lits @@ -505,10 +505,13 @@ val prop = PropLogic.all (map prop_for_literal lits @ map prop_for_comp comps @ map prop_for_sign_expr sexps) + (* use the first ML solver (to avoid startup overhead) *) + val solvers = !SatSolver.solvers + |> filter (member (op =) ["dptsat", "dpll"] o fst) in - case SatSolver.invoke_solver "dpll" prop of - SatSolver.SATISFIABLE asgns => - SOME (literals_from_assignments max_var asgns lits + case snd (hd solvers) prop of + SatSolver.SATISFIABLE assigns => + SOME (literals_from_assignments max_var assigns lits |> tap print_solution) | _ => NONE end diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Dec 14 16:48:49 2009 +0100 @@ -708,14 +708,14 @@ (* scope -> bool -> nut -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) fun choose_rep_for_const (scope as {ext_ctxt as {thy, ctxt, ...}, datatypes, - ofs, ...}) all_precise v (vs, table) = + ofs, ...}) all_exact v (vs, table) = let val x as (s, T) = (nickname_of v, type_of v) val R = (if is_abs_fun thy x then rep_for_abs_fun else if is_rep_fun thy x then Func oo best_non_opt_symmetric_reps_for_fun_type - else if all_precise orelse is_skolem_name v + else if all_exact orelse is_skolem_name v orelse member (op =) [@{const_name undefined_fast_The}, @{const_name undefined_fast_Eps}, @{const_name bisim}, @@ -737,8 +737,8 @@ fold (choose_rep_for_free_var scope) vs ([], table) (* scope -> bool -> nut list -> rep NameTable.table -> nut list * rep NameTable.table *) -fun choose_reps_for_consts scope all_precise vs table = - fold (choose_rep_for_const scope all_precise) vs ([], table) +fun choose_reps_for_consts scope all_exact vs table = + fold (choose_rep_for_const scope all_exact) vs ([], table) (* scope -> styp -> int -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) @@ -998,7 +998,7 @@ if is_opt_rep R then triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2) else if opt andalso polar = Pos andalso - not (is_fully_comparable_type datatypes (type_of u1)) then + not (is_concrete_type datatypes (type_of u1)) then Cst (False, T, Formula Pos) else s_op2 Subset T R u1 u2 @@ -1024,7 +1024,7 @@ else opt_opt_case () in if liberal orelse polar = Neg - orelse is_fully_comparable_type datatypes (type_of u1) then + orelse is_concrete_type datatypes (type_of u1) then case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of (true, true) => opt_opt_case () | (true, false) => hybrid_case u1' @@ -1127,7 +1127,7 @@ let val quant_u = s_op2 oper T (Formula polar) u1' u2' in if def orelse (liberal andalso (polar = Pos) = (oper = All)) - orelse is_precise_type datatypes (type_of u1) then + orelse is_complete_type datatypes (type_of u1) then quant_u else let @@ -1170,7 +1170,7 @@ else unopt_R |> opt ? opt_rep ofs T val u = Op2 (oper, T, R, u1', sub u2) in - if is_precise_type datatypes T orelse not opt1 then + if is_complete_type datatypes T orelse not opt1 then u else let diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Mon Dec 14 16:48:49 2009 +0100 @@ -299,7 +299,7 @@ | z => Func z) | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T fun best_set_rep_for_type (scope as {datatypes, ...}) T = - (if is_precise_type datatypes T then best_non_opt_set_rep_for_type + (if is_exact_type datatypes T then best_non_opt_set_rep_for_type else best_opt_set_rep_for_type) scope T fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...}) (Type ("fun", [T1, T2])) = diff -r 9e6326db46b4 -r c4988215a691 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Dec 14 12:31:00 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Mon Dec 14 16:48:49 2009 +0100 @@ -22,7 +22,8 @@ typ: typ, card: int, co: bool, - precise: bool, + complete: bool, + concrete: bool, shallow: bool, constrs: constr_spec list} @@ -35,8 +36,9 @@ val datatype_spec : dtype_spec list -> typ -> dtype_spec option val constr_spec : dtype_spec list -> styp -> constr_spec - val is_precise_type : dtype_spec list -> typ -> bool - val is_fully_comparable_type : dtype_spec list -> typ -> bool + val is_complete_type : dtype_spec list -> typ -> bool + val is_concrete_type : dtype_spec list -> typ -> bool + val is_exact_type : dtype_spec list -> typ -> bool val offset_of_type : int Typtab.table -> typ -> int val spec_of_type : scope -> typ -> int * int val pretties_for_scope : scope -> bool -> Pretty.T list @@ -67,7 +69,8 @@ typ: typ, card: int, co: bool, - precise: bool, + complete: bool, + concrete: bool, shallow: bool, constrs: constr_spec list} @@ -96,17 +99,20 @@ | NONE => constr_spec dtypes x (* dtype_spec list -> typ -> bool *) -fun is_precise_type dtypes (Type ("fun", Ts)) = - forall (is_precise_type dtypes) Ts - | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts - | is_precise_type dtypes T = - not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T)) +fun is_complete_type dtypes (Type ("fun", [T1, T2])) = + is_concrete_type dtypes T1 andalso is_complete_type dtypes T2 + | is_complete_type dtypes (Type ("*", Ts)) = + forall (is_complete_type dtypes) Ts + | is_complete_type dtypes T = + not (is_integer_type T) andalso #complete (the (datatype_spec dtypes T)) handle Option.Option => true -fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) = - is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2 - | is_fully_comparable_type dtypes (Type ("*", Ts)) = - forall (is_fully_comparable_type dtypes) Ts - | is_fully_comparable_type _ _ = true +and is_concrete_type dtypes (Type ("fun", [T1, T2])) = + is_complete_type dtypes T1 andalso is_concrete_type dtypes T2 + | is_concrete_type dtypes (Type ("*", Ts)) = + forall (is_concrete_type dtypes) Ts + | is_concrete_type dtypes T = + #concrete (the (datatype_spec dtypes T)) handle Option.Option => true +fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes (* int Typtab.table -> typ -> int *) fun offset_of_type ofs T = @@ -124,11 +130,11 @@ fun quintuple_for_scope quote ({ext_ctxt as {thy, ctxt, ...}, card_assigns, bisim_depth, datatypes, ...} : scope) = let - val (iter_asgns, card_asgns) = + val (iter_assigns, card_assigns) = card_assigns |> filter_out (curry (op =) @{typ bisim_iterator} o fst) |> List.partition (is_fp_iterator_type o fst) - val (unimportant_card_asgns, important_card_asgns) = - card_asgns |> List.partition ((is_integer_type orf is_datatype thy) o fst) + val (unimportant_card_assigns, important_card_assigns) = + card_assigns |> List.partition ((is_integer_type orf is_datatype thy) o fst) val cards = map (fn (T, k) => quote (string_for_type ctxt T) ^ " = " ^ string_of_int k) @@ -145,13 +151,13 @@ map (fn (T, k) => quote (Syntax.string_of_term ctxt (Const (const_for_iterator_type T))) ^ " = " ^ - string_of_int (k - 1)) iter_asgns + string_of_int (k - 1)) iter_assigns fun bisims () = if bisim_depth < 0 andalso forall (not o #co) datatypes then [] else ["bisim_depth = " ^ string_of_int bisim_depth] in setmp_show_all_types - (fn () => (cards important_card_asgns, cards unimportant_card_asgns, + (fn () => (cards important_card_assigns, cards unimportant_card_assigns, maxes (), iters (), bisims ())) () end @@ -204,52 +210,52 @@ fun project_block (column, block) = map (project_row column) block (* (''a * ''a -> bool) -> (''a option * int list) list -> ''a -> int list *) -fun lookup_ints_assign eq asgns key = - case triple_lookup eq asgns key of +fun lookup_ints_assign eq assigns key = + case triple_lookup eq assigns key of SOME ks => ks | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "") (* theory -> (typ option * int list) list -> typ -> int list *) -fun lookup_type_ints_assign thy asgns T = - map (curry Int.max 1) (lookup_ints_assign (type_match thy) asgns T) +fun lookup_type_ints_assign thy assigns T = + map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T) handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], []) (* theory -> (styp option * int list) list -> styp -> int list *) -fun lookup_const_ints_assign thy asgns x = - lookup_ints_assign (const_match thy) asgns x +fun lookup_const_ints_assign thy assigns x = + lookup_ints_assign (const_match thy) assigns x handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => raise TERM ("Nitpick_Scope.lookup_const_ints_assign", [Const x]) (* theory -> (styp option * int list) list -> styp -> row option *) -fun row_for_constr thy maxes_asgns constr = - SOME (Max constr, lookup_const_ints_assign thy maxes_asgns constr) +fun row_for_constr thy maxes_assigns constr = + SOME (Max constr, lookup_const_ints_assign thy maxes_assigns constr) handle TERM ("lookup_const_ints_assign", _) => NONE (* extended_context -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list -> typ -> block *) -fun block_for_type (ext_ctxt as {thy, ...}) cards_asgns maxes_asgns iters_asgns - bisim_depths T = +fun block_for_type (ext_ctxt as {thy, ...}) cards_assigns maxes_assigns + iters_assigns bisim_depths T = if T = @{typ bisim_iterator} then [(Card T, map (fn k => Int.max (0, k) + 1) bisim_depths)] else if is_fp_iterator_type T then [(Card T, map (fn k => Int.max (0, k) + 1) - (lookup_const_ints_assign thy iters_asgns + (lookup_const_ints_assign thy iters_assigns (const_for_iterator_type T)))] else - (Card T, lookup_type_ints_assign thy cards_asgns T) :: + (Card T, lookup_type_ints_assign thy cards_assigns T) :: (case datatype_constrs ext_ctxt T of [_] => [] - | constrs => map_filter (row_for_constr thy maxes_asgns) constrs) + | constrs => map_filter (row_for_constr thy maxes_assigns) constrs) (* extended_context -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list -> typ list -> typ list -> block list *) -fun blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns bisim_depths - mono_Ts nonmono_Ts = +fun blocks_for_types ext_ctxt cards_assigns maxes_assigns iters_assigns + bisim_depths mono_Ts nonmono_Ts = let (* typ -> block *) - val block_for = block_for_type ext_ctxt cards_asgns maxes_asgns iters_asgns - bisim_depths + val block_for = block_for_type ext_ctxt cards_assigns maxes_assigns + iters_assigns bisim_depths val mono_block = maps block_for mono_Ts val nonmono_blocks = map block_for nonmono_Ts in mono_block :: nonmono_blocks end @@ -290,117 +296,121 @@ type scope_desc = (typ * int) list * (styp * int) list (* extended_context -> scope_desc -> typ * int -> bool *) -fun is_surely_inconsistent_card_assign ext_ctxt (card_asgns, max_asgns) (T, k) = +fun is_surely_inconsistent_card_assign ext_ctxt (card_assigns, max_assigns) + (T, k) = case datatype_constrs ext_ctxt T of [] => false | xs => let - val precise_cards = + val exact_cards = map (Integer.prod - o map (bounded_precise_card_of_type ext_ctxt k 0 card_asgns) + o map (bounded_exact_card_of_type ext_ctxt k 0 card_assigns) o binder_types o snd) xs - val maxes = map (constr_max max_asgns) xs + val maxes = map (constr_max max_assigns) xs (* int -> int -> int *) fun effective_max 0 ~1 = k | effective_max 0 max = max | effective_max card ~1 = card | effective_max card max = Int.min (card, max) - val max = map2 effective_max precise_cards maxes |> Integer.sum + val max = map2 effective_max exact_cards maxes |> Integer.sum (* unit -> int *) fun doms_card () = - xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_asgns) + xs |> map (Integer.prod o map (bounded_card_of_type k ~1 card_assigns) o binder_types o snd) |> Integer.sum in max < k - orelse (forall (not_equal 0) precise_cards andalso doms_card () < k) + orelse (forall (not_equal 0) exact_cards andalso doms_card () < k) end handle TYPE ("Nitpick_HOL.card_of_type", _, _) => false (* extended_context -> scope_desc -> bool *) fun is_surely_inconsistent_scope_description ext_ctxt - (desc as (card_asgns, _)) = - exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_asgns + (desc as (card_assigns, _)) = + exists (is_surely_inconsistent_card_assign ext_ctxt desc) card_assigns (* extended_context -> scope_desc -> (typ * int) list option *) -fun repair_card_assigns ext_ctxt (card_asgns, max_asgns) = +fun repair_card_assigns ext_ctxt (card_assigns, max_assigns) = let (* (typ * int) list -> (typ * int) list -> (typ * int) list option *) fun aux seen [] = SOME seen | aux seen ((T, 0) :: _) = NONE - | aux seen ((T, k) :: asgns) = + | aux seen ((T, k) :: assigns) = (if is_surely_inconsistent_scope_description ext_ctxt - ((T, k) :: seen, max_asgns) then + ((T, k) :: seen, max_assigns) then raise SAME () else - case aux ((T, k) :: seen) asgns of - SOME asgns => SOME asgns + case aux ((T, k) :: seen) assigns of + SOME assigns => SOME assigns | NONE => raise SAME ()) - handle SAME () => aux seen ((T, k - 1) :: asgns) - in aux [] (rev card_asgns) end + handle SAME () => aux seen ((T, k - 1) :: assigns) + in aux [] (rev card_assigns) end (* theory -> (typ * int) list -> typ * int -> typ * int *) -fun repair_iterator_assign thy asgns (T as Type (s, Ts), k) = +fun repair_iterator_assign thy assigns (T as Type (s, Ts), k) = (T, if T = @{typ bisim_iterator} then - let val co_cards = map snd (filter (is_codatatype thy o fst) asgns) in - Int.min (k, Integer.sum co_cards) - end + let + val co_cards = map snd (filter (is_codatatype thy o fst) assigns) + in Int.min (k, Integer.sum co_cards) end else if is_fp_iterator_type T then case Ts of [] => 1 - | _ => bounded_card_of_type k ~1 asgns (foldr1 HOLogic.mk_prodT Ts) + | _ => bounded_card_of_type k ~1 assigns (foldr1 HOLogic.mk_prodT Ts) else k) - | repair_iterator_assign _ _ asgn = asgn + | repair_iterator_assign _ _ assign = assign (* row -> scope_desc -> scope_desc *) -fun add_row_to_scope_descriptor (kind, ks) (card_asgns, max_asgns) = +fun add_row_to_scope_descriptor (kind, ks) (card_assigns, max_assigns) = case kind of - Card T => ((T, the_single ks) :: card_asgns, max_asgns) - | Max x => (card_asgns, (x, the_single ks) :: max_asgns) + Card T => ((T, the_single ks) :: card_assigns, max_assigns) + | Max x => (card_assigns, (x, the_single ks) :: max_assigns) (* block -> scope_desc *) fun scope_descriptor_from_block block = fold_rev add_row_to_scope_descriptor block ([], []) (* extended_context -> block list -> int list -> scope_desc option *) fun scope_descriptor_from_combination (ext_ctxt as {thy, ...}) blocks columns = let - val (card_asgns, max_asgns) = + val (card_assigns, max_assigns) = maps project_block (columns ~~ blocks) |> scope_descriptor_from_block - val card_asgns = repair_card_assigns ext_ctxt (card_asgns, max_asgns) |> the + val card_assigns = repair_card_assigns ext_ctxt (card_assigns, max_assigns) + |> the in - SOME (map (repair_iterator_assign thy card_asgns) card_asgns, max_asgns) + SOME (map (repair_iterator_assign thy card_assigns) card_assigns, + max_assigns) end handle Option.Option => NONE (* theory -> (typ * int) list -> dtype_spec list -> int Typtab.table *) -fun offset_table_for_card_assigns thy asgns dtypes = +fun offset_table_for_card_assigns thy assigns dtypes = let (* int -> (int * int) list -> (typ * int) list -> int Typtab.table -> int Typtab.table *) fun aux next _ [] = Typtab.update_new (dummyT, next) - | aux next reusable ((T, k) :: asgns) = + | aux next reusable ((T, k) :: assigns) = if k = 1 orelse is_integer_type T then - aux next reusable asgns + aux next reusable assigns else if length (these (Option.map #constrs (datatype_spec dtypes T))) > 1 then - Typtab.update_new (T, next) #> aux (next + k) reusable asgns + Typtab.update_new (T, next) #> aux (next + k) reusable assigns else case AList.lookup (op =) reusable k of - SOME j0 => Typtab.update_new (T, j0) #> aux next reusable asgns + SOME j0 => Typtab.update_new (T, j0) #> aux next reusable assigns | NONE => Typtab.update_new (T, next) - #> aux (next + k) ((k, next) :: reusable) asgns - in aux 0 [] asgns Typtab.empty end + #> aux (next + k) ((k, next) :: reusable) assigns + in aux 0 [] assigns Typtab.empty end (* int -> (typ * int) list -> typ -> int *) -fun domain_card max card_asgns = - Integer.prod o map (bounded_card_of_type max max card_asgns) o binder_types +fun domain_card max card_assigns = + Integer.prod o map (bounded_card_of_type max max card_assigns) o binder_types (* scope_desc -> bool -> int -> (int -> int) -> int -> int -> bool * styp -> constr_spec list -> constr_spec list *) -fun add_constr_spec (card_asgns, max_asgns) co card sum_dom_cards num_self_recs - num_non_self_recs (self_rec, x as (s, T)) constrs = +fun add_constr_spec (card_assigns, max_assigns) co card sum_dom_cards + num_self_recs num_non_self_recs (self_rec, x as (s, T)) + constrs = let - val max = constr_max max_asgns x + val max = constr_max max_assigns x (* int -> int *) fun bound k = Int.min (card, (max >= 0 ? curry Int.min max) k) (* unit -> int *) @@ -412,7 +422,7 @@ end else if not co andalso num_self_recs > 0 then if not self_rec andalso num_non_self_recs = 1 - andalso domain_card 2 card_asgns T = 1 then + andalso domain_card 2 card_assigns T = 1 then {delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}), total = true} else if s = @{const_name Cons} then @@ -421,7 +431,7 @@ {delta = 0, epsilon = card, exclusive = false, total = false} else if card = sum_dom_cards (card + 1) then let val delta = next_delta () in - {delta = delta, epsilon = delta + domain_card card card_asgns T, + {delta = delta, epsilon = delta + domain_card card card_assigns T, exclusive = true, total = true} end else @@ -432,55 +442,62 @@ explicit_max = max, total = total} :: constrs end +(* extended_context -> (typ * int) list -> typ -> bool *) +fun has_exact_card ext_ctxt card_assigns T = + let val card = card_of_type card_assigns T in + card = bounded_exact_card_of_type ext_ctxt (card + 1) 0 card_assigns T + end + (* extended_context -> typ list -> scope_desc -> typ * int -> dtype_spec *) fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) shallow_dataTs - (desc as (card_asgns, _)) (T, card) = + (desc as (card_assigns, _)) (T, card) = let val shallow = member (op =) shallow_dataTs T val co = is_codatatype thy T val xs = boxed_datatype_constrs ext_ctxt T val self_recs = map (is_self_recursive_constr_type o snd) xs val (num_self_recs, num_non_self_recs) = - List.partition (curry (op =) true) self_recs |> pairself length - val precise = (card = bounded_precise_card_of_type ext_ctxt (card + 1) 0 - card_asgns T) + List.partition I self_recs |> pairself length + val complete = has_exact_card ext_ctxt card_assigns T + val concrete = xs |> maps (binder_types o snd) |> maps binder_types + |> forall (has_exact_card ext_ctxt card_assigns) (* int -> int *) fun sum_dom_cards max = - map (domain_card max card_asgns o snd) xs |> Integer.sum + map (domain_card max card_assigns o snd) xs |> Integer.sum val constrs = fold_rev (add_constr_spec desc co card sum_dom_cards num_self_recs num_non_self_recs) (self_recs ~~ xs) [] in - {typ = T, card = card, co = co, precise = precise, shallow = shallow, - constrs = constrs} + {typ = T, card = card, co = co, complete = complete, concrete = concrete, + shallow = shallow, constrs = constrs} end (* extended_context -> int -> typ list -> scope_desc -> scope *) fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs - (desc as (card_asgns, _)) = + (desc as (card_assigns, _)) = let val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt shallow_dataTs desc) - (filter (is_datatype thy o fst) card_asgns) - val bisim_depth = card_of_type card_asgns @{typ bisim_iterator} - 1 + (filter (is_datatype thy o fst) card_assigns) + val bisim_depth = card_of_type card_assigns @{typ bisim_iterator} - 1 in - {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes, + {ext_ctxt = ext_ctxt, card_assigns = card_assigns, datatypes = datatypes, bisim_depth = bisim_depth, ofs = if sym_break <= 0 then Typtab.empty - else offset_table_for_card_assigns thy card_asgns datatypes} + else offset_table_for_card_assigns thy card_assigns datatypes} end (* theory -> typ list -> (typ option * int list) list -> (typ option * int list) list *) fun fix_cards_assigns_wrt_boxing _ _ [] = [] - | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_asgns) = + | fix_cards_assigns_wrt_boxing thy Ts ((SOME T, ks) :: cards_assigns) = (if is_fun_type T orelse is_pair_type T then Ts |> filter (curry (type_match thy o swap) T o unbox_type) |> map (rpair ks o SOME) else - [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_asgns - | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_asgns) = - (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_asgns + [(SOME T, ks)]) @ fix_cards_assigns_wrt_boxing thy Ts cards_assigns + | fix_cards_assigns_wrt_boxing thy Ts ((NONE, ks) :: cards_assigns) = + (NONE, ks) :: fix_cards_assigns_wrt_boxing thy Ts cards_assigns val max_scopes = 4096 val distinct_threshold = 512 @@ -488,12 +505,12 @@ (* extended_context -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list -> typ list -> typ list -> typ list -> int * scope list *) -fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_asgns maxes_asgns - iters_asgns bisim_depths mono_Ts nonmono_Ts shallow_dataTs = +fun all_scopes (ext_ctxt as {thy, ...}) sym_break cards_assigns maxes_assigns + iters_assigns bisim_depths mono_Ts nonmono_Ts shallow_dataTs = let - val cards_asgns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_asgns - val blocks = blocks_for_types ext_ctxt cards_asgns maxes_asgns iters_asgns - bisim_depths mono_Ts nonmono_Ts + val cards_assigns = fix_cards_assigns_wrt_boxing thy mono_Ts cards_assigns + val blocks = blocks_for_types ext_ctxt cards_assigns maxes_assigns + iters_assigns bisim_depths mono_Ts nonmono_Ts val ranks = map rank_of_block blocks val all = all_combinations_ordered_smartly (map (rpair 0) ranks) val head = take max_scopes all