feat: Handle delay assigned mvars

Pantograph/Goal.lean

@@ -98,7 +98,8 @@ Brings into scope a list of goals
 -/
 protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
   if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
-    .error s!"Goals not in scope"
+    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
+    .error s!"Goals {invalid_goals} are not in scope"
   else
     -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
     let unassigned := goals.filter (λ goal =>

Pantograph/Library.lean

@@ -176,9 +176,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
     state.restoreMetaM
     return {
       root? := ← state.rootExpr?.mapM (λ expr => do
-        serializeExpression options (← unfoldAuxLemmas expr)),
+        serializeExpression options (← instantiateAll expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serializeExpression options (← unfoldAuxLemmas expr)),
+        serializeExpression options (← instantiateAll expr)),
     }
 @[export pantograph_goal_diag_m]
 def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=

Pantograph/Serial.lean

@@ -18,6 +18,23 @@ namespace Pantograph
 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)
+
+def instantiateAll (e: Expr): MetaM Expr := do
+  let e ← instantiateMVars e
+  let e ← unfoldAuxLemmas e
+  --let e ← instantiatePartialDelayedMVars e
+  return e
+
 --- Input Functions ---
 
 /-- Read syntax object from string -/
@@ -84,6 +101,7 @@ partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
   | _, .zero => s!"{k}"
   | _, _ => s!"(+ {u_str} {k})"
 
+
 /--
  Completely serializes an expression tree. Json not used due to compactness
 
@@ -92,7 +110,37 @@ A `_` symbol in the AST indicates automatic deductions not present in the origin
 partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
   self expr
   where
-  self (e: Expr): MetaM String :=
+  delayedMVarToSexp (e: Expr): MetaM (Option String) := do
+    let .mvar mvarId := e.getAppFn | return .none
+    let .some decl ← getDelayedMVarAssignment? mvarId | return .none
+    let mvarIdPending := decl.mvarIdPending
+    -- Print the function application e. See Lean's `withOverApp`
+    let args := e.getAppArgs
+
+    -- Not enough arguments to instantiate this
+    if args.size < decl.fvars.size then
+      return .none
+
+    let callee ← self $ ← instantiateMVars $ .mvar mvarIdPending
+    let sites ←
+      decl.fvars.zip args |>.mapM (λ (fvar, arg) => do
+        let fvarName := Expr.fvarId! fvar |>.name
+        return s!"({toString fvarName} {← self arg})"
+      )
+    let tailArgs ← args.toList.drop decl.fvars.size |>.mapM self
+
+
+    let sites := " ".intercalate sites.toList
+    let result := if tailArgs.isEmpty then
+        s!"(:subst {callee} {sites})"
+      else
+        let tailArgs := " ".intercalate tailArgs
+        s!"((:subst {callee} {sites}) {tailArgs})"
+    return .some result
+
+  self (e: Expr): MetaM String := do
+    if let .some result ← delayedMVarToSexp e then
+      return result
     match e with
     | .bvar deBruijnIndex =>
       -- This is very common so the index alone is shown. Literals are handled below.
@@ -103,11 +151,9 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       let name := ofName fvarId.name
       pure s!"(:fv {name})"
     | .mvar mvarId => do
-      if ← mvarId.isDelayedAssigned then
-        pure s!"(:mv)"
-      else
+        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
         let name := ofName mvarId.name
-        pure s!"(:mv {name})"
+        pure s!"(:{pref} {name})"
     | .sort level =>
       let level := serializeSortLevel level sanitize
       pure s!"(:sort {level})"
@@ -210,7 +256,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
       match localDecl with
       | .cdecl _ fvarId userName type _ _ =>
         let userName := userName.simpMacroScopes
-        let type ← instantiateMVars type
+        let type ← instantiate type
         return {
           name := ofName fvarId.name,
           userName:= ofName userName,
@@ -219,9 +265,9 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         }
       | .ldecl _ fvarId userName type val _ _ => do
         let userName := userName.simpMacroScopes
-        let type ← instantiateMVars type
+        let type ← instantiate type
         let value? ← if showLetValues then
-          let val ← instantiateMVars val
+          let val ← instantiate val
           pure $ .some (← serializeExpression options val)
         else
           pure $ .none
