make mangling sound w.r.t. type arguments
authorblanchet
Wed Sep 07 09:10:41 2011 +0200 (2011-09-07)
changeset 447710e5d4388bbac
parent 44770 3b1b4d805441
child 44772 60ac7b56296a
make mangling sound w.r.t. type arguments
src/HOL/Tools/ATP/atp_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 09:10:41 2011 +0200
     1.3 @@ -702,7 +702,7 @@
     1.4  (* The Booleans indicate whether all type arguments should be kept. *)
     1.5  datatype type_arg_policy =
     1.6    Explicit_Type_Args of bool |
     1.7 -  Mangled_Type_Args of bool |
     1.8 +  Mangled_Type_Args |
     1.9    No_Type_Args
    1.10  
    1.11  fun should_drop_arg_type_args (Simple_Types _) = false
    1.12 @@ -711,10 +711,10 @@
    1.13  
    1.14  fun type_arg_policy type_enc s =
    1.15    if s = type_tag_name then
    1.16 -    (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.17 -       Mangled_Type_Args
    1.18 -     else
    1.19 -       Explicit_Type_Args) false
    1.20 +    if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.21 +      Mangled_Type_Args
    1.22 +    else
    1.23 +      Explicit_Type_Args false
    1.24    else case type_enc of
    1.25      Tags (_, All_Types) => No_Type_Args
    1.26    | _ =>
    1.27 @@ -722,12 +722,10 @@
    1.28        if level = No_Types orelse s = @{const_name HOL.eq} orelse
    1.29           (s = app_op_name andalso level = Const_Arg_Types) then
    1.30          No_Type_Args
    1.31 +      else if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.32 +        Mangled_Type_Args
    1.33        else
    1.34 -        should_drop_arg_type_args type_enc
    1.35 -        |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    1.36 -              Mangled_Type_Args
    1.37 -            else
    1.38 -              Explicit_Type_Args)
    1.39 +        Explicit_Type_Args (should_drop_arg_type_args type_enc)
    1.40      end
    1.41  
    1.42  (* Make atoms for sorted type variables. *)
    1.43 @@ -1411,9 +1409,8 @@
    1.44             in
    1.45               case type_arg_policy type_enc s'' of
    1.46                 Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
    1.47 -             | Mangled_Type_Args drop_args =>
    1.48 -               (mangled_const_name format type_enc (filter_T_args drop_args)
    1.49 -                                   name, [])
    1.50 +             | Mangled_Type_Args =>
    1.51 +               (mangled_const_name format type_enc T_args name, [])
    1.52               | No_Type_Args => (name, [])
    1.53             end)
    1.54          |> (fn (name, T_args) => IConst (name, T, T_args))
    1.55 @@ -1846,7 +1843,7 @@
    1.56          val (s, s') =
    1.57            `(make_fixed_const NONE) @{const_name undefined}
    1.58            |> (case type_arg_policy type_enc @{const_name undefined} of
    1.59 -                Mangled_Type_Args _ => mangled_const_name format type_enc [T]
    1.60 +                Mangled_Type_Args => mangled_const_name format type_enc [T]
    1.61                | _ => I)
    1.62        in
    1.63          Symtab.map_default (s, [])