|
1 # -*- coding: utf-8 -*- |
|
2 """ |
|
3 pygments.lexers.verification |
|
4 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
5 |
|
6 Lexer for Intermediate Verification Languages (IVLs). |
|
7 |
|
8 :copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS. |
|
9 :license: BSD, see LICENSE for details. |
|
10 """ |
|
11 |
|
12 from pygments.lexer import RegexLexer, include, words |
|
13 from pygments.token import Comment, Operator, Keyword, Name, Number, \ |
|
14 Punctuation, Whitespace |
|
15 |
|
16 __all__ = ['BoogieLexer', 'SilverLexer'] |
|
17 |
|
18 |
|
19 class BoogieLexer(RegexLexer): |
|
20 """ |
|
21 For `Boogie <https://boogie.codeplex.com/>`_ source code. |
|
22 |
|
23 .. versionadded:: 2.1 |
|
24 """ |
|
25 name = 'Boogie' |
|
26 aliases = ['boogie'] |
|
27 filenames = ['*.bpl'] |
|
28 |
|
29 tokens = { |
|
30 'root': [ |
|
31 # Whitespace and Comments |
|
32 (r'\n', Whitespace), |
|
33 (r'\s+', Whitespace), |
|
34 (r'//[/!](.*?)\n', Comment.Doc), |
|
35 (r'//(.*?)\n', Comment.Single), |
|
36 (r'/\*', Comment.Multiline, 'comment'), |
|
37 |
|
38 (words(( |
|
39 'axiom', 'break', 'call', 'ensures', 'else', 'exists', 'function', |
|
40 'forall', 'if', 'invariant', 'modifies', 'procedure', 'requires', |
|
41 'then', 'var', 'while'), |
|
42 suffix=r'\b'), Keyword), |
|
43 (words(('const',), suffix=r'\b'), Keyword.Reserved), |
|
44 |
|
45 (words(('bool', 'int', 'ref'), suffix=r'\b'), Keyword.Type), |
|
46 include('numbers'), |
|
47 (r"(>=|<=|:=|!=|==>|&&|\|\||[+/\-=>*<\[\]])", Operator), |
|
48 (r"([{}():;,.])", Punctuation), |
|
49 # Identifier |
|
50 (r'[a-zA-Z_]\w*', Name), |
|
51 ], |
|
52 'comment': [ |
|
53 (r'[^*/]+', Comment.Multiline), |
|
54 (r'/\*', Comment.Multiline, '#push'), |
|
55 (r'\*/', Comment.Multiline, '#pop'), |
|
56 (r'[*/]', Comment.Multiline), |
|
57 ], |
|
58 'numbers': [ |
|
59 (r'[0-9]+', Number.Integer), |
|
60 ], |
|
61 } |
|
62 |
|
63 |
|
64 class SilverLexer(RegexLexer): |
|
65 """ |
|
66 For `Silver <https://bitbucket.org/viperproject/silver>`_ source code. |
|
67 |
|
68 .. versionadded:: 2.2 |
|
69 """ |
|
70 name = 'Silver' |
|
71 aliases = ['silver'] |
|
72 filenames = ['*.sil', '*.vpr'] |
|
73 |
|
74 tokens = { |
|
75 'root': [ |
|
76 # Whitespace and Comments |
|
77 (r'\n', Whitespace), |
|
78 (r'\s+', Whitespace), |
|
79 (r'//[/!](.*?)\n', Comment.Doc), |
|
80 (r'//(.*?)\n', Comment.Single), |
|
81 (r'/\*', Comment.Multiline, 'comment'), |
|
82 |
|
83 (words(( |
|
84 'result', 'true', 'false', 'null', 'method', 'function', |
|
85 'predicate', 'program', 'domain', 'axiom', 'var', 'returns', |
|
86 'field', 'define', 'requires', 'ensures', 'invariant', |
|
87 'fold', 'unfold', 'inhale', 'exhale', 'new', 'assert', |
|
88 'assume', 'goto', 'while', 'if', 'elseif', 'else', 'fresh', |
|
89 'constraining', 'Seq', 'Set', 'Multiset', 'union', 'intersection', |
|
90 'setminus', 'subset', 'unfolding', 'in', 'old', 'forall', 'exists', |
|
91 'acc', 'wildcard', 'write', 'none', 'epsilon', 'perm', 'unique', |
|
92 'apply', 'package', 'folding', 'label', 'forperm'), |
|
93 suffix=r'\b'), Keyword), |
|
94 (words(('Int', 'Perm', 'Bool', 'Ref'), suffix=r'\b'), Keyword.Type), |
|
95 include('numbers'), |
|
96 |
|
97 (r'[!%&*+=|?:<>/\-\[\]]', Operator), |
|
98 (r'([{}():;,.])', Punctuation), |
|
99 # Identifier |
|
100 (r'[\w$]\w*', Name), |
|
101 ], |
|
102 'comment': [ |
|
103 (r'[^*/]+', Comment.Multiline), |
|
104 (r'/\*', Comment.Multiline, '#push'), |
|
105 (r'\*/', Comment.Multiline, '#pop'), |
|
106 (r'[*/]', Comment.Multiline), |
|
107 ], |
|
108 'numbers': [ |
|
109 (r'[0-9]+', Number.Integer), |
|
110 ], |
|
111 } |