handle type class annotations on (co)datatype parameters gracefully
authorblanchet
Thu Aug 29 18:24:11 2013 +0200 (2013-08-29)
changeset 53268de1dc709f9d4
parent 53266 89f7f1cc9ae3
child 53269 854fbb41e6cd
handle type class annotations on (co)datatype parameters gracefully
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Aug 29 17:57:25 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Aug 29 18:24:11 2013 +0200
     1.3 @@ -199,15 +199,17 @@
     1.4        Binding.qualify mandatory data_b_name o
     1.5        (rep_compat ? Binding.qualify false rep_compat_prefix);
     1.6  
     1.7 -    fun tfree_name_of (TFree (s, _)) = s
     1.8 -      | tfree_name_of (TVar ((s, _), _)) = s
     1.9 -      | tfree_name_of (Type (s, _)) = Long_Name.base_name s;
    1.10 +    fun dest_TFree_or_TVar (TFree p) = p
    1.11 +      | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
    1.12 +      | dest_TFree_or_TVar _ = error "Invalid type argument";
    1.13  
    1.14 -    val (As, B) =
    1.15 +    val (unsorted_As, B) =
    1.16        no_defs_lthy
    1.17 -      |> variant_tfrees (map tfree_name_of As0)
    1.18 +      |> variant_tfrees (map (fst o dest_TFree_or_TVar) As0)
    1.19        ||> the_single o fst o mk_TFrees 1;
    1.20  
    1.21 +    val As = map2 (resort_tfree o snd o dest_TFree_or_TVar) As0 unsorted_As;
    1.22 +
    1.23      val dataT = Type (dataT_name, As);
    1.24      val ctrs = map (mk_ctr As) ctrs0;
    1.25      val ctr_Tss = map (binder_types o fastype_of) ctrs;
     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 17:57:25 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 18:24:11 2013 +0200
     2.3 @@ -1055,11 +1055,9 @@
     2.4        ||>> mk_TFrees nn
     2.5        ||>> variant_tfrees fp_b_names;
     2.6  
     2.7 -    fun add_fake_type spec =
     2.8 -      Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec)
     2.9 -      #>> (fn s => Type (s, unsorted_As));
    2.10 +    fun add_fake_type spec = Typedecl.basic_typedecl (type_binding_of spec, num_As, mixfix_of spec);
    2.11  
    2.12 -    val (fake_Ts, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
    2.13 +    val (fake_T_names, fake_lthy) = fold_map add_fake_type specs no_defs_lthy0;
    2.14  
    2.15      val qsoty = quote o Syntax.string_of_typ fake_lthy;
    2.16  
    2.17 @@ -1100,6 +1098,8 @@
    2.18        | extras => error ("Extra type variables on right-hand side: " ^
    2.19            commas (map (qsoty o TFree) extras)));
    2.20  
    2.21 +    val fake_Ts = map (fn s => Type (s, As)) fake_T_names;
    2.22 +
    2.23      fun eq_fpT_check (T as Type (s, Ts)) (T' as Type (s', Ts')) =
    2.24          s = s' andalso (Ts = Ts' orelse
    2.25            error ("Wrong type arguments in " ^ co_prefix fp ^ "recursive type " ^ qsoty T ^
    2.26 @@ -1279,7 +1279,7 @@
    2.27  
    2.28              val inject_tacss =
    2.29                map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
    2.30 -                  mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
    2.31 +                mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
    2.32  
    2.33              val half_distinct_tacss =
    2.34                map (map (fn (def, def') => fn {context = ctxt, ...} =>