From 66c6e12be113e354e9b3e294ca480e0025e9a248 Mon Sep 17 00:00:00 2001
From: utkn <utkns09@gmail.com>
Date: Thu, 5 Dec 2024 19:14:11 +0300
Subject: [PATCH] apply_impl and try_impls tactics

---
 Lampe/Lampe.lean                        |  6 ++--
 Lampe/Lampe/Basic.lean                  |  1 +
 Lampe/Lampe/Tactic/SeparationLogic.lean | 15 ----------
 Lampe/Lampe/Tactic/Traits.lean          | 38 +++++++++++++++++++++++++
 4 files changed, 42 insertions(+), 18 deletions(-)
 create mode 100644 Lampe/Lampe/Tactic/Traits.lean

diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
index 44492b2..b4e9ca8 100644
--- 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
index 98c0364..0fbd714 100644
--- 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
index f9c3978..51fd11d 100644
--- 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
new file mode 100644
index 0000000..2736746
--- /dev/null
+++ 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