# HG changeset patch
# User blanchet
# Date 1280794685 -7200
# Node ID d74b66ec02ceafbdc4be9d21f7db86f9b42a020d
# Parent  b517845154717ed433fcd609f4ac8d3cfd585372
handle free variables even more gracefully;
1. show those that only occur in assumptions as part of the constants;
2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld

diff -r b51784515471 -r d74b66ec02ce src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 01:16:08 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Aug 03 02:18:05 2010 +0200
@@ -274,7 +274,8 @@
        skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
-    val frees = fold Term.add_frees (neg_t :: assm_ts) []
+    val pseudo_frees = fold Term.add_frees assm_ts []
+    val real_frees = subtract (op =) pseudo_frees (Term.add_frees neg_t [])
     val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
@@ -451,7 +452,6 @@
                          (Typtab.dest ofs)
 *)
         val all_exact = forall (is_exact_type datatypes true) all_Ts
-        val repify_consts = choose_reps_for_consts scope all_exact
         val main_j0 = offset_of_type ofs bool_T
         val (nat_card, nat_j0) = spec_of_type scope nat_T
         val (int_card, int_j0) = spec_of_type scope int_T
@@ -460,9 +460,11 @@
                            "bad offsets")
         val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
         val (free_names, rep_table) =
-          choose_reps_for_free_vars scope free_names NameTable.empty
+          choose_reps_for_free_vars scope pseudo_frees free_names
+                                    NameTable.empty
         val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table
-        val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table
+        val (nonsel_names, rep_table) =
+          choose_reps_for_consts scope all_exact nonsel_names rep_table
         val min_highest_arity =
           NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1
         val min_univ_card =
@@ -589,8 +591,8 @@
         val (reconstructed_model, codatatypes_ok) =
           reconstruct_hol_model {show_datatypes = show_datatypes,
                                  show_consts = show_consts}
-              scope formats atomss frees free_names sel_names nonsel_names
-              rel_table bounds
+              scope formats atomss real_frees pseudo_frees free_names sel_names
+              nonsel_names rel_table bounds
         val genuine_means_genuine =
           got_all_user_axioms andalso none_true wfs andalso
           sound_finitizes andalso codatatypes_ok
diff -r b51784515471 -r d74b66ec02ce src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Aug 03 01:16:08 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Aug 03 02:18:05 2010 +0200
@@ -32,8 +32,8 @@
   val dest_plain_fun : term -> bool * (term list * term list)
   val reconstruct_hol_model :
     params -> scope -> (term option * int list) list
-    -> (typ option * string list) list -> styp list -> nut list -> nut list
-    -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
+    -> (typ option * string list) list -> styp list -> styp list -> nut list
+    -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
     -> Pretty.T * bool
   val prove_hol_model :
     scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
@@ -861,8 +861,8 @@
                       ground_thm_table, ersatz_table, skolems, special_funs,
                       unrolled_preds, wf_cache, constr_cache},
          binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
-        formats atomss all_frees free_names sel_names nonsel_names rel_table
-        bounds =
+        formats atomss real_frees pseudo_frees free_names sel_names nonsel_names
+        rel_table bounds =
   let
     val pool = Unsynchronized.ref []
     val (wacky_names as (_, base_step_names), ctxt) =
@@ -977,6 +977,14 @@
                (sort_wrt (original_name o nickname_of) names)
       else
         []
+    fun free_name_for_term keep_all (x as (s, T)) =
+      case filter (curry (op =) x
+                   o pairf nickname_of (uniterize_unarize_unbox_etc_type
+                                        o type_of)) free_names of
+        [name] => SOME name
+      | [] => if keep_all then SOME (FreeName (s, T, Any)) else NONE
+      | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model.\
+                         \free_name_for_term", [Const x])
     val (skolem_names, nonskolem_nonsel_names) =
       List.partition is_skolem_name nonsel_names
     val (eval_names, noneval_nonskolem_nonsel_names) =
@@ -985,17 +993,9 @@
       ||> filter_out (member (op =) [@{const_name bisim},
                                      @{const_name bisim_iterator_max}]
                       o nickname_of)
