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
|
# -*- coding: utf-8 -*- #
# frozen_string_literal: true
module Rouge
module Lexers
class Dafny < RegexLexer
title "Dafny"
desc "The Dafny programming language (github.com/dafny-lang/dafny)"
tag "dafny"
filenames "*.dfy"
mimetypes "text/x-dafny"
keywords = %w(
abstract allocated assert assume
break by
calc case class codatatype const constructor
datatype decreases downto
else ensures exists expect export extends
false for forall fresh function
ghost greatest
if import include invariant iterator
label least lemma
match method modifies modify module
nameonly new newtype null
old opened
predicate print provides
reads refines requires return returns reveal reveals
static
then this to trait true twostate type
unchanged
var
while witness
yield yields
)
literals = %w{ true false null }
textOperators = %w{ as is in }
types = %w(bool char int real string nat
array array? object object? ORDINAL
seq set iset map imap multiset )
idstart = /[0-9a-zA-Z?]/
idchar = /[0-9a-zA-Z_'?]/
id = /#{idstart}#{idchar}*/
arrayType = /array(?:1[0-9]+|[2-9][0-9]*)\??(?!#{idchar})/
bvType = /bv(?:0|[1-9][0-9]*)(?!#{idchar})/
digit = /\d/
digits = /#{digit}+(?:_#{digit}+)*/
bin_digits = /[01]+(?:_[01]+)*/
hex_digit = /(?:[0-9a-fA-F])/
hex_digits = /#{hex_digit}+(?:_#{hex_digit}+)*/
cchar = /(?:[^\\'\n\r]|\\["'ntr\\0])/
schar = /(?:[^\\"\n\r]|\\["'ntr\\0])/
uchar = /(?:\\u#{hex_digit}{4})/
## IMPORTANT: Rules are ordered, which allows later rules to be
## simpler than they would otherwise be
state :root do
rule %r(/\*), Comment::Multiline, :comment
rule %r(//.*?$), Comment::Single
rule %r(\*/), Error # should not have closing comment in :root
# is an improperly nested comment
rule %r/'#{cchar}'/, Str::Char # standard or escape char
rule %r/'#{uchar}'/, Str::Char # unicode char
rule %r/'[^'\n\r]*'/, Error # bad any other enclosed char
rule %r/'[^'\n\r]*$/, Error # bad unclosed char
rule %r/"(?:#{schar}|#{uchar})*"/, Str::Double # valid string
rule %r/".*"/, Error # anything else that is closed
rule %r/".*$/, Error # bad unclosed string
rule %r/@"([^"]|"")*"/, Str::Other # valid verbatim string
rule %r/@".*/m, Error # anything else , multiline unclosed
rule %r/#{digits}\.#{digits}(?!#{idchar})/, Num::Float
rule %r/0b#{bin_digits}(?!#{idchar})/, Num::Bin
rule %r/0b#{idchar}*/, Error
rule %r/0x#{hex_digits}(?!#{idchar})/, Num::Hex
rule %r/0x#{idchar}*/, Error
rule %r/#{digits}(?!#{idchar})/, Num::Integer
rule %r/_(?!#{idchar})/, Name
rule %r/_[0-9_]+[_]?(?!#{idchar})/, Error
rule %r/[0-9_]+_(?!#{idchar})/, Error
rule %r/[0-9]#{idchar}+/, Error
rule %r/#{arrayType}/, Keyword::Type
rule %r/#{bvType}/, Keyword::Type
rule id do |m|
if types.include?(m[0])
token Keyword::Type
elsif literals.include?(m[0])
token Keyword::Constant
elsif textOperators.include?(m[0])
token Operator::Word
elsif keywords.include?(m[0])
token Keyword::Reserved
else
token Name
end
end
rule %r/\.\./, Operator
rule %r/[*!%&<>\|^+=:.\/-]/, Operator
rule %r/[\[\](){},;`]/, Punctuation
rule %r/[^\S\n]+/, Text
rule %r/\n/, Text
rule %r/./, Error # Catchall
end
state :comment do
rule %r(\*/), Comment::Multiline, :pop!
rule %r(/\*), Comment::Multiline, :comment
rule %r([^*/]+), Comment::Multiline
rule %r(.), Comment::Multiline
end
end
end
end
|
