From 75e5f5bfd888a3aa022d973d50f953ce50201fbf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Sep 2019 18:34:45 -0700
Subject: [PATCH] feat(library/init/lean/expr): expose `abstract`

---
 library/init/lean/expr.lean |  3 +++
 src/kernel/abstract.cpp     | 25 +++++++++++++++++++++++++
 src/kernel/expr.h           |  3 +++
 tests/playground/abst.lean  | 18 ++++++++++++++++++
 4 files changed, 49 insertions(+)
 create mode 100644 tests/playground/abst.lean

diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean
index b1478bdf22..fd6790581a 100644
--- a/library/init/lean/expr.lean
+++ b/library/init/lean/expr.lean
@@ -108,6 +108,9 @@ constant instantiate : Expr → Array Expr → Expr := default _
 @[extern "lean_expr_instantiate_rev"]
 constant instantiateRev : Expr → Array Expr → Expr := default _
 
+@[extern "lean_expr_abstract"]
+constant abstract : Expr → Array Expr → Expr := default _
+
 end Expr
 
 def mkConst (n : Name) (ls : List Level := []) : Expr :=
diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 9f357f0f08..609d43b1f7 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -36,6 +36,31 @@ expr abstract(expr const & e, name const & n) {
     return abstract(e, 1, &fvar);
 }
 
+extern "C" object * lean_expr_abstract(object * e0, object * subst) {
+    expr const & e = reinterpret_cast<expr const &>(e0);
+    if (!has_fvar(e)) {
+        lean_inc(e0);
+        return e0;
+    }
+    size_t n = lean_array_size(subst);
+    expr r = replace(e, [=](expr const & m, unsigned offset) -> optional<expr> {
+            if (!has_fvar(m))
+                return some_expr(m); // expression m does not contain free variables
+            if (is_fvar(m)) {
+                size_t i = n;
+                while (i > 0) {
+                    --i;
+                    if (fvar_name_core(lean_array_get_core(subst, i)) == fvar_name(m))
+                        return some_expr(mk_bvar(offset + n - i - 1));
+                }
+                return none_expr();
+            }
+            return none_expr();
+        });
+    return r.steal();
+}
+
+
 /* ------ LEGACY CODE -------------
    The following API is to support legacy
    code where the type of a local constant (aka free variable)
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 0585820161..786c75a4a4 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -158,7 +158,9 @@ struct expr_pair_eq {
 
 // =======================================
 // Testers
+static expr_kind expr_kind_core(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
 inline bool is_bvar(expr const & e)        { return e.kind() == expr_kind::BVar; }
+inline bool is_fvar_core(object * o)       { return expr_kind_core(o) == expr_kind::FVar; }
 inline bool is_fvar(expr const & e)        { return e.kind() == expr_kind::FVar; }
 inline bool is_const(expr const & e)       { return e.kind() == expr_kind::Const; }
 inline bool is_mvar(expr const & e)        { return e.kind() == expr_kind::MVar; }
@@ -228,6 +230,7 @@ inline nat const &     proj_idx(expr const & e)              { lean_assert(is_pr
 inline expr const &    proj_expr(expr const & e)             { lean_assert(is_proj(e)); return static_cast<expr const &>(cnstr_get_ref(e, 2)); }
 inline nat const &     bvar_idx(expr const & e)              { lean_assert(is_bvar(e)); return static_cast<nat const &>(cnstr_get_ref(e, 0)); }
 inline bool            is_bvar(expr const & e, unsigned i)   { return is_bvar(e) && bvar_idx(e) == i; }
+inline name const &    fvar_name_core(object * o)            { lean_assert(is_fvar_core(o)); return static_cast<name const &>(cnstr_get_ref(o, 0)); }
 inline name const &    fvar_name(expr const & e)             { lean_assert(is_fvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
 inline level const &   sort_level(expr const & e)            { lean_assert(is_sort(e)); return static_cast<level const &>(cnstr_get_ref(e, 0)); }
 inline name const &    mvar_name(expr const & e)             { lean_assert(is_mvar(e)); return static_cast<name const &>(cnstr_get_ref(e, 0)); }
diff --git a/tests/playground/abst.lean b/tests/playground/abst.lean
new file mode 100644
index 0000000000..9a4d4209b0
--- /dev/null
+++ b/tests/playground/abst.lean
@@ -0,0 +1,18 @@
+import init.lean.expr
+open Lean
+
+def main (xs : List String) : IO Unit :=
+do
+let f := mkConst `f;
+let x := Expr.fvar `x;
+let y := Expr.fvar `y;
+let t := Expr.app (Expr.app (Expr.app f x) y) (Expr.app f x);
+IO.println t.dbgToString;
+let p := t.abstract [x, y].toArray;
+IO.println p.dbgToString;
+IO.println (p.instantiateRev [x, y].toArray).dbgToString;
+let a := mkConst `a;
+let b := Expr.app f (mkConst `b);
+IO.println (p.instantiateRev [a, b].toArray).dbgToString;
+IO.println (p.instantiate [a].toArray).dbgToString;
+pure ()