Test/Common.lean

@@ -89,10 +89,12 @@ def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSe
   runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
   termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
+def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
+  runMetaMSeq env $ termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
 
 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
 
-def parseSentence (s: String): MetaM Expr := do
+def parseSentence (s: String): Elab.TermElabM Expr := do
   let recursor ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -100,7 +102,7 @@ def parseSentence (s: String): MetaM Expr := do
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  runTermElabMInMeta $ Elab.Term.elabTerm (stx := recursor) .none
+  Elab.Term.elabTerm (stx := recursor) .none
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
@@ -110,6 +112,36 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do
   let t ← exprToStr (← mvarId.getType)
   return (name, t)
 
+
+-- Monadic testing
+
+abbrev TestT := StateT LSpec.TestSeq
+
+def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do
+  set $ (← get) ++ test
+
+def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq :=
+  Prod.snd <$> t.run LSpec.TestSeq.done
+
+def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
+  IO LSpec.TestSeq :=
+  runTermElabMSeq env $ runTest t
+
+def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl :=
+  { userName, type }
+
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+    Protocol.Goal :=
+  {
+    userName?,
+    target := { pp? := .some target},
+    vars := (nameType.map fun x => ({
+      userName := x.fst,
+      type? := .some { pp? := .some x.snd },
+      isInaccessible? := .some false
+    })).toArray
+  }
+
 end Test
 
 end Pantograph

Test/Proofs.lean

@@ -357,69 +357,6 @@ def test_or_comm: TestM Unit := do
       ]
     }
 
-def test_have: TestM Unit := do
-  let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
-  let state0 ← match state? with
-    | .some state => pure state
-    | .none => do
-      addTest $ assertUnreachable "Goal could not parse"
-      return ()
-  let tactic := "intro p q h"
-  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
-
-  let expr := "Or.inl (Or.inl h)"
-  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let haveBind := "y"
-  let haveType := "p ∨ q"
-  let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
-      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
-    ])
-
-  let expr := "Or.inl h"
-  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state2b ← match state3.continue state2 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ assertUnreachable e
-      return ()
-  let expr := "Or.inl y"
-  let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
-
 example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
   intro a b c1 c2 h
   conv =>
@@ -856,7 +793,6 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Nat.add_comm delta", test_delta_variable),
     ("arithmetic", test_arith),
     ("Or.comm", test_or_comm),
-    ("have", test_have),
     ("conv", test_conv),
     ("calc", test_calc),
     ("let via assign", test_let false),

Test/Tactic/Congruence.lean

@@ -7,103 +7,82 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.Congruence
 
-def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
+def test_congr_arg_list : TestT Elab.TermElabM Unit := do
   let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let mut tests := LSpec.TestSeq.done
+    let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      let (newGoals, test) ← runTermElabMInMeta do
+      [
-        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+        (`α, "Sort ?u.30"),
-        let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+        (`a₁, "?α"),
-          [
+        (`a₂, "?α"),
-            (`α, "Sort ?u.30"),
+        (`f, "?α → List α"),
-            (`a₁, "?α"),
+        (`h, "?a₁ = ?a₂"),
-            (`a₂, "?α"),
+        (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
-            (`f, "?α → List α"),
+      ])
-            (`h, "?a₁ = ?a₂"),
+    let f := newGoals.get! 3
-            (`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
+    let h := newGoals.get! 4
-          ])
+    let c := newGoals.get! 5
-        return (newGoals, test)
+    let results ← f.apply (← parseSentence "List.reverse")
-      tests := tests ++ test
+    addTest $ LSpec.check "apply" (results.length = 0)
-      let f := newGoals.get! 3
+    addTest $ LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂")
-      let h := newGoals.get! 4
+    addTest $ LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)")
-      let c := newGoals.get! 5
+def test_congr_arg : TestT Elab.TermElabM Unit := do
-      let results ← f.apply (← parseSentence "List.reverse")
-      tests := tests ++ (LSpec.check "apply" (results.length = 0))
-      tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
-      tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
-      return tests
-def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let mut tests := LSpec.TestSeq.done
+    let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      let test ← runTermElabMInMeta do
+      [
-        let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
+        (`α, "Sort ?u.70"),
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+        (`a₁, "?α"),
-          [
+        (`a₂, "?α"),
-            (`α, "Sort ?u.70"),
+        (`f, "?α → Nat"),
-            (`a₁, "?α"),
+        (`h, "?a₁ = ?a₂"),
-            (`a₂, "?α"),
+        (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
-            (`f, "?α → Nat"),
+      ])
-            (`h, "?a₁ = ?a₂"),
+def test_congr_fun : TestT Elab.TermElabM Unit := do
-            (`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
-          ])
-      tests := tests ++ test
-      return tests
-def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let mut tests := LSpec.TestSeq.done
+    let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      let test ← runTermElabMInMeta do
+      [
-        let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
+        (`α, "Sort ?u.159"),
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+        (`f₁, "?α → Nat"),
-          [
+        (`f₂, "?α → Nat"),
-            (`α, "Sort ?u.159"),
+        (`h, "?f₁ = ?f₂"),
-            (`f₁, "?α → Nat"),
+        (`a, "?α"),
-            (`f₂, "?α → Nat"),
+        (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
-            (`h, "?f₁ = ?f₂"),
+      ])
-            (`a, "?α"),
+def test_congr : TestT Elab.TermElabM Unit := do
-            (`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
-          ])
-      tests := tests ++ test
-      return tests
-def test_congr (env: Environment): IO LSpec.TestSeq :=
   let expr := "λ (a b: Nat) => a = b"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let mut tests := LSpec.TestSeq.done
+    let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    addTest $  LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
-      let test ← runTermElabMInMeta do
+      [
-        let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
+        (`α, "Sort ?u.10"),
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
+        (`f₁, "?α → Nat"),
-          [
+        (`f₂, "?α → Nat"),
-            (`α, "Sort ?u.10"),
+        (`a₁, "?α"),
-            (`f₁, "?α → Nat"),
+        (`a₂, "?α"),
-            (`f₂, "?α → Nat"),
+        (`h₁, "?f₁ = ?f₂"),
-            (`a₁, "?α"),
+        (`h₂, "?a₁ = ?a₂"),
-            (`a₂, "?α"),
+        (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
-            (`h₁, "?f₁ = ?f₂"),
+      ])
-            (`h₂, "?a₁ = ?a₂"),
-            (`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
-          ])
-      tests := tests ++ test
-      return tests
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("congrArg List.reverse", test_congr_arg_list env),
+    ("congrArg List.reverse", test_congr_arg_list),
-    ("congrArg", test_congr_arg env),
+    ("congrArg", test_congr_arg),
-    ("congrFun", test_congr_fun env),
+    ("congrFun", test_congr_fun),
-    ("congr", test_congr env),
+    ("congr", test_congr),
-  ]
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.Congruence

Test/Tactic/MotivatedApply.lean

@@ -7,82 +7,23 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.MotivatedApply
 
-def test_type_extract (env: Environment): IO LSpec.TestSeq :=
+def test_type_extract : TestT Elab.TermElabM Unit := do
-  runMetaMSeq env do
+  let recursor ← parseSentence "@Nat.brecOn"
-    let mut tests := LSpec.TestSeq.done
+  let recursorType ← Meta.inferType recursor
-    let recursor ← parseSentence "@Nat.brecOn"
+  addTest $ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
-    let recursorType ← Meta.inferType recursor
+    (← exprToStr recursorType))
-    tests := tests ++ LSpec.check "recursorType" ("{motive : Nat → Sort ?u.1} → (t : Nat) → ((t : Nat) → Nat.below t → motive t) → motive t" =
+  let info ← match Tactic.getRecursorInformation recursorType with
-      (← exprToStr recursorType))
+    | .some info => pure info
-    let info ← match Tactic.getRecursorInformation recursorType with
+    | .none => throwError "Failed to extract recursor info"
-      | .some info => pure info
+  addTest $ LSpec.check "iMotive" (info.iMotive = 2)
-      | .none => throwError "Failed to extract recursor info"
+  let motiveType := info.getMotiveType
-    tests := tests ++ LSpec.check "iMotive" (info.iMotive = 2)
+  addTest $ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
-    let motiveType := info.getMotiveType
+    (← exprToStr motiveType))
-    tests := tests ++ LSpec.check "motiveType" ("Nat → Sort ?u.1" =
-      (← exprToStr motiveType))
-    return tests
 
-def test_nat_brec_on (env: Environment): IO LSpec.TestSeq :=
+def test_nat_brec_on : TestT Elab.TermElabM Unit := do
   let expr := "λ (n t: Nat) => n + 0 = n"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => 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 mut tests := LSpec.TestSeq.done
-      -- Apply the tactic
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.motivatedApply recursor
-      let test ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-          [
-            "Nat → Prop",
-            "Nat",
-            "∀ (t : Nat), Nat.below t → ?motive t",
-            "?motive ?m.67 = (n + 0 = n)",
-          ])
-      tests := tests ++ test
-      return tests
-
-def test_list_brec_on (env: Environment): IO LSpec.TestSeq :=
-  let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
-  runMetaMSeq env do
-    let expr ← parseSentence expr
-    Meta.lambdaTelescope expr $ λ _ body => do
-      let recursor ← match Parser.runParserCategory
-        (env := ← MonadEnv.getEnv)
-        (catName := `term)
-        (input := "@List.brecOn")
-        (fileName := filename) with
-        | .ok syn => pure syn
-        | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
-      -- Apply the tactic
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let tactic := Tactic.motivatedApply recursor
-      let test ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-          [
-            "Type ?u.90",
-            "List ?m.92 → Prop",
-            "List ?m.92",
-            "∀ (t : List ?m.92), List.below t → ?motive t",
-            "?motive ?m.94 = (l ++ [] = [] ++ l)",
-          ])
-      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)
@@ -90,41 +31,83 @@ def test_partial_motive_instantiation (env: Environment): IO LSpec.TestSeq := do
       (fileName := filename) with
       | .ok syn => pure syn
       | .error error => throwError "Failed to parse: {error}"
-    let expr ← parseSentence expr
+    -- Apply the tactic
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      let mut tests := LSpec.TestSeq.done
+    let tactic := Tactic.motivatedApply recursor
-      -- Apply the tactic
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let test :=  LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-      let tactic := Tactic.motivatedApply recursor
+      [
-      let newGoals ← runTacticOnMVar tactic target.mvarId!
+        "Nat → Prop",
-      let majorId := 67
+        "Nat",
-      tests := tests ++ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+        "∀ (t : Nat), Nat.below t → ?motive t",
-        [
+        "?motive ?m.67 = (n + 0 = n)",
-          "Nat → Prop",
+      ])
-          "Nat",
+    addTest test
-          "∀ (t : Nat), Nat.below t → ?motive t",
-          s!"?motive ?m.{majorId} = (n + 0 = n)",
-        ]))
-      let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
-      tests := tests ++ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
 
-      -- Assign motive to `λ x => x + _`
+def test_list_brec_on : TestT Elab.TermElabM Unit := do
-      let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
+  let expr := "λ {α : Type} (l: List α) => l ++ [] = [] ++ l"
-      motive.assign motive_assign
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "@List.brecOn")
+      (fileName := filename) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.motivatedApply recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+      [
+        "Type ?u.90",
+        "List ?m.92 → Prop",
+        "List ?m.92",
+        "∀ (t : List ?m.92), List.below t → ?motive t",
+        "?motive ?m.94 = (l ++ [] = [] ++ l)",
+      ])
 
-      let test ← conduit.withContext do
+def test_partial_motive_instantiation : TestT Elab.TermElabM Unit := do
-        let t := toString (← Meta.ppExpr $ ← conduit.getType)
+  let expr := "λ (n t: Nat) => n + 0 = n"
-        return LSpec.check "conduit" (t = s!"(?m.{majorId}.add + 0 = ?m.138 ?m.{majorId}) = (n + 0 = n)")
+  let recursor ← match Parser.runParserCategory
-      tests := tests ++ test
+    (env := ← MonadEnv.getEnv)
+    (catName := `term)
+    (input := "@Nat.brecOn")
+    (fileName := filename) with
+    | .ok syn => pure syn
+    | .error error => throwError "Failed to parse: {error}"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.motivatedApply recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    let majorId := 67
+    addTest $ (LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+      [
+        "Nat → Prop",
+        "Nat",
+        "∀ (t : Nat), Nat.below t → ?motive t",
+        s!"?motive ?m.{majorId} = (n + 0 = n)",
+      ]))
+    let [motive, major, step, conduit] := newGoals | panic! "Incorrect goal number"
+    addTest $ (LSpec.check "goal name" (major.name.toString = s!"_uniq.{majorId}"))
 
