--- 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),