# HG changeset patch # User blanchet # Date 1306916983 -7200 # Node ID a198260805967fae70bfed37d59b9aa759204eb2 # Parent a3f3b7a0e99ebdb98a46bad22ffcaffa5a1d3be3 tuned names diff -r a3f3b7a0e99e -r a19826080596 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Jun 01 10:29:43 2011 +0200 @@ -43,7 +43,7 @@ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic datatype type_level = All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types - datatype type_heaviness = Heavy | Light + datatype type_heaviness = Heavyweight | Lightweight datatype type_sys = Simple_Types of type_level | @@ -504,7 +504,7 @@ datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic datatype type_level = All_Types | Nonmonotonic_Types | Finite_Types | Const_Arg_Types | No_Types -datatype type_heaviness = Heavy | Light +datatype type_heaviness = Heavyweight | Lightweight datatype type_sys = Simple_Types of type_level | @@ -534,22 +534,22 @@ | NONE => (All_Types, s)) ||> apsnd (fn s => case try (unsuffix "_heavy") s of - SOME s => (Heavy, s) - | NONE => (Light, s)) + SOME s => (Heavyweight, s) + | NONE => (Lightweight, s)) |> (fn (poly, (level, (heaviness, core))) => case (core, (poly, level, heaviness)) of - ("simple", (NONE, _, Light)) => Simple_Types level + ("simple", (NONE, _, Lightweight)) => Simple_Types level | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness) | ("tags", (SOME Polymorphic, All_Types, _)) => Tags (Polymorphic, All_Types, heaviness) | ("tags", (SOME Polymorphic, _, _)) => (* The actual light encoding is very unsound. *) - Tags (Polymorphic, level, Heavy) + Tags (Polymorphic, level, Heavyweight) | ("tags", (SOME poly, _, _)) => Tags (poly, level, heaviness) - | ("args", (SOME poly, All_Types (* naja *), Light)) => - Preds (poly, Const_Arg_Types, Light) - | ("erased", (NONE, All_Types (* naja *), Light)) => - Preds (Polymorphic, No_Types, Light) + | ("args", (SOME poly, All_Types (* naja *), Lightweight)) => + Preds (poly, Const_Arg_Types, Lightweight) + | ("erased", (NONE, All_Types (* naja *), Lightweight)) => + Preds (Polymorphic, No_Types, Lightweight) | _ => raise Same.SAME) handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") @@ -561,7 +561,7 @@ | level_of_type_sys (Preds (_, level, _)) = level | level_of_type_sys (Tags (_, level, _)) = level -fun heaviness_of_type_sys (Simple_Types _) = Heavy +fun heaviness_of_type_sys (Simple_Types _) = Heavyweight | heaviness_of_type_sys (Preds (_, _, heaviness)) = heaviness | heaviness_of_type_sys (Tags (_, _, heaviness)) = heaviness @@ -580,7 +580,7 @@ fun choose_format formats (Simple_Types level) = if member (op =) formats THF then (THF, Simple_Types level) else if member (op =) formats TFF then (TFF, Simple_Types level) - else choose_format formats (Preds (Mangled_Monomorphic, level, Heavy)) + else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight)) | choose_format formats type_sys = (case hd formats of CNF_UEQ => @@ -623,9 +623,9 @@ false (* since TFF doesn't support overloading *) | should_drop_arg_type_args type_sys = level_of_type_sys type_sys = All_Types andalso - heaviness_of_type_sys type_sys = Heavy + heaviness_of_type_sys type_sys = Heavyweight -fun general_type_arg_policy (Tags (_, All_Types, Heavy)) = No_Type_Args +fun general_type_arg_policy (Tags (_, All_Types, Heavyweight)) = No_Type_Args | general_type_arg_policy type_sys = if level_of_type_sys type_sys = No_Types then No_Type_Args @@ -983,7 +983,7 @@ fun should_predicate_on_type ctxt nonmono_Ts (Preds (_, level, heaviness)) should_predicate_on_var T = - (heaviness = Heavy orelse should_predicate_on_var ()) andalso + (heaviness = Heavyweight orelse should_predicate_on_var ()) andalso should_encode_type ctxt nonmono_Ts level T | should_predicate_on_type _ _ _ _ _ = false @@ -997,8 +997,8 @@ fun should_tag_with_type _ _ _ Top_Level _ _ = false | should_tag_with_type ctxt nonmono_Ts (Tags (_, level, heaviness)) site u T = (case heaviness of - Heavy => should_encode_type ctxt nonmono_Ts level T - | Light => + Heavyweight => should_encode_type ctxt nonmono_Ts level T + | Lightweight => case (site, is_var_or_bound_var u) of (Eq_Arg, true) => should_encode_type ctxt nonmono_Ts level T | _ => false) @@ -1204,7 +1204,7 @@ if s = const_prefix ^ app_op_name andalso length T_args = 2 andalso not (is_type_sys_virtually_sound type_sys) andalso - heaviness_of_type_sys type_sys = Heavy then + heaviness_of_type_sys type_sys = Heavyweight then T_args |> map (homogenized_type ctxt nonmono_Ts level 0) |> (fn Ts => let val T = hd Ts --> nth Ts 1 in (T --> T, tl Ts) @@ -1560,7 +1560,7 @@ is_tptp_user_symbol s andalso not (String.isPrefix bound_var_prefix s) andalso (case type_sys of Simple_Types _ => true - | Tags (_, _, Light) => true + | Tags (_, _, Lightweight) => true | _ => not pred_sym) fun sym_decl_table_for_facts ctxt type_sys repaired_sym_tab (conjs, facts) = @@ -1745,8 +1745,8 @@ end | Tags (_, _, heaviness) => (case heaviness of - Heavy => [] - | Light => + Heavyweight => [] + | Lightweight => let val n = length decls in (0 upto n - 1 ~~ decls) |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind @@ -1762,7 +1762,7 @@ |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind nonmono_Ts type_sys) -fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavy)) = +fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavyweight)) = level = Nonmonotonic_Types orelse level = Finite_Types | should_add_ti_ti_helper _ = false diff -r a3f3b7a0e99e -r a19826080596 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed Jun 01 10:29:43 2011 +0200 @@ -17,6 +17,8 @@ val trace_msg : Proof.context -> (unit -> string) -> unit val verbose : bool Config.T val verbose_warning : Proof.context -> string -> unit + val hol_term_from_metis : + mode -> int Symtab.table -> Proof.context -> Metis_Term.term -> term val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a val untyped_aconv : term -> term -> bool val replay_one_inference : @@ -244,7 +246,7 @@ |> infer_types ctxt val _ = app (fn t => trace_msg ctxt (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^ - " of type " ^ Syntax.string_of_typ ctxt (type_of t))) + " of type " ^ Syntax.string_of_typ ctxt (type_of t))) ts' in ts' end; diff -r a3f3b7a0e99e -r a19826080596 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Wed Jun 01 10:29:43 2011 +0200 @@ -53,7 +53,7 @@ (*Determining which axiom clauses are actually used*) fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) - | used_axioms _ _ = NONE; + | used_axioms _ _ = NONE val clause_params = {ordering = Metis_KnuthBendixOrder.default, diff -r a3f3b7a0e99e -r a19826080596 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Jun 01 10:29:43 2011 +0200 @@ -310,10 +310,16 @@ |> Metis_Thm.axiom, case try (unprefix conjecture_prefix) ident of SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s))) - | NONE => TrueI) + | NONE => +(* FIXME: missing: + if String.isPrefix helper_prefix then + ... + else +*) + TrueI) | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula" -val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Light) +val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight) (* Function to generate metis clauses, including comb and type clauses *) fun prepare_metis_problem ctxt MX type_sys conj_clauses fact_clauses = diff -r a3f3b7a0e99e -r a19826080596 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jun 01 10:29:43 2011 +0200 @@ -512,7 +512,7 @@ val atp_important_message_keep_quotient = 10 val fallback_best_type_systems = - [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Light)] + [Preds (Mangled_Monomorphic, Nonmonotonic_Types, Lightweight)] fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) = choose_format formats type_sys diff -r a3f3b7a0e99e -r a19826080596 src/HOL/ex/tptp_export.ML --- a/src/HOL/ex/tptp_export.ML Wed Jun 01 10:29:43 2011 +0200 +++ b/src/HOL/ex/tptp_export.ML Wed Jun 01 10:29:43 2011 +0200 @@ -95,7 +95,7 @@ (ATP_Translate.Polymorphic, if full_types then ATP_Translate.All_Types else ATP_Translate.Const_Arg_Types, - ATP_Translate.Heavy) + ATP_Translate.Heavyweight) val path = file_name |> Path.explode val _ = File.write path "" val facts0 = facts_of thy