# HG changeset patch # User blanchet # Date 1336919461 -7200 # Node ID 2168126446bb543fa107b6633812f7cb2401ad72 # Parent ca5b629a59957265dfb9697f1745cb17cb348def extend ATP data structure to avoid having to perform ((non-)capture avoiding) beta reduction -- fixes a bug in the THF translation of "is_measure.simps" diff -r ca5b629a5995 -r 2168126446bb src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri May 11 01:02:36 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Sun May 13 16:31:01 2012 +0200 @@ -9,7 +9,7 @@ sig datatype ('a, 'b) ho_term = ATerm of 'a * ('a, 'b) ho_term list | - AAbs of ('a * 'b) * ('a, 'b) ho_term + AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIff datatype ('a, 'b, 'c) formula = @@ -141,7 +141,7 @@ datatype ('a, 'b) ho_term = ATerm of 'a * ('a, 'b) ho_term list | - AAbs of ('a * 'b) * ('a, 'b) ho_term + AAbs of (('a * 'b) * ('a, 'b) ho_term) * ('a, 'b) ho_term list datatype quantifier = AForall | AExists datatype connective = ANot | AAnd | AOr | AImplies | AIff datatype ('a, 'b, 'c) formula = @@ -394,22 +394,26 @@ |> is_format_higher_order format ? enclose "(" ")" else case (s = tptp_ho_forall orelse s = tptp_ho_exists, s = tptp_choice andalso is_format_with_choice format, ts) of - (true, _, [AAbs ((s', ty), tm)]) => + (true, _, [AAbs (((s', ty), tm), [])]) => (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work around LEO-II 1.2.8 parser limitation. *) tptp_string_for_formula format (AQuant (if s = tptp_ho_forall then AForall else AExists, [(s', SOME ty)], AAtom tm)) - | (_, true, [AAbs ((s', ty), tm)]) => + | (_, true, [AAbs (((s', ty), tm), args)]) => (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an abstraction. *) - tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ - tptp_string_for_term format tm ^ "" - |> enclose "(" ")" + tptp_string_for_app format + (tptp_choice ^ "[" ^ s' ^ " : " ^ string_for_type format ty ^ "]: " ^ + tptp_string_for_term format tm ^ "" + |> enclose "(" ")") + (map (tptp_string_for_term format) args) | _ => tptp_string_for_app format s (map (tptp_string_for_term format) ts)) - | tptp_string_for_term (format as THF _) (AAbs ((s, ty), tm)) = - "(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ - tptp_string_for_term format tm ^ ")" + | tptp_string_for_term (format as THF _) (AAbs (((s, ty), tm), args)) = + tptp_string_for_app format + ("(^[" ^ s ^ " : " ^ string_for_type format ty ^ "]: " ^ + tptp_string_for_term format tm ^ ")") + (map (tptp_string_for_term format) args) | tptp_string_for_term _ _ = raise Fail "unexpected term in first-order format" and tptp_string_for_formula format (AQuant (q, xs, phi)) = @@ -809,8 +813,9 @@ pool_map nice_name names ##>> nice_type ty #>> ATyAbs fun nice_term (ATerm (name, ts)) = nice_name name ##>> pool_map nice_term ts #>> ATerm - | nice_term (AAbs ((name, ty), tm)) = - nice_name name ##>> nice_type ty ##>> nice_term tm #>> AAbs + | nice_term (AAbs (((name, ty), tm), args)) = + nice_name name ##>> nice_type ty ##>> nice_term tm + ##>> pool_map nice_term args #>> AAbs fun nice_formula (AQuant (q, xs, phi)) = pool_map nice_name (map fst xs) ##>> pool_map (fn NONE => pair NONE diff -r ca5b629a5995 -r 2168126446bb src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri May 11 01:02:36 2012 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sun May 13 16:31:01 2012 +0200 @@ -919,8 +919,8 @@ else I) #> fold (add_term_vars bounds) tms - | add_term_vars bounds (AAbs ((name, _), tm)) = - add_term_vars (name :: bounds) tm + | add_term_vars bounds (AAbs (((name, _), tm), args)) = + add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args fun close_formula_universally phi = close_universally add_term_vars phi fun add_iterm_vars bounds (IApp (tm1, tm2)) = @@ -1073,19 +1073,22 @@ | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args | (false, s) => - if is_tptp_equal s andalso length args = 2 then - IConst (`I tptp_equal, T, []) + if is_tptp_equal s then + if length args = 2 then + IConst (`I tptp_equal, T, []) + else + (* Eta-expand partially applied THF equality, because the + LEO-II and Satallax parsers complain about not being able to + infer the type of "=". *) + let val i_T = domain_type T in + IAbs ((`I "Y", i_T), + IAbs ((`I "Z", i_T), + IApp (IApp (IConst (`I tptp_equal, T, []), + IConst (`I "Y", i_T, [])), + IConst (`I "Z", i_T, [])))) + end else - (* Eta-expand partially applied THF equality, because the - LEO-II and Satallax parsers complain about not being able to - infer the type of "=". *) - let val i_T = domain_type T in - IAbs ((`I "X", i_T), - IAbs ((`I "Y", i_T), - IApp (IApp (IConst (`I tptp_equal, T, []), - IConst (`I "X", i_T, [])), - IConst (`I "Y", i_T, [])))) - end + IConst (name, T, []) | _ => IConst (name, T, []) else IConst (proxy_base |>> prefix const_prefix, T, T_args) @@ -1908,16 +1911,6 @@ | _ => raise Fail "unexpected lambda-abstraction") and ho_term_from_iterm ctxt mono type_enc pos = let - fun beta_red bs (IApp (IAbs ((name, _), tm), tm')) = - beta_red ((name, beta_red bs tm') :: bs) tm - | beta_red bs (IApp tmp) = IApp (pairself (beta_red bs) tmp) - | beta_red bs (tm as IConst (name, _, _)) = - (case AList.lookup (op =) bs name of - SOME tm' => tm' - | NONE => tm) - | beta_red bs (IAbs ((name, T), tm)) = - IAbs ((name, T), beta_red (AList.delete (op =) name bs) tm) - | beta_red _ tm = tm fun term site u = let val (head, args) = strip_iterm_comb u @@ -1936,8 +1929,8 @@ map (term Elsewhere) args |> mk_aterm type_enc name [] | IAbs ((name, T), tm) => if is_type_enc_higher_order type_enc then - AAbs ((name, ho_type_from_typ type_enc true 0 T), - term Elsewhere tm) + AAbs (((name, ho_type_from_typ type_enc true 0 T), + term Elsewhere tm), map (term Elsewhere) args) else raise Fail "unexpected lambda-abstraction" | IApp _ => raise Fail "impossible \"IApp\"" @@ -1948,7 +1941,7 @@ else t end - in term (Top_Level pos) o beta_red [] end + in term (Top_Level pos) end and formula_from_iformula ctxt polym_constrs mono type_enc should_guard_var = let val thy = Proof_Context.theory_of ctxt @@ -2538,7 +2531,8 @@ fun do_term pred_sym (ATerm (name as (s, _), tms)) = do_sym name (fn _ => default_type type_enc pred_sym s (length tms)) #> fold (do_term false) tms - | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm + | do_term _ (AAbs (((_, ty), tm), args)) = + do_type ty #> do_term false tm #> fold (do_term false) args fun do_formula (AQuant (_, xs, phi)) = fold do_type (map_filter snd xs) #> do_formula phi | do_formula (AConn (_, phis)) = fold do_formula phis @@ -2593,10 +2587,8 @@ normally the case for "metis" and the minimizer). *) val app_op_level = if length facts > app_op_and_predicator_threshold then - if polymorphism_of_type_enc type_enc = Polymorphic then - Min_App_Op - else - Sufficient_App_Op + if polymorphism_of_type_enc type_enc = Polymorphic then Min_App_Op + else Sufficient_App_Op else Sufficient_App_Op_And_Predicator val lam_trans = @@ -2691,7 +2683,8 @@ fun add_term_weights weight (ATerm (s, tms)) = is_tptp_user_symbol s ? Symtab.default (s, weight) #> fold (add_term_weights weight) tms - | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm + | add_term_weights weight (AAbs ((_, tm), args)) = + add_term_weights weight tm #> fold (add_term_weights weight) args fun add_line_weights weight (Formula (_, _, phi, _, _)) = formula_fold NONE (K (add_term_weights weight)) phi | add_line_weights _ _ = I @@ -2764,7 +2757,8 @@ #> fold (add_term_deps head) args else I - | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm + | add_term_deps head (AAbs ((_, tm), args)) = + add_term_deps head tm #> fold (add_term_deps head) args fun add_intro_deps pred (Formula (_, role, phi, _, info)) = if pred (role, info) then let val (hyps, concl) = strip_ahorn_etc phi in