From c73e628e50e6b0ddaed188eeb1e89106f4a0fbe3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Jun 2018 11:05:41 -0700 Subject: [PATCH] chore(kernel/abstract): add LEGACY comment --- src/kernel/abstract.cpp | 8 ++++++++ src/kernel/abstract.h | 9 +++++++++ 2 files changed, 17 insertions(+) diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp index 21a085e01e..82a8af1e7f 100644 --- a/src/kernel/abstract.cpp +++ b/src/kernel/abstract.cpp @@ -42,6 +42,14 @@ expr abstract(expr const & e, name const & l) { return abstract(e, 1, &local); } +/* ------ LEGACY CODE ------------- + The following API is to support legacy + code where the type of a local constant (aka free variable) + was stored in the local constant itself. + This approach was used in Lean2, and is being abandoned in Lean4. + + TODO(Leo): delete */ + template expr mk_binding(unsigned num, expr const * locals, expr const & b) { expr r = abstract(b, num, locals); diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h index ebbdc70db9..0f113539ef 100644 --- a/src/kernel/abstract.h +++ b/src/kernel/abstract.h @@ -14,6 +14,14 @@ expr abstract(expr const & e, unsigned n, expr const * s); inline expr abstract(expr const & e, expr const & s) { return abstract(e, 1, &s); } expr abstract(expr const & e, name const & l); +/* ------ LEGACY CODE ------------- + The following API is to support legacy + code where the type of a local constant (aka free variable) + was stored in the local constant itself. + This approach was used in Lean2, and is being abandoned in Lean4. + + TODO(Leo): delete */ + /** \brief Create a lambda-expression by abstracting the given local constants over b */ expr Fun(unsigned num, expr const * locals, expr const & b); inline expr Fun(expr const & local, expr const & b) { return Fun(1, &local, b); } @@ -25,4 +33,5 @@ expr Pi(unsigned num, expr const * locals, expr const & b); inline expr Pi(expr const & local, expr const & b) { return Pi(1, &local, b); } inline expr Pi(std::initializer_list const & locals, expr const & b) { return Pi(locals.size(), locals.begin(), b); } template expr Pi(T const & locals, expr const & b) { return Pi(locals.size(), locals.data(), b); } + }