From fdfff29bb13107116d5f52aad06171a96232a4e0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Dec 2019 08:10:40 -0800
Subject: [PATCH] feat: expose `liftLooseBVars` and `lowerLooseBVars`

---
 src/Init/Lean/Expr.lean   | 12 ++++++++++++
 src/kernel/expr.cpp       | 16 ++++++++++++++++
 tests/lean/run/expr1.lean | 14 ++++++++++++++
 3 files changed, 42 insertions(+)

diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index 9d5313ba83..8956f43c8c 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -547,6 +547,18 @@ e.looseBVarRange > 0
 @[extern "lean_expr_has_loose_bvar"]
 constant hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool := arbitrary _
 
+/--
+  Lower the loose bound variables `>= s` in `e` by `d`.
+  That is, a loose bound variable `bvar i`.
+  `i >= s` is mapped into `bvar (i-d)`. -/
+@[extern "lean_expr_lower_loose_bvars"]
+constant lowerLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _
+
+/--
+  Lift loose bound variables `>= s` in `e` by `d`. -/
+@[extern "lean_expr_lift_loose_bvars"]
+constant liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr := arbitrary _
+
 /-- 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"]
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 88da2c5bbc..184efddb1a 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -480,6 +480,14 @@ expr lower_loose_bvars(expr const & e, unsigned d) {
     return lower_loose_bvars(e, d, d);
 }
 
+extern "C" object * lean_expr_lower_loose_bvars(b_obj_arg e, b_obj_arg s, b_obj_arg d) {
+    if (!lean_is_scalar(s) || !lean_is_scalar(d) || lean_unbox(s) < lean_unbox(d)) {
+        lean_inc(e);
+        return e;
+    }
+    return lower_loose_bvars(TO_REF(expr, e), lean_unbox(s), lean_unbox(d)).steal();
+}
+
 expr lift_loose_bvars(expr const & e, unsigned s, unsigned d) {
     if (d == 0 || s >= get_loose_bvar_range(e))
         return e;
@@ -501,6 +509,14 @@ expr lift_loose_bvars(expr const & e, unsigned d) {
     return lift_loose_bvars(e, 0, d);
 }
 
+extern "C" object * lean_expr_lift_loose_bvars(b_obj_arg e, b_obj_arg s, b_obj_arg d) {
+    if (!lean_is_scalar(s) || !lean_is_scalar(d)) {
+        lean_inc(e);
+        return e;
+    }
+    return lift_loose_bvars(TO_REF(expr, e), lean_unbox(s), lean_unbox(d)).steal();
+}
+
 // =======================================
 // Implicit argument inference
 
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index 159261991c..3ba2799f88 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -92,3 +92,17 @@ do let f   := mkConst `f [];
    pure ()
 
 #eval tst5
+
+def tst6 : IO Unit := do
+let x1 := mkBVar 0;
+let x2 := mkBVar 1;
+let t1 := mkApp2 (mkConst `f) x1 x2;
+let t2 := mkForall `x BinderInfo.default (mkConst `Nat) t1;
+IO.println (t1.liftLooseBVars 0 1);
+IO.println (t2.liftLooseBVars 0 1);
+let t3 := (t2.liftLooseBVars 0 1).lowerLooseBVars 1 1;
+IO.println $ t3;
+unless (t2 == t3) $ throw "failed-1";
+pure ()
+
+#eval tst6