clearer terminology
authorblanchet
Mon Aug 22 15:02:45 2011 +0200 (2011-08-22)
changeset 44402f0bc74b9161e
parent 44401 c47f118fe008
child 44403 15160cdc4688
clearer terminology
src/HOL/Metis_Examples/Type_Encodings.thy
src/HOL/TPTP/ATP_Export.thy
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -27,46 +27,46 @@
     1.4  val type_encs =
     1.5    ["erased",
     1.6     "poly_guards",
     1.7 -   "poly_guards_heavy",
     1.8 +   "poly_guards_uniform",
     1.9     "poly_tags",
    1.10 -   "poly_tags_heavy",
    1.11 +   "poly_tags_uniform",
    1.12     "poly_args",
    1.13     "mono_guards",
    1.14 -   "mono_guards_heavy",
    1.15 +   "mono_guards_uniform",
    1.16     "mono_tags",
    1.17 -   "mono_tags_heavy",
    1.18 +   "mono_tags_uniform",
    1.19     "mono_args",
    1.20     "mangled_guards",
    1.21 -   "mangled_guards_heavy",
    1.22 +   "mangled_guards_uniform",
    1.23     "mangled_tags",
    1.24 -   "mangled_tags_heavy",
    1.25 +   "mangled_tags_uniform",
    1.26     "mangled_args",
    1.27     "simple",
    1.28     "poly_guards?",
    1.29 -   "poly_guards_heavy?",
    1.30 +   "poly_guards_uniform?",
    1.31     "poly_tags?",
    1.32 -(* "poly_tags_heavy?", *)
    1.33 +(* "poly_tags_uniform?", *)
    1.34     "mono_guards?",
    1.35 -   "mono_guards_heavy?",
    1.36 +   "mono_guards_uniform?",
    1.37     "mono_tags?",
    1.38 -   "mono_tags_heavy?",
    1.39 +   "mono_tags_uniform?",
    1.40     "mangled_guards?",
    1.41 -   "mangled_guards_heavy?",
    1.42 +   "mangled_guards_uniform?",
    1.43     "mangled_tags?",
    1.44 -   "mangled_tags_heavy?",
    1.45 +   "mangled_tags_uniform?",
    1.46     "simple?",
    1.47     "poly_guards!",
    1.48 -   "poly_guards_heavy!",
    1.49 +   "poly_guards_uniform!",
    1.50  (* "poly_tags!", *)
    1.51 -   "poly_tags_heavy!",
    1.52 +   "poly_tags_uniform!",
    1.53     "mono_guards!",
    1.54 -   "mono_guards_heavy!",
    1.55 +   "mono_guards_uniform!",
    1.56     "mono_tags!",
    1.57 -   "mono_tags_heavy!",
    1.58 +   "mono_tags_uniform!",
    1.59     "mangled_guards!",
    1.60 -   "mangled_guards_heavy!",
    1.61 +   "mangled_guards_uniform!",
    1.62     "mangled_tags!",
    1.63 -   "mangled_tags_heavy!",
    1.64 +   "mangled_tags_uniform!",
    1.65     "simple!"]
    1.66  
    1.67  fun metis_exhaust_tac ctxt ths =
     2.1 --- a/src/HOL/TPTP/ATP_Export.thy	Mon Aug 22 15:02:45 2011 +0200
     2.2 +++ b/src/HOL/TPTP/ATP_Export.thy	Mon Aug 22 15:02:45 2011 +0200
     2.3 @@ -27,8 +27,8 @@
     2.4  
     2.5  ML {*
     2.6  if do_it then
     2.7 -  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy"
     2.8 -      "/tmp/infs_poly_tags_heavy.tptp"
     2.9 +  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_uniform"
    2.10 +      "/tmp/infs_poly_tags_uniform.tptp"
    2.11  else
    2.12    ()
    2.13  *}
     3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Aug 22 15:02:45 2011 +0200
     3.3 @@ -30,8 +30,10 @@
     3.4    datatype formula_kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
     3.5    datatype 'a problem_line =
     3.6      Decl of string * 'a * 'a ho_type |
     3.7 -    Formula of string * formula_kind * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
     3.8 -               * (string, string ho_type) ho_term option * (string, string ho_type) ho_term option
     3.9 +    Formula of string * formula_kind
    3.10 +               * ('a, 'a ho_type, ('a, 'a ho_type) ho_term) formula
    3.11 +               * (string, string ho_type) ho_term option
    3.12 +               * (string, string ho_type) ho_term option
    3.13    type 'a problem = (string * 'a problem_line list) list
    3.14  
    3.15    val tptp_cnf : string
     4.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     4.3 @@ -28,12 +28,12 @@
     4.4      Fin_Nonmono_Types |
     4.5      Const_Arg_Types |
     4.6      No_Types
     4.7 -  datatype type_heaviness = Heavyweight | Lightweight
     4.8 +  datatype type_uniformity = Uniform | Nonuniform
     4.9  
    4.10    datatype type_enc =
    4.11      Simple_Types of order * type_level |
    4.12 -    Guards of polymorphism * type_level * type_heaviness |
    4.13 -    Tags of polymorphism * type_level * type_heaviness
    4.14 +    Guards of polymorphism * type_level * type_uniformity |
    4.15 +    Tags of polymorphism * type_level * type_uniformity
    4.16  
    4.17    val no_lambdasN : string
    4.18    val concealedN : string
    4.19 @@ -529,12 +529,12 @@
    4.20    Fin_Nonmono_Types |
    4.21    Const_Arg_Types |
    4.22    No_Types
    4.23 -datatype type_heaviness = Heavyweight | Lightweight
    4.24 +datatype type_uniformity = Uniform | Nonuniform
    4.25  
    4.26  datatype type_enc =
    4.27    Simple_Types of order * type_level |
    4.28 -  Guards of polymorphism * type_level * type_heaviness |
    4.29 -  Tags of polymorphism * type_level * type_heaviness
    4.30 +  Guards of polymorphism * type_level * type_uniformity |
    4.31 +  Tags of polymorphism * type_level * type_uniformity
    4.32  
    4.33  fun try_unsuffixes ss s =
    4.34    fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
    4.35 @@ -559,25 +559,25 @@
    4.36                SOME s => (Fin_Nonmono_Types, s)
    4.37              | NONE => (All_Types, s))
    4.38    ||> apsnd (fn s =>
    4.39 -                case try (unsuffix "_heavy") s of
    4.40 -                  SOME s => (Heavyweight, s)
    4.41 -                | NONE => (Lightweight, s))
    4.42 -  |> (fn (poly, (level, (heaviness, core))) =>
    4.43 -         case (core, (poly, level, heaviness)) of
    4.44 -           ("simple", (NONE, _, Lightweight)) =>
    4.45 +                case try (unsuffix "_uniform") s of
    4.46 +                  SOME s => (Uniform, s)
    4.47 +                | NONE => (Nonuniform, s))
    4.48 +  |> (fn (poly, (level, (uniformity, core))) =>
    4.49 +         case (core, (poly, level, uniformity)) of
    4.50 +           ("simple", (NONE, _, Nonuniform)) =>
    4.51             Simple_Types (First_Order, level)
    4.52 -         | ("simple_higher", (NONE, _, Lightweight)) =>
    4.53 +         | ("simple_higher", (NONE, _, Nonuniform)) =>
    4.54             (case level of
    4.55                Noninf_Nonmono_Types _ => raise Same.SAME
    4.56              | _ => Simple_Types (Higher_Order, level))
    4.57 -         | ("guards", (SOME poly, _, _)) => Guards (poly, level, heaviness)
    4.58 +         | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
    4.59           | ("tags", (SOME Polymorphic, _, _)) =>
    4.60 -           Tags (Polymorphic, level, heaviness)
    4.61 -         | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness)
    4.62 -         | ("args", (SOME poly, All_Types (* naja *), Lightweight)) =>
    4.63 -           Guards (poly, Const_Arg_Types, Lightweight)
    4.64 -         | ("erased", (NONE, All_Types (* naja *), Lightweight)) =>
    4.65 -           Guards (Polymorphic, No_Types, Lightweight)
    4.66 +           Tags (Polymorphic, level, uniformity)
    4.67 +         | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
    4.68 +         | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
    4.69 +           Guards (poly, Const_Arg_Types, Nonuniform)
    4.70 +         | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
    4.71 +           Guards (Polymorphic, No_Types, Nonuniform)
    4.72           | _ => raise Same.SAME)
    4.73    handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    4.74  
    4.75 @@ -592,9 +592,9 @@
    4.76    | level_of_type_enc (Guards (_, level, _)) = level
    4.77    | level_of_type_enc (Tags (_, level, _)) = level
    4.78  
    4.79 -fun heaviness_of_type_enc (Simple_Types _) = Heavyweight
    4.80 -  | heaviness_of_type_enc (Guards (_, _, heaviness)) = heaviness
    4.81 -  | heaviness_of_type_enc (Tags (_, _, heaviness)) = heaviness
    4.82 +fun uniformity_of_type_enc (Simple_Types _) = Uniform
    4.83 +  | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
    4.84 +  | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
    4.85  
    4.86  fun is_type_level_quasi_sound All_Types = true
    4.87    | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
    4.88 @@ -617,8 +617,7 @@
    4.89         if member (op =) formats TFF then
    4.90           (TFF, Simple_Types (First_Order, level))
    4.91         else
    4.92 -         choose_format formats
    4.93 -                       (Guards (Mangled_Monomorphic, level, Heavyweight)))
    4.94 +         choose_format formats (Guards (Mangled_Monomorphic, level, Uniform)))
    4.95    | choose_format formats type_enc =
    4.96      (case hd formats of
    4.97         CNF_UEQ =>
    4.98 @@ -682,7 +681,7 @@
    4.99      false (* since TFF doesn't support overloading *)
   4.100    | should_drop_arg_type_args type_enc =
   4.101      level_of_type_enc type_enc = All_Types andalso
   4.102 -    heaviness_of_type_enc type_enc = Heavyweight
   4.103 +    uniformity_of_type_enc type_enc = Uniform
   4.104  
   4.105  fun type_arg_policy type_enc s =
   4.106    if s = type_tag_name then
   4.107 @@ -691,7 +690,7 @@
   4.108       else
   4.109         Explicit_Type_Args) false
   4.110    else case type_enc of
   4.111 -    Tags (_, All_Types, Heavyweight) => No_Type_Args
   4.112 +    Tags (_, All_Types, Uniform) => No_Type_Args
   4.113    | _ =>
   4.114      let val level = level_of_type_enc type_enc in
   4.115        if level = No_Types orelse s = @{const_name HOL.eq} orelse
   4.116 @@ -1113,9 +1112,9 @@
   4.117        is_type_surely_finite ctxt T))
   4.118    | should_encode_type _ _ _ _ = false
   4.119  
   4.120 -fun should_guard_type ctxt mono (Guards (_, level, heaviness)) should_guard_var
   4.121 +fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
   4.122                        T =
   4.123 -    (heaviness = Heavyweight orelse should_guard_var ()) andalso
   4.124 +    (uniformity = Uniform orelse should_guard_var ()) andalso
   4.125      should_encode_type ctxt mono level T
   4.126    | should_guard_type _ _ _ _ _ = false
   4.127  
   4.128 @@ -1130,10 +1129,10 @@
   4.129    Elsewhere
   4.130  
   4.131  fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
   4.132 -  | should_tag_with_type ctxt mono (Tags (_, level, heaviness)) site u T =
   4.133 -    (case heaviness of
   4.134 -       Heavyweight => should_encode_type ctxt mono level T
   4.135 -     | Lightweight =>
   4.136 +  | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
   4.137 +    (case uniformity of
   4.138 +       Uniform => should_encode_type ctxt mono level T
   4.139 +     | Nonuniform =>
   4.140         case (site, is_var_or_bound_var u) of
   4.141           (Eq_Arg _, true) => should_encode_type ctxt mono level T
   4.142         | _ => false)
   4.143 @@ -2006,10 +2005,10 @@
   4.144        |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
   4.145                                                   type_enc n s)
   4.146      end
   4.147 -  | Tags (_, _, heaviness) =>
   4.148 -    (case heaviness of
   4.149 -       Heavyweight => []
   4.150 -     | Lightweight =>
   4.151 +  | Tags (_, _, uniformity) =>
   4.152 +    (case uniformity of
   4.153 +       Uniform => []
   4.154 +     | Nonuniform =>
   4.155         let val n = length decls in
   4.156           (0 upto n - 1 ~~ decls)
   4.157           |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
   4.158 @@ -2036,9 +2035,9 @@
   4.159                 syms []
   4.160    in mono_lines @ decl_lines end
   4.161  
   4.162 -fun needs_type_tag_idempotence (Tags (poly, level, heaviness)) =
   4.163 +fun needs_type_tag_idempotence (Tags (poly, level, uniformity)) =
   4.164      poly <> Mangled_Monomorphic andalso
   4.165 -    ((level = All_Types andalso heaviness = Lightweight) orelse
   4.166 +    ((level = All_Types andalso uniformity = Nonuniform) orelse
   4.167       is_type_level_monotonicity_based level)
   4.168    | needs_type_tag_idempotence _ = false
   4.169  
     5.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
     5.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
     5.3 @@ -39,8 +39,8 @@
     5.4  val partial_typesN = "partial_types"
     5.5  val no_typesN = "no_types"
     5.6  
     5.7 -val really_full_type_enc = "mangled_tags_heavy"
     5.8 -val full_type_enc = "poly_guards_heavy_query"
     5.9 +val really_full_type_enc = "mangled_tags_uniform"
    5.10 +val full_type_enc = "poly_guards_uniform_query"
    5.11  val partial_type_enc = "poly_args"
    5.12  val no_type_enc = "erased"
    5.13