chore: delete obsolete C++ file (#11561)

src/Lean/ProjFns.lean

@@ -36,13 +36,11 @@ def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=
 
 builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension
 
-@[export lean_add_projection_info]
 def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
   projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass }
 
 namespace Environment
 
-@[export lean_get_projection_info]
 def getProjectionFnInfo? (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
   projectionFnInfoExt.find? env projName
 

src/library/CMakeLists.txt

@@ -3,7 +3,6 @@ add_library(library OBJECT expr_lt.cpp
   module.cpp dynlib.cpp replace_visitor.cpp num.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   reducible.cpp init_module.cpp
-  projection.cpp
   aux_recursors.cpp
   profiling.cpp time_task.cpp
   formatter.cpp

src/library/projection.cpp

@@ -1,35 +0,0 @@
-/*
-Copyright (c) 2015 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/instantiate.h"
-#include "kernel/inductive.h"
-#include "library/util.h"
-#include "library/projection.h"
-
-namespace lean {
-extern "C" object * lean_mk_projection_info(object * ctor_name, object * nparams, object * i, uint8 from_class);
-extern "C" uint8 lean_projection_info_from_class(object * info);
-
-projection_info::projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit):
-    object_ref(lean_mk_projection_info(c.to_obj_arg(), nat(nparams).to_obj_arg(), nat(i).to_obj_arg(), inst_implicit)) {
-}
-
-bool projection_info::is_inst_implicit() const { return lean_projection_info_from_class(to_obj_arg()); }
-
-extern "C" object* lean_add_projection_info(object* env, object* p, object* ctor, object* nparams, object* i, uint8 fromClass);
-extern "C" object* lean_get_projection_info(object* env, object* p);
-
-elab_environment save_projection_info(elab_environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) {
-    return elab_environment(lean_add_projection_info(env.to_obj_arg(), p.to_obj_arg(), mk.to_obj_arg(), mk_nat_obj(nparams), mk_nat_obj(i), inst_implicit));
-}
-
-optional<projection_info> get_projection_info(elab_environment const & env, name const & p) {
-    return to_optional<projection_info>(lean_get_projection_info(env.to_obj_arg(), p.to_obj_arg()));
-}
-}

src/library/projection.h

@@ -1,56 +0,0 @@
-/*
-Copyright (c) 2015 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/elab_environment.h"
-
-namespace lean {
-/** \brief Auxiliary information attached to projections. This information
-    is used to simplify projection over constructor (efficiently).
-
-    That is, given a projection pr_i associated with the constructor mk
-    where A are parameters, we want to implement the following reduction
-    efficiently. The idea is to avoid unfolding pr_i.
-
-       pr_i A (mk A f_1 ... f_n) ==> f_i
-
-    We also use this information in the rewriter/simplifier.
-*/
-class projection_info : public object_ref {
-public:
-    projection_info(name const & c, unsigned nparams, unsigned i, bool inst_implicit);
-    projection_info():projection_info(name(), 0, 0, false) {}
-    projection_info(projection_info const & other):object_ref(other) {}
-    projection_info(projection_info && other) noexcept:object_ref(std::move(other)) {}
-    /* low-level constructors */
-    explicit projection_info(object * o):object_ref(o) {}
-    explicit projection_info(b_obj_arg o, bool b):object_ref(o, b) {}
-    explicit projection_info(object_ref const & o):object_ref(o) {}
-    projection_info & operator=(projection_info const & other) { object_ref::operator=(other); return *this; }
-    projection_info & operator=(projection_info && other) noexcept { object_ref::operator=(std::move(other)); return *this; }
-    name const & get_constructor() const { return static_cast<name const &>(cnstr_get_ref(*this, 0)); }
-    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 1)).get_small_value(); }
-    unsigned get_i() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
-    bool is_inst_implicit() const;
-};
-
-/** \brief Mark \c p as a projection in the given elab_environment and store that
-    \c mk is the constructor associated with it, \c nparams is the number of parameters, and
-    \c i says that \c p is the i-th projection.
-*/
-elab_environment save_projection_info(elab_environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i,
-                                 bool inst_implicit);
-
-/** \brief If \c p is a projection in the given elab_environment, then return the information
-    associated with it (constructor, number of parameters, and index).
-    If \c p is not a projection, then return nullptr.
-*/
-optional<projection_info> get_projection_info(elab_environment const & env, name const & p);
-
-inline bool is_projection(elab_environment const & env, name const & n) {
-    return static_cast<bool>(get_projection_info(env, n));
-}
-}

src/library/util.cpp

@@ -17,7 +17,6 @@ Author: Leonardo de Moura
 #include "library/suffixes.h"
 #include "library/annotation.h"
 #include "library/constants.h"
-#include "library/projection.h"
 #include "library/replace_visitor.h"
 #include "library/num.h"
 #include "githash.h" // NOLINT