apply_impl and try_impls tactics

reilabs · Dec 5, 2024 · 66c6e12 · 66c6e12
1 parent 0acd5f8
commit 66c6e12
Show file tree

Hide file tree

Showing 4 changed files with 42 additions and 18 deletions.
diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
@@ -136,7 +136,7 @@ def simpleTraitCall (tp : Tp) (arg : tp.denote P): Expr (Tp.denote P) tp :=
 example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall .field arg) (fun v => v = 2 * arg) := by
   simp only [simpleTraitCall]
   steps
-  resolve_trait [bulbulizeField.2]
+  apply_impl bulbulizeField.2
   tauto
   any_goals rfl
   simp only
@@ -149,7 +149,7 @@ example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall .field arg) (fun v =>
 example : STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCall (.u 32) arg) (fun v => v = 69) := by
   simp only [simpleTraitCall]
   steps
-  resolve_trait [bulbulizeU32.2]
+  apply_impl bulbulizeU32.2
   tauto
   any_goals rfl
   simp only
@@ -165,7 +165,7 @@ example {p} {arg : Tp.denote p Tp.field} :
   STHoare p simpleTraitEnv ⟦⟧ (simpleTraitCallSyntax.fn.body _ h![.field] |>.body h![arg]) (fun v => v = 2 * arg) := by
   simp only [simpleTraitCallSyntax]
   steps
-  resolve_trait [bulbulizeField.2]
+  try_impls [bulbulizeU32.2, bulbulizeField.2]
   tauto
   any_goals rfl
   simp only

diff --git a/Lampe/Lampe/Basic.lean b/Lampe/Lampe/Basic.lean
@@ -5,3 +5,4 @@ import Lampe.Tp
 import Lampe.Hoare.Total
 import Lampe.Hoare.SepTotal
 import Lampe.Tactic.SeparationLogic
+import Lampe.Tactic.Traits
diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -724,21 +724,6 @@ partial def steps (mvar : MVarId) : TacticM (List MVarId) := do
       catch _ => throwTacticEx (`steps) mvar s!"Can't solve"
   | _ => return [mvar]
 
-partial def tryImpls (traitResolutionGoal : MVarId) (allImpls : List $ TSyntax `term) : TacticM (List MVarId) := match allImpls with
-| [] => throwError "no impl works!"
-| impl :: impls =>
-  try evalTacticAt (←`(tactic|apply TraitResolution.ok (impl := $impl) (implGenerics := h![]) (h_mem := by tauto) <;> (first | rfl | tauto))) traitResolutionGoal
-  catch _ => tryImpls traitResolutionGoal impls
-
-partial def resolveTrait (mvar : MVarId) (impls : List $ TSyntax `term) : TacticM (List MVarId) := do
-  let fstGoals ← tryImpls mvar impls
-  return fstGoals
-
-syntax "resolve_trait" "[" term,* "]": tactic
-elab "resolve_trait" "[" impls:term,* "]" : tactic => do
-  let newGoals ← resolveTrait (←getMainGoal) impls.getElems.toList
-  replaceMainGoal newGoals
-
 syntax "steps" : tactic
 elab "steps" : tactic => do
   let newGoals ← steps (← getMainGoal)

diff --git a/Lampe/Lampe/Tactic/Traits.lean b/Lampe/Lampe/Tactic/Traits.lean
@@ -0,0 +1,38 @@
+import Lampe.SeparationLogic.State
+import Lampe.Hoare.SepTotal
+import Lampe.Hoare.Builtins
+import Lampe.Syntax
+
+import Lean.Meta.Tactic.Simp.Main
+
+open Lean Elab.Tactic Parser.Tactic Lean.Meta Qq
+
+partial def applyImpl (goal : MVarId) (impl : TSyntax `term) : TacticM $ List MVarId := do
+  let newGoals ← evalTacticAt (←`(tactic|
+    apply Lampe.TraitResolution.ok (impl := $impl) (implGenerics := h![]) (h_mem := by tauto) <;> (first | rfl | tauto)
+  )) goal
+  pure newGoals
+
+syntax "apply_impl" term : tactic
+elab "apply_impl" impl:term : tactic => do
+  let mainGoal ← getMainGoal
+  let newGoals ← applyImpl mainGoal impl
+  replaceMainGoal newGoals
+
+partial def tryImpls (allImpls : List $ TSyntax `term) : TacticM Unit := do
+  let oldState ← saveState
+  let mainGoal ← getMainGoal
+  match allImpls with
+  | impl :: impls => do
+    let subGoals ← applyImpl mainGoal impl
+    if subGoals.length > 0 then
+      oldState.restore
+      tryImpls impls
+    else
+      replaceMainGoal subGoals
+      return ()
+  | [] => throwError "no impl applies"
+
+syntax "try_impls" "[" term,* "]" : tactic
+elab "try_impls" "[" impls:term,* "]" : tactic => do
+  tryImpls impls.getElems.toList