Pantograph/Frontend/Basic.lean

@@ -60,7 +60,7 @@ def processOneCommand: FrontendM (CompilationStep × Bool) := do
   let s := (← get).commandState
   let before := s.env
   let done ← Elab.Frontend.processCommand
-  let stx := (← get).commands.back
+  let stx := (← get).commands.back!
   let src := (← read).inputCtx.input.toSubstring.extract (← get).cmdPos (← get).parserState.pos
   let s' := (← get).commandState
   let after := s'.env

Pantograph/Frontend/Elab.lean

@@ -70,9 +70,9 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
   | .context ctx tree => tree.filter p m |>.map (.context ctx)
   | .node info children =>
     if p info then
-      [.node info (children.toList.map (filter p m)).join.toPArray']
+      [.node info (children.toList.map (filter p m)).flatten.toPArray']
     else
-      (children.toList.map (filter p m)).join
+      (children.toList.map (filter p m)).flatten
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 end Lean.Elab.InfoTree
@@ -137,7 +137,8 @@ partial def findAllInfo (t : Elab.InfoTree) (context?: Option Elab.ContextInfo)
   match t with
   | .context inner t => findAllInfo t (inner.mergeIntoOuter? context?) pred
   | .node i children  =>
-      (if pred i then [(i, context?, children)] else []) ++ children.toList.bind (fun t => findAllInfo t context? pred)
+      (if pred i then [(i, context?, children)] else []) ++
+        children.toList.flatMap (fun t => findAllInfo t context? pred)
   | _ => []
 
 /-- Return all `TacticInfo` nodes in an `InfoTree` corresponding to tactics,
@@ -155,10 +156,10 @@ def collectTactics (t : Elab.InfoTree) : List TacticInvocation :=
 
 @[export pantograph_frontend_collect_tactics_from_compilation_step_m]
 def collectTacticsFromCompilationStep (step : CompilationStep) : IO (List Protocol.InvokedTactic) := do
-  let tacticInfoTrees := step.trees.bind λ tree => tree.filter λ
+  let tacticInfoTrees := step.trees.flatMap λ tree => tree.filter λ
     | info@(.ofTacticInfo _) => info.isOriginal
     | _ => false
-  let tactics := tacticInfoTrees.bind collectTactics
+  let tactics := tacticInfoTrees.flatMap collectTactics
   tactics.mapM λ invocation => do
     let goalBefore := (Format.joinSep (← invocation.goalState) "\n").pretty
     let goalAfter := (Format.joinSep (← invocation.goalStateAfter) "\n").pretty
@@ -191,7 +192,7 @@ private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
 -- NOTE: Plural deliberately not spelled "sorries"
 @[export pantograph_frontend_collect_sorrys_m]
 def collectSorrys (step: CompilationStep) : List InfoWithContext :=
-  step.trees.bind collectSorrysInTree
+  step.trees.flatMap collectSorrysInTree
 
 
 
@@ -211,7 +212,7 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
     | .ofTacticInfo tacticInfo => do
       MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
     | _ => panic! "Invalid info"
-  let goals := List.join (← goalsM.run {} |>.run' {})
+  let goals := List.flatten (← goalsM.run {} |>.run' {})
   let root := match goals with
     | [] => panic! "No MVars generated"
     | [g] => g

Test/Integration.lean

@@ -73,7 +73,7 @@ def test_tactic : Test :=
     step "goal.tactic" [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
      ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult),
     step "goal.print" [("stateId", .num 1)]
-     ({ parent? := .some { pp? := .some "fun x => ?m.12 x" }, }: Protocol.GoalPrintResult),
+     ({ parent? := .some { pp? := .some "fun x => ?m.11" }, }: Protocol.GoalPrintResult),
     step "goal.tactic" [("stateId", .num 1), ("goalId", .num 0), ("tactic", .str "intro y")]
      ({ nextStateId? := .some 2, goals? := #[goal2], }: Protocol.GoalTacticResult),
   ]

Test/Proofs.lean

@@ -564,10 +564,10 @@ def test_nat_zero_add: TestM Unit := do
       return ()
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
-      buildNamedGoal "_uniq.68" [("n", "Nat")] "Nat",
+      buildNamedGoal "_uniq.72" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "exact n"
@@ -650,13 +650,13 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let major := "_uniq.68"
+  let major := "_uniq.72"
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.67" [("n", "Nat")] "Nat → Prop" (.some "motive"),
+      buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat → Prop" (.some "motive"),
       buildNamedGoal major [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.69" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
+      buildNamedGoal "_uniq.73" [("n", "Nat")] "∀ (t : Nat), Nat.below t → ?motive t",
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "?motive ?m.68 = (n + 0 = n)" (.some "conduit")
+      buildNamedGoal "_uniq.74" [("n", "Nat")] "?motive ?m.72 = (n + 0 = n)" (.some "conduit")
     ])
 
   let tactic := "intro x"
@@ -673,7 +673,7 @@ def test_nat_zero_add_alt: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let (eqL, eqR, eqT) := ("_uniq.88", "_uniq.89", "_uniq.87")
+  let (eqL, eqR, eqT) := ("_uniq.92", "_uniq.93", "_uniq.91")
   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
@@ -684,16 +684,16 @@ def test_nat_zero_add_alt: TestM Unit := do
 
   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"
+  let fvN := "_uniq.67"
   let conduitRight := s!"((:c Eq) (:c Nat) ({cNatAdd} (:fv {fvN}) {cNat0}) (:fv {fvN}))"
   let substOf (mv: String) := s!"(:subst (:mv {mv}) (:fv {fvN}) (:mv {major}))"
   addTest $ LSpec.check "resume" ((← state2b.serializeGoals (options := { ← read with printExprAST := true })) =
     #[
       {
-        name := "_uniq.70",
+        name := "_uniq.74",
         userName? := .some "conduit",
         target := {
-          pp? := .some "(?m.92 ?m.68 = ?m.94 ?m.68) = (n + 0 = n)",
+          pp? := .some "(?m.96 ?m.72 = ?m.98 ?m.72) = (n + 0 = n)",
           sexp? := .some s!"((:c Eq) (:sort 0) ((:c Eq) {substOf eqT} {substOf eqL} {substOf eqR}) {conduitRight})",
         },
         vars := #[{

Test/Tactic/MotivatedApply.lean

@@ -40,7 +40,7 @@ def test_nat_brec_on : TestT Elab.TermElabM Unit := do
         "Nat → Prop",
         "Nat",
         "∀ (t : Nat), Nat.below t → ?motive t",
-        "?motive ?m.67 = (n + 0 = n)",
+        "?motive ?m.71 = (n + 0 = n)",
       ])
     addTest test
 
@@ -83,7 +83,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
     let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
     let tactic := Tactic.evalMotivatedApply recursor
     let newGoals ← runTacticOnMVar tactic target.mvarId!
-    let majorId := 67
+    let majorId := 71
     addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
       [
         "Nat → Prop",
@@ -100,7 +100,7 @@ def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
 
     addTest $ ← conduit.withContext do
       let t := toString (← Meta.ppExpr $ ← conduit.getType)
-      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
+      return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.146 ?m.{majorId}) = (n + 0 = n)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.14.0