src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 37262 c0fe8fa35771
parent 37261 8a89fd40ed0b
child 37265 9f2c3d3c8f0f
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 14:14:02 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 01 14:54:35 2010 +0200
     1.3 @@ -319,7 +319,7 @@
     1.4      fun nth_value_of_type n =
     1.5        let
     1.6          fun term unfold =
     1.7 -          reconstruct_term unfold pool wacky_names scope atomss sel_names
     1.8 +          reconstruct_term true unfold pool wacky_names scope atomss sel_names
     1.9                             rel_table bounds T T (Atom (card, 0)) [[n]]
    1.10        in
    1.11          case term false of
    1.12 @@ -331,7 +331,8 @@
    1.13          | t => t
    1.14        end
    1.15    in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
    1.16 -and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
    1.17 +and reconstruct_term maybe_opt unfold pool
    1.18 +        (wacky_names as ((maybe_name, abs_name), _))
    1.19          (scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
    1.20                     bits, datatypes, ofs, ...})
    1.21          atomss sel_names rel_table bounds =
    1.22 @@ -607,6 +608,7 @@
    1.23        | term_for_rep maybe_opt seen (Type (@{type_name fun}, [T1, T2])) T'
    1.24                       (Func (R1, Formula Neut)) jss =
    1.25          let
    1.26 +val _ = priority ("HERE: " ^ (if maybe_opt then "y" else "n")) (* ### *)
    1.27            val jss1 = all_combinations_for_rep R1
    1.28            val ts1 = map (term_for_rep true seen T1 T1 R1 o single) jss1
    1.29            val ts2 =
    1.30 @@ -633,7 +635,7 @@
    1.31                     string_of_int (length jss))
    1.32    in
    1.33      postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
    1.34 -    oooo term_for_rep true []
    1.35 +    oooo term_for_rep maybe_opt []
    1.36    end
    1.37  
    1.38  (** Constant postprocessing **)
    1.39 @@ -830,13 +832,6 @@
    1.40  
    1.41  (** Model reconstruction **)
    1.42  
    1.43 -fun term_for_name pool scope atomss sel_names rel_table bounds name =
    1.44 -  let val T = type_of name in
    1.45 -    tuple_list_for_name rel_table bounds name
    1.46 -    |> reconstruct_term false pool (("", ""), ("", "")) scope atomss sel_names
    1.47 -                        rel_table bounds T T (rep_of name)
    1.48 -  end
    1.49 -
    1.50  fun unfold_outer_the_binders (t as Const (@{const_name The}, _)
    1.51                                     $ Abs (s, T, Const (@{const_name "op ="}, _)
    1.52                                                  $ Bound 0 $ t')) =
    1.53 @@ -890,11 +885,13 @@
    1.54      val scope =
    1.55        {hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
    1.56         bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
    1.57 -    fun term_for_rep unfold =
    1.58 -      reconstruct_term unfold pool wacky_names scope atomss sel_names rel_table
    1.59 -                       bounds
    1.60 +    fun term_for_rep maybe_opt unfold =
    1.61 +      reconstruct_term maybe_opt unfold pool wacky_names scope atomss
    1.62 +                       sel_names rel_table bounds
    1.63      fun nth_value_of_type card T n =
    1.64 -      let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in
    1.65 +      let
    1.66 +        fun aux unfold = term_for_rep true unfold T T (Atom (card, 0)) [[n]]
    1.67 +      in
    1.68          case aux false of
    1.69            t as Const (s, _) =>
    1.70            if String.isPrefix (cyclic_const_prefix ()) s then
    1.71 @@ -932,7 +929,8 @@
    1.72                     Const (@{const_name undefined}, T')
    1.73                   else
    1.74                     tuple_list_for_name rel_table bounds name
    1.75 -                   |> term_for_rep false T T' (rep_of name)
    1.76 +                   |> term_for_rep (not (is_fully_representable_set name)) false
    1.77 +                                   T T' (rep_of name)
    1.78        in
    1.79          Pretty.block (Pretty.breaks
    1.80              [setmp_show_all_types (Syntax.pretty_term ctxt) t1,
    1.81 @@ -1011,6 +1009,14 @@
    1.82       forall (is_codatatype_wellformed codatatypes) codatatypes)
    1.83    end
    1.84  
    1.85 +fun term_for_name pool scope atomss sel_names rel_table bounds name =
    1.86 +  let val T = type_of name in
    1.87 +    tuple_list_for_name rel_table bounds name
    1.88 +    |> reconstruct_term (not (is_fully_representable_set name)) false pool
    1.89 +                        (("", ""), ("", "")) scope atomss sel_names rel_table
    1.90 +                        bounds T T (rep_of name)
    1.91 +  end
    1.92 +
    1.93  fun prove_hol_model (scope as {hol_ctxt = {thy, ctxt, debug, ...},
    1.94                                 card_assigns, ...})
    1.95                      auto_timeout free_names sel_names rel_table bounds prop =