-    val free_names =
-      map (fn x as (s, T) =>
-              case filter (curry (op =) x
-                       o pairf nickname_of
-                               (uniterize_unarize_unbox_etc_type o type_of))
-                       free_names of
-                [name] => name
-              | [] => FreeName (s, T, Any)
-              | _ => raise TERM ("Nitpick_Model.reconstruct_hol_model",
-                                 [Const x])) all_frees
-    val chunks = block_of_names true "Free variable" free_names @
+      ||> append (map_filter (free_name_for_term false) pseudo_frees)
+    val real_free_names = map_filter (free_name_for_term true) real_frees
+    val chunks = block_of_names true "Free variable" real_free_names @
                  block_of_names true "Skolem constant" skolem_names @
                  block_of_names true "Evaluated term" eval_names @
                  block_of_datatypes @ block_of_codatatypes @
diff -r b51784515471 -r d74b66ec02ce src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 03 01:16:08 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Aug 03 02:18:05 2010 +0200
@@ -7,6 +7,7 @@
 
 signature NITPICK_NUT =
 sig
+  type styp = Nitpick_Util.styp
   type hol_context = Nitpick_HOL.hol_context
   type scope = Nitpick_Scope.scope
   type name_pool = Nitpick_Peephole.name_pool
@@ -104,7 +105,8 @@
   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
+    scope -> styp list -> nut list -> rep NameTable.table
+    -> nut list * rep NameTable.table
   val choose_reps_for_consts :
     scope -> bool -> nut list -> rep NameTable.table
     -> nut list * rep NameTable.table
@@ -671,9 +673,12 @@
     Func (R1, (card_of_rep R1 <> card_of_rep R2 ? Opt) R2)
   end
 
-fun choose_rep_for_free_var scope v (vs, table) =
+fun choose_rep_for_free_var scope pseudo_frees v (vs, table) =
   let
-    val R = best_non_opt_set_rep_for_type scope (type_of v)
+    val R = (if exists (curry (op =) (nickname_of v) o fst) pseudo_frees then
+               best_opt_set_rep_for_type
+             else
+               best_non_opt_set_rep_for_type) scope (type_of v)
     val v = modify_name_rep v R
   in (v :: vs, NameTable.update (v, R) table) end
 fun choose_rep_for_const (scope as {hol_ctxt = {ctxt, ...}, ...}) all_exact v
@@ -701,8 +706,8 @@
     val v = modify_name_rep v R
   in (v :: vs, NameTable.update (v, R) table) end
 
-fun choose_reps_for_free_vars scope vs table =
-  fold (choose_rep_for_free_var scope) vs ([], table)
+fun choose_reps_for_free_vars scope pseudo_frees vs table =
+  fold (choose_rep_for_free_var scope pseudo_frees) vs ([], table)
 fun choose_reps_for_consts scope all_exact vs table =
   fold (choose_rep_for_const scope all_exact) vs ([], table)
 
diff -r b51784515471 -r d74b66ec02ce src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Aug 03 01:16:08 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Aug 03 02:18:05 2010 +0200
@@ -827,14 +827,15 @@
                                          list_comb (Const x2, bounds2 @ args2)))
   end
 
-fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) xs =
+fun special_congruence_axioms (hol_ctxt as {special_funs, ...}) ts =
   let
     val groups =
       !special_funs
       |> map (fn ((x, js, ts), x') => (x, (js, ts, x')))
       |> AList.group (op =)
       |> filter_out (is_equational_fun_surely_complete hol_ctxt o fst)
-      |> map (fn (x, zs) => (x, zs |> member (op =) xs x ? cons ([], [], x)))
+      |> map (fn (x, zs) =>
+                 (x, zs |> member (op =) ts (Const x) ? cons ([], [], x)))
     fun generality (js, _, _) = ~(length js)
     fun is_more_specific (j1, t1, x1) (j2, t2, x2) =
       x1 <> x2 andalso length j2 < length j1 andalso
@@ -856,21 +857,20 @@
 
 fun defined_free_by_assumption t =
   let
-    fun do_equals t1 t2 =
-      if exists_subterm (curry (op aconv) t1) t2 then NONE else SOME t1
+    fun do_equals x def =
+      if exists_subterm (curry (op aconv) (Free x)) def then NONE else SOME x
   in
     case t of
-      Const (@{const_name "=="}, _) $ (t1 as Free _) $ t2 => do_equals t1 t2
-    | @{const Trueprop} $ (Const (@{const_name "=="}, _)
-                           $ (t1 as Free _) $ t2) =>
-      do_equals t1 t2
+      Const (@{const_name "=="}, _) $ Free x $ def => do_equals x def
+    | @{const Trueprop} $ (Const (@{const_name "=="}, _) $ Free x $ def) =>
+      do_equals x def
     | _ => NONE
   end
 
 fun assumption_exclusively_defines_free assm_ts t =
   case defined_free_by_assumption t of
