Fall back to simp without only if simp only script step is broken

Under certain conditions, `simp?` seems to be necessarily broken. This
affects our script generation, which uses the underlying mechanism of
`simp?` to generate `simp only` script steps. We therefore now use the
original `simp` script step if the `simp only` one is broken.

Aesop/Script/SpecificTactics.lean

@@ -139,20 +139,61 @@ where
   mkPat (fvarId : FVarId) : MetaM (TSyntax `rintroPat) := do
     `(rintroPat| $(mkIdent $ ← fvarId.getUserName):ident)
 
-def simpAllOrSimpAtStarOnly (simpAll : Bool) (inGoal : MVarId)
+private def simpAllOrSimpAtStarStx [Monad m] [MonadQuotation m] (simpAll : Bool)
+    (configStx? : Option Term) : m (Syntax.Tactic) :=
+  if simpAll then
+    match configStx? with
+    | none => `(tactic| simp_all)
+    | some cfg => `(tactic| simp_all (config := $cfg))
+  else
+    match configStx? with
+    | none => `(tactic| simp at *)
+    | some cfg => `(tactic| simp (config := $cfg) at *)
+
+private def simpAllOrSimpAtStarOnlyStx (simpAll : Bool) (inGoal : MVarId)
     (configStx? : Option Term) (usedTheorems : Simp.UsedSimps) :
-    TacticBuilder := do
-  let originalStx ←
-    if simpAll then
-      match configStx? with
-      | none => `(tactic| simp_all)
-      | some cfg => `(tactic| simp_all (config := $cfg))
-    else
-      match configStx? with
-      | none => `(tactic| simp at *)
-      | some cfg => `(tactic| simp (config := $cfg) at *)
+    MetaM Syntax.Tactic := do
+  let originalStx ← simpAllOrSimpAtStarStx simpAll configStx?
   let stx ← inGoal.withContext do
     Elab.Tactic.mkSimpOnly originalStx usedTheorems
+  return ⟨stx⟩
+
+def simpAllOrSimpAtStarOnly (simpAll : Bool) (inGoal : MVarId)
+    (configStx? : Option Term) (usedTheorems : Simp.UsedSimps) :
+    TacticBuilder :=
+  .unstructured <$>
+    simpAllOrSimpAtStarOnlyStx simpAll inGoal configStx? usedTheorems
+
+private def isGlobalSimpTheorem (thms : SimpTheorems) (simprocs : Simprocs) : Origin → Bool
+  | origin@(.decl decl) =>
+    simprocs.simprocNames.contains decl ||
+    thms.lemmaNames.contains origin ||
+    thms.toUnfold.contains decl ||
+    thms.toUnfoldThms.contains decl
+  | _ => false
+
+def simpAllOrSimpAtStar (simpAll : Bool) (inGoal : MVarId)
+    (configStx? : Option Term) (usedTheorems : Simp.UsedSimps) :
+    TacticBuilder := do
+  let simpTheorems ← getSimpTheorems
+  let simprocs ← Simp.getSimprocs
+  let (map, size) ←
+    usedTheorems.map.foldlM (init := ({}, 0)) λ (map, size) origin thm => do
+      if isGlobalSimpTheorem simpTheorems simprocs origin then
+        return (map, size)
+      else
+        return (map.insert origin thm, size + 1)
+  let stx ←
+    match ← simpAllOrSimpAtStarOnlyStx simpAll inGoal configStx? { map, size } with
+    | `(tactic| simp_all $[$cfg:config]? only [$lems,*]) =>
+      `(tactic| simp_all $[$cfg]? [$lems,*])
+    | `(tactic| simp $[$cfg:config]? only [$lems,*] at *) =>
+      `(tactic| simp $[$cfg]? [$lems,*] at *)
+    | `(tactic| simp_all $[$cfg:config]? only) =>
+      `(tactic| simp_all $[$cfg]?)
+    | `(tactic| simp $[$cfg:config]? only at *) =>
+      `(tactic| simp $[$cfg]? at *)
+    | stx => throwError "simp tactic builder: unexpected syntax:{indentD stx}"
   return .unstructured ⟨stx⟩
 
 def intros (postGoal : MVarId) (newFVarIds : Array FVarId)

Aesop/Search/Expansion/Norm.lean

@@ -122,12 +122,21 @@ def mkNormSimpScriptStep
     (preState postState : Meta.SavedState) (usedTheorems : Simp.UsedSimps) :
     NormM Script.LazyStep := do
   let ctx := (← read).normSimpContext
-  let tacticBuilder :=
+  let simpBuilder :=
+    TacticBuilder.simpAllOrSimpAtStar (simpAll := ctx.useHyps) preGoal
+      ctx.configStx? usedTheorems
+  let simpOnlyBuilder :=
     TacticBuilder.simpAllOrSimpAtStarOnly (simpAll := ctx.useHyps) preGoal
       ctx.configStx? usedTheorems
+  let tacticBuilders :=
+    if (← read).options.useDefaultSimpSet then
+      #[simpOnlyBuilder, simpBuilder]
+    else
+      #[simpOnlyBuilder]
   return {
     postGoals := postGoal?.toArray
-    tacticBuilders := #[tacticBuilder]
+    tacticBuilders
+    tacticBuilders_ne := by simp only [tacticBuilders]; split <;> simp
     preGoal, preState, postState
   }