fix: bug in instantiateRangeS'

This PR fixes a bug in the function `instantiateRangeS'` in the `Sym` framework.

Author: leodemoura

src/Lean/Meta/Sym/InstantiateS.lean

@@ -56,15 +56,13 @@ It assumes `beginIdx ≤ endIdx` and `endIdx ≤ subst.size`
 def instantiateRangeS' (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) : AlphaShareBuilderM Expr :=
   if _ : beginIdx > endIdx then unreachable! else
   if _ : endIdx > subst.size then unreachable! else
-  let s := beginIdx
   let n := endIdx - beginIdx
   replaceS' e fun e offset => do
-    let s₁ := s + offset
     match e with
     | .bvar idx =>
-      if _h : idx >= s₁ then
-        if _h : idx < s₁ + n then
-          let v := subst[idx - s₁]
+      if _h : idx >= offset then
+        if _h : idx < offset + n then
+          let v := subst[beginIdx + idx - offset]
           liftLooseBVarsS' v 0 offset
         else
           mkBVarS (idx - n)
@@ -73,7 +71,7 @@ def instantiateRangeS' (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) :
     | .lit _ | .mvar _ | .fvar _ | .const _ _ | .sort _ =>
       return some e
     | _ =>
-      if s₁ >= e.looseBVarRange then
+      if offset >= e.looseBVarRange then
         return some e
       else
         return none

tests/lean/run/instantiateRevBetaS.lean

@@ -0,0 +1,10 @@
+import Lean
+
+/-- info: (a + 1).add a -/
+#guard_msgs in
+open Lean Meta Sym in
+run_meta SymM.run do
+  let s₁ ← share <| mkLambda `x .default Nat.mkType (mkApp (mkConst ``Nat.add) (mkNatAdd (mkBVar 0) (mkNatLit 1)))
+  let s₂ ← share <| mkConst `a
+  let e  ← share <| mkApp2 (mkBVar 1) (mkBVar 0) (mkBVar 0)
+  logInfo <| (← instantiateRevBetaS e #[s₁, s₂])