# HG changeset patch # User blanchet # Date 1340702079 -7200 # Node ID defbcdc60fd65d8da427b0fe4ddc15702078e12b # Parent 933d43c31689355db234d727eb16ce77771727a5 tuning diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Tue Jun 26 11:14:39 2012 +0200 @@ -174,7 +174,7 @@ let val type_enc = type_enc |> type_enc_from_string Strict |> adjust_type_enc format - val mono = polymorphism_of_type_enc type_enc <> Polymorphic + val mono = polymorphism_of_type_enc type_enc <> Raw_Polymorphic val path = file_name |> Path.explode val _ = File.write path "" val facts = facts_of thy diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Tue Jun 26 11:14:39 2012 +0200 @@ -28,7 +28,7 @@ gen_prec : bool, gen_simp : bool} - datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic + datatype polymorphism = Monomorphic | Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_choice = THF_Without_Choice | THF_With_Choice datatype thf_defs = THF_Without_Defs | THF_With_Defs @@ -37,8 +37,8 @@ CNF | CNF_UEQ | FOF | - TFF of tptp_polymorphism * tptp_explicitness | - THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs | + TFF of polymorphism * tptp_explicitness | + THF of polymorphism * tptp_explicitness * thf_choice * thf_defs | DFG datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture @@ -160,7 +160,7 @@ gen_prec : bool, gen_simp : bool} -datatype tptp_polymorphism = TPTP_Monomorphic | TPTP_Polymorphic +datatype polymorphism = Monomorphic | Polymorphic datatype tptp_explicitness = TPTP_Implicit | TPTP_Explicit datatype thf_choice = THF_Without_Choice | THF_With_Choice datatype thf_defs = THF_Without_Defs | THF_With_Defs @@ -169,8 +169,8 @@ CNF | CNF_UEQ | FOF | - TFF of tptp_polymorphism * tptp_explicitness | - THF of tptp_polymorphism * tptp_explicitness * thf_choice * thf_defs | + TFF of polymorphism * tptp_explicitness | + THF of polymorphism * tptp_explicitness * thf_choice * thf_defs | DFG datatype formula_role = Axiom | Definition | Lemma | Hypothesis | Conjecture @@ -786,7 +786,7 @@ if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE val avoid_clash = case format of - TFF (TPTP_Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars + TFF (Polymorphic, _) => avoid_clash_with_alt_ergo_type_vars | DFG => avoid_clash_with_dfg_keywords | _ => I val nice_name = nice_name avoid_clash diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Jun 26 11:14:39 2012 +0200 @@ -22,7 +22,7 @@ General | Induction | Intro | Inductive | Elim | Simp | Def type stature = scope * status - datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic + datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype strictness = Strict | Non_Strict datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars datatype type_level = @@ -126,7 +126,7 @@ datatype order = First_Order | Higher_Order of thf_choice -datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic +datatype polymorphism = Raw_Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype strictness = Strict | Non_Strict datatype granularity = All_Vars | Positively_Naked_Vars | Undercover_Vars datatype type_level = @@ -607,7 +607,7 @@ fun type_enc_from_string strictness s = (case try (unprefix "poly_") s of - SOME s => (SOME Polymorphic, s) + SOME s => (SOME Raw_Polymorphic, s) | NONE => case try (unprefix "raw_mono_") s of SOME s => (SOME Raw_Monomorphic, s) @@ -629,8 +629,8 @@ case (core, (poly, level)) of ("native", (SOME poly, _)) => (case (poly, level) of - (Polymorphic, All_Types) => - Native (First_Order, Polymorphic, All_Types) + (Raw_Polymorphic, All_Types) => + Native (First_Order, Raw_Polymorphic, All_Types) | (Mangled_Monomorphic, _) => if granularity_of_type_level level = All_Vars then Native (First_Order, Mangled_Monomorphic, level) @@ -639,8 +639,8 @@ | _ => raise Same.SAME) | ("native_higher", (SOME poly, _)) => (case (poly, level) of - (Polymorphic, All_Types) => - Native (Higher_Order THF_With_Choice, Polymorphic, All_Types) + (Raw_Polymorphic, All_Types) => + Native (Higher_Order THF_With_Choice, Raw_Polymorphic, All_Types) | (_, Nonmono_Types _) => raise Same.SAME | (Mangled_Monomorphic, _) => if granularity_of_type_level level = All_Vars then @@ -666,7 +666,7 @@ if poly = Mangled_Monomorphic then raise Same.SAME else Guards (poly, Const_Types true) | ("erased", (NONE, All_Types (* naja *))) => - Guards (Polymorphic, No_Types) + Guards (Raw_Polymorphic, No_Types) | _ => raise Same.SAME) handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") @@ -674,13 +674,13 @@ Higher_Order THF_Without_Choice | adjust_order _ type_enc = type_enc -fun adjust_type_enc (THF (TPTP_Polymorphic, _, choice, _)) +fun adjust_type_enc (THF (Polymorphic, _, choice, _)) (Native (order, poly, level)) = Native (adjust_order choice order, poly, level) - | adjust_type_enc (THF (TPTP_Monomorphic, _, choice, _)) + | adjust_type_enc (THF (Monomorphic, _, choice, _)) (Native (order, _, level)) = Native (adjust_order choice order, Mangled_Monomorphic, level) - | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Native (_, _, level)) = + | adjust_type_enc (TFF (Monomorphic, _)) (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) | adjust_type_enc DFG (Native (_, _, level)) = Native (First_Order, Mangled_Monomorphic, level) @@ -774,7 +774,7 @@ fun lift_lams_part_1 ctxt type_enc = map close_form #> rpair ctxt #-> Lambda_Lifting.lift_lambdas - (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then + (SOME ((if polymorphism_of_type_enc type_enc = Raw_Polymorphic then lam_lifted_poly_prefix else lam_lifted_mono_prefix) ^ "_a")) @@ -839,7 +839,7 @@ if s = type_tag_name then if poly = Mangled_Monomorphic then Mangled_Type_Args else All_Type_Args else case type_enc of - Native (_, Polymorphic, _) => All_Type_Args + Native (_, Raw_Polymorphic, _) => All_Type_Args | Tags (_, All_Types) => No_Type_Args | _ => let val level = level_of_type_enc type_enc in @@ -877,7 +877,7 @@ fun type_class_formula type_enc class arg = AAtom (ATerm (class, arg :: (case type_enc of - Native (First_Order, Polymorphic, _) => + Native (First_Order, Raw_Polymorphic, _) => if avoid_first_order_phantom_type_vars then [ATerm (TYPE_name, [arg])] else [] | _ => []))) @@ -981,7 +981,7 @@ fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys) | to_poly_atype _ = raise Fail "unexpected type abstraction" val to_atype = - if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then to_poly_atype else to_mangled_atype fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1)) fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty @@ -1703,7 +1703,7 @@ @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))] |> map (apsnd (map (apsnd zero_var_indexes))) -fun atype_of_type_vars (Native (_, Polymorphic, _)) = SOME atype_of_types +fun atype_of_type_vars (Native (_, Raw_Polymorphic, _)) = SOME atype_of_types | atype_of_type_vars _ = NONE fun bound_tvars type_enc sorts Ts = @@ -1730,7 +1730,7 @@ val type_tag = `(make_fixed_const NONE) type_tag_name fun could_specialize_helpers type_enc = - polymorphism_of_type_enc type_enc <> Polymorphic andalso + polymorphism_of_type_enc type_enc <> Raw_Polymorphic andalso level_of_type_enc type_enc <> No_Types fun should_specialize_helper type_enc t = could_specialize_helpers type_enc andalso @@ -2118,7 +2118,7 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) -fun type_enc_needs_free_types (Native (_, Polymorphic, _)) = true +fun type_enc_needs_free_types (Native (_, Raw_Polymorphic, _)) = true | type_enc_needs_free_types (Native _) = false | type_enc_needs_free_types _ = true @@ -2151,7 +2151,8 @@ fun decl_lines_for_classes type_enc classes = case type_enc of - Native (order, Polymorphic, _) => map (decl_line_for_class order) classes + Native (order, Raw_Polymorphic, _) => + map (decl_line_for_class order) classes | _ => [] fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) = @@ -2191,7 +2192,7 @@ fold add_formula_var_types phis | add_formula_var_types _ = I fun var_types () = - if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a] + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then [tvar_a] else fold (ifact_lift add_formula_var_types) (conjs @ facts) [] fun add_undefined_const T = let @@ -2216,7 +2217,7 @@ ? (fold (fold add_fact_syms) [conjs, facts] #> fold add_iterm_syms extra_tms #> (case type_enc of - Native (First_Order, Polymorphic, _) => + Native (First_Order, Raw_Polymorphic, _) => if avoid_first_order_phantom_type_vars then add_TYPE_const () else I | Native _ => I @@ -2283,7 +2284,7 @@ add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift fun monotonic_types_for_facts ctxt mono type_enc facts = let val level = level_of_type_enc type_enc in - [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso + [] |> (polymorphism_of_type_enc type_enc = Raw_Polymorphic andalso is_type_level_monotonicity_based level andalso granularity_of_type_level level <> Undercover_Vars) ? fold (add_fact_monotonic_types ctxt mono type_enc) facts @@ -2630,7 +2631,7 @@ Full_App_Op_And_Predicator else if length facts + length hyp_ts > app_op_and_predicator_threshold then - if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then Min_App_Op else Sufficient_App_Op else Sufficient_App_Op_And_Predicator diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Jun 26 11:14:39 2012 +0200 @@ -55,8 +55,7 @@ val satallax_unsat_coreN : string val parse_formula : string list -> (string, 'a, (string, 'a) ho_term) formula * string list - val atp_proof_from_tstplike_proof : - string problem -> string -> string -> string proof + val atp_proof_from_tstplike_proof : string problem -> string -> string proof val clean_up_atp_proof_dependencies : string proof -> string proof val map_term_names_in_atp_proof : (string -> string) -> string proof -> string proof @@ -485,8 +484,8 @@ (Scan.repeat1 (parse_line problem)))) |> fst -fun atp_proof_from_tstplike_proof _ _ "" = [] - | atp_proof_from_tstplike_proof problem output tstp = +fun atp_proof_from_tstplike_proof _ "" = [] + | atp_proof_from_tstplike_proof problem tstp = tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof problem |> sort (step_name_ord o pairself step_name) (* FIXME: needed? *) diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Jun 26 11:14:39 2012 +0200 @@ -185,7 +185,7 @@ (* Alt-Ergo *) -val alt_ergo_tff1 = TFF (TPTP_Polymorphic, TPTP_Explicit) +val alt_ergo_tff1 = TFF (Polymorphic, TPTP_Explicit) val alt_ergo_config : atp_config = {exec = (["WHY3_HOME"], "why3"), @@ -330,7 +330,7 @@ (* LEO-II supports definitions, but it performs significantly better on our benchmarks when they are not used. *) val leo2_thf0 = - THF (TPTP_Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs) + THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs) val leo2_config : atp_config = {exec = (["LEO2_HOME"], "leo"), @@ -359,7 +359,7 @@ (* Satallax *) val satallax_thf0 = - THF (TPTP_Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) + THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) val satallax_config : atp_config = {exec = (["SATALLAX_HOME"], "satallax"), @@ -429,7 +429,7 @@ fun is_new_vampire_version () = string_ord (getenv "VAMPIRE_VERSION", "1.8") = GREATER -val vampire_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) +val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit) val vampire_config : atp_config = {exec = (["VAMPIRE_HOME"], "vampire"), @@ -473,7 +473,7 @@ (* Z3 with TPTP syntax *) -val z3_tff0 = TFF (TPTP_Monomorphic, TPTP_Implicit) +val z3_tff0 = TFF (Monomorphic, TPTP_Implicit) val z3_tptp_config : atp_config = {exec = (["Z3_HOME"], "z3"), @@ -512,7 +512,7 @@ best_max_new_mono_instances = default_max_new_mono_instances} val dummy_thf_format = - THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) + THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs) val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher" val dummy_thf = (dummy_thfN, fn () => dummy_thf_config) @@ -587,7 +587,7 @@ (remote_prefix ^ name, remotify_config system_name system_versions best_slice o config) -val explicit_tff0 = TFF (TPTP_Monomorphic, TPTP_Explicit) +val explicit_tff0 = TFF (Monomorphic, TPTP_Explicit) val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Tue Jun 26 11:14:39 2012 +0200 @@ -211,7 +211,7 @@ fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses = let val (conj_clauses, fact_clauses) = - if polymorphism_of_type_enc type_enc = Polymorphic then + if polymorphism_of_type_enc type_enc = Raw_Polymorphic then (conj_clauses, fact_clauses) else conj_clauses @ fact_clauses diff -r 933d43c31689 -r defbcdc60fd6 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Jun 26 11:14:39 2012 +0200 @@ -717,7 +717,7 @@ |> not sound ? filter_out (is_dangerous_prop ctxt o prop_of o snd) |> take num_facts - |> polymorphism_of_type_enc type_enc <> Polymorphic + |> polymorphism_of_type_enc type_enc <> Raw_Polymorphic ? monomorphize_facts |> map (apsnd prop_of) |> prepare_atp_problem ctxt format prem_role type_enc @@ -750,7 +750,7 @@ (accum, extract_tstplike_proof_and_outcome verbose complete proof_delims known_failures output - |>> atp_proof_from_tstplike_proof atp_problem output + |>> atp_proof_from_tstplike_proof atp_problem handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete))) handle TimeLimit.TimeOut =>