Pantograph/Goal.lean

@@ -98,8 +98,7 @@ 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
-    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
-    .error s!"Goals {invalid_goals} are not in scope"
+    .error s!"Goals 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 (← instantiateAll expr)),
+        serializeExpression options (← unfoldAuxLemmas expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serializeExpression options (← instantiateAll expr)),
+        serializeExpression options (← unfoldAuxLemmas expr)),
     }
 @[export pantograph_goal_diag_m]
 def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : Lean.CoreM String :=

Pantograph/Serial.lean

@@ -18,23 +18,6 @@ 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 -/
@@ -101,7 +84,6 @@ 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
 
@@ -110,37 +92,7 @@ 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
-  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
+  self (e: Expr): MetaM String :=
     match e with
     | .bvar deBruijnIndex =>
       -- This is very common so the index alone is shown. Literals are handled below.
@@ -151,9 +103,11 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
       let name := ofName fvarId.name
       pure s!"(:fv {name})"
     | .mvar mvarId => do
-        let pref := if ← mvarId.isDelayedAssigned then "mvd" else "mv"
+      if ← mvarId.isDelayedAssigned then
+        pure s!"(:mv)"
+      else
         let name := ofName mvarId.name
-        pure s!"(:{pref} {name})"
+        pure s!"(:mv {name})"
     | .sort level =>
       let level := serializeSortLevel level sanitize
       pure s!"(:sort {level})"
@@ -256,7 +210,7 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
       match localDecl with
       | .cdecl _ fvarId userName type _ _ =>
         let userName := userName.simpMacroScopes
-        let type ← instantiate type
+        let type ← instantiateMVars type
         return {
           name := ofName fvarId.name,
           userName:= ofName userName,
@@ -265,9 +219,9 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
         }
       | .ldecl _ fvarId userName type val _ _ => do
         let userName := userName.simpMacroScopes
-        let type ← instantiate type
+        let type ← instantiateMVars type
         let value? ← if showLetValues then
-          let val ← instantiate val
+          let val ← instantiateMVars val
           pure $ .some (← serializeExpression options val)
         else
           pure $ .none
@@ -294,11 +248,10 @@ 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 (← instantiateMVars 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 [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope")
+  | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals 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,10 +243,9 @@ def test_or_comm: TestM Unit := do
   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) (_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)))"
+  -- This is due to delayed assignment
   addTest $ LSpec.test "(2 parent)" (state2parent ==
-    s!"((:subst {substHead} (_uniq.41 (:fv _uniq.16))) {extra}")
+    "((:mv) (: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
@@ -770,34 +769,13 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  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
+  let state2b ← match state3m2.resume (state3m2.goals ++ state2.goals) with
     | .ok state => pure state
     | .error e => do
       addTest $ assertUnreachable e
       return ()
-
-  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
-        }],
-      }
-    ])
+  addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
+    #[buildGoal [("n", "Nat"), ("t", "Nat"), ("h", "Nat.below t")] "t + 0 = t"])
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   let tests := [

Test/Serial.lean

@@ -52,7 +52,6 @@ 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,50 +93,12 @@ 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.brecOn", test_nat_brec_on env),
-    ("List.brecOn", test_list_brec_on env),
-    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env),
+    ("nat_brec_on", test_nat_brec_on env),
+    ("list_brec_on", test_list_brec_on env),
   ]
 
 end Pantograph.Test.Tactic.MotivatedApply