diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean index af7c70b726..4e5b0ca647 100644 --- a/src/Lean/ProjFns.lean +++ b/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 diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 0ae4d0dcdc..3457f188c6 100644 --- a/src/library/CMakeLists.txt +++ b/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 diff --git a/src/library/projection.cpp b/src/library/projection.cpp deleted file mode 100644 index 909b385ad0..0000000000 --- a/src/library/projection.cpp +++ /dev/null @@ -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 -#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 get_projection_info(elab_environment const & env, name const & p) { - return to_optional(lean_get_projection_info(env.to_obj_arg(), p.to_obj_arg())); -} -} diff --git a/src/library/projection.h b/src/library/projection.h deleted file mode 100644 index d9d237c8f5..0000000000 --- a/src/library/projection.h +++ /dev/null @@ -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(cnstr_get_ref(*this, 0)); } - unsigned get_nparams() const { return static_cast(cnstr_get_ref(*this, 1)).get_small_value(); } - unsigned get_i() const { return static_cast(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 get_projection_info(elab_environment const & env, name const & p); - -inline bool is_projection(elab_environment const & env, name const & n) { - return static_cast(get_projection_info(env, n)); -} -} diff --git a/src/library/util.cpp b/src/library/util.cpp index 93b0a4545c..5335fb430e 100644 --- a/src/library/util.cpp +++ b/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