1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 10:17:37 2011 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Mar 18 11:43:28 2011 +0100
1.3 @@ -27,15 +27,18 @@
1.4 -> Kodkod.bound list * Kodkod.formula list
1.5 val bound_for_plain_rel : Proof.context -> bool -> nut -> Kodkod.bound
1.6 val bound_for_sel_rel :
1.7 - Proof.context -> bool -> datatype_spec list -> nut -> Kodkod.bound
1.8 + Proof.context -> bool -> (typ * (nut * int) list option) list
1.9 + -> datatype_spec list -> nut -> Kodkod.bound
1.10 val merge_bounds : Kodkod.bound list -> Kodkod.bound list
1.11 val kodkod_formula_from_nut :
1.12 int Typtab.table -> kodkod_constrs -> nut -> Kodkod.formula
1.13 + val needed_values_for_datatype :
1.14 + nut list -> int Typtab.table -> datatype_spec -> (nut * int) list option
1.15 val declarative_axiom_for_plain_rel : kodkod_constrs -> nut -> Kodkod.formula
1.16 val declarative_axioms_for_datatypes :
1.17 - hol_context -> bool -> nut list -> int -> int -> int Typtab.table
1.18 - -> kodkod_constrs -> nut NameTable.table -> datatype_spec list
1.19 - -> Kodkod.formula list
1.20 + hol_context -> bool -> nut list -> (typ * (nut * int) list option) list
1.21 + -> int -> int -> int Typtab.table -> kodkod_constrs -> nut NameTable.table
1.22 + -> datatype_spec list -> Kodkod.formula list
1.23 end;
1.24
1.25 structure Nitpick_Kodkod : NITPICK_KODKOD =
1.26 @@ -297,24 +300,39 @@
1.27 | bound_for_plain_rel _ _ u =
1.28 raise NUT ("Nitpick_Kodkod.bound_for_plain_rel", [u])
1.29
1.30 -fun bound_for_sel_rel ctxt debug dtypes
1.31 +fun bound_for_sel_rel ctxt debug need_vals dtypes
1.32 (FreeRel (x, T as Type (@{type_name fun}, [T1, T2]),
1.33 R as Func (Atom (_, j0), R2), nick)) =
1.34 let
1.35 + val constr_s = original_name nick
1.36 val {delta, epsilon, exclusive, explicit_max, ...} =
1.37 - constr_spec dtypes (original_name nick, T1)
1.38 + constr_spec dtypes (constr_s, T1)
1.39 + val dtype as {card, ...} = datatype_spec dtypes T1 |> the
1.40 + val need_vals =
1.41 + AList.lookup (op =) need_vals T1 |> the_default NONE |> these
1.42 in
1.43 ([(x, bound_comment ctxt debug nick T R)],
1.44 - if explicit_max = 0 then
1.45 - [KK.TupleSet []]
1.46 - else
1.47 - let val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0) in
1.48 + let
1.49 + val ts = KK.TupleAtomSeq (epsilon - delta, delta + j0)
1.50 + val complete_need_vals = (length need_vals = card)
1.51 + val (my_need_vals, other_need_vals) =
1.52 + need_vals
1.53 + |> List.partition
1.54 + (fn (Construct (sel_us, _, _, _), _) =>
1.55 + exists (fn FreeRel (x', _, _, _) => x = x'
1.56 + | _ => false) sel_us
1.57 + | _ => false)
1.58 + in
1.59 + if explicit_max = 0 orelse
1.60 + (complete_need_vals andalso null my_need_vals) then
1.61 + [KK.TupleSet []]
1.62 + else
1.63 if R2 = Formula Neut then
1.64 [ts] |> not exclusive ? cons (KK.TupleSet [])
1.65 else
1.66 [KK.TupleSet [],
1.67 if T1 = T2 andalso epsilon > delta andalso
1.68 - is_datatype_acyclic (the (datatype_spec dtypes T1)) then
1.69 + is_datatype_acyclic dtype then
1.70 index_seq delta (epsilon - delta)
1.71 |> map (fn j =>
1.72 KK.TupleProduct (KK.TupleSet [KK.Tuple [j + j0]],
1.73 @@ -324,7 +342,7 @@
1.74 KK.TupleProduct (ts, upper_bound_for_rep R2)]
1.75 end)
1.76 end
1.77 - | bound_for_sel_rel _ _ _ u =
1.78 + | bound_for_sel_rel _ _ _ _ u =
1.79 raise NUT ("Nitpick_Kodkod.bound_for_sel_rel", [u])
1.80
1.81 fun merge_bounds bs =
1.82 @@ -1478,8 +1496,8 @@
1.83 "malformed Kodkod formula")
1.84 end
1.85
1.86 -fun needed_value_axioms_for_datatype [] _ _ _ = []
1.87 - | needed_value_axioms_for_datatype need_us ofs kk
1.88 +fun needed_values_for_datatype [] _ _ = SOME []
1.89 + | needed_values_for_datatype need_us ofs
1.90 ({typ, card, constrs, ...} : datatype_spec) =
1.91 let
1.92 fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
1.93 @@ -1507,11 +1525,11 @@
1.94 else
1.95 accum)
1.96 | aux _ = I
1.97 - in
1.98 - case SOME (index_seq 0 card, []) |> fold aux need_us of
1.99 - SOME (_, fixed) => fixed |> map (atom_equation_for_nut ofs kk)
1.100 - | NONE => [KK.False]
1.101 - end
1.102 + in SOME (index_seq 0 card, []) |> fold aux need_us |> Option.map snd end
1.103 +
1.104 +fun needed_value_axioms_for_datatype _ _ NONE = [KK.False]
1.105 + | needed_value_axioms_for_datatype ofs kk (SOME fixed) =
1.106 + fixed |> map (atom_equation_for_nut ofs kk)
1.107
1.108 fun all_ge ({kk_join, kk_reflexive_closure, ...} : kodkod_constrs) z r =
1.109 kk_join r (kk_reflexive_closure (KK.Rel (suc_rel_for_atom_seq z)))
1.110 @@ -1679,7 +1697,6 @@
1.111 |> maps (sym_break_axioms_for_datatype hol_ctxt binarize kk rel_table
1.112 nfas dtypes)
1.113
1.114 -
1.115 fun sel_axiom_for_sel hol_ctxt binarize j0
1.116 (kk as {kk_all, kk_formula_if, kk_subset, kk_no, kk_join, ...})
1.117 rel_table dom_r ({const, delta, epsilon, exclusive, ...} : constr_spec)
1.118 @@ -1776,7 +1793,7 @@
1.119 partition_axioms_for_datatype j0 kk rel_table dtype
1.120 end
1.121
1.122 -fun declarative_axioms_for_datatypes hol_ctxt binarize need_us
1.123 +fun declarative_axioms_for_datatypes hol_ctxt binarize need_us need_vals
1.124 datatype_sym_break bits ofs kk rel_table dtypes =
1.125 let
1.126 val nfas =
1.127 @@ -1785,7 +1802,7 @@
1.128 |> strongly_connected_sub_nfas
1.129 in
1.130 acyclicity_axioms_for_datatypes kk nfas @
1.131 - maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @
1.132 + maps (needed_value_axioms_for_datatype ofs kk o snd) need_vals @
1.133 sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
1.134 kk rel_table nfas dtypes @
1.135 maps (other_axioms_for_datatype hol_ctxt binarize bits ofs kk rel_table)