robust handling of types occurring in "eval" and "preconstr" options but not in the goal
authorblanchet
Wed Mar 02 13:09:57 2011 +0100 (2011-03-02 ago)
changeset 418699e367f1c9570
parent 41868 a4fb98eb0edf
child 41870 a14a492f472f
robust handling of types occurring in "eval" and "preconstr" options but not in the goal
src/HOL/Tools/Nitpick/nitpick.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 02 13:09:57 2011 +0100
     1.3 @@ -258,16 +258,16 @@
     1.4                       o Date.fromTimeLocal o Time.now)
     1.5      val neg_t = if falsify then Logic.mk_implies (orig_t, @{prop False})
     1.6                  else orig_t
     1.7 +    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
     1.8      val tfree_table =
     1.9 -      if merge_type_vars then
    1.10 -        merged_type_var_table_for_terms thy (neg_t :: assm_ts @ evals)
    1.11 -      else
    1.12 -        []
    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 thy merge_type_vars tfree_table)
    1.17 -                    evals
    1.18 +      if merge_type_vars then merged_type_var_table_for_terms thy conj_ts
    1.19 +      else []
    1.20 +    val merge_tfrees = merge_type_vars_in_term thy merge_type_vars tfree_table
    1.21 +    val neg_t = neg_t |> merge_tfrees
    1.22 +    val assm_ts = assm_ts |> map merge_tfrees
    1.23 +    val evals = evals |> map merge_tfrees
    1.24 +    val preconstrs = preconstrs |> map (apfst (Option.map merge_tfrees))
    1.25 +    val conj_ts = neg_t :: assm_ts @ evals @ map_filter fst preconstrs
    1.26      val original_max_potential = max_potential
    1.27      val original_max_genuine = max_genuine
    1.28      val max_bisim_depth = fold Integer.max bisim_depths ~1
    1.29 @@ -299,9 +299,9 @@
    1.30         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
    1.31         constr_cache = Unsynchronized.ref []}
    1.32      val pseudo_frees = []
    1.33 -    val real_frees = fold Term.add_frees (neg_t :: assm_ts) []
    1.34 -    val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
    1.35 -            raise NOT_SUPPORTED "schematic type variables"
    1.36 +    val real_frees = fold Term.add_frees conj_ts []
    1.37 +    val _ = null (fold Term.add_tvars conj_ts []) orelse
    1.38 +            error "Nitpick cannot handle goals with schematic type variables."
    1.39      val (nondef_ts, def_ts, preconstr_ts, got_all_mono_user_axioms,
    1.40           no_poly_user_axioms, binarize) =
    1.41        preprocess_formulas hol_ctxt assm_ts neg_t