# HG changeset patch # User blanchet # Date 1275396875 -7200 # Node ID c0fe8fa357718a8d7e9f0546d473cfeb314d31e6 # Parent 8a89fd40ed0bca963b39d4336db7f77acb8b9f33 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 diff -r 8a89fd40ed0b -r c0fe8fa35771 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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 = diff -r 8a89fd40ed0b -r c0fe8fa35771 src/HOL/Tools/Nitpick/nitpick_nut.ML --- 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