aesop? now works for unfinished proofs

closes #118

Aesop/Script.lean

@@ -71,12 +71,9 @@ def TacticState.applyTacticInvocation (tacticState : TacticState)
 
 namespace TacticInvocation
 
-def noop (preGoal : MVarId) (postGoal : GoalWithMVars)
-    (preState postState : Meta.SavedState) : TacticInvocation := {
-  tacticSeq := #[]
-  postGoals := #[postGoal]
-  preGoal, preState, postState
-}
+instance : ToMessageData TacticInvocation where
+  toMessageData ti :=
+    m!"{ti.preGoal.name} → {ti.postGoals.map (·.goal.name)}:{indentD $ tacticsToMessageData ti.tacticSeq}"
 
 def render (acc : Array Syntax.Tactic) (ti : TacticInvocation)
     (tacticState : TacticState) : m (Array Syntax.Tactic × TacticState) := do
@@ -133,10 +130,12 @@ inductive StructuredScript
   | empty
   | onGoal (goalPos : Nat) (ti : TacticInvocation) (tail : StructuredScript)
   | focusAndSolve (goalPos : Nat) (here tail : StructuredScript)
+  | sorryN (n : Nat)
   deriving Inhabited
 
-def StructuredScript.render (script : StructuredScript) :
-    m (Array Syntax.Tactic) := do
+namespace StructuredScript
+
+def render (script : StructuredScript) : m (Array Syntax.Tactic) := do
   go #[] script
   where
     go (acc : Array Syntax.Tactic) :
@@ -154,32 +153,52 @@ def StructuredScript.render (script : StructuredScript) :
             let posLit := mkOneBasedNumLit goalPos
             `(tactic| on_goal $posLit:num => { $nestedScript:tactic* })
         go (acc.push t) tail
+      | sorryN n => do
+        let sorryStx ← `(tactic| sorry)
+        let mut acc := acc
+        for _ in [:n] do
+          acc := acc.push sorryStx
+        return acc
+
+end StructuredScript
 
+variable [MonadRecDepth m] [MonadOptions m] [MonadTrace m] [AddMessageContext m]
+  [MonadLiftT BaseIO m] [MonadLiftT IO m] [MonadAlwaysExcept Exception m] in
 partial def UnstructuredScript.toStructuredScriptStatic
     (tacticState : TacticState) (script : UnstructuredScript) :
-    m StructuredScript := do
-  let mut steps : HashMap MVarId (Nat × TacticInvocation) := {}
+    m StructuredScript :=
+  withConstAesopTraceNode .debug (return m!"statically structuring the tactic script") do
+  aesop_trace[debug] "unstructured script:{indentD $ MessageData.joinSep (script.toList.map λ ti => m!"{ti}") "\n"}"
+  let mut steps : HashMap MVarId (Nat × TacticInvocation) :=
+    mkHashMap script.size
   for h : i in [:script.size] do
     let step := script[i]'h.2
+    if h : step.postGoals.size = 1 then
+      if step.postGoals[0].goal == step.preGoal then
+        continue
     steps := steps.insert step.preGoal (i, step)
   (·.fst) <$> go steps tacticState
 where
   go (steps : HashMap MVarId (Nat × TacticInvocation))
-      (tacticState : TacticState) : m (StructuredScript × TacticState) := do
-    if tacticState.hasNoVisibleGoals then
+      (tacticState : TacticState) : m (StructuredScript × TacticState) :=
+    withIncRecDepth do
+    if tacticState.visibleGoals.isEmpty then
       return (.empty, tacticState)
-    else if tacticState.hasSingleVisibleGoal ||
+    else if tacticState.visibleGoals.size == 1 ||
             tacticState.visibleGoalsHaveMVars then
       -- "Unstructured mode"
       -- TODO If the original order happens to solve the main goal, we can
       -- structure opportunistically.
       let firstStep? :=
         findFirstStep? tacticState.visibleGoals (steps.find? ·.goal) (·.fst)
-      let some (goalPos, _, _, firstStep) := firstStep?
-        | throwError "internal error: found no step to solve any visible goal"
-      let tacticState ← tacticState.applyTacticInvocation firstStep
-      let (tailScript, tacticState) ← go steps tacticState
-      return (.onGoal goalPos firstStep tailScript, tacticState)
+      if let some (goalPos, _, _, firstStep) := firstStep? then
+        let tacticState ← tacticState.applyTacticInvocation firstStep
+        let (tailScript, tacticState) ← go steps tacticState
+        return (.onGoal goalPos firstStep tailScript, tacticState)
+      else
+        let numVisibleGoals := tacticState.visibleGoals.size
+        let tacticState := tacticState.solveVisibleGoals
+        return (.sorryN numVisibleGoals, tacticState)
     else
       -- "Structured mode"
       let mut tacticState := tacticState
@@ -283,7 +302,7 @@ partial def UnstructuredScript.toStructuredScriptDynamic
     (preState : Meta.SavedState) (preGoal : MVarId)
     (script : UnstructuredScript) : MetaM (Option StructuredScript) :=
   withAesopTraceNode .debug (λ r => return m!"{ExceptToEmoji.toEmoji r} structuring generated tactic script") do
-    aesop_trace[debug] "unstructured script:{indentD $ toMessageData $ tacticsToTacticSeq $ script.concatMap (·.tacticSeq)}"
+    aesop_trace[debug] "unstructured script:{indentD $ tacticsToMessageData $ script.concatMap (·.tacticSeq)}"
     let (some result) ← go preState #[preGoal] |>.run script
       | return none
     return some result.script
@@ -309,7 +328,7 @@ where
         if preGoals.size = 1 then
           let (some (_, ti)) := (← read).steps[preGoal]
             | throwError "found no step for goal {preGoal.name}:{indentD $ ← preState.runMetaM' do addMessageContext $ toMessageData preGoal}"
-          aesop_trace[debug] "running tactics:{indentD $ toMessageData $ tacticsToTacticSeq ti.tacticSeq}"
+          aesop_trace[debug] "running tactics:{indentD $ tacticsToMessageData ti.tacticSeq}"
           withConstAesopTraceNode .debug (return m!"expected post goals:") do
             aesop_trace[debug] ← goalsToMessageData ti.postState $ ti.postGoals.map (·.goal)
           let (postState, postGoals) ←
@@ -363,7 +382,7 @@ where
       let firstStep? := findFirstStep? preGoals (steps[·]) (·.fst)
       let some (goalPos, goal, _, ti) := firstStep?
         | throwError "found no step for any of the visible goals{indentD $ ← goalsToMessageData preState preGoals}"
-      aesop_trace[debug] "running tactics on goal {goalPos}:{indentD $ toMessageData $ tacticsToTacticSeq ti.tacticSeq}"
+      aesop_trace[debug] "running tactics on goal {goalPos}:{indentD $ tacticsToMessageData ti.tacticSeq}"
       withConstAesopTraceNode .debug (return m!"expected post goals:") do
         aesop_trace[debug] ← goalsToMessageData ti.postState $ ti.postGoals.map (·.goal)
       let (postState, postGoals) ←
@@ -394,8 +413,4 @@ where
           (goals.map λ g => m!"?{g.name}:{indentD $ toMessageData g}").toList
           "\n"
 
-  tacticsToTacticSeq (ts : Array Syntax.Tactic) :
-      TSyntax ``Lean.Parser.Tactic.tacticSeq :=
-    Unhygienic.run do `(Lean.Parser.Tactic.tacticSeq| $ts:tactic*)
-
 end Aesop

Aesop/Script/TacticState.lean

@@ -50,15 +50,12 @@ def getVisibleGoalIndex (ts : TacticState) (goal : MVarId) : m Nat := do
 def getMainGoal? (ts : TacticState) : Option MVarId :=
   ts.visibleGoals[0]?.map (·.goal)
 
-def hasNoVisibleGoals (ts : TacticState) : Bool :=
-  ts.visibleGoals.isEmpty
-
-def hasSingleVisibleGoal (ts : TacticState) : Bool :=
-  ts.visibleGoals.size == 1
-
 def visibleGoalsHaveMVars (ts : TacticState) : Bool :=
   ts.visibleGoals.any λ g => ! g.mvars.isEmpty
 
+def solveVisibleGoals (ts : TacticState) : TacticState :=
+  { ts with visibleGoals := #[] }
+
 private def replaceWithArray [BEq α] (xs : Array α) (x : α) (r : Array α) :
     Option (Array α) := Id.run do
   let mut found := false

Aesop/Search/Main.lean

@@ -124,13 +124,14 @@ def finalizeProof : SearchM Q Unit := do
       aesop_trace[proof] "Final proof:{indentExpr proof}"
 
 open Lean.Elab.Tactic in
-def checkRenderedScript (script : Array Syntax.Tactic) : SearchM Q Unit := do
+def checkRenderedScript (completeProof : Bool) (script : Array Syntax.Tactic) :
+    SearchM Q Unit := do
   let initialState ← getRootMetaState
   let rootGoal ← getRootMVarId
   let go : TacticM Unit := do
     setGoals [rootGoal]
     evalTactic $ ← `(tacticSeq| $script:tactic*)
-    unless (← getUnsolvedGoals).isEmpty do
+    if completeProof && ! (← getUnsolvedGoals).isEmpty then
       throwError "script executed successfully but did not solve the main goal"
   try
     show MetaM Unit from withoutModifyingState do
@@ -154,34 +155,39 @@ register_option aesop.dev.dynamicStructuring : Bool := {
   defValue := false
 }
 
-def structureScript (uscript : UnstructuredScript) (rootState : Meta.SavedState)
-    (rootGoal : MVarId) : SearchM Q (Option StructuredScript) := do
-  if aesop.dev.dynamicStructuring.get (← getOptions) then
+def structureScript (completeProof : Bool) (uscript : UnstructuredScript)
+    (rootState : Meta.SavedState) (rootGoal : MVarId) :
+    SearchM Q (Option StructuredScript) := do
+  let dynamicStructuring := aesop.dev.dynamicStructuring.get (← getOptions)
+  if dynamicStructuring && completeProof then
     uscript.toStructuredScriptDynamic rootState rootGoal
   else
+    if dynamicStructuring then
+      logWarning "aesop: falling back to static structuring for incomplete proof"
     let rootGoalMVars ← rootState.runMetaM' rootGoal.getMVarDependencies
     let tacticState := {
       visibleGoals := #[⟨rootGoal, rootGoalMVars⟩]
       invisibleGoals := ∅
     }
     uscript.toStructuredScriptStatic tacticState
 
-def traceScript : SearchM Q Unit := do
+def traceScript (completeProof : Bool) : SearchM Q Unit := do
   let options := (← read).options
   if ! options.generateScript then
     return
-  let uscript ← (← getRootMVarCluster).extractScript
+  let uscript ← if completeProof then extractScript else extractSafePrefixScript
   checkScriptSteps uscript
   let rootGoal ← getRootMVarId
   let rootState ← getRootMetaState
-  let structuredScript? ← structureScript uscript rootState rootGoal
+  let structuredScript? ←
+    structureScript completeProof uscript rootState rootGoal
   if let some structuredScript := structuredScript? then
     let script ← structuredScript.render
     if options.traceScript then
       let script ← `(tacticSeq| $script*)
       addTryThisTacticSeqSuggestion (← getRef) script
     if ← Check.script.isEnabled then
-      checkRenderedScript script
+      checkRenderedScript completeProof script
   else
     let rootGoalMVars ← rootState.runMetaM' rootGoal.getMVarDependencies
     let tacticState :=
@@ -201,7 +207,7 @@ def finishIfProven : SearchM Q Bool := do
   unless (← (← getRootMVarCluster).get).state.isProven do
     return false
   finalizeProof
-  traceScript
+  traceScript (completeProof := true)
   traceTree
   return true
 
@@ -288,6 +294,7 @@ def handleNonfatalError (err : MessageData) : SearchM Q (Array MVarId) := do
         aesop_trace![proof] "{proof}"
     | none => aesop_trace![proof] "<no proof>"
   traceTree
+  traceScript (completeProof := false)
   let opts := (← read).options
   if opts.terminal then
     throwAesopEx (← getRootMVarId) safeGoals safeExpansionSuccess err

Aesop/Tree/ExtractScript.lean

@@ -15,6 +15,36 @@ namespace Aesop
 
 abbrev ExtractScriptM := StateRefT UnstructuredScript TreeM
 
+def visitGoal (g : Goal) : ExtractScriptM (Option (MVarId × Meta.SavedState)) := do
+  match g.normalizationState with
+  | .notNormal => throwError "expected goal {g.id} to be normalised"
+  | .provenByNormalization _ normScript? =>
+    go g.id normScript?
+    return none
+  | .normal postGoal postState normScript? =>
+    go g.id normScript?
+    return some (postGoal, postState)
+where
+  go (gid : GoalId) : Except DisplayRuleName UnstructuredScript →
+      ExtractScriptM Unit
+    | .ok script => do
+      modify (· ++ script)
+    | .error rule => throwError "normalization rule {rule} (at goal {gid}) does not support tactic script generation"
+
+def visitRapp (r : Rapp) (preGoal : MVarId) (preState : Meta.SavedState) :
+    ExtractScriptM Unit := do
+  let postState := r.metaState
+  let (some scriptBuilder) := r.scriptBuilder?
+    | throwError "rule {r.appliedRule.name} (at rapp {r.id}) does not support tactic script generation"
+  let tacticSeq ←
+    try
+      postState.runMetaM' scriptBuilder.unstructured.run
+    catch e =>
+      throwError "script builder for rapp {r.id} reported error:{indentD $ e.toMessageData}"
+  let postGoals ← postState.runMetaM' do
+    r.originalSubgoals.mapM λ g => return ⟨g, ← g.getMVarDependencies⟩
+  modify λ s => s.push { postState, tacticSeq, preGoal, postGoals, preState }
+
 mutual
   partial def MVarClusterRef.extractScriptCore (cref : MVarClusterRef) :
       ExtractScriptM Unit := do
@@ -25,42 +55,46 @@ mutual
 
   partial def GoalRef.extractScriptCore (gref : GoalRef) : ExtractScriptM Unit := do
     let g ← gref.get
-    match g.normalizationState with
-    | .notNormal => throwError "expected goal {g.id} to be normalised"
-    | .provenByNormalization _ normScript? =>
-      modify (· ++ (← getNormScript g.id normScript?))
-    | .normal postGoal postState normScript? =>
-      modify (· ++ (← getNormScript g.id normScript?))
+    if let some (postNormGoal, postNormState) ← visitGoal g then
       let (some rref) ← g.firstProvenRapp? | throwError
         m!"goal {g.id} does not have a proven rapp"
-      rref.extractScriptCore postGoal postState
-    where
-      @[inline, always_inline]
-      getNormScript (gid : GoalId) :
-          Except DisplayRuleName UnstructuredScript → ExtractScriptM UnstructuredScript
-        | .ok script => pure script
-        | .error rule => throwError "normalization rule {rule} (at goal {gid}) does not support tactic script generation"
+      rref.extractScriptCore postNormGoal postNormState
 
   partial def RappRef.extractScriptCore (rref : RappRef) (preGoal : MVarId)
       (preState : Meta.SavedState) : ExtractScriptM Unit := do
     let r ← rref.get
-    let postState := r.metaState
-    let (some scriptBuilder) := r.scriptBuilder?
-      | throwError "rule {r.appliedRule.name} (at rapp {r.id}) does not support tactic script generation"
-    let tacticSeq ←
-      try
-        postState.runMetaM' scriptBuilder.unstructured.run
-      catch e =>
-        throwError "script builder for rapp {r.id} reported error:{indentD $ e.toMessageData}"
-    let postGoals ← postState.runMetaM' do
-      r.originalSubgoals.mapM λ g => return ⟨g, ← g.getMVarDependencies⟩
-    modify λ s => s.push { postState, tacticSeq, preGoal, postGoals, preState }
+    visitRapp r preGoal preState
     r.children.forM (·.extractScriptCore)
 end
 
 @[inline]
-def MVarClusterRef.extractScript (cref : MVarClusterRef) :
-    TreeM UnstructuredScript :=
-  (·.snd) <$> cref.extractScriptCore.run #[]
+def extractScript : TreeM UnstructuredScript := do
+  (·.snd) <$> (← getRootGoal).extractScriptCore.run #[]
+
+mutual
+  partial def MVarClusterRef.extractSafePrefixScriptCore
+      (mref : MVarClusterRef) : ExtractScriptM Unit := do
+    (← mref.get).goals.forM (·.extractSafePrefixScriptCore)
+
+  partial def GoalRef.extractSafePrefixScriptCore (gref : GoalRef) :
+      ExtractScriptM Unit := do
+    let g ← gref.get
+    if let some (postNormGoal, postNormState) ← visitGoal g then
+      let safeRapps ← g.safeRapps
+      if safeRapps.size > 1 then
+        throwError "aesop: internal error: goal {g.id} has {safeRapps.size} safe rapps"
+      if let some rref := safeRapps[0]? then
+        rref.extractSafePrefixScriptCore postNormGoal postNormState
+
+  partial def RappRef.extractSafePrefixScriptCore (rref : RappRef)
+      (preGoal : MVarId) (preState : Meta.SavedState) :
+      ExtractScriptM Unit := do
+    let r ← rref.get
+    visitRapp r preGoal preState
+    r.forSubgoalsM (·.extractSafePrefixScriptCore)
+end
+
+def extractSafePrefixScript : TreeM UnstructuredScript := do
+  (·.snd) <$> (← getRootGoal).extractSafePrefixScriptCore.run #[]
 
 end Aesop

Aesop/Util/Basic.lean

@@ -424,4 +424,7 @@ register_option aesop.smallErrorMessages : Bool := {
     descr := "(aesop) Print smaller error messages. Used for testing."
   }
 
+def tacticsToMessageData (ts : Array Syntax.Tactic) : MessageData :=
+  MessageData.joinSep (ts.map toMessageData |>.toList) "\n"
+
 end Aesop

AesopTest/EraseUnfold.lean

@@ -36,7 +36,7 @@ error: tactic 'aesop' failed, failed to prove the goal after exhaustive search.
 -/
 #guard_msgs in
 example : foo = 37 := by
-  aesop? (config := { terminal := true })
+  aesop (config := { terminal := true })
 
 example : foo = 37 := by
   unfold foo