-
Notifications
You must be signed in to change notification settings - Fork 26
/
Util.lean
50 lines (44 loc) · 1.59 KB
/
Util.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
/-
Copyright (c) 2024 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop.RuleTac.Forward.Basic
import Aesop.Util.Basic
import Aesop.Util.EqualUpToIds
open Lean Lean.Meta
namespace Aesop.Script
-- Without {α β : Type} universe inference goes haywire.
@[specialize]
def findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β)
(stepOrder : β → Nat) : Option (Nat × α × β) := Id.run do
let mut firstStep? := none
for h : pos in [:goals.size] do
let g := goals[pos]'h.2
if let some step := step? g then
if let some (_, _, currentFirstStep) := firstStep? then
if stepOrder step < stepOrder currentFirstStep then
firstStep? := some (pos, g, step)
else
firstStep? := some (pos, g, step)
else
continue
return firstStep?
def matchGoals (postState₁ postState₂ : Meta.SavedState)
(goals₁ goals₂ : Array MVarId) : MetaM (Option (HashMap MVarId MVarId)) := do
let goals₁ ← getProperGoals postState₁ goals₁
let goals₂ ← getProperGoals postState₂ goals₂
let (equal, s) ←
tacticStatesEqualUpToIds' none postState₁.meta.mctx
postState₂.meta.mctx goals₁ goals₂ (allowAssignmentDiff := true)
if ! equal then
return none
else
return s.equalMVarIds
where
getProperGoals (state : Meta.SavedState) (goals : Array MVarId) :
MetaM (Array MVarId) :=
state.runMetaM' do
let (properGoals, _) ← partitionGoalsAndMVars goals
return properGoals.map (·.fst)
end Aesop.Script