# HG changeset patch # User bulwahn # Date 1315400320 -7200 # Node ID e0da66339e472045450d41508bba1b57b04221c9 # Parent 7f1f164696a4d981c7a48e577a4c3caf5e2ce631# Parent 3c0741556e197ad7ccc0db4bb87f023b27c61d5d merged diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed Sep 07 14:58:40 2011 +0200 @@ -236,6 +236,12 @@ | string_for_kind Hypothesis = "hypothesis" | string_for_kind Conjecture = "conjecture" +fun string_for_app format func args = + if is_format_thf format then + "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" + else + func ^ "(" ^ commas args ^ ")" + fun flatten_type (ATyAbs (tys, ty)) = ATyAbs (tys, flatten_type ty) | flatten_type (ty as AFun (ty1 as AType _, ty2)) = (case flatten_type ty2 of @@ -247,16 +253,17 @@ | flatten_type _ = raise Fail "unexpected higher-order type in first-order format" -fun str_for_type ty = +fun str_for_type format ty = let fun str _ (AType (s, [])) = s | str _ (AType (s, tys)) = - tys |> map (str false) - |> (if s = tptp_product_type then - space_implode (" " ^ tptp_product_type ^ " ") - #> length tys > 1 ? enclose "(" ")" - else - commas #> enclose "(" ")" #> prefix s) + let val ss = tys |> map (str false) in + if s = tptp_product_type then + ss |> space_implode (" " ^ tptp_product_type ^ " ") + |> length ss > 1 ? enclose "(" ")" + else + string_for_app format s ss + end | str rhs (AFun (ty1, ty2)) = str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2 |> not rhs ? enclose "(" ")" @@ -266,8 +273,8 @@ ss) ^ "]: " ^ str false ty in str true ty end -fun string_for_type (THF _) ty = str_for_type ty - | string_for_type (TFF _) ty = str_for_type (flatten_type ty) +fun string_for_type (format as THF _) ty = str_for_type format ty + | string_for_type (format as TFF _) ty = str_for_type format (flatten_type ty) | string_for_type _ _ = raise Fail "unexpected type in untyped format" fun string_for_quantifier AForall = tptp_forall @@ -293,35 +300,27 @@ fun string_for_term _ (ATerm (s, [])) = s | string_for_term format (ATerm (s, ts)) = - if s = tptp_empty_list then - (* used for lists in the optional "source" field of a derivation *) - "[" ^ commas (map (string_for_term format) ts) ^ "]" - else if is_tptp_equal s then - space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) - |> is_format_thf format ? enclose "(" ")" - else - (case (s = tptp_ho_forall orelse s = tptp_ho_exists, - s = tptp_choice andalso is_format_with_choice format, ts) of - (true, _, [AAbs ((s', ty), tm)]) => - (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever - possible, to work around LEO-II 1.2.8 parser limitation. *) - string_for_formula format - (AQuant (if s = tptp_ho_forall then AForall else AExists, - [(s', SOME ty)], AAtom tm)) - | (_, true, [AAbs ((s', ty), tm)]) => - (* There is code in "ATP_Translate" to ensure that "Eps" is always - applied to an abstraction. *) - tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ - string_for_term format tm ^ "" - |> enclose "(" ")" - - | _ => - let val ss = map (string_for_term format) ts in - if is_format_thf format then - "(" ^ space_implode (" " ^ tptp_app ^ " ") (s :: ss) ^ ")" - else - s ^ "(" ^ commas ss ^ ")" - end) + (if s = tptp_empty_list then + (* used for lists in the optional "source" field of a derivation *) + "[" ^ commas (map (string_for_term format) ts) ^ "]" + else if is_tptp_equal s then + space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) + |> is_format_thf format ? enclose "(" ")" + else case (s = tptp_ho_forall orelse s = tptp_ho_exists, + s = tptp_choice andalso is_format_with_choice format, ts) of + (true, _, [AAbs ((s', ty), tm)]) => + (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever + possible, to work around LEO-II 1.2.8 parser limitation. *) + string_for_formula format + (AQuant (if s = tptp_ho_forall then AForall else AExists, + [(s', SOME ty)], AAtom tm)) + | (_, true, [AAbs ((s', ty), tm)]) => + (* There is code in "ATP_Translate" to ensure that "Eps" is always + applied to an abstraction. *) + tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ + string_for_term format tm ^ "" + |> enclose "(" ")" + | _ => string_for_app format s (map (string_for_term format) ts)) | string_for_term (format as THF _) (AAbs ((s, ty), tm)) = "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ string_for_term format tm ^ ")" diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Sep 07 14:58:40 2011 +0200 @@ -92,9 +92,6 @@ InternalError | UnknownError of string -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" -val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char - fun elide_string threshold s = if size s > threshold then String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ @@ -475,7 +472,7 @@ fun parse_line problem spass_names = parse_tstp_line problem || parse_spass_line spass_names fun parse_proof problem spass_names tstp = - tstp |> strip_spaces_except_between_ident_chars + tstp |> strip_spaces_except_between_idents |> raw_explode |> Scan.finite Symbol.stopper (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 14:58:40 2011 +0200 @@ -152,7 +152,7 @@ union (op =) (resolve_fact facts_offset fact_names name) | add_fact ctxt _ _ (Inference (_, _, deps)) = if AList.defined (op =) deps leo2_ext then - insert (op =) (ext_name ctxt, Extensionality) + insert (op =) (ext_name ctxt, General) else I | add_fact _ _ _ _ = I diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Sep 07 14:58:40 2011 +0200 @@ -403,11 +403,11 @@ prem_kind = Hypothesis, best_slices = K [(1.0, (false, (200, format, type_enc, "")))]} -val pff_format = TFF (TPTP_Polymorphic, TPTP_Implicit) +val pff_format = TFF (TPTP_Polymorphic, TPTP_Explicit) val pff_config = dummy_config pff_format "poly_simple" val pff = (pffN, pff_config) -val phf_format = THF (TPTP_Polymorphic, TPTP_Implicit, THF_With_Choice) +val phf_format = THF (TPTP_Polymorphic, TPTP_Explicit, THF_With_Choice) val phf_config = dummy_config phf_format "poly_simple_higher" val phf = (phfN, phf_config) diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 14:58:40 2011 +0200 @@ -16,24 +16,18 @@ type 'a problem = 'a ATP_Problem.problem datatype locality = - General | Helper | Induction | Extensionality | Intro | Elim | Simp | - Local | Assum | Chained + General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained - datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype soundness = Sound_Modulo_Infiniteness | Sound - datatype uniformity = Uniform | Nonuniform + datatype heaviness = Heavy | Ann_Light | Arg_Light datatype type_level = All_Types | - Noninf_Nonmono_Types of soundness * uniformity | - Fin_Nonmono_Types of uniformity | + Noninf_Nonmono_Types of soundness * heaviness | + Fin_Nonmono_Types of heaviness | Const_Arg_Types | No_Types - - datatype type_enc = - Simple_Types of order * polymorphism * type_level | - Guards of polymorphism * type_level | - Tags of polymorphism * type_level + type type_enc val type_tag_idempotence : bool Config.T val type_tag_arguments : bool Config.T @@ -531,17 +525,16 @@ in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end datatype locality = - General | Helper | Induction | Extensionality | Intro | Elim | Simp | - Local | Assum | Chained + General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic datatype soundness = Sound_Modulo_Infiniteness | Sound -datatype uniformity = Uniform | Nonuniform +datatype heaviness = Heavy | Ann_Light | Arg_Light datatype type_level = All_Types | - Noninf_Nonmono_Types of soundness * uniformity | - Fin_Nonmono_Types of uniformity | + Noninf_Nonmono_Types of soundness * heaviness | + Fin_Nonmono_Types of heaviness | Const_Arg_Types | No_Types @@ -561,9 +554,9 @@ | level_of_type_enc (Guards (_, level)) = level | level_of_type_enc (Tags (_, level)) = level -fun is_level_uniform (Noninf_Nonmono_Types (_, Nonuniform)) = false - | is_level_uniform (Fin_Nonmono_Types Nonuniform) = false - | is_level_uniform _ = true +fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness + | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness + | heaviness_of_level _ = Heavy fun is_type_level_quasi_sound All_Types = true | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true @@ -578,11 +571,25 @@ | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true | is_type_level_monotonicity_based _ = false +(* "_query", "_bang", and "_at" are for the ASCII-challenged Metis and + Mirabelle. *) +val queries = ["?", "_query"] +val bangs = ["!", "_bang"] +val ats = ["@", "_at"] + fun try_unsuffixes ss s = fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE -val queries = ["?", "_query"] -val bangs = ["!", "_bang"] +fun try_nonmono constr suffixes fallback s = + case try_unsuffixes suffixes s of + SOME s => + (case try_unsuffixes suffixes s of + SOME s => (constr Ann_Light, s) + | NONE => + case try_unsuffixes ats s of + SOME s => (constr Arg_Light, s) + | NONE => (constr Heavy, s)) + | NONE => fallback s fun type_enc_from_string soundness s = (case try (unprefix "poly_") s of @@ -594,21 +601,9 @@ case try (unprefix "mono_") s of SOME s => (SOME Mangled_Monomorphic, s) | NONE => (NONE, s)) - ||> (fn s => - (* "_query" and "_bang" are for the ASCII-challenged Metis and - Mirabelle. *) - case try_unsuffixes queries s of - SOME s => - (case try_unsuffixes queries s of - SOME s => (Noninf_Nonmono_Types (soundness, Nonuniform), s) - | NONE => (Noninf_Nonmono_Types (soundness, Uniform), s)) - | NONE => - case try_unsuffixes bangs s of - SOME s => - (case try_unsuffixes bangs s of - SOME s => (Fin_Nonmono_Types Nonuniform, s) - | NONE => (Fin_Nonmono_Types Uniform, s)) - | NONE => (All_Types, s)) + ||> (pair All_Types + |> try_nonmono Fin_Nonmono_Types bangs + |> try_nonmono (curry Noninf_Nonmono_Types soundness) queries) |> (fn (poly, (level, core)) => case (core, (poly, level)) of ("simple", (SOME poly, _)) => @@ -616,7 +611,7 @@ (Polymorphic, All_Types) => Simple_Types (First_Order, Polymorphic, All_Types) | (Mangled_Monomorphic, _) => - if is_level_uniform level then + if heaviness_of_level level = Heavy then Simple_Types (First_Order, Mangled_Monomorphic, level) else raise Same.SAME @@ -627,7 +622,7 @@ Simple_Types (Higher_Order, Polymorphic, All_Types) | (_, Noninf_Nonmono_Types _) => raise Same.SAME | (Mangled_Monomorphic, _) => - if is_level_uniform level then + if heaviness_of_level level = Heavy then Simple_Types (Higher_Order, Mangled_Monomorphic, level) else raise Same.SAME @@ -640,7 +635,7 @@ | ("erased", (NONE, All_Types (* naja *))) => Guards (Polymorphic, No_Types) | _ => raise Same.SAME) - handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".") + handle Same.SAME => error ("Unknown type encoding: " ^ quote s ^ ".") fun adjust_type_enc (THF (TPTP_Monomorphic, _, _)) (Simple_Types (order, _, level)) = @@ -1241,7 +1236,7 @@ | should_encode_type _ _ _ _ = false fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T = - (is_level_uniform level orelse should_guard_var ()) andalso + (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso should_encode_type ctxt mono level T | should_guard_type _ _ _ _ _ = false @@ -1258,7 +1253,7 @@ fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false | should_tag_with_type ctxt mono (Tags (_, level)) site u T = - (if is_level_uniform level then + (if heaviness_of_level level = Heavy then should_encode_type ctxt mono level T else case (site, is_maybe_universal_var u) of (Eq_Arg _, true) => should_encode_type ctxt mono level T @@ -1366,21 +1361,21 @@ K (add_iterm_syms_to_table ctxt explicit_apply) |> formula_fold NONE |> fact_lift -val default_sym_tab_entries : (string * sym_info) list = - (prefixed_predicator_name, - {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) - (* FIXME: needed? *) :: +fun default_sym_tab_entries type_enc = (make_fixed_const NONE @{const_name undefined}, - {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: + {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: ([tptp_false, tptp_true] |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ ([tptp_equal, tptp_old_equal] |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) + |> not (is_type_enc_higher_order type_enc) + ? cons (prefixed_predicator_name, + {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) -fun sym_table_for_facts ctxt explicit_apply facts = +fun sym_table_for_facts ctxt type_enc explicit_apply facts = ((false, []), Symtab.empty) |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd - |> fold Symtab.update default_sym_tab_entries + |> fold Symtab.update (default_sym_tab_entries type_enc) fun min_ary_of sym_tab s = case Symtab.lookup sym_tab s of @@ -1657,7 +1652,8 @@ fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T = - not (is_level_uniform level) andalso should_encode_type ctxt mono level T + heaviness_of_level level <> Heavy andalso + should_encode_type ctxt mono level T | should_generate_tag_bound_decl _ _ _ _ _ = false fun mk_aterm format type_enc name T_args args = @@ -1877,8 +1873,8 @@ ? (fold (add_fact_syms true) conjs #> fold (add_fact_syms false) facts #> (case type_enc of - Simple_Types (_, poly, _) => - if poly = Polymorphic then add_TYPE_const () else I + Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const () + | Simple_Types _ => I | _ => fold add_undefined_const (var_types ()))) end @@ -2131,7 +2127,7 @@ type_enc n s) end | Tags (_, level) => - if is_level_uniform level then + if heaviness_of_level level = Heavy then [] else let val n = length decls in @@ -2209,11 +2205,13 @@ val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) = translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc hyp_ts concl_t facts - val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply + val sym_tab = + conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc val firstorderize = firstorderize_fact thy format type_enc sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize) - val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false) + val sym_tab = + conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false) val helpers = sym_tab |> helper_facts_for_sym_table ctxt format type_enc |> map firstorderize diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_util.ML Wed Sep 07 14:58:40 2011 +0200 @@ -10,6 +10,7 @@ val hash_string : string -> int val hash_term : term -> int val strip_spaces : bool -> (char -> bool) -> string -> string + val strip_spaces_except_between_idents : string -> string val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string @@ -88,6 +89,9 @@ fun strip_spaces skip_comments is_evil = implode o strip_spaces_in_list skip_comments is_evil o String.explode +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" +val strip_spaces_except_between_idents = strip_spaces true is_ident_char + val subscript = implode o map (prefix "\<^isub>") o raw_explode (* FIXME Symbol.explode (?) *) fun nat_subscript n = n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Wed Sep 07 14:58:40 2011 +0200 @@ -59,8 +59,9 @@ ((prefixed_predicator_name, 1), (K metis_predicator, false)), ((prefixed_app_op_name, 2), (K metis_app_op, false)), ((prefixed_type_tag_name, 2), - (fn Tags (_, All_Types) => metis_systematic_type_tag - | _ => metis_ad_hoc_type_tag, true))] + (fn type_enc => + if level_of_type_enc type_enc = All_Types then metis_systematic_type_tag + else metis_ad_hoc_type_tag, true))] fun old_skolem_const_name i j num_T_args = old_skolem_const_prefix ^ Long_Name.separator ^ diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/Nitpick/nitrox.ML --- a/src/HOL/Tools/Nitpick/nitrox.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/Nitpick/nitrox.ML Wed Sep 07 14:58:40 2011 +0200 @@ -21,8 +21,7 @@ exception SYNTAX of string -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" -val tptp_explode = raw_explode o strip_spaces true is_ident_char +val tptp_explode = raw_explode o strip_spaces_except_between_idents fun parse_file_path (c :: ss) = if c = "'" orelse c = "\"" then diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Sep 07 14:58:40 2011 +0200 @@ -144,7 +144,6 @@ (j + 1, ((nth_name j, if member Thm.eq_thm_prop chained_ths th then Chained - else if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality else General), th) :: rest)) |> snd end @@ -576,7 +575,7 @@ | _ => SOME tab in aux (prop_of th) [] end -(* FIXME: This is currently only useful for polymorphic type systems. *) +(* FIXME: This is currently only useful for polymorphic type encodings. *) fun could_benefit_from_ext is_built_in_const facts = fold (consider_arities is_built_in_const o snd) facts (SOME Symtab.empty) |> is_none @@ -845,8 +844,7 @@ else if global then case Termtab.lookup clasimpset_table (prop_of th) of SOME loc => loc - | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality - else General + | NONE => General else if is_assum th then Assum else Local fun is_good_unnamed_local th = not (Thm.has_name_hint th) andalso diff -r 7f1f164696a4 -r e0da66339e47 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 13:51:39 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Sep 07 14:58:40 2011 +0200 @@ -19,6 +19,7 @@ structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = struct +open ATP_Util open ATP_Systems open ATP_Translate open Sledgehammer_Util @@ -151,13 +152,9 @@ error ("Unknown parameter: " ^ quote name ^ ".")) -(* Ensure that type systems such as "mono_simple?" and "mono_guards!!" are - handled correctly. *) -fun implode_param [s, "?"] = s ^ "?" - | implode_param [s, "??"] = s ^ "??" - | implode_param [s, "!"] = s ^ "!" - | implode_param [s, "!!"] = s ^ "!!" - | implode_param ss = space_implode " " ss +(* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are + read correctly. *) +val implode_param = strip_spaces_except_between_idents o space_implode " " structure Data = Theory_Data (