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
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
|
# -*- coding: utf-8 -*- #
# frozen_string_literal: true
# NOTE: This is for Lean 3 (community fork).
module Rouge
module Lexers
class Lean < RegexLexer
title 'Lean'
desc 'The Lean programming language (leanprover.github.io)'
tag 'lean'
aliases 'lean'
filenames '*.lean'
def self.keywords
@keywords ||= Set.new %w(
abbreviation
add_rewrite
alias
assume
axiom
begin
by
calc
calc_refl
calc_subst
calc_trans
#check
coercion
conjecture
constant
constants
context
corollary
def
definition
end
#eval
example
export
expose
exposing
exit
extends
from
fun
have
help
hiding
hott
hypothesis
import
include
including
inductive
infix
infixl
infixr
inline
instance
irreducible
lemma
match
namespace
notation
opaque
opaque_hint
open
options
parameter
parameters
postfix
precedence
prefix
#print
private
protected
#reduce
reducible
renaming
repeat
section
set_option
show
tactic_hint
theorem
universe
universes
using
variable
variables
with
)
end
def self.types
@types ||= %w(
Sort
Prop
Type
)
end
def self.operators
@operators ||= %w(
!= # & && \* \+ - / @ ! ` -\. ->
\. \.\. \.\.\. :: :> ; ;; <
<- = == > _ \| \|\| ~ => <= >=
/\ \/ ∀ Π λ ↔ ∧ ∨ ≠ ≤ ≥ ⊎
¬ ⁻¹ ⬝ ▸ → ∃ ℕ ℤ ≈ × ⌞ ⌟ ≡ ⟨ ⟩
)
end
state :root do
# comments starting after some space
rule %r/\s*--+\s+.*?$/, Comment::Doc
rule %r/"/, Str, :string
rule %r/\d+/, Num::Integer
# special commands or keywords
rule(/#?\w+/) do |m|
match = m[0]
if self.class.keywords.include?(match)
token Keyword
elsif self.class.types.include?(match)
token Keyword::Type
else
token Name
end
end
# special unicode keywords
rule %r/[λ]/, Keyword
# ----------------
# operators rules
# ----------------
rule %r/\:=?/, Text
rule %r/\.[0-9]*/, Operator
rule %r(#{Lean.operators.join('|')}), Operator
# unmatched symbols
rule %r/[\s\(\),\[\]αβ‹›]+/, Text
# show missing matches
rule %r/./, Error
end
state :string do
rule %r/"/, Str, :pop!
rule %r/\\/, Str::Escape, :escape
rule %r/[^\\"]+/, Str
end
state :escape do
rule %r/[nrt"'\\]/, Str::Escape, :pop!
rule %r/x[\da-f]+/i, Str::Escape, :pop!
end
end
end
end
|
