tuning
authorblanchet
Wed Sep 07 13:50:16 2011 +0200 (2011-09-07)
changeset 44782ba4c0205267f
parent 44778 18b1ba7cfcfe
child 44783 3634c6dba23f
tuning
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Metis/metis_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 11:36:39 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:16 2011 +0200
     1.3 @@ -19,21 +19,16 @@
     1.4      General | Helper | Induction | Extensionality | Intro | Elim | Simp |
     1.5      Local | Assum | Chained
     1.6  
     1.7 -  datatype order = First_Order | Higher_Order
     1.8    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     1.9    datatype soundness = Sound_Modulo_Infiniteness | Sound
    1.10 -  datatype uniformity = Uniform | Nonuniform
    1.11 +  datatype heaviness = Heavy | Ann_Light | Arg_Light
    1.12    datatype type_level =
    1.13      All_Types |
    1.14 -    Noninf_Nonmono_Types of soundness * uniformity |
    1.15 -    Fin_Nonmono_Types of uniformity |
    1.16 +    Noninf_Nonmono_Types of soundness * heaviness |
    1.17 +    Fin_Nonmono_Types of heaviness |
    1.18      Const_Arg_Types |
    1.19      No_Types
    1.20 -
    1.21 -  datatype type_enc =
    1.22 -    Simple_Types of order * polymorphism * type_level |
    1.23 -    Guards of polymorphism * type_level |
    1.24 -    Tags of polymorphism * type_level
    1.25 +  type type_enc
    1.26  
    1.27    val type_tag_idempotence : bool Config.T
    1.28    val type_tag_arguments : bool Config.T
    1.29 @@ -537,11 +532,11 @@
    1.30  datatype order = First_Order | Higher_Order
    1.31  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    1.32  datatype soundness = Sound_Modulo_Infiniteness | Sound
    1.33 -datatype uniformity = Uniform | Nonuniform
    1.34 +datatype heaviness = Heavy | Ann_Light | Arg_Light
    1.35  datatype type_level =
    1.36    All_Types |
    1.37 -  Noninf_Nonmono_Types of soundness * uniformity |
    1.38 -  Fin_Nonmono_Types of uniformity |
    1.39 +  Noninf_Nonmono_Types of soundness * heaviness |
    1.40 +  Fin_Nonmono_Types of heaviness |
    1.41    Const_Arg_Types |
    1.42    No_Types
    1.43  
    1.44 @@ -561,9 +556,9 @@
    1.45    | level_of_type_enc (Guards (_, level)) = level
    1.46    | level_of_type_enc (Tags (_, level)) = level
    1.47  
    1.48 -fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false
    1.49 -  | is_level_uniform (Fin_Nonmono_Types Nonuniform) = false
    1.50 -  | is_level_uniform _ = true
    1.51 +fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
    1.52 +  | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
    1.53 +  | heaviness_of_level _ = Heavy
    1.54  
    1.55  fun is_type_level_quasi_sound All_Types = true
    1.56    | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
    1.57 @@ -600,14 +595,14 @@
    1.58            case try_unsuffixes queries s of
    1.59              SOME s =>
    1.60              (case try_unsuffixes queries s of
    1.61 -               SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s)
    1.62 -             | NONE => (Noninf_Nonmono_Types (soundness, Uniform), s))
    1.63 +               SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s)
    1.64 +             | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s))
    1.65            | NONE =>
    1.66              case try_unsuffixes bangs s of
    1.67                SOME s =>
    1.68                (case try_unsuffixes bangs s of
    1.69 -                 SOME s => (Fin_Nonmono_Types Nonuniform, s)
    1.70 -               | NONE => (Fin_Nonmono_Types Uniform, s))
    1.71 +                 SOME s => (Fin_Nonmono_Types Ann_Light, s)
    1.72 +               | NONE => (Fin_Nonmono_Types Heavy, s))
    1.73              | NONE => (All_Types, s))
    1.74    |> (fn (poly, (level, core)) =>
    1.75           case (core, (poly, level)) of
    1.76 @@ -616,7 +611,7 @@
    1.77                (Polymorphic, All_Types) =>
    1.78                Simple_Types (First_Order, Polymorphic, All_Types)
    1.79              | (Mangled_Monomorphic, _) =>
    1.80 -              if is_level_uniform level then
    1.81 +              if heaviness_of_level level = Heavy then
    1.82                  Simple_Types (First_Order, Mangled_Monomorphic, level)
    1.83                else
    1.84                  raise Same.SAME
    1.85 @@ -627,7 +622,7 @@
    1.86                Simple_Types (Higher_Order, Polymorphic, All_Types)
    1.87              | (_, Noninf_Nonmono_Types _) => raise Same.SAME
    1.88              | (Mangled_Monomorphic, _) =>
    1.89 -              if is_level_uniform level then
    1.90 +              if heaviness_of_level level = Heavy then
    1.91                  Simple_Types (Higher_Order, Mangled_Monomorphic, level)
    1.92                else
    1.93                  raise Same.SAME
    1.94 @@ -1241,7 +1236,7 @@
    1.95    | should_encode_type _ _ _ _ = false
    1.96  
    1.97  fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
    1.98 -    (is_level_uniform level orelse should_guard_var ()) andalso
    1.99 +    (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso
   1.100      should_encode_type ctxt mono level T
   1.101    | should_guard_type _ _ _ _ _ = false
   1.102  
   1.103 @@ -1258,7 +1253,7 @@
   1.104  
   1.105  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   1.106    | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
   1.107 -    (if is_level_uniform level then
   1.108 +    (if heaviness_of_level level = Heavy then
   1.109         should_encode_type ctxt mono level T
   1.110       else case (site, is_maybe_universal_var u) of
   1.111         (Eq_Arg _, true) => should_encode_type ctxt mono level T
   1.112 @@ -1657,7 +1652,8 @@
   1.113  
   1.114  fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
   1.115    | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
   1.116 -    not (is_level_uniform level) andalso should_encode_type ctxt mono level T
   1.117 +    heaviness_of_level level <> Heavy andalso
   1.118 +    should_encode_type ctxt mono level T
   1.119    | should_generate_tag_bound_decl _ _ _ _ _ = false
   1.120  
   1.121  fun mk_aterm format type_enc name T_args args =
   1.122 @@ -2131,7 +2127,7 @@
   1.123                                                   type_enc n s)
   1.124      end
   1.125    | Tags (_, level) =>
   1.126 -    if is_level_uniform level then
   1.127 +    if heaviness_of_level level = Heavy then
   1.128        []
   1.129      else
   1.130        let val n = length decls in
     2.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Sep 07 11:36:39 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Sep 07 13:50:16 2011 +0200
     2.3 @@ -59,8 +59,9 @@
     2.4     ((prefixed_predicator_name, 1), (K metis_predicator, false)),
     2.5     ((prefixed_app_op_name, 2), (K metis_app_op, false)),
     2.6     ((prefixed_type_tag_name, 2),
     2.7 -    (fn Tags (_, All_Types) => metis_systematic_type_tag
     2.8 -      | _ => metis_ad_hoc_type_tag, true))]
     2.9 +    (fn type_enc =>
    2.10 +        if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag
    2.11 +        else metis_ad_hoc_type_tag, true))]
    2.12  
    2.13  fun old_skolem_const_name i j num_T_args =
    2.14    old_skolem_const_prefix ^ Long_Name.separator ^