# HG changeset patch # User blanchet # Date 1368632622 -7200 # Node ID f732a674db1be51e3ebab72a4b80c5b81f47be2d # Parent 8dbe623a7804f2c052d315b3dc5262d9bab9f47b renamed Sledgehammer functions with 'for' in their names to 'of' diff -r 8dbe623a7804 -r f732a674db1b src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Wed May 15 17:43:42 2013 +0200 @@ -33,15 +33,15 @@ val fact_name_of = prefix fact_prefix o ascii_of -fun atp_for_format (THF (Polymorphic, _, _, _)) = dummy_thfN - | atp_for_format (THF (Monomorphic, _, _, _)) = satallaxN - | atp_for_format (DFG Polymorphic) = spass_polyN - | atp_for_format (DFG Monomorphic) = spassN - | atp_for_format (TFF (Polymorphic, _)) = alt_ergoN - | atp_for_format (TFF (Monomorphic, _)) = vampireN - | atp_for_format FOF = eN - | atp_for_format CNF_UEQ = waldmeisterN - | atp_for_format CNF = eN +fun atp_of_format (THF (Polymorphic, _, _, _)) = dummy_thfN + | atp_of_format (THF (Monomorphic, _, _, _)) = satallaxN + | atp_of_format (DFG Polymorphic) = spass_polyN + | atp_of_format (DFG Monomorphic) = spassN + | atp_of_format (TFF (Polymorphic, _)) = alt_ergoN + | atp_of_format (TFF (Monomorphic, _)) = vampireN + | atp_of_format FOF = eN + | atp_of_format CNF_UEQ = waldmeisterN + | atp_of_format CNF = eN val atp_timeout = seconds 0.5 @@ -49,11 +49,11 @@ let val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") - val atp = atp_for_format format + val atp = atp_of_format format val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp - val _ = problem |> lines_for_atp_problem format ord (K []) + val _ = problem |> lines_of_atp_problem format ord (K []) |> File.write_list prob_file val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = @@ -70,7 +70,7 @@ tracing ("Ran ATP: " ^ (case outcome of NONE => "Success" - | SOME failure => string_for_failure failure)) + | SOME failure => string_of_failure failure)) in outcome end fun is_problem_line_reprovable ctxt format prelude axioms deps @@ -138,22 +138,22 @@ [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}, @{typ bool}, @{typ unit}] -fun ground_type_for_tvar _ [] tvar = - raise TYPE ("ground_type_for_sorts", [TVar tvar], []) - | ground_type_for_tvar thy (T :: Ts) tvar = +fun ground_type_of_tvar _ [] tvar = + raise TYPE ("ground_type_of_tvar", [TVar tvar], []) + | ground_type_of_tvar thy (T :: Ts) tvar = if can (Sign.typ_match thy (TVar tvar, T)) Vartab.empty then T - else ground_type_for_tvar thy Ts tvar + else ground_type_of_tvar thy Ts tvar fun monomorphize_term ctxt t = let val thy = Proof_Context.theory_of ctxt in - t |> map_types (map_type_tvar (ground_type_for_tvar thy ground_types)) + t |> map_types (map_type_tvar (ground_type_of_tvar thy ground_types)) handle TYPE _ => @{prop True} end fun heading_sort_key heading = if String.isPrefix "Relevant fact" heading then "_" ^ heading else heading -fun problem_for_theory ctxt thy format infer_policy type_enc = +fun problem_of_theory ctxt thy format infer_policy type_enc = let val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt val type_enc = @@ -214,8 +214,8 @@ |> order_problem_facts name_ord end -fun lines_for_problem ctxt format = - lines_for_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K []) +fun lines_of_problem ctxt format = + lines_of_atp_problem format (effective_term_order ctxt eN (* dummy *)) (K []) fun write_lines path ss = let @@ -226,8 +226,8 @@ fun generate_atp_inference_file_for_theory ctxt thy format infer_policy type_enc file_name = let - val problem = problem_for_theory ctxt thy format infer_policy type_enc - val ss = lines_for_problem ctxt format problem + val problem = problem_of_theory ctxt thy format infer_policy type_enc + val ss = lines_of_problem ctxt format problem in write_lines (Path.explode file_name) ss end fun ap dir = Path.append dir o Path.explode @@ -296,20 +296,20 @@ val include_dir = ap problem_dir include_name val _ = Isabelle_System.mkdir include_dir val (prelude, groups) = - problem_for_theory ctxt thy format infer_policy type_enc + problem_of_theory ctxt thy format infer_policy type_enc |> split_last ||> (snd #> chop_maximal_groups (op = o pairself theory_name_of_fact) #> map (`(include_base_name_of_fact o hd))) fun write_prelude () = - let val ss = lines_for_problem ctxt format prelude in + let val ss = lines_of_problem ctxt format prelude in File.append file_order_path (prelude_base_name ^ "\n"); write_lines (ap include_dir prelude_name) ss end fun write_include_file (base_name, facts) = let val name = base_name ^ include_suffix - val ss = lines_for_problem ctxt format [(factsN, facts)] + val ss = lines_of_problem ctxt format [(factsN, facts)] in File.append file_order_path (base_name ^ "\n"); write_lines (ap include_dir name) ss @@ -321,7 +321,7 @@ write_problem_files n (includes @ [include_line base_name]) [] groups | write_problem_files n includes seen ((base_name, fact :: facts) :: groups) = - let val fact_s = tptp_string_for_line format fact in + let val fact_s = tptp_string_of_line format fact in (if should_generate_problem thy base_name fact then let val (name, conj) = @@ -329,7 +329,7 @@ Formula ((ident, alt), _, phi, _, _) => (problem_name_of base_name n (encode_meta alt), Formula ((ident, alt), Conjecture, phi, NONE, []))) - val conj_s = tptp_string_for_line format conj + val conj_s = tptp_string_of_line format conj in File.append problem_order_path (name ^ "\n"); write_lines (ap problem_dir name) (seen @ [conj_s]) diff -r 8dbe623a7804 -r f732a674db1b src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Wed May 15 17:43:42 2013 +0200 @@ -31,7 +31,7 @@ default_params ctxt override_params val name = hd provers val prover = get_prover ctxt mode name - val default_max_facts = default_max_facts_for_prover ctxt slice name + val default_max_facts = default_max_facts_of_prover ctxt slice name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i val ho_atp = exists (is_ho_atp ctxt) provers val reserved = reserved_isar_keyword_table () diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Wed May 15 17:43:42 2013 +0200 @@ -126,8 +126,8 @@ val formula_map : ('c -> 'e) -> ('a, 'b, 'c, 'd) formula -> ('a, 'b, 'e, 'd) formula val is_format_higher_order : atp_format -> bool - val tptp_string_for_line : atp_format -> string problem_line -> string - val lines_for_atp_problem : + val tptp_string_of_line : atp_format -> string problem_line -> string + val lines_of_atp_problem : atp_format -> term_order -> (unit -> (string * int) list) -> string problem -> string list val ensure_cnf_problem : @@ -331,17 +331,17 @@ | is_format_typed (DFG _) = true | is_format_typed _ = false -fun tptp_string_for_role Axiom = "axiom" - | tptp_string_for_role Definition = "definition" - | tptp_string_for_role Lemma = "lemma" - | tptp_string_for_role Hypothesis = "hypothesis" - | tptp_string_for_role Conjecture = "conjecture" - | tptp_string_for_role Negated_Conjecture = "negated_conjecture" - | tptp_string_for_role Plain = "plain" - | tptp_string_for_role Unknown = "unknown" +fun tptp_string_of_role Axiom = "axiom" + | tptp_string_of_role Definition = "definition" + | tptp_string_of_role Lemma = "lemma" + | tptp_string_of_role Hypothesis = "hypothesis" + | tptp_string_of_role Conjecture = "conjecture" + | tptp_string_of_role Negated_Conjecture = "negated_conjecture" + | tptp_string_of_role Plain = "plain" + | tptp_string_of_role Unknown = "unknown" -fun tptp_string_for_app _ func [] = func - | tptp_string_for_app format func args = +fun tptp_string_of_app _ func [] = func + | tptp_string_of_app format func args = if is_format_higher_order format then "(" ^ space_implode (" " ^ tptp_app ^ " ") (func :: args) ^ ")" else @@ -363,7 +363,7 @@ val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types) -fun str_for_type format ty = +fun str_of_type format ty = let val dfg = case format of DFG _ => true | _ => false fun str _ (AType (s, [])) = @@ -375,7 +375,7 @@ (if dfg then ", " else " " ^ tptp_product_type ^ " ") |> (not dfg andalso length ss > 1) ? enclose "(" ")" else - tptp_string_for_app format s ss + tptp_string_of_app format s ss end | str rhs (AFun (ty1, ty2)) = (str false ty1 |> dfg ? enclose "(" ")") ^ " " ^ @@ -389,96 +389,96 @@ str false ty in str true ty end -fun string_for_type (format as THF _) ty = str_for_type format ty - | string_for_type format ty = str_for_type format (flatten_type ty) +fun string_of_type (format as THF _) ty = str_of_type format ty + | string_of_type format ty = str_of_type format (flatten_type ty) -fun tptp_string_for_quantifier AForall = tptp_forall - | tptp_string_for_quantifier AExists = tptp_exists +fun tptp_string_of_quantifier AForall = tptp_forall + | tptp_string_of_quantifier AExists = tptp_exists -fun tptp_string_for_connective ANot = tptp_not - | tptp_string_for_connective AAnd = tptp_and - | tptp_string_for_connective AOr = tptp_or - | tptp_string_for_connective AImplies = tptp_implies - | tptp_string_for_connective AIff = tptp_iff +fun tptp_string_of_connective ANot = tptp_not + | tptp_string_of_connective AAnd = tptp_and + | tptp_string_of_connective AOr = tptp_or + | tptp_string_of_connective AImplies = tptp_implies + | tptp_string_of_connective AIff = tptp_iff -fun string_for_bound_var format (s, ty) = +fun string_of_bound_var format (s, ty) = s ^ (if is_format_typed format then " " ^ tptp_has_type ^ " " ^ (ty |> the_default (AType (tptp_individual_type, [])) - |> string_for_type format) + |> string_of_type format) else "") -fun tptp_string_for_term _ (ATerm ((s, []), [])) = s - | tptp_string_for_term format (ATerm ((s, tys), ts)) = +fun tptp_string_of_term _ (ATerm ((s, []), [])) = s + | tptp_string_of_term format (ATerm ((s, tys), ts)) = (if s = tptp_empty_list then (* used for lists in the optional "source" field of a derivation *) - "[" ^ commas (map (tptp_string_for_term format) ts) ^ "]" + "[" ^ commas (map (tptp_string_of_term format) ts) ^ "]" else if is_tptp_equal s then space_implode (" " ^ tptp_equal ^ " ") - (map (tptp_string_for_term format) ts) + (map (tptp_string_of_term format) ts) |> is_format_higher_order format ? enclose "(" ")" else case (s = tptp_ho_forall orelse s = tptp_ho_exists, s = tptp_choice, 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. *) - tptp_string_for_formula format + tptp_string_of_formula format (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) | (_, true, [AAbs (((s', ty), tm), args)]) => (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an abstraction. *) - tptp_string_for_app format - (tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ - tptp_string_for_term format tm ^ "" + tptp_string_of_app format + (tptp_choice ^ "[" ^ s' ^ " : " ^ string_of_type format ty ^ "]: " ^ + tptp_string_of_term format tm ^ "" |> enclose "(" ")") - (map (tptp_string_for_term format) args) + (map (tptp_string_of_term format) args) | _ => - tptp_string_for_app format s - (map (string_for_type format) tys - @ map (tptp_string_for_term format) ts)) - | tptp_string_for_term (format as THF _) (AAbs (((s, ty), tm), args)) = - tptp_string_for_app format - ("(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ - tptp_string_for_term format tm ^ ")") - (map (tptp_string_for_term format) args) - | tptp_string_for_term _ _ = + tptp_string_of_app format s + (map (string_of_type format) tys + @ map (tptp_string_of_term format) ts)) + | tptp_string_of_term (format as THF _) (AAbs (((s, ty), tm), args)) = + tptp_string_of_app format + ("(^[" ^ s ^ " : " ^ string_of_type format ty ^ "]: " ^ + tptp_string_of_term format tm ^ ")") + (map (tptp_string_of_term format) args) + | tptp_string_of_term _ _ = raise Fail "unexpected term in first-order format" -and tptp_string_for_formula format (ATyQuant (q, xs, phi)) = - tptp_string_for_quantifier q ^ +and tptp_string_of_formula format (ATyQuant (q, xs, phi)) = + tptp_string_of_quantifier q ^ "[" ^ - commas (map (suffix_type_of_types o string_for_type format o fst) xs) ^ - "]: " ^ tptp_string_for_formula format phi + commas (map (suffix_type_of_types o string_of_type format o fst) xs) ^ + "]: " ^ tptp_string_of_formula format phi |> enclose "(" ")" - | tptp_string_for_formula format (AQuant (q, xs, phi)) = - tptp_string_for_quantifier q ^ - "[" ^ commas (map (string_for_bound_var format) xs) ^ "]: " ^ - tptp_string_for_formula format phi + | tptp_string_of_formula format (AQuant (q, xs, phi)) = + tptp_string_of_quantifier q ^ + "[" ^ commas (map (string_of_bound_var format) xs) ^ "]: " ^ + tptp_string_of_formula format phi |> enclose "(" ")" - | tptp_string_for_formula format + | tptp_string_of_formula format (AConn (ANot, [AAtom (ATerm (("=" (* tptp_equal *), []), ts))])) = space_implode (" " ^ tptp_not_infix ^ tptp_equal ^ " ") - (map (tptp_string_for_term format) ts) + (map (tptp_string_of_term format) ts) |> is_format_higher_order format ? enclose "(" ")" - | tptp_string_for_formula format (AConn (c, [phi])) = - tptp_string_for_connective c ^ " " ^ - (tptp_string_for_formula format phi + | tptp_string_of_formula format (AConn (c, [phi])) = + tptp_string_of_connective c ^ " " ^ + (tptp_string_of_formula format phi |> is_format_higher_order format ? enclose "(" ")") |> enclose "(" ")" - | tptp_string_for_formula format (AConn (c, phis)) = - space_implode (" " ^ tptp_string_for_connective c ^ " ") - (map (tptp_string_for_formula format) phis) + | tptp_string_of_formula format (AConn (c, phis)) = + space_implode (" " ^ tptp_string_of_connective c ^ " ") + (map (tptp_string_of_formula format) phis) |> enclose "(" ")" - | tptp_string_for_formula format (AAtom tm) = tptp_string_for_term format tm + | tptp_string_of_formula format (AAtom tm) = tptp_string_of_term format tm -fun tptp_string_for_format CNF = tptp_cnf - | tptp_string_for_format CNF_UEQ = tptp_cnf - | tptp_string_for_format FOF = tptp_fof - | tptp_string_for_format (TFF _) = tptp_tff - | tptp_string_for_format (THF _) = tptp_thf - | tptp_string_for_format (DFG _) = raise Fail "non-TPTP format" +fun tptp_string_of_format CNF = tptp_cnf + | tptp_string_of_format CNF_UEQ = tptp_cnf + | tptp_string_of_format FOF = tptp_fof + | tptp_string_of_format (TFF _) = tptp_tff + | tptp_string_of_format (THF _) = tptp_thf + | tptp_string_of_format (DFG _) = raise Fail "non-TPTP format" val atype_of_types = AType (tptp_type_of_types, []) @@ -487,24 +487,24 @@ fun maybe_alt "" = "" | maybe_alt s = " % " ^ s -fun tptp_string_for_line format (Type_Decl (ident, ty, ary)) = - tptp_string_for_line format (Sym_Decl (ident, ty, nary_type_decl_type ary)) - | tptp_string_for_line format (Sym_Decl (ident, sym, ty)) = - tptp_string_for_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ - " : " ^ string_for_type format ty ^ ").\n" - | tptp_string_for_line format (Formula ((ident, alt), kind, phi, source, _)) = - tptp_string_for_format format ^ "(" ^ ident ^ ", " ^ - tptp_string_for_role kind ^ "," ^ maybe_alt alt ^ - "\n (" ^ tptp_string_for_formula format phi ^ ")" ^ +fun tptp_string_of_line format (Type_Decl (ident, ty, ary)) = + tptp_string_of_line format (Sym_Decl (ident, ty, nary_type_decl_type ary)) + | tptp_string_of_line format (Sym_Decl (ident, sym, ty)) = + tptp_string_of_format format ^ "(" ^ ident ^ ", type,\n " ^ sym ^ + " : " ^ string_of_type format ty ^ ").\n" + | tptp_string_of_line format (Formula ((ident, alt), kind, phi, source, _)) = + tptp_string_of_format format ^ "(" ^ ident ^ ", " ^ + tptp_string_of_role kind ^ "," ^ maybe_alt alt ^ + "\n (" ^ tptp_string_of_formula format phi ^ ")" ^ (case source of - SOME tm => ", " ^ tptp_string_for_term format tm + SOME tm => ", " ^ tptp_string_of_term format tm | NONE => "") ^ ").\n" fun tptp_lines format = maps (fn (_, []) => [] | (heading, lines) => "\n% " ^ heading ^ " (" ^ string_of_int (length lines) ^ ")\n" :: - map (tptp_string_for_line format) lines) + map (tptp_string_of_line format) lines) fun arity_of_type (APi (tys, ty)) = arity_of_type ty |>> Integer.add (length tys) @@ -516,20 +516,19 @@ val dfg_class_inter = space_implode " & " -fun dfg_string_for_term (ATerm ((s, tys), tms)) = +fun dfg_string_of_term (ATerm ((s, tys), tms)) = s ^ (if null tys then "" - else "<" ^ commas (map (string_for_type (DFG Polymorphic)) tys) ^ ">") ^ + else "<" ^ commas (map (string_of_type (DFG Polymorphic)) tys) ^ ">") ^ (if null tms then "" - else "(" ^ commas (map dfg_string_for_term tms) ^ ")") - | dfg_string_for_term _ = raise Fail "unexpected atom in first-order format" + else "(" ^ commas (map dfg_string_of_term tms) ^ ")") + | dfg_string_of_term _ = raise Fail "unexpected atom in first-order format" -fun dfg_string_for_formula poly gen_simp info = +fun dfg_string_of_formula poly gen_simp info = let - val str_for_typ = string_for_type (DFG poly) - fun str_for_bound_typ (ty, []) = str_for_typ ty - | str_for_bound_typ (ty, cls) = - str_for_typ ty ^ " : " ^ dfg_class_inter cls + val str_of_typ = string_of_type (DFG poly) + fun str_of_bound_typ (ty, []) = str_of_typ ty + | str_of_bound_typ (ty, cls) = str_of_typ ty ^ " : " ^ dfg_class_inter cls fun suffix_tag top_level s = if top_level then case extract_isabelle_status info of @@ -543,42 +542,42 @@ | NONE => s else s - fun str_for_atom top_level (ATerm ((s, tys), tms)) = + fun str_of_atom top_level (ATerm ((s, tys), tms)) = let val s' = if is_tptp_equal s then "equal" |> suffix_tag top_level else if s = tptp_true then "true" else if s = tptp_false then "false" else s - in dfg_string_for_term (ATerm ((s', tys), tms)) end - | str_for_atom _ _ = raise Fail "unexpected atom in first-order format" - fun str_for_quant AForall = "forall" - | str_for_quant AExists = "exists" - fun str_for_conn _ ANot = "not" - | str_for_conn _ AAnd = "and" - | str_for_conn _ AOr = "or" - | str_for_conn _ AImplies = "implies" - | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level - fun str_for_formula top_level (ATyQuant (q, xs, phi)) = - str_for_quant q ^ "_sorts([" ^ commas (map str_for_bound_typ xs) ^ - "], " ^ str_for_formula top_level phi ^ ")" - | str_for_formula top_level (AQuant (q, xs, phi)) = - str_for_quant q ^ "([" ^ - commas (map (string_for_bound_var (DFG poly)) xs) ^ "], " ^ - str_for_formula top_level phi ^ ")" - | str_for_formula top_level (AConn (c, phis)) = - str_for_conn top_level c ^ "(" ^ - commas (map (str_for_formula false) phis) ^ ")" - | str_for_formula top_level (AAtom tm) = str_for_atom top_level tm - in str_for_formula true end + in dfg_string_of_term (ATerm ((s', tys), tms)) end + | str_of_atom _ _ = raise Fail "unexpected atom in first-order format" + fun str_of_quant AForall = "forall" + | str_of_quant AExists = "exists" + fun str_of_conn _ ANot = "not" + | str_of_conn _ AAnd = "and" + | str_of_conn _ AOr = "or" + | str_of_conn _ AImplies = "implies" + | str_of_conn top_level AIff = "equiv" |> suffix_tag top_level + fun str_of_formula top_level (ATyQuant (q, xs, phi)) = + str_of_quant q ^ "_sorts([" ^ commas (map str_of_bound_typ xs) ^ "], " ^ + str_of_formula top_level phi ^ ")" + | str_of_formula top_level (AQuant (q, xs, phi)) = + str_of_quant q ^ "([" ^ + commas (map (string_of_bound_var (DFG poly)) xs) ^ "], " ^ + str_of_formula top_level phi ^ ")" + | str_of_formula top_level (AConn (c, phis)) = + str_of_conn top_level c ^ "(" ^ + commas (map (str_of_formula false) phis) ^ ")" + | str_of_formula top_level (AAtom tm) = str_of_atom top_level tm + in str_of_formula true end fun maybe_enclose bef aft "" = "% " ^ bef ^ aft | maybe_enclose bef aft s = bef ^ s ^ aft fun dfg_lines poly {is_lpo, gen_weights, gen_prec, gen_simp} ord_info problem = let - val typ = string_for_type (DFG poly) - val term = dfg_string_for_term + val typ = string_of_type (DFG poly) + val term = dfg_string_of_term fun spair (s, s') = "(" ^ s ^ ", " ^ s' ^ ")" fun tm_ary sym ty = spair (sym, string_of_arity (arity_of_type ty)) fun ty_ary 0 ty = ty @@ -602,7 +601,7 @@ fun formula pred (Formula ((ident, alt), kind, phi, _, info)) = if pred kind then let val rank = extract_isabelle_rank info in - "formula(" ^ dfg_string_for_formula poly gen_simp info phi ^ + "formula(" ^ dfg_string_of_formula poly gen_simp info phi ^ ", " ^ ident ^ (if rank = default_rank then "" else ", " ^ string_of_int rank) ^ ")." ^ maybe_alt alt @@ -684,7 +683,7 @@ ["end_problem.\n"] end -fun lines_for_atp_problem format ord ord_info problem = +fun lines_of_atp_problem format ord ord_info problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: (case format of diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed May 15 17:43:42 2013 +0200 @@ -918,7 +918,7 @@ fun ho_term_from_ho_type (AType (name, tys)) = ATerm ((name, []), map ho_term_from_ho_type tys) | ho_term_from_ho_type _ = raise Fail "unexpected type" -fun ho_type_for_type_arg type_enc T = +fun ho_type_of_type_arg type_enc T = if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T) (* This shouldn't clash with anything else. *) @@ -982,7 +982,7 @@ (map (native_ho_type_from_typ type_enc false 0) T_args, []) else ([], map_filter (Option.map ho_term_from_ho_type - o ho_type_for_type_arg type_enc) T_args) + o ho_type_of_type_arg type_enc) T_args) fun class_atom type_enc (cl, T) = let @@ -999,7 +999,7 @@ fun class_atoms type_enc (cls, T) = map (fn cl => class_atom type_enc (cl, T)) cls -fun class_membs_for_types type_enc add_sorts_on_typ Ts = +fun class_membs_of_types type_enc add_sorts_on_typ Ts = [] |> (polymorphism_of_type_enc type_enc <> Type_Class_Polymorphic andalso level_of_type_enc type_enc <> No_Types) ? fold add_sorts_on_typ Ts @@ -1065,7 +1065,7 @@ ty_args "" in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end fun mangled_const_name type_enc = - map_filter (ho_type_for_type_arg type_enc) + map_filter (ho_type_of_type_arg type_enc) #> raw_mangled_const_name generic_mangled_type_name val parse_mangled_ident = @@ -1579,7 +1579,7 @@ end in add_iterm_syms end -fun sym_table_for_facts ctxt type_enc app_op_level conjs facts = +fun sym_table_of_facts ctxt type_enc app_op_level conjs facts = let fun add_iterm_syms conj_fact = add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true @@ -1773,7 +1773,7 @@ case filter is_TVar Ts of [] => I | Ts => - (sorts ? mk_ahorn (Ts |> class_membs_for_types type_enc add_sorts_on_tvar + (sorts ? mk_ahorn (Ts |> class_membs_of_types type_enc add_sorts_on_tvar |> map (class_atom type_enc))) #> (case type_enc of Native (_, poly, _) => @@ -1809,8 +1809,8 @@ could_specialize_helpers type_enc andalso not (null (Term.hidden_polymorphism t)) -fun add_helper_facts_for_sym ctxt format type_enc completish - (s, {types, ...} : sym_info) = +fun add_helper_facts_of_sym ctxt format type_enc completish + (s, {types, ...} : sym_info) = case unprefix_and_unascii const_prefix s of SOME mangled_s => let @@ -1852,8 +1852,8 @@ (if completish then completish_helper_table else helper_table) end | NONE => I -fun helper_facts_for_sym_table ctxt format type_enc completish sym_tab = - Symtab.fold_rev (add_helper_facts_for_sym ctxt format type_enc completish) +fun helper_facts_of_sym_table ctxt format type_enc completish sym_tab = + Symtab.fold_rev (add_helper_facts_of_sym ctxt format type_enc completish) sym_tab [] (***************************************************************) @@ -2152,7 +2152,7 @@ (* Each fact is given a unique fact number to avoid name clashes (e.g., because of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) -fun line_for_fact ctxt prefix encode alt freshen pos mono type_enc rank +fun line_of_fact ctxt prefix encode alt freshen pos mono type_enc rank (j, {name, stature = (_, status), role, iformula, atomic_types}) = Formula ((prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, alt name), @@ -2164,21 +2164,21 @@ |> bound_tvars type_enc true atomic_types, NONE, isabelle_info (string_of_status status) (rank j)) -fun lines_for_subclass type_enc sub super = +fun lines_of_subclass type_enc sub super = Formula ((subclass_prefix ^ ascii_of sub ^ "___" ^ ascii_of super, ""), Axiom, AConn (AImplies, [sub, super] |> map (fn s => class_atom type_enc (s, tvar_a))) |> bound_tvars type_enc false [tvar_a], NONE, isabelle_info inductiveN helper_rank) -fun lines_for_subclass_pair type_enc (sub, supers) = +fun lines_of_subclass_pair type_enc (sub, supers) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then [Class_Decl (class_decl_prefix ^ ascii_of sub, `make_class sub, map (`make_class) supers)] else - map (lines_for_subclass type_enc sub) supers + map (lines_of_subclass type_enc sub) supers -fun line_for_tcon_clause type_enc (name, prems, (cl, T)) = +fun line_of_tcon_clause type_enc (name, prems, (cl, T)) = if polymorphism_of_type_enc type_enc = Type_Class_Polymorphic then Class_Memb (class_memb_prefix ^ name, map (fn (cls, T) => @@ -2192,8 +2192,8 @@ |> bound_tvars type_enc true (snd (dest_Type T)), NONE, isabelle_info inductiveN helper_rank) -fun line_for_conjecture ctxt mono type_enc - ({name, role, iformula, atomic_types, ...} : ifact) = +fun line_of_conjecture ctxt mono type_enc + ({name, role, iformula, atomic_types, ...} : ifact) = Formula ((conjecture_prefix ^ name, ""), role, iformula |> formula_from_iformula ctxt mono type_enc @@ -2201,7 +2201,7 @@ |> close_formula_universally |> bound_tvars type_enc true atomic_types, NONE, []) -fun lines_for_free_types type_enc (facts : ifact list) = +fun lines_of_free_types type_enc (facts : ifact list) = if is_type_enc_polymorphic type_enc then let val type_classes = @@ -2216,14 +2216,14 @@ class_atom type_enc (cl, T), NONE, []) val membs = fold (union (op =)) (map #atomic_types facts) [] - |> class_membs_for_types type_enc add_sorts_on_tfree + |> class_membs_of_types type_enc add_sorts_on_tfree in map2 line (0 upto length membs - 1) membs end else [] (** Symbol declarations **) -fun decl_line_for_class phantoms s = +fun decl_line_of_class phantoms s = let val name as (s, _) = `make_class s in Sym_Decl (sym_decl_prefix ^ s, name, APi ([tvar_a_name], @@ -2233,13 +2233,13 @@ bool_atype)) end -fun decl_lines_for_classes type_enc classes = +fun decl_lines_of_classes type_enc = case type_enc of Native (_, Raw_Polymorphic phantoms, _) => - map (decl_line_for_class phantoms) classes - | _ => [] + map (decl_line_of_class phantoms) + | _ => K [] -fun sym_decl_table_for_facts thy type_enc sym_tab (conjs, facts, extra_tms) = +fun sym_decl_table_of_facts thy type_enc sym_tab (conjs, facts, extra_tms) = let fun add_iterm_syms tm = let val (head, args) = strip_iterm_comb tm in @@ -2346,7 +2346,7 @@ fun add_fact_mononotonicity_info ctxt level ({role, iformula, ...} : ifact) = formula_fold (SOME (role <> Conjecture)) (add_iterm_mononotonicity_info ctxt level) iformula -fun mononotonicity_info_for_facts ctxt type_enc completish facts = +fun mononotonicity_info_of_facts ctxt type_enc completish facts = let val level = level_of_type_enc type_enc in default_mono level completish |> is_type_level_monotonicity_based level @@ -2367,14 +2367,14 @@ fun add_fact_monotonic_types ctxt mono type_enc = ifact_lift (add_iformula_monotonic_types ctxt mono type_enc) -fun monotonic_types_for_facts ctxt mono type_enc facts = +fun monotonic_types_of_facts ctxt mono type_enc facts = let val level = level_of_type_enc type_enc in [] |> (is_type_enc_polymorphic type_enc andalso is_type_level_monotonicity_based level) ? fold (add_fact_monotonic_types ctxt mono type_enc) facts end -fun line_for_guards_mono_type ctxt mono type_enc T = +fun line_of_guards_mono_type ctxt mono type_enc T = Formula ((guards_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, IConst (`make_bound_var "X", T, []) @@ -2386,7 +2386,7 @@ |> bound_tvars type_enc true (atomic_types_of T), NONE, isabelle_info inductiveN helper_rank) -fun line_for_tags_mono_type ctxt mono type_enc T = +fun line_of_tags_mono_type ctxt mono type_enc T = let val x_var = ATerm ((`make_bound_var "X", []), []) in Formula ((tags_sym_formula_prefix ^ ascii_of (mangled_type type_enc T), ""), Axiom, @@ -2395,14 +2395,13 @@ NONE, isabelle_info non_rec_defN helper_rank) end -fun lines_for_mono_types ctxt mono type_enc Ts = +fun lines_of_mono_types ctxt mono type_enc = case type_enc of - Native _ => [] - | Guards _ => map (line_for_guards_mono_type ctxt mono type_enc) Ts - | Tags _ => map (line_for_tags_mono_type ctxt mono type_enc) Ts + Native _ => K [] + | Guards _ => map (line_of_guards_mono_type ctxt mono type_enc) + | Tags _ => map (line_of_tags_mono_type ctxt mono type_enc) -fun decl_line_for_sym ctxt mono type_enc s - (s', T_args, T, pred_sym, ary, _) = +fun decl_line_of_sym ctxt mono type_enc s (s', T_args, T, pred_sym, ary, _) = let val thy = Proof_Context.theory_of ctxt val (T, T_args) = @@ -2425,8 +2424,8 @@ fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I) -fun line_for_guards_sym_decl ctxt mono type_enc n s j - (s', T_args, T, _, ary, in_conj) = +fun line_of_guards_sym_decl ctxt mono type_enc n s j + (s', T_args, T, _, ary, in_conj) = let val thy = Proof_Context.theory_of ctxt val (role, maybe_negate) = honor_conj_sym_role in_conj @@ -2459,8 +2458,8 @@ NONE, isabelle_info inductiveN helper_rank) end -fun lines_for_tags_sym_decl ctxt mono type_enc n s - (j, (s', T_args, T, pred_sym, ary, in_conj)) = +fun lines_of_tags_sym_decl ctxt mono type_enc n s + (j, (s', T_args, T, pred_sym, ary, in_conj)) = let val thy = Proof_Context.theory_of ctxt val level = level_of_type_enc type_enc @@ -2504,9 +2503,9 @@ end | rationalize_decls _ decls = decls -fun lines_for_sym_decls ctxt mono type_enc (s, decls) = +fun lines_of_sym_decls ctxt mono type_enc (s, decls) = case type_enc of - Native _ => [decl_line_for_sym ctxt mono type_enc s (hd decls)] + Native _ => [decl_line_of_sym ctxt mono type_enc s (hd decls)] | Guards (_, level) => let val thy = Proof_Context.theory_of ctxt @@ -2517,7 +2516,7 @@ o result_type_of_decl) in (0 upto length decls - 1, decls) - |-> map2 (line_for_guards_sym_decl ctxt mono type_enc n s) + |-> map2 (line_of_guards_sym_decl ctxt mono type_enc n s) end | Tags (_, level) => if is_type_level_uniform level then @@ -2525,20 +2524,20 @@ else let val n = length decls in (0 upto n - 1 ~~ decls) - |> maps (lines_for_tags_sym_decl ctxt mono type_enc n s) + |> maps (lines_of_tags_sym_decl ctxt mono type_enc n s) end -fun lines_for_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab = +fun lines_of_sym_decl_table ctxt mono type_enc mono_Ts sym_decl_tab = let val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst - val mono_lines = lines_for_mono_types ctxt mono type_enc mono_Ts - val decl_lines = maps (lines_for_sym_decls ctxt mono type_enc) syms + val mono_lines = lines_of_mono_types ctxt mono type_enc mono_Ts + val decl_lines = maps (lines_of_sym_decls ctxt mono type_enc) syms in mono_lines @ decl_lines end fun pair_append (xs1, xs2) (ys1, ys2) = (xs1 @ ys1, xs2 @ ys2) -fun do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 sym_tab - base_s0 types in_conj = +fun do_uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 sym_tab + base_s0 types in_conj = let fun do_alias ary = let @@ -2582,7 +2581,7 @@ else pair_append (do_alias (ary - 1))) end in do_alias end -fun uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 +fun uncurried_alias_lines_of_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 => @@ -2590,20 +2589,20 @@ let val base_s0 = mangled_s |> unmangled_invert_const in - do_uncurried_alias_lines_for_sym ctxt constrs mono type_enc sym_tab0 - sym_tab base_s0 types in_conj min_ary + do_uncurried_alias_lines_of_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 constrs mono type_enc - uncurried_aliases sym_tab0 sym_tab = +fun uncurried_alias_lines_of_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 constrs mono type_enc sym_tab0 - sym_tab) sym_tab + o uncurried_alias_lines_of_sym ctxt constrs mono type_enc sym_tab0 + sym_tab) sym_tab val implicit_declsN = "Should-be-implicit typings" val explicit_declsN = "Explicit typings" @@ -2725,46 +2724,46 @@ translate_formulas ctxt prem_role format type_enc lam_trans preproc hyp_ts concl_t facts val (_, sym_tab0) = - sym_table_for_facts ctxt type_enc app_op_level conjs facts + sym_table_of_facts ctxt type_enc app_op_level conjs facts val mono = - conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc completish + conjs @ facts |> mononotonicity_info_of_facts ctxt type_enc completish val constrs = all_constrs_of_polymorphic_datatypes thy fun firstorderize in_helper = firstorderize_fact thy constrs 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_for_facts ctxt type_enc Min_App_Op conjs facts + sym_table_of_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 constrs mono type_enc - uncurried_aliases sym_tab0 sym_tab + uncurried_alias_lines_of_sym_table ctxt constrs mono type_enc + uncurried_aliases sym_tab0 sym_tab val (_, sym_tab) = (ho_stuff, sym_tab) |> fold (add_iterm_syms_to_sym_table ctxt Min_App_Op false false) uncurried_alias_eq_tms val helpers = - sym_tab |> helper_facts_for_sym_table ctxt format type_enc completish + sym_tab |> helper_facts_of_sym_table ctxt format type_enc completish |> map (firstorderize true) val mono_Ts = - helpers @ conjs @ facts |> monotonic_types_for_facts ctxt mono type_enc - val class_decl_lines = decl_lines_for_classes type_enc classes + helpers @ conjs @ facts |> monotonic_types_of_facts ctxt mono type_enc + val class_decl_lines = decl_lines_of_classes type_enc classes val sym_decl_lines = (conjs, helpers @ facts, uncurried_alias_eq_tms) - |> sym_decl_table_for_facts thy type_enc sym_tab - |> lines_for_sym_decl_table ctxt mono type_enc mono_Ts + |> sym_decl_table_of_facts thy type_enc sym_tab + |> lines_of_sym_decl_table ctxt mono type_enc mono_Ts val num_facts = length facts val fact_lines = - map (line_for_fact ctxt fact_prefix ascii_of I (not exporter) + map (line_of_fact ctxt fact_prefix ascii_of I (not exporter) (not exporter) mono type_enc (rank_of_fact_num num_facts)) (0 upto num_facts - 1 ~~ facts) - val subclass_lines = maps (lines_for_subclass_pair type_enc) subclass_pairs - val tcon_lines = map (line_for_tcon_clause type_enc) tcon_clauses + val subclass_lines = maps (lines_of_subclass_pair type_enc) subclass_pairs + val tcon_lines = map (line_of_tcon_clause type_enc) tcon_clauses val helper_lines = 0 upto length helpers - 1 ~~ helpers - |> map (line_for_fact ctxt helper_prefix I (K "") false true mono type_enc - (K default_rank)) - val free_type_lines = lines_for_free_types type_enc (facts @ conjs) - val conj_lines = map (line_for_conjecture ctxt mono type_enc) conjs + |> map (line_of_fact ctxt helper_prefix I (K "") false true mono type_enc + (K default_rank)) + val free_type_lines = lines_of_free_types type_enc (facts @ conjs) + val conj_lines = map (line_of_conjecture ctxt mono type_enc) conjs (* Reordering these might confuse the proof reconstruction code. *) val problem = [(explicit_declsN, class_decl_lines @ sym_decl_lines), diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed May 15 17:43:42 2013 +0200 @@ -41,7 +41,7 @@ type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list val short_output : bool -> string -> string - val string_for_failure : failure -> string + val string_of_failure : failure -> string val extract_important_message : string -> string val extract_known_failure : (failure * string) list -> string -> failure option @@ -105,27 +105,27 @@ "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^ " " -fun string_for_failure Unprovable = "The generated problem is unprovable." - | string_for_failure GaveUp = "The prover gave up." - | string_for_failure ProofMissing = +fun string_of_failure Unprovable = "The generated problem is unprovable." + | string_of_failure GaveUp = "The prover gave up." + | string_of_failure ProofMissing = "The prover claims the conjecture is a theorem but did not provide a proof." - | string_for_failure ProofIncomplete = + | string_of_failure ProofIncomplete = "The prover claims the conjecture is a theorem but provided an incomplete \ \(or unparsable) proof." - | string_for_failure (UnsoundProof (false, ss)) = + | string_of_failure (UnsoundProof (false, ss)) = "The prover found an unsound proof " ^ involving ss ^ "(or, less likely, your axioms are inconsistent). Specify a sound type \ \encoding or omit the \"type_enc\" option." - | string_for_failure (UnsoundProof (true, ss)) = + | string_of_failure (UnsoundProof (true, ss)) = "The prover found an unsound proof " ^ involving ss ^ "(or, less likely, your axioms are inconsistent). Please report this to \ \the Isabelle developers." - | string_for_failure CantConnect = "Cannot connect to remote server." - | string_for_failure TimedOut = "Timed out." - | string_for_failure Inappropriate = + | string_of_failure CantConnect = "Cannot connect to remote server." + | string_of_failure TimedOut = "Timed out." + | string_of_failure Inappropriate = "The generated problem lies outside the prover's scope." - | string_for_failure OutOfResources = "The prover ran out of resources." - | string_for_failure OldSPASS = + | string_of_failure OutOfResources = "The prover ran out of resources." + | string_of_failure OldSPASS = "The version of SPASS you are using is obsolete. Please upgrade to \ \SPASS 3.8ds. To install it, download and extract the package \ \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \ @@ -134,20 +134,20 @@ (Path.variable "ISABELLE_HOME_USER" :: map Path.basic ["etc", "components"])))) ^ " on a line of its own." - | string_for_failure NoPerl = "Perl" ^ missing_message_tail - | string_for_failure NoLibwwwPerl = + | string_of_failure NoPerl = "Perl" ^ missing_message_tail + | string_of_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail - | string_for_failure MalformedInput = + | string_of_failure MalformedInput = "The generated problem is malformed. Please report this to the Isabelle \ \developers." - | string_for_failure MalformedOutput = "The prover output is malformed." - | string_for_failure Interrupted = "The prover was interrupted." - | string_for_failure Crashed = "The prover crashed." - | string_for_failure InternalError = "An internal prover error occurred." - | string_for_failure (UnknownError string) = + | string_of_failure MalformedOutput = "The prover output is malformed." + | string_of_failure Interrupted = "The prover was interrupted." + | string_of_failure Crashed = "The prover crashed." + | string_of_failure InternalError = "An internal prover error occurred." + | string_of_failure (UnknownError s) = "A prover error occurred" ^ - (if string = "" then ". (Pass the \"verbose\" option for details.)" - else ":\n" ^ string) + (if s = "" then ". (Pass the \"verbose\" option for details.)" + else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output = output |> first_field begin_delim |> the |> snd diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed May 15 17:43:42 2013 +0200 @@ -646,7 +646,7 @@ (output, 0) => split_lines output | (output, _) => (warning (case extract_known_failure known_perl_failures output of - SOME failure => string_for_failure failure + SOME failure => string_of_failure failure | NONE => trim_line output ^ "."); [])) () handle TimeLimit.TimeOut => [] diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Wed May 15 17:43:42 2013 +0200 @@ -246,7 +246,7 @@ false false [] @{prop False} props (* val _ = tracing ("ATP PROBLEM: " ^ - cat_lines (lines_for_atp_problem CNF atp_problem)) + cat_lines (lines_of_atp_problem CNF atp_problem)) *) (* "rev" is for compatibility with existing proof scripts. *) val axioms = diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Wed May 15 17:43:42 2013 +0200 @@ -656,7 +656,7 @@ #> pairself (Envir.subst_term_types tyenv)) val tysubst = tyenv |> Vartab.dest in (tysubst, tsubst) end - fun subst_info_for_prem subgoal_no prem = + fun subst_info_of_prem subgoal_no prem = case prem of _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => let val ax_no = HOLogic.dest_nat num in @@ -675,7 +675,7 @@ NONE fun clusters_in_term skolem t = Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst) - fun deps_for_term_subst (var, t) = + fun deps_of_term_subst (var, t) = case clusters_in_term false var of [] => NONE | [(ax_no, cluster_no)] => @@ -684,9 +684,9 @@ |> cluster_no > 1 ? cons (ax_no, cluster_no - 1)) | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var]) val prems = Logic.strip_imp_prems (prop_of prems_imp_false) - val substs = prems |> map2 subst_info_for_prem (1 upto length prems) + val substs = prems |> map2 subst_info_of_prem (1 upto length prems) |> sort (int_ord o pairself fst) - val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs + val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs val clusters = maps (op ::) depss val ordered_clusters = Int_Pair_Graph.empty @@ -720,7 +720,7 @@ cluster_no = 0 andalso skolem) |> sort shuffle_ord |> map (fst o snd) (* for debugging only: - fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = + fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) = "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^ "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^ commas (map ((fn (s, t) => s ^ " |-> " ^ t) @@ -729,12 +729,12 @@ val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts) val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names) val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^ - cat_lines (map string_for_subst_info substs)) + cat_lines (map string_of_subst_info substs)) *) fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1) - fun rotation_for_subgoal i = + fun rotation_of_subgoal i = find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs in Goal.prove ctxt [] [] @{prop False} @@ -746,7 +746,7 @@ THEN match_tac [prems_imp_false] 1 THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i - THEN rotate_tac (rotation_for_subgoal i) i + THEN rotate_tac (rotation_of_subgoal i) i THEN PRIMITIVE (unify_first_prem_with_concl thy i) THEN assume_tac i THEN flexflex_tac))) diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed May 15 17:43:42 2013 +0200 @@ -216,7 +216,7 @@ (* TODO: add Skolem variables to context? *) fun enrich_with_fact l t = Proof_Context.put_thms false - (string_for_label l, SOME [Skip_Proof.make_thm thy t]) + (string_of_label l, SOME [Skip_Proof.make_thm thy t]) fun enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t | enrich_with_step _ = I diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Wed May 15 17:43:42 2013 +0200 @@ -245,7 +245,7 @@ (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp) -fun hackish_string_for_term ctxt = +fun hackish_string_of_term ctxt = with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces (* This is a terrible hack. Free variables are sometimes coded as "M__" when @@ -269,12 +269,8 @@ (Term.add_vars t [] |> sort_wrt (fst o fst)) |> fst -fun backquote_term ctxt t = - t |> close_form - |> hackish_string_for_term ctxt - |> backquote - -fun backquote_thm ctxt th = backquote_term ctxt (prop_of th) +fun backquote_term ctxt = close_form #> hackish_string_of_term ctxt #> backquote +fun backquote_thm ctxt = backquote_term ctxt o prop_of fun clasimpset_rule_table_of ctxt = let @@ -384,7 +380,7 @@ val p_inst = concl_prop |> map_aterms varify_noninducts |> close_form |> lambda (Free ind_x) - |> hackish_string_for_term ctxt + |> hackish_string_of_term ctxt in ((fn () => name () ^ "[where " ^ p_name ^ " = " ^ quote p_inst ^ "]", stature), th |> read_instantiate ctxt [((p_name, 0), p_inst)]) diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed May 15 17:43:42 2013 +0200 @@ -334,13 +334,13 @@ fun is_raw_param_relevant_for_minimize (name, _) = member (op =) params_for_minimize name -fun string_for_raw_param (key, values) = +fun string_of_raw_param (key, values) = key ^ (case implode_param values of "" => "" | value => " = " ^ value) -fun nice_string_for_raw_param (p as (key, ["false"])) = +fun nice_string_of_raw_param (p as (key, ["false"])) = (case AList.find (op =) negated_alias_params key of [neg] => neg - | _ => string_for_raw_param p) - | nice_string_for_raw_param p = string_for_raw_param p + | _ => string_of_raw_param p) + | nice_string_of_raw_param p = string_of_raw_param p fun minimize_command override_params i more_override_params prover_name fact_names = @@ -350,7 +350,7 @@ |> filter_out (AList.defined (op =) more_override_params o fst)) @ more_override_params |> filter is_raw_param_relevant_for_minimize - |> map nice_string_for_raw_param + |> map nice_string_of_raw_param |> (if prover_name = default_minimize_prover then I else cons prover_name) |> space_implode ", " in @@ -428,7 +428,7 @@ Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of) -fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value +fun string_of_raw_param (name, value) = name ^ " = " ^ implode_param value fun sledgehammer_params_trans params = Toplevel.theory @@ -439,7 +439,7 @@ (case default_raw_params ctxt |> rev of [] => "none" | params => - params |> map string_for_raw_param + params |> map string_of_raw_param |> sort_strings |> cat_lines)) end)) diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed May 15 17:43:42 2013 +0200 @@ -574,7 +574,7 @@ val thy = Proof_Context.theory_of ctxt fun is_built_in (x as (s, _)) args = if member (op =) logical_consts s then (true, args) - else is_built_in_const_for_prover ctxt prover x args + else is_built_in_const_of_prover ctxt prover x args val fixes = map snd (Variable.dest_fixes ctxt) val classes = Sign.classes_of thy fun add_classes @{sort type} = I diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML Wed May 15 17:43:42 2013 +0200 @@ -50,11 +50,11 @@ datatype pattern = PVar | PApp of string * pattern list datatype ptype = PType of int * pattern list -fun string_for_pattern PVar = "_" - | string_for_pattern (PApp (s, ps)) = - if null ps then s else s ^ string_for_patterns ps -and string_for_patterns ps = "(" ^ commas (map string_for_pattern ps) ^ ")" -fun string_for_ptype (PType (_, ps)) = string_for_patterns ps +fun string_of_pattern PVar = "_" + | string_of_pattern (PApp (s, ps)) = + if null ps then s else s ^ string_of_patterns ps +and string_of_patterns ps = "(" ^ commas (map string_of_pattern ps) ^ ")" +fun string_of_ptype (PType (_, ps)) = string_of_patterns ps (*Is the second type an instance of the first one?*) fun match_pattern (PVar, _) = true @@ -74,20 +74,20 @@ fun pconst_hyper_mem f const_tab (s, ps) = exists (curry (match_ptype o f) ps) (these (Symtab.lookup const_tab s)) -fun pattern_for_type (Type (s, Ts)) = PApp (s, map pattern_for_type Ts) - | pattern_for_type (TFree (s, _)) = PApp (s, []) - | pattern_for_type (TVar _) = PVar +fun pattern_of_type (Type (s, Ts)) = PApp (s, map pattern_of_type Ts) + | pattern_of_type (TFree (s, _)) = PApp (s, []) + | pattern_of_type (TVar _) = PVar (* Pairs a constant with the list of its type instantiations. *) fun ptype thy const x = - (if const then map pattern_for_type (these (try (Sign.const_typargs thy) x)) + (if const then map pattern_of_type (these (try (Sign.const_typargs thy) x)) else []) fun rich_ptype thy const (s, T) = PType (order_of_type T, ptype thy const (s, T)) fun rich_pconst thy const (s, T) = (s, rich_ptype thy const (s, T)) -fun string_for_hyper_pconst (s, ps) = - s ^ "{" ^ commas (map string_for_ptype ps) ^ "}" +fun string_of_hyper_pconst (s, ps) = + s ^ "{" ^ commas (map string_of_ptype ps) ^ "}" (* Add a pconstant to the table, but a [] entry means a standard connective, which we ignore.*) @@ -264,7 +264,7 @@ * pow_int higher_order_irrel_weight (order - 1) end -fun multiplier_for_const_name local_const_multiplier s = +fun multiplier_of_const_name local_const_multiplier s = if String.isSubstring "." s then 1.0 else local_const_multiplier (* Computes a constant's weight, as determined by its frequency. *) @@ -278,7 +278,7 @@ else if String.isSuffix theory_const_suffix s then theory_const_weight else - multiplier_for_const_name local_const_multiplier s + multiplier_of_const_name local_const_multiplier s * weight_for m (pconst_freq (match_ptype o f) const_tab c) |> (if chained_const_weight < 1.0 andalso pconst_hyper_mem I chained_const_tab c then @@ -448,7 +448,7 @@ trace_msg ctxt (fn () => "New or updated constants: " ^ commas (rel_const_tab' |> Symtab.dest |> subtract (op =) (rel_const_tab |> Symtab.dest) - |> map string_for_hyper_pconst)); + |> map string_of_hyper_pconst)); map (fst o fst) accepts @ (if remaining_max = 0 then [] @@ -477,7 +477,7 @@ Real.toString thres ^ ", constants: " ^ commas (rel_const_tab |> Symtab.dest |> filter (curry (op <>) [] o snd) - |> map string_for_hyper_pconst)); + |> map string_of_hyper_pconst)); relevant [] [] hopeful end fun uses_const s t = @@ -516,11 +516,11 @@ let val thy = Proof_Context.theory_of ctxt val is_built_in_const = - Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover + Sledgehammer_Provers.is_built_in_const_of_prover ctxt prover val fudge = case fudge of SOME fudge => fudge - | NONE => Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover + | NONE => Sledgehammer_Provers.relevance_fudge_of_prover ctxt prover val decay = Math.pow ((1.0 - thres1) / (1.0 - thres0), 1.0 / Real.fromInt (max_facts + 1)) in diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed May 15 17:43:42 2013 +0200 @@ -91,7 +91,7 @@ print silent (fn () => case outcome of - SOME failure => string_for_failure failure + SOME failure => string_of_failure failure | NONE => "Found proof" ^ (if length used_facts = length facts then "" diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed May 15 17:43:42 2013 +0200 @@ -69,7 +69,7 @@ (* lookup facts in context *) fun resolve_fact_names ctxt names = (names - |>> map string_for_label + |>> map string_of_label |> op @ |> maps (thms_of_name ctxt)) handle ERROR msg => error ("preplay error: " ^ msg) diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed May 15 17:43:42 2013 +0200 @@ -28,7 +28,7 @@ val no_label : label val no_facts : facts - val string_for_label : label -> string + val string_of_label : label -> string val fix_of_proof : isar_proof -> fix val assms_of_proof : isar_proof -> assms val steps_of_proof : isar_proof -> isar_step list @@ -63,7 +63,7 @@ val no_label = ("", ~1) val no_facts = ([],[]) -fun string_for_label (s, num) = s ^ string_of_int num +fun string_of_label (s, num) = s ^ string_of_int num fun fix_of_proof (Proof (fix, _, _)) = fix fun assms_of_proof (Proof (_, assms, _)) = assms diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed May 15 17:43:42 2013 +0200 @@ -115,14 +115,14 @@ Proof.context -> string -> string option val remotify_prover_if_not_installed : Proof.context -> string -> string option - val default_max_facts_for_prover : Proof.context -> bool -> string -> int + val default_max_facts_of_prover : Proof.context -> bool -> string -> int val is_unit_equality : term -> bool - val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool - val is_built_in_const_for_prover : + val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool + val is_built_in_const_of_prover : Proof.context -> string -> string * typ -> term list -> bool * term list val atp_relevance_fudge : relevance_fudge val smt_relevance_fudge : relevance_fudge - val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge + val relevance_fudge_of_prover : Proof.context -> string -> relevance_fudge val weight_smt_fact : Proof.context -> int -> ((string * stature) * thm) * int -> (string * stature) * (int option * thm) @@ -171,7 +171,7 @@ fun is_smt_prover ctxt = member (op =) (SMT_Solver.available_solvers_of ctxt) -fun is_atp_for_format is_format ctxt name = +fun is_atp_of_format is_format ctxt name = let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of SOME config => @@ -180,8 +180,8 @@ | NONE => false end -val is_unit_equational_atp = is_atp_for_format (curry (op =) CNF_UEQ) -val is_ho_atp = is_atp_for_format is_format_higher_order +val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ) +val is_ho_atp = is_atp_of_format is_format_higher_order fun is_prover_supported ctxt = let val thy = Proof_Context.theory_of ctxt in @@ -213,7 +213,7 @@ fun slice_max_facts (_, (_, ( ((max_facts, _), _, _, _, _), _))) = max_facts -fun default_max_facts_for_prover ctxt slice name = +fun default_max_facts_of_prover ctxt slice name = let val thy = Proof_Context.theory_of ctxt in if is_reconstructor name then reconstructor_default_max_facts @@ -243,10 +243,10 @@ is_good_unit_equality T t u | is_unit_equality _ = false -fun is_appropriate_prop_for_prover ctxt name = +fun is_appropriate_prop_of_prover ctxt name = if is_unit_equational_atp ctxt name then is_unit_equality else K true -fun is_built_in_const_for_prover ctxt name = +fun is_built_in_const_of_prover ctxt name = if is_smt_prover ctxt name then let val ctxt = ctxt |> select_smt_solver name in fn x => fn ts => @@ -304,7 +304,7 @@ threshold_divisor = #threshold_divisor atp_relevance_fudge, ridiculous_threshold = #ridiculous_threshold atp_relevance_fudge} -fun relevance_fudge_for_prover ctxt name = +fun relevance_fudge_of_prover ctxt name = if is_smt_prover ctxt name then smt_relevance_fudge else atp_relevance_fudge fun supported_provers ctxt = @@ -445,7 +445,7 @@ (info, (smt_fact_weight ctxt j num_facts, th |> Thm.transfer thy)) end -fun overlord_file_location_for_prover prover = +fun overlord_file_location_of_prover prover = (getenv "ISABELLE_HOME_USER", "prob_" ^ prover) fun proof_banner mode name = @@ -490,14 +490,14 @@ val full_tac = Method.insert_tac facts i THEN tac ctxt i in time_limit timeout (try (Seq.pull o full_tac)) goal end -fun tac_for_reconstructor (Metis (type_enc, lam_trans)) = +fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans - | tac_for_reconstructor SMT = SMT_Solver.smt_tac + | tac_of_reconstructor SMT = SMT_Solver.smt_tac fun timed_reconstructor reconstr debug timeout ths = (Config.put Metis_Tactic.verbose debug #> Config.put SMT_Config.verbose debug - #> (fn ctxt => tac_for_reconstructor reconstr ctxt ths)) + #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths)) |> timed_apply timeout fun is_fact_chained ((_, (sc, _)), _) = sc = Chained @@ -528,7 +528,7 @@ let val _ = if verbose then - "Trying \"" ^ string_for_reconstructor reconstr ^ "\"" ^ + "Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^ (case timeout of SOME timeout => " for " ^ string_from_time timeout | NONE => "") ^ "..." @@ -553,8 +553,8 @@ clearly inconsistent facts such as X = a | X = b, though it by no means guarantees soundness. *) -fun get_facts_for_filter _ [(_, facts)] = facts - | get_facts_for_filter fact_filter factss = +fun get_facts_of_filter _ [(_, facts)] = facts + | get_facts_of_filter fact_filter factss = case AList.lookup (op =) factss fact_filter of SOME facts => facts | NONE => snd (hd factss) @@ -647,12 +647,12 @@ (max_new_instances |> the_default best_max_new_instances) #> Config.put Legacy_Monomorph.keep_partial_instances false -fun suffix_for_mode Auto_Try = "_try" - | suffix_for_mode Try = "_try" - | suffix_for_mode Normal = "" - | suffix_for_mode MaSh = "" - | suffix_for_mode Auto_Minimize = "_min" - | suffix_for_mode Minimize = "_min" +fun suffix_of_mode Auto_Try = "_try" + | suffix_of_mode Try = "_try" + | suffix_of_mode Normal = "" + | suffix_of_mode MaSh = "" + | suffix_of_mode Auto_Minimize = "_min" + | suffix_of_mode Minimize = "_min" (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on Linux appears to be the only ATP that does not honor its time limit. *) @@ -681,11 +681,11 @@ else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val (dest_dir, problem_prefix) = - if overlord then overlord_file_location_for_prover name + if overlord then overlord_file_location_of_prover name else (Config.get ctxt dest_dir, Config.get ctxt problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ - suffix_for_mode mode ^ "_" ^ string_of_int subgoal) + suffix_of_mode mode ^ "_" ^ string_of_int subgoal) val prob_path = if dest_dir = "" then File.tmp_path problem_file_name @@ -763,7 +763,7 @@ let val effective_fact_filter = fact_filter |> the_default best_fact_filter - val facts = get_facts_for_filter effective_fact_filter factss + val facts = get_facts_of_filter effective_fact_filter factss val num_facts = Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge @@ -834,7 +834,7 @@ |> enclose "TIMEFORMAT='%3R'; { time " " ; }" val _ = atp_problem - |> lines_for_atp_problem format ord ord_info + |> lines_of_atp_problem format ord ord_info |> cons ("% " ^ command ^ "\n") |> File.write_list prob_path val ((output, run_time), used_from, (atp_proof, outcome)) = @@ -864,7 +864,7 @@ val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in - if debug then (warning (string_for_failure failure); NONE) + if debug then (warning (string_of_failure failure); NONE) else SOME failure end | NONE => NONE) @@ -966,7 +966,7 @@ end | SOME failure => ([], Lazy.value (Failed_to_Play plain_metis), - fn _ => string_for_failure failure, "") + fn _ => string_of_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, @@ -1024,7 +1024,7 @@ |> Config.put SMT_Config.verbose debug |> (if overlord then Config.put SMT_Config.debug_files - (overlord_file_location_for_prover name + (overlord_file_location_of_prover name |> (fn (path, name) => path ^ "/" ^ name)) else I) @@ -1112,7 +1112,7 @@ if verbose andalso is_some outcome then quote name ^ " invoked with " ^ num_of_facts fact_filter num_facts ^ ": " ^ - string_for_failure (failure_from_smt_failure (the outcome)) ^ + string_of_failure (failure_from_smt_failure (the outcome)) ^ " Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^ "..." |> Output.urgent_message @@ -1166,7 +1166,7 @@ "") | SOME failure => (Lazy.value (Failed_to_Play plain_metis), - fn _ => string_for_failure failure, "") + fn _ => string_of_failure failure, "") in {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time, preplay = preplay, message = message, @@ -1212,7 +1212,7 @@ in {outcome = SOME failure, used_facts = [], used_from = [], run_time = Time.zeroTime, preplay = Lazy.value play, - message = fn _ => string_for_failure failure, message_tail = ""} + message = fn _ => string_of_failure failure, message_tail = ""} end end diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed May 15 17:43:42 2013 +0200 @@ -27,7 +27,7 @@ * (string * stature) list vector * int Symtab.table * string proof * thm val smtN : string - val string_for_reconstructor : reconstructor -> string + val string_of_reconstructor : reconstructor -> string val lam_trans_from_atp_proof : string proof -> string -> string val is_typed_helper_used_in_atp_proof : string proof -> bool val used_facts_in_atp_proof : @@ -78,9 +78,9 @@ val smtN = "smt" -fun string_for_reconstructor (Metis (type_enc, lam_trans)) = +fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans - | string_for_reconstructor SMT = smtN + | string_of_reconstructor SMT = smtN (** fact extraction from ATP proofs **) @@ -207,7 +207,7 @@ fun using_labels [] = "" | using_labels ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " + "using " ^ space_implode " " (map string_of_label ls) ^ " " fun command_call name [] = name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")" @@ -216,7 +216,7 @@ fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = (* unusing_chained_facts used_chaineds num_chained ^ *) using_labels ls ^ apply_on_subgoal i n ^ - command_call (string_for_reconstructor reconstr) ss + command_call (string_of_reconstructor reconstr) ss fun try_command_line banner time command = banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "." @@ -270,14 +270,14 @@ val have_prefix = "f" val raw_prefix = "x" -fun raw_label_for_name (num, ss) = +fun raw_label_of_name (num, ss) = case resolve_conjecture ss of [j] => (conjecture_prefix, j) | _ => (raw_prefix ^ ascii_of num, 0) -fun label_of_clause [name] = raw_label_for_name name +fun label_of_clause [name] = raw_label_of_name name | label_of_clause c = - (space_implode "___" (map (fst o raw_label_for_name) c), 0) + (space_implode "___" (map (fst o raw_label_of_name) c), 0) fun add_fact_from_dependencies fact_names (names as [(_, ss)]) = if is_fact fact_names ss then @@ -425,13 +425,13 @@ val indent_size = 2 -fun string_for_proof ctxt type_enc lam_trans i n proof = +fun string_of_proof ctxt type_enc lam_trans i n proof = let val register_fixes = map Free #> fold Variable.auto_fixes fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) fun of_indent ind = replicate_string (ind * indent_size) " " fun of_moreover ind = of_indent ind ^ "moreover\n" - fun of_label l = if l = no_label then "" else string_for_label l ^ ": " + fun of_label l = if l = no_label then "" else string_of_label l ^ ": " fun of_obtain qs nr = (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then "ultimately " @@ -558,7 +558,7 @@ Proof (fix, do_assms assms, map do_step steps) in do_proof proof end -fun prefix_for_depth n = replicate_string (n + 1) +fun prefix_of_depth n = replicate_string (n + 1) val relabel_proof = let @@ -566,7 +566,7 @@ if l = no_label then old else - let val l' = (prefix_for_depth depth prefix, next) in + let val l' = (prefix_of_depth depth prefix, next) in (l', (l, l') :: subst, next + 1) end fun do_facts subst = @@ -677,7 +677,7 @@ (case resolve_conjecture ss of [j] => if j = length hyp_ts then NONE - else SOME (raw_label_for_name name, nth hyp_ts j) + else SOME (raw_label_of_name name, nth hyp_ts j) | _ => NONE) | _ => NONE) val bot = atp_proof |> List.last |> #1 @@ -808,8 +808,8 @@ (if isar_proofs = SOME true then isar_compress else 1000.0)) |>> clean_up_labels_in_proof val isar_text = - string_for_proof ctxt type_enc lam_trans subgoal subgoal_count - isar_proof + string_of_proof ctxt type_enc lam_trans subgoal subgoal_count + isar_proof in case isar_text of "" => diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed May 15 17:27:24 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed May 15 17:43:42 2013 +0200 @@ -74,7 +74,7 @@ val birth_time = Time.now () val death_time = Time.+ (birth_time, hard_timeout) val max_facts = - max_facts |> the_default (default_max_facts_for_prover ctxt slice name) + max_facts |> the_default (default_max_facts_of_prover ctxt slice name) val num_facts = length facts |> not only ? Integer.min max_facts fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal @@ -219,7 +219,7 @@ case max_facts of SOME n => n | NONE => - 0 |> fold (Integer.max o default_max_facts_for_prover ctxt slice) + 0 |> fold (Integer.max o default_max_facts_of_prover ctxt slice) provers |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor) in