Pantograph/Goal.lean

@@ -232,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 (λ mvar => do pure !(← mvar.isAssigned))
+    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
     return .success {
       root := state.root,
       savedState := {
@@ -521,13 +521,9 @@ def getForallArgsBody: Expr → List Expr × Expr
     (d :: innerArgs, innerBody)
   | e => ([], e)
 def collectMotiveArguments (forallBody: Expr): SSet Nat :=
-  -- Get all de Bruijn indices
+  match forallBody with
-  Id.run $ do
+  | .app (.bvar i) _ => SSet.empty.insert i
-    Expr.foldlM (λ acc subexpr => do
+  | _ => SSet.empty
-      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
@@ -552,6 +548,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
 
       let (forallArgs, forallBody) := getForallArgsBody recursorType
       let motiveIndices := collectMotiveArguments forallBody
+      --IO.println s!"{motiveIndices.toList} from {← Meta.ppExpr forallBody}"
 
       let numArgs ← Meta.getExpectedNumArgs recursorType
 
@@ -563,16 +560,26 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
           -- 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 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)
 
-      pure $ newMVars.toList.map (·.mvarId!)
+      let nextGoals ← newMVars.toList.map (·.mvarId!) |>.filterM (not <$> ·.isAssigned)
+      pure nextGoals
     return .success {
       root := state.root,
       savedState := {

Pantograph/Library.lean

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

Test/Proofs.lean

@@ -49,9 +49,11 @@ 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): Protocol.Goal :=
+def buildNamedGoal (name: String) (nameType: List (String × String)) (target: String)
+    (userName?: Option String := .none): Protocol.Goal :=
   {
     name,
+    userName?,
     target := { pp? := .some target},
     vars := (nameType.map fun x => ({
       userName := x.fst,
@@ -59,7 +61,8 @@ 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): Protocol.Goal :=
+def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none):
+    Protocol.Goal :=
   {
     userName?,
     target := { pp? := .some target},
@@ -658,9 +661,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",
+      buildNamedGoal "_uniq.70" [("n", "Nat")] "Nat → Sort ?u.66" (.some "motive"),
       buildNamedGoal "_uniq.71" [("n", "Nat")] "Nat",
-      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?m.70 t"
+      buildNamedGoal "_uniq.72" [("n", "Nat")] "(t : Nat) → Nat.below t → ?motive t"
     ])
 
   let tactic := "exact n"