-
Notifications
You must be signed in to change notification settings - Fork 26
/
ElabM.lean
63 lines (45 loc) · 1.67 KB
/
ElabM.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
51
52
53
54
55
56
57
58
59
60
61
62
63
/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Lean
open Lean Lean.Meta Lean.Elab
namespace Aesop.ElabM
structure Context where
parsePriorities : Bool
goal : MVarId
namespace Context
def forAdditionalRules (goal : MVarId) : Context where
parsePriorities := true
goal := goal
-- HACK: Some of the elaboration functions require that we pass in the current
-- goal. The goal is used exclusively to look up fvars in the lctx, so when
-- we operate outside a goal, we pass in a dummy mvar with empty lctx.
def forAdditionalGlobalRules : MetaM Context := do
let mvarId := (← mkFreshExprMVarAt {} {} (.const ``True [])).mvarId!
return .forAdditionalRules mvarId
def forErasing (goal : MVarId) : Context where
parsePriorities := false
goal := goal
-- HACK: See `forAdditionalGlobalRules`
def forGlobalErasing : MetaM Context := do
let mvarId := (← mkFreshExprMVarAt {} {} (.const ``True [])).mvarId!
return .forErasing mvarId
end ElabM.Context
abbrev ElabM := ReaderT ElabM.Context $ TermElabM
-- Generate specialized pure/bind implementations so we don't need to optimise
-- them on the fly at each use site.
instance : Monad ElabM :=
{ inferInstanceAs (Monad ElabM) with }
protected def ElabM.run (ctx : Context) (x : ElabM α) : TermElabM α := do
ReaderT.run x ctx
def shouldParsePriorities : ElabM Bool :=
return (← read).parsePriorities
def getGoal : ElabM MVarId :=
return (← read).goal
def getRuleName : Expr → MetaM Name
| .const decl _ => return decl
| .fvar fvarId => return (← fvarId.getDecl).userName
| _ => mkFreshId
end Aesop