# HG changeset patch # User blanchet # Date 1341497235 -7200 # Node ID 5156cadedfa51b5155d5c6c7cb8c14251e4dad3d # Parent 0e552737cc5a7199bd09ab5dc37d1588c606bd5b fiddled with "tags_at" a bit -- the only non-tuning part of the change is a slight simplification of the typing axioms diff -r 0e552737cc5a -r 5156cadedfa5 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 05 16:07:15 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu Jul 05 16:07:15 2012 +0200 @@ -26,8 +26,8 @@ datatype constr_optim = With_Constr_Optim | Without_Constr_Optim datatype type_level = All_Types | + Undercover_Types | Nonmono_Types of strictness * uniformity | - Undercover_Types | Const_Types of constr_optim | No_Types type type_enc @@ -137,8 +137,8 @@ datatype constr_optim = With_Constr_Optim | Without_Constr_Optim datatype type_level = All_Types | + Undercover_Types | Nonmono_Types of strictness * uniformity | - Undercover_Types | Const_Types of constr_optim | No_Types @@ -834,10 +834,10 @@ (* The Booleans indicate whether all type arguments should be kept. *) datatype type_arg_policy = - Mangled_Type_Args | + Mangled_Type_Args | (* ### TODO: get rid of this *) All_Type_Args | - Not_Input_Type_Args | - Constr_Input_Type_Args | + Noninfer_Type_Args | + Constr_Infer_Type_Args | No_Type_Args fun type_arg_policy constrs type_enc s = @@ -847,7 +847,6 @@ else case type_enc of Native (_, Raw_Polymorphic _, _) => All_Type_Args | Native (_, Type_Class_Polymorphic, _) => All_Type_Args - | Tags (_, All_Types) => No_Type_Args | _ => let val level = level_of_type_enc type_enc in if level = No_Types orelse s = @{const_name HOL.eq} orelse @@ -855,11 +854,15 @@ No_Type_Args else if poly = Mangled_Monomorphic then Mangled_Type_Args - else if level = All_Types orelse level = Undercover_Types then - Not_Input_Type_Args + else if level = All_Types then + case type_enc of + Guards _ => Noninfer_Type_Args + | Tags _ => No_Type_Args + else if level = Undercover_Types then + Noninfer_Type_Args else if member (op =) constrs s andalso level <> Const_Types Without_Constr_Optim then - Constr_Input_Type_Args + Constr_Infer_Type_Args else All_Type_Args end @@ -1170,9 +1173,9 @@ case type_arg_policy constrs type_enc s'' of Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" | All_Type_Args => T_args - | Not_Input_Type_Args => + | Noninfer_Type_Args => filter_type_args (not o fst) thy s'' (chop_fun ary) T_args - | Constr_Input_Type_Args => + | Constr_Infer_Type_Args => filter_type_args fst thy s'' strip_type T_args | No_Type_Args => [] end @@ -1337,27 +1340,22 @@ (** Finite and infinite type inference **) -fun tvar_footprint thy body s ary = +fun tvar_footprint thy s ary = (case unprefix_and_unascii const_prefix s of SOME s => - let - val (binder_Ts, body_T) = - s |> invert_const |> robust_const_type thy |> chop_fun ary - fun tvars_of T = - [] |> Term.add_tvarsT T - |> (fn Ts => if body then Ts - else subtract (op =) (Term.add_tvarsT body_T []) Ts) - |> map fst - in binder_Ts |> map tvars_of end + let fun tvars_of T = [] |> Term.add_tvarsT T |> map fst in + s |> invert_const |> robust_const_type thy |> chop_fun ary |> fst + |> map tvars_of + end | NONE => []) handle TYPE _ => [] -fun type_arg_cover thy pos body s ary = +fun type_arg_cover thy pos s ary = if is_tptp_equal s then if pos = SOME false then [] else 0 upto ary - 1 else let - val footprint = tvar_footprint thy body s ary + val footprint = tvar_footprint thy s ary val eq = (s = @{const_name HOL.eq}) fun cover _ [] = [] | cover seen ((i, tvars) :: args) = @@ -1391,8 +1389,7 @@ proofs. On the other hand, all HOL infinite types can be given the same models in first-order logic (via Löwenheim-Skolem). *) -fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true - | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, +fun should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts, ...} (Nonmono_Types (strictness, _)) T = let val thy = Proof_Context.theory_of ctxt in @@ -1402,16 +1399,18 @@ is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts T))) end - | should_encode_type _ _ Undercover_Types _ = true - | should_encode_type _ _ _ _ = false + | should_encode_type _ _ level _ = + (level = All_Types orelse level = Undercover_Types) fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T = should_guard_var () andalso should_encode_type ctxt mono level T | should_guard_type _ _ _ _ _ = false -fun is_maybe_universal_var (IConst ((s, _), _, _)) = - String.isPrefix bound_var_prefix s orelse - String.isPrefix all_bound_var_prefix s +fun is_maybe_universal_name s = + String.isPrefix bound_var_prefix s orelse + String.isPrefix all_bound_var_prefix s + +fun is_maybe_universal_var (IConst ((s, _), _, _)) = is_maybe_universal_name s | is_maybe_universal_var (IVar _) = true | is_maybe_universal_var _ = false @@ -1433,7 +1432,7 @@ (case (site, is_maybe_universal_var u) of (Eq_Arg pos, true) => pos <> SOME false | (Arg (s, j, ary), true) => - member (op =) (type_arg_cover thy NONE true s ary) j + member (op =) (type_arg_cover thy NONE s ary) j | _ => false) | _ => should_encode_type ctxt mono level T end @@ -1516,8 +1515,7 @@ let val (head, args) = strip_iterm_comb tm in (case head of IConst ((s, _), T, _) => - if String.isPrefix bound_var_prefix s orelse - String.isPrefix all_bound_var_prefix s then + if is_maybe_universal_name s then add_universal_var T accum else if String.isPrefix exist_bound_var_prefix s then accum @@ -1998,7 +1996,7 @@ | is_undercover (ATerm (((s, _), _), tms)) = let val ary = length tms - val cover = type_arg_cover thy pos true s ary + val cover = type_arg_cover thy pos s ary in exists (fn (j, tm) => tm = var andalso member (op =) cover j) (0 upto ary - 1 ~~ tms) orelse @@ -2010,11 +2008,11 @@ fun should_guard_var_in_formula thy level pos phi (SOME true) name = (case level of All_Types => true + | Undercover_Types => + formula_fold pos (is_var_undercover_in_term thy name) phi false | Nonmono_Types (_, Uniform) => true | Nonmono_Types (_, Non_Uniform) => formula_fold pos (is_var_positively_naked_in_term name) phi false - | Undercover_Types => - formula_fold pos (is_var_undercover_in_term thy name) phi false | _ => false) | should_guard_var_in_formula _ _ _ _ _ _ = true @@ -2054,6 +2052,7 @@ Top_Level pos => pos | Eq_Arg pos => pos | _ => NONE + val T = ityp_of u val t = case head of IConst (name as (s, _), _, T_args) => @@ -2074,13 +2073,8 @@ else raise Fail "unexpected lambda-abstraction" | IApp _ => raise Fail "impossible \"IApp\"" - val T = ityp_of u - in - if should_tag_with_type ctxt mono type_enc site u T then - tag_with_type ctxt mono type_enc pos T t - else - t - end + val tag = should_tag_with_type ctxt mono type_enc site u T + in t |> tag ? tag_with_type ctxt mono type_enc pos T end in term (Top_Level pos) end and formula_from_iformula ctxt mono type_enc should_guard_var = let @@ -2263,6 +2257,7 @@ else fold (ifact_lift add_formula_var_types) (conjs @ facts) [] fun add_undefined_const T = let + (* FIXME: make sure type arguments are filtered / clean up code *) val (s, s') = `(make_fixed_const NONE) @{const_name undefined} |> (case type_arg_policy [] type_enc @{const_name undefined} of @@ -2420,7 +2415,7 @@ bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, [])) val bound_Ts = if exists (curry (op =) dummyT) T_args then - let val cover = type_arg_cover thy NONE true s ary in + let val cover = type_arg_cover thy NONE s ary in map2 (fn j => if member (op =) cover j then SOME else K NONE) (0 upto ary - 1) arg_Ts end @@ -2455,30 +2450,22 @@ val bounds = bound_names |> map (fn name => ATerm ((name, []), [])) val cst = mk_aterm type_enc (s, s') T_args val eq = maybe_negate oo eq_formula type_enc (atomic_types_of T) [] pred_sym - val should_encode = should_encode_type ctxt mono level val tag_with = tag_with_type ctxt mono type_enc NONE - val add_formula_for_res = - if should_encode res_T then - let - val (lhs, rhs) = - if level = Undercover_Types then - let - val lhs_cover = type_arg_cover thy NONE false s ary - val rhs_cover = type_arg_cover thy NONE true s ary - fun maybe_tag cover (j, arg_T) = - member (op =) cover j ? tag_with arg_T - fun covered_bounds cover = - map2 (maybe_tag cover) (0 upto ary - 1 ~~ arg_Ts) bounds - in (lhs_cover, rhs_cover) |> pairself (covered_bounds #> cst) end - else - `I (cst bounds) - in - cons (Formula (ident, role, eq (tag_with res_T lhs) rhs, - NONE, isabelle_info defN helper_rank)) - end - else - I - in [] |> not pred_sym ? add_formula_for_res end + fun formula c = + [Formula (ident, role, eq (tag_with res_T c) c, NONE, isabelle_info + defN helper_rank)] + in + if pred_sym orelse not (should_encode_type ctxt mono level res_T) then + [] + else if level = Undercover_Types then + let + val cover = type_arg_cover thy NONE s ary + fun maybe_tag (j, arg_T) = member (op =) cover j ? tag_with arg_T + val bounds = bounds |> map2 maybe_tag (0 upto ary - 1 ~~ arg_Ts) + in formula (cst bounds) end + else + formula (cst bounds) + end fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd