diff -r 9f6f0a89d16b -r 9a9238342963 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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