# HG changeset patch
# User blanchet
# Date 1281084652 -7200
# Node ID a7e92239922f17030011de312778e4f97df0f313
# Parent  7f4755c5e77b89d4e170c988a2341477a668696b
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"

diff -r 7f4755c5e77b -r a7e92239922f src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 05 21:56:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 06 10:50:52 2010 +0200
@@ -240,13 +240,14 @@
                 else orig_t
     val tfree_table =
       if merge_type_vars then
-        merged_type_var_table_for_terms (neg_t :: assm_ts @ evals)
+        merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals)
       else
         []
-    val neg_t = merge_type_vars_in_term merge_type_vars tfree_table neg_t
-    val assm_ts = map (merge_type_vars_in_term merge_type_vars tfree_table)
+    val neg_t = merge_type_vars_in_term thy merge_type_vars tfree_table neg_t
+    val assm_ts = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
                       assm_ts
-    val evals = map (merge_type_vars_in_term merge_type_vars tfree_table) evals
+    val evals = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
+                    evals
     val original_max_potential = max_potential
     val original_max_genuine = max_genuine
     val max_bisim_depth = fold Integer.max bisim_depths ~1
diff -r 7f4755c5e77b -r a7e92239922f src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 21:56:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 10:50:52 2010 +0200
@@ -212,8 +212,10 @@
   val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
   val equational_fun_axioms : hol_context -> styp -> term list
   val is_equational_fun_surely_complete : hol_context -> styp -> bool
-  val merged_type_var_table_for_terms : term list -> (sort * string) list
-  val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term
+  val merged_type_var_table_for_terms :
+    theory -> term list -> (sort * string) list
+  val merge_type_vars_in_term :
+    theory -> bool -> (sort * string) list -> term -> term
   val ground_types_in_type : hol_context -> bool -> typ -> typ list
   val ground_types_in_terms : hol_context -> bool -> term list -> typ list
 end;
@@ -2255,21 +2257,25 @@
 
 (** Type preprocessing **)
 
-fun merged_type_var_table_for_terms ts =
+fun merged_type_var_table_for_terms thy ts =
   let
-    fun add_type (TFree (s, S)) table =
-        (case AList.lookup (op =) table S of
-           SOME s' =>
-           if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
-           else table
-         | NONE => (S, s) :: table)
-      | add_type _ table = table
-  in fold (fold_types (fold_atyps add_type)) ts [] end
+    fun add (s, S) table =
+      table
+      |> (case AList.lookup (Sign.subsort thy o swap) table S of
+            SOME _ => I
+          | NONE =>
+            filter_out (fn (S', _) => Sign.subsort thy (S, S'))
+            #> cons (S, s))
+    val tfrees = [] |> fold Term.add_tfrees ts
+                    |> sort (string_ord o pairself fst)
+  in [] |> fold add tfrees |> rev end
 
-fun merge_type_vars_in_term merge_type_vars table =
+fun merge_type_vars_in_term thy merge_type_vars table =
   merge_type_vars
   ? map_types (map_atyps
-        (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S)
+        (fn TFree (_, S) =>
+            TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S))
+                         |> the |> swap)
           | T => T))
 
 fun add_ground_types hol_ctxt binarize =
diff -r 7f4755c5e77b -r a7e92239922f src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 21:56:22 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Aug 06 10:50:52 2010 +0200
@@ -902,7 +902,7 @@
                  |> (fn dtypes' =>
                         dtypes'
                         |> length dtypes' > datatype_sym_break
-                           ? (sort (rev_order o datatype_ord)
+                           ? (sort (datatype_ord o swap)
                               #> take datatype_sym_break)))
 
 fun sel_axiom_for_sel hol_ctxt binarize j0