# HG changeset patch # User blanchet # Date 1630070517 -7200 # Node ID 1a8d8dd77513589d8bb3676c4eba12a83101f7b1 # Parent adf767b94f775623ded5de5a6a5147345b83df97 made sure lambda-lifting works well with native let binders in Sledgehammer diff -r adf767b94f77 -r 1a8d8dd77513 src/HOL/Tools/ATP/atp_problem_generate.ML --- a/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Aug 27 14:29:02 2021 +0200 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Fri Aug 27 15:21:57 2021 +0200 @@ -567,34 +567,48 @@ (* Converts an Isabelle/HOL term (with combinators) into an intermediate term. Also accumulates sort infomation. *) -fun iterm_of_term thy type_enc bs (P $ Q) = - let - 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_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_of_term _ _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of 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 :: - val s' = new_skolem_const_name s (length Ts) - 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_of_term _ _ bs (Bound j) = - nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of 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_of_term thy type_enc ((s, (name, T)) :: bs) t - in - (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) - end +fun iterm_of_term thy type_enc = + let + fun iot true bs ((t0 as Const (\<^const_name>\Let\, _)) $ t1 $ (t2 as Abs (s, T, t'))) = + let + val (t0', t0_atomics_Ts) = iot true bs t0 + val (t1', t1_atomics_Ts) = iot true bs t1 + val (t2', t2_atomics_Ts) = iot true bs t2 + in + (IApp (IApp (t0', t1'), t2'), + fold (union (op =)) [t0_atomics_Ts, t1_atomics_Ts, t2_atomics_Ts] []) + end + | iot true bs ((t0 as Const (\<^const_name>\Let\, _)) $ t1 $ t2) = + iot true bs (t0 $ t1 $ eta_expand (map (snd o snd) bs) t2 1) + | iot fool bs (P $ Q) = + let + val (P', P_atomics_Ts) = iot fool bs P + val (Q', Q_atomics_Ts) = iot fool bs Q + in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end + | iot _ _ (Const (c, T)) = + (IConst (`(make_fixed_const (SOME type_enc)) c, T, robust_const_type_args thy (c, T)), + atomic_types_of T) + | iot _ _ (Free (s, T)) = (IConst (`make_fixed_var s, T, []), atomic_types_of T) + | iot _ _ (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 (SOME type_enc)) s', T, Ts) end + else + IVar ((make_schematic_var v, s), T), atomic_types_of T) + | iot _ bs (Bound j) = + nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atomic_types_of T)) + | iot fool 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) = iot fool ((s, (name, T)) :: bs) t + in + (IAbs ((name, T), tm), union (op =) atomic_Ts (atomic_types_of T)) + end + in iot (is_type_enc_fool type_enc) end (* "_query" and "_at" are for the ASCII-challenged Metis and Mirabelle. *) val queries = ["?", "_query"] @@ -745,8 +759,8 @@ is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2 | _ => not (exists_subterm (fn Abs _ => true | _ => false) t)) -fun simple_translate_lambdas do_lambdas ctxt type_enc t = - if is_first_order_lambda_free t then +fun simple_translate_lambdas eta_matters do_lambdas ctxt type_enc t = + if not eta_matters andalso is_first_order_lambda_free t then t else let @@ -791,9 +805,11 @@ | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts | _ => t) - val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order - val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt - in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end + val (t', ctxt') = yield_singleton (Variable.import_terms true) t ctxt + in + t' |> (if is_type_enc_fool type_enc then trans_fool else trans_first_order) [] + |> singleton (Variable.export_terms ctxt' ctxt) + end fun do_cheaply_conceal_lambdas Ts (t1 $ t2) = do_cheaply_conceal_lambdas Ts t1 @@ -819,7 +835,8 @@ |> reveal_bounds Ts) (* A type variable of sort "{}" will make abstraction fail. *) handle THM _ => t |> do_cheaply_conceal_lambdas Ts -val introduce_combinators = simple_translate_lambdas do_introduce_combinators + +val introduce_combinators = simple_translate_lambdas false do_introduce_combinators fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t) @@ -827,28 +844,32 @@ (if String.isPrefix lam_lifted_prefix s then Const else Free) x | constify_lifted t = t +fun is_binder true (Const (\<^const_name>\Let\, _) $ _) = true + | is_binder _ t = Lambda_Lifting.is_quantifier t + fun lift_lams_part_1 ctxt type_enc = map hol_close_form #> rpair ctxt - #-> Lambda_Lifting.lift_lambdas - (SOME ((if is_type_enc_polymorphic type_enc then - lam_lifted_poly_prefix - else - lam_lifted_mono_prefix) ^ "_a")) - Lambda_Lifting.is_quantifier + #-> Lambda_Lifting.lift_lambdas (SOME + ((if is_type_enc_polymorphic type_enc then lam_lifted_poly_prefix + else lam_lifted_mono_prefix) ^ "_a")) + (is_binder (is_type_enc_fool type_enc)) #> fst fun lift_lams_part_2 ctxt type_enc (facts, lifted) = (facts, lifted) - (* Lambda-lifting sometimes leaves some lambdas around; we need some way to - get rid of them *) + (* Lambda-lifting sometimes leaves some lambdas around; we need some way to get rid of them *) |> apply2 (map (introduce_combinators ctxt type_enc)) |> apply2 (map constify_lifted) - (* Requires bound variables not to clash with any schematic variables (as - should be the case right after lambda-lifting). *) + (* Requires bound variables not to clash with any schematic variables (as should be the case right + after lambda-lifting). *) |>> map (hol_open_form (unprefix hol_close_form_prefix)) ||> map (hol_open_form I) -fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc +fun lift_lams ctxt type_enc = + (is_type_enc_fool type_enc ? + map (simple_translate_lambdas true (fn _ => fn _ => fn t => t) ctxt type_enc)) + #> lift_lams_part_1 ctxt type_enc + #> lift_lams_part_2 ctxt type_enc fun intentionalize_def (Const (\<^const_name>\All\, _) $ Abs (_, _, t)) = intentionalize_def t @@ -1186,12 +1207,7 @@ val tm2' = intro false [] tm2 val tm2'' = (case tm1' of - IApp (IConst ((s, _), _, _), _) => - if s = tptp_let then - eta_expand_quantifier_body tm2' - else - tm2' - | IConst ((s, _), _, _) => + IConst ((s, _), _, _) => if s = tptp_ho_forall orelse s = tptp_ho_exists then eta_expand_quantifier_body tm2' else @@ -1379,9 +1395,10 @@ fun presimp_prop simp_options ctxt type_enc t = let - val t = t |> Envir.beta_eta_contract - |> transform_elim_prop - |> Object_Logic.atomize_term ctxt + val t = + t |> Envir.beta_eta_contract + |> transform_elim_prop + |> Object_Logic.atomize_term ctxt val need_trueprop = (fastype_of t = \<^typ>\bool\) val is_ho = is_type_enc_full_higher_order type_enc in