refactor: Cleanup the congruence tactics #81

Merged
aniva merged 4 commits from tactic/congruence into dev 2024-06-23 13:35:36 -07:00
2 changed files with 35 additions and 6 deletions
Showing only changes of commit f80d90ce87 - Show all commits

View File

@ -311,7 +311,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
let pref := if goalState.newMVars.contains mvarId then "~" else " "
printMVar pref mvarId decl
)
pure $ result ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
where
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
let resultFVars: List String ←
@ -337,7 +337,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
else pure $ value
pure s!"\n := {← Meta.ppExpr value}"
else if let .some { mvarIdPending, .. } ← getDelayedMVarAssignment? mvarId then
pure s!"\n := $ {mvarIdPending.name}"
pure s!"\n ::= {mvarIdPending.name}"
else
pure ""
else

View File

@ -7,6 +7,34 @@ open Pantograph
namespace Pantograph.Test.Tactic.Congruence
def test_congr_arg_list (env: Environment): IO LSpec.TestSeq :=
let expr := "λ {α} (l1 l2 : List α) (h: l1 = l2) => l1.reverse = l2.reverse"
runMetaMSeq env do
let expr ← parseSentence expr
Meta.lambdaTelescope expr $ λ _ body => do
let mut tests := LSpec.TestSeq.done
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
let (newGoals, test) ← runTermElabMInMeta do
let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
let test := LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
[
(`α, "Sort ?u.30"),
(`a₁, "?α"),
(`a₂, "?α"),
(`f, "?α → List α"),
(`h, "?a₁ = ?a₂"),
(`conduit, "(?f ?a₁ = ?f ?a₂) = (l1.reverse = l2.reverse)"),
])
return (newGoals, test)
tests := tests ++ test
let f := newGoals.get! 3
let h := newGoals.get! 4
let c := newGoals.get! 5
let results ← f.apply (← parseSentence "List.reverse")
tests := tests ++ (LSpec.check "apply" (results.length = 0))
tests := tests ++ (LSpec.check "h" ((← exprToStr $ ← h.getType) = "?a₁ = ?a₂"))
tests := tests ++ (LSpec.check "conduit" ((← exprToStr $ ← c.getType) = "(?a₁.reverse = ?a₂.reverse) = (l1.reverse = l2.reverse)"))
return tests
def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
runMetaMSeq env do
@ -72,6 +100,7 @@ def test_congr (env: Environment): IO LSpec.TestSeq :=
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
[
("congrArg List.reverse", test_congr_arg_list env),
("congrArg", test_congr_arg env),
("congrFun", test_congr_fun env),
("congr", test_congr env),