fix: Nested delayed assignment instantiation

Pantograph/Expr.lean

@@ -10,29 +10,94 @@ def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
-def instantiatePartialDelayedMVars (e: Expr): MetaM Expr := do
-  Meta.transform e
-    (pre := fun e => e.withApp fun f args => do
-      if let .mvar mvarId := f then
-        if let some decl ← getDelayedMVarAssignment? mvarId then
-          if args.size ≥ decl.fvars.size then
-            let pending ← instantiateMVars (.mvar decl.mvarIdPending)
-            if !pending.isMVar then
-              return .visit <| (← Meta.mkLambdaFVars decl.fvars pending).beta args
-      return .continue)
+/--
+Force the instantiation of delayed metavariables even if they cannot be fully
+instantiated. This is used during resumption.
 
+Since Lean 4 does not have an `Expr` constructor corresponding to delayed
+metavariables, any delayed metavariables must be recursively handled by this
+function to ensure that nested delayed metavariables can be properly processed.
+The caveat is this recursive call will lead to infinite recursion if a loop
+between metavariable assignment exists.
+
+This function ensures any metavariable in the result is either
+1. Delayed assigned with its pending mvar not assigned in any form
+2. Not assigned (delay or not)
+ -/
+partial def instantiateDelayedMVars (eOrig: Expr): MetaM Expr := do
+  --let padding := String.join $ List.replicate level "  "
+  --IO.println s!"{padding}Starting {toString eOrig}"
+  let result ← Meta.transform (← instantiateMVars eOrig)
+    (pre := fun e => e.withApp fun f args => do
+      --IO.println s!"{padding} V {toString e}"
+      if let .mvar mvarId := f then
+        if ← mvarId.isAssigned then
+          --IO.println s!"{padding} A ?{mvarId.name}"
+          return .continue <| .some (← self e)
+        if let some { fvars, mvarIdPending } ← getDelayedMVarAssignment? mvarId then
+          -- No progress can be made on this
+          if !(← mvarIdPending.isAssigned) then
+            --IO.println s!"{padding} D/T1: {toString e}"
+            let args ← args.mapM self
+            let result := mkAppN f args
+            return .done result
+
+          --IO.println s!"{padding} D ?{mvarId.name} := [{fvars.size}] ?{mvarIdPending.name}"
+          -- This asstion fails when a tactic or elaboration function is
+          -- implemented incorrectly. See `instantiateExprMVars`
+          if args.size < fvars.size then
+            --IO.println s!"{padding} Illegal callsite: {args.size} < {fvars.size}"
+            throwError "Not enough arguments to instantiate a delay assigned mvar. This is due to bad implementations of a tactic: {args.size} < {fvars.size}. Expr: {toString e}; Origin: {toString eOrig}"
+          assert! !(← mvarIdPending.isDelayedAssigned)
+          let pending ← self (.mvar mvarIdPending)
+          if pending == .mvar mvarIdPending then
+            -- No progress could be made on this case
+            --IO.println s!"{padding}D/N {toString e}"
+            assert! !(← mvarIdPending.isAssigned)
+            assert! !(← mvarIdPending.isDelayedAssigned)
+          --else if pending.isMVar then
+          --  assert! !(← pending.mvarId!.isAssigned)
+          --  assert! !(← pending.mvarId!.isDelayedAssigned)
+          --  -- Progress made, but this is now another delayed assigned mvar
+          --  let nextMVarId ← mkFreshMVarId
+          --  assignDelayedMVar nextMVarId fvars pending.mvarId!
+          --  let args ← args.mapM self
+          --  let result := mkAppN (.mvar nextMVarId) args
+          --  return .done result
+          else
+            -- Progress has been made on this mvar
+            let pending := pending.abstract fvars
+            let args ← args.mapM self
+            -- Craete the function call structure
+            let subst := pending.instantiateRevRange 0 fvars.size args
+            let result := mkAppRange subst fvars.size args.size args
+            --IO.println s!"{padding}D/T2 {toString result}"
+            return .done result
+      return .continue)
+  --IO.println s!"{padding}Result {toString result}"
+  return result
+  where
+  self e := instantiateDelayedMVars e
+
+/--
+Convert an expression to an equiavlent form with
+1. No nested delayed assigned mvars
+2. No aux lemmas
+3. No assigned mvars
+ -/
 @[export pantograph_instantiate_all_meta_m]
 def instantiateAll (e: Expr): MetaM Expr := do