@@ -248,10 +294,11 @@ 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 (← instantiateMVars mvarDecl.type)),
+      target := (← serializeExpression options (← instantiateAll mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where
+  instantiate := instantiateAll
   ofName (n: Name) := serializeName n (sanitize := false)
 
 protected def GoalState.serializeGoals

Test/Metavar.lean

@@ -263,7 +263,7 @@ def test_partial_continuation: TestM Unit := do
 
   -- Continuation should fail if the state does not exist:
   match state0.resume coupled_goals with
-  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals not in scope")
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
   | .ok _ => addTest $ assertUnreachable "(continuation failure)"
   -- Continuation should fail if some goals have not been solved
   match state2.continue state1 with

Test/Proofs.lean

@@ -243,9 +243,10 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
   let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
-  -- This is due to delayed assignment
+  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) (_uniq.54 (:fv _uniq.16)) (_uniq.55 (:fv _uniq.50))) (_uniq.50 0))) (_uniq.47 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) (_uniq.67 (:fv _uniq.16)) (_uniq.68 (:fv _uniq.63))) (_uniq.63 0))) (_uniq.60 0))))"
+  let extra := "((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))"
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+    s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state
@@ -769,13 +770,34 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with
+  addTest $ LSpec.check tactic $ state3m2.goals.map (·.name.toString) = ["_uniq.85", "_uniq.86", "_uniq.84"]
+  let [_motive, _major, _step, conduit] := state2.goals | panic! "Goals conflict"
+  let state2b ← match state3m2.resume [conduit] with
     | .ok state => pure state
     | .error e => do
       addTest $ assertUnreachable e
       return ()
-  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
-    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
+
+  let cNatAdd := "(:c HAdd.hAdd) (:c Nat) (:c Nat) (:c Nat) ((:c instHAdd) (:c Nat) (:c instAddNat))"
+  let cNat0 := "((:c OfNat.ofNat) (:c Nat) (:lit 0) ((:c instOfNatNat) (:lit 0)))"
+  let fvN := "_uniq.63"
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
+    #[
+      {
+        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 _uniq.84) (:mv _uniq.85) (:mv _uniq.86)) (_uniq.77 (:mv _uniq.68))) ((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN})))",
+        },
+        vars := #[{
+          name := fvN,
+          userName := "n",
+          type? := .some { pp? := .some "Nat", sexp? := .some "(:c Nat)" },
+          isInaccessible? := .some false
+        }],
+      }
+    ])
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [

Test/Serial.lean

@@ -52,6 +52,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
     ("λ x: Array Nat => x.data", "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"),
     -- This tests `autoBoundImplicit`
     ("λ {α : Sort (u + 1)} => List α", "(:lambda α (:sort (+ u 1)) ((:c List) 0) :implicit)"),
+    ("(2: Nat) <= (5: Nat)", "((:c LE.le) (:mv _uniq.37) (:mv _uniq.38) ((:c OfNat.ofNat) (:mv _uniq.23) (:lit 2) (:mv _uniq.24)) ((:c OfNat.ofNat) (:mv _uniq.33) (:lit 5) (:mv _uniq.34)))"),
   ]
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (source, target) => do
     let env ← MonadEnv.getEnv

Test/Tactic/MotivatedApply.lean

@@ -93,12 +93,50 @@ def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
       tests := tests ++ test
       return tests
 
+def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
+  let expr := "λ (n t: Nat) => n + 0 = n"
+  runMetaMSeq env $ runTermElabMInMeta do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "@Nat.brecOn")
+      (fileName := filename) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    let (expr, exprType) ← valueAndType expr
+    Meta.lambdaTelescope expr $ λ _ body => do
+      let mut tests := LSpec.TestSeq.done
+      -- Apply the tactic
+      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      let tactic := Tactic.motivatedApply recursor
+      let newGoals ← runTacticOnMVar tactic target.mvarId!
+      tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+        [
+          "Nat → Prop",
+          "Nat",
+          "∀ (t : Nat), Nat.below t → ?motive t",
+          "?motive ?m.69 = (n + 0 = n)",
+        ]))
+      let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
+      tests := tests ++ (LSpec.check "goal name" (major.name.toString = "_uniq.69"))
+
+      -- Assign motive to `λ x => x + _`
+      let (motive_assign, _) ← valueAndType "λ (x: Nat) => @Nat.add x + 0 = _"
+      motive.assign motive_assign
+
+      let test ← conduit.withContext do
+        let t := toString (← Meta.ppExpr $ ← conduit.getType)
+        return LSpec.check "conduit" (t = "(?m.69.add + 0 = ?m.140 ?m.69) = (n + 0 = n)")
+      tests := tests ++ test
+
+      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("type_extract", test_type_extract env),
-    ("nat_brec_on", test_nat_brec_on env),
-    ("list_brec_on", test_list_brec_on env),
+    ("Nat.brecOn", test_nat_brec_on env),
+    ("List.brecOn", test_list_brec_on env),
+    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env),
   ]
 
 end Pantograph.Test.Tactic.MotivatedApply