Add New Rule Builder: Tactic Generator

Aesop/Builder/Tactic.lean

@@ -21,8 +21,11 @@ def RuleBuilder.tactic (opts : RegularBuilderOptions) : RuleBuilder :=
       mkResult $ .singleRuleTac decl
     else if ← isDefEq (mkConst ``RuleTac) type then
       mkResult $ .ruleTac decl
+    else if ← isDefEq (← mkArrow (mkConst ``MVarId) (mkApp (mkConst ``MetaM) (← mkAppM ``Array #[(← mkAppM ``Prod #[(mkConst ``String), (mkConst ``Float)])]))) type then
+      -- MVarId → MetaM (Array (String × Float))
+      mkResult $ .tacGen decl
     else
-      throwError "aesop: {decl} was expected to be a tactic, i.e. to have one of these types:\n  TacticM Unit\n  SimpleRuleTac\n  RuleTac\nHowever, it has type{indentExpr type}"
+      throwError "aesop: {decl} was expected to be a tactic, i.e. to have one of these types:\n  TacticM Unit\n  SimpleRuleTac\n  RuleTac\n  MVarId → MetaM (Array (String × Float))\nHowever, it has type{indentExpr type}"
   where
     builderName : BuilderName :=
       .tactic

Aesop/RuleTac.lean

@@ -28,6 +28,7 @@ protected def run : RuleTacDescr → RuleTacInput → MetaM RuleTacOutput
   | tacticM decl => RuleTac.tacticM decl
   | singleRuleTac decl => RuleTac.singleRuleTac decl
   | ruleTac decl => RuleTac.ruleTac decl
+  | tacGen decl => RuleTac.tacGen decl
   | preprocess => RuleTac.preprocess
 
 end RuleTacDescr

Aesop/RuleTac/Basic.lean

@@ -49,6 +49,7 @@ structure RuleApplication where
   goals : Array MVarId
   postState : Meta.SavedState
   scriptBuilder? : Option RuleTacScriptBuilder
+  probabilityModifier : Float := 1.0
 
 namespace RuleApplication
 
@@ -114,6 +115,7 @@ inductive RuleTacDescr
       (isRecursiveType : Bool)
   | tacticM (decl : Name)
   | ruleTac (decl : Name)
+  | tacGen (decl : Name)
   | singleRuleTac (decl : Name)
   | preprocess
   deriving Inhabited
@@ -129,6 +131,7 @@ def isGlobal : RuleTacDescr → Bool
   | cases .. => true
   | tacticM .. => true
   | ruleTac .. => true
+  | tacGen .. => true
   | singleRuleTac .. => true
   | preprocess => true
 

Aesop/RuleTac/RuleApplicationWithMVarInfo.lean

@@ -38,6 +38,7 @@ structure RuleApplicationWithMVarInfo where
   mvars : UnorderedArraySet MVarId
   introducedMVars : UnorderedArraySet MVarId
   assignedMVars : UnorderedArraySet MVarId
+  probabilityModifier : Float
   scriptBuilder? : Option (ScriptBuilder MetaM)
 
 namespace RuleApplicationWithMVarInfo

Aesop/RuleTac/Tactic.lean

@@ -8,7 +8,7 @@ import Aesop.RuleTac.Basic
 
 open Lean
 open Lean.Meta
-open Lean.Elab.Tactic (TacticM run)
+open Lean.Elab.Tactic (TacticM evalTactic run)
 
 namespace Aesop.RuleTac
 
@@ -42,4 +42,47 @@ unsafe def singleRuleTacImpl (decl : Name) : RuleTac :=
 @[implemented_by singleRuleTacImpl]
 opaque singleRuleTac (decl : Name) : RuleTac
 
+-- Precondition: `decl` has type `MVarId → MetaM (Array (String × Float))`.
+unsafe def tacGenImpl (decl : Name) : RuleTac := λ input => do
+  let tac ← evalConst (MVarId → MetaM (Array (String × Float))) decl
+  let initialState ← saveState
+  let suggestions ← tac input.goal
+  let apps ← suggestions.filterMapM fun (tacticStr, score) => do
+    assert! 0 ≤ score ∧ score ≤ 1   
+    match Parser.runParserCategory (← getEnv) `tactic tacticStr (fileName := "<stdin>") with
+    | .error _ => return none
+    | .ok stx =>
+      try 
+        initialState.restore
+        let tac := commitIfNoEx $ evalTactic stx
+        -- let tstx : TSyntax `tactic := {raw := stx}
+        let goals ← run input.goal tac |>.run'
+        let pf? ← getExprMVarAssignment? input.goal
+        if pf?.isSome then
+          if (← instantiateMVars pf?.get!) |>.hasSorry then 
+            initialState.restore
+            return none
+        -- let scriptBuilder? :=
+        --   mkScriptBuilder? generateScript $
+        --     .ofTactic goals.toArray.size do
+        --       withAllTransparencySyntax md tstx
+        let postState ← saveState
+        let thisApp : RuleApplication := {
+          postState := postState
+          goals := goals.toArray
+          probabilityModifier := score
+          -- scriptBuilder? := scriptBuilder?
+          scriptBuilder? := none
+        }
+        return thisApp
+      catch _ => pure none
+  restoreState initialState
+  if apps.isEmpty then throwError
+    "failed to apply any tactics generated"
+  return ⟨apps⟩
+
+-- Precondition: `decl` has type `MVarId → MetaM (Array (String × Float))`.
+@[implemented_by tacGenImpl]
+opaque tacGen (decl : Name) : RuleTac
+
 end Aesop.RuleTac

Aesop/Search/Expansion.lean

@@ -64,12 +64,14 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule)
     (rapps : Array RuleApplicationWithMVarInfo) :
     SearchM Q RuleResult := do
   let parent ← parentRef.get
-  let successProbability := parent.successProbability * rule.successProbability
 
   let mut rrefs := Array.mkEmpty rapps.size
   let mut subgoals := Array.mkEmpty $ rapps.size * 3
   for h : i in [:rapps.size] do
     let rapp := rapps[i]'(by simp_all [Membership.mem])
+    let some probabilityModifier := Percent.ofFloat rapp.probabilityModifier | throwError 
+      "aesop: internal error: rule {rule.name} returned an invalid probability modifier {rapp.probabilityModifier}"
+    let successProbability := parent.successProbability * rule.successProbability * probabilityModifier
     let rref ← addRapp {
       rapp with
       parent := parentRef

AesopTest/TacGen.lean

@@ -0,0 +1,21 @@
+import Aesop
+
+open Lean
+open Lean.Meta
+
+theorem foo (a b c : Nat) : a + b + c = c + b + a := by
+  rw [Nat.add_assoc]
+  rw [Nat.add_comm]
+  rw [Nat.add_comm b]
+
+-- @[aesop unsafe 50% tactic]
+-- def x (_ : MVarId) : MetaM (Array (String × Float)) := do
+--  return #[("apply foo", 1.0)]
+
+-- It wouldn't work without this.
+@[aesop unsafe 80% tactic]
+def x : MVarId → MetaM (Array (String × Float)) := fun _ => do
+  return #[("rw [Nat.add_comm b]", 0.5), ("rw [Nat.add_assoc]", 0.9), ("rw [Nat.add_comm]", 0.8)]
+
+example (a b c : Nat) : a + b + c = c + b + a := by
+  aesop

README.md

@@ -943,4 +943,4 @@ usually perfectly safe rule `∀ n, n < n + 1` would, if treated as safe, force
 to commit to one particular instantiation of the metavariable `?m`.
 
 For more details on the handling of metavariables, see the [Aesop
-paper](https://zenodo.org/record/7430233).
+paper](https://zenodo.org/record/7430233).