# HG changeset patch # User blanchet # Date 1315396216 -7200 # Node ID ba4c0205267f96280f95f7fd06905298417fca69 # Parent 18b1ba7cfcfeb6a301ac4c476013e80cb85d6c42 tuning diff -r 18b1ba7cfcfe -r ba4c0205267f src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 11:36:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 13:50:16 2011 +0200 @@ -19,21 +19,16 @@ General | Helper | Induction | Extensionality | Intro | Elim | Simp | Local | Assum | Chained - datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype soundness = Sound_Modulo_Infiniteness | Sound - datatype uniformity = Uniform | Nonuniform + datatype heaviness = Heavy | Ann_Light | Arg_Light datatype type_level = All_Types | - Noninf_Nonmono_Types of soundness * uniformity | - Fin_Nonmono_Types of uniformity | + Noninf_Nonmono_Types of soundness * heaviness | + Fin_Nonmono_Types of heaviness | Const_Arg_Types | No_Types - - datatype type_enc = - Simple_Types of order * polymorphism * type_level | - Guards of polymorphism * type_level | - Tags of polymorphism * type_level + type type_enc val type_tag_idempotence : bool Config.T val type_tag_arguments : bool Config.T @@ -537,11 +532,11 @@ datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype soundness = Sound_Modulo_Infiniteness | Sound -datatype uniformity = Uniform | Nonuniform +datatype heaviness = Heavy | Ann_Light | Arg_Light datatype type_level = All_Types | - Noninf_Nonmono_Types of soundness * uniformity | - Fin_Nonmono_Types of uniformity | + Noninf_Nonmono_Types of soundness * heaviness | + Fin_Nonmono_Types of heaviness | Const_Arg_Types | No_Types @@ -561,9 +556,9 @@ | level_of_type_enc (Guards (_, level)) = level | level_of_type_enc (Tags (_, level)) = level -fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false - | is_level_uniform (Fin_Nonmono_Types Nonuniform) = false - | is_level_uniform _ = true +fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness + | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness + | heaviness_of_level _ = Heavy fun is_type_level_quasi_sound All_Types = true | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true @@ -600,14 +595,14 @@ case try_unsuffixes queries s of SOME s => (case try_unsuffixes queries s of - SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s) - | NONE => (Noninf_Nonmono_Types (soundness, Uniform), s)) + SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s) + | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s)) | NONE => case try_unsuffixes bangs s of SOME s => (case try_unsuffixes bangs s of - SOME s => (Fin_Nonmono_Types Nonuniform, s) - | NONE => (Fin_Nonmono_Types Uniform, s)) + SOME s => (Fin_Nonmono_Types Ann_Light, s) + | NONE => (Fin_Nonmono_Types Heavy, s)) | NONE => (All_Types, s)) |> (fn (poly, (level, core)) => case (core, (poly, level)) of @@ -616,7 +611,7 @@ (Polymorphic, All_Types) => Simple_Types (First_Order, Polymorphic, All_Types) | (Mangled_Monomorphic, _) => - if is_level_uniform level then + if heaviness_of_level level = Heavy then Simple_Types (First_Order, Mangled_Monomorphic, level) else raise Same.SAME @@ -627,7 +622,7 @@ Simple_Types (Higher_Order, Polymorphic, All_Types) | (_, Noninf_Nonmono_Types _) => raise Same.SAME | (Mangled_Monomorphic, _) => - if is_level_uniform level then + if heaviness_of_level level = Heavy then Simple_Types (Higher_Order, Mangled_Monomorphic, level) else raise Same.SAME @@ -1241,7 +1236,7 @@ | should_encode_type _ _ _ _ = false fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T = - (is_level_uniform level orelse should_guard_var ()) andalso + (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso should_encode_type ctxt mono level T | should_guard_type _ _ _ _ _ = false @@ -1258,7 +1253,7 @@ fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false | should_tag_with_type ctxt mono (Tags (_, level)) site u T = - (if is_level_uniform level then + (if heaviness_of_level level = Heavy then should_encode_type ctxt mono level T else case (site, is_maybe_universal_var u) of (Eq_Arg _, true) => should_encode_type ctxt mono level T @@ -1657,7 +1652,8 @@ fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T = - not (is_level_uniform level) andalso should_encode_type ctxt mono level T + heaviness_of_level level <> Heavy andalso + should_encode_type ctxt mono level T | should_generate_tag_bound_decl _ _ _ _ _ = false fun mk_aterm format type_enc name T_args args = @@ -2131,7 +2127,7 @@ type_enc n s) end | Tags (_, level) => - if is_level_uniform level then + if heaviness_of_level level = Heavy then [] else let val n = length decls in diff -r 18b1ba7cfcfe -r ba4c0205267f src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 11:36:39 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 13:50:16 2011 +0200 @@ -59,8 +59,9 @@ ((prefixed_predicator_name, 1), (K metis_predicator, false)), ((prefixed_app_op_name, 2), (K metis_app_op, false)), ((prefixed_type_tag_name, 2), - (fn Tags (_, All_Types) => metis_systematic_type_tag - | _ => metis_ad_hoc_type_tag, true))] + (fn type_enc => + if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag + else metis_ad_hoc_type_tag, true))] fun old_skolem_const_name i j num_T_args = old_skolem_const_prefix ^ Long_Name.separator ^