Pantograph/Goal.lean

@@ -4,7 +4,6 @@ Functions for handling metavariables
 All the functions starting with `try` resume their inner monadic state.
 -/
 import Pantograph.Protocol
-import Pantograph.Tactic
 import Lean
 
 def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
@@ -145,6 +144,24 @@ protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): O
 
 --- Tactic execution functions ---
 
+/-- Inner function for executing tactic on goal state -/
+def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) :
+    Elab.TermElabM (Except (Array String) Elab.Tactic.SavedState):= do
+  let tacticM (stx: Syntax):  Elab.Tactic.TacticM (Except (Array String) Elab.Tactic.SavedState) := do
+    state.restore
+    Elab.Tactic.setGoals [goal]
+    try
+      Elab.Tactic.evalTactic stx
+      if (← getThe Core.State).messages.hasErrors then
+        let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
+        let errors ← (messages.map Message.data).mapM fun md => md.toString
+        return .error errors
+      else
+        return .ok (← MonadBacktrack.saveState)
+    catch exception =>
+      return .error #[← exception.toMessageData.toString]
+  tacticM tactic { elaborator := .anonymous } |>.run' state.tactic
+
 /-- Response for executing a tactic -/
 inductive TacticResult where
   -- Goes to next state
@@ -158,35 +175,14 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+/-- Execute tactic on given state -/
-          Elab.TermElabM TacticResult := do
+protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
+    Elab.TermElabM TacticResult := do
   state.restoreElabM
   let goal ← match state.savedState.tactic.goals.get? goalId with
     | .some goal => pure $ goal
     | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.execute
+  goal.checkNotAssigned `GoalState.tryTactic
-  try
-    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
-    if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.getErrorMessages |>.toList.toArray
-      let errors ← (messages.map Message.data).mapM fun md => md.toString
-      return .failure errors
-    let nextElabState ← MonadBacktrack.saveState
-    let nextMCtx := nextElabState.meta.meta.mctx
-    let prevMCtx := state.mctx
-    return .success {
-      state with
-      savedState := { term := nextElabState, tactic := newGoals },
-      newMVars := newMVarSet prevMCtx nextMCtx,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none,
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
-/-- Execute tactic on given state -/
-protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
-    Elab.TermElabM TacticResult := do
   let tactic ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := if state.isConv then `conv else `tactic)
@@ -194,7 +190,22 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
     (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.execute goalId $ Elab.Tactic.evalTactic tactic
+  match ← executeTactic (state := state.savedState) (goal := goal) (tactic := tactic) with
+  | .error errors =>
+    return .failure errors
+  | .ok nextSavedState =>
+    -- Assert that the definition of metavariables are the same
+    let nextMCtx := nextSavedState.term.meta.meta.mctx
+    let prevMCtx := state.mctx
+    -- Generate a list of mvarIds that exist in the parent state; Also test the
+    -- assertion that the types have not changed on any mvars.
+    return .success {
+      state with
+      savedState := nextSavedState
+      newMVars := newMVarSet prevMCtx nextMCtx,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none,
+    }
 
 /-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
 protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
@@ -221,7 +232,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
     -- Generate a list of mvarIds that exist in the parent state; Also test the
     -- assertion that the types have not changed on any mvars.
     let newMVars := newMVarSet prevMCtx nextMCtx
-    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
+    let nextGoals ← newMVars.toList.filterM (λ mvar => do pure !(← mvar.isAssigned))
     return .success {
       root := state.root,
       savedState := {
@@ -504,6 +515,19 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
+def getForallArgsBody: Expr → List Expr × Expr
+  | .forallE _ d b _ =>
+    let (innerArgs, innerBody) := getForallArgsBody b
+    (d :: innerArgs, innerBody)
+  | e => ([], e)
+def collectMotiveArguments (forallBody: Expr): SSet Nat :=
+  -- Get all de Bruijn indices
+  Id.run $ do
+    Expr.foldlM (λ acc subexpr => do
+      match subexpr with
+      | .app (.bvar i) _ => return acc.insert i
+      | _ => return acc
+      ) SSet.empty forallBody
 
 protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
       Elab.TermElabM TacticResult := do
@@ -520,6 +544,46 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+  try
+    -- Implemented similarly to the intro tactic
+    let nextGoals: List MVarId ← goal.withContext do
+      let recursor ← Elab.Term.elabTerm (stx := recursor) .none
+      let recursorType ← Meta.inferType recursor
+
+      let (forallArgs, forallBody) := getForallArgsBody recursorType
+      let motiveIndices := collectMotiveArguments forallBody
+
+      let numArgs ← Meta.getExpectedNumArgs recursorType
+
+      let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
+        if i ≥ numArgs then
+          return prev
+        else
+          let argType := forallArgs.get! i
+          -- If `argType` has motive references, its goal needs to be placed in it
+          let argType := argType.instantiateRev prev
+          -- Create the goal
+          let argGoal ← Meta.mkFreshExprMVar argType .natural .anonymous
+          let prev :=  prev ++ [argGoal]
+          go (i + 1) prev
+        termination_by numArgs - i
+      let newMVars ← go 0 #[]
+
+      -- Create the main goal for the return type of the recursor
+      goal.assign (mkAppN recursor newMVars)
+
+      pure $ newMVars.toList.map (·.mvarId!)
+    return .success {
+      root := state.root,
+      savedState := {
+        term := ← MonadBacktrack.saveState,
+        tactic := { goals := nextGoals }
+      },
+      newMVars := nextGoals.toSSet,
+      parentMVar? := .some goal,
+      calcPrevRhs? := .none
+    }
+  catch exception =>
+    return .failure #[← exception.toMessageData.toString]
 
 end Pantograph

Pantograph/Library.lean

@@ -38,7 +38,7 @@ namespace Pantograph
 
 def defaultTermElabMContext: Lean.Elab.Term.Context := {
     autoBoundImplicit := true,
-    declName? := .some `_pantograph,
+    declName? := some "_pantograph".toName,
     errToSorry := false
   }
 def runMetaM { α } (metaM: Lean.MetaM α): Lean.CoreM α :=

Pantograph/Tactic.lean

@@ -1,2 +0,0 @@
-
-import Pantograph.Tactic.MotivatedApply

Pantograph/Tactic/MotivatedApply.lean

@@ -1,59 +0,0 @@
-import Lean
-
-open Lean
-
-namespace Pantograph.Tactic
-
-def getForallArgsBody: Expr → List Expr × Expr
-  | .forallE _ d b _ =>
-    let (innerArgs, innerBody) := getForallArgsBody b
-    (d :: innerArgs, innerBody)
-  | e => ([], e)
-def collectMotiveArguments (forallBody: Expr): SSet Nat :=
-  match forallBody with
-  | .app (.bvar i) _ => SSet.empty.insert i
-  | _ => SSet.empty
-
-def motivatedApply: Elab.Tactic.Tactic := λ stx => do
-  let goal ← Elab.Tactic.getMainGoal
-  let nextGoals: List MVarId ← goal.withContext do
-    let recursor ← Elab.Term.elabTerm (stx := stx) .none
-    let recursorType ← Meta.inferType recursor
-
-    let (forallArgs, forallBody) := getForallArgsBody recursorType
-    let motiveIndices := collectMotiveArguments forallBody
-    --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
-
-    let numArgs ← Meta.getExpectedNumArgs recursorType
-
-    let rec go (i: Nat) (prev: Array Expr): MetaM (Array Expr) := do
-      if i ≥ numArgs then
-        return prev
-      else
-        let argType := forallArgs.get! i
-        -- If `argType` has motive references, its goal needs to be placed in it
-        let argType := argType.instantiateRev prev
-        -- Create the goal
-        let userName := if motiveIndices.contains (numArgs - i - 1) then `motive else .anonymous
-        let argGoal ← Meta.mkFreshExprMVar argType .syntheticOpaque (userName := userName)
-        IO.println s!"Creating [{i}] {← Meta.ppExpr argGoal}"
-        let prev :=  prev ++ [argGoal]
-        go (i + 1) prev
-      termination_by numArgs - i
-    let newMVars ← go 0 #[]
-
-    -- FIXME: Add an `Eq` target and swap out the motive type
-
-    --let sourceType := forallBody.instantiateRev newMVars
-    --unless ← withTheReader Meta.Context (λ ctx => { ctx with config := { ctx.config with } }) $
-    --       Meta.isDefEq sourceType (← goal.getType) do
-    --  throwError "invalid mapply: The resultant type {← Meta.ppExpr sourceType} cannot be unified with {← Meta.ppExpr $ ← goal.getType}"
-
-    -- Create the main goal for the return type of the recursor
-    goal.assign (mkAppN recursor newMVars)
-
-    let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
-    pure nextGoals
-  Elab.Tactic.setGoals nextGoals
-
-end Pantograph.Tactic

Test/Proofs.lean

@@ -49,11 +49,9 @@ def startProof (start: Start): TestM (Option GoalState) := do
         let goal ← GoalState.create (expr := expr)
         return Option.some goal
 
-def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String): Protocol.Goal :=
-    (userName?: Option String := .none): Protocol.Goal :=
   {
     name,
-    userName?,
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
       userName := x.fst,
@@ -61,8 +59,7 @@ def buildNamedGoal (name: String) (nameType: List (String × String)) (target: S
       isInaccessible? := .some false
     })).toArray
   }
-def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal :=
-    Protocol.Goal :=
   {
     userName?,
     target := { pp? := .some target},
@@ -661,9 +658,9 @@ def test_nat_zero_add: TestM Unit := do
       return ()
   addTest $ LSpec.check s!"mapply {recursor}" ((← state2.serializeGoals (options := ← read)).map (·.devolatilizeVars) =
     #[
-      buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"),
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66",
       buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t"
+      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t"
     ])
 
   let tactic := "exact n"