Skip to content

Commit 22859e6

Browse files
mdbrnowskimdbrnowski
authored
Add Lean lexer (#1071)
Resolves #908
1 parent 5409db0 commit 22859e6

File tree

3 files changed

+272
-0
lines changed

3 files changed

+272
-0
lines changed

‎lexers/embedded/lean.xml

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
<lexer>
2+
<config>
3+
<name>Lean4</name>
4+
<alias>lean4</alias>
5+
<alias>lean</alias>
6+
<filename>*.lean</filename>
7+
<mime_type>text/x-lean4</mime_type>
8+
<mime_type>text/x-lean</mime_type>
9+
</config>
10+
<rules>
11+
<state name="expression">
12+
<rule pattern="\s+"><token type="TextWhitespace"/></rule>
13+
<rule pattern="/--"><token type="LiteralStringDoc"/><push state="docstring"/></rule>
14+
<rule pattern="/-"><token type="Comment"/><push state="comment"/></rule>
15+
<rule pattern="--.*$"><token type="CommentSingle"/></rule>
16+
<rule pattern="\b(Type|Prop|Sort)\b"><token type="KeywordType"/></rule>
17+
<rule pattern="\b(sorry|admit)\b"><token type="GenericError"/></rule>
18+
<rule pattern="(!=|\#|\&amp;|\&amp;\&amp;|\*|\+|\-|/|@|!|\-\.|\-&gt;|\.|\.\.|\.\.\.|::|:&gt;|;|;;|&lt;|&lt;\-|=|==|&gt;|_|\||\|\||\~|=&gt;|&lt;=|&gt;=|/\\|\\/|∀|Π|λ|↔|∧|∨|≠|≤|≥|¬|⁻¹|⬝|▸|→|∃|≈|×|⌞|⌟|≡|⟨|⟩|↦)"><token type="NameBuiltinPseudo"/></rule>
19+
<rule pattern="(\(|\)|:|\{|\}|\[|\]|⦃|⦄|:=|,)"><token type="Operator"/></rule>
20+
<rule pattern="(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9&#x27;ⁿ-₉ₐ-ₜᵢ-ᵪ!?])*"><token type="Name"/></rule>
21+
<rule pattern="``?(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9&#x27;ⁿ-₉ₐ-ₜᵢ-ᵪ!?])*(\.(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟](?:(?![λΠΣ])[_a-zA-Zα-ωΑ-Ωϊ-ϻἀ-῾℀-⅏𝒜-𝖟0-9&#x27;ⁿ-₉ₐ-ₜᵢ-ᵪ!?])*)*"><token type="LiteralStringSymbol"/></rule>
22+
<rule pattern="(?&lt;=\.)\d+"><token type="LiteralNumber"/></rule>
23+
<rule pattern="(\d+\.\d*)([eE][+-]?[0-9]+)?"><token type="LiteralNumberFloat"/></rule>
24+
<rule pattern="\d+"><token type="LiteralNumberInteger"/></rule>
25+
<rule pattern="&quot;"><token type="LiteralStringDouble"/><push state="string"/></rule>
26+
<rule pattern="[~?][a-z][\w\&#x27;]*:"><token type="NameVariable"/></rule>
27+
<rule pattern="\S"><token type="NameBuiltinPseudo"/></rule>
28+
</state>
29+
<state name="root">
30+
<rule pattern="\b(import|unif_hint|renaming|inline|hiding|lemma|variable|theorem|axiom|inductive|structure|universe|alias|\#help|precedence|postfix|prefix|infix|infixl|infixr|notation|\#eval|\#check|\#reduce|\#exit|end|private|using|namespace|instance|section|protected|export|set_option|extends|open|example|\#print|opaque|def|macro|elab|syntax|macro_rules|\#reduce|where|abbrev|noncomputable|class|attribute|\#synth|mutual|scoped|local)\b"><token type="KeywordNamespace"/></rule>
31+
<rule pattern="\b(forall|fun|obtain|from|have|show|assume|let|if|else|then|by|in|with|calc|match|nomatch|do|at)\b"><token type="Keyword"/></rule>
32+
<rule pattern="@\["><token type="KeywordDeclaration"/><push state="attribute"/></rule>
33+
<rule><include state="expression"/></rule>
34+
</state>
35+
<state name="attribute">
36+
<rule pattern="\]"><token type="KeywordDeclaration"/><pop depth="1"/></rule>
37+
<rule><include state="expression"/></rule>
38+
</state>
39+
<state name="comment">
40+
<rule pattern="[^/-]+"><token type="CommentMultiline"/></rule>
41+
<rule pattern="/-"><token type="CommentMultiline"/><push/></rule>
42+
<rule pattern="-/"><token type="CommentMultiline"/><pop depth="1"/></rule>
43+
<rule pattern="[/-]"><token type="CommentMultiline"/></rule>
44+
</state>
45+
<state name="docstring">
46+
<rule pattern="[^/-]+"><token type="LiteralStringDoc"/></rule>
47+
<rule pattern="-/"><token type="LiteralStringDoc"/><pop depth="1"/></rule>
48+
<rule pattern="[/-]"><token type="LiteralStringDoc"/></rule>
49+
</state>
50+
<state name="string">
51+
<rule pattern="[^\\&quot;]+"><token type="LiteralStringDouble"/></rule>
52+
<rule pattern="\\[n&quot;\\\n]"><token type="LiteralStringEscape"/></rule>
53+
<rule pattern="&quot;"><token type="LiteralStringDouble"/><pop depth="1"/></rule>
54+
</state>
55+
</rules>
56+
</lexer>

‎lexers/testdata/lean.actual

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
def f(x : Nat) : Nat := x + 1
2+
3+
-- comment
4+
5+
theorem thm (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
6+
intro ⟨hp, hqr⟩
7+
show (p ∧ q) ∨ (p ∧ r)
8+
cases hqr with
9+
| inl hq =>
10+
have hpq : p ∧ q := And.intro hp hq
11+
apply Or.inl
12+
exact hpq
13+
| inr hr =>
14+
have hpr : p ∧ r := And.intro hp hr
15+
apply Or.inr
16+
exact hpr

‎lexers/testdata/lean.expected

Lines changed: 200 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,200 @@
1+
[
2+
{"type":"KeywordNamespace","value":"def"},
3+
{"type":"TextWhitespace","value":" "},
4+
{"type":"Name","value":"f"},
5+
{"type":"Operator","value":"("},
6+
{"type":"Name","value":"x"},
7+
{"type":"TextWhitespace","value":" "},
8+
{"type":"Operator","value":":"},
9+
{"type":"TextWhitespace","value":" "},
10+
{"type":"Name","value":"Nat"},
11+
{"type":"Operator","value":")"},
12+
{"type":"TextWhitespace","value":" "},
13+
{"type":"Operator","value":":"},
14+
{"type":"TextWhitespace","value":" "},
15+
{"type":"Name","value":"Nat"},
16+
{"type":"TextWhitespace","value":" "},
17+
{"type":"Operator","value":":"},
18+
{"type":"NameBuiltinPseudo","value":"="},
19+
{"type":"TextWhitespace","value":" "},
20+
{"type":"Name","value":"x"},
21+
{"type":"TextWhitespace","value":" "},
22+
{"type":"NameBuiltinPseudo","value":"+"},
23+
{"type":"TextWhitespace","value":" "},
24+
{"type":"LiteralNumberInteger","value":"1"},
25+
{"type":"TextWhitespace","value":"\n\n"},
26+
{"type":"CommentSingle","value":"-- comment"},
27+
{"type":"TextWhitespace","value":"\n\n"},
28+
{"type":"KeywordNamespace","value":"theorem"},
29+
{"type":"TextWhitespace","value":" "},
30+
{"type":"Name","value":"thm"},
31+
{"type":"TextWhitespace","value":" "},
32+
{"type":"Operator","value":"("},
33+
{"type":"Name","value":"p"},
34+
{"type":"TextWhitespace","value":" "},
35+
{"type":"Name","value":"q"},
36+
{"type":"TextWhitespace","value":" "},
37+
{"type":"Name","value":"r"},
38+
{"type":"TextWhitespace","value":" "},
39+
{"type":"Operator","value":":"},
40+
{"type":"TextWhitespace","value":" "},
41+
{"type":"KeywordType","value":"Prop"},
42+
{"type":"Operator","value":")"},
43+
{"type":"TextWhitespace","value":" "},
44+
{"type":"Operator","value":":"},
45+
{"type":"TextWhitespace","value":" "},
46+
{"type":"Name","value":"p"},
47+
{"type":"TextWhitespace","value":" "},
48+
{"type":"NameBuiltinPseudo","value":"∧"},
49+
{"type":"TextWhitespace","value":" "},
50+
{"type":"Operator","value":"("},
51+
{"type":"Name","value":"q"},
52+
{"type":"TextWhitespace","value":" "},
53+
{"type":"NameBuiltinPseudo","value":"∨"},
54+
{"type":"TextWhitespace","value":" "},
55+
{"type":"Name","value":"r"},
56+
{"type":"Operator","value":")"},
57+
{"type":"TextWhitespace","value":" "},
58+
{"type":"NameBuiltinPseudo","value":"→"},
59+
{"type":"TextWhitespace","value":" "},
60+
{"type":"Operator","value":"("},
61+
{"type":"Name","value":"p"},
62+
{"type":"TextWhitespace","value":" "},
63+
{"type":"NameBuiltinPseudo","value":"∧"},
64+
{"type":"TextWhitespace","value":" "},
65+
{"type":"Name","value":"q"},
66+
{"type":"Operator","value":")"},
67+
{"type":"TextWhitespace","value":" "},
68+
{"type":"NameBuiltinPseudo","value":"∨"},
69+
{"type":"TextWhitespace","value":" "},
70+
{"type":"Operator","value":"("},
71+
{"type":"Name","value":"p"},
72+
{"type":"TextWhitespace","value":" "},
73+
{"type":"NameBuiltinPseudo","value":"∧"},
74+
{"type":"TextWhitespace","value":" "},
75+
{"type":"Name","value":"r"},
76+
{"type":"Operator","value":")"},
77+
{"type":"TextWhitespace","value":" "},
78+
{"type":"Operator","value":":"},
79+
{"type":"NameBuiltinPseudo","value":"="},
80+
{"type":"TextWhitespace","value":" "},
81+
{"type":"Keyword","value":"by"},
82+
{"type":"TextWhitespace","value":"\n "},
83+
{"type":"Name","value":"intro"},
84+
{"type":"TextWhitespace","value":" "},
85+
{"type":"NameBuiltinPseudo","value":"⟨"},
86+
{"type":"Name","value":"hp"},
87+
{"type":"Operator","value":","},
88+
{"type":"TextWhitespace","value":" "},
89+
{"type":"Name","value":"hqr"},
90+
{"type":"NameBuiltinPseudo","value":"⟩"},
91+
{"type":"TextWhitespace","value":"\n "},
92+
{"type":"Keyword","value":"show"},
93+
{"type":"TextWhitespace","value":" "},
94+
{"type":"Operator","value":"("},
95+
{"type":"Name","value":"p"},
96+
{"type":"TextWhitespace","value":" "},
97+
{"type":"NameBuiltinPseudo","value":"∧"},
98+
{"type":"TextWhitespace","value":" "},
99+
{"type":"Name","value":"q"},
100+
{"type":"Operator","value":")"},
101+
{"type":"TextWhitespace","value":" "},
102+
{"type":"NameBuiltinPseudo","value":"∨"},
103+
{"type":"TextWhitespace","value":" "},
104+
{"type":"Operator","value":"("},
105+
{"type":"Name","value":"p"},
106+
{"type":"TextWhitespace","value":" "},
107+
{"type":"NameBuiltinPseudo","value":"∧"},
108+
{"type":"TextWhitespace","value":" "},
109+
{"type":"Name","value":"r"},
110+
{"type":"Operator","value":")"},
111+
{"type":"TextWhitespace","value":"\n "},
112+
{"type":"Name","value":"cases"},
113+
{"type":"TextWhitespace","value":" "},
114+
{"type":"Name","value":"hqr"},
115+
{"type":"TextWhitespace","value":" "},
116+
{"type":"Keyword","value":"with"},
117+
{"type":"TextWhitespace","value":"\n "},
118+
{"type":"NameBuiltinPseudo","value":"|"},
119+
{"type":"TextWhitespace","value":" "},
120+
{"type":"Name","value":"inl"},
121+
{"type":"TextWhitespace","value":" "},
122+
{"type":"Name","value":"hq"},
123+
{"type":"TextWhitespace","value":" "},
124+
{"type":"NameBuiltinPseudo","value":"=\u003e"},
125+
{"type":"TextWhitespace","value":"\n "},
126+
{"type":"Keyword","value":"have"},
127+
{"type":"TextWhitespace","value":" "},
128+
{"type":"Name","value":"hpq"},
129+
{"type":"TextWhitespace","value":" "},
130+
{"type":"Operator","value":":"},
131+
{"type":"TextWhitespace","value":" "},
132+
{"type":"Name","value":"p"},
133+
{"type":"TextWhitespace","value":" "},
134+
{"type":"NameBuiltinPseudo","value":"∧"},
135+
{"type":"TextWhitespace","value":" "},
136+
{"type":"Name","value":"q"},
137+
{"type":"TextWhitespace","value":" "},
138+
{"type":"Operator","value":":"},
139+
{"type":"NameBuiltinPseudo","value":"="},
140+
{"type":"TextWhitespace","value":" "},
141+
{"type":"Name","value":"And"},
142+
{"type":"NameBuiltinPseudo","value":"."},
143+
{"type":"Name","value":"intro"},
144+
{"type":"TextWhitespace","value":" "},
145+
{"type":"Name","value":"hp"},
146+
{"type":"TextWhitespace","value":" "},
147+
{"type":"Name","value":"hq"},
148+
{"type":"TextWhitespace","value":"\n "},
149+
{"type":"Name","value":"apply"},
150+
{"type":"TextWhitespace","value":" "},
151+
{"type":"Name","value":"Or"},
152+
{"type":"NameBuiltinPseudo","value":"."},
153+
{"type":"Name","value":"inl"},
154+
{"type":"TextWhitespace","value":"\n "},
155+
{"type":"Name","value":"exact"},
156+
{"type":"TextWhitespace","value":" "},
157+
{"type":"Name","value":"hpq"},
158+
{"type":"TextWhitespace","value":"\n "},
159+
{"type":"NameBuiltinPseudo","value":"|"},
160+
{"type":"TextWhitespace","value":" "},
161+
{"type":"Name","value":"inr"},
162+
{"type":"TextWhitespace","value":" "},
163+
{"type":"Name","value":"hr"},
164+
{"type":"TextWhitespace","value":" "},
165+
{"type":"NameBuiltinPseudo","value":"=\u003e"},
166+
{"type":"TextWhitespace","value":"\n "},
167+
{"type":"Keyword","value":"have"},
168+
{"type":"TextWhitespace","value":" "},
169+
{"type":"Name","value":"hpr"},
170+
{"type":"TextWhitespace","value":" "},
171+
{"type":"Operator","value":":"},
172+
{"type":"TextWhitespace","value":" "},
173+
{"type":"Name","value":"p"},
174+
{"type":"TextWhitespace","value":" "},
175+
{"type":"NameBuiltinPseudo","value":"∧"},
176+
{"type":"TextWhitespace","value":" "},
177+
{"type":"Name","value":"r"},
178+
{"type":"TextWhitespace","value":" "},
179+
{"type":"Operator","value":":"},
180+
{"type":"NameBuiltinPseudo","value":"="},
181+
{"type":"TextWhitespace","value":" "},
182+
{"type":"Name","value":"And"},
183+
{"type":"NameBuiltinPseudo","value":"."},
184+
{"type":"Name","value":"intro"},
185+
{"type":"TextWhitespace","value":" "},
186+
{"type":"Name","value":"hp"},
187+
{"type":"TextWhitespace","value":" "},
188+
{"type":"Name","value":"hr"},
189+
{"type":"TextWhitespace","value":"\n "},
190+
{"type":"Name","value":"apply"},
191+
{"type":"TextWhitespace","value":" "},
192+
{"type":"Name","value":"Or"},
193+
{"type":"NameBuiltinPseudo","value":"."},
194+
{"type":"Name","value":"inr"},
195+
{"type":"TextWhitespace","value":"\n "},
196+
{"type":"Name","value":"exact"},
197+
{"type":"TextWhitespace","value":" "},
198+
{"type":"Name","value":"hpr"},
199+
{"type":"TextWhitespace","value":"\n"}
200+
]

0 commit comments

Comments
 (0)