src/HOL/Tools/ATP/atp_translate.ML
changeset 44402 f0bc74b9161e
parent 44399 cd1e32b8d4c4
child 44403 15160cdc4688
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -28,12 +28,12 @@
     1.4      Fin_Nonmono_Types |
     1.5      Const_Arg_Types |
     1.6      No_Types
     1.7 -  datatype type_heaviness = Heavyweight | Lightweight
     1.8 +  datatype type_uniformity = Uniform | Nonuniform
     1.9  
    1.10    datatype type_enc =
    1.11      Simple_Types of order * type_level |
    1.12 -    Guards of polymorphism * type_level * type_heaviness |
    1.13 -    Tags of polymorphism * type_level * type_heaviness
    1.14 +    Guards of polymorphism * type_level * type_uniformity |
    1.15 +    Tags of polymorphism * type_level * type_uniformity
    1.16  
    1.17    val no_lambdasN : string
    1.18    val concealedN : string
    1.19 @@ -529,12 +529,12 @@
    1.20    Fin_Nonmono_Types |
    1.21    Const_Arg_Types |
    1.22    No_Types
    1.23 -datatype type_heaviness = Heavyweight | Lightweight
    1.24 +datatype type_uniformity = Uniform | Nonuniform
    1.25  
    1.26  datatype type_enc =
    1.27    Simple_Types of order * type_level |
    1.28 -  Guards of polymorphism * type_level * type_heaviness |
    1.29 -  Tags of polymorphism * type_level * type_heaviness
    1.30 +  Guards of polymorphism * type_level * type_uniformity |
    1.31 +  Tags of polymorphism * type_level * type_uniformity
    1.32  
    1.33  fun try_unsuffixes ss s =
    1.34    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    1.35 @@ -559,25 +559,25 @@
    1.36                SOME s => (Fin_Nonmono_Types, s)
    1.37              | NONE => (All_Types, s))
    1.38    ||> apsnd (fn s =>
    1.39 -                case try (unsuffix "_heavy") s of
    1.40 -                  SOME s => (Heavyweight, s)
    1.41 -                | NONE => (Lightweight, s))
    1.42 -  |> (fn (poly, (level, (heaviness, core))) =>
    1.43 -         case (core, (poly, level, heaviness)) of
    1.44 -           ("simple", (NONE, _, Lightweight)) =>
    1.45 +                case try (unsuffix "_uniform") s of
    1.46 +                  SOME s => (Uniform, s)
    1.47 +                | NONE => (Nonuniform, s))
    1.48 +  |> (fn (poly, (level, (uniformity, core))) =>
    1.49 +         case (core, (poly, level, uniformity)) of
    1.50 +           ("simple", (NONE, _, Nonuniform)) =>
    1.51             Simple_Types (First_Order, level)
    1.52 -         | ("simple_higher", (NONE, _, Lightweight)) =>
    1.53 +         | ("simple_higher", (NONE, _, Nonuniform)) =>
    1.54             (case level of
    1.55                Noninf_Nonmono_Types _ => raise Same.SAME
    1.56              | _ => Simple_Types (Higher_Order, level))
    1.57 -         | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
    1.58 +         | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
    1.59           | ("tags", (SOME Polymorphic, _, _)) =>
    1.60 -           Tags (Polymorphic, level, heaviness)
    1.61 -         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
    1.62 -         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
    1.63 -           Guards (poly, Const_Arg_Types, Lightweight)
    1.64 -         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
    1.65 -           Guards (Polymorphic, No_Types, Lightweight)
    1.66 +           Tags (Polymorphic, level, uniformity)
    1.67 +         | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
    1.68 +         | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
    1.69 +           Guards (poly, Const_Arg_Types, Nonuniform)
    1.70 +         | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
    1.71 +           Guards (Polymorphic, No_Types, Nonuniform)
    1.72           | _ => raise Same.SAME)
    1.73    handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    1.74  
    1.75 @@ -592,9 +592,9 @@
    1.76    | level_of_type_enc (Guards (_, level, _)) = level
    1.77    | level_of_type_enc (Tags (_, level, _)) = level
    1.78  
    1.79 -fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
    1.80 -  | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
    1.81 -  | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
    1.82 +fun uniformity_of_type_enc (Simple_Types _) = Uniform
    1.83 +  | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
    1.84 +  | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
    1.85  
    1.86  fun is_type_level_quasi_sound All_Types = true
    1.87    | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
    1.88 @@ -617,8 +617,7 @@
    1.89         if member (op =) formats TFF then
    1.90           (TFF, Simple_Types (First_Order, level))
    1.91         else
    1.92 -         choose_format formats
    1.93 -                       (Guards (Mangled_Monomorphic, level, Heavyweight)))
    1.94 +         choose_format formats (Guards (Mangled_Monomorphic, level, Uniform)))
    1.95    | choose_format formats type_enc =
    1.96      (case hd formats of
    1.97         CNF_UEQ =>
    1.98 @@ -682,7 +681,7 @@
    1.99      false (* since TFF doesn't support overloading *)
   1.100    | should_drop_arg_type_args type_enc =
   1.101      level_of_type_enc type_enc = All_Types andalso
   1.102 -    heaviness_of_type_enc type_enc = Heavyweight
   1.103 +    uniformity_of_type_enc type_enc = Uniform
   1.104  
   1.105  fun type_arg_policy type_enc s =
   1.106    if s = type_tag_name then
   1.107 @@ -691,7 +690,7 @@
   1.108       else
   1.109         Explicit_Type_Args) false
   1.110    else case type_enc of
   1.111 -    Tags (_, All_Types, Heavyweight) => No_Type_Args
   1.112 +    Tags (_, All_Types, Uniform) => No_Type_Args
   1.113    | _ =>
   1.114      let val level = level_of_type_enc type_enc in
   1.115        if level = No_Types orelse s = @{const_name HOL.eq} orelse
   1.116 @@ -1113,9 +1112,9 @@
   1.117        is_type_surely_finite ctxt T))
   1.118    | should_encode_type _ _ _ _ = false
   1.119  
   1.120 -fun should_guard_type ctxt mono (Guards (_, level, heaviness)) should_guard_var
   1.121 +fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
   1.122                        T =
   1.123 -    (heaviness = Heavyweight orelse should_guard_var ()) andalso
   1.124 +    (uniformity = Uniform orelse should_guard_var ()) andalso
   1.125      should_encode_type ctxt mono level T
   1.126    | should_guard_type _ _ _ _ _ = false
   1.127  
   1.128 @@ -1130,10 +1129,10 @@
   1.129    Elsewhere
   1.130  
   1.131  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   1.132 -  | should_tag_with_type ctxt mono (Tags (_, level, heaviness)) site u T =
   1.133 -    (case heaviness of
   1.134 -       Heavyweight => should_encode_type ctxt mono level T
   1.135 -     | Lightweight =>
   1.136 +  | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
   1.137 +    (case uniformity of
   1.138 +       Uniform => should_encode_type ctxt mono level T
   1.139 +     | Nonuniform =>
   1.140         case (site, is_var_or_bound_var u) of
   1.141           (Eq_Arg _, true) => should_encode_type ctxt mono level T
   1.142         | _ => false)
   1.143 @@ -2006,10 +2005,10 @@
   1.144        |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
   1.145                                                   type_enc n s)
   1.146      end
   1.147 -  | Tags (_, _, heaviness) =>
   1.148 -    (case heaviness of
   1.149 -       Heavyweight => []
   1.150 -     | Lightweight =>
   1.151 +  | Tags (_, _, uniformity) =>
   1.152 +    (case uniformity of
   1.153 +       Uniform => []
   1.154 +     | Nonuniform =>
   1.155         let val n = length decls in
   1.156           (0 upto n - 1 ~~ decls)
   1.157           |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
   1.158 @@ -2036,9 +2035,9 @@
   1.159                 syms []
   1.160    in mono_lines @ decl_lines end
   1.161  
   1.162 -fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
   1.163 +fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
   1.164      poly <> Mangled_Monomorphic andalso
   1.165 -    ((level = All_Types andalso heaviness = Lightweight) orelse
   1.166 +    ((level = All_Types andalso uniformity = Nonuniform) orelse
   1.167       is_type_level_monotonicity_based level)
   1.168    | needs_type_tag_idempotence _ = false
   1.169