-    SOME t1 =>
-    length (filter ((fn SOME t1' => t1 aconv t1' | NONE => false)
+    SOME x =>
+    length (filter ((fn SOME x' => x = x' | NONE => false)
                      o defined_free_by_assumption) assm_ts) = 1
   | NONE => false
 
@@ -890,8 +890,11 @@
                       fast_descrs, evals, def_table, nondef_table,
                       choice_spec_table, user_nondefs, ...}) assm_ts neg_t =
   let
+    val (def_assm_ts, nondef_assm_ts) =
+      List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
+    val def_assm_table = map (`(the o defined_free_by_assumption)) def_assm_ts
     type accumulator = styp list * (term list * term list)
-    fun add_axiom get app depth t (accum as (xs, axs)) =
+    fun add_axiom get app depth t (accum as (seen, axs)) =
       let
         val t = t |> unfold_defs_in_term hol_ctxt
                   |> skolemize_term_and_more hol_ctxt ~1 (*### why ~1? *)
@@ -901,7 +904,7 @@
         else
           let val t' = t |> specialize_consts_in_term hol_ctxt depth in
             if exists (member (op aconv) (get axs)) [t, t'] then accum
-            else add_axioms_for_term (depth + 1) t' (xs, app (cons t') axs)
+            else add_axioms_for_term (depth + 1) t' (seen, app (cons t') axs)
           end
       end
     and add_def_axiom depth = add_axiom fst apfst depth
@@ -912,15 +915,15 @@
     and add_eq_axiom depth t =
       (if is_constr_pattern_formula ctxt t then add_def_axiom
        else add_nondef_axiom) depth t
-    and add_axioms_for_term depth t (accum as (xs, axs)) =
+    and add_axioms_for_term depth t (accum as (seen, axs)) =
       case t of
         t1 $ t2 => accum |> fold (add_axioms_for_term depth) [t1, t2]
       | Const (x as (s, T)) =>
-        (if member (op =) xs x orelse
+        (if member (op aconv) seen t orelse
             is_built_in_const thy stds fast_descrs x then
            accum
          else
-           let val accum = (x :: xs, axs) in
+           let val accum = (t :: seen, axs) in
              if depth > axioms_max_depth then
                raise TOO_LARGE ("Nitpick_Preproc.axioms_for_term.\
                                 \add_axioms_for_term",
@@ -983,7 +986,13 @@
                                (nondef_props_for_const thy false nondef_table x)
            end)
         |> add_axioms_for_type depth T
-      | Free (_, T) => add_axioms_for_type depth T accum
+      | Free (x as (_, T)) =>
+        (if member (op aconv) seen t then
+           accum
+         else case AList.lookup (op =) def_assm_table x of
+           SOME t => add_def_axiom depth t accum
+         | NONE => accum)
+        |> add_axioms_for_type depth T
       | Var (_, T) => add_axioms_for_type depth T accum
       | Bound _ => accum
       | Abs (_, T, t) => accum |> add_axioms_for_term depth t
@@ -1028,16 +1037,13 @@
       List.partition (null o Term.hidden_polymorphism) user_nondefs
     val eval_axioms = map2 eval_axiom_for_term (index_seq 0 (length evals))
                            evals
-    val (def_assm_ts, nondef_assm_ts) =
-      List.partition (assumption_exclusively_defines_free assm_ts) assm_ts
-    val (xs, (defs, nondefs)) =
+    val (seen, (defs, nondefs)) =
       ([], ([], []))
       |> add_axioms_for_term 1 neg_t
-      |> fold_rev (add_def_axiom 1) def_assm_ts
       |> fold_rev (add_nondef_axiom 1) nondef_assm_ts
       |> fold_rev (add_def_axiom 1) eval_axioms
       |> user_axioms = SOME true ? fold (add_nondef_axiom 1) mono_user_nondefs
-    val defs = defs @ special_congruence_axioms hol_ctxt xs
+    val defs = defs @ special_congruence_axioms hol_ctxt seen
     val got_all_mono_user_axioms =
       (user_axioms = SOME true orelse null mono_user_nondefs)
   in