--- 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])
--- 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 ()
--- 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
--- 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),
--- 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
--- 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 => []
--- 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 =
--- 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)))
--- 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
--- 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)])
--- 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))
--- 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
--- 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
--- 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 ""
--- 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)
--- 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
--- 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
--- 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
"" =>
--- 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