-
Notifications
You must be signed in to change notification settings - Fork 3
/
Lean4Lean.lean
48 lines (40 loc) · 1.58 KB
/
Lean4Lean.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
import Lean4Lean.Environment
/-
open Lean Elab Command
namespace CollectPartial
structure State where
visited : NameSet := {}
opaques : Array (List Expr) := #[]
abbrev M := ReaderT Environment $ StateT State MetaM
partial def collect (stack : List Expr) (c : Name) : M Unit := do
let collectExpr (e : Expr) : M Unit := e.getUsedConstants.forM (collect (mkConst c::stack))
let s ← get
unless s.visited.contains c do
modify fun s => { s with visited := s.visited.insert c }
let env ← read
match env.find? c with
| some (ConstantInfo.ctorInfo _)
| some (ConstantInfo.recInfo _)
| some (ConstantInfo.inductInfo _)
| some (ConstantInfo.quotInfo _) =>
pure ()
| some (ConstantInfo.defnInfo v)
| some (ConstantInfo.thmInfo v) =>
unless ← Meta.isProp v.type do collectExpr v.value
| some (ConstantInfo.axiomInfo v)
| some (ConstantInfo.opaqueInfo v) =>
unless ← Meta.isProp v.type do
modify fun s => { s with opaques := s.opaques.push (mkConst c:: stack) }
| none =>
modify fun s => { s with opaques := s.opaques.push (mkConst c:: stack) }
end CollectPartial
elab "#print" "partial" name:ident : command => do
let constName ← resolveGlobalConstNoOverloadWithInfo name
let env ← getEnv
let (_, s) ← liftTermElabM <| ((CollectPartial.collect [] constName).run env).run {}
if s.opaques.isEmpty then
logInfo m!"'{constName}' does not use any partial definitions"
else
logInfo m!"'{constName}' depends on opaques: {s.opaques.toList}"
#print partial Environment.addDecl'
-/