From 80421a580d20b5c2efd4a914355317059cc68b8f Mon Sep 17 00:00:00 2001 From: Florian Hahn Date: Wed, 6 Jan 2016 12:16:19 +0100 Subject: Add lexer for the Silver language --- pygments/lexers/_mapping.py | 1 + pygments/lexers/esoteric.py | 50 ++++++++++- tests/examplefiles/test.sil | 206 ++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 256 insertions(+), 1 deletion(-) create mode 100644 tests/examplefiles/test.sil diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py index a08e806c..3fe81907 100644 --- a/pygments/lexers/_mapping.py +++ b/pygments/lexers/_mapping.py @@ -347,6 +347,7 @@ LEXERS = { 'RubyConsoleLexer': ('pygments.lexers.ruby', 'Ruby irb session', ('rbcon', 'irb'), (), ('text/x-ruby-shellsession',)), 'RubyLexer': ('pygments.lexers.ruby', 'Ruby', ('rb', 'ruby', 'duby'), ('*.rb', '*.rbw', 'Rakefile', '*.rake', '*.gemspec', '*.rbx', '*.duby', 'Gemfile'), ('text/x-ruby', 'application/x-ruby')), 'RustLexer': ('pygments.lexers.rust', 'Rust', ('rust',), ('*.rs', '*.rs.in'), ('text/rust',)), + 'SilverLexer': ('pygments.lexers.esoteric', 'Silver', ('silver',), ('*.sil',), ()), 'SLexer': ('pygments.lexers.r', 'S', ('splus', 's', 'r'), ('*.S', '*.R', '.Rhistory', '.Rprofile', '.Renviron'), ('text/S-plus', 'text/S', 'text/x-r-source', 'text/x-r', 'text/x-R', 'text/x-r-history', 'text/x-r-profile')), 'SMLLexer': ('pygments.lexers.ml', 'Standard ML', ('sml',), ('*.sml', '*.sig', '*.fun'), ('text/x-standardml', 'application/x-standardml')), 'SassLexer': ('pygments.lexers.css', 'Sass', ('sass',), ('*.sass',), ('text/x-sass',)), diff --git a/pygments/lexers/esoteric.py b/pygments/lexers/esoteric.py index 73ea4a4a..d7951c35 100644 --- a/pygments/lexers/esoteric.py +++ b/pygments/lexers/esoteric.py @@ -13,7 +13,7 @@ from pygments.lexer import RegexLexer, include, words from pygments.token import Text, Comment, Operator, Keyword, Name, String, \ Number, Punctuation, Error, Whitespace -__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer', 'CAmkESLexer'] +__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer', 'CAmkESLexer', 'SilverLexer'] class BrainfuckLexer(RegexLexer): @@ -217,3 +217,51 @@ class BoogieLexer(RegexLexer): (r'[0-9]+', Number.Integer), ], } + +class SilverLexer(RegexLexer): + """ + For `Silver `_ source code. + + .. versionadded:: 2.1 + """ + name = 'Silver' + aliases = ['silver'] + filenames = ['*.sil'] + + tokens = { + 'root': [ + # Whitespace and Comments + (r'\n', Whitespace), + (r'\s+', Whitespace), + (r'//[/!](.*?)\n', Comment.Doc), + (r'//(.*?)\n', Comment.Single), + (r'/\*', Comment.Multiline, 'comment'), + + (words(( + 'result', 'true', 'false', 'null', 'method', 'function', + 'predicate', 'program', 'domain', 'axiom', 'var', 'returns', + 'field', 'define', 'requires', 'ensures', 'invariant', + 'fold', 'unfold', 'inhale', 'exhale', 'new', 'assert', + 'assume', 'goto', 'while', 'if', 'elseif', 'else', 'fresh', + 'constraining', 'Seq', 'Set', 'Multiset', 'union', 'intersection', + 'setminus', 'subset', 'unfolding', 'in', 'old', 'forall', 'exists', + 'acc', 'wildcard', 'write', 'none', 'epsilon', 'perm', 'unique'), + suffix=r'\b'), Keyword), + (words(('Int', 'Perm', 'Bool', 'Ref'), suffix=r'\b'), Keyword.Type), + include('numbers'), + + (r'[!%&*+=|?:<>/-]', Operator), + (r"([{}():;,.])", Punctuation), + # Identifier + (r'[a-zA-Z_$0-9]\w*', Name), + ], + 'comment': [ + (r'[^*/]+', Comment.Multiline), + (r'/\*', Comment.Multiline, '#push'), + (r'\*/', Comment.Multiline, '#pop'), + (r'[*/]', Comment.Multiline), + ], + 'numbers': [ + (r'[0-9]+', Number.Integer), + ], + } diff --git a/tests/examplefiles/test.sil b/tests/examplefiles/test.sil new file mode 100644 index 00000000..3bcee835 --- /dev/null +++ b/tests/examplefiles/test.sil @@ -0,0 +1,206 @@ +domain Option__Node { + unique function Option__Node__Some(): Option__Node + unique function Option__Node__None(): Option__Node + + function variantOfOptionNode(self: Ref): Option__Node + + function isOptionNode(self: Ref): Bool + + axiom ax_variantOfOptionNodeChoices { + forall x: Ref :: { variantOfOptionNode(x) } + (variantOfOptionNode(x) == Option__Node__Some() || variantOfOptionNode(x) == Option__Node__None()) + } + + axiom ax_isCounterState { + forall x: Ref :: { variantOfOptionNode(x) } + isOptionNode(x) == (variantOfOptionNode(x) == Option__Node__Some() || + variantOfOptionNode(x) == Option__Node__None()) + } +} + +predicate validOption(this: Ref) { + isOptionNode(this) && + variantOfOptionNode(this) == Option__Node__Some() ==> ( + acc(this.Option__Node__Some__1, write) && + acc(validNode(this.Option__Node__Some__1)) + ) +} + +field Option__Node__Some__1: Ref + +field Node__v: Int +field Node__next: Ref + +predicate validNode(this: Ref) { + acc(this.Node__v) && + acc(this.Node__next) && + acc(validOption(this.Node__next)) +} + + +function length(this: Ref): Int + requires acc(validNode(this), write) + ensures result >= 1 +{ + (unfolding acc(validNode(this), write) in + unfolding acc(validOption(this.Node__next)) in + (variantOfOptionNode(this.Node__next) == Option__Node__None()) ? + 1 : 1 + length(this.Node__next.Option__Node__Some__1) + ) +} + +function itemAt(this: Ref, i: Int): Int + requires acc(validNode(this), write) + requires 0 <= i && i < length(this) +{ + unfolding acc(validNode(this), write) in unfolding acc(validOption(this.Node__next)) in ( + (i == 0) ? + this.Node__v: + (variantOfOptionNode(this.Node__next) == Option__Node__Some()) ? + itemAt(this.Node__next.Option__Node__Some__1, i-1) : this.Node__v + ) +} + +function sum(this$1: Ref): Int + requires acc(validNode(this$1), write) +{ + (unfolding acc(validNode(this$1), write) in unfolding acc(validOption(this$1.Node__next)) in + (variantOfOptionNode(this$1.Node__next) == Option__Node__None()) ? this$1.Node__v : this$1.Node__v + sum(this$1.Node__next.Option__Node__Some__1)) +} + +method append(this: Ref, val: Int) + requires acc(validNode(this), write) + ensures acc(validNode(this), write) /* POST1 */ + ensures length(this) == (old(length(this)) + 1) /* POST2 */ + ensures (forall i: Int :: (0 <= i && i < old(length(this))) ==> (itemAt(this, i) == old(itemAt(this, i)))) /* POST3 */ + ensures itemAt(this, length(this) - 1) == val /* POST4 */ + ensures true ==> true +{ + var tmp_node: Ref + var tmp_option: Ref + + unfold acc(validNode(this), write) + unfold acc(validOption(this.Node__next), write) + + if (variantOfOptionNode(this.Node__next) == Option__Node__None()) { + tmp_node := new(Node__next, Node__v) + tmp_node.Node__next := null + tmp_node.Node__v := val + + assume variantOfOptionNode(tmp_node.Node__next) == Option__Node__None() + fold acc(validOption(tmp_node.Node__next)) + fold acc(validNode(tmp_node), write) + + tmp_option := new(Option__Node__Some__1) + tmp_option.Option__Node__Some__1 := tmp_node + assume variantOfOptionNode(tmp_option) == Option__Node__Some() + fold acc(validOption(tmp_option)) + + this.Node__next := tmp_option + + + unfold validOption(tmp_option) + assert length(tmp_node) == 1 /* TODO: Required by Silicon, POST2 fails otherwise */ + assert itemAt(tmp_node, 0) == val /* TODO: Required by Silicon, POST4 fails otherwise */ + fold validOption(tmp_option) + } else { + append(this.Node__next.Option__Node__Some__1, val) + fold acc(validOption(this.Node__next), write) + } + + fold acc(validNode(this), write) +} + +method prepend(tail: Ref, val: Int) returns (res: Ref) + requires acc(validNode(tail)) + ensures acc(validNode(res)) + //ensures acc(validNode(tail)) + ensures length(res) == old(length(tail)) + 1 + + ensures (forall i: Int :: (1 <= i && i < length(res)) ==> (itemAt(res, i) == old(itemAt(tail, i-1)))) /* POST3 */ + ensures itemAt(res, 0) == val +{ + var tmp_option: Ref + + res := new(Node__v, Node__next) + res.Node__v := val + + tmp_option := new(Option__Node__Some__1) + tmp_option.Option__Node__Some__1 := tail + assume variantOfOptionNode(tmp_option) == Option__Node__Some() + + res.Node__next := tmp_option + + assert acc(validNode(tail)) + fold acc(validOption(res.Node__next)) + fold acc(validNode(res)) +} + +method length_iter(list: Ref) returns (len: Int) + requires acc(validNode(list), write) + ensures old(length(list)) == len + // TODO we have to preserve this property + // ensures acc(validNode(list)) +{ + var curr: Ref := list + var tmp: Ref := list + + len := 1 + + unfold acc(validNode(curr)) + unfold acc(validOption(curr.Node__next)) + while(variantOfOptionNode(curr.Node__next) == Option__Node__Some()) + invariant acc(curr.Node__v) + invariant acc(curr.Node__next) + invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> ( + acc(curr.Node__next.Option__Node__Some__1, write) && + acc(validNode(curr.Node__next.Option__Node__Some__1)) + )) + invariant (variantOfOptionNode(curr.Node__next) == Option__Node__Some() ==> len + length(curr.Node__next.Option__Node__Some__1) == old(length(list))) + invariant (variantOfOptionNode(curr.Node__next) == Option__Node__None() ==> len == old(length(list))) + { + assert acc(validNode(curr.Node__next.Option__Node__Some__1)) + len := len + 1 + tmp := curr + curr := curr.Node__next.Option__Node__Some__1 + unfold acc(validNode(curr)) + unfold acc(validOption(curr.Node__next)) + } +} + +method t1() +{ + var l: Ref + + l := new(Node__v, Node__next) + l.Node__next := null + l.Node__v := 1 + assume variantOfOptionNode(l.Node__next) == Option__Node__None() + + fold validOption(l.Node__next) + fold validNode(l) + + assert length(l) == 1 + assert itemAt(l, 0) == 1 + + append(l, 7) + assert itemAt(l, 1) == 7 + assert itemAt(l, 0) == 1 + assert length(l) == 2 + + l := prepend(l, 10) + assert itemAt(l, 2) == 7 + assert itemAt(l, 1) == 1 + assert itemAt(l, 0) == 10 + assert length(l) == 3 + + //assert sum(l) == 18 +} + +method t2(l: Ref) returns (res: Ref) + requires acc(validNode(l), write) + ensures acc(validNode(res), write) + ensures length(res) > old(length(l)) +{ + res := prepend(l, 10) +} -- cgit v1.2.1 From 8760a680a6e0561bdfacd8134555f1d3ad05eab8 Mon Sep 17 00:00:00 2001 From: Florian Hahn Date: Thu, 11 Feb 2016 10:56:53 +0100 Subject: Move Silver and Boogie lexers to separate modules --- pygments/lexers/_mapping.py | 4 +- pygments/lexers/boogie.py | 62 +++++++++++++++++++++++++++++ pygments/lexers/esoteric.py | 95 +-------------------------------------------- pygments/lexers/silver.py | 65 +++++++++++++++++++++++++++++++ 4 files changed, 130 insertions(+), 96 deletions(-) create mode 100644 pygments/lexers/boogie.py create mode 100644 pygments/lexers/silver.py diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py index 3fe81907..dfdbf4b7 100644 --- a/pygments/lexers/_mapping.py +++ b/pygments/lexers/_mapping.py @@ -54,7 +54,7 @@ LEXERS = { 'BlitzMaxLexer': ('pygments.lexers.basic', 'BlitzMax', ('blitzmax', 'bmax'), ('*.bmx',), ('text/x-bmx',)), 'BnfLexer': ('pygments.lexers.grammar_notation', 'BNF', ('bnf',), ('*.bnf',), ('text/x-bnf',)), 'BooLexer': ('pygments.lexers.dotnet', 'Boo', ('boo',), ('*.boo',), ('text/x-boo',)), - 'BoogieLexer': ('pygments.lexers.esoteric', 'Boogie', ('boogie',), ('*.bpl',), ()), + 'BoogieLexer': ('pygments.lexers.boogie', 'Boogie', ('boogie',), ('*.bpl',), ()), 'BrainfuckLexer': ('pygments.lexers.esoteric', 'Brainfuck', ('brainfuck', 'bf'), ('*.bf', '*.b'), ('application/x-brainfuck',)), 'BroLexer': ('pygments.lexers.dsls', 'Bro', ('bro',), ('*.bro',), ()), 'BugsLexer': ('pygments.lexers.modeling', 'BUGS', ('bugs', 'winbugs', 'openbugs'), ('*.bug',), ()), @@ -347,7 +347,7 @@ LEXERS = { 'RubyConsoleLexer': ('pygments.lexers.ruby', 'Ruby irb session', ('rbcon', 'irb'), (), ('text/x-ruby-shellsession',)), 'RubyLexer': ('pygments.lexers.ruby', 'Ruby', ('rb', 'ruby', 'duby'), ('*.rb', '*.rbw', 'Rakefile', '*.rake', '*.gemspec', '*.rbx', '*.duby', 'Gemfile'), ('text/x-ruby', 'application/x-ruby')), 'RustLexer': ('pygments.lexers.rust', 'Rust', ('rust',), ('*.rs', '*.rs.in'), ('text/rust',)), - 'SilverLexer': ('pygments.lexers.esoteric', 'Silver', ('silver',), ('*.sil',), ()), + 'SilverLexer': ('pygments.lexers.silver', 'Silver', ('silver',), ('*.sil',), ()), 'SLexer': ('pygments.lexers.r', 'S', ('splus', 's', 'r'), ('*.S', '*.R', '.Rhistory', '.Rprofile', '.Renviron'), ('text/S-plus', 'text/S', 'text/x-r-source', 'text/x-r', 'text/x-R', 'text/x-r-history', 'text/x-r-profile')), 'SMLLexer': ('pygments.lexers.ml', 'Standard ML', ('sml',), ('*.sml', '*.sig', '*.fun'), ('text/x-standardml', 'application/x-standardml')), 'SassLexer': ('pygments.lexers.css', 'Sass', ('sass',), ('*.sass',), ('text/x-sass',)), diff --git a/pygments/lexers/boogie.py b/pygments/lexers/boogie.py new file mode 100644 index 00000000..5ce0ba6a --- /dev/null +++ b/pygments/lexers/boogie.py @@ -0,0 +1,62 @@ +# -*- coding: utf-8 -*- +""" + pygments.lexers.boogie + ~~~~~~~~~~~~~~~~~~~~~~~~ + + Lexers for esoteric languages. + + :copyright: Copyright 2006-2016 by the Pygments team, see AUTHORS. + :license: BSD, see LICENSE for details. +""" + +from pygments.lexer import RegexLexer, include, words +from pygments.token import Comment, Operator, Keyword, Name, Number, \ + Punctuation, Whitespace + +__all__ = ['BoogieLexer',] + + + +class BoogieLexer(RegexLexer): + """ + For `Boogie `_ source code. + + .. versionadded:: 2.1 + """ + name = 'Boogie' + aliases = ['boogie'] + filenames = ['*.bpl'] + + tokens = { + 'root': [ + # Whitespace and Comments + (r'\n', Whitespace), + (r'\s+', Whitespace), + (r'//[/!](.*?)\n', Comment.Doc), + (r'//(.*?)\n', Comment.Single), + (r'/\*', Comment.Multiline, 'comment'), + + (words(( + 'axiom', 'break', 'call', 'ensures', 'else', 'exists', 'function', + 'forall', 'if', 'invariant', 'modifies', 'procedure', 'requires', + 'then', 'var', 'while'), + suffix=r'\b'), Keyword), + (words(('const',), suffix=r'\b'), Keyword.Reserved), + + (words(('bool', 'int', 'ref'), suffix=r'\b'), Keyword.Type), + include('numbers'), + (r"(>=|<=|:=|!=|==>|&&|\|\||[+/\-=>*<\[\]])", Operator), + (r"([{}():;,.])", Punctuation), + # Identifier + (r'[a-zA-Z_]\w*', Name), + ], + 'comment': [ + (r'[^*/]+', Comment.Multiline), + (r'/\*', Comment.Multiline, '#push'), + (r'\*/', Comment.Multiline, '#pop'), + (r'[*/]', Comment.Multiline), + ], + 'numbers': [ + (r'[0-9]+', Number.Integer), + ], + } diff --git a/pygments/lexers/esoteric.py b/pygments/lexers/esoteric.py index d7951c35..ae6d0598 100644 --- a/pygments/lexers/esoteric.py +++ b/pygments/lexers/esoteric.py @@ -13,7 +13,7 @@ from pygments.lexer import RegexLexer, include, words from pygments.token import Text, Comment, Operator, Keyword, Name, String, \ Number, Punctuation, Error, Whitespace -__all__ = ['BrainfuckLexer', 'BefungeLexer', 'BoogieLexer', 'RedcodeLexer', 'CAmkESLexer', 'SilverLexer'] +__all__ = ['BrainfuckLexer', 'BefungeLexer', 'RedcodeLexer', 'CAmkESLexer'] class BrainfuckLexer(RegexLexer): @@ -172,96 +172,3 @@ class RedcodeLexer(RegexLexer): (r'[-+]?\d+', Number.Integer), ], } - - -class BoogieLexer(RegexLexer): - """ - For `Boogie `_ source code. - - .. versionadded:: 2.1 - """ - name = 'Boogie' - aliases = ['boogie'] - filenames = ['*.bpl'] - - tokens = { - 'root': [ - # Whitespace and Comments - (r'\n', Whitespace), - (r'\s+', Whitespace), - (r'//[/!](.*?)\n', Comment.Doc), - (r'//(.*?)\n', Comment.Single), - (r'/\*', Comment.Multiline, 'comment'), - - (words(( - 'axiom', 'break', 'call', 'ensures', 'else', 'exists', 'function', - 'forall', 'if', 'invariant', 'modifies', 'procedure', 'requires', - 'then', 'var', 'while'), - suffix=r'\b'), Keyword), - (words(('const',), suffix=r'\b'), Keyword.Reserved), - - (words(('bool', 'int', 'ref'), suffix=r'\b'), Keyword.Type), - include('numbers'), - (r"(>=|<=|:=|!=|==>|&&|\|\||[+/\-=>*<\[\]])", Operator), - (r"([{}():;,.])", Punctuation), - # Identifier - (r'[a-zA-Z_]\w*', Name), - ], - 'comment': [ - (r'[^*/]+', Comment.Multiline), - (r'/\*', Comment.Multiline, '#push'), - (r'\*/', Comment.Multiline, '#pop'), - (r'[*/]', Comment.Multiline), - ], - 'numbers': [ - (r'[0-9]+', Number.Integer), - ], - } - -class SilverLexer(RegexLexer): - """ - For `Silver `_ source code. - - .. versionadded:: 2.1 - """ - name = 'Silver' - aliases = ['silver'] - filenames = ['*.sil'] - - tokens = { - 'root': [ - # Whitespace and Comments - (r'\n', Whitespace), - (r'\s+', Whitespace), - (r'//[/!](.*?)\n', Comment.Doc), - (r'//(.*?)\n', Comment.Single), - (r'/\*', Comment.Multiline, 'comment'), - - (words(( - 'result', 'true', 'false', 'null', 'method', 'function', - 'predicate', 'program', 'domain', 'axiom', 'var', 'returns', - 'field', 'define', 'requires', 'ensures', 'invariant', - 'fold', 'unfold', 'inhale', 'exhale', 'new', 'assert', - 'assume', 'goto', 'while', 'if', 'elseif', 'else', 'fresh', - 'constraining', 'Seq', 'Set', 'Multiset', 'union', 'intersection', - 'setminus', 'subset', 'unfolding', 'in', 'old', 'forall', 'exists', - 'acc', 'wildcard', 'write', 'none', 'epsilon', 'perm', 'unique'), - suffix=r'\b'), Keyword), - (words(('Int', 'Perm', 'Bool', 'Ref'), suffix=r'\b'), Keyword.Type), - include('numbers'), - - (r'[!%&*+=|?:<>/-]', Operator), - (r"([{}():;,.])", Punctuation), - # Identifier - (r'[a-zA-Z_$0-9]\w*', Name), - ], - 'comment': [ - (r'[^*/]+', Comment.Multiline), - (r'/\*', Comment.Multiline, '#push'), - (r'\*/', Comment.Multiline, '#pop'), - (r'[*/]', Comment.Multiline), - ], - 'numbers': [ - (r'[0-9]+', Number.Integer), - ], - } diff --git a/pygments/lexers/silver.py b/pygments/lexers/silver.py new file mode 100644 index 00000000..a4461ebf --- /dev/null +++ b/pygments/lexers/silver.py @@ -0,0 +1,65 @@ +# -*- coding: utf-8 -*- +""" + pygments.lexers.esoteric + ~~~~~~~~~~~~~~~~~~~~~~~~ + + Lexers for esoteric languages. + + :copyright: Copyright 2006-2016 by the Pygments team, see AUTHORS. + :license: BSD, see LICENSE for details. +""" + +from pygments.lexer import RegexLexer, include, words +from pygments.token import Text, Comment, Operator, Keyword, Name, Number, \ + Punctuation, Whitespace + +__all__ = ['SilverLexer',] + + +class SilverLexer(RegexLexer): + """ + For `Silver `_ source code. + + .. versionadded:: 2.1 + """ + name = 'Silver' + aliases = ['silver'] + filenames = ['*.sil'] + + tokens = { + 'root': [ + # Whitespace and Comments + (r'\n', Whitespace), + (r'\s+', Whitespace), + (r'//[/!](.*?)\n', Comment.Doc), + (r'//(.*?)\n', Comment.Single), + (r'/\*', Comment.Multiline, 'comment'), + + (words(( + 'result', 'true', 'false', 'null', 'method', 'function', + 'predicate', 'program', 'domain', 'axiom', 'var', 'returns', + 'field', 'define', 'requires', 'ensures', 'invariant', + 'fold', 'unfold', 'inhale', 'exhale', 'new', 'assert', + 'assume', 'goto', 'while', 'if', 'elseif', 'else', 'fresh', + 'constraining', 'Seq', 'Set', 'Multiset', 'union', 'intersection', + 'setminus', 'subset', 'unfolding', 'in', 'old', 'forall', 'exists', + 'acc', 'wildcard', 'write', 'none', 'epsilon', 'perm', 'unique'), + suffix=r'\b'), Keyword), + (words(('Int', 'Perm', 'Bool', 'Ref'), suffix=r'\b'), Keyword.Type), + include('numbers'), + + (r'[!%&*+=|?:<>/-]', Operator), + (r"([{}():;,.])", Punctuation), + # Identifier + (r'[a-zA-Z_$0-9]\w*', Name), + ], + 'comment': [ + (r'[^*/]+', Comment.Multiline), + (r'/\*', Comment.Multiline, '#push'), + (r'\*/', Comment.Multiline, '#pop'), + (r'[*/]', Comment.Multiline), + ], + 'numbers': [ + (r'[0-9]+', Number.Integer), + ], + } -- cgit v1.2.1