# HG changeset patch # User blanchet # Date 1368702352 -7200 # Node ID 97dd505ee058687cc3402e5c7dc53a36f6f2b214 # Parent 9f94930b12e67e16c83b65833549b046f5a52b6f tuning diff -r 9f94930b12e6 -r 97dd505ee058 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:05:52 2013 +0200 @@ -25,12 +25,12 @@ datatype strictness = Strict | Non_Strict datatype uniformity = Uniform | Non_Uniform - datatype constr_optim = With_Constr_Optim | Without_Constr_Optim + datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim datatype type_level = All_Types | Undercover_Types | Nonmono_Types of strictness * uniformity | - Const_Types of constr_optim | + Const_Types of ctr_optim | No_Types type type_enc @@ -142,12 +142,12 @@ Mangled_Monomorphic datatype strictness = Strict | Non_Strict datatype uniformity = Uniform | Non_Uniform -datatype constr_optim = With_Constr_Optim | Without_Constr_Optim +datatype ctr_optim = With_Ctr_Optim | Without_Ctr_Optim datatype type_level = All_Types | Undercover_Types | Nonmono_Types of strictness * uniformity | - Const_Types of constr_optim | + Const_Types of ctr_optim | No_Types datatype type_enc = @@ -671,13 +671,13 @@ Tags (poly, level) | ("args", (SOME poly, All_Types (* naja *))) => if poly = Type_Class_Polymorphic then raise Same.SAME - else Guards (poly, Const_Types Without_Constr_Optim) + else Guards (poly, Const_Types Without_Ctr_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 With_Constr_Optim) + Guards (poly, Const_Types With_Ctr_Optim) | ("erased", (NONE, All_Types (* naja *))) => Guards (Raw_Polymorphic With_Phantom_Type_Vars, No_Types) | _ => raise Same.SAME) @@ -850,7 +850,7 @@ chop_fun (n - 1) ran_T |>> cons dom_T | chop_fun _ T = ([], T) -fun filter_type_args thy constrs type_enc s ary T_args = +fun filter_type_args thy ctrs type_enc s ary T_args = let val poly = polymorphism_of_type_enc type_enc in if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *) T_args @@ -876,7 +876,7 @@ in map (filt o apfst dest_TVar) (U_args ~~ T_args) end handle TYPE _ => T_args val noninfer_type_args = gen_type_args (not o fst) (chop_fun ary) - val constr_infer_type_args = gen_type_args fst strip_type + val ctr_infer_type_args = gen_type_args fst strip_type val level = level_of_type_enc type_enc in if level = No_Types orelse s = @{const_name HOL.eq} orelse @@ -890,9 +890,9 @@ | Tags _ => [] else if level = Undercover_Types then noninfer_type_args T_args - else if member (op =) constrs s andalso - level <> Const_Types Without_Constr_Optim then - constr_infer_type_args T_args + else if member (op =) ctrs s andalso + level <> Const_Types Without_Ctr_Optim then + ctr_infer_type_args T_args else T_args end @@ -1173,19 +1173,18 @@ I fun filter_type_args_in_const _ _ _ _ _ [] = [] - | filter_type_args_in_const thy constrs type_enc ary s T_args = + | filter_type_args_in_const thy ctrs 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'' => - filter_type_args thy constrs type_enc (unmangled_invert_const s'') ary - T_args -fun filter_type_args_in_iterm thy constrs type_enc = + filter_type_args thy ctrs type_enc (unmangled_invert_const s'') ary T_args +fun filter_type_args_in_iterm thy ctrs 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 constrs type_enc ary s T_args + filter_type_args_in_const thy ctrs 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 @@ -1643,8 +1642,7 @@ |> mangle_type_args_in_iterm type_enc in list_app app [head, arg] end -fun firstorderize_fact thy constrs type_enc sym_tab uncurried_aliases - completish = +fun firstorderize_fact thy ctrs type_enc sym_tab uncurried_aliases completish = let fun do_app arg head = mk_app_op type_enc head arg fun list_app_ops (head, args) = fold do_app args head @@ -1692,7 +1690,7 @@ val do_iterm = not (is_type_enc_higher_order type_enc) ? (introduce_app_ops #> introduce_predicators) - #> filter_type_args_in_iterm thy constrs type_enc + #> filter_type_args_in_iterm thy ctrs type_enc in update_iformula (formula_map do_iterm) end (** Helper facts **) @@ -1874,24 +1872,23 @@ val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars -fun fold_type_constrs f (Type (s, Ts)) x = - fold (fold_type_constrs f) Ts (f (s, x)) - | fold_type_constrs _ _ x = x +fun fold_type_ctrs f (Type (s, Ts)) x = fold (fold_type_ctrs f) Ts (f (s, x)) + | fold_type_ctrs _ _ x = x (* Type constructors used to instantiate overloaded constants are the only ones needed. *) -fun add_type_constrs_in_term thy = +fun add_type_ctrs_in_term thy = let fun add (Const (@{const_name Meson.skolem}, _) $ _) = I | add (t $ u) = add t #> add u | add (Const x) = - x |> robust_const_type_args thy |> fold (fold_type_constrs set_insert) + x |> robust_const_type_args thy |> fold (fold_type_ctrs set_insert) | add (Abs (_, _, u)) = add u | add _ = I in add end -fun type_constrs_of_terms thy ts = - Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty) +fun type_ctrs_of_terms thy ts = + Symtab.keys (fold (add_type_ctrs_in_term thy) ts Symtab.empty) fun extract_lambda_def (Const (@{const_name HOL.eq}, _) $ t $ u) = let val (head, args) = strip_comb t in @@ -1991,7 +1988,7 @@ val all_ts = concl_t :: hyp_ts @ fact_ts val subs = tfree_classes_of_terms all_ts val supers = tvar_classes_of_terms all_ts - val tycons = type_constrs_of_terms thy all_ts + val tycons = type_ctrs_of_terms thy all_ts val (supers, tcon_clauses) = if level_of_type_enc type_enc = No_Types then ([], []) else make_tcon_clauses thy tycons supers @@ -2539,24 +2536,23 @@ val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms in mono_lines @ decl_lines end -fun datatypes_of_facts ctxt (DFG Polymorphic) (type_enc as Native (_, _, level)) - facts = +fun datatypes_of_sym_table ctxt mono (DFG Polymorphic) + (type_enc as Native (_, _, level)) sym_tab = let val thy = Proof_Context.theory_of ctxt - val mono = default_mono level false val ho_term_from_term = iterm_from_term thy type_enc [] #> fst #> ho_term_from_iterm ctxt mono type_enc NONE in if is_type_enc_polymorphic type_enc then [(native_ho_type_from_typ type_enc false 0 @{typ nat}, - map ho_term_from_term [@{term "0::nat"}, @{term Suc}]) (*, + map ho_term_from_term [@{term "0::nat"}, @{term Suc}]), (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}), - map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}]) *)] + map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}])] else [] end - | datatypes_of_facts _ _ _ _ = [] + | datatypes_of_sym_table _ _ _ _ _ = [] fun decl_line_of_datatype (ty as AType ((_, s'), ty_args), ctrs) = let @@ -2568,7 +2564,7 @@ fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 sym_tab +fun do_uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 sym_tab base_s0 types in_conj = let fun do_alias ary = @@ -2582,7 +2578,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 constrs type_enc + val filter_ty_args = filter_type_args_in_iterm thy ctrs 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) @@ -2613,27 +2609,27 @@ else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 - sym_tab (s, {min_ary, types, in_conj, ...} : sym_info) = +fun uncurried_alias_lines_of_sym ctxt ctrs 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 => if String.isSubstring uncurried_alias_sep mangled_s then let val base_s0 = mangled_s |> unmangled_invert_const in - do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 - sym_tab base_s0 types in_conj min_ary + do_uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 sym_tab + base_s0 types in_conj min_ary end else ([], []) | NONE => ([], []) -fun uncurried_alias_lines_of_sym_table ctxt constrs mono type_enc - uncurried_aliases sym_tab0 sym_tab = +fun uncurried_alias_lines_of_sym_table ctxt ctrs mono type_enc uncurried_aliases + sym_tab0 sym_tab = ([], []) |> uncurried_aliases ? Symtab.fold_rev (pair_append - o uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 + o uncurried_alias_lines_of_sym ctxt ctrs mono type_enc sym_tab0 sym_tab) sym_tab val implicit_declsN = "Should-be-implicit typings" @@ -2715,13 +2711,13 @@ syms [] in (heading, decls) :: problem end -fun is_poly_constr (Datatype.DtTFree _) = true - | is_poly_constr (Datatype.DtType (_, Us)) = exists is_poly_constr Us - | is_poly_constr _ = false +fun is_poly_ctr (Datatype.DtTFree _) = true + | is_poly_ctr (Datatype.DtType (_, Us)) = exists is_poly_ctr Us + | is_poly_ctr _ = false -fun all_constrs_of_polymorphic_datatypes thy = +fun all_ctrs_of_polymorphic_datatypes thy = Symtab.fold (snd #> #descr #> maps (#3 o snd) - #> (fn cs => exists (exists is_poly_constr o snd) cs + #> (fn cs => exists (exists is_poly_ctr o snd) cs ? append (map fst cs))) (Datatype.get_all thy) [] @@ -2762,15 +2758,15 @@ sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish - val constrs = all_constrs_of_polymorphic_datatypes thy + val ctrs = all_ctrs_of_polymorphic_datatypes thy fun firstorderize in_helper = - firstorderize_fact thy constrs type_enc sym_tab0 + firstorderize_fact thy ctrs type_enc sym_tab0 (uncurried_aliases andalso not in_helper) completish val (conjs, facts) = (conjs, facts) |> pairself (map (firstorderize false)) val (ho_stuff, sym_tab) = sym_table_of_facts ctxt type_enc Min_App_Op conjs facts val (uncurried_alias_eq_tms, uncurried_alias_eq_lines) = - uncurried_alias_lines_of_sym_table ctxt constrs mono type_enc + uncurried_alias_lines_of_sym_table ctxt ctrs mono type_enc uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab) @@ -2781,7 +2777,7 @@ |> map (firstorderize true) val all_facts = helpers @ conjs @ facts val mono_Ts = monotonic_types_of_facts ctxt mono type_enc all_facts - val datatypes = datatypes_of_facts ctxt format type_enc all_facts + val datatypes = datatypes_of_sym_table ctxt mono format type_enc sym_tab val class_decl_lines = decl_lines_of_classes type_enc classes val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms)