-
Notifications
You must be signed in to change notification settings - Fork 27
/
Name.lean
147 lines (112 loc) · 3.29 KB
/
Name.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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop.Util.Basic
open Lean
open Lean.Meta
namespace Aesop
inductive PhaseName
| norm
| safe
| «unsafe»
deriving Inhabited, BEq, Hashable
-- NOTE: Constructors should be listed in alphabetical order for the Ord
-- instance.
namespace PhaseName
instance : Ord PhaseName where
compare s₁ s₂ := compare s₁.toCtorIdx s₂.toCtorIdx
instance : ToString PhaseName where
toString
| norm => "norm"
| safe => "safe"
| «unsafe» => "unsafe"
end PhaseName
inductive ScopeName
| global
| «local»
deriving Inhabited, BEq, Hashable
-- NOTE: Constructors should be listed in alphabetical order for the Ord
-- instance.
namespace ScopeName
instance : Ord ScopeName where
compare s₁ s₂ := compare s₁.toCtorIdx s₂.toCtorIdx
instance : ToString ScopeName where
toString
| global => "global"
| «local» => "local"
end ScopeName
inductive BuilderName
| apply
| cases
| constructors
| destruct
| forward
| simp
| tactic
| unfold
deriving Inhabited, BEq, Hashable
-- NOTE: Constructors should be listed in alphabetical order for the Ord
-- instance.
namespace BuilderName
instance : Ord BuilderName where
compare b₁ b₂ := compare b₁.toCtorIdx b₂.toCtorIdx
instance : ToString BuilderName where
toString
| apply => "apply"
| cases => "cases"
| constructors => "constructors"
| destruct => "destruct"
| forward => "forward"
| simp => "simp"
| tactic => "tactic"
| unfold => "unfold"
end BuilderName
-- Rules are identified by a `RuleName` throughout Aesop. We assume that rule
-- names are unique within our 'universe', i.e. within the rule sets that we are
-- working with. All data structures should enforce this invariant.
structure RuleName where
name : Name
builder : BuilderName
phase : PhaseName
scope : ScopeName
protected hash : UInt64 :=
mixHash (hash name) $ mixHash (hash builder) $ mixHash (hash phase)
(hash scope)
deriving Inhabited
namespace RuleName
instance : Hashable RuleName where
hash n := n.hash
instance : BEq RuleName where
beq n₁ n₂ :=
n₁.hash == n₂.hash && n₁.builder == n₂.builder && n₁.phase == n₂.phase &&
n₁.scope == n₂.scope && n₁.name == n₂.name
protected def compare : (_ _ : RuleName) → Ordering :=
compareLex (compareOn (·.builder)) $
compareLex (compareOn (·.phase)) $
compareLex (compareOn (·.scope)) $
(λ n₁ n₂ => n₁.name.cmp n₂.name)
protected def quickCompare (n₁ n₂ : RuleName) : Ordering :=
match compare n₁.hash n₂.hash with
| Ordering.eq => n₁.compare n₂
| ord => ord
instance : Ord RuleName :=
⟨RuleName.compare⟩
instance : ToString RuleName where
toString n :=
toString n.phase ++ "|" ++ toString n.builder ++ "|" ++ toString n.scope ++
"|" ++ toString n.name
end RuleName
inductive DisplayRuleName
| ruleName (n : RuleName)
| normSimp
| normUnfold
deriving Inhabited, BEq, Ord, Hashable
namespace DisplayRuleName
instance : ToString DisplayRuleName where
toString
| ruleName n => toString n
| normSimp => "<norm simp>"
| normUnfold => "<norm unfold>"
end Aesop.DisplayRuleName