# HG changeset patch # User blanchet # Date 1256666417 -3600 # Node ID a2db56854b8304e28ecf7c7a6cd652c474c6893d # Parent 107f3df799f698580a444826b065667ed79b260e optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem diff -r 107f3df799f6 -r a2db56854b83 src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Tue Oct 27 17:53:19 2009 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Tue Oct 27 19:00:17 2009 +0100 @@ -7,6 +7,8 @@ * Replaced "special_depth" and "skolemize_depth" options by "specialize" and "skolemize" * Renamed "coalesce_type_vars" to "merge_type_vars" + * Optimized Kodkod encoding of datatypes whose constructors don't appear in + the formula to falsify * Fixed monotonicity check Version 1.2.2 (16 Oct 2009) diff -r 107f3df799f6 -r a2db56854b83 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 17:53:19 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Oct 27 19:00:17 2009 +0100 @@ -283,6 +283,21 @@ handle TYPE (_, Ts, ts) => raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts) + val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t + val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq) + def_ts + val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq) + nondef_ts + val (free_names, const_names) = + fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], []) + val (sel_names, nonsel_names) = + List.partition (is_sel o nickname_of) const_names + val would_be_genuine = got_all_user_axioms andalso none_true wfs +(* + val _ = List.app (priority o string_for_nut ctxt) + (core_u :: def_us @ nondef_us) +*) + val unique_scope = forall (equal 1 o length o snd) cards_assigns (* typ -> bool *) fun is_free_type_monotonic T = @@ -298,6 +313,8 @@ not (is_pure_typedef thy T) orelse is_univ_typedef thy T orelse is_number_type thy T orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t + fun is_datatype_shallow T = + not (exists (equal T o domain_type o type_of) sel_names) val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts) |> sort TermOrd.typ_ord val (all_dataTs, all_free_Ts) = @@ -326,7 +343,7 @@ () val mono_Ts = mono_dataTs @ mono_free_Ts val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts - + val shallow_dataTs = filter is_datatype_shallow mono_dataTs (* val _ = priority "Monotonic datatypes:" val _ = List.app (priority o string_for_type ctxt) mono_dataTs @@ -338,19 +355,6 @@ val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts *) - val core_u = nut_from_term thy fast_descrs (!special_funs) Eq core_t - val def_us = map (nut_from_term thy fast_descrs (!special_funs) DefEq) - def_ts - val nondef_us = map (nut_from_term thy fast_descrs (!special_funs) Eq) - nondef_ts - val (free_names, const_names) = - fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], []) - val nonsel_names = filter_out (is_sel o nickname_of) const_names - val would_be_genuine = got_all_user_axioms andalso none_true wfs -(* - val _ = List.app (priority o string_for_nut ctxt) - (core_u :: def_us @ nondef_us) -*) val need_incremental = Int.max (max_potential, max_genuine) >= 2 val effective_sat_solver = if sat_solver <> "smart" then @@ -812,6 +816,7 @@ val _ = scopes := all_scopes ext_ctxt sym_break cards_assigns maxes_assigns iters_assigns bisim_depths mono_Ts nonmono_Ts + shallow_dataTs val batches = batch_list batch_size (!scopes) val outcome_code = (run_batches 0 (length batches) batches (max_potential, max_genuine, 0) diff -r 107f3df799f6 -r a2db56854b83 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 17:53:19 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Oct 27 19:00:17 2009 +0100 @@ -716,8 +716,8 @@ (* extended_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> dtype_spec -> nfa_entry option *) fun nfa_entry_for_datatype _ _ _ _ ({co = true, ...} : dtype_spec) = NONE - | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes - ({typ, constrs, ...} : dtype_spec) = + | nfa_entry_for_datatype _ _ _ _ {shallow = true, ...} = NONE + | nfa_entry_for_datatype ext_ctxt kk rel_table dtypes {typ, constrs, ...} = SOME (typ, maps (nfa_transitions_for_constr ext_ctxt kk rel_table dtypes o #const) constrs) @@ -884,12 +884,13 @@ (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec -> Kodkod.formula list *) -fun other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) = - let val j0 = offset_of_type ofs typ in - sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @ - uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @ - partition_axioms_for_datatype j0 kk rel_table dtype - end +fun other_axioms_for_datatype _ _ _ _ {shallow = true, ...} = [] + | other_axioms_for_datatype ext_ctxt ofs kk rel_table (dtype as {typ, ...}) = + let val j0 = offset_of_type ofs typ in + sel_axioms_for_datatype ext_ctxt j0 kk rel_table dtype @ + uniqueness_axioms_for_datatype ext_ctxt kk rel_table dtype @ + partition_axioms_for_datatype j0 kk rel_table dtype + end (* extended_context -> int Typtab.table -> kodkod_constrs -> nut NameTable.table -> dtype_spec list -> Kodkod.formula list *) diff -r 107f3df799f6 -r a2db56854b83 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 27 17:53:19 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Oct 27 19:00:17 2009 +0100 @@ -329,7 +329,8 @@ HOLogic.mk_number nat_T j else case datatype_spec datatypes T of NONE => atom for_auto T j - | SOME {constrs, co, ...} => + | SOME {shallow = true, ...} => atom for_auto T j + | SOME {co, constrs, ...} => let (* styp -> int list *) fun tuples_for_const (s, T) = @@ -600,11 +601,12 @@ (* typ -> dtype_spec list *) fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, - precise = false, constrs = []}] + precise = false, shallow = false, constrs = []}] handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] val (codatatypes, datatypes) = - List.partition #co datatypes - ||> append (integer_datatype nat_T @ integer_datatype int_T) + datatypes |> filter_out #shallow + |> List.partition #co + ||> append (integer_datatype nat_T @ integer_datatype int_T) val block_of_datatypes = if show_datatypes andalso not (null datatypes) then [Pretty.big_list ("Datatype" ^ plural_s_for_list datatypes ^ ":") diff -r 107f3df799f6 -r a2db56854b83 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Oct 27 17:53:19 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Oct 27 19:00:17 2009 +0100 @@ -749,8 +749,9 @@ (~1 upto num_sels_for_constr_type T - 1) (* scope -> dtype_spec -> nut list * rep NameTable.table -> nut list * rep NameTable.table *) -fun choose_rep_for_sels_of_datatype scope ({constrs, ...} : dtype_spec) = - fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs +fun choose_rep_for_sels_of_datatype _ ({shallow = true, ...} : dtype_spec) = I + | choose_rep_for_sels_of_datatype scope {constrs, ...} = + fold_rev (choose_rep_for_sels_for_constr scope o #const) constrs (* scope -> rep NameTable.table -> nut list * rep NameTable.table *) fun choose_reps_for_all_sels (scope as {datatypes, ...}) = fold (choose_rep_for_sels_of_datatype scope) datatypes o pair [] diff -r 107f3df799f6 -r a2db56854b83 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Oct 27 17:53:19 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Oct 27 19:00:17 2009 +0100 @@ -22,6 +22,7 @@ card: int, co: bool, precise: bool, + shallow: bool, constrs: constr_spec list} type scope = { @@ -44,7 +45,7 @@ val all_scopes : extended_context -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list - -> int list -> typ list -> typ list -> scope list + -> int list -> typ list -> typ list -> typ list -> scope list end; structure Nitpick_Scope : NITPICK_SCOPE = @@ -66,6 +67,7 @@ card: int, co: bool, precise: bool, + shallow: bool, constrs: constr_spec list} type scope = { @@ -126,7 +128,7 @@ card_assigns |> filter_out (equal @{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_datatype thy orf is_integer_type) o fst) + card_asgns |> 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) @@ -431,10 +433,11 @@ explicit_max = max, total = total} :: constrs end -(* extended_context -> scope_desc -> typ * int -> dtype_spec *) -fun datatype_spec_from_scope_descriptor (ext_ctxt as {thy, ...}) +(* 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) = let + val shallow = T mem shallow_dataTs 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 @@ -448,14 +451,18 @@ 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, constrs = constrs} end + in + {typ = T, card = card, co = co, precise = precise, shallow = shallow, + constrs = constrs} + end -(* extended_context -> int -> scope_desc -> scope *) -fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break +(* extended_context -> int -> typ list -> scope_desc -> scope *) +fun scope_from_descriptor (ext_ctxt as {thy, ...}) sym_break shallow_dataTs (desc as (card_asgns, _)) = let - val datatypes = map (datatype_spec_from_scope_descriptor ext_ctxt desc) - (filter (is_datatype thy o fst) card_asgns) + 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 in {ext_ctxt = ext_ctxt, card_assigns = card_asgns, datatypes = datatypes, @@ -480,9 +487,9 @@ (* extended_context -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list - -> typ list -> typ list -> scope list *) + -> typ list -> typ list -> typ list -> scope list *) fun all_scopes (ext_ctxt as {thy, ctxt, ...}) sym_break cards_asgns maxes_asgns - iters_asgns bisim_depths mono_Ts nonmono_Ts = + iters_asgns 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 ctxt cards_asgns maxes_asgns iters_asgns @@ -492,7 +499,7 @@ |> map_filter (scope_descriptor_from_combination thy blocks) in descs |> length descs <= distinct_threshold ? distinct (op =) - |> map (scope_from_descriptor ext_ctxt sym_break) + |> map (scope_from_descriptor ext_ctxt sym_break shallow_dataTs) end end;