From 1bf12905707a8506eefa7deb493a7bf031e07ef4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Nov 2019 03:33:03 -0800 Subject: [PATCH] feat: use kernel projections in constructions Motivation: auxiliary recursors such as `brecOn` do not depend on user-facing projection definitions anymore. Thus, we can simplify `whnfCore` at `TypeUtil`. --- library/Init/Lean/TypeUtil.lean | 42 +----------------------------- src/library/constructions/util.cpp | 24 ++++++----------- src/library/type_context.cpp | 20 +++++++++++--- 3 files changed, 26 insertions(+), 60 deletions(-) diff --git a/library/Init/Lean/TypeUtil.lean b/library/Init/Lean/TypeUtil.lean index 9866cb473d..9cbd5f330a 100644 --- a/library/Init/Lean/TypeUtil.lean +++ b/library/Init/Lean/TypeUtil.lean @@ -159,46 +159,6 @@ else let val := val.betaRev revArgs; successK (extractIdRhs val) -private def reduceAuxRec - (whnf : Expr → TypeUtilM σ ϕ Expr) - (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) - (failK : Unit → TypeUtilM σ ϕ Expr) (successK : Expr → TypeUtilM σ ϕ Expr) : TypeUtilM σ ϕ Expr := -deltaBetaDefinition c lvls revArgs failK $ fun e => - /- Remark: - - `brecOn ...` unfolds to a term of the form (PProd.fst (rec ...)) - `whnfCore` does not unfold projection functions because of lazy delta reduction at `isDefEq`. - For example, when solving constraints such as `(PProd.fst ?m) =?= (PProd.fst (1, 2))` - - That being said, we observed a negative performance impact on - constraints containing `brecOn` that come from the equation compiler. - For example, consider the following definition - - ``` - def nastySize : List Nat → Nat - | [] := 1000000 - | (a::as) := nastySize as + 1000000 - ``` - - We will get a constraint of the form - ``` - (List.brecOn [] ...) =?= bit0 ... - ``` - The isDefEq method reduces this constraint using whnfCore. So, we obtain - ``` - PProd.fst ... =?= bit0 ... - ``` - This constraint is then handled by isDefEqDelta, which decides to unfold `bit0` which is a poor decision. - The key problem here is that we morally did not reduce `brecOn`. - Thus, we fix the issue by reducing the projection function if the auxiliary recursor is a brecOn. - This fix is a little non modular because `brecOn` auxiliary recursors are defined in - a completely different module, and `TypeUtil` should not be aware of them. -/ - match c.name with - | Name.mkString _ "brecOn" => do - env ← getEnv; - reduceProjectionFn whnf env e (fun _ => successK e) successK - | _ => successK e - /-- Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction, expand let-expressions, expand assigned meta-variables. @@ -234,7 +194,7 @@ deltaBetaDefinition c lvls revArgs failK $ fun e => | ConstantInfo.quotInfo rec => reduceQuotRecAux whnf env rec lvls e.getAppArgs done whnfCore | c@(ConstantInfo.defnInfo _) => if reduceAuxRec? && isAuxRecursor env c.name then - reduceAuxRec whnf c lvls e.getAppRevArgs done whnfCore + deltaBetaDefinition c lvls e.getAppArgs done whnfCore else done() | _ => done () diff --git a/src/library/constructions/util.cpp b/src/library/constructions/util.cpp index 2029aba486..155259765b 100644 --- a/src/library/constructions/util.cpp +++ b/src/library/constructions/util.cpp @@ -23,14 +23,12 @@ expr mk_and_intro(type_checker & ctx, expr const & Ha, expr const & Hb) { return mk_app(mk_constant(get_and_intro_name()), ctx.infer(Ha), ctx.infer(Hb), Ha, Hb); } -expr mk_and_left(type_checker & ctx, expr const & H) { - expr a_and_b = ctx.whnf(ctx.infer(H)); - return mk_app(mk_constant(get_and_left_name()), app_arg(app_fn(a_and_b)), app_arg(a_and_b), H); +expr mk_and_left(type_checker &, expr const & H) { + return mk_proj(get_and_name(), nat(0), H); } -expr mk_and_right(type_checker & ctx, expr const & H) { - expr a_and_b = ctx.whnf(ctx.infer(H)); - return mk_app(mk_constant(get_and_right_name()), app_arg(app_fn(a_and_b)), app_arg(a_and_b), H); +expr mk_and_right(type_checker &, expr const & H) { + return mk_proj(get_and_name(), nat(1), H); } expr mk_pprod(type_checker & ctx, expr const & A, expr const & B) { @@ -47,18 +45,12 @@ expr mk_pprod_mk(type_checker & ctx, expr const & a, expr const & b) { return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b); } -expr mk_pprod_fst(type_checker & ctx, expr const & p) { - expr AxB = ctx.whnf(ctx.infer(p)); - expr const & A = app_arg(app_fn(AxB)); - expr const & B = app_arg(AxB); - return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p); +expr mk_pprod_fst(type_checker &, expr const & p) { + return mk_proj(get_pprod_name(), nat(0), p); } -expr mk_pprod_snd(type_checker & ctx, expr const & p) { - expr AxB = ctx.whnf(ctx.infer(p)); - expr const & A = app_arg(app_fn(AxB)); - expr const & B = app_arg(AxB); - return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p); +expr mk_pprod_snd(type_checker &, expr const & p) { + return mk_proj(get_pprod_name(), nat(1), p); } expr mk_pprod(type_checker & ctx, expr const & a, expr const & b, bool prop) { diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index aa1cbba3c1..ce301d8cf2 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -635,9 +635,23 @@ optional type_context_old::reduce_projection(expr const & e) { return reduce_projection_core(info, e); } -optional type_context_old::reduce_proj(expr const & /* e */) { - // TODO(Leo) - throw exception("projection reduction is only implemented in the kernel."); +optional type_context_old::reduce_proj(expr const & e) { + if (!proj_idx(e).is_small()) + return none_expr(); + unsigned idx = proj_idx(e).get_small_value(); + expr c = whnf(proj_expr(e)); + buffer args; + expr const & mk = get_app_args(c, args); + if (!is_constant(mk)) + return none_expr(); + constant_info mk_info = env().get(const_name(mk)); + if (!mk_info.is_constructor()) + return none_expr(); + unsigned nparams = mk_info.to_constructor_val().get_nparams(); + if (nparams + idx < args.size()) + return some_expr(args[nparams + idx]); + else + return none_expr(); } optional type_context_old::reduce_aux_recursor(expr const & e) {