more readable error message if some types do not correspond to sort constraints of the datatype
authorkuncar
Sat May 02 13:58:06 2015 +0200 (2015-05-02)
changeset 6023417ff843807cb
parent 60233 89d500d7e3eb
child 60235 3cab6f891c2f
more readable error message if some types do not correspond to sort constraints of the datatype
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
     1.3 @@ -495,6 +495,18 @@
     1.4                Raw_Simplifier.rewrite_goal_tac ctxt simp_rules, rtac TrueI ]] i
     1.5          end
     1.6      end
     1.7 +    
     1.8 +    (* stolen from bnf_fp_n2m.ML *)
     1.9 +    fun force_typ ctxt T =
    1.10 +      Term.map_types Type_Infer.paramify_vars
    1.11 +      #> Type.constraint T
    1.12 +      #> singleton (Type_Infer_Context.infer_types ctxt);
    1.13 +
    1.14 +    (* The following tests that types in rty have corresponding arities imposed by constraints of
    1.15 +       the datatype fp. Otherwise rep_isom_code_tac could fail (especially transfer in it) is such
    1.16 +       a way that it is not easy to infer the problem with sorts.
    1.17 +    *)
    1.18 +    val _ = yield_singleton (mk_Frees "x") (#T fp) lthy |> fst |> force_typ lthy qty
    1.19  
    1.20      val rep_isom_code = Goal.prove_sorry lthy [] [] rep_isom_code_goal
    1.21        (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1)