# HG changeset patch # User blanchet # Date 1300445008 -3600 # Node ID 03c2d29ec790fdac5694a0279715023013c8955f # Parent c567c860caf67803765d5569eddabbffaa3e4db3 optimize Kodkod bounds when "need" is specified diff -r c567c860caf6 -r 03c2d29ec790 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 18 10:17:37 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Mar 18 11:43:28 2011 +0100 @@ -564,9 +564,13 @@ val plain_rels = free_rels @ other_rels val plain_bounds = map (bound_for_plain_rel ctxt debug) plain_rels val plain_axioms = map (declarative_axiom_for_plain_rel kk) plain_rels - val sel_bounds = map (bound_for_sel_rel ctxt debug datatypes) sel_rels + val need_vals = + map (fn dtype as {typ, ...} => + (typ, needed_values_for_datatype need_us ofs dtype)) datatypes + val sel_bounds = + map (bound_for_sel_rel ctxt debug need_vals datatypes) sel_rels val dtype_axioms = - declarative_axioms_for_datatypes hol_ctxt binarize need_us + declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals datatype_sym_break bits ofs kk rel_table datatypes val declarative_axioms = plain_axioms @ dtype_axioms val univ_card = Int.max (univ_card nat_card int_card main_j0 diff -r c567c860caf6 -r 03c2d29ec790 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 10:17:37 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 11:43:28 2011 +0100 @@ -27,15 +27,18 @@ -> Kodkod.bound list * Kodkod.formula list val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound val bound_for_sel_rel : - Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound + Proof.context -> bool -> (typ * (nut * int) list option) list + -> datatype_spec list -> nut -> Kodkod.bound val merge_bounds : Kodkod.bound list -> Kodkod.bound list val kodkod_formula_from_nut : int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula + val needed_values_for_datatype : + nut list -> int Typtab.table -> datatype_spec -> (nut * int) list option val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula val declarative_axioms_for_datatypes : - hol_context -> bool -> nut list -> int -> int -> int Typtab.table - -> kodkod_constrs -> nut NameTable.table -> datatype_spec list - -> Kodkod.formula list + hol_context -> bool -> nut list -> (typ * (nut * int) list option) list + -> int -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table + -> datatype_spec list -> Kodkod.formula list end; structure Nitpick_Kodkod : NITPICK_KODKOD = @@ -297,24 +300,39 @@ | bound_for_plain_rel _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u]) -fun bound_for_sel_rel ctxt debug dtypes +fun bound_for_sel_rel ctxt debug need_vals dtypes (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]), R as Func (Atom (_, j0), R2), nick)) = let + val constr_s = original_name nick val {delta, epsilon, exclusive, explicit_max, ...} = - constr_spec dtypes (original_name nick, T1) + constr_spec dtypes (constr_s, T1) + val dtype as {card, ...} = datatype_spec dtypes T1 |> the + val need_vals = + AList.lookup (op =) need_vals T1 |> the_default NONE |> these in ([(x, bound_comment ctxt debug nick T R)], - if explicit_max = 0 then - [KK.TupleSet []] - else - let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in + let + val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) + val complete_need_vals = (length need_vals = card) + val (my_need_vals, other_need_vals) = + need_vals + |> List.partition + (fn (Construct (sel_us, _, _, _), _) => + exists (fn FreeRel (x', _, _, _) => x = x' + | _ => false) sel_us + | _ => false) + in + if explicit_max = 0 orelse + (complete_need_vals andalso null my_need_vals) then + [KK.TupleSet []] + else if R2 = Formula Neut then [ts] |> not exclusive ? cons (KK.TupleSet []) else [KK.TupleSet [], if T1 = T2 andalso epsilon > delta andalso - is_datatype_acyclic (the (datatype_spec dtypes T1)) then + is_datatype_acyclic dtype then index_seq delta (epsilon - delta) |> map (fn j => KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]], @@ -324,7 +342,7 @@ KK.TupleProduct (ts, upper_bound_for_rep R2)] end) end - | bound_for_sel_rel _ _ _ u = + | bound_for_sel_rel _ _ _ _ u = raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u]) fun merge_bounds bs = @@ -1478,8 +1496,8 @@ "malformed Kodkod formula") end -fun needed_value_axioms_for_datatype [] _ _ _ = [] - | needed_value_axioms_for_datatype need_us ofs kk +fun needed_values_for_datatype [] _ _ = SOME [] + | needed_values_for_datatype need_us ofs ({typ, card, constrs, ...} : datatype_spec) = let fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) = @@ -1507,11 +1525,11 @@ else accum) | aux _ = I - in - case SOME (index_seq 0 card, []) |> fold aux need_us of - SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk) - | NONE => [KK.False] - end + in SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map snd end + +fun needed_value_axioms_for_datatype _ _ NONE = [KK.False] + | needed_value_axioms_for_datatype ofs kk (SOME fixed) = + fixed |> map (atom_equation_for_nut ofs kk) fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r = kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z))) @@ -1679,7 +1697,6 @@ |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table nfas dtypes) - fun sel_axiom_for_sel hol_ctxt binarize j0 (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...}) rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec) @@ -1776,7 +1793,7 @@ partition_axioms_for_datatype j0 kk rel_table dtype end -fun declarative_axioms_for_datatypes hol_ctxt binarize need_us +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals datatype_sym_break bits ofs kk rel_table dtypes = let val nfas = @@ -1785,7 +1802,7 @@ |> strongly_connected_sub_nfas in acyclicity_axioms_for_datatypes kk nfas @ - maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @ + maps (needed_value_axioms_for_datatype ofs kk o snd) need_vals @ sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break kk rel_table nfas dtypes @ maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)