improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
authorblanchet
Fri Aug 06 10:50:52 2010 +0200 (2010-08-06)
changeset 38212a7e92239922f
parent 38210 7f4755c5e77b
child 38213 d4cbc80e7271
improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Aug 05 21:56:22 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Aug 06 10:50:52 2010 +0200
     1.3 @@ -240,13 +240,14 @@
     1.4                  else orig_t
     1.5      val tfree_table =
     1.6        if merge_type_vars then
     1.7 -        merged_type_var_table_for_terms (neg_t :: assm_ts @ evals)
     1.8 +        merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals)
     1.9        else
    1.10          []
    1.11 -    val neg_t = merge_type_vars_in_term merge_type_vars tfree_table neg_t
    1.12 -    val assm_ts = map (merge_type_vars_in_term merge_type_vars tfree_table)
    1.13 +    val neg_t = merge_type_vars_in_term thy merge_type_vars tfree_table neg_t
    1.14 +    val assm_ts = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
    1.15                        assm_ts
    1.16 -    val evals = map (merge_type_vars_in_term merge_type_vars tfree_table) evals
    1.17 +    val evals = map (merge_type_vars_in_term thy merge_type_vars tfree_table)
    1.18 +                    evals
    1.19      val original_max_potential = max_potential
    1.20      val original_max_genuine = max_genuine
    1.21      val max_bisim_depth = fold Integer.max bisim_depths ~1
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Aug 05 21:56:22 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Aug 06 10:50:52 2010 +0200
     2.3 @@ -212,8 +212,10 @@
     2.4    val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term
     2.5    val equational_fun_axioms : hol_context -> styp -> term list
     2.6    val is_equational_fun_surely_complete : hol_context -> styp -> bool
     2.7 -  val merged_type_var_table_for_terms : term list -> (sort * string) list
     2.8 -  val merge_type_vars_in_term : bool -> (sort * string) list -> term -> term
     2.9 +  val merged_type_var_table_for_terms :
    2.10 +    theory -> term list -> (sort * string) list
    2.11 +  val merge_type_vars_in_term :
    2.12 +    theory -> bool -> (sort * string) list -> term -> term
    2.13    val ground_types_in_type : hol_context -> bool -> typ -> typ list
    2.14    val ground_types_in_terms : hol_context -> bool -> term list -> typ list
    2.15  end;
    2.16 @@ -2255,21 +2257,25 @@
    2.17  
    2.18  (** Type preprocessing **)
    2.19  
    2.20 -fun merged_type_var_table_for_terms ts =
    2.21 +fun merged_type_var_table_for_terms thy ts =
    2.22    let
    2.23 -    fun add_type (TFree (s, S)) table =
    2.24 -        (case AList.lookup (op =) table S of
    2.25 -           SOME s' =>
    2.26 -           if string_ord (s', s) = LESS then AList.update (op =) (S, s') table
    2.27 -           else table
    2.28 -         | NONE => (S, s) :: table)
    2.29 -      | add_type _ table = table
    2.30 -  in fold (fold_types (fold_atyps add_type)) ts [] end
    2.31 +    fun add (s, S) table =
    2.32 +      table
    2.33 +      |> (case AList.lookup (Sign.subsort thy o swap) table S of
    2.34 +            SOME _ => I
    2.35 +          | NONE =>
    2.36 +            filter_out (fn (S', _) => Sign.subsort thy (S, S'))
    2.37 +            #> cons (S, s))
    2.38 +    val tfrees = [] |> fold Term.add_tfrees ts
    2.39 +                    |> sort (string_ord o pairself fst)
    2.40 +  in [] |> fold add tfrees |> rev end
    2.41  
    2.42 -fun merge_type_vars_in_term merge_type_vars table =
    2.43 +fun merge_type_vars_in_term thy merge_type_vars table =
    2.44    merge_type_vars
    2.45    ? map_types (map_atyps
    2.46 -        (fn TFree (_, S) => TFree (AList.lookup (op =) table S |> the, S)
    2.47 +        (fn TFree (_, S) =>
    2.48 +            TFree (table |> find_first (fn (S', _) => Sign.subsort thy (S', S))
    2.49 +                         |> the |> swap)
    2.50            | T => T))
    2.51  
    2.52  fun add_ground_types hol_ctxt binarize =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Thu Aug 05 21:56:22 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Fri Aug 06 10:50:52 2010 +0200
     3.3 @@ -902,7 +902,7 @@
     3.4                   |> (fn dtypes' =>
     3.5                          dtypes'
     3.6                          |> length dtypes' > datatype_sym_break
     3.7 -                           ? (sort (rev_order o datatype_ord)
     3.8 +                           ? (sort (datatype_ord o swap)
     3.9                                #> take datatype_sym_break)))
    3.10  
    3.11  fun sel_axiom_for_sel hol_ctxt binarize j0