# HG changeset patch # User nik # Date 1314276952 -3600 # Node ID 4c2242c8a96c8f2abb91b7df0a7b46562b9f1dc7 # Parent a77901b3774ec75174d5298700b37ff15ceb7a90 added choice operator output for Satallax diff -r a77901b3774e -r 4c2242c8a96c src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Aug 25 14:25:07 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Aug 25 13:55:52 2011 +0100 @@ -50,6 +50,7 @@ val tptp_ho_forall : string val tptp_exists : string val tptp_ho_exists : string + val tptp_choice : string val tptp_not : string val tptp_and : string val tptp_or : string @@ -147,6 +148,7 @@ val tptp_ho_forall = "!!" val tptp_exists = "?" val tptp_ho_exists = "??" +val tptp_choice = "@+" val tptp_not = "~" val tptp_and = "&" val tptp_or = "|" @@ -264,13 +266,21 @@ space_implode (" " ^ tptp_equal ^ " ") (map (string_for_term format) ts) |> is_format_thf format ? enclose "(" ")" else - (case (s = tptp_ho_forall orelse s = tptp_ho_exists, ts) of - (true, [AAbs ((s', ty), tm)]) => + (case (s = tptp_ho_forall orelse s = tptp_ho_exists, + s = tptp_choice andalso format = THF With_Choice, ts) of + (true, _, [AAbs ((s', ty), tm)]) => (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work around LEO-II 1.2.8 parser limitation. *) string_for_formula format (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) + | (_, true, [AAbs ((s', ty), tm)]) => + (*There is code in ATP_Translate to ensure that Eps is always applied + to an abstraction*) + tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "] : " ^ + string_for_term format tm ^ "" + |> enclose "(" ")" + | _ => let val ss = map (string_for_term format) ts in if is_format_thf format then diff -r a77901b3774e -r 4c2242c8a96c src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Aug 25 14:25:07 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Aug 25 13:55:52 2011 +0100 @@ -308,8 +308,10 @@ fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x)) (* "HOL.eq" is mapped to the ATP's equality. *) -fun make_fixed_const @{const_name HOL.eq} = tptp_old_equal - | make_fixed_const c = const_prefix ^ lookup_const c +fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal + | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) = + tptp_choice + | make_fixed_const _ c = const_prefix ^ lookup_const c fun make_fixed_type_const c = type_const_prefix ^ lookup_const c @@ -483,38 +485,38 @@ (* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort infomation. *) -fun iterm_from_term thy bs (P $ Q) = +fun iterm_from_term thy format bs (P $ Q) = let - val (P', P_atomics_Ts) = iterm_from_term thy bs P - val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q + val (P', P_atomics_Ts) = iterm_from_term thy format bs P + val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end - | iterm_from_term thy _ (Const (c, T)) = - (IConst (`make_fixed_const c, T, + | iterm_from_term thy format _ (Const (c, T)) = + (IConst (`(make_fixed_const (SOME format)) c, T, if String.isPrefix old_skolem_const_prefix c then [] |> Term.add_tvarsT T |> map TVar else (c, T) |> Sign.const_typargs thy), atyps_of T) - | iterm_from_term _ _ (Free (s, T)) = + | iterm_from_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, if String.isPrefix polymorphic_free_prefix s then [T] else []), atyps_of T) - | iterm_from_term _ _ (Var (v as (s, _), T)) = + | iterm_from_term _ format _ (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 IConst (`make_fixed_const s', T, Ts) end + in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end else IVar ((make_schematic_var v, s), T), atyps_of T) - | iterm_from_term _ bs (Bound j) = + | iterm_from_term _ _ bs (Bound j) = nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T)) - | iterm_from_term thy bs (Abs (s, T, t)) = + | iterm_from_term thy format 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 ((s, (name, T)) :: bs) t + val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end datatype locality = @@ -882,15 +884,20 @@ | _ => IConst (name, T, []) else IConst (proxy_base |>> prefix const_prefix, T, T_args) - | NONE => IConst (name, T, T_args)) + | NONE => if s = tptp_choice then + (*this could be made neater by adding c_Eps as a proxy, + but we'd need to be able to "see" Hilbert_Choice.Eps + at this level in order to define fEps*) + tweak_ho_quant tptp_choice T args + else IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) | intro _ _ tm = tm in intro true [] end -fun iformula_from_prop thy type_enc eq_as_iff = +fun iformula_from_prop thy format type_enc eq_as_iff = let fun do_term bs t atomic_types = - iterm_from_term thy bs (Envir.eta_contract t) + iterm_from_term thy format bs (Envir.eta_contract t) |>> (introduce_proxies type_enc #> AAtom) ||> union (op =) atomic_types fun do_quant bs q pos s T t' = @@ -1041,10 +1048,10 @@ end (* making fact and conjecture formulas *) -fun make_formula thy type_enc eq_as_iff name loc kind t = +fun make_formula thy format type_enc eq_as_iff name loc kind t = let val (iformula, atomic_types) = - iformula_from_prop thy type_enc eq_as_iff (SOME (kind <> Conjecture)) t [] + iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t [] in {name = name, locality = loc, kind = kind, iformula = iformula, atomic_types = atomic_types} @@ -1052,8 +1059,8 @@ fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) = let val thy = Proof_Context.theory_of ctxt in - case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name - loc Axiom of + case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF) + name loc Axiom of formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} => if s = tptp_true then NONE else SOME formula | formula => SOME formula @@ -1065,7 +1072,7 @@ fun make_conjecture thy format type_enc = map (fn ((name, loc), (kind, t)) => t |> kind = Conjecture ? s_not_trueprop - |> make_formula thy type_enc (format <> CNF) name loc kind) + |> make_formula thy format type_enc (format <> CNF) name loc kind) (** Finite and infinite type inference **) @@ -1243,14 +1250,14 @@ val default_sym_tab_entries : (string * sym_info) list = (prefixed_predicator_name, {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: - (make_fixed_const @{const_name undefined}, + (make_fixed_const NONE @{const_name undefined}, {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: ([tptp_false, tptp_true] |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ ([tptp_equal, tptp_old_equal] |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) -fun sym_table_for_facts ctxt explicit_apply facts = +fun sym_table_for_facts ctxt format explicit_apply facts = ((false, []), Symtab.empty) |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd |> fold Symtab.update default_sym_tab_entries @@ -1280,7 +1287,7 @@ | NONE => false val predicator_combconst = - IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, []) + IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, []) fun predicator tm = IApp (predicator_combconst, tm) fun introduce_predicators_in_iterm sym_tab tm = @@ -1291,7 +1298,7 @@ fun list_app head args = fold (curry (IApp o swap)) args head -val app_op = `make_fixed_const app_op_name +val app_op = `(make_fixed_const NONE) app_op_name fun explicit_app arg head = let @@ -1346,7 +1353,8 @@ | aux arity (IConst (name as (s, _), T, T_args)) = (case strip_prefix_and_unascii const_prefix s of NONE => - (name, if level_of_type_enc type_enc = No_Types then [] else T_args) + (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice + then [] else T_args) | SOME s'' => let val s'' = invert_const s'' @@ -1433,7 +1441,7 @@ |> bound_tvars type_enc atomic_Ts |> close_formula_universally -val type_tag = `make_fixed_const type_tag_name +val type_tag = `(make_fixed_const NONE) type_tag_name fun type_tag_idempotence_fact type_enc = let @@ -1580,7 +1588,7 @@ (conjs, facts @ lambdas, class_rel_clauses, arity_clauses)) end -val type_guard = `make_fixed_const type_guard_name +val type_guard = `(make_fixed_const NONE) type_guard_name fun type_guard_iterm ctxt format type_enc T tm = IApp (IConst (type_guard, T --> @{typ bool}, [T]) @@ -1790,7 +1798,7 @@ fun add_undefined_const T = let val (s, s') = - `make_fixed_const @{const_name undefined} + `(make_fixed_const (SOME format)) @{const_name undefined} |> (case type_arg_policy type_enc @{const_name undefined} of Mangled_Type_Args _ => mangled_const_name format type_enc [T] | _ => I) @@ -2108,12 +2116,12 @@ val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) = translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc hyp_ts concl_t facts - val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply + val sym_tab = conjs @ facts |> sym_table_for_facts ctxt format explicit_apply val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc val repair = repair_fact ctxt format type_enc sym_tab val (conjs, facts) = (conjs, facts) |> pairself (map repair) val repaired_sym_tab = - conjs @ facts |> sym_table_for_facts ctxt (SOME false) + conjs @ facts |> sym_table_for_facts ctxt format (SOME false) val helpers = repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc |> map repair