# HG changeset patch # User blanchet # Date 1341400124 -7200 # Node ID 6c0ac78154669c681c3d4bab58448e606e072a1f # Parent 221a17a97faba2be67e2c92a38554d4deb79a4f1 tuning diff -r 221a17a97fab -r 6c0ac7815466 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jul 03 22:09:23 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 04 13:08:44 2012 +0200 @@ -18,16 +18,17 @@ datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter datatype scope = Global | Local | Assum | Chained - datatype status = - General | Induction | Intro | Inductive | Elim | Simp | Def + datatype status = General | Induction | Intro | Inductive | Elim | Simp | Def type stature = scope * status datatype strictness = Strict | Non_Strict - datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars + datatype uniformity = Uniform | Non_Uniform + datatype constr_optim = With_Constr_Optim | Without_Constr_Optim datatype type_level = All_Types | - Nonmono_Types of strictness * granularity | - Const_Types of bool | + Nonmono_Types of strictness * uniformity | + Undercover_Types | + Const_Types of constr_optim | No_Types type type_enc @@ -132,11 +133,13 @@ Raw_Monomorphic | Mangled_Monomorphic datatype strictness = Strict | Non_Strict -datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars +datatype uniformity = Uniform | Non_Uniform +datatype constr_optim = With_Constr_Optim | Without_Constr_Optim datatype type_level = All_Types | - Nonmono_Types of strictness * granularity | - Const_Types of bool | + Nonmono_Types of strictness * uniformity | + Undercover_Types | + Const_Types of constr_optim | No_Types datatype type_enc = @@ -163,12 +166,13 @@ | level_of_type_enc (Guards (_, level)) = level | level_of_type_enc (Tags (_, level)) = level -fun granularity_of_type_level (Nonmono_Types (_, grain)) = grain - | granularity_of_type_level _ = All_Vars +fun is_type_level_uniform (Nonmono_Types (_, Non_Uniform)) = false + | is_type_level_uniform Undercover_Types = false + | is_type_level_uniform _ = true -fun is_type_level_sound All_Types = true - | is_type_level_sound (Nonmono_Types _) = true - | is_type_level_sound _ = false +fun is_type_level_sound (Const_Types _) = false + | is_type_level_sound No_Types = false + | is_type_level_sound _ = true val is_type_enc_sound = is_type_level_sound o level_of_type_enc fun is_type_level_monotonicity_based (Nonmono_Types _) = true @@ -608,18 +612,18 @@ case try_unsuffixes queries s of SOME s => (case try_unsuffixes queries s of - SOME s => (Nonmono_Types (strictness, Positively_Naked_Vars), s) - | NONE => (Nonmono_Types (strictness, All_Vars), s)) + SOME s => (Nonmono_Types (strictness, Non_Uniform), s) + | NONE => (Nonmono_Types (strictness, Uniform), s)) | NONE => (case try_unsuffixes ats s of - SOME s => (Nonmono_Types (strictness, Undercover_Vars), s) + SOME s => (Undercover_Types, s) | NONE => (All_Types, s))) |> (fn (poly, (level, core)) => case (core, (poly, level)) of ("native", (SOME poly, _)) => (case (poly, level) of (Mangled_Monomorphic, _) => - if granularity_of_type_level level = All_Vars then + if is_type_level_uniform level then Native (First_Order, Mangled_Monomorphic, level) else raise Same.SAME @@ -628,8 +632,9 @@ | ("native_higher", (SOME poly, _)) => (case (poly, level) of (_, Nonmono_Types _) => raise Same.SAME + | (_, Undercover_Types) => raise Same.SAME | (Mangled_Monomorphic, _) => - if granularity_of_type_level level = All_Vars then + if is_type_level_uniform level then Native (Higher_Order THF_With_Choice, Mangled_Monomorphic, level) else @@ -639,27 +644,27 @@ | _ => raise Same.SAME) | ("guards", (SOME poly, _)) => if (poly = Mangled_Monomorphic andalso - granularity_of_type_level level = Undercover_Vars) orelse + level = Undercover_Types) orelse poly = Type_Class_Polymorphic then raise Same.SAME else Guards (poly, level) | ("tags", (SOME poly, _)) => if (poly = Mangled_Monomorphic andalso - granularity_of_type_level level = Undercover_Vars) orelse + level = Undercover_Types) orelse poly = Type_Class_Polymorphic then raise Same.SAME else Tags (poly, level) | ("args", (SOME poly, All_Types (* naja *))) => if poly = Type_Class_Polymorphic then raise Same.SAME - else Guards (poly, Const_Types false) - | ("args", (SOME poly, Nonmono_Types (_, All_Vars) (* naja *))) => + else Guards (poly, Const_Types Without_Constr_Optim) + | ("args", (SOME poly, Nonmono_Types (_, Uniform) (* naja *))) => if poly = Mangled_Monomorphic orelse poly = Type_Class_Polymorphic then raise Same.SAME else - Guards (poly, Const_Types true) + Guards (poly, Const_Types With_Constr_Optim) | ("erased", (NONE, All_Types (* naja *))) => Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) | _ => raise Same.SAME) @@ -853,11 +858,12 @@ Mangled_Type_Args else if level = All_Types then Not_Input_Type_Args - else if granularity_of_type_level level = Undercover_Vars then + else if level = Undercover_Types then case type_enc of Tags _ => Only_In_Or_Output_Type_Args | _ => Not_Input_Type_Args - else if member (op =) constrs s andalso level <> Const_Types false then + else if member (op =) constrs s andalso + level <> Const_Types Without_Constr_Optim then Constr_Input_Type_Args else All_Type_Args @@ -1388,15 +1394,15 @@ fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts, ...} - (Nonmono_Types (strictness, grain)) T = + (Nonmono_Types (strictness, _)) T = let val thy = Proof_Context.theory_of ctxt in - grain = Undercover_Vars orelse (exists (type_intersect thy T) maybe_nonmono_Ts andalso not (exists (type_instance thy T) surely_infinite_Ts orelse (not (member (type_equiv thy) maybe_finite_Ts T) andalso is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts T))) end + | should_encode_type _ _ Undercover_Types _ = true | should_encode_type _ _ _ _ = false fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T = @@ -1418,15 +1424,17 @@ fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false | should_tag_with_type ctxt mono (Tags (_, level)) site u T = let val thy = Proof_Context.theory_of ctxt in - case granularity_of_type_level level of - All_Vars => should_encode_type ctxt mono level T - | grain => + case level of + Nonmono_Types (_, Non_Uniform) => (case (site, is_maybe_universal_var u) of (Eq_Arg _, true) => should_encode_type ctxt mono level T - | (Arg (s, j, ary), true) => - grain = Undercover_Vars andalso - member (op =) (type_arg_cover thy s ary) j | _ => false) + | Undercover_Types => + (case (site, is_maybe_universal_var u) of + (Eq_Arg _, true) => true + | (Arg (s, j, ary), true) => member (op =) (type_arg_cover thy s ary) j + | _ => false) + | _ => should_encode_type ctxt mono level T end | should_tag_with_type _ _ _ _ _ _ = false @@ -1999,20 +2007,22 @@ in is_undercover tm end fun should_guard_var_in_formula thy level pos phi (SOME true) name = - (case granularity_of_type_level level of - All_Vars => true - | Positively_Naked_Vars => + (case level of + All_Types => true + | Nonmono_Types (_, Uniform) => true + | Nonmono_Types (_, Non_Uniform) => formula_fold pos (is_var_positively_naked_in_term name) phi false - | Undercover_Vars => + | Undercover_Types => formula_fold pos (is_var_positively_naked_or_undercover_in_term thy name) - phi false) + phi false + | _ => false) | should_guard_var_in_formula _ _ _ _ _ _ = true fun always_guard_var_in_formula _ _ _ _ _ _ = true fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T = - granularity_of_type_level level <> All_Vars andalso + not (is_type_level_uniform level) andalso should_encode_type ctxt mono level T | should_generate_tag_bound_decl _ _ _ _ _ = false @@ -2336,8 +2346,7 @@ fun monotonic_types_for_facts ctxt mono type_enc facts = let val level = level_of_type_enc type_enc in [] |> (is_type_enc_polymorphic type_enc andalso - is_type_level_monotonicity_based level andalso - granularity_of_type_level level <> Undercover_Vars) + is_type_level_monotonicity_based level) ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end @@ -2432,8 +2441,7 @@ let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc - val grain = granularity_of_type_level level - val ident_base = + val ident = tags_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else "") val (role, maybe_negate) = honor_conj_sym_role in_conj @@ -2448,7 +2456,7 @@ if should_encode res_T then let val tagged_bounds = - if grain = Undercover_Vars then + if level = Undercover_Types then let val cover = type_arg_cover thy s ary in map2 (fn (j, arg_T) => member (op =) cover j ? tag_with arg_T) (0 upto ary - 1 ~~ arg_Ts) bounds @@ -2456,7 +2464,7 @@ else bounds in - cons (Formula (ident_base ^ "_res", role, + cons (Formula (ident, role, eq (tag_with res_T (cst bounds)) (cst tagged_bounds), NONE, isabelle_info defN helper_rank)) end @@ -2494,7 +2502,7 @@ |-> map2 (line_for_guards_sym_decl ctxt mono type_enc n s) end | Tags (_, level) => - if granularity_of_type_level level = All_Vars then + if is_type_level_uniform level then [] else let val n = length decls in