-  let e ← instantiateMVars e
+  let e ← instantiateDelayedMVars e
   let e ← unfoldAuxLemmas e
-  --let e ← instantiatePartialDelayedMVars e
   return e
 
 structure DelayedMVarInvocation where
   mvarIdPending: MVarId
   args: Array (FVarId × (Option Expr))
+  -- Extra arguments applied to the result of this substitution
   tail: Array Expr
 
+-- The pending mvar of any delayed assigned mvar must not be assigned in any way.
 @[export pantograph_to_delayed_mvar_invocation_meta_m]
 def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
   let .mvar mvarId := e.getAppFn | return .none
@@ -42,7 +107,9 @@ def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := d
   -- Print the function application e. See Lean's `withOverApp`
   let args := e.getAppArgs
 
-  assert! args.size >= decl.fvars.size
+  assert! args.size ≥ decl.fvars.size
+  assert! !(← mvarIdPending.isAssigned)
+  assert! !(← mvarIdPending.isDelayedAssigned)
   let fvarArgMap: HashMap FVarId Expr := HashMap.ofList $ (decl.fvars.map (·.fvarId!) |>.zip args).toList
   let subst ← mvarDecl.lctx.foldlM (init := []) λ acc localDecl => do
     let fvarId := localDecl.fvarId

Pantograph/Serial.lean

@@ -91,7 +91,7 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
   where
   delayedMVarToSexp (e: Expr): MetaM (Option String) := do
     let .some invocation ← toDelayedMVarInvocation e | return .none
-    let callee ← self $ ← instantiateMVars $ .mvar invocation.mvarIdPending
+    let callee ← self $ .mvar invocation.mvarIdPending
     let sites ← invocation.args.mapM (λ (fvarId, arg) => do
         let arg := match arg with
           | .some arg => arg
@@ -264,7 +264,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
       name := ofName goal.name,
       userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
-      target := (← serializeExpression options (← instantiateAll mvarDecl.type)),
+      target := (← serializeExpression options (← instantiate mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where

Test/Integration.lean

@@ -88,11 +88,11 @@ def test_tactic : IO LSpec.TestSeq :=
     vars := #[{ name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
   }
   let goal2: Protocol.Goal := {
-    name := "_uniq.14",
+    name := "_uniq.17",
     target := { pp? := .some "x ∨ y → y ∨ x" },
     vars := #[
       { name := "_uniq.10", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }},
-      { name := "_uniq.13", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
+      { name := "_uniq.16", userName := "y", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}
     ],
   }
   subroutine_runner [

Test/Proofs.lean

@@ -226,11 +226,25 @@ def test_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
+  let fvP := "_uniq.10"
+  let fvQ := "_uniq.13"
+  let fvH := "_uniq.16"
+  let state1g0 := "_uniq.17"
+  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)) =
+    #[{
+      name := state1g0,
+      target := { pp? := .some "q ∨ p" },
+      vars := #[
+        { name := fvP, userName := "p", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
+        { name := fvQ, userName := "q", type? := .some { pp? := .some "Prop" }, isInaccessible? := .some false },
+        { name := fvH, userName := "h", type? := .some { pp? := .some "p ∨ q" }, isInaccessible? := .some false }
+      ]
+    }])
   addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
   addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
 
+  let state1parent ← serializeExpressionSexp (← instantiateAll state1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(1 parent)" (state1parent == s!"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda h ((:c Or) 1 0) (:subst (:mv {state1g0}) (:fv {fvP}) (:fv {fvQ}) 0))))")
   let tactic := "cases h"
   let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
