determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
authorbulwahn
Mon Sep 19 16:18:19 2011 +0200 (2011-09-19)
changeset 44998f12ef61ea76e
parent 44997 e534939f880d
child 44999 04b794da039e
determining the fastype of a case-pattern but ignoring dummy type constructors that were added as markers for type annotations
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
     1.3 @@ -581,6 +581,11 @@
     1.4  
     1.5  (* inference of type annotations for disambiguation with type classes *)
     1.6  
     1.7 +fun dest_tagged_type (Type ("", [T])) = (true, T)
     1.8 +  | dest_tagged_type T = (false, T)
     1.9 +
    1.10 +val untag_term = map_types (snd o dest_tagged_type)
    1.11 +
    1.12  fun annotate_term (proj_sort, _) eqngr =
    1.13    let
    1.14      val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
    1.15 @@ -786,7 +791,7 @@
    1.16      val tys = arg_types num_args (snd c_ty);
    1.17      val ty = nth tys t_pos;
    1.18      fun mk_constr c t = let val n = Code.args_number thy c
    1.19 -      in ((c, arg_types n (fastype_of t) ---> ty), n) end;
    1.20 +      in ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
    1.21      val constrs = if null case_pats then []
    1.22        else map2 mk_constr case_pats (nth_drop t_pos ts);
    1.23      fun casify naming constrs ty ts =