# HG changeset patch # User blanchet # Date 1300465648 -3600 # Node ID c2e1503fad8f891d4e397aa9c6f2aeb85bc53105 # Parent 33b7d118e9dcf1f1e06f53ff0538ecfe7929ddc3 optimize Kodkod axioms further w.r.t. "need" option diff -r 33b7d118e9dc -r c2e1503fad8f src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 12:20:32 2011 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 17:27:28 2011 +0100 @@ -305,6 +305,16 @@ ([Type (_, Ts1)], [T2]) => forall (curry (op =) typ) (T2 :: Ts1) | _ => false +fun needed_values need_vals T = + AList.lookup (op =) need_vals T |> the_default NONE |> these + +fun all_values_are_needed need_vals ({typ, card, ...} : datatype_spec) = + length (needed_values need_vals typ) = card + +fun is_sel_of_constr x (Construct (sel_us, _, _, _), _) = + exists (fn FreeRel (x', _, _, _) => x = x' | _ => false) sel_us + | is_sel_of_constr _ _ = false + 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)) = @@ -313,19 +323,13 @@ val {delta, epsilon, exclusive, explicit_max, ...} = 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 + val T1_need_vals = needed_values need_vals T1 in ([(x, bound_comment ctxt debug nick T R)], let - val complete_need_vals = (length need_vals = card) + val complete_need_vals = (length T1_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) + T1_need_vals |> List.partition (is_sel_of_constr x) fun upper_bound_ts () = if complete_need_vals then my_need_vals |> map (KK.Tuple o single o snd) |> KK.TupleSet @@ -337,11 +341,13 @@ KK.TupleAtomSeq (epsilon - delta, delta + j0) in if explicit_max = 0 orelse - (complete_need_vals andalso null my_need_vals) (* ### needed? *) then + (complete_need_vals andalso null my_need_vals) then [KK.TupleSet []] else if R2 = Formula Neut then - [upper_bound_ts ()] |> not exclusive ? cons (KK.TupleSet []) + [upper_bound_ts ()] + |> not (exclusive orelse all_values_are_needed need_vals dtype) + ? cons (KK.TupleSet []) else [KK.TupleSet [], if T1 = T2 andalso epsilon > delta andalso @@ -1715,27 +1721,35 @@ |> 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) - n = +fun sel_axioms_for_sel hol_ctxt binarize j0 + (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, kk_union, + ...}) need_vals rel_table dom_r (dtype as {typ, ...}) + ({const, delta, epsilon, exclusive, ...} : constr_spec) n = let val x = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize const n val (r, R, _) = const_triple rel_table x + val rel_x = + case r of + KK.Rel x => x + | _ => raise BAD ("Nitpick_Kodkod.sel_axioms_for_sel", "non-Rel") val R2 = dest_Func R |> snd val z = (epsilon - delta, delta + j0) in if exclusive then - kk_n_ary_function kk (Func (Atom z, R2)) r + [kk_n_ary_function kk (Func (Atom z, R2)) r] + else if all_values_are_needed need_vals dtype then + typ |> needed_values need_vals + |> filter (is_sel_of_constr rel_x) + |> map (fn (_, j) => kk_n_ary_function kk R2 (kk_join (KK.Atom j) r)) else let val r' = kk_join (KK.Var (1, 0)) r in - kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] - (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) - (kk_n_ary_function kk R2 r') (kk_no r')) + [kk_all [KK.DeclOne ((1, 0), KK.AtomSeq z)] + (kk_formula_if (kk_subset (KK.Var (1, 0)) dom_r) + (kk_n_ary_function kk R2 r') (kk_no r'))] end end -fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table - (constr as {const, delta, epsilon, explicit_max, ...}) = +fun sel_axioms_for_constr hol_ctxt binarize bits j0 kk need_vals rel_table + dtype (constr as {const, delta, epsilon, explicit_max, ...}) = let val honors_explicit_max = explicit_max < 0 orelse epsilon - delta <= explicit_max @@ -1757,17 +1771,20 @@ " too small for \"max\"") in max_axiom :: - map (sel_axiom_for_sel hol_ctxt binarize j0 kk rel_table dom_r constr) - (index_seq 0 (num_sels_for_constr_type (snd const))) + maps (sel_axioms_for_sel hol_ctxt binarize j0 kk need_vals rel_table + dom_r dtype constr) + (index_seq 0 (num_sels_for_constr_type (snd const))) end end -fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table - ({constrs, ...} : datatype_spec) = - maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table) constrs +fun sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table need_vals + (dtype as {constrs, ...}) = + maps (sel_axioms_for_constr hol_ctxt binarize bits j0 kk rel_table need_vals + dtype) constrs -fun uniqueness_axiom_for_constr hol_ctxt binarize +fun uniqueness_axioms_for_constr hol_ctxt binarize ({kk_all, kk_implies, kk_and, kk_rel_eq, kk_lone, kk_join, ...} - : kodkod_constrs) rel_table ({const, ...} : constr_spec) = + : kodkod_constrs) need_vals rel_table dtype + ({const, ...} : constr_spec) = let fun conjunct_for_sel r = kk_rel_eq (kk_join (KK.Var (1, 0)) r) (kk_join (KK.Var (1, 1)) r) @@ -1779,36 +1796,42 @@ val set_r = triples |> hd |> #1 in if num_sels = 0 then - kk_lone set_r + [kk_lone set_r] + else if all_values_are_needed need_vals dtype then + [] else - kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) - (kk_implies - (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) - (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1)))) + [kk_all (map (KK.DeclOne o rpair set_r o pair 1) [0, 1]) + (kk_implies + (fold1 kk_and (map (conjunct_for_sel o #1) (tl triples))) + (kk_rel_eq (KK.Var (1, 0)) (KK.Var (1, 1))))] end -fun uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table - ({constrs, ...} : datatype_spec) = - map (uniqueness_axiom_for_constr hol_ctxt binarize kk rel_table) constrs +fun uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table + (dtype as {constrs, ...}) = + maps (uniqueness_axioms_for_constr hol_ctxt binarize kk need_vals rel_table + dtype) constrs fun effective_constr_max ({delta, epsilon, ...} : constr_spec) = epsilon - delta fun partition_axioms_for_datatype j0 (kk as {kk_rel_eq, kk_union, ...}) - rel_table - ({card, constrs, ...} : datatype_spec) = + need_vals rel_table (dtype as {card, constrs, ...}) = if forall #exclusive constrs then [Integer.sum (map effective_constr_max constrs) = card |> formula_for_bool] + else if all_values_are_needed need_vals dtype then + [] else let val rs = map (discr_rel_expr rel_table o #const) constrs in [kk_rel_eq (fold1 kk_union rs) (KK.AtomSeq (card, j0)), kk_disjoint_sets kk rs] end -fun other_axioms_for_datatype _ _ _ _ _ _ {deep = false, ...} = [] - | other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table +fun other_axioms_for_datatype _ _ _ _ _ _ _ {deep = false, ...} = [] + | other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk rel_table (dtype as {typ, ...}) = let val j0 = offset_of_type ofs typ in - sel_axioms_for_datatype hol_ctxt binarize bits j0 kk rel_table dtype @ - uniqueness_axioms_for_datatype hol_ctxt binarize kk rel_table dtype @ - partition_axioms_for_datatype j0 kk rel_table dtype + sel_axioms_for_datatype hol_ctxt binarize bits j0 kk need_vals rel_table + dtype @ + uniqueness_axioms_for_datatype hol_ctxt binarize kk need_vals rel_table + dtype @ + partition_axioms_for_datatype j0 kk need_vals rel_table dtype end fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals @@ -1823,8 +1846,8 @@ 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) - dtypes + maps (other_axioms_for_datatype hol_ctxt binarize need_vals bits ofs kk + rel_table) dtypes end end;