From e3c6909ad593e5a966a449df5e92abb1f0dbc317 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 2 Mar 2025 17:10:27 -0800 Subject: [PATCH] chore: reimplement `mk_projections` in Lean (#7295) This PR translates `lean::mk_projections` into Lean, adding `Lean.Meta.mkProjections`. It also puts `hasLooseBVarInExplicitDomain` back in sync with the kernel version. Deletes `src/library/constructions/projection.{h,cpp}`. --- src/Lean/Elab/Structure.lean | 19 +-- src/Lean/Expr.lean | 34 +++-- src/Lean/Meta/Structure.lean | 96 +++++++++++- src/library/constructions/CMakeLists.txt | 2 +- src/library/constructions/init_module.cpp | 3 - src/library/constructions/projection.cpp | 144 ------------------ src/library/constructions/projection.h | 23 --- src/library/elab_environment.cpp | 2 +- .../autoImplicitForbidden.lean.expected.out | 1 + tests/lean/run/345.lean | 2 + tests/lean/run/structure_recursive.lean | 5 +- 11 files changed, 132 insertions(+), 199 deletions(-) delete mode 100644 src/library/constructions/projection.cpp delete mode 100644 src/library/constructions/projection.h diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index dae9be7b13..e865d90d53 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -825,23 +825,18 @@ private partial def checkResultingUniversesForFields (fieldInfos : Array StructF which is not less than or equal to the structure's resulting universe level{indentD u}" throwErrorAt info.ref msg -@[extern "lean_mk_projections"] -private opaque mkProjections (env : Environment) (structName : Name) (projs : List Name) (isClass : Bool) : Except Kernel.Exception Environment - private def addProjections (r : ElabHeaderResult) (fieldInfos : Array StructFieldInfo) : TermElabM Unit := do - if r.type.isProp then - if let some fieldInfo ← fieldInfos.findM? (not <$> Meta.isProof ·.fvar) then - throwErrorAt fieldInfo.ref m!"failed to generate projections for 'Prop' structure, field '{format fieldInfo.name}' is not a proof" - let projNames := fieldInfos |>.filter (!·.isFromSubobject) |>.map (·.declName) - let env ← getEnv - let env ← ofExceptKernelException (mkProjections env r.view.declName projNames.toList r.view.isClass) - setEnv env + let projDecls : Array StructProjDecl := + fieldInfos + |>.filter (!·.isFromSubobject) + |>.map (fun info => { ref := info.ref, projName := info.declName }) + mkProjections r.view.declName projDecls r.view.isClass for fieldInfo in fieldInfos do if fieldInfo.isSubobject then addDeclarationRangesFromSyntax fieldInfo.declName r.view.ref fieldInfo.ref - for n in projNames do + for decl in projDecls do -- projections may generate equation theorems - enableRealizationsForConst n + enableRealizationsForConst decl.projName private def registerStructure (structName : Name) (infos : Array StructFieldInfo) : TermElabM Unit := do let fields ← infos.filterMapM fun info => do diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index a2bd98dd66..cdfcd523bc 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -1272,11 +1272,23 @@ This operation traverses the expression tree. @[extern "lean_expr_has_loose_bvar"] opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool -/-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/ -def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool - | Expr.forallE _ d b bi, bvarIdx, tryRange => - (bi.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange - | e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx +/-- +Returns true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, +or in the range if `considerRange == true`. +Additionally, if the bound variable appears in an implicit parameter, +it transitively looks for that implicit parameter. +-/ +-- This should be kept in sync with `lean::has_loose_bvars_in_domain` +def hasLooseBVarInExplicitDomain (e : Expr) (bvarIdx : Nat) (considerRange : Bool) : Bool := + match e with + | Expr.forallE _ d b bi => + (hasLooseBVar d bvarIdx + && (bi.isExplicit + -- "Transitivity": bvar occurs in current implicit argument, + -- so we search for the current argument in the body. + || hasLooseBVarInExplicitDomain b 0 considerRange)) + || hasLooseBVarInExplicitDomain b (bvarIdx+1) considerRange + | e => considerRange && hasLooseBVar e bvarIdx /-- Lower the loose bound variables `>= s` in `e` by `d`. @@ -1297,16 +1309,16 @@ opaque liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr It marks any parameter with an explicit binder annotation if there is another explicit arguments that depends on it or the resulting type if `considerRange == true`. -Remark: we use this function to infer the bind annotations of inductive datatype constructors, and structure projections. -When the `{}` annotation is used in these commands, we set `considerRange == false`. +Remark: we use this function to infer the binder annotations of structure projections. -/ -def inferImplicit : Expr → Nat → Bool → Expr - | Expr.forallE n d b bi, i+1, considerRange => +-- This should be kept in synch with `lean::infer_implicit` +def inferImplicit (e : Expr) (numParams : Nat) (considerRange : Bool) : Expr := + match e, numParams with + | Expr.forallE n d b bi, i + 1 => let b := inferImplicit b i considerRange let newInfo := if bi.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else bi mkForall n newInfo d b - | e, 0, _ => e - | e, _, _ => e + | e, _ => e /-- Instantiates the loose bound variables in `e` using the `subst` array, diff --git a/src/Lean/Meta/Structure.lean b/src/Lean/Meta/Structure.lean index 63f5b494a9..fe1267e04f 100644 --- a/src/Lean/Meta/Structure.lean +++ b/src/Lean/Meta/Structure.lean @@ -1,16 +1,23 @@ /- Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura - -Additional helper methods that require `MetaM` infrastructure. +Authors: Leonardo de Moura, Kyle Miller -/ prelude +import Lean.AddDecl import Lean.Structure import Lean.Meta.AppBuilder +/-! +# Structure methods that require `MetaM` infrastructure +-/ + namespace Lean.Meta +/-- +If `struct` is an application of the form `S ..` with `S` a constant for a structure, +returns the name of the structure, otherwise throws an error. +-/ def getStructureName (struct : Expr) : MetaM Name := match struct.getAppFn with | Expr.const declName .. => do @@ -19,4 +26,87 @@ def getStructureName (struct : Expr) : MetaM Name := return declName | _ => throwError "expected structure" +/-- +Structure projection declaration for `mkProjections`. +-/ +structure StructProjDecl where + ref : Syntax + projName : Name + +/-- +Adds projection functions to the environment for the one-constructor inductive type named `n`. +- The `projName`s in each `StructProjDecl` are used for the names of the declarations added to the environment. +- If `instImplicit` is true, then generates projections with `self` being instance implicit. + +Notes: +- This function supports everything that `Expr.proj` supports (see `lean::type_checker::infer_proj`). + This means we can generate projections for inductive types with one-constructor, + even if it is an indexed family (which is not supported by the `structure` command). +- We throw errors in the cases that `Expr.proj` is not type-correct. +-/ +def mkProjections (n : Name) (projDecls : Array StructProjDecl) (instImplicit : Bool) : MetaM Unit := + withLCtx {} {} do + let indVal ← getConstInfoInduct n + if indVal.numCtors != 1 then + throwError "cannot generate projections for '{.ofConstName n}', does not have exactly one constructor" + let ctorVal ← getConstInfoCtor indVal.ctors.head! + let isPredicate ← isPropFormerType indVal.type + let lvls := indVal.levelParams.map mkLevelParam + forallBoundedTelescope ctorVal.type indVal.numParams fun params ctorType => do + if params.size != indVal.numParams then + throwError "projection generation failed, '{.ofConstName n}' is an ill-formed inductive datatype" + let selfType := mkAppN (.const n lvls) params + let selfBI : BinderInfo := if instImplicit then .instImplicit else .default + withLocalDecl `self selfBI selfType fun self => do + let projArgs := params.push self + -- Make modifications to parameter binder infos that apply to all projections + let mut lctx ← getLCtx + for param in params do + let fvarId := param.fvarId! + let decl ← fvarId.getDecl + if !decl.binderInfo.isInstImplicit && !decl.type.isOutParam then + /- We reset the implicit binder to have it be inferred by `Expr.inferImplicit`. + However, outparams must be implicit. -/ + lctx := lctx.setBinderInfo fvarId .default + else if decl.binderInfo.isInstImplicit && instImplicit then + lctx := lctx.setBinderInfo fvarId .implicit + -- Construct the projection functions: + let mut ctorType := ctorType + for h : i in [0:projDecls.size] do + let {ref, projName} := projDecls[i] + unless ctorType.isForall do + throwErrorAt ref "\ + failed to generate projection '{projName}' for '{.ofConstName n}', \ + not enough constructor fields" + let resultType := ctorType.bindingDomain!.consumeTypeAnnotations + let isProp ← isProp resultType + if isPredicate && !isProp then + throwErrorAt ref "\ + failed to generate projection '{projName}' for the 'Prop'-valued type '{.ofConstName n}', \ + field must be a proof, but it has type\ + {indentExpr resultType}" + let projType := lctx.mkForall projArgs resultType + let projType := projType.inferImplicit indVal.numParams (considerRange := true) + let projVal := lctx.mkLambda projArgs <| Expr.proj n i self + let cval : ConstantVal := { name := projName, levelParams := indVal.levelParams, type := projType } + withRef ref do + if isProp then + let env ← getEnv + addDecl <| + if env.hasUnsafe projType || env.hasUnsafe projVal then + -- Theorems cannot be unsafe, using opaque instead. + Declaration.opaqueDecl { cval with value := projVal, isUnsafe := true } + else + Declaration.thmDecl { cval with value := projVal } + else + let decl ← mkDefinitionValInferrringUnsafe projName indVal.levelParams projType projVal ReducibilityHints.abbrev + -- Projections have special compiler support. No need to compile. + addDecl <| Declaration.defnDecl decl + -- Recall: we want instance projections to be in "reducible canonical form" + if !instImplicit then + setReducibleAttribute projName + modifyEnv fun env => addProjectionFnInfo env projName ctorVal.name indVal.numParams i instImplicit + let proj := mkApp (mkAppN (.const projName lvls) params) self + ctorType := ctorType.bindingBody!.instantiate1 proj + end Lean.Meta diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt index 0737620c57..6e4b4968f8 100644 --- a/src/library/constructions/CMakeLists.txt +++ b/src/library/constructions/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(constructions OBJECT cases_on.cpp - no_confusion.cpp projection.cpp init_module.cpp + no_confusion.cpp init_module.cpp util.cpp) diff --git a/src/library/constructions/init_module.cpp b/src/library/constructions/init_module.cpp index 32fc32aa35..04028f9877 100644 --- a/src/library/constructions/init_module.cpp +++ b/src/library/constructions/init_module.cpp @@ -5,17 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "library/constructions/init_module.h" -#include "library/constructions/projection.h" #include "library/constructions/util.h" namespace lean{ void initialize_constructions_module() { initialize_constructions_util(); - initialize_def_projection(); } void finalize_constructions_module() { - finalize_def_projection(); finalize_constructions_util(); } } diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp deleted file mode 100644 index 0e40d4b6ce..0000000000 --- a/src/library/constructions/projection.cpp +++ /dev/null @@ -1,144 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "runtime/sstream.h" -#include "kernel/kernel_exception.h" -#include "kernel/abstract.h" -#include "kernel/type_checker.h" -#include "kernel/inductive.h" -#include "kernel/instantiate.h" -#include "library/reducible.h" -#include "library/projection.h" -#include "library/util.h" -#include "library/class.h" -#include "library/constructions/projection.h" -#include "library/constructions/util.h" - -namespace lean { -[[ noreturn ]] static void throw_ill_formed(name const & n) { - throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype"); -} - -static bool is_prop(expr type) { - while (is_pi(type)) { - type = binding_body(type); - } - return is_sort(type) && is_zero(sort_level(type)); -} - -elab_environment mk_projections(elab_environment const & env, name const & n, buffer const & proj_names, bool inst_implicit) { - local_ctx lctx; - name_generator ngen = mk_constructions_name_generator(); - constant_info ind_info = env.get(n); - if (!ind_info.is_inductive()) - throw exception(sstream() << "projection generation, '" << n << "' is not an inductive datatype"); - inductive_val ind_val = ind_info.to_inductive_val(); - unsigned nparams = ind_val.get_nparams(); - name rec_name = mk_rec_name(n); - if (ind_val.get_nindices() > 0) - throw exception(sstream() << "projection generation, '" << n << "' is an indexed inductive datatype family"); - if (length(ind_val.get_cnstrs()) != 1) - throw exception(sstream() << "projection generation, '" << n << "' does not have a single constructor"); - constant_info cnstr_info = env.get(head(ind_val.get_cnstrs())); - expr cnstr_type = cnstr_info.get_type(); - bool is_predicate = is_prop(ind_info.get_type()); - names lvl_params = ind_info.get_lparams(); - levels lvls = lparams_to_levels(lvl_params); - buffer params; // datatype parameters - expr cnstr_type_orig = cnstr_type; - for (unsigned i = 0; i < nparams; i++) { - if (!is_pi(cnstr_type)) - throw_ill_formed(n); - lean_assert(is_pi(cnstr_type_orig)); - auto bi = binding_info(cnstr_type); - auto bi_orig = binding_info(cnstr_type_orig); - auto type = binding_domain(cnstr_type); - auto type_orig = binding_domain(cnstr_type_orig); - if (!is_inst_implicit(bi_orig) && !is_class_out_param(type_orig)) { - // We reset implicit binders in favor of having them inferred by `infer_implicit_params` later IF - // 1. The original binder before `mk_outparam_args_implicit` is not an instance implicit. - // 2. It is not originally an outparam. Outparams must be implicit. - bi = mk_binder_info(); - } else if (is_inst_implicit(bi_orig) && inst_implicit) { - bi = mk_implicit_binder_info(); - } - expr param = lctx.mk_local_decl(ngen, binding_name(cnstr_type), type, bi); - cnstr_type = instantiate(binding_body(cnstr_type), param); - cnstr_type_orig = binding_body(cnstr_type_orig); - params.push_back(param); - } - expr C_A = mk_app(mk_constant(n, lvls), params); - binder_info c_bi = inst_implicit ? mk_inst_implicit_binder_info() : mk_binder_info(); - expr c = lctx.mk_local_decl(ngen, name("self"), C_A, c_bi); - buffer cnstr_type_args; // arguments that are not parameters - expr it = cnstr_type; - while (is_pi(it)) { - expr local = lctx.mk_local_decl(ngen, binding_name(it), binding_domain(it), binding_info(it)); - cnstr_type_args.push_back(local); - it = instantiate(binding_body(it), local); - } - unsigned i = 0; - elab_environment new_env = env; - for (name const & proj_name : proj_names) { - if (!is_pi(cnstr_type)) - throw exception(sstream() << "generating projection '" << proj_name << "', '" - << n << "' does not have sufficient data"); - expr result_type = consume_type_annotations(binding_domain(cnstr_type)); - bool is_prop = type_checker(new_env, lctx).is_prop(result_type); - if (is_predicate && !is_prop) { - throw exception(sstream() << "failed to generate projection '" << proj_name << "' for '" << n << "', " - << "type is an inductive predicate, but field is not a proposition"); - } - buffer proj_args; - proj_args.append(params); - proj_args.push_back(c); - expr proj_type = lctx.mk_pi(proj_args, result_type); - proj_type = infer_implicit_params(proj_type, nparams, implicit_infer_kind::RelaxedImplicit); - expr proj_val = mk_proj(n, i, c); - proj_val = lctx.mk_lambda(proj_args, proj_val); - declaration new_d; - if (is_prop) { - bool unsafe = use_unsafe(env, proj_type) || use_unsafe(env, proj_val); - if (unsafe) { - // theorems cannot be unsafe - new_d = mk_opaque(proj_name, lvl_params, proj_type, proj_val, unsafe); - } else { - new_d = mk_theorem(proj_name, lvl_params, proj_type, proj_val); - } - } else { - new_d = mk_definition_inferring_unsafe(env, proj_name, lvl_params, proj_type, proj_val, - reducibility_hints::mk_abbreviation()); - } - new_env = new_env.add(new_d); - if (!inst_implicit && !is_prop) - new_env = set_reducible(new_env, proj_name, reducible_status::Reducible, true); - new_env = save_projection_info(new_env, proj_name, cnstr_info.get_name(), nparams, i, inst_implicit); - expr proj = mk_app(mk_app(mk_constant(proj_name, lvls), params), c); - cnstr_type = instantiate(binding_body(cnstr_type), proj); - i++; - } - return new_env; -} - - -extern "C" LEAN_EXPORT object * lean_mk_projections(object * env, object * struct_name, object * proj_infos, uint8 inst_implicit) { - elab_environment new_env(env); - name n(struct_name); - list_ref ps(proj_infos); - buffer proj_names; - for (auto p : ps) { - proj_names.push_back(p); - } - return catch_kernel_exceptions([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); }); -} - -void initialize_def_projection() { -} - -void finalize_def_projection() { -} -} diff --git a/src/library/constructions/projection.h b/src/library/constructions/projection.h deleted file mode 100644 index 95abd81b3d..0000000000 --- a/src/library/constructions/projection.h +++ /dev/null @@ -1,23 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/environment.h" -#include "library/util.h" - -namespace lean { -/** \brief Create projections operators for the structure named \c n. - The procedure assumes \c n is a structure. - - If \c inst_implicit == true, then the structure argument of the projection is decorated as - "instance implicit" - [s : n] -*/ -environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit = false); - -void initialize_def_projection(); -void finalize_def_projection(); -} diff --git a/src/library/elab_environment.cpp b/src/library/elab_environment.cpp index 0d075bd3f2..8beff6106d 100644 --- a/src/library/elab_environment.cpp +++ b/src/library/elab_environment.cpp @@ -16,7 +16,7 @@ namespace lean { Updates an elab environment with a given kernel environment. NOTE: Ideally this language switching would not be necessary and we could do all this in Lean - only but the old code generator and `mk_projections` still need a C++ `elab_environment::add` + only but the old code generator still needs a C++ `elab_environment::add` that throws C++ exceptions. */ extern "C" obj_res lean_elab_environment_update_base_after_kernel_add(obj_arg env, obj_arg kenv, obj_arg decl); diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out index dc28113019..0d92b70454 100644 --- a/tests/lean/autoImplicitForbidden.lean.expected.out +++ b/tests/lean/autoImplicitForbidden.lean.expected.out @@ -1,6 +1,7 @@ autoImplicitForbidden.lean:1:8-1:9: error: unknown identifier 'f' autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h' autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla' +autoImplicitForbidden.lean:14:2-14:5: warning: declaration uses 'sorry' autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo' autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2' autoImplicitForbidden.lean:28:14-28:20: error: unknown identifier 'foobar' diff --git a/tests/lean/run/345.lean b/tests/lean/run/345.lean index c109666af0..6091cca2b6 100644 --- a/tests/lean/run/345.lean +++ b/tests/lean/run/345.lean @@ -20,6 +20,8 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex due to the absence of the instance above Additional diagnostic information may be available using the `set_option diagnostics true` command. +--- +warning: declaration uses 'sorry' -/ #guard_msgs in structure Foo where diff --git a/tests/lean/run/structure_recursive.lean b/tests/lean/run/structure_recursive.lean index a0dabe3e3a..a95e5e22cf 100644 --- a/tests/lean/run/structure_recursive.lean +++ b/tests/lean/run/structure_recursive.lean @@ -123,7 +123,10 @@ structure RecS where /-! Incidental new feature: checking projections when the structure is Prop. -/ -/-- error: failed to generate projections for 'Prop' structure, field 'x' is not a proof -/ +/-- +error: failed to generate projection 'Exists'.x' for the 'Prop'-valued type 'Exists'', field must be a proof, but it has type + α +-/ #guard_msgs in structure Exists' {α : Sort _} (p : α → Prop) : Prop where x : α