From f1283e65e34483658a89bc48a885f840ce6c8a34 Mon Sep 17 00:00:00 2001 From: Hillel Date: Sat, 19 Nov 2022 08:09:00 +0100 Subject: [PATCH] Update Alloy for Alloy 6 (PR #1963) manual cherry-pick --- CHANGES | 1 + pygments/lexers/dsls.py | 22 +++++--- tests/examplefiles/alloy/example.als | 40 +++++++-------- tests/examplefiles/alloy/example.als.output | 56 ++++++++++----------- 4 files changed, 64 insertions(+), 55 deletions(-) diff --git a/CHANGES b/CHANGES index 360fe2f92d..6c8f782e26 100644 --- a/CHANGES +++ b/CHANGES @@ -21,6 +21,7 @@ Version 2.14.0 - Updated lexers: + * Alloy: update for Alloy 6 (#1963) * C family (C, C++ and many others): fix an issue where a chunk would be wrongly recognized as a function definition due to braces in comments (#2210) diff --git a/pygments/lexers/dsls.py b/pygments/lexers/dsls.py index 34e9b55f66..ea16766483 100644 --- a/pygments/lexers/dsls.py +++ b/pygments/lexers/dsls.py @@ -601,7 +601,8 @@ class AlloyLexer(RegexLexer): flags = re.MULTILINE | re.DOTALL - iden_rex = r'[a-zA-Z_][\w\']*' + iden_rex = r'[a-zA-Z_][\w]*"*' + string_rex = r'"\b(\\\\|\\[^\\]|[^"\\])*"' text_tuple = (r'[^\S\n]+', Whitespace) tokens = { @@ -621,6 +622,10 @@ class AlloyLexer(RegexLexer): (r'\{', Operator, '#pop'), (iden_rex, Name, '#pop'), ], + 'fact': [ + include('fun'), + (string_rex, String, '#pop'), + ], 'root': [ (r'--.*?$', Comment.Single), (r'//.*?$', Comment.Single), @@ -631,17 +636,20 @@ class AlloyLexer(RegexLexer): (r'(sig|enum)(\s+)', bygroups(Keyword.Declaration, Whitespace), 'sig'), (r'(iden|univ|none)\b', Keyword.Constant), (r'(int|Int)\b', Keyword.Type), - (r'(this|abstract|extends|set|seq|one|lone|let)\b', Keyword), + (r'(var|this|abstract|extends|set|seq|one|lone|let)\b', Keyword), (r'(all|some|no|sum|disj|when|else)\b', Keyword), - (r'(run|check|for|but|exactly|expect|as)\b', Keyword), + (r'(run|check|for|but|exactly|expect|as|steps)\b', Keyword), + (r'(always|after|eventually|until|release)\b', Keyword), # future time operators + (r'(historically|before|once|since|triggered)\b', Keyword), # past time operators (r'(and|or|implies|iff|in)\b', Operator.Word), - (r'(fun|pred|fact|assert)(\s+)', bygroups(Keyword, Whitespace), 'fun'), - (r'!|#|&&|\+\+|<<|>>|>=|<=>|<=|\.|->', Operator), - (r'[-+/*%=<>&!^|~{}\[\]().]', Operator), + (r'(fun|pred|assert)(\s+)', bygroups(Keyword, Whitespace), 'fun'), + (r'(fact)(\s+)', bygroups(Keyword, Whitespace), 'fact'), + (r'!|#|&&|\+\+|<<|>>|>=|<=>|<=|\.\.|\.|->', Operator), + (r'[-+/*%=<>&!^|~{}\[\]().\';]', Operator), (iden_rex, Name), (r'[:,]', Punctuation), (r'[0-9]+', Number.Integer), - (r'"(\\\\|\\[^\\]|[^"\\])*"', String), + (string_rex, String), (r'\n', Whitespace), ] } diff --git a/tests/examplefiles/alloy/example.als b/tests/examplefiles/alloy/example.als index 3a5ab82bf8..c1a6d27e26 100644 --- a/tests/examplefiles/alloy/example.als +++ b/tests/examplefiles/alloy/example.als @@ -32,8 +32,8 @@ module examples/systems/views * * As a terminological convention, when there are two * complementary view relationships, we will give them types - * t and t'. For example, KeySetView propagates from map to - * set, and KeySetView' propagates from set to map. + * t and t". For example, KeySetView propagates from map to + * set, and KeySetView" propagates from set to map. * * author: Daniel Jackson */ @@ -76,12 +76,12 @@ sig SetRef extends Ref {} fact {State.obj[SetRef] in Set} abstract sig ViewType {} -one sig KeySetView, KeySetView', IteratorView extends ViewType {} +one sig KeySetView, KeySetView", IteratorView extends ViewType {} fact ViewTypes { State.views[KeySetView] in MapRef -> SetRef - State.views[KeySetView'] in SetRef -> MapRef + State.views[KeySetView"] in SetRef -> MapRef State.views[IteratorView] in IteratorRef -> SetRef - all s: State | s.views[KeySetView] = ~(s.views[KeySetView']) + all s: State | s.views[KeySetView] = ~(s.views[KeySetView"]) } /** @@ -107,20 +107,20 @@ pred allocates [pre, post: State, rs: set Ref] { } /** - * models frame condition that limits change to view object from v to v' when backing object changes to b' + * models frame condition that limits change to view object from v to v" when backing object changes to b" */ -pred viewFrame [t: ViewType, v, v', b': Object] { - t in KeySetView => v'.elts = dom [b'.map] - t in KeySetView' => b'.elts = dom [v'.map] - t in KeySetView' => (b'.elts) <: (v.map) = (b'.elts) <: (v'.map) - t in IteratorView => v'.elts = b'.left + b'.done +pred viewFrame [t: ViewType, v, v", b": Object] { + t in KeySetView => v".elts = dom [b".map] + t in KeySetView" => b".elts = dom [v".map] + t in KeySetView" => (b".elts) <: (v.map) = (b".elts) <: (v".map) + t in IteratorView => v".elts = b".left + b".done } pred MapRef.keySet [pre, post: State, setRefs: SetRef] { post.obj[setRefs].elts = dom [pre.obj[this].map] modifies [pre, post, none] allocates [pre, post, setRefs] - post.views = pre.views + KeySetView->this->setRefs + KeySetView'->setRefs->this + post.views = pre.views + KeySetView->this->setRefs + KeySetView"->setRefs->this } pred MapRef.put [pre, post: State, k, v: Ref] { @@ -141,10 +141,10 @@ pred SetRef.iterator [pre, post: State, iterRef: IteratorRef] { } pred IteratorRef.remove [pre, post: State] { - let i = pre.obj[this], i' = post.obj[this] { - i'.left = i.left - i'.done = i.done - i.lastRef - no i'.lastRef + let i = pre.obj[this], i" = post.obj[this] { + i".left = i.left + i".done = i.done - i.lastRef + no i".lastRef } modifies [pre,post,this] allocates [pre, post, none] @@ -152,11 +152,11 @@ pred IteratorRef.remove [pre, post: State] { } pred IteratorRef.next [pre, post: State, ref: Ref] { - let i = pre.obj[this], i' = post.obj[this] { + let i = pre.obj[this], i" = post.obj[this] { ref in i.left - i'.left = i.left - ref - i'.done = i.done + ref - i'.lastRef = ref + i".left = i.left - ref + i".done = i.done + ref + i".lastRef = ref } modifies [pre, post, this] allocates [pre, post, none] diff --git a/tests/examplefiles/alloy/example.als.output b/tests/examplefiles/alloy/example.als.output index fc7d42b30f..bda535e208 100644 --- a/tests/examplefiles/alloy/example.als.output +++ b/tests/examplefiles/alloy/example.als.output @@ -9,7 +9,7 @@ '\n' Text.Whitespace -"/*\n * Model of views in object-oriented programming.\n *\n * Two object references, called the view and the backing,\n * are related by a view mechanism when changes to the\n * backing are automatically propagated to the view. Note\n * that the state of a view need not be a projection of the\n * state of the backing; the keySet method of Map, for\n * example, produces two view relationships, and for the\n * one in which the map is modified by changes to the key\n * set, the value of the new map cannot be determined from\n * the key set. Note that in the iterator view mechanism,\n * the iterator is by this definition the backing object,\n * since changes are propagated from iterator to collection\n * and not vice versa. Oddly, a reference may be a view of\n * more than one backing: there can be two iterators on the\n * same collection, eg. A reference cannot be a view under\n * more than one view type.\n *\n * A reference is made dirty when it is a backing for a view\n * with which it is no longer related by the view invariant.\n * This usually happens when a view is modified, either\n * directly or via another backing. For example, changing a\n * collection directly when it has an iterator invalidates\n * it, as does changing the collection through one iterator\n * when there are others.\n *\n * More work is needed if we want to model more closely the\n * failure of an iterator when its collection is invalidated.\n *\n * As a terminological convention, when there are two\n * complementary view relationships, we will give them types\n * t and t'. For example, KeySetView propagates from map to\n * set, and KeySetView' propagates from set to map.\n *\n * author: Daniel Jackson\n */" Comment.Multiline +'/*\n * Model of views in object-oriented programming.\n *\n * Two object references, called the view and the backing,\n * are related by a view mechanism when changes to the\n * backing are automatically propagated to the view. Note\n * that the state of a view need not be a projection of the\n * state of the backing; the keySet method of Map, for\n * example, produces two view relationships, and for the\n * one in which the map is modified by changes to the key\n * set, the value of the new map cannot be determined from\n * the key set. Note that in the iterator view mechanism,\n * the iterator is by this definition the backing object,\n * since changes are propagated from iterator to collection\n * and not vice versa. Oddly, a reference may be a view of\n * more than one backing: there can be two iterators on the\n * same collection, eg. A reference cannot be a view under\n * more than one view type.\n *\n * A reference is made dirty when it is a backing for a view\n * with which it is no longer related by the view invariant.\n * This usually happens when a view is modified, either\n * directly or via another backing. For example, changing a\n * collection directly when it has an iterator invalidates\n * it, as does changing the collection through one iterator\n * when there are others.\n *\n * More work is needed if we want to model more closely the\n * failure of an iterator when its collection is invalidated.\n *\n * As a terminological convention, when there are two\n * complementary view relationships, we will give them types\n * t and t". For example, KeySetView propagates from map to\n * set, and KeySetView" propagates from set to map.\n *\n * author: Daniel Jackson\n */' Comment.Multiline '\n' Text.Whitespace '\n' Text.Whitespace @@ -407,7 +407,7 @@ 'KeySetView' Name ',' Punctuation ' ' Text.Whitespace -"KeySetView'" Name +'KeySetView"' Name ',' Punctuation ' ' Text.Whitespace 'IteratorView' Name @@ -449,7 +449,7 @@ '.' Operator 'views' Name '[' Operator -"KeySetView'" Name +'KeySetView"' Name ']' Operator ' ' Text.Whitespace 'in' Operator.Word @@ -503,7 +503,7 @@ '.' Operator 'views' Name '[' Operator -"KeySetView'" Name +'KeySetView"' Name ']' Operator ')' Operator '\n' Text.Whitespace @@ -837,7 +837,7 @@ '\n' Text.Whitespace -"/** \n * models frame condition that limits change to view object from v to v' when backing object changes to b'\n */" Comment.Multiline +'/** \n * models frame condition that limits change to view object from v to v" when backing object changes to b"\n */' Comment.Multiline '\n' Text.Whitespace 'pred' Keyword @@ -854,10 +854,10 @@ 'v' Name ',' Punctuation ' ' Text.Whitespace -"v'" Name +'v"' Name ',' Punctuation ' ' Text.Whitespace -"b'" Name +'b"' Name ':' Punctuation ' ' Text.Whitespace 'Object' Name @@ -876,7 +876,7 @@ '=' Operator '>' Operator ' ' Text.Whitespace -"v'" Name +'v"' Name '.' Operator 'elts' Name ' ' Text.Whitespace @@ -885,7 +885,7 @@ 'dom' Name ' ' Text.Whitespace '[' Operator -"b'" Name +'b"' Name '.' Operator 'map' Name ']' Operator @@ -896,12 +896,12 @@ ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace -"KeySetView'" Name +'KeySetView"' Name ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace -"b'" Name +'b"' Name '.' Operator 'elts' Name ' ' Text.Whitespace @@ -910,7 +910,7 @@ 'dom' Name ' ' Text.Whitespace '[' Operator -"v'" Name +'v"' Name '.' Operator 'map' Name ']' Operator @@ -921,13 +921,13 @@ ' ' Text.Whitespace 'in' Operator.Word ' ' Text.Whitespace -"KeySetView'" Name +'KeySetView"' Name ' ' Text.Whitespace '=' Operator '>' Operator ' ' Text.Whitespace '(' Operator -"b'" Name +'b"' Name '.' Operator 'elts' Name ')' Operator @@ -944,7 +944,7 @@ '=' Operator ' ' Text.Whitespace '(' Operator -"b'" Name +'b"' Name '.' Operator 'elts' Name ')' Operator @@ -953,7 +953,7 @@ ':' Punctuation ' ' Text.Whitespace '(' Operator -"v'" Name +'v"' Name '.' Operator 'map' Name ')' Operator @@ -969,19 +969,19 @@ '=' Operator '>' Operator ' ' Text.Whitespace -"v'" Name +'v"' Name '.' Operator 'elts' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace -"b'" Name +'b"' Name '.' Operator 'left' Name ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace -"b'" Name +'b"' Name '.' Operator 'done' Name '\n' Text.Whitespace @@ -1092,7 +1092,7 @@ ' ' Text.Whitespace '+' Operator ' ' Text.Whitespace -"KeySetView'" Name +'KeySetView"' Name '->' Operator 'setRefs' Name '->' Operator @@ -1370,7 +1370,7 @@ ']' Operator ',' Punctuation ' ' Text.Whitespace -"i'" Name +'i"' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace @@ -1385,7 +1385,7 @@ '\n' Text.Whitespace ' ' Text.Whitespace -"i'" Name +'i"' Name '.' Operator 'left' Name ' ' Text.Whitespace @@ -1397,7 +1397,7 @@ '\n' Text.Whitespace ' ' Text.Whitespace -"i'" Name +'i"' Name '.' Operator 'done' Name ' ' Text.Whitespace @@ -1417,7 +1417,7 @@ ' ' Text.Whitespace 'no' Keyword ' ' Text.Whitespace -"i'" Name +'i"' Name '.' Operator 'lastRef' Name '\n' Text.Whitespace @@ -1510,7 +1510,7 @@ ']' Operator ',' Punctuation ' ' Text.Whitespace -"i'" Name +'i"' Name ' ' Text.Whitespace '=' Operator ' ' Text.Whitespace @@ -1535,7 +1535,7 @@ '\n' Text.Whitespace ' ' Text.Whitespace -"i'" Name +'i"' Name '.' Operator 'left' Name ' ' Text.Whitespace @@ -1551,7 +1551,7 @@ '\n' Text.Whitespace ' ' Text.Whitespace -"i'" Name +'i"' Name '.' Operator 'done' Name ' ' Text.Whitespace @@ -1567,7 +1567,7 @@ '\n' Text.Whitespace ' ' Text.Whitespace -"i'" Name +'i"' Name '.' Operator 'lastRef' Name ' ' Text.Whitespace