feat: expose liftLooseBVars and lowerLooseBVars

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"]

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
 

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