@@ -239,22 +253,25 @@ def test_or_comm: TestM Unit := do
       return ()
   addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
     #[branchGoal "inl" "p", branchGoal "inr" "q"])
+  let (caseL, caseR) := ("_uniq.62", "_uniq.75")
+  addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.name) =
+    #[caseL, caseR])
   addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
-  let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-  let substHead := "((:c Or.casesOn) (:fv _uniq.10) (:fv _uniq.13) (:lambda t._@._hyg.26 ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:forall h ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) 0) ((:c Or) (:fv _uniq.13) (:fv _uniq.10)))) (:fv _uniq.16) (:lambda h._@._hyg.27 (:fv _uniq.10) (:subst (:lambda h._@._hyg.28 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inl) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47))) (:subst (:subst (:mv _uniq.59) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.47) (:fv _uniq.16) (:fv _uniq.50)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.47) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)) (:lambda h._@._hyg.29 (:fv _uniq.13) (:subst (:lambda h._@._hyg.30 ((:c Eq) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16) ((:c Or.inr) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60))) (:subst (:subst (:mv _uniq.72) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.60) (:fv _uniq.16) (:fv _uniq.63)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.60) 0)) (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) 0)))"
-  let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16))"
+  let state2parent ← serializeExpressionSexp (← instantiateAll state2.parentExpr?.get!) (sanitize := false)
+  let orPQ := s!"((:c Or) (:fv {fvP}) (:fv {fvQ}))"
+  let orQP := s!"((:c Or) (:fv {fvQ}) (:fv {fvP}))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    s!"((:subst {substHead} (:fv _uniq.10) (:fv _uniq.13) (:fv _uniq.16) (:fv _uniq.16)) {extra})")
+    s!"((:c Or.casesOn) (:fv {fvP}) (:fv {fvQ}) (:lambda t._@._hyg.26 {orPQ} (:forall h ((:c Eq) {orPQ} (:fv {fvH}) 0) {orQP})) (:fv {fvH}) (:lambda h._@._hyg.27 (:fv {fvP}) (:lambda h._@._hyg.28 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inl) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseL}))) (:lambda h._@._hyg.29 (:fv {fvQ}) (:lambda h._@._hyg.30 ((:c Eq) {orPQ} (:fv {fvH}) ((:c Or.inr) (:fv {fvP}) (:fv {fvQ}) 0)) (:mv {caseR}))) ((:c Eq.refl) {orPQ} (:fv {fvH})))")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
+  let state3_1parent ← serializeExpressionSexp (← instantiateAll state3_1.parentExpr?.get!) (sanitize := false)
+  addTest $ LSpec.test "(3_1 parent)" (state3_1parent == s!"((:c Or.inr) (:fv {fvQ}) (:fv {fvP}) (:mv _uniq.87))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
     | .success state => pure state
@@ -262,8 +279,8 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false)
-  addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
+  let state4_1parent ← instantiateAll state4_1.parentExpr?.get!
+  addTest $ LSpec.test "(4_1 parent)" state4_1parent.isFVar
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
   let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with
     | .success state => pure state
@@ -771,7 +788,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let (eqL, eqR, eqT) := ("_uniq.85", "_uniq.86", "_uniq.84")
+  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
   addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = [eqL, eqR, eqT]
   let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
   let state2b ← match state3m2.resume [conduit] with
@@ -789,8 +806,8 @@ def test_nat_zero_add_alt: TestM Unit := do
         name := "_uniq.70",
         userName? := .some "conduit",
         target := {
-          pp? := .some "?m.79 ?m.68 = (n + 0 = n)",
-          sexp? := .some s!"((:c Eq) (:sort 0) (:subst ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) (:fv {fvN}) (:mv {major})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+          pp? := .some "(?motive.a = ?motive.a) = (n + 0 = n)",
+          sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) (:mv {eqT}) (:mv {eqL}) (:mv {eqR})) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
         },
         vars := #[{
           name := fvN,