feat: Partial instantiate metavariables

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 -/
@@ -103,11 +120,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 +225,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 +234,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 +263,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/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

@@ -245,7 +245,7 @@ def test_or_comm: TestM Unit := do
   let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
   -- This is due to delayed assignment
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    "((:mv) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
+    "((:mvd _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
 
   let state3_1 ← match ← state2.tryTactic (goalId := 0) (tactic := "apply Or.inr") with
     | .success state => pure state

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