feat(library/init/lean/expr): add abstractRange

library/init/lean/expr.lean

@@ -102,14 +102,22 @@ def isAppOfArity : Expr → Name → Nat → Bool
 | Expr.app f _,   n, a+1 => isAppOfArity f n a
 | _,              _, _   => false
 
+/-- Instantiate the loose bound variables in `e` using `subst`.
+    That is, a loose `Expr.bvar i` is replaced with `subst[i]`. -/
 @[extern "lean_expr_instantiate"]
-constant instantiate : Expr → Array Expr → Expr := default _
+constant instantiate (e : Expr) (subst : Array Expr) : Expr := default _
 
+/-- Similar to instantiate, but `Expr.bvar i` is replaced with `subst[subst.size - i - 1]` -/
 @[extern "lean_expr_instantiate_rev"]
-constant instantiateRev : Expr → Array Expr → Expr := default _
+constant instantiateRev (e : Expr) (subst : Array Expr) : Expr := default _
 
+/-- Replace free variables `xs` with loose bound variables. -/
 @[extern "lean_expr_abstract"]
-constant abstract : Expr → Array Expr → Expr := default _
+constant abstract (e : Expr) (xs : Array Expr) : Expr := default _
+
+/-- Similar to `abstract`, but consider only the first `min n xs.size` entries in `xs`. -/
+@[extern "lean_expr_abstract_range"]
+constant abstractRange (e : Expr) (n : Nat) (xs : Array Expr) : Expr := default _
 
 end Expr
 

src/kernel/abstract.cpp

@@ -36,13 +36,13 @@ expr abstract(expr const & e, name const & n) {
     return abstract(e, 1, &fvar);
 }
 
-extern "C" object * lean_expr_abstract(object * e0, object * subst) {
+static object * lean_expr_abstract_core(object * e0, size_t n, object * subst) {
+    lean_assert(n <= lean_array_size(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
@@ -50,7 +50,8 @@ extern "C" object * lean_expr_abstract(object * e0, object * subst) {
                 size_t i = n;
                 while (i > 0) {
                     --i;
-                    if (fvar_name_core(lean_array_get_core(subst, i)) == fvar_name(m))
+                    object * v = lean_array_get_core(subst, i);
+                    if (is_fvar_core(v) && fvar_name_core(v) == fvar_name(m))
                         return some_expr(mk_bvar(offset + n - i - 1));
                 }
                 return none_expr();
@@ -60,6 +61,16 @@ extern "C" object * lean_expr_abstract(object * e0, object * subst) {
     return r.steal();
 }
 
+extern "C" object * lean_expr_abstract_range(object * e, object * n, object * subst) {
+    if (!lean_is_scalar(n))
+        return lean_expr_abstract_core(e, lean_array_size(subst), subst);
+    else
+        return lean_expr_abstract_core(e, std::min(lean_unbox(n), lean_array_size(subst)), subst);
+}
+
+extern "C" object * lean_expr_abstract(object * e, object * subst) {
+    return lean_expr_abstract_core(e, lean_array_size(subst), subst);
+}
 
 /* ------ LEGACY CODE -------------
    The following API is to support legacy

tests/playground/abst.lean

@@ -15,4 +15,8 @@ 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;
+let p := t.abstractRange 1 [x, y].toArray;
+IO.println p.dbgToString;
+let p := t.abstractRange 3 [x, y].toArray;
+IO.println p.dbgToString;
 pure ()