--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu May 16 13:34:13 2013 +0200
@@ -219,7 +219,7 @@
val timing = true;
fun time timer msg = (if timing
- then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
+ then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
else (); Timer.startRealTimer ());
val preN = "pre_"
--- a/src/HOL/TPTP/atp_problem_import.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML Thu May 16 13:34:13 2013 +0200
@@ -108,7 +108,7 @@
fun refute_tptp_file thy timeout file_name =
let
- fun print_szs_from_outcome falsify s =
+ fun print_szs_of_outcome falsify s =
"% SZS status " ^
(if s = "genuine" then
if falsify then "CounterSatisfiable" else "Satisfiable"
@@ -122,7 +122,7 @@
in
Refute.refute_term ctxt params (defs @ nondefs)
(case conjs of conj :: _ => conj | [] => @{prop True})
- |> print_szs_from_outcome (not (null conjs))
+ |> print_szs_of_outcome (not (null conjs))
end
@@ -263,7 +263,7 @@
Logic.list_implies (rev defs @ rev nondefs,
case conjs of conj :: _ => conj | [] => @{prop False})
-fun print_szs_from_success conjs success =
+fun print_szs_of_success conjs success =
Output.urgent_message ("% SZS status " ^
(if success then
if null conjs then "Unsatisfiable" else "Theorem"
@@ -277,7 +277,7 @@
val conj = make_conj assms conjs
in
can_tac ctxt (sledgehammer_tac true ctxt timeout 1) conj
- |> print_szs_from_success conjs
+ |> print_szs_of_success conjs
end
fun generic_isabelle_tptp_file demo thy timeout file_name =
@@ -292,7 +292,7 @@
can_tac ctxt (sledgehammer_tac demo ctxt (timeout div 2) 1) conj orelse
can_tac ctxt (SOLVE_TIMEOUT timeout (last_hope_atp ^ "(*)")
(atp_tac ctxt last_hope_completeness [] timeout last_hope_atp 1)) conj)
- |> print_szs_from_success conjs
+ |> print_szs_of_success conjs
end
val isabelle_tptp_file = generic_isabelle_tptp_file false
--- a/src/HOL/TPTP/atp_theory_export.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu May 16 13:34:13 2013 +0200
@@ -157,7 +157,7 @@
let
val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
val type_enc =
- type_enc |> type_enc_from_string Non_Strict
+ type_enc |> type_enc_of_string Non_Strict
|> adjust_type_enc format
val mono = not (is_type_enc_polymorphic type_enc)
val facts =
--- a/src/HOL/TPTP/mash_eval.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Thu May 16 13:34:13 2013 +0200
@@ -75,7 +75,7 @@
let val facts = facts |> map (fst o fst) in
str_of_method method ^
(if is_none outcome then
- "Success (" ^ ATP_Util.string_from_time run_time ^ "): " ^
+ "Success (" ^ ATP_Util.string_of_time run_time ^ "): " ^
(used_facts |> map (with_index facts o fst)
|> sort (int_ord o pairself fst)
|> map index_str
@@ -199,7 +199,7 @@
"slice" |> not slice ? prefix "dont_",
"type_enc = " ^ the_default "smart" type_enc,
"lam_trans = " ^ the_default "smart" lam_trans,
- "timeout = " ^ ATP_Util.string_from_time (the_default one_year timeout),
+ "timeout = " ^ ATP_Util.string_of_time (the_default one_year timeout),
"instantiate_inducts" |> not inst_inducts ? prefix "dont_"]
val _ = print " * * *";
val _ = print ("Options: " ^ commas options);
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Thu May 16 13:34:13 2013 +0200
@@ -87,7 +87,7 @@
val proxify_const : string -> (string * string) option
val invert_const : string -> string
val unproxify_const : string -> string
- val new_skolem_var_name_from_const : string -> string
+ val new_skolem_var_name_of_const : string -> string
val atp_logical_consts : string list
val atp_irrelevant_consts : string list
val atp_widely_irrelevant_consts : string list
@@ -96,7 +96,7 @@
val is_type_enc_polymorphic : type_enc -> bool
val level_of_type_enc : type_enc -> type_level
val is_type_enc_sound : type_enc -> bool
- val type_enc_from_string : strictness -> string -> type_enc
+ val type_enc_of_string : strictness -> string -> type_enc
val adjust_type_enc : atp_format -> type_enc -> type_enc
val is_lambda_free : term -> bool
val mk_aconns :
@@ -104,7 +104,7 @@
val unmangled_const : string -> string * (string, 'b) ho_term list
val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * (status * thm) list) list
- val trans_lams_from_string :
+ val trans_lams_of_string :
Proof.context -> type_enc -> string -> term list -> term list * term list
val string_of_status : status -> string
val factsN : string
@@ -395,7 +395,7 @@
fun make_class clas = class_prefix ^ ascii_of clas
-fun new_skolem_var_name_from_const s =
+fun new_skolem_var_name_of_const s =
let val ss = s |> space_explode Long_Name.separator in
nth ss (length ss - 2)
end
@@ -568,18 +568,18 @@
(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
Also accumulates sort infomation. *)
-fun iterm_from_term thy type_enc bs (P $ Q) =
+fun iterm_of_term thy type_enc bs (P $ Q) =
let
- val (P', P_atomics_Ts) = iterm_from_term thy type_enc bs P
- val (Q', Q_atomics_Ts) = iterm_from_term thy type_enc bs Q
+ val (P', P_atomics_Ts) = iterm_of_term thy type_enc bs P
+ val (Q', Q_atomics_Ts) = iterm_of_term thy type_enc bs Q
in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
- | iterm_from_term thy type_enc _ (Const (c, T)) =
+ | iterm_of_term thy type_enc _ (Const (c, T)) =
(IConst (`(make_fixed_const (SOME type_enc)) c, T,
robust_const_type_args thy (c, T)),
atomic_types_of T)
- | iterm_from_term _ _ _ (Free (s, T)) =
+ | iterm_of_term _ _ _ (Free (s, T)) =
(IConst (`make_fixed_var s, T, []), atomic_types_of T)
- | iterm_from_term _ type_enc _ (Var (v as (s, _), T)) =
+ | iterm_of_term _ type_enc _ (Var (v as (s, _), T)) =
(if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val Ts = T |> strip_type |> swap |> op ::
@@ -587,15 +587,14 @@
in IConst (`(make_fixed_const (SOME type_enc)) s', T, Ts) end
else
IVar ((make_schematic_var v, s), T), atomic_types_of T)
- | iterm_from_term _ _ bs (Bound j) =
+ | iterm_of_term _ _ bs (Bound j) =
nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T))
- | iterm_from_term thy type_enc bs (Abs (s, T, t)) =
+ | iterm_of_term thy type_enc bs (Abs (s, T, t)) =
let
fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
val s = vary s
val name = `make_bound_var s
- val (tm, atomic_Ts) =
- iterm_from_term thy type_enc ((s, (name, T)) :: bs) t
+ val (tm, atomic_Ts) = iterm_of_term thy type_enc ((s, (name, T)) :: bs) t
in (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) end
(* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *)
@@ -605,7 +604,7 @@
fun try_unsuffixes ss s =
fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
-fun type_enc_from_string strictness s =
+fun type_enc_of_string strictness s =
(case try (unprefix "tc_") s of
SOME s => (SOME Type_Class_Polymorphic, s)
| NONE =>
@@ -903,7 +902,7 @@
val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
val fused_infinite_type = Type (fused_infinite_type_name, [])
-fun raw_ho_type_from_typ type_enc =
+fun raw_ho_type_of_typ type_enc =
let
fun term (Type (s, Ts)) =
AType (case (is_type_enc_higher_order type_enc, s) of
@@ -919,11 +918,12 @@
| term (TVar z) = AType (tvar_name z, [])
in term end
-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_term_of_ho_type (AType (name, tys)) =
+ ATerm ((name, []), map ho_term_of_ho_type tys)
+ | ho_term_of_ho_type _ = raise Fail "unexpected type"
fun ho_type_of_type_arg type_enc T =
- if T = dummyT then NONE else SOME (raw_ho_type_from_typ type_enc T)
+ if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T)
(* This shouldn't clash with anything else. *)
val uncurried_alias_sep = "\000"
@@ -938,7 +938,7 @@
| generic_mangled_type_name _ _ = raise Fail "unexpected type"
fun mangled_type type_enc =
- generic_mangled_type_name fst o raw_ho_type_from_typ type_enc
+ generic_mangled_type_name fst o raw_ho_type_of_typ type_enc
fun make_native_type s =
if s = tptp_bool_type orelse s = tptp_fun_type orelse
@@ -947,7 +947,7 @@
else
native_type_prefix ^ ascii_of s
-fun native_ho_type_from_raw_ho_type type_enc pred_sym ary =
+fun native_ho_type_of_raw_ho_type type_enc pred_sym ary =
let
fun to_mangled_atype ty =
AType ((make_native_type (generic_mangled_type_name fst ty),
@@ -967,9 +967,9 @@
| to_ho _ = raise Fail "unexpected type"
in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
-fun native_ho_type_from_typ type_enc pred_sym ary =
- native_ho_type_from_raw_ho_type type_enc pred_sym ary
- o raw_ho_type_from_typ type_enc
+fun native_ho_type_of_typ type_enc pred_sym ary =
+ native_ho_type_of_raw_ho_type type_enc pred_sym ary
+ o raw_ho_type_of_typ type_enc
(* Make atoms for sorted type variables. *)
fun generic_add_sorts_on_type _ [] = I
@@ -983,9 +983,9 @@
fun process_type_args type_enc T_args =
if is_type_enc_native type_enc then
- (map (native_ho_type_from_typ type_enc false 0) T_args, [])
+ (map (native_ho_type_of_typ type_enc false 0) T_args, [])
else
- ([], map_filter (Option.map ho_term_from_ho_type
+ ([], map_filter (Option.map ho_term_of_ho_type
o ho_type_of_type_arg type_enc) T_args)
fun class_atom type_enc (cl, T) =
@@ -1194,11 +1194,11 @@
| filt _ tm = tm
in filt 0 end
-fun iformula_from_prop ctxt type_enc iff_for_eq =
+fun iformula_of_prop ctxt type_enc iff_for_eq =
let
val thy = Proof_Context.theory_of ctxt
fun do_term bs t atomic_Ts =
- iterm_from_term thy type_enc bs (Envir.eta_contract t)
+ iterm_of_term thy type_enc bs (Envir.eta_contract t)
|>> (introduce_proxies_in_iterm type_enc
#> mangle_type_args_in_iterm type_enc #> AAtom)
||> union (op =) atomic_Ts
@@ -1297,8 +1297,7 @@
let
val iff_for_eq = iff_for_eq andalso should_use_iff_for_eq format type_enc
val (iformula, atomic_Ts) =
- iformula_from_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t
- []
+ iformula_of_prop ctxt type_enc iff_for_eq (SOME (role <> Conjecture)) t []
|>> close_universally add_iterm_vars
in
{name = name, stature = stature, role = role, iformula = iformula,
@@ -1903,7 +1902,7 @@
end
| extract_lambda_def _ = raise Fail "malformed lifted lambda"
-fun trans_lams_from_string ctxt type_enc lam_trans =
+fun trans_lams_of_string ctxt type_enc lam_trans =
if lam_trans = no_lamsN then
rpair []
else if lam_trans = hide_lamsN then
@@ -1955,7 +1954,7 @@
concl_t facts =
let
val thy = Proof_Context.theory_of ctxt
- val trans_lams = trans_lams_from_string ctxt type_enc lam_trans
+ val trans_lams = trans_lams_of_string ctxt type_enc lam_trans
val fact_ts = facts |> map snd
(* Remove existing facts from the conjecture, as this can dramatically
boost an ATP's performance (for some reason). *)
@@ -2058,17 +2057,17 @@
fun do_bound_type ctxt mono type_enc =
case type_enc of
Native (_, _, level) =>
- fused_type ctxt mono level 0 #> native_ho_type_from_typ type_enc false 0
+ fused_type ctxt mono level 0 #> native_ho_type_of_typ type_enc false 0
#> SOME
| _ => K NONE
fun tag_with_type ctxt mono type_enc pos T tm =
IConst (type_tag, T --> T, [T])
|> mangle_type_args_in_iterm type_enc
- |> ho_term_from_iterm ctxt mono type_enc pos
+ |> ho_term_of_iterm ctxt mono type_enc pos
|> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
| _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_iterm ctxt mono type_enc pos =
+and ho_term_of_iterm ctxt mono type_enc pos =
let
fun term site u =
let
@@ -2094,7 +2093,7 @@
map (term Elsewhere) args |> mk_aterm type_enc name []
| IAbs ((name, T), tm) =>
if is_type_enc_higher_order type_enc then
- AAbs (((name, native_ho_type_from_typ type_enc true 0 T), (* FIXME? why "true"? *)
+ AAbs (((name, native_ho_type_of_typ type_enc true 0 T), (* FIXME? why "true"? *)
term Elsewhere tm), map (term Elsewhere) args)
else
raise Fail "unexpected lambda-abstraction"
@@ -2102,11 +2101,11 @@
val tag = should_tag_with_type ctxt mono type_enc site u T
in t |> tag ? tag_with_type ctxt mono type_enc pos T end
in term (Top_Level pos) end
-and formula_from_iformula ctxt mono type_enc should_guard_var =
+and formula_of_iformula ctxt mono type_enc should_guard_var =
let
val thy = Proof_Context.theory_of ctxt
val level = level_of_type_enc type_enc
- val do_term = ho_term_from_iterm ctxt mono type_enc
+ val do_term = ho_term_of_iterm ctxt mono type_enc
fun do_out_of_bound_type pos phi universal (name, T) =
if should_guard_type ctxt mono type_enc
(fn () => should_guard_var thy level pos phi universal name) T then
@@ -2121,7 +2120,7 @@
else
NONE
fun do_formula pos (ATyQuant (q, xs, phi)) =
- ATyQuant (q, map (apfst (native_ho_type_from_typ type_enc false 0)) xs,
+ ATyQuant (q, map (apfst (native_ho_type_of_typ type_enc false 0)) xs,
do_formula pos phi)
| do_formula pos (AQuant (q, xs, phi)) =
let
@@ -2161,7 +2160,7 @@
encode name, alt name),
role,
iformula
- |> formula_from_iformula ctxt mono type_enc
+ |> formula_of_iformula ctxt mono type_enc
should_guard_var_in_formula (if pos then SOME true else NONE)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types,
@@ -2188,7 +2187,7 @@
map (fn (cls, T) =>
(T |> dest_TVar |> tvar_name, map (`make_class) cls))
prems,
- native_ho_type_from_typ type_enc false 0 T, `make_class cl)
+ native_ho_type_of_typ type_enc false 0 T, `make_class cl)
else
Formula ((tcon_clause_prefix ^ name, ""), Axiom,
mk_ahorn (maps (class_atoms type_enc) prems)
@@ -2200,7 +2199,7 @@
({name, role, iformula, atomic_types, ...} : ifact) =
Formula ((conjecture_prefix ^ name, ""), role,
iformula
- |> formula_from_iformula ctxt mono type_enc
+ |> formula_of_iformula ctxt mono type_enc
should_guard_var_in_formula (SOME false)
|> close_formula_universally
|> bound_tvars type_enc true atomic_types, NONE, [])
@@ -2213,8 +2212,7 @@
fun line j (cl, T) =
if type_classes then
Class_Memb (class_memb_prefix ^ string_of_int j, [],
- native_ho_type_from_typ type_enc false 0 T,
- `make_class cl)
+ native_ho_type_of_typ type_enc false 0 T, `make_class cl)
else
Formula ((tfree_clause_prefix ^ string_of_int j, ""), Hypothesis,
class_atom type_enc (cl, T), NONE, [])
@@ -2386,8 +2384,8 @@
IConst (`make_bound_var "X", T, [])
|> type_guard_iterm type_enc T
|> AAtom
- |> formula_from_iformula ctxt mono type_enc
- always_guard_var_in_formula (SOME true)
+ |> formula_of_iformula ctxt mono type_enc always_guard_var_in_formula
+ (SOME true)
|> close_formula_universally
|> bound_tvars type_enc true (atomic_types_of T),
NONE, isabelle_info inductiveN helper_rank)
@@ -2423,7 +2421,7 @@
in
Sym_Decl (sym_decl_prefix ^ s, (s, s'),
T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
- |> native_ho_type_from_typ type_enc pred_sym ary
+ |> native_ho_type_of_typ type_enc pred_sym ary
|> not (null T_args)
? curry APi (map (tvar_name o dest_TVar) T_args))
end
@@ -2456,8 +2454,8 @@
|> fold (curry (IApp o swap)) bounds
|> type_guard_iterm type_enc res_T
|> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
- |> formula_from_iformula ctxt mono type_enc
- always_guard_var_in_formula (SOME true)
+ |> formula_of_iformula ctxt mono type_enc
+ always_guard_var_in_formula (SOME true)
|> close_formula_universally
|> bound_tvars type_enc (n > 1) (atomic_types_of T)
|> maybe_negate,
@@ -2544,15 +2542,15 @@
(type_enc as Native (_, _, level)) sym_tab =
let
val thy = Proof_Context.theory_of ctxt
- val ho_term_from_term =
- iterm_from_term thy type_enc []
- #> fst #> ho_term_from_iterm ctxt mono type_enc NONE
+ val ho_term_of_term =
+ iterm_of_term thy type_enc []
+ #> fst #> ho_term_of_iterm ctxt mono type_enc NONE
in
if is_type_enc_polymorphic type_enc then
- [(native_ho_type_from_typ type_enc false 0 @{typ nat},
- map ho_term_from_term [@{term "0::nat"}, @{term Suc}], true) (*,
- (native_ho_type_from_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
- map (ho_term_from_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
+ [(native_ho_type_of_typ type_enc false 0 @{typ nat},
+ map ho_term_of_term [@{term "0::nat"}, @{term Suc}], true) (*,
+ (native_ho_type_of_typ type_enc false 0 (Logic.varifyT_global @{typ "'a list"}),
+ map (ho_term_of_term o Logic.varify_types_global) [@{term Nil}, @{term Cons}],
true) *)]
else
[]
@@ -2584,7 +2582,7 @@
val base_ary = min_ary_of sym_tab0 base_s
fun do_const name = IConst (name, T, T_args)
val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc
- val ho_term_of = ho_term_from_iterm ctxt mono type_enc (SOME true)
+ val ho_term_of = ho_term_of_iterm ctxt mono type_enc (SOME true)
val name1 as (s1, _) =
base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
val name2 as (s2, _) = base_name |> aliased_uncurried ary
--- a/src/HOL/Tools/ATP/atp_proof.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu May 16 13:34:13 2013 +0200
@@ -55,7 +55,7 @@
val parse_formula :
string list
-> (string, 'a, (string, 'a) ho_term, string) formula * string list
- val atp_proof_from_tstplike_proof : string problem -> string -> string proof
+ val atp_proof_of_tstplike_proof : string problem -> string -> string proof
val clean_up_atp_proof_dependencies : string proof -> string proof
val map_term_names_in_atp_proof :
(string -> string) -> string proof -> string proof
@@ -493,8 +493,8 @@
(Scan.repeat1 (parse_line problem))))
#> fst
-fun atp_proof_from_tstplike_proof _ "" = []
- | atp_proof_from_tstplike_proof problem tstp =
+fun atp_proof_of_tstplike_proof _ "" = []
+ | atp_proof_of_tstplike_proof problem tstp =
tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
|> sort (step_name_ord o pairself #1)
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu May 16 13:34:13 2013 +0200
@@ -26,10 +26,10 @@
val forall_of : term -> term -> term
val exists_of : term -> term -> term
val unalias_type_enc : string -> string list
- val term_from_atp :
+ val term_of_atp :
Proof.context -> bool -> int Symtab.table -> typ option ->
(string, string) ho_term -> term
- val prop_from_atp :
+ val prop_of_atp :
Proof.context -> bool -> int Symtab.table ->
(string, string, (string, string) ho_term, string) formula -> term
end;
@@ -97,8 +97,8 @@
(* Type variables are given the basic sort "HOL.type". Some will later be
constrained by information from type literals, or by type inference. *)
-fun typ_from_atp ctxt (u as ATerm ((a, _), us)) =
- let val Ts = map (typ_from_atp ctxt) us in
+fun typ_of_atp ctxt (u as ATerm ((a, _), us)) =
+ let val Ts = map (typ_of_atp ctxt) us in
case unprefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
@@ -117,8 +117,8 @@
(* Type class literal applied to a type. Returns triple of polarity, class,
type. *)
-fun type_constraint_from_term ctxt (u as ATerm ((a, _), us)) =
- case (unprefix_and_unascii class_prefix a, map (typ_from_atp ctxt) us) of
+fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) =
+ case (unprefix_and_unascii class_prefix a, map (typ_of_atp ctxt) us) of
(SOME b, [T]) => (b, T)
| _ => raise HO_TERM [u]
@@ -166,7 +166,7 @@
(* First-order translation. No types are known for variables. "HOLogic.typeT"
should allow them to be inferred. *)
-fun term_from_atp ctxt textual sym_tab =
+fun term_of_atp ctxt textual sym_tab =
let
val thy = Proof_Context.theory_of ctxt
(* For Metis, we use 1 rather than 0 because variable references in clauses
@@ -198,7 +198,7 @@
if s' = type_tag_name then
case mangled_us @ us of
[typ_u, term_u] =>
- do_term extra_ts (SOME (typ_from_atp ctxt typ_u)) term_u
+ do_term extra_ts (SOME (typ_of_atp ctxt typ_u)) term_u
| _ => raise HO_TERM us
else if s' = predicator_name then
do_term [] (SOME @{typ bool}) (hd us)
@@ -223,7 +223,7 @@
val T =
(if not (null type_us) andalso
num_type_args thy s' = length type_us then
- let val Ts = type_us |> map (typ_from_atp ctxt) in
+ let val Ts = type_us |> map (typ_of_atp ctxt) in
if new_skolem then
SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts))
else if textual then
@@ -240,7 +240,7 @@
| NONE => HOLogic.typeT))
val t =
if new_skolem then
- Var ((new_skolem_var_name_from_const s'', var_index), T)
+ Var ((new_skolem_var_name_of_const s'', var_index), T)
else
Const (unproxify_const s', T)
in list_comb (t, term_ts @ extra_ts) end
@@ -277,12 +277,12 @@
in list_comb (t, ts) end
in do_term [] end
-fun term_from_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
+fun term_of_atom ctxt textual sym_tab pos (u as ATerm ((s, _), _)) =
if String.isPrefix class_prefix s then
- add_type_constraint pos (type_constraint_from_term ctxt u)
+ add_type_constraint pos (type_constraint_of_term ctxt u)
#> pair @{const True}
else
- pair (term_from_atp ctxt textual sym_tab (SOME @{typ bool}) u)
+ pair (term_of_atp ctxt textual sym_tab (SOME @{typ bool}) u)
(* Update schematic type variables with detected sort constraints. It's not
totally clear whether this code is necessary. *)
@@ -308,7 +308,7 @@
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
appear in the formula. *)
-fun prop_from_atp ctxt textual sym_tab phi =
+fun prop_of_atp ctxt textual sym_tab phi =
let
fun do_formula pos phi =
case phi of
@@ -329,7 +329,7 @@
| AImplies => s_imp
| AIff => s_iff
| ANot => raise Fail "impossible connective")
- | AAtom tm => term_from_atom ctxt textual sym_tab pos tm
+ | AAtom tm => term_of_atom ctxt textual sym_tab pos tm
| _ => raise FORMULA [phi]
in repair_tvar_sorts (do_formula true phi Vartab.empty) end
--- a/src/HOL/Tools/ATP/atp_util.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Thu May 16 13:34:13 2013 +0200
@@ -17,8 +17,8 @@
val nat_subscript : int -> string
val unyxml : string -> string
val maybe_quote : string -> string
- val string_from_ext_time : bool * Time.time -> string
- val string_from_time : Time.time -> string
+ val string_of_ext_time : bool * Time.time -> string
+ val string_of_time : Time.time -> string
val type_instance : theory -> typ -> typ -> bool
val type_generalization : theory -> typ -> typ -> bool
val type_intersect : theory -> typ -> typ -> bool
@@ -134,7 +134,7 @@
Keyword.is_keyword s) ? quote
end
-fun string_from_ext_time (plus, time) =
+fun string_of_ext_time (plus, time) =
let val ms = Time.toMilliseconds time in
(if plus then "> " else "") ^
(if plus andalso ms mod 1000 = 0 then
@@ -145,7 +145,7 @@
string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
end
-val string_from_time = string_from_ext_time o pair false
+val string_of_time = string_of_ext_time o pair false
fun type_instance thy T T' = Sign.typ_instance thy (T, T')
fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu May 16 13:34:13 2013 +0200
@@ -191,7 +191,7 @@
(* Given the definition of a Skolem function, return a theorem to replace
an existential formula by a use of that function.
Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B" [.] *)
-fun old_skolem_theorem_from_def thy rhs0 =
+fun old_skolem_theorem_of_def thy rhs0 =
let
val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
val rhs' = rhs |> Thm.dest_comb |> snd
@@ -200,7 +200,7 @@
val T =
case hilbert of
Const (_, Type (@{type_name fun}, [_, T])) => T
- | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
+ | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
[hilbert])
val cex = cterm_of thy (HOLogic.exists_const T)
val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
@@ -372,7 +372,7 @@
nnf_axiom choice_ths new_skolem ax_no th ctxt0
fun clausify th =
make_cnf (if new_skolem orelse null choice_ths then []
- else map (old_skolem_theorem_from_def thy) (old_skolem_defs th))
+ else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
th ctxt ctxt
val (cnf_ths, ctxt) = clausify nnf_th
fun intr_imp ct th =
--- a/src/HOL/Tools/Metis/metis_generate.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML Thu May 16 13:34:13 2013 +0200
@@ -138,7 +138,7 @@
val prepare_helper =
Meson.make_meta_clause #> rewrite_rule (map safe_mk_meta_eq proxy_defs)
-fun metis_term_from_atp type_enc (ATerm ((s, []), tms)) =
+fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
if is_tptp_variable s then
Metis_Term.Var (Metis_Name.fromString s)
else
@@ -147,24 +147,23 @@
| NONE => (s, false))
|> (fn (s, swap) =>
Metis_Term.Fn (Metis_Name.fromString s,
- tms |> map (metis_term_from_atp type_enc)
+ tms |> map (metis_term_of_atp type_enc)
|> swap ? rev))
-fun metis_atom_from_atp type_enc (AAtom tm) =
- (case metis_term_from_atp type_enc tm of
+fun metis_atom_of_atp type_enc (AAtom tm) =
+ (case metis_term_of_atp type_enc tm of
Metis_Term.Fn x => x
| _ => raise Fail "non CNF -- expected function")
- | metis_atom_from_atp _ _ = raise Fail "not CNF -- expected atom"
-fun metis_literal_from_atp type_enc (AConn (ANot, [phi])) =
- (false, metis_atom_from_atp type_enc phi)
- | metis_literal_from_atp type_enc phi =
- (true, metis_atom_from_atp type_enc phi)
-fun metis_literals_from_atp type_enc (AConn (AOr, phis)) =
- maps (metis_literals_from_atp type_enc) phis
- | metis_literals_from_atp type_enc phi = [metis_literal_from_atp type_enc phi]
-fun metis_axiom_from_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
+ | metis_atom_of_atp _ _ = raise Fail "not CNF -- expected atom"
+fun metis_literal_of_atp type_enc (AConn (ANot, [phi])) =
+ (false, metis_atom_of_atp type_enc phi)
+ | metis_literal_of_atp type_enc phi = (true, metis_atom_of_atp type_enc phi)
+fun metis_literals_of_atp type_enc (AConn (AOr, phis)) =
+ maps (metis_literals_of_atp type_enc) phis
+ | metis_literals_of_atp type_enc phi = [metis_literal_of_atp type_enc phi]
+fun metis_axiom_of_atp type_enc clauses (Formula ((ident, _), _, phi, _, _)) =
let
fun some isa =
- SOME (phi |> metis_literals_from_atp type_enc
+ SOME (phi |> metis_literals_of_atp type_enc
|> Metis_LiteralSet.fromList
|> Metis_Thm.axiom, isa)
in
@@ -197,7 +196,7 @@
end
| NONE => TrueI |> Isa_Raw |> some
end
- | metis_axiom_from_atp _ _ _ = raise Fail "not CNF -- expected formula"
+ | metis_axiom_of_atp _ _ _ = raise Fail "not CNF -- expected formula"
fun eliminate_lam_wrappers (Const (@{const_name Metis.lambda}, _) $ t) =
eliminate_lam_wrappers t
@@ -251,7 +250,7 @@
(* "rev" is for compatibility with existing proof scripts. *)
val axioms =
atp_problem
- |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
+ |> maps (map_filter (metis_axiom_of_atp type_enc clauses) o snd) |> rev
fun ord_info () = atp_problem_term_order_info atp_problem
in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu May 16 13:34:13 2013 +0200
@@ -13,7 +13,7 @@
exception METIS_RECONSTRUCT of string * string
- val hol_clause_from_metis :
+ val hol_clause_of_metis :
Proof.context -> type_enc -> int Symtab.table
-> (string * term) list * (string * term) list -> Metis_Thm.thm -> term
val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
@@ -36,40 +36,40 @@
exception METIS_RECONSTRUCT of string * string
-fun atp_name_from_metis type_enc s =
+fun atp_name_of_metis type_enc s =
case find_first (fn (_, (f, _)) => f type_enc = s) metis_name_table of
SOME ((s, _), (_, swap)) => (s, swap)
| _ => (s, false)
-fun atp_term_from_metis type_enc (Metis_Term.Fn (s, tms)) =
- let val (s, swap) = atp_name_from_metis type_enc (Metis_Name.toString s) in
- ATerm ((s, []), tms |> map (atp_term_from_metis type_enc) |> swap ? rev)
+fun atp_term_of_metis type_enc (Metis_Term.Fn (s, tms)) =
+ let val (s, swap) = atp_name_of_metis type_enc (Metis_Name.toString s) in
+ ATerm ((s, []), tms |> map (atp_term_of_metis type_enc) |> swap ? rev)
end
- | atp_term_from_metis _ (Metis_Term.Var s) =
+ | atp_term_of_metis _ (Metis_Term.Var s) =
ATerm ((Metis_Name.toString s, []), [])
-fun hol_term_from_metis ctxt type_enc sym_tab =
- atp_term_from_metis type_enc #> term_from_atp ctxt false sym_tab NONE
+fun hol_term_of_metis ctxt type_enc sym_tab =
+ atp_term_of_metis type_enc #> term_of_atp ctxt false sym_tab NONE
-fun atp_literal_from_metis type_enc (pos, atom) =
- atom |> Metis_Term.Fn |> atp_term_from_metis type_enc
+fun atp_literal_of_metis type_enc (pos, atom) =
+ atom |> Metis_Term.Fn |> atp_term_of_metis type_enc
|> AAtom |> not pos ? mk_anot
-fun atp_clause_from_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
- | atp_clause_from_metis type_enc lits =
- lits |> map (atp_literal_from_metis type_enc) |> mk_aconns AOr
+fun atp_clause_of_metis _ [] = AAtom (ATerm ((tptp_false, []), []))
+ | atp_clause_of_metis type_enc lits =
+ lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
fun polish_hol_terms ctxt (lifted, old_skolems) =
map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
#> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
-fun hol_clause_from_metis ctxt type_enc sym_tab concealed =
+fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
Metis_Thm.clause
#> Metis_LiteralSet.toList
- #> atp_clause_from_metis type_enc
- #> prop_from_atp ctxt false sym_tab
+ #> atp_clause_of_metis type_enc
+ #> prop_of_atp ctxt false sym_tab
#> singleton (polish_hol_terms ctxt concealed)
-fun hol_terms_from_metis ctxt type_enc concealed sym_tab fol_tms =
- let val ts = map (hol_term_from_metis ctxt type_enc sym_tab) fol_tms
+fun hol_terms_of_metis ctxt type_enc concealed sym_tab fol_tms =
+ let val ts = map (hol_term_of_metis ctxt type_enc sym_tab) fol_tms
val _ = trace_msg ctxt (fn () => " calling type inference:")
val _ = app (fn t => trace_msg ctxt
(fn () => Syntax.string_of_term ctxt t)) ts
@@ -102,7 +102,7 @@
(* INFERENCE RULE: AXIOM *)
(* This causes variables to have an index of 1 by default. See also
- "term_from_atp" in "ATP_Proof_Reconstruct". *)
+ "term_of_atp" in "ATP_Proof_Reconstruct". *)
val axiom_inference = Thm.incr_indexes 1 oo lookth
(* INFERENCE RULE: ASSUME *)
@@ -118,7 +118,7 @@
fun assume_inference ctxt type_enc concealed sym_tab atom =
inst_excluded_middle
(Proof_Context.theory_of ctxt)
- (singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
+ (singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
(Metis_Term.Fn atom))
(* INFERENCE RULE: INSTANTIATE (SUBST). Type instantiations are ignored. Trying
@@ -134,14 +134,14 @@
fun subst_translation (x,y) =
let val v = find_var x
(* We call "polish_hol_terms" below. *)
- val t = hol_term_from_metis ctxt type_enc sym_tab y
+ val t = hol_term_of_metis ctxt type_enc sym_tab y
in SOME (cterm_of thy (Var v), t) end
handle Option.Option =>
(trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
| TYPE _ =>
- (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
+ (trace_msg ctxt (fn () => "\"hol_term_of_metis\" failed for " ^ x ^
" in " ^ Display.string_of_thm ctxt i_th);
NONE)
fun remove_typeinst (a, t) =
@@ -275,7 +275,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_atom =
- singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab)
+ singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab)
(Metis_Term.Fn atom)
val _ = trace_msg ctxt (fn () =>
" atom: " ^ Syntax.string_of_term ctxt i_atom)
@@ -309,7 +309,7 @@
let
val thy = Proof_Context.theory_of ctxt
val i_t =
- singleton (hol_terms_from_metis ctxt type_enc concealed sym_tab) t
+ singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) t
val _ = trace_msg ctxt (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end
@@ -323,7 +323,7 @@
let val thy = Proof_Context.theory_of ctxt
val m_tm = Metis_Term.Fn atom
val [i_atom, i_tm] =
- hol_terms_from_metis ctxt type_enc concealed sym_tab [m_tm, fr]
+ hol_terms_of_metis ctxt type_enc concealed sym_tab [m_tm, fr]
val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Markup.print_bool pos)
fun replace_item_list lx 0 (_::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu May 16 13:34:13 2013 +0200
@@ -47,9 +47,9 @@
"t => t'", where "t" and "t'" are the same term modulo type tags.
In Isabelle, type tags are stripped away, so we are left with "t = t" or
"t => t". Type tag idempotence is also handled this way. *)
-fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth =
+fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
let val thy = Proof_Context.theory_of ctxt in
- case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of
+ case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
Const (@{const_name HOL.eq}, _) $ _ $ t =>
let
val ct = cterm_of thy t
@@ -62,11 +62,11 @@
end
|> Meson.make_meta_clause
-fun lam_lifted_from_metis ctxt type_enc sym_tab concealed mth =
+fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
let
val thy = Proof_Context.theory_of ctxt
val tac = rewrite_goals_tac @{thms lambda_def [abs_def]} THEN rtac refl 1
- val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth
+ val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
@@ -158,13 +158,13 @@
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
- val type_enc = type_enc_from_string Strict type_enc
+ val type_enc = type_enc_of_string Strict type_enc
val (sym_tab, axioms, ord_info, concealed) =
prepare_metis_problem ctxt type_enc lam_trans cls ths
fun get_isa_thm mth Isa_Reflexive_or_Trivial =
- reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
+ reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth
| get_isa_thm mth Isa_Lambda_Lifted =
- lam_lifted_from_metis ctxt type_enc sym_tab concealed mth
+ lam_lifted_of_metis ctxt type_enc sym_tab concealed mth
| get_isa_thm _ (Isa_Raw ith) = ith
val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith))
val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES")
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu May 16 13:34:13 2013 +0200
@@ -1051,7 +1051,7 @@
(print_nt (fn () => excipit "ran out of time after checking");
if !met_potential > 0 then potentialN else unknownN)
val _ = print_v (fn () =>
- "Total time: " ^ string_from_time (Timer.checkRealTimer timer) ^
+ "Total time: " ^ string_of_time (Timer.checkRealTimer timer) ^
".")
in (outcome_code, !state_ref) end
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Thu May 16 13:34:13 2013 +0200
@@ -52,7 +52,7 @@
val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
- val string_from_time : Time.time -> string
+ val string_of_time : Time.time -> string
val nat_subscript : int -> string
val flip_polarity : polarity -> polarity
val prop_T : typ
@@ -237,7 +237,7 @@
val parse_bool_option = Sledgehammer_Util.parse_bool_option
val parse_time_option = Sledgehammer_Util.parse_time_option
-val string_from_time = ATP_Util.string_from_time
+val string_of_time = ATP_Util.string_of_time
val i_subscript = implode o map (prefix "\<^isub>") o Symbol.explode
fun nat_subscript n =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu May 16 13:34:13 2013 +0200
@@ -21,7 +21,7 @@
val ignore_no_atp : bool Config.T
val instantiate_inducts : bool Config.T
val no_fact_override : fact_override
- val fact_from_ref :
+ val fact_of_ref :
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
val backquote_thm : Proof.context -> thm -> string
@@ -119,7 +119,7 @@
fun stature_of_thm global assms chained css name th =
(scope_of_thm global assms chained th, status_of_thm css name th)
-fun fact_from_ref ctxt reserved chained css (xthm as (xref, args)) =
+fun fact_of_ref ctxt reserved chained css (xthm as (xref, args)) =
let
val ths = Attrib.eval_thms ctxt [xthm]
val bracket =
@@ -502,7 +502,7 @@
in
(if only then
maps (map (fn ((name, stature), th) => ((K name, stature), th))
- o fact_from_ref ctxt reserved chained css) add
+ o fact_of_ref ctxt reserved chained css) add
else
let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
all_facts ctxt false ho_atp reserved add chained css
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu May 16 13:34:13 2013 +0200
@@ -159,7 +159,7 @@
| _ => value)
| NONE => (name, value)
-val any_type_enc = type_enc_from_string Strict "erased"
+val any_type_enc = type_enc_of_string Strict "erased"
(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
can be omitted. For the last four, this is a secret feature. *)
@@ -171,9 +171,9 @@
else if null value then
if is_prover_list ctxt name then
("provers", [name])
- else if can (type_enc_from_string Strict) name then
+ else if can (type_enc_of_string Strict) name then
("type_enc", [name])
- else if can (trans_lams_from_string ctxt any_type_enc) name then
+ else if can (trans_lams_of_string ctxt any_type_enc) name then
("lam_trans", [name])
else if member (op =) fact_filters name then
("fact_filter", [name])
@@ -295,7 +295,7 @@
NONE
else case lookup_string "type_enc" of
"smart" => NONE
- | s => (type_enc_from_string Strict s; SOME s)
+ | s => (type_enc_of_string Strict s; SOME s)
val strict = mode = Auto_Try orelse lookup_bool "strict"
val lam_trans = lookup_option lookup_string "lam_trans"
val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu May 16 13:34:13 2013 +0200
@@ -1024,7 +1024,7 @@
"Learned " ^ string_of_int num_proofs ^ " " ^
(if run_prover then "automatic" else "Isar") ^ " proof" ^
plural_s num_proofs ^ " in the last " ^
- string_from_time commit_timeout ^ "."
+ string_of_time commit_timeout ^ "."
|> Output.urgent_message
end
else
@@ -1111,10 +1111,8 @@
if verbose orelse auto_level < 2 then
"Learned " ^ string_of_int n ^ " nontrivial " ^
(if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
- (if verbose then
- " in " ^ string_from_time (Timer.checkRealTimer timer)
- else
- "") ^ "."
+ (if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
+ else "") ^ "."
else
""
end
@@ -1138,7 +1136,7 @@
("MaShing through " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^ " for automatic proofs (" ^ quote prover ^
(case timeout of
- SOME timeout => " timeout: " ^ string_from_time timeout
+ SOME timeout => " timeout: " ^ string_of_time timeout
| NONE => "") ^ ").\n\nCollecting Isar proofs first..."
|> Output.urgent_message;
learn 1 false;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu May 16 13:34:13 2013 +0200
@@ -65,7 +65,7 @@
"Testing " ^ n_facts (map fst facts) ^
(if verbose then
case timeout of
- SOME timeout => " (timeout: " ^ string_from_time timeout ^ ")"
+ SOME timeout => " (timeout: " ^ string_of_time timeout ^ ")"
| _ => ""
else
"") ^ "...")
@@ -96,7 +96,7 @@
"Found proof" ^
(if length used_facts = length facts then ""
else " with " ^ n_facts used_facts) ^
- " (" ^ string_from_time run_time ^ ").");
+ " (" ^ string_of_time run_time ^ ").");
result
end
@@ -351,7 +351,7 @@
val css = clasimpset_rule_table_of ctxt
val facts =
refs |> maps (map (apsnd single)
- o fact_from_ref ctxt reserved chained_ths css)
+ o fact_of_ref ctxt reserved chained_ths css)
in
case subgoal_count state of
0 => Output.urgent_message "No subgoal!"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu May 16 13:34:13 2013 +0200
@@ -36,7 +36,7 @@
fun add_preplay_time (b1, t1) (b2, t2) = (b1 orelse b2, Time.+(t1,t2))
-val string_of_preplay_time = ATP_Util.string_from_ext_time
+val string_of_preplay_time = ATP_Util.string_of_ext_time
(* preplay tracing *)
fun preplay_trace ctxt assms concl time =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 16 13:34:13 2013 +0200
@@ -530,7 +530,7 @@
if verbose then
"Trying \"" ^ string_of_reconstructor reconstr ^ "\"" ^
(case timeout of
- SOME timeout => " for " ^ string_from_time timeout
+ SOME timeout => " for " ^ string_of_time timeout
| NONE => "") ^ "..."
|> Output.urgent_message
else
@@ -616,7 +616,7 @@
fun choose_type_enc soundness best_type_enc format =
the_default best_type_enc
- #> type_enc_from_string soundness
+ #> type_enc_of_string soundness
#> adjust_type_enc format
fun isar_proof_reconstructor ctxt name =
@@ -793,7 +793,7 @@
" with " ^ string_of_int num_facts ^ " fact" ^
plural_s num_facts ^
(case slice_timeout of
- SOME timeout => " for " ^ string_from_time timeout
+ SOME timeout => " for " ^ string_of_time timeout
| NONE => "") ^ "..."
|> Output.urgent_message
else
@@ -849,7 +849,7 @@
(accum, facts,
extract_tstplike_proof_and_outcome verbose proof_delims
known_failures output
- |>> atp_proof_from_tstplike_proof atp_problem
+ |>> atp_proof_of_tstplike_proof atp_problem
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))
handle TimeLimit.TimeOut =>
@@ -921,7 +921,7 @@
val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
val reconstrs =
bunch_of_reconstructors needs_full_types
- (lam_trans_from_atp_proof atp_proof
+ (lam_trans_of_atp_proof atp_proof
o (fn desperate => if desperate then hide_lamsN
else metis_default_lam_trans))
in
@@ -955,7 +955,7 @@
one_line_params
end,
(if verbose then
- "\nATP real CPU time: " ^ string_from_time run_time ^ "."
+ "\nATP real CPU time: " ^ string_of_time run_time ^ "."
else
"") ^
(if important_message <> "" then
@@ -991,17 +991,16 @@
(139, Crashed)]
val smt_failures = remote_smt_failures @ z3_failures @ unix_failures
-fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
+fun failure_of_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
if is_real_cex then Unprovable else GaveUp
- | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
- | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
+ | failure_of_smt_failure SMT_Failure.Time_Out = TimedOut
+ | failure_of_smt_failure (SMT_Failure.Abnormal_Termination code) =
(case AList.lookup (op =) smt_failures code of
SOME failure => failure
| NONE => UnknownError ("Abnormal termination with exit code " ^
string_of_int code ^ "."))
- | failure_from_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
- | failure_from_smt_failure (SMT_Failure.Other_Failure msg) =
- UnknownError msg
+ | failure_of_smt_failure SMT_Failure.Out_Of_Memory = OutOfResources
+ | failure_of_smt_failure (SMT_Failure.Other_Failure s) = UnknownError s
(* FUDGE *)
val smt_max_slices =
@@ -1059,7 +1058,7 @@
quote name ^ " slice " ^ string_of_int slice ^ " with " ^
string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
(case slice_timeout of
- SOME timeout => " for " ^ string_from_time timeout
+ SOME timeout => " for " ^ string_of_time timeout
| NONE => "") ^ "..."
|> Output.urgent_message
else
@@ -1112,7 +1111,7 @@
if verbose andalso is_some outcome then
quote name ^ " invoked with " ^
num_of_facts fact_filter num_facts ^ ": " ^
- string_of_failure (failure_from_smt_failure (the outcome)) ^
+ string_of_failure (failure_of_smt_failure (the outcome)) ^
" Retrying with " ^ num_of_facts new_fact_filter new_num_facts ^
"..."
|> Output.urgent_message
@@ -1142,7 +1141,7 @@
val {outcome, used_facts = used_pairs, used_from, run_time} =
smt_filter_loop name params state goal subgoal weighted_factss
val used_facts = used_pairs |> map fst
- val outcome = outcome |> Option.map failure_from_smt_failure
+ val outcome = outcome |> Option.map failure_of_smt_failure
val (preplay, message, message_tail) =
case outcome of
NONE =>
@@ -1161,7 +1160,7 @@
val num_chained = length (#facts (Proof.goal state))
in one_line_proof_text num_chained one_line_params end,
if verbose then
- "\nSMT solver real CPU time: " ^ string_from_time run_time ^ "."
+ "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
else
"")
| SOME failure =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu May 16 13:19:27 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu May 16 13:34:13 2013 +0200
@@ -28,7 +28,7 @@
val smtN : string
val string_of_reconstructor : reconstructor -> string
- val lam_trans_from_atp_proof : string proof -> string -> string
+ val lam_trans_of_atp_proof : string proof -> string -> string
val is_typed_helper_used_in_atp_proof : string proof -> bool
val used_facts_in_atp_proof :
Proof.context -> (string * stature) list vector -> string proof ->
@@ -121,7 +121,7 @@
fun is_axiom_used_in_proof pred =
exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
-fun lam_trans_from_atp_proof atp_proof default =
+fun lam_trans_of_atp_proof atp_proof default =
case (is_axiom_used_in_proof is_combinator_def atp_proof,
is_axiom_used_in_proof is_lam_lifted atp_proof) of
(false, false) => default
@@ -190,7 +190,7 @@
(** one-liner reconstructor proofs **)
fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")"
+ | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
(* FIXME: Various bugs, esp. with "unfolding"
fun unusing_chained_facts _ 0 = ""
@@ -279,12 +279,12 @@
| label_of_clause c =
(space_implode "___" (map (fst o raw_label_of_name) c), 0)
-fun add_fact_from_dependencies fact_names (names as [(_, ss)]) =
+fun add_fact_of_dependencies fact_names (names as [(_, ss)]) =
if is_fact fact_names ss then
apsnd (union (op =) (map fst (resolve_fact fact_names ss)))
else
apfst (insert (op =) (label_of_clause names))
- | add_fact_from_dependencies fact_names names =
+ | add_fact_of_dependencies fact_names names =
apfst (insert (op =) (label_of_clause names))
fun repair_name "$true" = "c_True"
@@ -325,7 +325,7 @@
fun decode_line sym_tab (name, role, u, rule, deps) ctxt =
let
val thy = Proof_Context.theory_of ctxt
- val t = u |> prop_from_atp ctxt true sym_tab
+ val t = u |> prop_of_atp ctxt true sym_tab
|> uncombine_term thy |> infer_formula_types ctxt
in
((name, role, t, rule, deps),
@@ -648,7 +648,7 @@
val type_enc =
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
else partial_typesN
- val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans
+ val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans
val preplay = preplay_timeout <> SOME Time.zeroTime
fun isar_proof_of () =
@@ -744,7 +744,7 @@
val t = prop_of_clause c
val by =
By_Metis ([],
- (fold (add_fact_from_dependencies fact_names)
+ (fold (add_fact_of_dependencies fact_names)
gamma no_facts))
fun prove by = Prove (maybe_show outer c [], l, t, by)
fun do_rest l step =