92 lines
3.1 KiB
Python
Executable File
92 lines
3.1 KiB
Python
Executable File
# -*- coding: utf-8 -*-
|
|
#!/usr/bin/env python3
|
|
"""
|
|
pygments.lexers.dafny
|
|
~~~~~~~~~~~~~~~~~~~~~~~~~~
|
|
|
|
Lexers for Dafny.
|
|
|
|
:copyright: Copyright 2006-2022 by the Pygments team, see AUTHORS.
|
|
:license: BSD, see LICENSE for details.
|
|
"""
|
|
|
|
import re
|
|
|
|
from pygments.lexer import RegexLexer, include, bygroups
|
|
from pygments.token import *
|
|
|
|
import argparse
|
|
import sys
|
|
import pygments.cmdline as _cmdline
|
|
import pygments.lexer as _lexer
|
|
import pygments.token as _token
|
|
|
|
|
|
def main(args):
|
|
parser = argparse.ArgumentParser()
|
|
parser.add_argument('-l', dest='lexer', type=str)
|
|
opts, rest = parser.parse_known_args(args[1:])
|
|
if opts.lexer == 'dafny':
|
|
args = [__file__, '-l', __file__ + ':DafnyLexer', '-x', *rest]
|
|
_cmdline.main(args)
|
|
|
|
|
|
class DafnyLexer(RegexLexer):
|
|
"""
|
|
For Dafny source code.
|
|
"""
|
|
|
|
name = 'Dafny'
|
|
aliases = ['dafny']
|
|
filenames = ['*.dfy']
|
|
mimetypes = []
|
|
|
|
flags = re.DOTALL | re.UNICODE | re.MULTILINE
|
|
|
|
valid_name = r'[\w_]+'
|
|
|
|
tokens = {
|
|
'commentsandwhitespace': [
|
|
(r'\s+', Text),
|
|
(r'//.*?\n', Comment.Single),
|
|
(r'/\*.*?\*/', Comment.Multiline),
|
|
],
|
|
'string': [
|
|
(r'"(\\\\|\\"|[^"])*"', String.Double),
|
|
(r"'(\\\\|\\'|[^'])*'", String.Single),
|
|
],
|
|
'root': [
|
|
include('commentsandwhitespace'),
|
|
(r'(:=)', Operator),
|
|
(r'(\|)', Operator),
|
|
(r'(;|::|:|\.\.|`)', Punctuation),
|
|
(r'[{(\[,.\])}]', Punctuation),
|
|
(r'(==|!=|<=|>=|=|&&|[-<>+*/%])', Operator),
|
|
(r'(in)\b', Operator),
|
|
(r'(this|old|print)\b', Name.Function.Magic),
|
|
(r'(multiset)(\s*)(\()', bygroups(Name.Function.Magic, Text, Punctuation)),
|
|
(r'(reads|modifies|ensures|requires|assert|assume|expect|invariant|decreases|constructor)\b', Keyword),
|
|
(r'(if|then|else|while|returns|forall)\b', Keyword),
|
|
(r'(function|method|predicate|lemma)(\s+\{[^\}]+\}\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Function)),
|
|
(r'(function|method|predicate|lemma)(\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Function)),
|
|
(r'(function|method|predicate|lemma)', Keyword.Declaration),
|
|
(r'(trait|class|datatype)(\s+\{[^\}]+\}\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Class)),
|
|
(r'(trait|class|datatype)(\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name.Class)),
|
|
(r'(trait|class|datatype)', Keyword.Declaration),
|
|
(r'(extends)(\s+)(\w+)', bygroups(Keyword, Text, Name.Class)),
|
|
(r'(extends)', Keyword),
|
|
(r'(var)(\s+)(\w+)', bygroups(Keyword.Declaration, Text, Name)), # actually Name.Variable.Instance, but that would be inconsistent, as we don't know this information on other occurrences
|
|
(r'(var|ghost)\b', Keyword.Declaration),
|
|
(r'(true|false)\b', Keyword.Constant),
|
|
(r'(array|seq|set|multiset|int|nat|string|char)\b', Keyword.Type),
|
|
(r'[0-9]+', Number.Integer),
|
|
include('string'),
|
|
|
|
(valid_name, Name),
|
|
]
|
|
}
|
|
|
|
if __name__ == '__main__':
|
|
main(sys.argv)
|
|
|