feat: Prograde tactics #83
|
@ -1,6 +1,7 @@
|
|||
import Pantograph.Goal
|
||||
import Pantograph.Library
|
||||
import Pantograph.Protocol
|
||||
import Pantograph.Condensed
|
||||
import Lean
|
||||
import LSpec
|
||||
|
||||
|
@ -10,12 +11,7 @@ namespace Pantograph
|
|||
|
||||
deriving instance Repr for Expr
|
||||
-- Use strict equality check for expressions
|
||||
--instance : BEq Expr := ⟨Expr.equal⟩
|
||||
instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
|
||||
if h : Expr.equal x y then
|
||||
.isTrue h
|
||||
else
|
||||
.isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
|
||||
instance : BEq Expr := ⟨Expr.equal⟩
|
||||
|
||||
def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
|
||||
|
||||
|
@ -25,6 +21,7 @@ def Goal.devolatilizeVars (goal: Goal): Goal :=
|
|||
{
|
||||
goal with
|
||||
vars := goal.vars.map removeInternalAux,
|
||||
|
||||
}
|
||||
where removeInternalAux (v: Variable): Variable :=
|
||||
{
|
||||
|
@ -47,6 +44,24 @@ deriving instance DecidableEq, Repr for InteractionError
|
|||
deriving instance DecidableEq, Repr for Option
|
||||
end Protocol
|
||||
|
||||
namespace Condensed
|
||||
|
||||
deriving instance BEq, Repr for LocalDecl
|
||||
deriving instance BEq, Repr for Goal
|
||||
|
||||
protected def LocalDecl.devolatilize (decl: LocalDecl): LocalDecl :=
|
||||
{
|
||||
decl with fvarId := { name := .anonymous }
|
||||
}
|
||||
protected def Goal.devolatilize (goal: Goal): Goal :=
|
||||
{
|
||||
goal with
|
||||
mvarId := { name := .anonymous },
|
||||
context := goal.context.map LocalDecl.devolatilize
|
||||
}
|
||||
|
||||
end Condensed
|
||||
|
||||
def TacticResult.toString : TacticResult → String
|
||||
| .success state => s!".success ({state.goals.length} goals)"
|
||||
| .failure messages =>
|
||||
|
|
|
@ -25,12 +25,33 @@ def test_eval (env: Environment): IO LSpec.TestSeq :=
|
|||
let target: Expr := mkAnd
|
||||
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
|
||||
(mkOr (.fvar ⟨uniq 8⟩) (.fvar ⟨uniq 9⟩))
|
||||
let test := LSpec.test "goals before" ((← goal.mvarId!.getType) == target)
|
||||
let h := .fvar ⟨uniq 8⟩
|
||||
let test := LSpec.test "goals before" ((← toCondensedGoal goal.mvarId!).devolatilize == {
|
||||
context := #[
|
||||
{ userName := `p, type := .sort 0 },
|
||||
{ userName := `q, type := .sort 0 },
|
||||
{ userName := `h, type := h}
|
||||
],
|
||||
target,
|
||||
})
|
||||
tests := tests ++ test
|
||||
let tactic := Tactic.evaluate `h2 e
|
||||
let m := .mvar ⟨uniq 13⟩
|
||||
let test ← runTermElabMInMeta do
|
||||
let newGoals ← runTacticOnMVar tactic goal.mvarId!
|
||||
pure $ LSpec.test "goals after" ((← newGoals.head!.getType) == target)
|
||||
let [goal] ← runTacticOnMVar tactic goal.mvarId! | panic! "Incorrect goal number"
|
||||
pure $ LSpec.test "goals after" ((← toCondensedGoal goal).devolatilize == {
|
||||
context := #[
|
||||
{ userName := `p, type := .sort 0 },
|
||||
{ userName := `q, type := .sort 0 },
|
||||
{ userName := `h, type := h},
|
||||
{
|
||||
userName := `h2,
|
||||
type := mkOr h m,
|
||||
value? := .some $ mkApp3 (mkConst `Or.inl) h m (.fvar ⟨uniq 10⟩)
|
||||
}
|
||||
],
|
||||
target,
|
||||
})
|
||||
tests := tests ++ test
|
||||
return tests
|
||||
|
||||
|
|
Loading…
Reference in New Issue