-      return tests
+    -- Assign motive to `λ x => x + _`
+    let motive_assign ← parseSentence "λ (x: Nat) => @Nat.add x + 0 = _"
+    motive.assign motive_assign
+
+    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)")
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("type_extract", test_type_extract env),
+    ("type_extract", test_type_extract),
-    ("Nat.brecOn", test_nat_brec_on env),
+    ("Nat.brecOn", test_nat_brec_on),
-    ("List.brecOn", test_list_brec_on env),
+    ("List.brecOn", test_list_brec_on),
-    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation env),
+    ("Nat.brecOn partial motive instantiation", test_partial_motive_instantiation),
-  ]
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.MotivatedApply

Test/Tactic/NoConfuse.lean

@@ -7,81 +7,66 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.NoConfuse
 
-def test_nat (env: Environment): IO LSpec.TestSeq :=
+def test_nat : TestT Elab.TermElabM Unit := do
   let expr := "λ (n: Nat) (h: 0 = n + 1) => False"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
-      let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
-        (env := ← MonadEnv.getEnv)
+      (catName := `term)
-        (catName := `term)
+      (input := "h")
-        (input := "h")
+      (fileName := filename) with
-        (fileName := filename) with
+      | .ok syn => pure syn
-        | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
-        | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
-      let mut tests := LSpec.TestSeq.done
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      -- Apply the tactic
+    let tactic := Tactic.noConfuse recursor
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
-      let tactic := Tactic.noConfuse recursor
+    addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
-      let test ← runTermElabMInMeta do
-        let newGoals ← runTacticOnMVar tactic target.mvarId!
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
-          [])
-      tests := tests ++ test
-      return tests
 
-def test_nat_fail (env: Environment): IO LSpec.TestSeq :=
+def test_nat_fail : TestT Elab.TermElabM Unit := do
   let expr := "λ (n: Nat) (h: n = n) => False"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
-    Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
-      let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
-        (env := ← MonadEnv.getEnv)
+      (catName := `term)
-        (catName := `term)
+      (input := "h")
-        (input := "h")
+      (fileName := filename) with
-        (fileName := filename) with
+      | .ok syn => pure syn
-        | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
-        | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
-      let mut tests := LSpec.TestSeq.done
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      -- Apply the tactic
+    try
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      try
-        let tactic := Tactic.noConfuse recursor
-        let _ ← runTermElabMInMeta $ runTacticOnMVar tactic target.mvarId!
-        tests := tests ++ assertUnreachable "Tactic should fail"
-      catch _ =>
-        tests := tests ++ LSpec.check "Tactic should fail" true
-        return tests
-      return tests
-
-def test_list (env: Environment): IO LSpec.TestSeq :=
-  let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
-  runMetaMSeq env do
-    let expr ← parseSentence expr
-    Meta.lambdaTelescope expr $ λ _ body => do
-      let recursor ← match Parser.runParserCategory
-        (env := ← MonadEnv.getEnv)
-        (catName := `term)
-        (input := "h")
-        (fileName := filename) with
-        | .ok syn => pure syn
-        | .error error => throwError "Failed to parse: {error}"
-      let mut tests := LSpec.TestSeq.done
-      -- Apply the tactic
-      let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
       let tactic := Tactic.noConfuse recursor
-      let test ← runTermElabMInMeta do
+      let _ ← runTacticOnMVar tactic target.mvarId!
-        let newGoals ← runTacticOnMVar tactic target.mvarId!
+      addTest $ assertUnreachable "Tactic should fail"
-        pure $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) =
+    catch _ =>
-          [])
+      addTest $ LSpec.check "Tactic should fail" true
-      tests := tests ++ test
+
-      return tests
+def test_list : TestT Elab.TermElabM Unit := do
+  let expr := "λ (l: List Nat) (h: [] = 1 :: l) => False"
+  let expr ← parseSentence expr
+  Meta.lambdaTelescope expr $ λ _ body => do
+    let recursor ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
+      (catName := `term)
+      (input := "h")
+      (fileName := filename) with
+      | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
+    let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
+    let tactic := Tactic.noConfuse recursor
+    let newGoals ← runTacticOnMVar tactic target.mvarId!
+    addTest $ LSpec.check "goals"
+      ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = [])
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("Nat", test_nat env),
+    ("Nat", test_nat),
-    ("Nat fail", test_nat_fail env),
+    ("Nat fail", test_nat_fail),
-    ("List", test_list env),
+    ("List", test_list),
-  ]
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.NoConfuse

Test/Tactic/Prograde.lean

@@ -7,57 +7,113 @@ open Pantograph
 
 namespace Pantograph.Test.Tactic.Prograde
 
