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

@@ -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

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,

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

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)

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();
 }
 }

src/library/constructions/projection.cpp

@@ -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 <string>
-#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<name> 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<expr> 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<expr> 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<expr> 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<name> ps(proj_infos);
-    buffer<name> proj_names;
-    for (auto p : ps) {
-        proj_names.push_back(p);
-    }
-    return catch_kernel_exceptions<elab_environment>([&]() { return mk_projections(new_env, n, proj_names, inst_implicit != 0); });
-}
-
-void initialize_def_projection() {
-}
-
-void finalize_def_projection() {
-}
-}

src/library/constructions/projection.h

@@ -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 <name> const & proj_names, bool inst_implicit = false);
-
-void initialize_def_projection();
-void finalize_def_projection();
-}

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);
 

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'

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

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 : α