# HG changeset patch # User blanchet # Date 1338971705 -7200 # Node ID c75f36d190df39c86cacf874e337822eccde487e # Parent 94835838ed2c7960e4f12bde47e83cb1db04c614 generalized monotonic constructor optimisation so that it works with e.g. the product type diff -r 94835838ed2c -r c75f36d190df src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jun 06 10:35:05 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jun 06 10:35:05 2012 +0200 @@ -840,17 +840,18 @@ (* The Booleans indicate whether all type arguments should be kept. *) datatype type_arg_policy = - Explicit_Type_Args of bool (* infer_from_term_args *) | Mangled_Type_Args | + All_Type_Args | + Noninferable_Type_Args | + Constr_Type_Args | No_Type_Args -fun type_arg_policy monom_constrs type_enc s = +fun type_arg_policy constrs type_enc s = let val poly = polymorphism_of_type_enc type_enc in if s = type_tag_name then - if poly = Mangled_Monomorphic then Mangled_Type_Args - else Explicit_Type_Args false + if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args else case type_enc of - Native (_, Polymorphic, _) => Explicit_Type_Args false + Native (_, Polymorphic, _) => All_Type_Args | Tags (_, All_Types) => No_Type_Args | _ => let val level = level_of_type_enc type_enc in @@ -859,13 +860,13 @@ No_Type_Args else if poly = Mangled_Monomorphic then Mangled_Type_Args - else if member (op =) monom_constrs s andalso - granularity_of_type_level level <> Ghost_Type_Arg_Vars then - No_Type_Args + else if level = All_Types orelse + granularity_of_type_level level = Ghost_Type_Arg_Vars then + Noninferable_Type_Args + else if member (op =) constrs s then + Constr_Type_Args else - Explicit_Type_Args - (level = All_Types orelse - granularity_of_type_level level = Ghost_Type_Arg_Vars) + All_Type_Args end end @@ -1131,42 +1132,38 @@ chop_fun (n - 1) ran_T |>> cons dom_T | chop_fun _ T = ([], T) -fun filter_const_type_args _ _ _ [] = [] - | filter_const_type_args thy s ary T_args = +fun infer_type_args _ _ _ _ [] = [] + | infer_type_args maybe_not thy s binders_of T_args = let val U = robust_const_type thy s - val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) [] + val arg_U_vars = fold Term.add_tvarsT (binders_of U) [] + fun filt (U, T) = + if maybe_not (member (op =) arg_U_vars (dest_TVar U)) then dummyT else T val U_args = (s, U) |> robust_const_typargs thy - in - U_args ~~ T_args - |> map (fn (U, T) => - if member (op =) arg_U_vars (dest_TVar U) then dummyT else T) - end + in map filt (U_args ~~ T_args) end handle TYPE _ => T_args fun filter_type_args_in_const _ _ _ _ _ [] = [] - | filter_type_args_in_const thy monom_constrs type_enc ary s T_args = + | filter_type_args_in_const thy constrs type_enc ary s T_args = case unprefix_and_unascii const_prefix s of NONE => if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then [] else T_args | SOME s'' => - let - val s'' = invert_const s'' - fun filter_T_args false = T_args - | filter_T_args true = filter_const_type_args thy s'' ary T_args - in - case type_arg_policy monom_constrs type_enc s'' of - Explicit_Type_Args infer_from_term_args => - filter_T_args infer_from_term_args + let val s'' = invert_const s'' in + case type_arg_policy constrs type_enc s'' of + Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" + | All_Type_Args => T_args + | Noninferable_Type_Args => + infer_type_args I thy s'' (fst o chop_fun ary) T_args + | Constr_Type_Args => infer_type_args not thy s'' binder_types T_args | No_Type_Args => [] - | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol" end -fun filter_type_args_in_iterm thy monom_constrs type_enc = +fun filter_type_args_in_iterm thy constrs type_enc = let fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2) | filt ary (IConst (name as (s, _), T, T_args)) = - filter_type_args_in_const thy monom_constrs type_enc ary s T_args + filter_type_args_in_const thy constrs type_enc ary s T_args |> (fn T_args => IConst (name, T, T_args)) | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm) | filt _ tm = tm @@ -1623,7 +1620,7 @@ |> mangle_type_args_in_iterm type_enc in list_app app [head, arg] end -fun firstorderize_fact thy monom_constrs type_enc sym_tab uncurried_aliases +fun firstorderize_fact thy constrs type_enc sym_tab uncurried_aliases aggressive = let fun do_app arg head = mk_app_op type_enc head arg @@ -1651,7 +1648,7 @@ val do_iterm = not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators) - #> filter_type_args_in_iterm thy monom_constrs type_enc + #> filter_type_args_in_iterm thy constrs type_enc in update_iformula (formula_map do_iterm) end (** Helper facts **) @@ -2513,8 +2510,8 @@ fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0 - sym_tab base_s0 types in_conj = +fun do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 sym_tab + base_s0 types in_conj = let fun do_alias ary = let @@ -2527,8 +2524,7 @@ mangle_type_args_in_const type_enc base_name T_args val base_ary = min_ary_of sym_tab0 base_s fun do_const name = IConst (name, T, T_args) - val filter_ty_args = - filter_type_args_in_iterm thy monom_constrs type_enc + val filter_ty_args = filter_type_args_in_iterm thy constrs type_enc val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true) val name1 as (s1, _) = base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1) @@ -2558,7 +2554,7 @@ else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc sym_tab0 +fun uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => @@ -2566,20 +2562,20 @@ let val base_s0 = mangled_s |> unmangled_const_name |> hd |> invert_const in - do_uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc - sym_tab0 sym_tab base_s0 types in_conj min_ary + do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 + sym_tab base_s0 types in_conj min_ary end else ([], []) | NONE => ([], []) -fun uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc +fun uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc uncurried_aliases sym_tab0 sym_tab = ([], []) |> uncurried_aliases ? Symtab.fold_rev (pair_append - o uncurried_alias_lines_for_sym ctxt monom_constrs mono type_enc - sym_tab0 sym_tab) sym_tab + o uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 + sym_tab) sym_tab val implicit_declsN = "Should-be-implicit typings" val explicit_declsN = "Explicit typings" @@ -2658,17 +2654,14 @@ (case U of Datatype.DtType (_, Us) => exists ex Us | _ => false) in ex end -fun is_poly_constr (_, Us) = - exists (exists_subdtype (fn Datatype.DtTFree _ => true | _ => false)) Us +val is_poly_constr = + exists_subdtype (fn Datatype.DtTFree _ => true | _ => false) fun all_constrs_of_polymorphic_datatypes thy = - Symtab.fold (snd - #> #descr - #> maps (snd #> #3) - #> (fn cs => exists is_poly_constr cs ? append cs)) - (Datatype.get_all thy) [] - |> List.partition is_poly_constr - |> pairself (map fst) + Symtab.fold (snd #> #descr #> maps (#3 o snd) + #> (fn cs => exists (exists is_poly_constr o snd) cs + ? append (map fst cs))) + (Datatype.get_all thy) [] val app_op_and_predicator_threshold = 50 @@ -2707,17 +2700,15 @@ val (_, sym_tab0) = sym_table_for_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc - val (_, monom_constrs) = - all_constrs_of_polymorphic_datatypes thy - |>> map (make_fixed_const (SOME type_enc)) + val constrs = all_constrs_of_polymorphic_datatypes thy fun firstorderize in_helper = - firstorderize_fact thy monom_constrs type_enc sym_tab0 + firstorderize_fact thy constrs type_enc sym_tab0 (uncurried_aliases andalso not in_helper) aggressive val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) val (ho_stuff, sym_tab) = sym_table_for_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = - uncurried_alias_lines_for_sym_table ctxt monom_constrs mono type_enc + uncurried_alias_lines_for_sym_table ctxt constrs mono type_enc uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab)