# HG changeset patch # User blanchet # Date 1310904695 -7200 # Node ID b7890554c424d122aadd7c2e0ed001a7a1f54a57 # Parent be41d12de6fa61d45cb7f85d814b5bc5ff981eb5 renamed internal data structure diff -r be41d12de6fa -r b7890554c424 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:35 2011 +0200 @@ -447,21 +447,22 @@ fun make_class_rel_clauses thy subs supers = map make_class_rel_clause (class_pairs thy subs supers) -datatype combterm = - CombConst of name * typ * typ list | - CombVar of name * typ | - CombApp of combterm * combterm | - CombAbs of (name * typ) * combterm +(* intermediate terms *) +datatype iterm = + IConst of name * typ * typ list | + IVar of name * typ | + IApp of iterm * iterm | + IAbs of (name * typ) * iterm -fun combtyp_of (CombConst (_, T, _)) = T - | combtyp_of (CombVar (_, T)) = T - | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1)) - | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm +fun ityp_of (IConst (_, T, _)) = T + | ityp_of (IVar (_, T)) = T + | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1)) + | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm (*gets the head of a combinator application, along with the list of arguments*) -fun strip_combterm_comb u = +fun strip_iterm_comb u = let - fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts) + fun stripc (IApp (t, u), ts) = stripc (t, u :: ts) | stripc x = x in stripc (u, []) end @@ -471,42 +472,41 @@ [new_skolem_const_prefix, s, string_of_int num_T_args] |> space_implode Long_Name.separator -(* Converts a term (with combinators) into a combterm. Also accumulates sort - infomation. *) -fun combterm_from_term thy bs (P $ Q) = +(* Converts an Isabelle/HOL term (with combinators) into an intermediate term. + Also accumulates sort infomation. *) +fun iterm_from_term thy bs (P $ Q) = let - val (P', P_atomics_Ts) = combterm_from_term thy bs P - val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q - in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end - | combterm_from_term thy _ (Const (c, T)) = + val (P', P_atomics_Ts) = iterm_from_term thy bs P + val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q + in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end + | iterm_from_term thy _ (Const (c, T)) = let val tvar_list = (if String.isPrefix old_skolem_const_prefix c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy) - val c' = CombConst (`make_fixed_const c, T, tvar_list) + val c' = IConst (`make_fixed_const c, T, tvar_list) in (c', atyps_of T) end - | combterm_from_term _ _ (Free (v, T)) = - (CombConst (`make_fixed_var v, T, []), atyps_of T) - | combterm_from_term _ _ (Var (v as (s, _), T)) = + | iterm_from_term _ _ (Free (v, T)) = + (IConst (`make_fixed_var v, T, []), atyps_of T) + | iterm_from_term _ _ (Var (v as (s, _), T)) = (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then let val Ts = T |> strip_type |> swap |> op :: val s' = new_skolem_const_name s (length Ts) - in CombConst (`make_fixed_const s', T, Ts) end + in IConst (`make_fixed_const s', T, Ts) end else - CombVar ((make_schematic_var v, s), T), atyps_of T) - | combterm_from_term _ bs (Bound j) = - nth bs j - |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T)) - | combterm_from_term thy bs (Abs (s, T, t)) = + IVar ((make_schematic_var v, s), T), atyps_of T) + | iterm_from_term _ bs (Bound j) = + nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T)) + | iterm_from_term thy 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 (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t + val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t in - (CombAbs ((`make_bound_var s, T), tm), + (IAbs ((`make_bound_var s, T), tm), union (op =) atomic_Ts (atyps_of T)) end @@ -621,15 +621,15 @@ {name : string, locality : locality, kind : formula_kind, - combformula : (name, typ, combterm) formula, + iformula : (name, typ, iterm) formula, atomic_types : typ list} -fun update_combformula f ({name, locality, kind, combformula, atomic_types} - : translated_formula) = - {name = name, locality = locality, kind = kind, combformula = f combformula, +fun update_iformula f ({name, locality, kind, iformula, atomic_types} + : translated_formula) = + {name = name, locality = locality, kind = kind, iformula = f iformula, atomic_types = atomic_types} : translated_formula -fun fact_lift f ({combformula, ...} : translated_formula) = f combformula +fun fact_lift f ({iformula, ...} : translated_formula) = f iformula val type_instance = Sign.typ_instance o Proof_Context.theory_of @@ -712,11 +712,11 @@ |> filter_out (member (op =) bounds o fst)) in mk_aquant AForall (formula_vars [] phi []) phi end -fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2] - | combterm_vars (CombConst _) = I - | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T) - | combterm_vars (CombAbs (_, tm)) = combterm_vars tm -fun close_combformula_universally phi = close_universally combterm_vars phi +fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2] + | iterm_vars (IConst _) = I + | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T) + | iterm_vars (IAbs (_, tm)) = iterm_vars tm +fun close_iformula_universally phi = close_universally iterm_vars phi fun term_vars bounds (ATerm (name as (s, _), tms)) = (is_tptp_variable s andalso not (member (op =) bounds name)) @@ -816,9 +816,9 @@ fun introduce_proxies type_enc = let - fun intro top_level (CombApp (tm1, tm2)) = - CombApp (intro top_level tm1, intro false tm2) - | intro top_level (CombConst (name as (s, _), T, T_args)) = + fun intro top_level (IApp (tm1, tm2)) = + IApp (intro top_level tm1, intro false tm2) + | intro top_level (IConst (name as (s, _), T, T_args)) = (case proxify_const s of SOME proxy_base => if top_level orelse is_type_enc_higher_order type_enc then @@ -838,15 +838,15 @@ else (proxy_base |>> prefix const_prefix, T_args) | NONE => (name, T_args)) - |> (fn (name, T_args) => CombConst (name, T, T_args)) - | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm) + |> (fn (name, T_args) => IConst (name, T, T_args)) + | intro _ (IAbs (bound, tm)) = IAbs (bound, intro false tm) | intro _ tm = tm in intro true end -fun combformula_from_prop thy type_enc eq_as_iff = +fun iformula_from_prop thy type_enc eq_as_iff = let fun do_term bs t atomic_types = - combterm_from_term thy bs (Envir.eta_contract t) + iterm_from_term thy bs (Envir.eta_contract t) |>> (introduce_proxies type_enc #> AAtom) ||> union (op =) atomic_types fun do_quant bs q s T t' = @@ -986,10 +986,10 @@ (* making fact and conjecture formulas *) fun make_formula thy type_enc eq_as_iff name loc kind t = let - val (combformula, atomic_types) = - combformula_from_prop thy type_enc eq_as_iff t [] + val (iformula, atomic_types) = + iformula_from_prop thy type_enc eq_as_iff t [] in - {name = name, locality = loc, kind = kind, combformula = combformula, + {name = name, locality = loc, kind = kind, iformula = iformula, atomic_types = atomic_types} end @@ -999,7 +999,7 @@ case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name loc Axiom of - formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} => + formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => if s = tptp_true then NONE else SOME formula | formula => SOME formula end @@ -1017,7 +1017,7 @@ (Conjecture, I) else (prem_kind, - if prem_kind = Conjecture then update_combformula mk_anot + if prem_kind = Conjecture then update_iformula mk_anot else I) in t |> preproc ? @@ -1054,9 +1054,9 @@ should_encode_type ctxt nonmono_Ts level T | should_predicate_on_type _ _ _ _ _ = false -fun is_var_or_bound_var (CombConst ((s, _), _, _)) = +fun is_var_or_bound_var (IConst ((s, _), _, _)) = String.isPrefix bound_var_prefix s - | is_var_or_bound_var (CombVar _) = true + | is_var_or_bound_var (IVar _) = true | is_var_or_bound_var _ = false datatype tag_site = @@ -1096,7 +1096,7 @@ type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list} -fun add_combterm_syms_to_table ctxt explicit_apply = +fun add_iterm_syms_to_table ctxt explicit_apply = let fun consider_var_arity const_T var_T max_ary = let @@ -1128,9 +1128,9 @@ else accum fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) = - let val (head, args) = strip_combterm_comb tm in + let val (head, args) = strip_iterm_comb tm in (case head of - CombConst ((s, _), T, _) => + IConst ((s, _), T, _) => if String.isPrefix bound_var_prefix s then add_var_or_bound_var T accum else @@ -1170,16 +1170,15 @@ sym_tab end) end - | CombVar (_, T) => add_var_or_bound_var T accum - | CombAbs ((_, T), tm) => - accum |> add_var_or_bound_var T |> add false tm + | IVar (_, T) => add_var_or_bound_var T accum + | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm | _ => accum) |> fold (add false) args end in add true end fun add_fact_syms_to_table ctxt explicit_apply = fact_lift (formula_fold NONE - (K (add_combterm_syms_to_table ctxt explicit_apply))) + (K (add_iterm_syms_to_table ctxt explicit_apply))) val default_sym_tab_entries : (string * sym_info) list = (prefixed_predicator_name, @@ -1219,33 +1218,32 @@ | NONE => false val predicator_combconst = - CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) -fun predicator tm = CombApp (predicator_combconst, tm) + IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) +fun predicator tm = IApp (predicator_combconst, tm) -fun introduce_predicators_in_combterm sym_tab tm = - case strip_combterm_comb tm of - (CombConst ((s, _), _, _), _) => +fun introduce_predicators_in_iterm sym_tab tm = + case strip_iterm_comb tm of + (IConst ((s, _), _, _), _) => if is_pred_sym sym_tab s then tm else predicator tm | _ => predicator tm -fun list_app head args = fold (curry (CombApp o swap)) args head +fun list_app head args = fold (curry (IApp o swap)) args head val app_op = `make_fixed_const app_op_name fun explicit_app arg head = let - val head_T = combtyp_of head + val head_T = ityp_of head val (arg_T, res_T) = dest_funT head_T - val explicit_app = - CombConst (app_op, head_T --> head_T, [arg_T, res_T]) + val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T]) in list_app explicit_app [head, arg] end fun list_explicit_app head args = fold explicit_app args head -fun introduce_explicit_apps_in_combterm sym_tab = +fun introduce_explicit_apps_in_iterm sym_tab = let fun aux tm = - case strip_combterm_comb tm of - (head as CombConst ((s, _), _, _), args) => + case strip_iterm_comb tm of + (head as IConst ((s, _), _, _), args) => args |> map aux |> chop (min_arity_of sym_tab s) |>> list_app head @@ -1279,12 +1277,11 @@ end handle TYPE _ => T_args -fun enforce_type_arg_policy_in_combterm ctxt format type_enc = +fun enforce_type_arg_policy_in_iterm ctxt format type_enc = let val thy = Proof_Context.theory_of ctxt - fun aux arity (CombApp (tm1, tm2)) = - CombApp (aux (arity + 1) tm1, aux 0 tm2) - | aux arity (CombConst (name as (s, _), T, T_args)) = + fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2) + | aux arity (IConst (name as (s, _), T, T_args)) = (case strip_prefix_and_unascii const_prefix s of NONE => (name, T_args) | SOME s'' => @@ -1301,19 +1298,18 @@ name, []) | No_Type_Args => (name, []) end) - |> (fn (name, T_args) => CombConst (name, T, T_args)) - | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm) + |> (fn (name, T_args) => IConst (name, T, T_args)) + | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm) | aux _ tm = tm in aux 0 end -fun repair_combterm ctxt format type_enc sym_tab = +fun repair_iterm ctxt format type_enc sym_tab = not (is_type_enc_higher_order type_enc) - ? (introduce_explicit_apps_in_combterm sym_tab - #> introduce_predicators_in_combterm sym_tab) - #> enforce_type_arg_policy_in_combterm ctxt format type_enc + ? (introduce_explicit_apps_in_iterm sym_tab + #> introduce_predicators_in_iterm sym_tab) + #> enforce_type_arg_policy_in_iterm ctxt format type_enc fun repair_fact ctxt format type_enc sym_tab = - update_combformula (formula_map - (repair_combterm ctxt format type_enc sym_tab)) + update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab)) (** Helper facts **) @@ -1490,9 +1486,9 @@ val type_pred = `make_fixed_const type_pred_name -fun type_pred_combterm ctxt format type_enc T tm = - CombApp (CombConst (type_pred, T --> @{typ bool}, [T]) - |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm) +fun type_pred_iterm ctxt format type_enc T tm = + IApp (IConst (type_pred, T --> @{typ bool}, [T]) + |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm) fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum = @@ -1506,16 +1502,16 @@ ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args) fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm = - CombConst (type_tag, T --> T, [T]) - |> enforce_type_arg_policy_in_combterm ctxt format type_enc - |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos) + IConst (type_tag, T --> T, [T]) + |> enforce_type_arg_policy_in_iterm ctxt format type_enc + |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos) |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]) | _ => raise Fail "unexpected lambda-abstraction") -and ho_term_from_combterm ctxt format nonmono_Ts type_enc = +and ho_term_from_iterm ctxt format nonmono_Ts type_enc = let fun aux site u = let - val (head, args) = strip_combterm_comb u + val (head, args) = strip_iterm_comb u val pos = case site of Top_Level pos => pos @@ -1523,17 +1519,19 @@ | Elsewhere => NONE val t = case head of - CombConst (name as (s, _), _, T_args) => + IConst (name as (s, _), _, T_args) => let val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere in mk_aterm format type_enc name T_args (map (aux arg_site) args) end - | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args) - | CombAbs ((name, T), tm) => - AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm) - | CombApp _ => raise Fail "impossible \"CombApp\"" - val T = combtyp_of u + | IVar (name, _) => + mk_aterm format type_enc name [] (map (aux Elsewhere) args) + | IAbs ((name, T), tm) => + AAbs ((name, ho_type_from_typ format type_enc true 0 T), + aux Elsewhere tm) + | IApp _ => raise Fail "impossible \"IApp\"" + val T = ityp_of u in t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then tag_with_type ctxt format nonmono_Ts type_enc pos T @@ -1541,11 +1539,11 @@ I) end in aux end -and formula_from_combformula ctxt format nonmono_Ts type_enc - should_predicate_on_var = +and formula_from_iformula ctxt format nonmono_Ts type_enc + should_predicate_on_var = let fun do_term pos = - ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos) + ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos) val do_bound_type = case type_enc of Simple_Types (_, level) => @@ -1555,8 +1553,8 @@ fun do_out_of_bound_type pos phi universal (name, T) = if should_predicate_on_type ctxt nonmono_Ts type_enc (fn () => should_predicate_on_var pos phi universal name) T then - CombVar (name, T) - |> type_pred_combterm ctxt format type_enc T + IVar (name, T) + |> type_pred_iterm ctxt format type_enc T |> do_term pos |> AAtom |> SOME else NONE @@ -1587,14 +1585,14 @@ of monomorphization). The TPTP explicitly forbids name clashes, and some of the remote provers might care. *) fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts - type_enc (j, {name, locality, kind, combformula, atomic_types}) = + type_enc (j, {name, locality, kind, iformula, atomic_types}) = (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind, - combformula - |> close_combformula_universally - |> formula_from_combformula ctxt format nonmono_Ts type_enc - should_predicate_on_var_in_formula - (if pos then SOME true else NONE) + iformula + |> close_iformula_universally + |> formula_from_iformula ctxt format nonmono_Ts type_enc + should_predicate_on_var_in_formula + (if pos then SOME true else NONE) |> bound_tvars type_enc atomic_types |> close_formula_universally, NONE, @@ -1629,11 +1627,11 @@ |> close_formula_universally, isabelle_info introN, NONE) fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc - ({name, kind, combformula, atomic_types, ...} : translated_formula) = + ({name, kind, iformula, atomic_types, ...} : translated_formula) = Formula (conjecture_prefix ^ name, kind, - formula_from_combformula ctxt format nonmono_Ts type_enc + formula_from_iformula ctxt format nonmono_Ts type_enc should_predicate_on_var_in_formula (SOME false) - (close_combformula_universally combformula) + (close_iformula_universally iformula) |> bound_tvars type_enc atomic_types |> close_formula_universally, NONE, NONE) @@ -1661,10 +1659,10 @@ fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) = let - fun add_combterm in_conj tm = - let val (head, args) = strip_combterm_comb tm in + fun add_iterm in_conj tm = + let val (head, args) = strip_iterm_comb tm in (case head of - CombConst ((s, s'), T, T_args) => + IConst ((s, s'), T, T_args) => let val pred_sym = is_pred_sym repaired_sym_tab s in if should_declare_sym type_enc pred_sym s then Symtab.map_default (s, []) @@ -1673,12 +1671,11 @@ else I end - | CombAbs (_, tm) => add_combterm in_conj tm + | IAbs (_, tm) => add_iterm in_conj tm | _ => I) - #> fold (add_combterm in_conj) args + #> fold (add_iterm in_conj) args end - fun add_fact in_conj = - fact_lift (formula_fold NONE (K (add_combterm in_conj))) + fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj))) in Symtab.empty |> is_type_enc_fairly_sound type_enc @@ -1687,10 +1684,9 @@ (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it out with monotonicity" paper presented at CADE 2011. *) -fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I - | add_combterm_nonmonotonic_types ctxt level sound locality _ - (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1), - tm2)) = +fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I + | add_iterm_nonmonotonic_types ctxt level sound locality _ + (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) = (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso (case level of Noninf_Nonmono_Types => @@ -1698,12 +1694,12 @@ not (is_type_surely_infinite ctxt sound T) | Fin_Nonmono_Types => is_type_surely_finite ctxt false T | _ => true)) ? insert_type ctxt I (deep_freeze_type T) - | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I + | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I fun add_fact_nonmonotonic_types ctxt level sound - ({kind, locality, combformula, ...} : translated_formula) = + ({kind, locality, iformula, ...} : translated_formula) = formula_fold (SOME (kind <> Conjecture)) - (add_combterm_nonmonotonic_types ctxt level sound locality) - combformula + (add_iterm_nonmonotonic_types ctxt level sound locality) + iformula fun nonmonotonic_types_for_facts ctxt type_enc sound facts = let val level = level_of_type_enc type_enc in if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then @@ -1740,7 +1736,7 @@ val bound_names = 1 upto num_args |> map (`I o make_bound_var o string_of_int) val bounds = - bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, [])) + bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, [])) val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args fun should_keep_arg_type T = sym_needs_arg_types orelse @@ -1750,12 +1746,12 @@ in Formula (preds_sym_formula_prefix ^ s ^ (if n > 1 then "_" ^ string_of_int j else ""), kind, - CombConst ((s, s'), T, T_args) - |> fold (curry (CombApp o swap)) bounds - |> type_pred_combterm ctxt format type_enc res_T + IConst ((s, s'), T, T_args) + |> fold (curry (IApp o swap)) bounds + |> type_pred_iterm ctxt format type_enc res_T |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts) - |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc - (K (K (K (K true)))) (SOME true) + |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc + (K (K (K (K true)))) (SOME true) |> n > 1 ? bound_tvars type_enc (atyps_of T) |> close_formula_universally |> maybe_negate,