--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 10:55:41 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Thu Mar 03 11:20:48 2011 +0100
@@ -1478,8 +1478,8 @@
"malformed Kodkod formula")
end
-fun preconstructed_value_axioms_for_datatype [] _ _ _ = []
- | preconstructed_value_axioms_for_datatype preconstr_us ofs kk
+fun needed_value_axioms_for_datatype [] _ _ _ = []
+ | needed_value_axioms_for_datatype need_us ofs kk
({typ, card, constrs, ...} : datatype_spec) =
let
fun aux (u as Construct (FreeRel (_, _, _, s) :: _, T, _, us)) =
@@ -1507,10 +1507,9 @@
else
accum)
| aux u =
- raise NUT ("Nitpick_Kodkod.preconstructed_value_axioms_for_datatype\
- \.aux", [u])
+ raise NUT ("Nitpick_Kodkod.needed_value_axioms_for_datatype.aux", [u])
in
- case SOME (index_seq 0 card, []) |> fold aux preconstr_us of
+ 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
@@ -1654,14 +1653,14 @@
nfas dtypes)
end
-fun is_datatype_in_preconstructed_value T (Construct (_, T', _, us)) =
- T = T' orelse exists (is_datatype_in_preconstructed_value T) us
- | is_datatype_in_preconstructed_value _ _ = false
+fun is_datatype_in_needed_value T (Construct (_, T', _, us)) =
+ T = T' orelse exists (is_datatype_in_needed_value T) us
+ | is_datatype_in_needed_value _ _ = false
val min_sym_break_card = 7
-fun sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
- datatype_sym_break kk rel_table nfas dtypes =
+fun sym_break_axioms_for_datatypes hol_ctxt binarize need_us datatype_sym_break
+ kk rel_table nfas dtypes =
if datatype_sym_break = 0 then
[]
else
@@ -1673,8 +1672,7 @@
o binder_types o snd o #const) constrs)
|> filter_out
(fn {typ, ...} =>
- exists (is_datatype_in_preconstructed_value typ)
- preconstr_us)
+ exists (is_datatype_in_needed_value typ) need_us)
|> (fn dtypes' =>
dtypes' |> length dtypes' > datatype_sym_break
? (sort (datatype_ord o swap)
@@ -1779,7 +1777,7 @@
partition_axioms_for_datatype j0 kk rel_table dtype
end
-fun declarative_axioms_for_datatypes hol_ctxt binarize preconstr_us
+fun declarative_axioms_for_datatypes hol_ctxt binarize need_us
datatype_sym_break bits ofs kk rel_table dtypes =
let
val nfas =
@@ -1788,9 +1786,9 @@
|> strongly_connected_sub_nfas
in
acyclicity_axioms_for_datatypes kk nfas @
- maps (preconstructed_value_axioms_for_datatype preconstr_us ofs kk) dtypes @
- sym_break_axioms_for_datatypes hol_ctxt binarize preconstr_us
- datatype_sym_break kk rel_table nfas dtypes @
+ maps (needed_value_axioms_for_datatype need_us ofs kk) dtypes @
+ 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
end