-def test_eval (env: Environment): IO LSpec.TestSeq :=
+def test_eval : TestT Elab.TermElabM Unit := do
   let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
-  runMetaMSeq env do
+  let expr ← parseSentence expr
-    let expr ← parseSentence expr
+  Meta.forallTelescope expr $ λ _ body => do
-    Meta.forallTelescope expr $ λ _ body => do
+    let e ← match Parser.runParserCategory
-      let e ← match Parser.runParserCategory
+      (env := ← MonadEnv.getEnv)
-        (env := ← MonadEnv.getEnv)
+      (catName := `term)
-        (catName := `term)
+      (input := "Or.inl h")
-        (input := "Or.inl h")
+      (fileName := filename) with
-        (fileName := filename) with
+      | .ok syn => pure syn
-        | .ok syn => pure syn
+      | .error error => throwError "Failed to parse: {error}"
-        | .error error => throwError "Failed to parse: {error}"
+    -- Apply the tactic
-      let mut tests := LSpec.TestSeq.done
+    let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
-      -- Apply the tactic
+    let target: Expr := mkAnd
-      let goal ← Meta.mkFreshExprSyntheticOpaqueMVar body
+      (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
-      let target: Expr := mkAnd
+      (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
-        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+    let h := .fvar ⟨uniq 8⟩
-        (mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
+    addTest $ LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
-      let h := .fvar ⟨uniq 8⟩
+      context := #[
-      let test := LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
+        cdeclOf `p (.sort 0),
-        context := #[
+        cdeclOf `q (.sort 0),
-          { userName := `p, type := .sort 0 },
+        cdeclOf `h h
-          { userName := `q, type := .sort 0 },
+      ],
-          { userName := `h, type := h}
+      target,
-        ],
+    })
-        target,
+    let tactic := Tactic.evaluate `h2 e
-      })
+    let m := .mvar ⟨uniq 13⟩
-      tests := tests ++ test
+    let [newGoal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
-      let tactic := Tactic.evaluate `h2 e
+    addTest $ LSpec.test "goals after" ((← toCondensedGoal newGoal).devolatilize == {
-      let m := .mvar ⟨uniq 13⟩
+      context := #[
-      let test ← runTermElabMInMeta do
+        cdeclOf `p (.sort 0),
-        let [goal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
+        cdeclOf `q (.sort 0),
-        pure $ LSpec.test "goals after" ((← toCondensedGoal goal).devolatilize == {
+        cdeclOf `h h,
-        context := #[
+        {
-          { userName := `p, type := .sort 0 },
+          userName := `h2,
-          { userName := `q, type := .sort 0 },
+          type := mkOr h m,
-          { userName := `h, type := h},
+          value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
-          {
+        }
-            userName := `h2,
+      ],
-            type := mkOr h m,
+      target,
-            value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
+    })
-          }
+    addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
-        ],
+
-        target,
+def test_have : TestT Elab.TermElabM Unit := do
-      })
+  let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
-      tests := tests ++ test
+  let state0 ← GoalState.create rootExpr
-      return tests
+  let tactic := "intro p q h"
+  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check tactic ((← state1.serializeGoals).map (·.devolatilize) =
+    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])
+
+  let expr := "Or.inl (Or.inl h)"
+  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let haveBind := "y"
+  let haveType := "p ∨ q"
+  let state2 ← match ← state1.tryHave (goalId := 0) (binderName := haveBind) (type := haveType) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!"have {haveBind}: {haveType}" ((← state2.serializeGoals).map (·.devolatilize) =
+    #[
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "p ∨ q",
+      buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p"), ("y", "p ∨ q")] "(p ∨ q) ∨ p ∨ q"
+    ])
+
+  let expr := "Or.inl h"
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state3.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  let state2b ← match state3.continue state2 with
+    | .ok state => pure state
+    | .error e => do
+      addTest $ assertUnreachable e
+      return ()
+  let expr := "Or.inl y"
+  let state4 ← match ← state2b.tryAssign (goalId := 0) (expr := expr) with
+    | .success state => pure state
+    | other => do
+      addTest $ assertUnreachable $ other.toString
+      return ()
+  addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
+    #[])
+
+  addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
+
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("eval", test_eval env),
+    ("eval", test_eval),
-  ]
+    ("have", test_have),
+  ] |>.map (λ (name, t) => (name, runTestTermElabM env t))
 
 end Pantograph.Test.Tactic.Prograde