don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 14:14:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 14:54:35 2010 +0200
@@ -319,7 +319,7 @@
fun nth_value_of_type n =
let
fun term unfold =
- reconstruct_term unfold pool wacky_names scope atomss sel_names
+ reconstruct_term true unfold pool wacky_names scope atomss sel_names
rel_table bounds T T (Atom (card, 0)) [[n]]
in
case term false of
@@ -331,7 +331,8 @@
| t => t
end
in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
-and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
+and reconstruct_term maybe_opt unfold pool
+ (wacky_names as ((maybe_name, abs_name), _))
(scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
bits, datatypes, ofs, ...})
atomss sel_names rel_table bounds =
@@ -607,6 +608,7 @@
| term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
(Func (R1, Formula Neut)) jss =
let
+val _ = priority ("HERE: " ^ (if maybe_opt then "y" else "n")) (* ### *)
val jss1 = all_combinations_for_rep R1
val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
val ts2 =
@@ -633,7 +635,7 @@
string_of_int (length jss))
in
postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
- oooo term_for_rep true []
+ oooo term_for_rep maybe_opt []
end
(** Constant postprocessing **)
@@ -830,13 +832,6 @@
(** Model reconstruction **)
-fun term_for_name pool scope atomss sel_names rel_table bounds name =
- let val T = type_of name in
- tuple_list_for_name rel_table bounds name
- |> reconstruct_term false pool (("", ""), ("", "")) scope atomss sel_names
- rel_table bounds T T (rep_of name)
- end
-
fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
$ Abs (s, T, Const (@{const_name "op ="}, _)
$ Bound 0 $ t')) =
@@ -890,11 +885,13 @@
val scope =
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
- fun term_for_rep unfold =
- reconstruct_term unfold pool wacky_names scope atomss sel_names rel_table
- bounds
+ fun term_for_rep maybe_opt unfold =
+ reconstruct_term maybe_opt unfold pool wacky_names scope atomss
+ sel_names rel_table bounds
fun nth_value_of_type card T n =
- let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in
+ let
+ fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
+ in
case aux false of
t as Const (s, _) =>
if String.isPrefix (cyclic_const_prefix ()) s then
@@ -932,7 +929,8 @@
Const (@{const_name undefined}, T')
else
tuple_list_for_name rel_table bounds name
- |> term_for_rep false T T' (rep_of name)
+ |> term_for_rep (not (is_fully_representable_set name)) false
+ T T' (rep_of name)
in
Pretty.block (Pretty.breaks
[setmp_show_all_types (Syntax.pretty_term ctxt) t1,
@@ -1011,6 +1009,14 @@
forall (is_codatatype_wellformed codatatypes) codatatypes)
end
+fun term_for_name pool scope atomss sel_names rel_table bounds name =
+ let val T = type_of name in
+ tuple_list_for_name rel_table bounds name
+ |> reconstruct_term (not (is_fully_representable_set name)) false pool
+ (("", ""), ("", "")) scope atomss sel_names rel_table
+ bounds T T (rep_of name)
+ end
+
fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
card_assigns, ...})
auto_timeout free_names sel_names rel_table bounds prop =
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 01 14:14:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 01 14:54:35 2010 +0200
@@ -105,6 +105,7 @@
val the_name : 'a NameTable.table -> nut -> 'a
val the_rel : nut NameTable.table -> nut -> Kodkod.n_ary_index
val nut_from_term : hol_context -> op2 -> term -> nut
+ val is_fully_representable_set : nut -> bool
val choose_reps_for_free_vars :
scope -> nut list -> rep NameTable.table -> nut list * rep NameTable.table
val choose_reps_for_consts :
@@ -677,6 +678,23 @@
end
in aux eq [] [] end
+fun is_fully_representable_set u =
+ not (is_opt_rep (rep_of u)) andalso
+ case u of
+ FreeName _ => true
+ | Op1 (SingletonSet, _, _, _) => true
+ | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
+ | Op2 (oper, _, _, u1, u2) =>
+ if oper = Union orelse oper = SetDifference orelse oper = Intersect then
+ forall is_fully_representable_set [u1, u2]
+ else if oper = Apply then
+ case u1 of
+ ConstName (s, _, _) => is_sel_like_and_no_discr s
+ | _ => false
+ else
+ false
+ | _ => false
+
fun rep_for_abs_fun scope T =
let val (R1, R2) = best_non_opt_symmetric_reps_for_fun_type scope T in
Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
@@ -766,22 +784,6 @@
fun unknown_boolean T R =
Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
T, R)
-fun is_fully_representable_set u =
- not (is_opt_rep (rep_of u)) andalso
- case u of
- FreeName _ => true
- | Op1 (SingletonSet, _, _, _) => true
- | Op1 (Converse, _, _, u1) => is_fully_representable_set u1
- | Op2 (oper, _, _, u1, u2) =>
- if oper = Union orelse oper = SetDifference orelse oper = Intersect then
- forall is_fully_representable_set [u1, u2]
- else if oper = Apply then
- case u1 of
- ConstName (s, _, _) => is_sel_like_and_no_discr s
- | _ => false
- else
- false
- | _ => false
fun s_op1 oper T R u1 =
((if oper = Not then