diff --git a/.squot b/.squot index ef1ee79..3cb76da 100644 --- a/.squot +++ b/.squot @@ -23,5 +23,6 @@ OrderedDictionary { 'packages/DomainCode-Parser' : #SquotTonelSerializer, 'packages/DomainCode-Core' : #SquotTonelSerializer, 'packages/DomainCode-Diff' : #SquotTonelSerializer, - 'packages/DomainCode-Truediff' : #SquotTonelSerializer + 'packages/DomainCode-Truediff' : #SquotTonelSerializer, + 'packages/Sandblocks-Tlaplus' : #SquotTonelSerializer } \ No newline at end of file diff --git a/packages/DomainCode-Core/CompiledMethod.extension.st b/packages/DomainCode-Core/CompiledMethod.extension.st index 0a1e6d3..ade1943 100644 --- a/packages/DomainCode-Core/CompiledMethod.extension.st +++ b/packages/DomainCode-Core/CompiledMethod.extension.st @@ -3,7 +3,7 @@ Extension { #name : #CompiledMethod } { #category : #'*DomainCode-Core' } CompiledMethod >> openDC: convert [ - + convert do: [DCSmalltalkMethod for: self] ] diff --git a/packages/DomainCode-Core/Morph.extension.st b/packages/DomainCode-Core/Morph.extension.st index bb84cf8..6c4133d 100644 --- a/packages/DomainCode-Core/Morph.extension.st +++ b/packages/DomainCode-Core/Morph.extension.st @@ -55,7 +55,7 @@ Morph >> childCount [ { #category : #'*DomainCode-Core' } Morph >> children [ - ^ submorphs + ^ Array streamContents: [:s | self childrenDo: [:c | s nextPut: c]] ] { #category : #'*DomainCode-Core' } @@ -174,6 +174,12 @@ Morph >> setBoundsDirect: aRectangle [ box = priorBounds ifFalse: [self invalidRect: (priorBounds quickMerge: box)] ] +{ #category : #'*DomainCode-Core' } +Morph >> showInQuery [ + + ^ false +] + { #category : #'*DomainCode-Core' } Morph >> treeSize [ diff --git a/packages/DomainCode-Core/SBTSLanguage.extension.st b/packages/DomainCode-Core/SBTSLanguage.extension.st new file mode 100644 index 0000000..b24637b --- /dev/null +++ b/packages/DomainCode-Core/SBTSLanguage.extension.st @@ -0,0 +1,30 @@ +Extension { #name : #SBTSLanguage } + +{ #category : #'*DomainCode-Core' } +SBTSLanguage class >> grammarRule: aSymbol [ + + ^ self rawGrammar rules at: aSymbol +] + +{ #category : #'*DomainCode-Core' } +SBTSLanguage class >> rawGrammar [ + + ^ RawGrammar ifNil: [RawGrammar := Json readFrom: self grammarJson readStream] +] + +{ #category : #'*DomainCode-Core' } +SBTSLanguage class >> ruleIsInlined: aSymbol [ + + ^ ((self rawGrammar at: #inline) includes: aSymbol) or: [aSymbol first = $_] +] + +{ #category : #'*DomainCode-Core' } +SBTSLanguage class >> supertype: aSymbol includes: anotherSymbol [ + + ^ ((self rawGrammar supertypes includes: aSymbol) or: [self ruleIsInlined: aSymbol]) + ifTrue: [ | nestedRule | + nestedRule := self grammarRule: aSymbol. + nestedRule type = 'CHOICE' ifFalse: [nestedRule := nestedRule content]. + nestedRule members anySatisfy: [:rule | self supertype: (rule name ifNil: [rule content name]) includes: anotherSymbol]] + ifFalse: [aSymbol = anotherSymbol] +] diff --git a/packages/DomainCode-Parser/DCBlock.class.st b/packages/DomainCode-Parser/DCBlock.class.st index 5209c7b..b33d66a 100644 --- a/packages/DomainCode-Parser/DCBlock.class.st +++ b/packages/DomainCode-Parser/DCBlock.class.st @@ -6,7 +6,9 @@ Class { 'language', 'range', 'highlight', - 'field' + 'field', + 'baseChildren', + 'baseParent' ], #category : #'DomainCode-Parser' } @@ -20,20 +22,18 @@ DCBlock class >> addUncapturedTextTo: aNode in: aCursor language: aLanguage isLe text isolateLineBreaks do: [:part | part isEmpty ifFalse: [ part = String cr - ifTrue: [aNode addMorphBack: (DCLineBreak new range: (SBTSRange start: start size: 1))] + ifTrue: [aNode baseAndMorphAdd: (DCLineBreak new range: (SBTSRange start: start size: 1))] ifFalse: [ - aNode addMorphBack: (DCText new + aNode baseAndMorphAdd: (DCText new contents: part; - field: aCursor fieldName; range: (SBTSRange start: start size: part size))]]. start := start + part size]. aCursor advance: text size. aBoolean ifTrue: [ text := aCursor uncapturedText. - aNode addMorphBack: (DCText new + aNode baseAndMorphAdd: (DCText new contents: text; - field: aCursor fieldName; range: aCursor range)] ] @@ -45,10 +45,23 @@ DCBlock class >> cardsCard [ [:x | x language = SBCards]. [:x | x type = #card]. [:x | - x - ensureReplacement: CardsCard - embed: [:g | {g childNodes first}] - initDo: [:g :name | g addMorphBack: name]]} + x ensureReplacement: CardsCardContainer initDo: [:g | + g syncTextFrom: [:source | source childNodes first] to: g card name. + g embedMany: [:s | (s atType: #arguments) namedChildren] onChange: [:list | g card arguments: list]. + g + embedMany: [:source | + source baseChildren + detect: [:c | c type = #resources] + ifFound: [:scope | scope namedChildren] + ifNone: [{}]] + onChange: [:list | g resources: list]. + g + embedMany: [:source | + source baseChildren + detect: [:c | c type = #scope] + ifFound: [:scope | scope namedChildren] + ifNone: [{}]] + onChange: [:list | g scope: list]]]} ] { #category : #cards } @@ -59,13 +72,13 @@ DCBlock class >> cardsGroup [ [:x | x language = SBCards]. [:x | x type = #group]. [:x | - x - ensureReplacement: CardsGroup - embed: [:g | {g childNodes second. (g childNodes viewAllButFirst: 3 andLast: 1) select: [:n | n contents ~= '.']}] - initDo: [:g :name :statements | - g - addMorphBack: name; - addAllMorphsBack: statements]]} + x ensureReplacement: CardsGroup initDo: [:g | + g syncTextFrom: [:source | source childNodes second] to: g name. + g + embedMany: [:s | (s childNodes viewAllButFirst: 3 andLast: 1) select: [:n | n contents ~= '.']] + onChange: [:list | + g submorphs allButFirstDo: #delete. + g addAllMorphsBack: list]]]} ] { #category : #cards } @@ -75,11 +88,20 @@ DCBlock class >> cardsPool [ ^ { [:x | x language = SBCards]. [:x | x type = #pool]. + [:x | x ensureReplacement: CardsPool initDo: [:g | g addMorphBack: (g embed: [:s | s childNodes second])]]} +] + +{ #category : #cards } +DCBlock class >> cardsResources [ + + + ^ { + [:x | x language = SBCards]. + [:x | x type = #identifier and: [x parent type = #resources]]. [:x | x - ensureReplacement: CardsPool - embed: [:g | {g childNodes second}] - initDo: [:g :name | g addMorphBack: name]]} + ensureReplacement: CardsCard + initDo: [:c | c syncTextFrom: [:source | source childNodes first] to: c name]]} ] { #category : #cards } @@ -90,10 +112,10 @@ DCBlock class >> cardsSequence [ [:x | x language = SBCards]. [:x | x type = #sequence]. [:x | - x - ensureReplacement: CardsSequence - embed: [:g | {g children}] - initDo: [:g :cards | g addAllMorphsBack: cards]]} + x ensureReplacement: CardsSequence initDo: [:g | + g embedMany: #namedChildren onChange: [:list | + g removeAllMorphs. + g addAllMorphsBack: list]]]} ] { #category : #'text modify' } @@ -145,7 +167,7 @@ DCBlock class >> fromCursor: aCursor language: aLanguage [ ifTrue: [ [ self addUncapturedTextTo: node in: aCursor language: aLanguage isLeaf: false. - node addMorphBack: (self fromCursor: aCursor language: aLanguage)] doWhileFalse: [aCursor gotoNextSibling]. + node baseAndMorphAdd: (self fromCursor: aCursor language: aLanguage)] doWhileFalse: [aCursor gotoNextSibling]. self addUncapturedTextTo: node in: aCursor language: aLanguage isLeaf: false. aCursor gotoParent] ifFalse: [self addUncapturedTextTo: node in: aCursor language: aLanguage isLeaf: true]. @@ -194,6 +216,45 @@ DCBlock class >> insert: aString in: aContainerString at: aNumber do: aBlock [ value: [:source :block | self deleteFrom: source at: aNumber do: block] ] +{ #category : #javascript } +DCBlock class >> jsExtractTableOfContents: aBlock into: aMorph toc: aReplacement [ + + (aBlock type = #'class_declaration' or: [aBlock type = #'function_declaration']) + ifTrue: [ | container | + container := self jsToCContainer. + container addMorphBack: (aReplacement embed: [:s | aBlock atField: #name]). + + aBlock children do: [:c | self jsExtractTableOfContents: c into: container toc: aReplacement]. + + aMorph addMorphBack: container] + ifFalse: [aBlock children do: [:c | self jsExtractTableOfContents: c into: aMorph toc: aReplacement]] +] + +{ #category : #javascript } +DCBlock class >> jsTableOfContents [ + + + ^ { + [:x | x language = SBJavascript]. + [:x | x type = #program]. + [:x | false]. + [:x | + x + ensureReplacement: DCJsTableOfContents + initDo: [:toc | self jsExtractTableOfContents: x into: toc toc: toc]]} +] + +{ #category : #'as yet unclassified' } +DCBlock class >> jsToCContainer [ + + ^ SBBlock new + layoutPolicy: TableLayout new; + hResizing: #shrinkWrap; + vResizing: #shrinkWrap; + layoutInset: 4; + yourself +] + { #category : #parsing } DCBlock class >> language: aLanguage [ @@ -280,8 +341,8 @@ DCBlock class >> lspShowHover [ DCBlock class >> maybeAddTrailingLineBreak: aBlock [ | last | - last := aBlock lastDeepSubmorph. - aBlock addMorphBack: (DCLineBreak new range: (SBTSRange start: last range end end: last range end + 1)). + last := aBlock lastDeepBaseChild. + aBlock baseAndMorphAdd: (DCLineBreak new range: (SBTSRange start: last range end end: last range end + 1)). ^ aBlock ] @@ -361,19 +422,17 @@ DCBlock class >> smalltalkBabylonianBuildExample [ ^ { + [:x | true]. self smalltalkMessageSendSelector. [:selector :message | selector = #example:args:label:]. [:selector :message | - message - ensureReplacement: DCExample - embed: [:m | {m childNodes third. m childNodes fifth. m childNodes seventh}] - initDo: [:m :selfBlock :argsBlock :label | - m - addMorphBack: label; - addMorphBack: (SBStringMorph new contents: 'self: '); - addMorphBack: selfBlock; - addMorphBack: (SBStringMorph new contents: 'args: '); - addMorphBack: argsBlock]]} + message ensureReplacement: DCExample initDo: [:r | + r + addMorphBack: (r embed: [:s | s childNodes seventh]); + addMorphBack: (SBStringMorph new contents: 'self: '); + addMorphBack: (r embed: [:s | s childNodes third]); + addMorphBack: (SBStringMorph new contents: 'args: '); + addMorphBack: (r embed: [:s | s childNodes fifth])]]} ] { #category : #'smalltalk - helpers' } @@ -382,6 +441,7 @@ DCBlock class >> smalltalkBabylonianExample [ ^ { [:x | x language = SBTSSmalltalk]. [:x | x containingArtefact]. + [:x | x class = DCSmalltalkMethod]. [:x | x method childNodes detect: [:node | node type = #statement and: [node childSandblocks first class = DCExample]] @@ -554,7 +614,7 @@ DCBlock class >> smalltalkCheckbox [ ^ { - [:x | false]. + [:x | true]. [:x | x language = SBTSSmalltalk]. [:x | x isReplacement not]. [:x | {#true. #false} includes: x type]. @@ -649,9 +709,18 @@ DCBlock class >> smalltalkDeclaration [ with: scope]} first: scopes) ifNil: [ (Symbol lookup: id contents) ifNotNil: [:sym | - id containingArtefact methodClass - bindingOf: sym - environment: id containingArtefact methodClass environment]]) ifNil: [id containingArtefact ifNotNil: [:m | m methodClass allInstVarNames detect: [:n | n = id contents] ifNone: [nil]]]. + id containingArtefact class = DCSmalltalkMethod + ifTrue: [ + id containingArtefact methodClass + bindingOf: sym + environment: id containingArtefact methodClass environment] + ifFalse: [nil]]]) ifNil: [ + id containingArtefact class = DCSmalltalkMethod + ifTrue: [ + id containingArtefact methodClass allInstVarNames + detect: [:n | n = id contents] + ifNone: [nil]] + ifFalse: [nil]]. {#args. id. decl}]} ] @@ -740,8 +809,7 @@ DCBlock class >> smalltalkFlagMarker [ [:selector :message | message ensureReplacement: DCFlagMarker - embed: [:m | {m children last}] - initDo: [:m :expr | m addMorphBack: expr]]} + initDo: [:m | m addMorphBack: (m embed: [:s | s children last])]]} ] { #category : #smalltalk } @@ -796,6 +864,7 @@ DCBlock class >> smalltalkIdentifierAutocompletion [ with: id. id]. [:id | {#args. id. id containingArtefact}]. + [:id :method | method class = DCSmalltalkMethod]. [:id :method | id addOwnSuggestions: method methodClass instVarNames label: 'inst var']} ] @@ -1159,7 +1228,7 @@ DCBlock class >> smalltalkVisualSelf [ ^ { - [:x | false]. + [:x | true]. [:x | x language = SBTSSmalltalk]. [:x | x type = 'self']. [:x | x ensureReplacement: DCReplacement initDo: [:r | r addMorphBack: SBIcon iconHeart]]} @@ -1181,13 +1250,14 @@ DCBlock class >> smalltalkWatch [ ifTrue: [message parent] ifFalse: [message]) ensureReplacement: DCWatch - embed: [:w | | expr | - expr := message childNodes third. - { + initDo: [:w | + w addMorphBack: (w embed: [:s | | expr | + expr := (s type = #'parenthesized_expression' + ifTrue: [s childNodes second] + ifFalse: [s]) childNodes third. expr type = 'parenthesized_expression' ifTrue: [expr childNodes second] - ifFalse: [expr]}] - initDo: [:w :expr | w addMorphBack: expr]]} + ifFalse: [expr]])]]} ] { #category : #'text modify' } @@ -1308,6 +1378,13 @@ DCBlock >> adaptInput: input in: source at: cursorIndex textMorph: textMorph eve ^ input ] +{ #category : #'base accessing' } +DCBlock >> addBaseChild: aNode at: aNumber [ + + self baseChildren add: aNode beforeIndex: aNumber. + aNode baseParent: self +] + { #category : #'query actions' } DCBlock >> addOwnSuggestions: aCollection label: aString [ @@ -1326,12 +1403,31 @@ DCBlock >> alias [ ^ nil ] +{ #category : #queries } +DCBlock >> all: aCollection [ + + ^ Array streamContents: [:s | self allBlocksDo: [:b | (DCQuery script: aCollection with: b) ifNotNil: [:res | s nextPut: res]]] +] + { #category : #queries } DCBlock >> all: aCollection do: aBlock [ (self allBlocksSelect: [:b | (DCQuery script: aCollection with: b) notNil]) do: aBlock ] +{ #category : #'base accessing' } +DCBlock >> allBaseChildrenDo: aBlock [ + + self baseChildren do: [:c | c allBaseChildrenDo: aBlock]. + aBlock value: self +] + +{ #category : #'base accessing' } +DCBlock >> allBaseChildrenExceptSelfDo: aBlock [ + + self baseChildren do: [:c | c allBaseChildrenDo: aBlock] +] + { #category : #'as yet unclassified' } DCBlock >> allChildrenDetect: aBlock ifFound: aSuccessBlock ifNone: aFailBlock [ @@ -1429,7 +1525,7 @@ DCBlock >> applyEdit: edit source: newSource cursorAt: newIndex undoDo: aBlock [ DCBlock >> applyEditsIn: newTree to: oldTree [ true ifTrue: [ - oldTree allChildrenDo: [:m | m clearDiffCache]. + oldTree allBaseChildrenDo: [:m | m clearDiffCache]. ^ DCTrueDiff new compare: oldTree to: newTree]. DCMatcher new performEditsIn: newTree to: oldTree ] @@ -1460,12 +1556,94 @@ DCBlock >> assertConsecutiveRanges [ current := m range end index]] ] +{ #category : #'as yet unclassified' } +DCBlock >> atField: aSymbol [ + + ^ self children detect: [:c | c field = aSymbol] +] + +{ #category : #nil } +DCBlock >> atType: aSymbol [ + + ^ self children detect: [:c | c type = aSymbol] +] + +{ #category : #'as yet unclassified' } +DCBlock >> atType: aSymbol ifPresent: aBlock ifAbsent: anotherBlock [ + + ^ self children detect: [:c | c type = aSymbol] ifFound: aBlock ifNone: anotherBlock +] + { #category : #'query actions' } DCBlock >> attachHighlight [ self queryState highlight: self ] +{ #category : #'base accessing' } +DCBlock >> baseAndMorphAdd: aNode [ + + self addMorphBack: aNode. + self addBaseChild: aNode at: self baseChildren size + 1 +] + +{ #category : #'base accessing' } +DCBlock >> baseChildren [ + + ^ baseChildren +] + +{ #category : #'base accessing' } +DCBlock >> baseChildren: aCollection [ + + baseChildren := aCollection +] + +{ #category : #'base accessing' } +DCBlock >> baseMorph [ + + ^ self replacedParent ifNotNil: [:p | p] ifNil: [self] +] + +{ #category : #'base accessing' } +DCBlock >> baseParent [ + + ^ baseParent +] + +{ #category : #'base accessing' } +DCBlock >> baseParent: aNode [ + + baseParent := aNode +] + +{ #category : #'base accessing' } +DCBlock >> baseRemoveFromParent [ + + self baseParent baseChildren remove: self. + self baseParent: nil +] + +{ #category : #'base accessing' } +DCBlock >> baseSiblingIndex [ + + | i | + i := 1. + self baseParent baseChildren do: [:c | + c = self ifTrue: [^ i]. + i := i + 1]. + ^ 0 +] + +{ #category : #'base accessing' } +DCBlock >> baseTreeHeight [ + + ^ self baseChildren size = 0 ifTrue: [0] ifFalse: [ | max | + max := 0. + self baseChildren do: [:c | max := c baseTreeHeight max: max]. + max + 1] +] + { #category : #'as yet unclassified' } DCBlock >> blockFor: aRange [ @@ -1525,10 +1703,8 @@ DCBlock >> children [ { #category : #'as yet unclassified' } DCBlock >> childrenDo: aBlock [ - ^ self submorphs do: [:c | - c isReplacement - ifTrue: [c resolveSource ifNotNil: [:child | aBlock value: child]] - ifFalse: [aBlock value: c]] + ^ self baseChildren do: [:c | + (c replacedParent notNil and: [c replacedParent showInQuery]) ifTrue: [aBlock value: c replacedParent] ifFalse: [aBlock value: c]] ] { #category : #'as yet unclassified' } @@ -1553,6 +1729,14 @@ DCBlock >> clearInput [ self infoForEditDo: [:source :textMorph | self class replace: (self activeTextMorph ifNil: [self]) range in: source with: '' do: self applyBlock] ] +{ #category : #grammar } +DCBlock >> commandForInsert: aNode at: aNumber [ + + | children | + children := self childNodes readStream. + self match: self grammarRule with: children do: [:child :rule | {rule. child}] +] + { #category : #'as yet unclassified' } DCBlock >> compatibleWithType: aSymbol [ @@ -1608,6 +1792,22 @@ DCBlock >> currentTextMorph [ ^ nil ] +{ #category : #'as yet unclassified' } +DCBlock >> cursorPositionsDo: aBlock shallow: aBoolean [ + + true ifTrue: [^ super cursorPositionsDo: aBlock shallow: aBoolean]. + + aBlock value: (SBCursorSelect new block: self). + self match: self grammarRule with: self childNodes readStream do: [:child :rule | + (rule type = 'SYMBOL' or: [rule type = 'ALIAS']) + ifTrue: [aBoolean ifFalse: [child cursorPositionsDo: aBlock shallow: aBoolean]] + ifFalse: [ + (child containingSandblock startInputCommandIn: child) ifNotNil: [:command | + aBlock value: (SBCursorText new + block: child containingSandblock; + currentCommand: command)]]] +] + { #category : #'as yet unclassified' } DCBlock >> deleteAfterCursor [ @@ -1773,6 +1973,12 @@ DCBlock >> grammarHandler [ ^ DCGrammarHandler new ] +{ #category : #grammar } +DCBlock >> grammarRule [ + + ^ (self language grammarRule: self type) ifNil: [self resolveAlias: self type in: self owner grammarRule] +] + { #category : #'as yet unclassified' } DCBlock >> handleInsertEvent: anEvent in: textMorph [ @@ -1893,6 +2099,8 @@ DCBlock >> initialize [ super initialize. range := SBTSRange null. + baseParent := nil. + baseChildren := OrderedCollection new: 1. self layoutPolicy: DCLayout new; @@ -2155,6 +2363,10 @@ DCBlock >> isTSMorph [ { #category : #'as yet unclassified' } DCBlock >> keyStroke: anEvent [ + | editor artefact | + editor := self sandblockEditor. + artefact := self containingArtefact. + self infoForEditDo: [:source :textMorph :cursorIndex | | input | input := anEvent keyCharacter asString. (input first isPrintable and: [anEvent commandKeyPressed not]) ifTrue: [ @@ -2164,7 +2376,7 @@ DCBlock >> keyStroke: anEvent [ in: source at: cursorIndex + 1 do: (self applyBlockWithCursor: cursorIndex + (text indexOf: anEvent keyCharacter))]]]. - self batchedChangeStep + editor batchedChangeStep: artefact ] { #category : #'as yet unclassified' } @@ -2179,6 +2391,15 @@ DCBlock >> language: aLanguage [ language := aLanguage ] +{ #category : #'base accessing' } +DCBlock >> lastDeepBaseChild [ + + | current | + current := self. + [current baseChildren isEmpty] whileFalse: [current := current baseChildren last]. + ^ current +] + { #category : #'as yet unclassified' } DCBlock >> layoutCommands [ @@ -2201,6 +2422,80 @@ DCBlock >> layoutInset [ ^ 2 @ (self submorphCount > 3 ifTrue: [2] ifFalse: [0]) ] +{ #category : #'as yet unclassified' } +DCBlock >> match: aRule with: aStream do: aBlock [ + + ^ aRule type caseOf: { + ['STRING'] -> [ + aRule value = aStream peek contents + ifTrue: [ + aBlock value: aStream next value: aRule. + true] + ifFalse: [false]]. + ['TOKEN'] -> [ + " TODO match contents" + aStream peek class = DCText + ifTrue: [ + aBlock value: aStream next value: aRule. + true] + ifFalse: [false]]. + ['IMMEDIATE_TOKEN'] -> [ + " TODO match contents" + aStream peek class = DCText + ifTrue: [ + aBlock value: aStream next value: aRule. + true] + ifFalse: [false]]. + ['PATTERN'] -> [ + " TODO match contents" + aStream peek class = DCText + ifTrue: [ + aBlock value: aStream next value: aRule. + true] + ifFalse: [false]]. + ['SYMBOL'] -> [ + (self language ruleIsInlined: aRule name) + ifTrue: [ + self + match: ((self language grammarRule: aRule name) ifNil: ["TODO external symbols" + JsonObject fromAssociations: {'type' -> 'BLANK'}]) + with: aStream + do: aBlock] + ifFalse: [ + (self language supertype: aRule name includes: aStream peek type) + ifTrue: [ + aBlock value: aStream next value: aRule. + true] + ifFalse: [false]]]. + ['ALIAS'] -> [ + (self language supertype: aRule value includes: aStream peek type) + ifTrue: [ + aBlock value: aStream next value: aRule. + true] + ifFalse: [false]]. + ['SEQ'] -> [aRule members allSatisfy: [:childRule | self match: childRule with: aStream do: aBlock]]. + ['PREC_LEFT'] -> [self match: aRule content with: aStream do: aBlock]. + ['PREC_RIGHT'] -> [self match: aRule content with: aStream do: aBlock]. + ['PREC'] -> [self match: aRule content with: aStream do: aBlock]. + ['PREC_DYNAMIC'] -> [self match: aRule content with: aStream do: aBlock]. + ['FIELD'] -> [self match: aRule content with: aStream do: aBlock]. + ['CHOICE'] -> [ + aRule members + detect: [:childRule | self match: childRule with: aStream copy do: [:child :rule | ]] + ifFound: [:childRule | self match: childRule with: aStream do: aBlock] + ifNone: [false]]. + ['BLANK'] -> [true]. + ['REPEAT'] -> [ + [aStream atEnd not and: [self match: aRule content with: aStream do: aBlock]] whileTrue. + true]. + ['REPEAT1'] -> [ + (self match: aRule content with: aStream do: aBlock) + ifTrue: [ + [aStream atEnd not and: [self match: aRule content with: aStream do: aBlock]] whileTrue. + true] + ifFalse: [false]]} +] + { #category : #'as yet unclassified' } DCBlock >> maybeAddSeparator: input textMorph: aTextMorph [ @@ -2216,6 +2511,12 @@ DCBlock >> minBoundsWith: info [ ^ info bounds ] +{ #category : #'as yet unclassified' } +DCBlock >> namedChildren [ + + ^ self children select: [:c | c type notEmpty] +] + { #category : #'as yet unclassified' } DCBlock >> nonExtraChildrenBounds [ @@ -2309,9 +2610,7 @@ DCBlock >> pairMap [ { #category : #hierarchy } DCBlock >> parent [ - ^ self replacedParent - ifNotNil: [:p | p parent ifNotNil: #source] - ifNil: [self parentSandblock] + ^ (self owner ifNotNil: [:o | o showInQuery] ifNil: [false]) ifTrue: [self owner] ifFalse: [self baseParent] ] { #category : #'as yet unclassified' } @@ -2570,10 +2869,19 @@ DCBlock >> reportError: anError [ self queryState reportError: anError for: self ] -{ #category : #'as yet unclassified' } -DCBlock >> resolveSource [ +{ #category : #grammar } +DCBlock >> resolveAlias: aSymbol in: aNode [ - ^ self + (aNode type = 'ALIAS' and: [(aNode at: #value) = aSymbol]) ifTrue: [ + ^ aNode content type = 'SYMBOL' + ifTrue: [self language grammarRule: aNode content name] + ifFalse: [aNode content]]. + + aNode members ifNotNil: [aNode members do: [:m | (self resolveAlias: aSymbol in: m) ifNotNil: [:g | ^ g]]]. + + aNode content ifNotNil: [^ self resolveAlias: aSymbol in: aNode content]. + + ^ nil ] { #category : #'as yet unclassified' } @@ -2600,7 +2908,10 @@ DCBlock >> restoreCursorAfter: aBlock [ { #category : #'as yet unclassified' } DCBlock >> rootBlock [ - ^ self orAnyParent: self language rootRuleName + | current | + current := self. + [current isRootBlock] whileFalse: [current := current baseParent]. + ^ current ] { #category : #queries } @@ -2667,6 +2978,12 @@ DCBlock >> shallowCopyBlock [ highlight: highlight ] +{ #category : #'as yet unclassified' } +DCBlock >> showInQuery [ + + ^ true +] + { #category : #hierarchy } DCBlock >> siblingIndex [ diff --git a/packages/DomainCode-Parser/DCEmbedMarker.class.st b/packages/DomainCode-Parser/DCEmbedMarker.class.st index 119ec13..c271da6 100644 --- a/packages/DomainCode-Parser/DCEmbedMarker.class.st +++ b/packages/DomainCode-Parser/DCEmbedMarker.class.st @@ -30,12 +30,6 @@ DCEmbedMarker >> parent [ ^ self owner ] -{ #category : #'as yet unclassified' } -DCEmbedMarker >> printOn [ - - -] - { #category : #'as yet unclassified' } DCEmbedMarker >> printOn: aStream [ @@ -44,12 +38,6 @@ DCEmbedMarker >> printOn: aStream [ aStream nextPut: $) ] -{ #category : #'as yet unclassified' } -DCEmbedMarker >> resolveSource [ - - ^ self source resolveSource -] - { #category : #'as yet unclassified' } DCEmbedMarker >> siblingIndex [ diff --git a/packages/DomainCode-Parser/DCJsTableOfContents.class.st b/packages/DomainCode-Parser/DCJsTableOfContents.class.st new file mode 100644 index 0000000..3bdfa53 --- /dev/null +++ b/packages/DomainCode-Parser/DCJsTableOfContents.class.st @@ -0,0 +1,16 @@ +Class { + #name : #DCJsTableOfContents, + #superclass : #DCReplacement, + #category : #'DomainCode-Parser' +} + +{ #category : #'as yet unclassified' } +DCJsTableOfContents >> initialize [ + + super initialize. + + self + layoutPolicy: TableLayout new; + listDirection: #topToBottom; + layoutInset: 4 +] diff --git a/packages/DomainCode-Parser/DCLineBreak.class.st b/packages/DomainCode-Parser/DCLineBreak.class.st index 96ba87e..1b6d9d3 100644 --- a/packages/DomainCode-Parser/DCLineBreak.class.st +++ b/packages/DomainCode-Parser/DCLineBreak.class.st @@ -61,5 +61,5 @@ DCLineBreak >> treeLabel [ { #category : #'as yet unclassified' } DCLineBreak >> type [ - ^ '' + ^ '' ] diff --git a/packages/DomainCode-Parser/DCQueryState.class.st b/packages/DomainCode-Parser/DCQueryState.class.st index ee9c5b6..0ac9183 100644 --- a/packages/DomainCode-Parser/DCQueryState.class.st +++ b/packages/DomainCode-Parser/DCQueryState.class.st @@ -112,9 +112,6 @@ DCQueryState >> atData: aSymbol put: anObject [ DCQueryState >> ensureReplacement: aClass for: aBlock embed: aClosure initDo: anotherClosure [ | replacement | - " do not replace off-screen nodes " - aBlock sandblockEditor ifNil: [^ self]. - replacement := (aBlock class = aClass or: [(aBlock replacedParent ifNotNil: #class) = aClass]) ifFalse: [ | r hadFocus | hadFocus := (aBlock sandblockEditor ifNotNil: #textFocus) @@ -122,18 +119,16 @@ DCQueryState >> ensureReplacement: aClass for: aBlock embed: aClosure initDo: an ifNil: [false]. r := aClass new. - aBlock replaceNodeBy: r. + aBlock replaceBy: r. aBlock replacedParent: r. - r - source: aBlock; - embed: aClosure. - anotherClosure valueWithArguments: {r}, r updateEmbeds. + r source: aBlock. + anotherClosure valueWithArguments: {r}. hadFocus ifTrue: [r startInputAtEnd]. r updateReplacement. r] ifTrue: [ | r | r := aBlock class = aClass ifFalse: [aBlock replacedParent] ifTrue: [aBlock]. - r updateEmbeds. + r updateReplacement. r]. (transientReplacements at: currentTrigger) add: replacement ] diff --git a/packages/DomainCode-Parser/DCReplacement.class.st b/packages/DomainCode-Parser/DCReplacement.class.st index 7638e8c..0d2c0d4 100644 --- a/packages/DomainCode-Parser/DCReplacement.class.st +++ b/packages/DomainCode-Parser/DCReplacement.class.st @@ -48,31 +48,12 @@ DCReplacement >> activeUninstall [ self source startInputAtEnd ] -{ #category : #'as yet unclassified' } -DCReplacement >> addEmbed: aBlock [ - - currentEmbeds ifNil: [currentEmbeds := OrderedCollection new]. - - ^ currentEmbeds add: (aBlock = self source - ifFalse: [ | marker | - marker := DCEmbedMarker new source: aBlock. - aBlock replaceNodeBy: marker. - aBlock] - ifTrue: [ - self assert: aBlock replacedParent = self. - aBlock]) -] - -{ #category : #'as yet unclassified' } -DCReplacement >> children [ - - ^ self source ifNotNil: #children ifNil: [#()] -] - { #category : #'as yet unclassified' } DCReplacement >> childrenDo: aBlock [ - ^ self source ifNotNil: [:s | s childrenDo: aBlock] + self hasType + ifTrue: [currentEmbeds do: aBlock] + ifFalse: [self source baseChildren do: aBlock] ] { #category : #'as yet unclassified' } @@ -88,20 +69,38 @@ DCReplacement >> currentTextMorph [ ^ nil ] -{ #category : #'as yet unclassified' } -DCReplacement >> deleteBlock [ - +{ #category : #binding } +DCReplacement >> embed: aBlock [ - self source deleteBlock + | shard | + shard := DCShard new. + self + fromSource: [:source :repl | | block | + block := aBlock value: source. + shard update: block. + currentEmbeds add: block] + toSource: [:source :repl | ]. + ^ shard ] -{ #category : #'as yet unclassified' } -DCReplacement >> embed: aClosure [ +{ #category : #binding } +DCReplacement >> embedMany: aBlock onChange: anotherBlock [ - collectEmbeds := aClosure + | shard current | + shard := DCShard new. + current := nil. + self + fromSource: [:source :repl | | new | + new := (aBlock value: source) collect: #baseMorph. + new do: [:block | currentEmbeds add: block]. + current = new ifFalse: [ + anotherBlock value: new. + current := new]] + toSource: [:source :repl | ]. + ^ shard ] -{ #category : #'as yet unclassified' } +{ #category : #binding } DCReplacement >> fromSource: aBlock toSource: anotherBlock [ bindings add: aBlock -> anotherBlock @@ -114,6 +113,12 @@ DCReplacement >> gapFor: aMorph [ ^ nil ] +{ #category : #'as yet unclassified' } +DCReplacement >> hasType [ + + ^ self type notEmpty +] + { #category : #'as yet unclassified' } DCReplacement >> initialize [ @@ -138,10 +143,16 @@ DCReplacement >> isReplacement [ ^ true ] +{ #category : #'block api' } +DCReplacement >> isRootBlock [ + + ^ self source isRootBlock +] + { #category : #'as yet unclassified' } DCReplacement >> language [ - ^ language + ^ self source language ] { #category : #'as yet unclassified' } @@ -169,7 +180,7 @@ DCReplacement >> passiveUninstall [ hadFocus := self sandblockEditor textFocus ifNotNil: [:t | (t ownerSatisfying: [:o | o = self]) notNil] ifNil: [false]. - self source ifNotNil: [self replaceNodeBy: self source] ifNil: [self delete]. + self source ifNotNil: [self replaceBy: self source] ifNil: [self delete]. hadFocus ifTrue: [self source startInputAtEnd] ] @@ -220,15 +231,17 @@ DCReplacement >> range [ ] { #category : #'as yet unclassified' } -DCReplacement >> resolveSource [ +DCReplacement >> rootBlock [ - ^ self source ifNotNil: [:c | c resolveSource] + source isRootBlock ifTrue: [^ source]. + + ^ self ownerSatisfying: [:b | b isTSMorph and: [b type = self language rootRuleName]] ] { #category : #'as yet unclassified' } -DCReplacement >> rootBlock [ +DCReplacement >> showInQuery [ - ^ self ownerSatisfying: [:b | b isTSMorph and: [b type = self language rootRuleName]] + ^ self hasType ] { #category : #'as yet unclassified' } @@ -251,6 +264,17 @@ DCReplacement >> source: aBlock [ self language: aBlock language ] +{ #category : #binding } +DCReplacement >> syncTextFrom: aClosure to: aTextBlock [ + + self + fromSource: [:source :repl | aTextBlock contents: (aClosure value: source) contents] + toSource: [:source :repl | ]. + aTextBlock + when: #keyStroke + evaluate: [:e | (aClosure value: self source) replaceWith: aTextBlock contents] +] + { #category : #'as yet unclassified' } DCReplacement >> treeHash [ @@ -272,40 +296,13 @@ DCReplacement >> type [ { #category : #'as yet unclassified' } DCReplacement >> uninstallEmbeds [ - currentEmbeds ifNotNil: [:e | e do: [:embed | embed = self source ifFalse: [embed replacedParent uninstall]]] -] - -{ #category : #'as yet unclassified' } -DCReplacement >> updateEmbeds [ - - | newEmbeds collected | - collected := collectEmbeds value: self source. - newEmbeds := collected flatten. - currentEmbeds - ifNil: [ - newEmbeds do: [:embed | self addEmbed: embed]. - currentEmbeds ifNil: [currentEmbeds := {}]] - ifNotNil: [ - newEmbeds do: [:e | - self - assert: e class ~= DCEmbedMarker - description: 'use children to navigate the tree for embedding (selected marker block)']. - - (currentEmbeds copyWithoutAll: newEmbeds) do: [:gone | gone replacedParent uninstall]. - - (newEmbeds copyWithoutAll: currentEmbeds) do: [:new | | marker | - marker := DCEmbedMarker new source: new. - new replaceNodeBy: marker. - self addMorphBack: new]. - - currentEmbeds := newEmbeds]. - - ^ collected + currentEmbeds ifNotNil: [:e | e do: [:embed | embed source ifNotNil: [:source | source baseParent addMorph: source asElementNumber: embed baseSiblingIndex]]] ] { #category : #'as yet unclassified' } DCReplacement >> updateReplacement [ + currentEmbeds := OrderedCollection new. bindings do: [:assoc | assoc key value: self source value: self] ] @@ -314,16 +311,3 @@ DCReplacement >> updateSource [ bindings do: [:assoc | assoc value value: self source value: self] ] - -{ #category : #'as yet unclassified' } -DCReplacement >> updateSourceDuring: aBlock [ - - bindings do: [:assoc | assoc value value: self source value: self]. - aBlock value -] - -{ #category : #'as yet unclassified' } -DCReplacement >> writeSourceOn: aStream indent: aNumber forCompare: aBoolean [ - - self updateSourceDuring: [self source writeSourceOn: aStream indent: aNumber forCompare: aBoolean] -] diff --git a/packages/DomainCode-Parser/DCReplacementTest.class.st b/packages/DomainCode-Parser/DCReplacementTest.class.st index 68ecdfa..c82bcc5 100644 --- a/packages/DomainCode-Parser/DCReplacementTest.class.st +++ b/packages/DomainCode-Parser/DCReplacementTest.class.st @@ -8,7 +8,7 @@ Class { DCReplacementTest >> parse: aString withQueries: aCollection do: aBlock [ | root editor | - root := DCBlock parseBlock: aString language: SBJavascript. + root := DCBlock parse: aString language: SBJavascript. root queryState querySourceOverride: [:type :block | aCollection do: [:assoc | assoc key = type ifTrue: [block value: assoc value]]]. editor := self editorAndWorldFor: root. self tick. @@ -26,8 +26,7 @@ DCReplacementTest >> testEditEmbeddedChild [ [:x | x ensureReplacement: DCTestReplacement - embed: [:w | {w children second}] - initDo: [:w :num | w addMorphBack: num]]}} + initDo: [:w | w addMorphBack: (w embed: [:s | s children second])]]}} do: [:block :editor | | replacement | editor selection firstDeepChild startInputAtEnd. editor performForSelection: #moveCursorLeft. @@ -42,11 +41,9 @@ DCReplacementTest >> testEditEmbeddedChild [ assert: '2+3' equals: block children first children first children second generatedSourceString. - self assert: #'binary_expression' equals: replacement firstSubmorph type. - self assert: DCBlock equals: replacement firstSubmorph class. - - self assert: DCEmbedMarker equals: replacement firstSubmorph replacedParent class. - self assert: #'parenthesized_expression' equals: replacement firstSubmorph parent type] + self assert: #'binary_expression' equals: replacement firstSubmorph source type. + self assert: DCShard equals: replacement firstSubmorph class. + self assert: DCBlock equals: replacement firstSubmorph firstSubmorph class] ] { #category : #'as yet unclassified' } @@ -57,7 +54,7 @@ DCReplacementTest >> testEditEmbeddedRoot [ withQueries: { #always -> { [:x | x type = #number]. - [:x | x ensureReplacement: DCTestReplacement embed: [:w | {w}] initDo: [:w :num | w addMorphBack: num]]}} + [:x | x ensureReplacement: DCTestReplacement initDo: [:w | w addMorphBack: (w embed: [:s | s])]]}} do: [:block :editor | | replacement | editor selection firstDeepChild startInputAtEnd. editor handle: (SBTest keyboardEvent: $3). @@ -67,8 +64,7 @@ DCReplacementTest >> testEditEmbeddedRoot [ self assert: #number equals: block children first children first type. self assert: '23' equals: block children first children first contents. - self assert: DCBlock equals: replacement firstSubmorph class. - self assert: replacement equals: replacement firstSubmorph replacedParent] + self assert: DCShard equals: replacement firstSubmorph class] ] { #category : #'as yet unclassified' } @@ -103,19 +99,17 @@ DCReplacementTest >> testPassiveReplacementWithChildEmbed [ [:x | x ensureReplacement: DCTestReplacement - embed: [:w | {w children second}] - initDo: [:w :num | w addMorphBack: num]]}} + initDo: [:w | w addMorphBack: (w embed: [:s | s children second])]]}} do: [:block :editor | | replacement | replacement := block childSandblocks first childSandblocks first. self assert: DCTestReplacement equals: replacement class. self assert: #'parenthesized_expression' equals: block children first children first type. self assert: #number equals: block children first children first children second type. - self assert: #number equals: replacement firstSubmorph type. - self assert: DCBlock equals: replacement firstSubmorph class. + self assert: #number equals: replacement firstSubmorph firstSubmorph type. + self assert: DCBlock equals: replacement firstSubmorph firstSubmorph class. - self assert: DCEmbedMarker equals: replacement firstSubmorph replacedParent class. - self assert: #'parenthesized_expression' equals: replacement firstSubmorph parent type] + self assert: DCShard equals: replacement firstSubmorph class] ] { #category : #'as yet unclassified' } @@ -126,14 +120,30 @@ DCReplacementTest >> testPassiveReplacementWithRootEmbed [ withQueries: { #always -> { [:x | x type = #number]. - [:x | x ensureReplacement: DCTestReplacement embed: [:w | {w}] initDo: [:w :num | w addMorphBack: num]]}} + [:x | x ensureReplacement: DCTestReplacement initDo: [:w | w addMorphBack: (w embed: [:s | s])]]}} do: [:block :editor | | replacement | replacement := block childSandblocks first childSandblocks first. self assert: DCTestReplacement equals: replacement class. self assert: #number equals: block children first children first type. - self assert: DCBlock equals: replacement firstSubmorph class. - self assert: replacement equals: replacement firstSubmorph replacedParent] + self assert: DCShard equals: replacement firstSubmorph class] +] + +{ #category : #'as yet unclassified' } +DCReplacementTest >> testUninstallAfterTypeChange [ + + self + parse: ';2' + withQueries: { + #always -> { + [:x | x type = #number]. + [:x | x ensureReplacement: DCTestReplacement initDo: [:w | w addMorphBack: SBIcon iconAt]]}} + do: [:block :editor | + editor selection firstDeepChild startInputAtEnd. + editor handle: (SBTest keyboardEvent: $a). + self tick. + + self assert: 'a2' equals: block children second children first contents] ] { #category : #'as yet unclassified' } @@ -148,8 +158,7 @@ DCReplacementTest >> testUninstallWithEmbeddedChild [ [:x | x ensureReplacement: DCTestReplacement - embed: [:w | {w children second}] - initDo: [:w :num | w addMorphBack: num]]}} + initDo: [:w :num | w addMorphBack: (w embed: [:s | s children second])]]}} do: [:block :editor | | replacement | editor selection firstDeepChild startInputAtStart. editor handle: (SBTest keyboardEvent: $a). @@ -171,7 +180,7 @@ DCReplacementTest >> testUninstallWithEmbeddedRoot [ withQueries: { #always -> { [:x | x type = #number]. - [:x | x ensureReplacement: DCTestReplacement embed: [:w | {w}] initDo: [:w :num | w addMorphBack: num]]}} + [:x | x ensureReplacement: DCTestReplacement initDo: [:w | w addMorphBack: (w embed: [:s | s])]]}} do: [:block :editor | | replacement | editor selection firstDeepChild startInputAtStart. editor handle: (SBTest keyboardEvent: $a). diff --git a/packages/DomainCode-Parser/DCShard.class.st b/packages/DomainCode-Parser/DCShard.class.st new file mode 100644 index 0000000..71ec6da --- /dev/null +++ b/packages/DomainCode-Parser/DCShard.class.st @@ -0,0 +1,38 @@ +Class { + #name : #DCShard, + #superclass : #SBBlock, + #category : #'DomainCode-Parser' +} + +{ #category : #'as yet unclassified' } +DCShard >> initialize [ + + super initialize. + + self + layoutPolicy: TableLayout new; + hResizing: #shrinkWrap; + vResizing: #shrinkWrap +] + +{ #category : #'as yet unclassified' } +DCShard >> printOn: aStream [ + + aStream nextPutAll: 'Shard('. + aStream print: self source. + aStream nextPut: $) +] + +{ #category : #'as yet unclassified' } +DCShard >> source [ + + ^ self hasSubmorphs ifTrue: [self firstSubmorph] ifFalse: [nil] +] + +{ #category : #'as yet unclassified' } +DCShard >> update: aBlock [ + + self hasSubmorphs + ifFalse: [self addMorph: aBlock] + ifTrue: [aBlock = self source ifFalse: [self source replaceBy: aBlock]] +] diff --git a/packages/DomainCode-Parser/DCSmalltalkMethod.class.st b/packages/DomainCode-Parser/DCSmalltalkMethod.class.st index 64231ee..b8b38c8 100644 --- a/packages/DomainCode-Parser/DCSmalltalkMethod.class.st +++ b/packages/DomainCode-Parser/DCSmalltalkMethod.class.st @@ -204,6 +204,14 @@ DCSmalltalkMethod >> object [ ifAbsent: [self] ] +{ #category : #'as yet unclassified' } +DCSmalltalkMethod >> outOfWorld: aWorld [ + + super outOfWorld: aWorld. + + SystemChangeNotifier uniqueInstance noMoreNotificationsFor: self +] + { #category : #'as yet unclassified' } DCSmalltalkMethod >> relatedClass [ @@ -262,8 +270,14 @@ DCSmalltalkMethod >> selector [ ^ (((selector childSandblocks viewFrom: 1 by: 2) collect: [:p | p contents]) joinSeparatedBy: '') asSymbol ] +{ #category : #'as yet unclassified' } +DCSmalltalkMethod >> showInQuery [ + + ^ true +] + { #category : #'as yet unclassified' } DCSmalltalkMethod >> type [ - ^ nil + ^ 'smalltalk_method' ] diff --git a/packages/DomainCode-Parser/DCText.class.st b/packages/DomainCode-Parser/DCText.class.st index a9cdc1c..fb414e9 100644 --- a/packages/DomainCode-Parser/DCText.class.st +++ b/packages/DomainCode-Parser/DCText.class.st @@ -4,7 +4,8 @@ Class { #instVars : [ 'range', 'highlight', - 'field' + 'field', + 'baseParent' ], #category : #'DomainCode-Parser' } @@ -15,12 +16,72 @@ DCText >> alias [ ^ nil ] +{ #category : #'base accessing' } +DCText >> allBaseChildrenDo: aBlock [ + + aBlock value: self +] + +{ #category : #'base accessing' } +DCText >> allBaseChildrenExceptSelfDo: aBlock [ + + +] + { #category : #hierarchy } DCText >> allParentsUpTo: aBlock [ ^ {self parent}, (self parent allParentsUpTo: aBlock) ] +{ #category : #'base accessing' } +DCText >> baseChildren [ + + ^ #() +] + +{ #category : #'base accessing' } +DCText >> baseMorph [ + + ^ self replacedParent ifNotNil: [:p | p baseMorph] ifNil: [self] +] + +{ #category : #'base accessing' } +DCText >> baseParent [ + + ^ baseParent +] + +{ #category : #'base accessing' } +DCText >> baseParent: aNode [ + + baseParent := aNode +] + +{ #category : #'base accessing' } +DCText >> baseRemoveFromParent [ + + self parent baseChildren remove: self. + self baseParent: nil +] + +{ #category : #'base accessing' } +DCText >> baseSiblingIndex [ + + | i | + i := 1. + self baseParent baseChildren do: [:c | + c = self ifTrue: [^ i]. + i := i + 1]. + ^ 0 +] + +{ #category : #'as yet unclassified' } +DCText >> baseTreeHeight [ + + ^ 0 +] + { #category : #'as yet unclassified' } DCText >> childrenDo: aBlock [ ] @@ -115,7 +176,9 @@ DCText >> initialize [ super initialize. - range := SBTSRange null + range := SBTSRange null. + self hResizing: #shrinkWrap. + self vResizing: #shrinkWrap ] { #category : #'as yet unclassified' } @@ -189,7 +252,7 @@ DCText >> ownerWithForegroundColor [ { #category : #'as yet unclassified' } DCText >> parent [ - ^ self replacedParent ifNotNil: [:p | p isReplacement ifTrue: [p owner] ifFalse: [p]] ifNil: [self parentSandblock] + ^ self owner showInQuery ifTrue: [self owner] ifFalse: [self baseParent] ] { #category : #'as yet unclassified' } @@ -239,12 +302,6 @@ DCText >> range: aRange [ range := aRange ] -{ #category : #'as yet unclassified' } -DCText >> resolveSource [ - - ^ self -] - { #category : #'as yet unclassified' } DCText >> rootBlock [ @@ -261,6 +318,12 @@ DCText >> shallowCopyBlock [ field: field ] +{ #category : #'as yet unclassified' } +DCText >> showInQuery [ + + ^ true +] + { #category : #'as yet unclassified' } DCText >> shownColor [ diff --git a/packages/DomainCode-Truediff/DCBlock.extension.st b/packages/DomainCode-Truediff/DCBlock.extension.st index 87ecb96..8fbe7dc 100644 --- a/packages/DomainCode-Truediff/DCBlock.extension.st +++ b/packages/DomainCode-Truediff/DCBlock.extension.st @@ -24,7 +24,7 @@ DCBlock >> literalHash [ ^ self valueOfProperty: #literalHash - ifAbsentPut: [self children inject: 0 into: [:compound :node | compound + node literalHash]] + ifAbsentPut: [self baseChildren inject: 0 into: [:compound :node | compound + node literalHash]] ] { #category : #'*DomainCode-TrueDiff' } @@ -58,7 +58,7 @@ DCBlock >> structureHash [ ^ self valueOfProperty: #structureHash ifAbsentPut: [ | writer | writer := #[] writeStream. writer nextPutAll: self type. - self children do: [:c | writer nextLittleEndianNumber: 4 put: c structureHash]. + self baseChildren do: [:c | writer nextLittleEndianNumber: 4 put: c structureHash]. SecureHashAlgorithm new hashStream: writer contents readStream] ] diff --git a/packages/DomainCode-Truediff/DCEditBuffer.class.st b/packages/DomainCode-Truediff/DCEditBuffer.class.st index d1b61ff..5caa442 100644 --- a/packages/DomainCode-Truediff/DCEditBuffer.class.st +++ b/packages/DomainCode-Truediff/DCEditBuffer.class.st @@ -16,24 +16,25 @@ DCEditBuffer >> apply [ posBuf do: [:b | b value] ] -{ #category : #'as yet unclassified' } +{ #category : #operations } DCEditBuffer >> attach: aNode to: aParentNode at: aNumber [ self assert: aNode ~~ aParentNode. + self assert: aNumber >= 1. posBuf add: [ - aParentNode ifNotNil: [ | target | - target := aNode replacedParent ifNil: [aNode]. - aParentNode addMorph: target asElementNumber: aNumber]]. + aParentNode ifNotNil: [ + aParentNode addBaseChild: aNode at: aNumber. + aParentNode addMorph: aNode baseMorph asElementNumber: aNumber]]. self logChanges: {#attach. aNode. aParentNode. aNumber} ] -{ #category : #'as yet unclassified' } +{ #category : #operations } DCEditBuffer >> detach: aNode [ - negBuf add: [ | target | - target := aNode replacedParent ifNil: [aNode]. - target delete]. - detachListNext add: {aNode parent -> aNode}. + negBuf add: [ + aNode baseRemoveFromParent. + aNode replacedParent ifNotNil: #delete ifNil: [aNode delete]]. + detachListNext add: {aNode baseParent -> aNode}. self logChanges: {#detach. aNode} ] @@ -50,18 +51,18 @@ DCEditBuffer >> initialize [ { #category : #'as yet unclassified' } DCEditBuffer >> logChanges: aCollection [ - true ifTrue: [Transcript showln: aCollection] + false ifTrue: [Transcript showln: aCollection] ] -{ #category : #'as yet unclassified' } +{ #category : #operations } DCEditBuffer >> remove: aNode [ + "used to deallocate deattached children, gc does that for us" - negBuf add: ["aNode replacedParent ifNotNil: [:p | p isReplacement ifTrue: [p queryState replacementDeleted: p]]" - ]. + negBuf add: []. self logChanges: {#remove. aNode} ] -{ #category : #'as yet unclassified' } +{ #category : #operations } DCEditBuffer >> update: aNode to: aString [ posBuf add: [aNode contents: aString]. diff --git a/packages/DomainCode-Truediff/DCSubtreeShare.class.st b/packages/DomainCode-Truediff/DCSubtreeShare.class.st index 9a6b274..87694e4 100644 --- a/packages/DomainCode-Truediff/DCSubtreeShare.class.st +++ b/packages/DomainCode-Truediff/DCSubtreeShare.class.st @@ -21,12 +21,12 @@ DCSubtreeShare >> deregisterAvailableTree: aNode subtreeReg: aRegistry [ ifNotNil: [ aNode share availableTrees removeKey: aNode uri. aNode share: nil. - aNode children do: [:t | self deregisterAvailableTree: t subtreeReg: aRegistry]] + aNode baseChildren do: [:t | self deregisterAvailableTree: t subtreeReg: aRegistry]] ifNil: [ aNode assigned ifNotNil: [ | that | that := aNode assigned. aNode unassignTree. - that allChildrenDo: [:t | aRegistry assignShare: t]]] + that allBaseChildrenDo: [:t | aRegistry assignShare: t]]] ] { #category : #'as yet unclassified' } @@ -71,8 +71,8 @@ DCSubtreeShare >> takeTree: aNode that: anotherNode subtreeReg: aRegistry [ aNode share availableTrees removeKey: aNode uri. aNode share hasPreferredTrees ifTrue: [aNode share preferredTrees removeKey: aNode literalHash ifAbsent: []]. aNode share: nil. - aNode children do: [:t | self deregisterAvailableTree: t subtreeReg: aRegistry]. - anotherNode onlyChildrenDo: [:thatNode | + aNode baseChildren do: [:t | self deregisterAvailableTree: t subtreeReg: aRegistry]. + anotherNode allBaseChildrenExceptSelfDo: [:thatNode | thatNode assigned ifNotNil: [ | thisNode | thisNode := thatNode assigned. aRegistry assignShareAndRegisterTree: thisNode]]. diff --git a/packages/DomainCode-Truediff/DCTrueDiff.class.st b/packages/DomainCode-Truediff/DCTrueDiff.class.st index 297f828..a1abf63 100644 --- a/packages/DomainCode-Truediff/DCTrueDiff.class.st +++ b/packages/DomainCode-Truediff/DCTrueDiff.class.st @@ -33,15 +33,15 @@ DCTrueDiff >> assignSharesListFrom: thisList to: thatList subtreeReg: aRegistry { #category : #'as yet unclassified' } DCTrueDiff >> assignSharesRecurseFrom1: this to: that subtreeReg: aRegistry [ - (this type = that type and: [this children size = that children size]) + (this type = that type and: [this baseChildren size = that baseChildren size]) ifTrue: [ this share registerAvailableTree: this. - this children - with: that children + this baseChildren + with: that baseChildren do: [:l :r | self assignSharesFrom: l to: r subtreeReg: aRegistry]] ifFalse: [ - this allChildrenDo: [:c | aRegistry assignShareAndRegisterTree: c]. - that onlyChildrenDo: [:c | aRegistry assignShare: c]] + this allBaseChildrenDo: [:c | aRegistry assignShareAndRegisterTree: c]. + that allBaseChildrenExceptSelfDo: [:c | aRegistry assignShare: c]] ] { #category : #'as yet unclassified' } @@ -49,32 +49,32 @@ DCTrueDiff >> assignSharesRecurseFrom: this to: that subtreeReg: aRegistry [ this type = that type ifTrue: [ | thisList thatList | - thisList := this children asOrderedCollection. - thatList := that children asOrderedCollection. + thisList := this baseChildren asOrderedCollection. + thatList := that baseChildren asOrderedCollection. self assignSharesListFrom: thisList to: thatList subtreeReg: aRegistry. self assignSharesListFrom: thisList reverseInPlace to: thatList reverseInPlace subtreeReg: aRegistry. thisList withOrNil: thatList do: [:l :r | - l ifNil: [r allChildrenDo: [:c | aRegistry assignShare: c]] ifNotNil: [ - r ifNil: [l allChildrenDo: [:c | aRegistry assignShareAndRegisterTree: c]] ifNotNil: [ + l ifNil: [r allBaseChildrenDo: [:c | aRegistry assignShare: c]] ifNotNil: [ + r ifNil: [l allBaseChildrenDo: [:c | aRegistry assignShareAndRegisterTree: c]] ifNotNil: [ aRegistry assignShareAndRegisterTree: l. aRegistry assignShare: r. self assignSharesRecurseFrom: l to: r subtreeReg: aRegistry]]]] ifFalse: [ - this onlyChildrenDo: [:c | aRegistry assignShareAndRegisterTree: c]. - that onlyChildrenDo: [:c | aRegistry assignShare: c]] + this allBaseChildrenExceptSelfDo: [:c | aRegistry assignShareAndRegisterTree: c]. + that allBaseChildrenExceptSelfDo: [:c | aRegistry assignShare: c]] ] { #category : #'as yet unclassified' } DCTrueDiff >> assignSubtreesFrom: this to: that subtreeReg: aRegistry [ | queue | - queue := SortedCollection sortBlock: [:a :b | a treeHeight > b treeHeight]. + queue := SortedCollection sortBlock: [:a :b | a baseTreeHeight > b baseTreeHeight]. queue add: that. [queue isEmpty] whileFalse: [ | level nextNodes remainingMatchedNodes unassignedNodes | - level := queue first treeHeight. + level := queue first baseTreeHeight. nextNodes := OrderedCollection new. - [queue notEmpty and: [queue first treeHeight = level]] whileTrue: [ | next | + [queue notEmpty and: [queue first baseTreeHeight = level]] whileTrue: [ | next | next := queue removeFirst. next assigned ifNil: [nextNodes add: next]]. remainingMatchedNodes := self @@ -85,7 +85,7 @@ DCTrueDiff >> assignSubtreesFrom: this to: that subtreeReg: aRegistry [ selectAvailableTreeFrom: remainingMatchedNodes literalMatch: false subtreeReg: aRegistry. - unassignedNodes do: [:node | queue addAll: node children]] + unassignedNodes do: [:node | queue addAll: node baseChildren]] ] { #category : #'as yet unclassified' } @@ -105,7 +105,9 @@ DCTrueDiff >> assignTreeRecFrom: this to: that [ this assigned: that. that assigned: this. - this children with: that children do: [:l :r | self assignTreeRecFrom: l to: r] + this baseChildren + with: that baseChildren + do: [:l :r | self assignTreeRecFrom: l to: r] ] { #category : #'as yet unclassified' } @@ -142,10 +144,10 @@ DCTrueDiff >> computeEditScriptFrom: this to: that parent: anotherNode parentTyp (this type = that type and: [this assigned isNil and: [that assigned isNil]]) ifTrue: [ - this children do: [:c | + this baseChildren do: [:c | anEditBuffer detach: c. self unloadUnassigned: c in: anEditBuffer]. - that children withIndexDo: [:c :index | | new | + that baseChildren withIndexDo: [:c :index | | new | new := self loadUnassigned: c in: anEditBuffer. anEditBuffer attach: new to: this at: index]. newTree := this] @@ -201,8 +203,8 @@ DCTrueDiff >> computeEditScriptRecurse2From: this to: that parent: aNode parentT ifTrue: [ | thatList thisList | this range: that range. - thisList := this children asOrderedCollection. - thatList := that children asOrderedCollection. + thisList := this baseChildren asOrderedCollection. + thatList := that baseChildren asOrderedCollection. [thisList notEmpty and: [thatList notEmpty]] whileTrue: [ (thisList first assigned isNil and: [thatList first assigned isNil]) ifTrue: [ @@ -211,7 +213,7 @@ DCTrueDiff >> computeEditScriptRecurse2From: this to: that parent: aNode parentT to: thatList first parent: this parentType: this type - link: thatList first siblingIndex + link: thatList first baseSiblingIndex edits: anEditBuffer. thisList removeFirst. thatList removeFirst] @@ -225,7 +227,7 @@ DCTrueDiff >> computeEditScriptRecurse2From: this to: that parent: aNode parentT (thisList first assigned notNil and: [thatList includes: thisList first assigned]) ifTrue: [ anEditBuffer detach: thisList first. - anEditBuffer attach: thisList first to: this at: thisList first assigned siblingIndex. + anEditBuffer attach: thisList first to: this at: thisList first assigned baseSiblingIndex. self updateLiteralsFrom: thisList first to: thisList first assigned in: anEditBuffer. thatList remove: thisList first assigned. thisList removeFirst] @@ -241,7 +243,7 @@ DCTrueDiff >> computeEditScriptRecurse2From: this to: that parent: aNode parentT to: thatList first parent: this parentType: this type - link: thatList first siblingIndex + link: thatList first baseSiblingIndex edits: anEditBuffer. thisList removeFirst. thatList removeFirst]]]]]. @@ -249,7 +251,7 @@ DCTrueDiff >> computeEditScriptRecurse2From: this to: that parent: aNode parentT anEditBuffer attach: (self loadUnassigned: thatNode in: anEditBuffer) to: aNode - at: thatNode siblingIndex]. + at: thatNode baseSiblingIndex]. thisList do: [:thisNode | anEditBuffer detach: thisNode. self unloadUnassigned: thisNode in: anEditBuffer]. @@ -260,16 +262,16 @@ DCTrueDiff >> computeEditScriptRecurse2From: this to: that parent: aNode parentT { #category : #'as yet unclassified' } DCTrueDiff >> computeEditScriptRecurseFrom: this to: that parent: aNode parentType: aSymbol link: aLink in: anEditBuffer [ - ^ (this type = that type and: [this children size = that children size]) + ^ (this type = that type and: [this baseChildren size = that baseChildren size]) ifTrue: [ this range: that range. - this children with: that children do: [:thisNode :thatNode | | newNode | + this baseChildren with: that baseChildren do: [:thisNode :thatNode | | newNode | newNode := self computeEditScriptFrom: thisNode to: thatNode parent: this parentType: this type - link: thisNode siblingIndex + link: thisNode baseSiblingIndex edits: anEditBuffer]. this] ifFalse: [nil] @@ -282,7 +284,7 @@ DCTrueDiff >> loadUnassigned: aNode in: anEditBuffer [ ifNotNil: [self updateLiteralsFrom: aNode assigned to: aNode in: anEditBuffer] ifNil: [ | parent | parent := aNode shallowCopyBlock. - aNode children withIndexDo: [:c :index | anEditBuffer attach: (self loadUnassigned: c in: anEditBuffer) to: parent at: index]. + aNode baseChildren withIndexDo: [:c :index | anEditBuffer attach: (self loadUnassigned: c in: anEditBuffer) to: parent at: index]. parent] ] @@ -323,7 +325,7 @@ DCTrueDiff >> unloadUnassigned: aNode in: anEditBuffer [ aNode assigned ifNotNil: [aNode assigned: nil] ifNil: [ anEditBuffer remove: aNode. - aNode children do: [:c | self unloadUnassigned: c in: anEditBuffer]] + aNode baseChildren do: [:c | self unloadUnassigned: c in: anEditBuffer]] ] { #category : #'as yet unclassified' } @@ -331,8 +333,8 @@ DCTrueDiff >> updateLiteralsFrom: this to: that in: anEditBuffer [ this range: that range. this treeLabel = that treeLabel ifFalse: [anEditBuffer update: this to: that contents]. - this children - with: that children + this baseChildren + with: that baseChildren do: [:l :r | self updateLiteralsFrom: l to: r in: anEditBuffer]. ^ this ] diff --git a/packages/Sandblocks-Tlaplus/.squot-contents b/packages/Sandblocks-Tlaplus/.squot-contents new file mode 100644 index 0000000..1a2d841 --- /dev/null +++ b/packages/Sandblocks-Tlaplus/.squot-contents @@ -0,0 +1,6 @@ +SquotTrackedObjectMetadata { + #objectClassName : #PackageInfo, + #id : UUID [ 'ec1565dd709542339961a44f2477bfcb' ], + #objectsReplacedByNames : true, + #serializer : #SquotTonelSerializer +} \ No newline at end of file diff --git a/packages/Sandblocks-Tlaplus/SBTlaplus.class.st b/packages/Sandblocks-Tlaplus/SBTlaplus.class.st new file mode 100644 index 0000000..b025c5a --- /dev/null +++ b/packages/Sandblocks-Tlaplus/SBTlaplus.class.st @@ -0,0 +1,9871 @@ +Class { + #name : #SBTlaplus, + #superclass : #SBTSLanguage, + #category : #'Sandblocks-Tlaplus' +} + +{ #category : #'as yet unclassified' } +SBTlaplus class >> allFileSuffixes [ + + ^ {'tla'} +] + +{ #category : #properties } +SBTlaplus class >> grammarJson [ + + " https://github.com/tlaplus-community/tree-sitter-tlaplus/blob/master/src/grammar.json " + ^ '{ + "name": "tlaplus", + "word": "identifier", + "rules": { + "source_file": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "leading_extramodular_text" + }, + "named": true, + "value": "extramodular_text" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "REPEAT1", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "module" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "trailing_extramodular_text" + }, + "named": true, + "value": "extramodular_text" + }, + { + "type": "BLANK" + } + ] + } + ] + } + } + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "extends" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "_unit" + } + } + ] + } + ] + }, + "comment": { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 0, + "content": { + "type": "PATTERN", + "value": "\\\\\\*.*" + } + } + }, + "block_comment": { + "type": "SEQ", + "members": [ + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "STRING", + "value": "(*" + } + } + }, + { + "type": "REPEAT", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_algorithm" + }, + { + "type": "SYMBOL", + "name": "block_comment_text" + } + ] + } + }, + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "STRING", + "value": "*)" + } + } + } + ] + }, + "block_comment_text": { + "type": "PREC_RIGHT", + "value": 0, + "content": { + "type": "REPEAT1", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "PATTERN", + "value": "[^*()]|[^*][)]|[(][^(*]|[*][)][ \t]*(\r\n|\n)?[ \t]*[(][*]" + } + } + }, + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "PATTERN", + "value": "\\*" + } + } + }, + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "PATTERN", + "value": "\\(" + } + } + }, + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 1, + "content": { + "type": "PATTERN", + "value": "\\)" + } + } + } + ] + } + } + }, + "module": { + "type": "SEQ", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "single_line" + }, + "named": true, + "value": "header_line" + }, + { + "type": "STRING", + "value": "MODULE" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "single_line" + }, + "named": true, + "value": "header_line" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "extends" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "_unit" + } + }, + { + "type": "SYMBOL", + "name": "double_line" + } + ] + }, + "single_line": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "----" + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "-*" + } + } + ] + }, + "double_line": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "====" + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "=*" + } + } + ] + }, + "def_eq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "==" + }, + { + "type": "STRING", + "value": "≜" + } + ] + }, + "set_in": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\in" + }, + { + "type": "STRING", + "value": "∈" + } + ] + }, + "gets": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "<-" + }, + { + "type": "STRING", + "value": "⟵" + }, + { + "type": "STRING", + "value": "←" + } + ] + }, + "forall": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\A" + }, + { + "type": "STRING", + "value": "\\forall" + }, + { + "type": "STRING", + "value": "∀" + } + ] + }, + "exists": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\E" + }, + { + "type": "STRING", + "value": "\\exists" + }, + { + "type": "STRING", + "value": "∃" + } + ] + }, + "temporal_forall": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\AA" + } + ] + }, + "temporal_exists": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\EE" + } + ] + }, + "all_map_to": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "|->" + }, + { + "type": "STRING", + "value": "⟼" + }, + { + "type": "STRING", + "value": "↦" + } + ] + }, + "maps_to": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "->" + }, + { + "type": "STRING", + "value": "⟶" + }, + { + "type": "STRING", + "value": "→" + } + ] + }, + "langle_bracket": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "<<" + }, + { + "type": "STRING", + "value": "〈" + }, + { + "type": "STRING", + "value": "⟨" + } + ] + }, + "rangle_bracket": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ">>" + }, + { + "type": "STRING", + "value": "〉" + }, + { + "type": "STRING", + "value": "⟩" + } + ] + }, + "rangle_bracket_sub": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ">>_" + }, + { + "type": "STRING", + "value": "〉_" + }, + { + "type": "STRING", + "value": "⟩_" + } + ] + }, + "case_box": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "[]" + }, + { + "type": "STRING", + "value": "□" + } + ] + }, + "case_arrow": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "->" + }, + { + "type": "STRING", + "value": "⟶" + }, + { + "type": "STRING", + "value": "→" + } + ] + }, + "colon": { + "type": "STRING", + "value": ":" + }, + "address": { + "type": "STRING", + "value": "@" + }, + "label_as": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "::" + }, + { + "type": "STRING", + "value": "∷" + } + ] + }, + "placeholder": { + "type": "STRING", + "value": "_" + }, + "bullet_conj": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "/\\" + }, + { + "type": "STRING", + "value": "∧" + } + ] + }, + "bullet_disj": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\/" + }, + { + "type": "STRING", + "value": "∨" + } + ] + }, + "keyword": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "ASSUME" + }, + { + "type": "STRING", + "value": "ELSE" + }, + { + "type": "STRING", + "value": "LOCAL" + }, + { + "type": "STRING", + "value": "UNION" + }, + { + "type": "STRING", + "value": "ASSUMPTION" + }, + { + "type": "STRING", + "value": "ENABLED" + }, + { + "type": "STRING", + "value": "MODULE" + }, + { + "type": "STRING", + "value": "VARIABLE" + }, + { + "type": "STRING", + "value": "AXIOM" + }, + { + "type": "STRING", + "value": "EXCEPT" + }, + { + "type": "STRING", + "value": "OTHER" + }, + { + "type": "STRING", + "value": "VARIABLES" + }, + { + "type": "STRING", + "value": "CASE" + }, + { + "type": "STRING", + "value": "EXTENDS" + }, + { + "type": "STRING", + "value": "SF_" + }, + { + "type": "STRING", + "value": "WF_" + }, + { + "type": "STRING", + "value": "CHOOSE" + }, + { + "type": "STRING", + "value": "IF" + }, + { + "type": "STRING", + "value": "SUBSET" + }, + { + "type": "STRING", + "value": "WITH" + }, + { + "type": "STRING", + "value": "CONSTANT" + }, + { + "type": "STRING", + "value": "IN" + }, + { + "type": "STRING", + "value": "THEN" + }, + { + "type": "STRING", + "value": "CONSTANTS" + }, + { + "type": "STRING", + "value": "INSTANCE" + }, + { + "type": "STRING", + "value": "THEOREM" + }, + { + "type": "STRING", + "value": "COROLLARY" + }, + { + "type": "STRING", + "value": "DOMAIN" + }, + { + "type": "STRING", + "value": "LET" + }, + { + "type": "STRING", + "value": "UNCHANGED" + }, + { + "type": "STRING", + "value": "BY" + }, + { + "type": "STRING", + "value": "HAVE" + }, + { + "type": "STRING", + "value": "QED" + }, + { + "type": "STRING", + "value": "TAKE" + }, + { + "type": "STRING", + "value": "DEF" + }, + { + "type": "STRING", + "value": "HIDE" + }, + { + "type": "STRING", + "value": "RECURSIVE" + }, + { + "type": "STRING", + "value": "USE" + }, + { + "type": "STRING", + "value": "DEFINE" + }, + { + "type": "STRING", + "value": "PROOF" + }, + { + "type": "STRING", + "value": "WITNESS" + }, + { + "type": "STRING", + "value": "PICK" + }, + { + "type": "STRING", + "value": "DEFS" + }, + { + "type": "STRING", + "value": "PROVE" + }, + { + "type": "STRING", + "value": "SUFFICES" + }, + { + "type": "STRING", + "value": "NEW" + }, + { + "type": "STRING", + "value": "LAMBDA" + }, + { + "type": "STRING", + "value": "STATE" + }, + { + "type": "STRING", + "value": "ACTION" + }, + { + "type": "STRING", + "value": "TEMPORAL" + }, + { + "type": "STRING", + "value": "OBVIOUS" + }, + { + "type": "STRING", + "value": "OMITTED" + }, + { + "type": "STRING", + "value": "LEMMA" + }, + { + "type": "STRING", + "value": "PROPOSITION" + }, + { + "type": "STRING", + "value": "ONLY" + } + ] + }, + "identifier": { + "type": "PATTERN", + "value": "[0-9_]*[A-Za-z][A-Za-z0-9_]*" + }, + "extends": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "EXTENDS" + }, + { + "type": "SEQ", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + } + ] + } + } + ] + } + ] + }, + "_unit": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "variable_declaration" + }, + { + "type": "SYMBOL", + "name": "constant_declaration" + }, + { + "type": "SYMBOL", + "name": "recursive_declaration" + }, + { + "type": "SYMBOL", + "name": "use_or_hide" + }, + { + "type": "SYMBOL", + "name": "local_definition" + }, + { + "type": "SYMBOL", + "name": "_definition" + }, + { + "type": "SYMBOL", + "name": "assumption" + }, + { + "type": "SYMBOL", + "name": "theorem" + }, + { + "type": "SYMBOL", + "name": "module" + }, + { + "type": "SYMBOL", + "name": "single_line" + } + ] + }, + "local_definition": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "LOCAL" + }, + { + "type": "SYMBOL", + "name": "_definition" + } + ] + }, + "_definition": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "operator_definition" + }, + { + "type": "SYMBOL", + "name": "function_definition" + }, + { + "type": "SYMBOL", + "name": "instance" + }, + { + "type": "SYMBOL", + "name": "module_definition" + } + ] + }, + "variable_declaration": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "VARIABLE" + }, + { + "type": "STRING", + "value": "VARIABLES" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + } + ] + }, + "constant_declaration": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "CONSTANT" + }, + { + "type": "STRING", + "value": "CONSTANTS" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + } + ] + } + } + ] + } + ] + }, + "recursive_declaration": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "RECURSIVE" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + } + ] + } + } + ] + } + ] + }, + "operator_declaration": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "placeholder" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "placeholder" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "prefix_op_symbol" + } + }, + { + "type": "SYMBOL", + "name": "placeholder" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "placeholder" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "infix_op_symbol" + } + }, + { + "type": "SYMBOL", + "name": "placeholder" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "placeholder" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "postfix_op_symbol" + } + } + ] + } + ] + }, + "_id_or_op_declaration": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "operator_declaration" + } + ] + }, + "operator_definition": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + { + "type": "BLANK" + } + ] + } + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "prefix_op_symbol" + } + }, + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "infix_op_symbol" + } + }, + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "postfix_op_symbol" + } + } + ] + } + ] + }, + { + "type": "SYMBOL", + "name": "def_eq" + }, + { + "type": "FIELD", + "name": "definition", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + }, + "function_definition": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": "[" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "quantifier_bound" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "quantifier_bound" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": "]" + }, + { + "type": "SYMBOL", + "name": "def_eq" + }, + { + "type": "FIELD", + "name": "definition", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + }, + "quantifier_bound": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + }, + { + "type": "SYMBOL", + "name": "tuple_of_identifiers" + } + ] + }, + { + "type": "SYMBOL", + "name": "set_in" + }, + { + "type": "FIELD", + "name": "set", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + }, + "tuple_of_identifiers": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "langle_bracket" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + }, + { + "type": "SYMBOL", + "name": "rangle_bracket" + } + ] + }, + "instance": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "INSTANCE" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "WITH" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "substitution" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "substitution" + } + ] + } + } + ] + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "substitution": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "SYMBOL", + "name": "prefix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "infix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "postfix_op_symbol" + } + ] + }, + { + "type": "SYMBOL", + "name": "gets" + }, + { + "type": "SYMBOL", + "name": "_op_or_expr" + } + ] + }, + "_op_or_expr": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_op" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "_op": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "prefix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "infix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "postfix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "lambda" + } + ] + }, + "subexpr_prefix": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "subexpr_component" + }, + { + "type": "SYMBOL", + "name": "proof_step_ref" + } + ] + }, + { + "type": "STRING", + "value": "!" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "subexpr_component" + }, + { + "type": "SYMBOL", + "name": "subexpr_tree_nav" + } + ] + }, + { + "type": "STRING", + "value": "!" + } + ] + } + } + ] + }, + "subexpr_component": { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "SYMBOL", + "name": "bound_op" + }, + { + "type": "SYMBOL", + "name": "bound_nonfix_op" + }, + { + "type": "SYMBOL", + "name": "prefix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "infix_op_symbol" + }, + { + "type": "SYMBOL", + "name": "postfix_op_symbol" + } + ] + }, + "bound_op": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + } + }, + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_op_or_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_op_or_expr" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + } + ] + }, + "bound_nonfix_op": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "prefix_op_symbol" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "infix_op_symbol" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "postfix_op_symbol" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + } + ] + }, + "subexpr_tree_nav": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "langle_bracket" + }, + { + "type": "SYMBOL", + "name": "rangle_bracket" + }, + { + "type": "SYMBOL", + "name": "child_id" + }, + { + "type": "SYMBOL", + "name": "colon" + }, + { + "type": "SYMBOL", + "name": "address" + }, + { + "type": "SYMBOL", + "name": "operator_args" + } + ] + }, + "child_id": { + "type": "PATTERN", + "value": "\\d+" + }, + "operator_args": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_op_or_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_op_or_expr" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + "lambda": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "LAMBDA" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "module_definition": { + "type": "SEQ", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + { + "type": "BLANK" + } + ] + } + } + ] + }, + { + "type": "SYMBOL", + "name": "def_eq" + }, + { + "type": "FIELD", + "name": "definition", + "content": { + "type": "SYMBOL", + "name": "instance" + } + } + ] + }, + "_expr": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_number" + }, + { + "type": "SYMBOL", + "name": "string" + }, + { + "type": "SYMBOL", + "name": "boolean" + }, + { + "type": "SYMBOL", + "name": "_primitive_value_set" + }, + { + "type": "SYMBOL", + "name": "parentheses" + }, + { + "type": "SYMBOL", + "name": "label" + }, + { + "type": "SYMBOL", + "name": "subexpression" + }, + { + "type": "SYMBOL", + "name": "proof_step_ref" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "SYMBOL", + "name": "bound_op" + }, + { + "type": "SYMBOL", + "name": "bound_nonfix_op" + }, + { + "type": "SYMBOL", + "name": "prefixed_op" + }, + { + "type": "SYMBOL", + "name": "bound_prefix_op" + }, + { + "type": "SYMBOL", + "name": "bound_infix_op" + }, + { + "type": "SYMBOL", + "name": "bound_postfix_op" + }, + { + "type": "SYMBOL", + "name": "bounded_quantification" + }, + { + "type": "SYMBOL", + "name": "unbounded_quantification" + }, + { + "type": "SYMBOL", + "name": "choose" + }, + { + "type": "SYMBOL", + "name": "finite_set_literal" + }, + { + "type": "SYMBOL", + "name": "set_filter" + }, + { + "type": "SYMBOL", + "name": "set_map" + }, + { + "type": "SYMBOL", + "name": "function_evaluation" + }, + { + "type": "SYMBOL", + "name": "function_literal" + }, + { + "type": "SYMBOL", + "name": "set_of_functions" + }, + { + "type": "SYMBOL", + "name": "record_literal" + }, + { + "type": "SYMBOL", + "name": "set_of_records" + }, + { + "type": "SYMBOL", + "name": "record_value" + }, + { + "type": "SYMBOL", + "name": "except" + }, + { + "type": "SYMBOL", + "name": "prev_func_val" + }, + { + "type": "SYMBOL", + "name": "tuple_literal" + }, + { + "type": "SYMBOL", + "name": "step_expr_or_stutter" + }, + { + "type": "SYMBOL", + "name": "step_expr_no_stutter" + }, + { + "type": "SYMBOL", + "name": "fairness" + }, + { + "type": "SYMBOL", + "name": "if_then_else" + }, + { + "type": "SYMBOL", + "name": "case" + }, + { + "type": "SYMBOL", + "name": "let_in" + }, + { + "type": "SYMBOL", + "name": "conj_list" + }, + { + "type": "SYMBOL", + "name": "disj_list" + } + ] + }, + "_subscript_expr": { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "SYMBOL", + "name": "bound_op" + }, + { + "type": "SYMBOL", + "name": "bound_nonfix_op" + }, + { + "type": "SYMBOL", + "name": "prefixed_op" + }, + { + "type": "SYMBOL", + "name": "parentheses" + }, + { + "type": "SYMBOL", + "name": "finite_set_literal" + }, + { + "type": "SYMBOL", + "name": "set_filter" + }, + { + "type": "SYMBOL", + "name": "set_map" + }, + { + "type": "SYMBOL", + "name": "function_literal" + }, + { + "type": "SYMBOL", + "name": "set_of_functions" + }, + { + "type": "SYMBOL", + "name": "record_literal" + }, + { + "type": "SYMBOL", + "name": "set_of_records" + }, + { + "type": "SYMBOL", + "name": "except" + }, + { + "type": "SYMBOL", + "name": "tuple_literal" + }, + { + "type": "SYMBOL", + "name": "step_expr_or_stutter" + }, + { + "type": "SYMBOL", + "name": "step_expr_no_stutter" + } + ] + }, + "prefixed_op": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "prefix", + "content": { + "type": "SYMBOL", + "name": "subexpr_prefix" + } + }, + { + "type": "FIELD", + "name": "op", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "SYMBOL", + "name": "bound_op" + }, + { + "type": "SYMBOL", + "name": "bound_nonfix_op" + } + ] + } + } + ] + }, + "_number": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "nat_number" + }, + { + "type": "SYMBOL", + "name": "real_number" + }, + { + "type": "SYMBOL", + "name": "binary_number" + }, + { + "type": "SYMBOL", + "name": "octal_number" + }, + { + "type": "SYMBOL", + "name": "hex_number" + } + ] + }, + "nat_number": { + "type": "PATTERN", + "value": "\\d+" + }, + "real_number": { + "type": "PATTERN", + "value": "\\d*\\.\\d+" + }, + "binary_number": { + "type": "SEQ", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\b" + }, + { + "type": "STRING", + "value": "\\B" + } + ] + }, + "named": true, + "value": "format" + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "[0-1]+" + } + }, + "named": true, + "value": "value" + } + ] + }, + "octal_number": { + "type": "SEQ", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\o" + }, + { + "type": "STRING", + "value": "\\O" + } + ] + }, + "named": true, + "value": "format" + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "[0-7]+" + } + }, + "named": true, + "value": "value" + } + ] + }, + "hex_number": { + "type": "SEQ", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\h" + }, + { + "type": "STRING", + "value": "\\H" + } + ] + }, + "named": true, + "value": "format" + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "[0-9a-fA-F]+" + } + }, + "named": true, + "value": "value" + } + ] + }, + "string": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "\"" + }, + { + "type": "REPEAT", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "[^\"\\n]" + } + }, + { + "type": "SYMBOL", + "name": "escape_char" + } + ] + } + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "STRING", + "value": "\"" + } + } + ] + }, + "escape_char": { + "type": "SEQ", + "members": [ + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "STRING", + "value": "\\" + } + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "." + } + } + ] + }, + "boolean": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "TRUE" + }, + { + "type": "STRING", + "value": "FALSE" + } + ] + }, + "_primitive_value_set": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "string_set" + }, + { + "type": "SYMBOL", + "name": "boolean_set" + }, + { + "type": "SYMBOL", + "name": "nat_number_set" + }, + { + "type": "SYMBOL", + "name": "int_number_set" + }, + { + "type": "SYMBOL", + "name": "real_number_set" + } + ] + }, + "string_set": { + "type": "STRING", + "value": "STRING" + }, + "boolean_set": { + "type": "STRING", + "value": "BOOLEAN" + }, + "nat_number_set": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "Nat" + }, + { + "type": "STRING", + "value": "ℕ" + } + ] + }, + "int_number_set": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "Int" + }, + { + "type": "STRING", + "value": "ℤ" + } + ] + }, + "real_number_set": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "Real" + }, + { + "type": "STRING", + "value": "ℝ" + } + ] + }, + "label": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + { + "type": "BLANK" + } + ] + } + } + ] + } + }, + { + "type": "SYMBOL", + "name": "label_as" + }, + { + "type": "FIELD", + "name": "expression", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + "subexpression": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "subexpr_prefix" + }, + { + "type": "SYMBOL", + "name": "subexpr_tree_nav" + } + ] + }, + "parentheses": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + "bounded_quantification": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "quantifier", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "forall" + }, + { + "type": "SYMBOL", + "name": "exists" + } + ] + } + }, + { + "type": "FIELD", + "name": "bound", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "quantifier_bound" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "quantifier_bound" + } + ] + } + } + ] + } + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "FIELD", + "name": "expression", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + "unbounded_quantification": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "quantifier", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "forall" + }, + { + "type": "SYMBOL", + "name": "exists" + }, + { + "type": "SYMBOL", + "name": "temporal_forall" + }, + { + "type": "SYMBOL", + "name": "temporal_exists" + } + ] + } + }, + { + "type": "FIELD", + "name": "identifier", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + } + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "FIELD", + "name": "expression", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + "choose": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "CHOOSE" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "tuple_of_identifiers" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "set_in" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + }, + "finite_set_literal": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "{" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": "}" + } + ] + }, + "set_filter": { + "type": "PREC_DYNAMIC", + "value": 1, + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "{" + }, + { + "type": "FIELD", + "name": "generator", + "content": { + "type": "SYMBOL", + "name": "quantifier_bound" + } + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "FIELD", + "name": "filter", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "STRING", + "value": "}" + } + ] + } + }, + "set_map": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "{" + }, + { + "type": "FIELD", + "name": "map", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "FIELD", + "name": "generator", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "quantifier_bound" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "quantifier_bound" + } + ] + } + } + ] + } + }, + { + "type": "STRING", + "value": "}" + } + ] + }, + "function_evaluation": { + "type": "PREC", + "value": "16-16", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "[" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": "]" + } + ] + } + }, + "function_literal": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "quantifier_bound" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "quantifier_bound" + } + ] + } + } + ] + }, + { + "type": "SYMBOL", + "name": "all_map_to" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + "set_of_functions": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "maps_to" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + "record_literal": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "all_map_to" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "all_map_to" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + "set_of_records": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + "record_value": { + "type": "PREC_LEFT", + "value": "17-17", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "." + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + } + ] + } + }, + "except": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "FIELD", + "name": "expr_to_update", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "STRING", + "value": "EXCEPT" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "except_update" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "except_update" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + "except_update": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "update_specifier", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "!" + }, + { + "type": "SYMBOL", + "name": "except_update_specifier" + } + ] + } + }, + { + "type": "STRING", + "value": "=" + }, + { + "type": "FIELD", + "name": "new_val", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + }, + "except_update_specifier": { + "type": "REPEAT1", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "except_update_record_field" + }, + { + "type": "SYMBOL", + "name": "except_update_fn_appl" + } + ] + } + }, + "except_update_record_field": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "." + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + } + ] + }, + "except_update_fn_appl": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + "prev_func_val": { + "type": "STRING", + "value": "@" + }, + "tuple_literal": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "langle_bracket" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "SYMBOL", + "name": "rangle_bracket" + } + ] + }, + "step_expr_or_stutter": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "]_" + }, + { + "type": "SYMBOL", + "name": "_subscript_expr" + } + ] + }, + "step_expr_no_stutter": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "langle_bracket" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "rangle_bracket_sub" + }, + { + "type": "SYMBOL", + "name": "_subscript_expr" + } + ] + }, + "fairness": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "WF_" + }, + { + "type": "STRING", + "value": "SF_" + } + ] + }, + { + "type": "SYMBOL", + "name": "_subscript_expr" + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + "if_then_else": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "IF" + }, + { + "type": "FIELD", + "name": "if", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "STRING", + "value": "THEN" + }, + { + "type": "FIELD", + "name": "then", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "STRING", + "value": "ELSE" + }, + { + "type": "FIELD", + "name": "else", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + "case": { + "type": "PREC_RIGHT", + "value": 0, + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "CASE" + }, + { + "type": "SYMBOL", + "name": "case_arm" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "case_box" + }, + { + "type": "SYMBOL", + "name": "case_arm" + } + ] + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "case_box" + }, + { + "type": "SYMBOL", + "name": "other_arm" + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + } + }, + "case_arm": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "case_arrow" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + }, + "other_arm": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "OTHER" + }, + { + "type": "SYMBOL", + "name": "case_arrow" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + }, + "let_in": { + "type": "PREC", + "value": "0-0", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "LET" + }, + { + "type": "FIELD", + "name": "definitions", + "content": { + "type": "REPEAT1", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "operator_definition" + }, + { + "type": "SYMBOL", + "name": "function_definition" + }, + { + "type": "SYMBOL", + "name": "module_definition" + }, + { + "type": "SYMBOL", + "name": "recursive_declaration" + } + ] + } + } + }, + { + "type": "STRING", + "value": "IN" + }, + { + "type": "FIELD", + "name": "expression", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + "conj_list": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_indent" + }, + { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "conj_item" + } + }, + { + "type": "SYMBOL", + "name": "_dedent" + } + ] + }, + "conj_item": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_bullet" + }, + { + "type": "SYMBOL", + "name": "bullet_conj" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "disj_list": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_indent" + }, + { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "disj_item" + } + }, + { + "type": "SYMBOL", + "name": "_dedent" + } + ] + }, + "disj_item": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_bullet" + }, + { + "type": "SYMBOL", + "name": "bullet_disj" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "lnot": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\lnot" + }, + { + "type": "STRING", + "value": "\\neg" + }, + { + "type": "STRING", + "value": "~" + }, + { + "type": "STRING", + "value": "¬" + } + ] + }, + "union": { + "type": "STRING", + "value": "UNION" + }, + "powerset": { + "type": "STRING", + "value": "SUBSET" + }, + "domain": { + "type": "STRING", + "value": "DOMAIN" + }, + "negative": { + "type": "STRING", + "value": "-" + }, + "negative_dot": { + "type": "STRING", + "value": "-." + }, + "enabled": { + "type": "STRING", + "value": "ENABLED" + }, + "unchanged": { + "type": "STRING", + "value": "UNCHANGED" + }, + "always": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "[]" + }, + { + "type": "STRING", + "value": "□" + } + ] + }, + "eventually": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "<>" + }, + { + "type": "STRING", + "value": "⋄" + } + ] + }, + "prefix_op_symbol": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "lnot" + }, + { + "type": "SYMBOL", + "name": "union" + }, + { + "type": "SYMBOL", + "name": "powerset" + }, + { + "type": "SYMBOL", + "name": "domain" + }, + { + "type": "SYMBOL", + "name": "enabled" + }, + { + "type": "SYMBOL", + "name": "unchanged" + }, + { + "type": "SYMBOL", + "name": "always" + }, + { + "type": "SYMBOL", + "name": "eventually" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "negative_dot" + }, + "named": true, + "value": "negative" + } + ] + }, + "bound_prefix_op": { + "type": "CHOICE", + "members": [ + { + "type": "PREC_LEFT", + "value": "4-4", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "lnot" + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "8-8", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "union" + }, + { + "type": "SYMBOL", + "name": "powerset" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "9-9", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "domain" + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "12-12", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "negative" + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "15-15", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "enabled" + }, + { + "type": "SYMBOL", + "name": "unchanged" + }, + { + "type": "SYMBOL", + "name": "always" + }, + { + "type": "SYMBOL", + "name": "eventually" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + } + ] + }, + "implies": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=>" + }, + { + "type": "STRING", + "value": "⟹" + }, + { + "type": "STRING", + "value": "⇒" + } + ] + }, + "plus_arrow": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "-+->" + }, + { + "type": "STRING", + "value": "⇸" + }, + { + "type": "STRING", + "value": "⥅" + } + ] + }, + "equiv": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\equiv" + }, + { + "type": "STRING", + "value": "≡" + } + ] + }, + "iff": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "<=>" + }, + { + "type": "STRING", + "value": "⟺" + }, + { + "type": "STRING", + "value": "⇔" + } + ] + }, + "leads_to": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "~>" + }, + { + "type": "STRING", + "value": "⇝" + }, + { + "type": "STRING", + "value": "↝" + } + ] + }, + "land": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "/\\" + }, + { + "type": "STRING", + "value": "\\land" + }, + { + "type": "STRING", + "value": "∧" + } + ] + }, + "lor": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\/" + }, + { + "type": "STRING", + "value": "\\lor" + }, + { + "type": "STRING", + "value": "∨" + } + ] + }, + "assign": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ":=" + }, + { + "type": "STRING", + "value": "≔" + } + ] + }, + "bnf_rule": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "::=" + }, + { + "type": "STRING", + "value": "⩴" + } + ] + }, + "eq": { + "type": "STRING", + "value": "=" + }, + "neq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "/=" + }, + { + "type": "STRING", + "value": "#" + }, + { + "type": "STRING", + "value": "≠" + } + ] + }, + "lt": { + "type": "STRING", + "value": "<" + }, + "gt": { + "type": "STRING", + "value": ">" + }, + "leq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "<=" + }, + { + "type": "STRING", + "value": "=<" + }, + { + "type": "STRING", + "value": "\\leq" + }, + { + "type": "STRING", + "value": "≤" + } + ] + }, + "geq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ">=" + }, + { + "type": "STRING", + "value": "\\geq" + }, + { + "type": "STRING", + "value": "≥" + } + ] + }, + "approx": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\approx" + }, + { + "type": "STRING", + "value": "≈" + } + ] + }, + "rs_ttile": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "|-" + }, + { + "type": "STRING", + "value": "⊢" + } + ] + }, + "rd_ttile": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "|=" + }, + { + "type": "STRING", + "value": "⊨" + } + ] + }, + "ls_ttile": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "-|" + }, + { + "type": "STRING", + "value": "⊣" + } + ] + }, + "ld_ttile": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=|" + }, + { + "type": "STRING", + "value": "⫤" + } + ] + }, + "asymp": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\asymp" + }, + { + "type": "STRING", + "value": "≍" + } + ] + }, + "cong": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\cong" + }, + { + "type": "STRING", + "value": "≅" + } + ] + }, + "doteq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\doteq" + }, + { + "type": "STRING", + "value": "≐" + } + ] + }, + "gg": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\gg" + }, + { + "type": "STRING", + "value": "≫" + } + ] + }, + "ll": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\ll" + }, + { + "type": "STRING", + "value": "≪" + } + ] + }, + "in": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\in" + }, + { + "type": "STRING", + "value": "∈" + } + ] + }, + "notin": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\notin" + }, + { + "type": "STRING", + "value": "∉" + } + ] + }, + "prec": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\prec" + }, + { + "type": "STRING", + "value": "≺" + } + ] + }, + "succ": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\succ" + }, + { + "type": "STRING", + "value": "≻" + } + ] + }, + "preceq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\preceq" + }, + { + "type": "STRING", + "value": "⪯" + } + ] + }, + "succeq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\succeq" + }, + { + "type": "STRING", + "value": "⪰" + } + ] + }, + "propto": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\propto" + }, + { + "type": "STRING", + "value": "∝" + } + ] + }, + "sim": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sim" + }, + { + "type": "STRING", + "value": "∼" + } + ] + }, + "simeq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\simeq" + }, + { + "type": "STRING", + "value": "≃" + } + ] + }, + "sqsubset": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sqsubset" + }, + { + "type": "STRING", + "value": "⊏" + } + ] + }, + "sqsupset": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sqsupset" + }, + { + "type": "STRING", + "value": "⊐" + } + ] + }, + "sqsubseteq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sqsubseteq" + }, + { + "type": "STRING", + "value": "⊑" + } + ] + }, + "sqsupseteq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sqsupseteq" + }, + { + "type": "STRING", + "value": "⊒" + } + ] + }, + "subset": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\subset" + }, + { + "type": "STRING", + "value": "⊂" + } + ] + }, + "supset": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\supset" + }, + { + "type": "STRING", + "value": "⊃" + } + ] + }, + "subseteq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\subseteq" + }, + { + "type": "STRING", + "value": "⊆" + } + ] + }, + "supseteq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\supseteq" + }, + { + "type": "STRING", + "value": "⊇" + } + ] + }, + "compose": { + "type": "STRING", + "value": "@@" + }, + "map_to": { + "type": "STRING", + "value": ":>" + }, + "map_from": { + "type": "STRING", + "value": "<:" + }, + "setminus": { + "type": "STRING", + "value": "\\" + }, + "cap": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\cap" + }, + { + "type": "STRING", + "value": "\\intersect" + }, + { + "type": "STRING", + "value": "∩" + } + ] + }, + "cup": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\cup" + }, + { + "type": "STRING", + "value": "\\union" + }, + { + "type": "STRING", + "value": "∪" + } + ] + }, + "dots_2": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ".." + }, + { + "type": "STRING", + "value": "‥" + } + ] + }, + "dots_3": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "..." + }, + { + "type": "STRING", + "value": "…" + } + ] + }, + "plus": { + "type": "STRING", + "value": "+" + }, + "plusplus": { + "type": "STRING", + "value": "++" + }, + "oplus": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\oplus" + }, + { + "type": "STRING", + "value": "(+)" + }, + { + "type": "STRING", + "value": "⊕" + } + ] + }, + "ominus": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\ominus" + }, + { + "type": "STRING", + "value": "(-)" + }, + { + "type": "STRING", + "value": "⊖" + } + ] + }, + "mod": { + "type": "STRING", + "value": "%" + }, + "modmod": { + "type": "STRING", + "value": "%%" + }, + "vert": { + "type": "STRING", + "value": "|" + }, + "vertvert": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "||" + }, + { + "type": "STRING", + "value": "‖" + } + ] + }, + "minus": { + "type": "STRING", + "value": "-" + }, + "minusminus": { + "type": "STRING", + "value": "--" + }, + "amp": { + "type": "STRING", + "value": "&" + }, + "ampamp": { + "type": "STRING", + "value": "&&" + }, + "odot": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\odot" + }, + { + "type": "STRING", + "value": "(.)" + }, + { + "type": "STRING", + "value": "⊙" + } + ] + }, + "oslash": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\oslash" + }, + { + "type": "STRING", + "value": "(/)" + }, + { + "type": "STRING", + "value": "⊘" + } + ] + }, + "otimes": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\otimes" + }, + { + "type": "STRING", + "value": "(\\X)" + }, + { + "type": "STRING", + "value": "⊗" + } + ] + }, + "mul": { + "type": "STRING", + "value": "*" + }, + "mulmul": { + "type": "STRING", + "value": "**" + }, + "slash": { + "type": "STRING", + "value": "/" + }, + "slashslash": { + "type": "STRING", + "value": "//" + }, + "bigcirc": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\bigcirc" + }, + { + "type": "STRING", + "value": "◯" + } + ] + }, + "bullet": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\bullet" + }, + { + "type": "STRING", + "value": "●" + } + ] + }, + "div": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\div" + }, + { + "type": "STRING", + "value": "÷" + } + ] + }, + "circ": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\o" + }, + { + "type": "STRING", + "value": "\\circ" + }, + { + "type": "STRING", + "value": "∘" + } + ] + }, + "star": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\star" + }, + { + "type": "STRING", + "value": "⋆" + } + ] + }, + "excl": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "!!" + }, + { + "type": "STRING", + "value": "‼" + } + ] + }, + "hashhash": { + "type": "STRING", + "value": "##" + }, + "dol": { + "type": "STRING", + "value": "$" + }, + "doldol": { + "type": "STRING", + "value": "$$" + }, + "qq": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "??" + }, + { + "type": "STRING", + "value": "⁇" + } + ] + }, + "sqcap": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sqcap" + }, + { + "type": "STRING", + "value": "⊓" + } + ] + }, + "sqcup": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\sqcup" + }, + { + "type": "STRING", + "value": "⊔" + } + ] + }, + "uplus": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\uplus" + }, + { + "type": "STRING", + "value": "⊎" + } + ] + }, + "times": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\X" + }, + { + "type": "STRING", + "value": "\\times" + }, + { + "type": "STRING", + "value": "×" + } + ] + }, + "wr": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\wr" + }, + { + "type": "STRING", + "value": "≀" + } + ] + }, + "cdot": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "\\cdot" + }, + { + "type": "STRING", + "value": "⋅" + } + ] + }, + "pow": { + "type": "STRING", + "value": "^" + }, + "powpow": { + "type": "STRING", + "value": "^^" + }, + "infix_op_symbol": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "implies" + }, + { + "type": "SYMBOL", + "name": "plus_arrow" + }, + { + "type": "SYMBOL", + "name": "equiv" + }, + { + "type": "SYMBOL", + "name": "iff" + }, + { + "type": "SYMBOL", + "name": "leads_to" + }, + { + "type": "SYMBOL", + "name": "land" + }, + { + "type": "SYMBOL", + "name": "lor" + }, + { + "type": "SYMBOL", + "name": "assign" + }, + { + "type": "SYMBOL", + "name": "bnf_rule" + }, + { + "type": "SYMBOL", + "name": "eq" + }, + { + "type": "SYMBOL", + "name": "neq" + }, + { + "type": "SYMBOL", + "name": "lt" + }, + { + "type": "SYMBOL", + "name": "gt" + }, + { + "type": "SYMBOL", + "name": "leq" + }, + { + "type": "SYMBOL", + "name": "geq" + }, + { + "type": "SYMBOL", + "name": "approx" + }, + { + "type": "SYMBOL", + "name": "rs_ttile" + }, + { + "type": "SYMBOL", + "name": "rd_ttile" + }, + { + "type": "SYMBOL", + "name": "ls_ttile" + }, + { + "type": "SYMBOL", + "name": "ld_ttile" + }, + { + "type": "SYMBOL", + "name": "asymp" + }, + { + "type": "SYMBOL", + "name": "cong" + }, + { + "type": "SYMBOL", + "name": "doteq" + }, + { + "type": "SYMBOL", + "name": "gg" + }, + { + "type": "SYMBOL", + "name": "ll" + }, + { + "type": "SYMBOL", + "name": "in" + }, + { + "type": "SYMBOL", + "name": "notin" + }, + { + "type": "SYMBOL", + "name": "prec" + }, + { + "type": "SYMBOL", + "name": "succ" + }, + { + "type": "SYMBOL", + "name": "preceq" + }, + { + "type": "SYMBOL", + "name": "succeq" + }, + { + "type": "SYMBOL", + "name": "propto" + }, + { + "type": "SYMBOL", + "name": "sim" + }, + { + "type": "SYMBOL", + "name": "simeq" + }, + { + "type": "SYMBOL", + "name": "sqsubset" + }, + { + "type": "SYMBOL", + "name": "sqsupset" + }, + { + "type": "SYMBOL", + "name": "sqsubseteq" + }, + { + "type": "SYMBOL", + "name": "sqsupseteq" + }, + { + "type": "SYMBOL", + "name": "subset" + }, + { + "type": "SYMBOL", + "name": "supset" + }, + { + "type": "SYMBOL", + "name": "subseteq" + }, + { + "type": "SYMBOL", + "name": "supseteq" + }, + { + "type": "SYMBOL", + "name": "compose" + }, + { + "type": "SYMBOL", + "name": "map_to" + }, + { + "type": "SYMBOL", + "name": "setminus" + }, + { + "type": "SYMBOL", + "name": "cap" + }, + { + "type": "SYMBOL", + "name": "cup" + }, + { + "type": "SYMBOL", + "name": "dots_2" + }, + { + "type": "SYMBOL", + "name": "dots_3" + }, + { + "type": "SYMBOL", + "name": "plus" + }, + { + "type": "SYMBOL", + "name": "plusplus" + }, + { + "type": "SYMBOL", + "name": "oplus" + }, + { + "type": "SYMBOL", + "name": "ominus" + }, + { + "type": "SYMBOL", + "name": "mod" + }, + { + "type": "SYMBOL", + "name": "modmod" + }, + { + "type": "SYMBOL", + "name": "vert" + }, + { + "type": "SYMBOL", + "name": "vertvert" + }, + { + "type": "SYMBOL", + "name": "minus" + }, + { + "type": "SYMBOL", + "name": "minusminus" + }, + { + "type": "SYMBOL", + "name": "amp" + }, + { + "type": "SYMBOL", + "name": "ampamp" + }, + { + "type": "SYMBOL", + "name": "odot" + }, + { + "type": "SYMBOL", + "name": "oslash" + }, + { + "type": "SYMBOL", + "name": "otimes" + }, + { + "type": "SYMBOL", + "name": "mul" + }, + { + "type": "SYMBOL", + "name": "mulmul" + }, + { + "type": "SYMBOL", + "name": "slash" + }, + { + "type": "SYMBOL", + "name": "slashslash" + }, + { + "type": "SYMBOL", + "name": "bigcirc" + }, + { + "type": "SYMBOL", + "name": "bullet" + }, + { + "type": "SYMBOL", + "name": "div" + }, + { + "type": "SYMBOL", + "name": "circ" + }, + { + "type": "SYMBOL", + "name": "star" + }, + { + "type": "SYMBOL", + "name": "excl" + }, + { + "type": "SYMBOL", + "name": "hashhash" + }, + { + "type": "SYMBOL", + "name": "dol" + }, + { + "type": "SYMBOL", + "name": "doldol" + }, + { + "type": "SYMBOL", + "name": "qq" + }, + { + "type": "SYMBOL", + "name": "sqcap" + }, + { + "type": "SYMBOL", + "name": "sqcup" + }, + { + "type": "SYMBOL", + "name": "uplus" + }, + { + "type": "SYMBOL", + "name": "times" + }, + { + "type": "SYMBOL", + "name": "wr" + }, + { + "type": "SYMBOL", + "name": "cdot" + }, + { + "type": "SYMBOL", + "name": "pow" + }, + { + "type": "SYMBOL", + "name": "powpow" + }, + { + "type": "SYMBOL", + "name": "map_from" + } + ] + }, + "bound_infix_op": { + "type": "CHOICE", + "members": [ + { + "type": "PREC_LEFT", + "value": "1-1", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "implies" + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "2-2", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "plus_arrow" + }, + { + "type": "SYMBOL", + "name": "equiv" + }, + { + "type": "SYMBOL", + "name": "iff" + }, + { + "type": "SYMBOL", + "name": "leads_to" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "3-3", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "land" + }, + { + "type": "SYMBOL", + "name": "lor" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "5-5", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "assign" + }, + { + "type": "SYMBOL", + "name": "bnf_rule" + }, + { + "type": "SYMBOL", + "name": "eq" + }, + { + "type": "SYMBOL", + "name": "neq" + }, + { + "type": "SYMBOL", + "name": "lt" + }, + { + "type": "SYMBOL", + "name": "gt" + }, + { + "type": "SYMBOL", + "name": "leq" + }, + { + "type": "SYMBOL", + "name": "geq" + }, + { + "type": "SYMBOL", + "name": "approx" + }, + { + "type": "SYMBOL", + "name": "rs_ttile" + }, + { + "type": "SYMBOL", + "name": "rd_ttile" + }, + { + "type": "SYMBOL", + "name": "ls_ttile" + }, + { + "type": "SYMBOL", + "name": "ld_ttile" + }, + { + "type": "SYMBOL", + "name": "asymp" + }, + { + "type": "SYMBOL", + "name": "cong" + }, + { + "type": "SYMBOL", + "name": "doteq" + }, + { + "type": "SYMBOL", + "name": "gg" + }, + { + "type": "SYMBOL", + "name": "ll" + }, + { + "type": "SYMBOL", + "name": "in" + }, + { + "type": "SYMBOL", + "name": "notin" + }, + { + "type": "SYMBOL", + "name": "prec" + }, + { + "type": "SYMBOL", + "name": "succ" + }, + { + "type": "SYMBOL", + "name": "preceq" + }, + { + "type": "SYMBOL", + "name": "succeq" + }, + { + "type": "SYMBOL", + "name": "propto" + }, + { + "type": "SYMBOL", + "name": "sim" + }, + { + "type": "SYMBOL", + "name": "simeq" + }, + { + "type": "SYMBOL", + "name": "sqsubset" + }, + { + "type": "SYMBOL", + "name": "sqsupset" + }, + { + "type": "SYMBOL", + "name": "sqsubseteq" + }, + { + "type": "SYMBOL", + "name": "sqsupseteq" + }, + { + "type": "SYMBOL", + "name": "subset" + }, + { + "type": "SYMBOL", + "name": "supset" + }, + { + "type": "SYMBOL", + "name": "subseteq" + }, + { + "type": "SYMBOL", + "name": "supseteq" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "6-6", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "SYMBOL", + "name": "compose" + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "7-7", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "map_to" + }, + { + "type": "SYMBOL", + "name": "map_from" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "8-8", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "setminus" + }, + { + "type": "SYMBOL", + "name": "cap" + }, + { + "type": "SYMBOL", + "name": "cup" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "9-9", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "dots_2" + }, + { + "type": "SYMBOL", + "name": "dots_3" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "10-10", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "plus" + }, + { + "type": "SYMBOL", + "name": "plusplus" + }, + { + "type": "SYMBOL", + "name": "oplus" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "11-11", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "ominus" + }, + { + "type": "SYMBOL", + "name": "mod" + }, + { + "type": "SYMBOL", + "name": "modmod" + }, + { + "type": "SYMBOL", + "name": "vert" + }, + { + "type": "SYMBOL", + "name": "vertvert" + }, + { + "type": "SYMBOL", + "name": "minus" + }, + { + "type": "SYMBOL", + "name": "minusminus" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "13-13", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "amp" + }, + { + "type": "SYMBOL", + "name": "ampamp" + }, + { + "type": "SYMBOL", + "name": "odot" + }, + { + "type": "SYMBOL", + "name": "oslash" + }, + { + "type": "SYMBOL", + "name": "otimes" + }, + { + "type": "SYMBOL", + "name": "mul" + }, + { + "type": "SYMBOL", + "name": "mulmul" + }, + { + "type": "SYMBOL", + "name": "slash" + }, + { + "type": "SYMBOL", + "name": "slashslash" + }, + { + "type": "SYMBOL", + "name": "bigcirc" + }, + { + "type": "SYMBOL", + "name": "bullet" + }, + { + "type": "SYMBOL", + "name": "div" + }, + { + "type": "SYMBOL", + "name": "circ" + }, + { + "type": "SYMBOL", + "name": "star" + }, + { + "type": "SYMBOL", + "name": "excl" + }, + { + "type": "SYMBOL", + "name": "hashhash" + }, + { + "type": "SYMBOL", + "name": "dol" + }, + { + "type": "SYMBOL", + "name": "doldol" + }, + { + "type": "SYMBOL", + "name": "qq" + }, + { + "type": "SYMBOL", + "name": "sqcap" + }, + { + "type": "SYMBOL", + "name": "sqcup" + }, + { + "type": "SYMBOL", + "name": "uplus" + }, + { + "type": "SYMBOL", + "name": "times" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + }, + { + "type": "PREC_LEFT", + "value": "14-14", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "wr" + }, + { + "type": "SYMBOL", + "name": "cdot" + }, + { + "type": "SYMBOL", + "name": "pow" + }, + { + "type": "SYMBOL", + "name": "powpow" + } + ] + } + }, + { + "type": "FIELD", + "name": "rhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + } + } + ] + }, + "sup_plus": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "^+" + }, + { + "type": "STRING", + "value": "⁺" + } + ] + }, + "asterisk": { + "type": "STRING", + "value": "^*" + }, + "sup_hash": { + "type": "STRING", + "value": "^#" + }, + "prime": { + "type": "STRING", + "value": "''" + }, + "postfix_op_symbol": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "sup_plus" + }, + { + "type": "SYMBOL", + "name": "asterisk" + }, + { + "type": "SYMBOL", + "name": "sup_hash" + }, + { + "type": "SYMBOL", + "name": "prime" + } + ] + }, + "bound_postfix_op": { + "type": "CHOICE", + "members": [ + { + "type": "PREC", + "value": "15-15", + "content": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "lhs", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + }, + { + "type": "FIELD", + "name": "symbol", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "sup_plus" + }, + { + "type": "SYMBOL", + "name": "asterisk" + }, + { + "type": "SYMBOL", + "name": "sup_hash" + }, + { + "type": "SYMBOL", + "name": "prime" + } + ] + } + } + ] + } + } + ] + }, + "assumption": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "ASSUME" + }, + { + "type": "STRING", + "value": "ASSUMPTION" + }, + { + "type": "STRING", + "value": "AXIOM" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "SYMBOL", + "name": "def_eq" + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "theorem": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "THEOREM" + }, + { + "type": "STRING", + "value": "PROPOSITION" + }, + { + "type": "STRING", + "value": "LEMMA" + }, + { + "type": "STRING", + "value": "COROLLARY" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "SYMBOL", + "name": "def_eq" + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "assume_prove" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_proof" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "assume_prove": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "ASSUME" + }, + { + "type": "FIELD", + "name": "assumption", + "content": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "new" + }, + { + "type": "SYMBOL", + "name": "inner_assume_prove" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "new" + }, + { + "type": "SYMBOL", + "name": "inner_assume_prove" + } + ] + } + ] + } + } + ] + } + }, + { + "type": "STRING", + "value": "PROVE" + }, + { + "type": "FIELD", + "name": "conclusion", + "content": { + "type": "SYMBOL", + "name": "_expr" + } + } + ] + }, + "inner_assume_prove": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "label_as" + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "SYMBOL", + "name": "assume_prove" + } + ] + }, + "new": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "NEW" + }, + { + "type": "SYMBOL", + "name": "level" + }, + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "NEW" + }, + { + "type": "SYMBOL", + "name": "level" + } + ] + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "set_in" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + { + "type": "SYMBOL", + "name": "_id_or_op_declaration" + } + ] + } + ] + }, + "level": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "CONSTANT" + }, + { + "type": "STRING", + "value": "VARIABLE" + }, + { + "type": "STRING", + "value": "STATE" + }, + { + "type": "STRING", + "value": "ACTION" + }, + { + "type": "STRING", + "value": "TEMPORAL" + } + ] + }, + "_proof": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "terminal_proof" + }, + { + "type": "SYMBOL", + "name": "non_terminal_proof" + } + ] + }, + "terminal_proof": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "PROOF" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "BY" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "ONLY" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "SYMBOL", + "name": "use_body" + } + ] + }, + { + "type": "STRING", + "value": "OBVIOUS" + }, + { + "type": "STRING", + "value": "OMITTED" + } + ] + } + ] + }, + "non_terminal_proof": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "PROOF" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "SYMBOL", + "name": "_begin_proof" + }, + { + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "proof_step" + } + }, + { + "type": "SYMBOL", + "name": "qed_step" + } + ] + }, + "proof_step": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_begin_proof_step" + }, + { + "type": "SYMBOL", + "name": "proof_step_id" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "definition_proof_step" + }, + { + "type": "SYMBOL", + "name": "have_proof_step" + }, + { + "type": "SYMBOL", + "name": "witness_proof_step" + }, + { + "type": "SYMBOL", + "name": "take_proof_step" + }, + { + "type": "SYMBOL", + "name": "suffices_proof_step" + }, + { + "type": "SYMBOL", + "name": "case_proof_step" + }, + { + "type": "SYMBOL", + "name": "pick_proof_step" + }, + { + "type": "SYMBOL", + "name": "use_or_hide" + }, + { + "type": "SYMBOL", + "name": "instance" + } + ] + } + ] + }, + "definition_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "DEFINE" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "REPEAT1", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "operator_definition" + }, + { + "type": "SYMBOL", + "name": "function_definition" + }, + { + "type": "SYMBOL", + "name": "module_definition" + } + ] + } + } + ] + }, + "have_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "HAVE" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "witness_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "WITNESS" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + } + ] + }, + "take_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "TAKE" + }, + { + "type": "SYMBOL", + "name": "_bound_or_identifier_list" + } + ] + }, + "suffices_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "SUFFICES" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "assume_prove" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_proof" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "case_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "CASE" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_proof" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pick_proof_step": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "PICK" + }, + { + "type": "SYMBOL", + "name": "_bound_or_identifier_list" + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_proof" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "_bound_or_identifier_list": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "quantifier_bound" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "quantifier_bound" + } + ] + } + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + } + ] + } + ] + }, + "qed_step": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_begin_proof_step" + }, + { + "type": "SYMBOL", + "name": "proof_step_id" + }, + { + "type": "STRING", + "value": "QED" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_proof" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "use_or_hide": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "USE" + }, + { + "type": "STRING", + "value": "HIDE" + } + ] + }, + { + "type": "SYMBOL", + "name": "use_body" + } + ] + }, + "use_body": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "use_body_expr" + }, + { + "type": "SYMBOL", + "name": "use_body_def" + }, + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "use_body_expr" + }, + { + "type": "SYMBOL", + "name": "use_body_def" + } + ] + } + ] + }, + "use_body_expr": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "module_ref" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "SYMBOL", + "name": "module_ref" + } + ] + } + ] + } + } + ] + }, + "use_body_def": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "DEF" + }, + { + "type": "STRING", + "value": "DEFS" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_op_or_expr" + }, + { + "type": "SYMBOL", + "name": "module_ref" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_op_or_expr" + }, + { + "type": "SYMBOL", + "name": "module_ref" + } + ] + } + ] + } + } + ] + } + ] + }, + "module_ref": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "MODULE" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + } + ] + }, + "proof_step_id": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "<" + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "\\d+|\\+|\\*" + } + }, + "named": true, + "value": "level" + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "STRING", + "value": ">" + } + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "[\\w|\\d]*" + } + }, + "named": true, + "value": "name" + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "\\.*" + } + } + ] + }, + "proof_step_ref": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "<" + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "\\d+|\\*" + } + }, + "named": true, + "value": "level" + }, + { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "STRING", + "value": ">" + } + }, + { + "type": "ALIAS", + "content": { + "type": "IMMEDIATE_TOKEN", + "content": { + "type": "PATTERN", + "value": "[\\w|\\d]+" + } + }, + "named": true, + "value": "name" + } + ] + }, + "pcal_algorithm": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_pcal_p_algorithm" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_algorithm" + } + ] + }, + "_pcal_p_algorithm": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_algorithm_start" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_var_decls" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_definitions" + }, + "named": true, + "value": "pcal_definitions" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_macro" + }, + "named": true, + "value": "pcal_macro" + } + }, + { + "type": "REPEAT", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_procedure" + }, + "named": true, + "value": "pcal_procedure" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "REPEAT1", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_process" + }, + "named": true, + "value": "pcal_process" + } + } + ] + }, + { + "type": "STRING", + "value": "end" + }, + { + "type": "STRING", + "value": "algorithm" + }, + { + "type": "SYMBOL", + "name": "_notify_pcal_algorithm_end" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "_pcal_c_algorithm": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_algorithm_start" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": "{" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_var_decls" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_definitions" + }, + "named": true, + "value": "pcal_definitions" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "REPEAT", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_macro" + }, + "named": true, + "value": "pcal_macro" + } + }, + { + "type": "REPEAT", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_procedure" + }, + "named": true, + "value": "pcal_procedure" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "REPEAT1", + "content": { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_process" + }, + "named": true, + "value": "pcal_process" + } + } + ] + }, + { + "type": "STRING", + "value": "}" + }, + { + "type": "SYMBOL", + "name": "_notify_pcal_algorithm_end" + } + ] + }, + "pcal_algorithm_start": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 2, + "content": { + "type": "STRING", + "value": "--algorithm" + } + } + }, + { + "type": "SYMBOL", + "name": "fair" + } + ] + }, + { + "type": "SYMBOL", + "name": "_notify_pcal_algorithm_start" + } + ] + }, + "fair": { + "type": "SEQ", + "members": [ + { + "type": "TOKEN", + "content": { + "type": "PREC", + "value": 2, + "content": { + "type": "STRING", + "value": "--fair" + } + } + }, + { + "type": "STRING", + "value": "algorithm" + } + ] + }, + "pcal_p_definitions": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "define" + }, + { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "_definition" + } + }, + { + "type": "STRING", + "value": "end" + }, + { + "type": "STRING", + "value": "define" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_c_definitions": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "define" + }, + { + "type": "STRING", + "value": "{" + }, + { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "_definition" + } + }, + { + "type": "STRING", + "value": "}" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_p_macro": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_macro_decl" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "STRING", + "value": "end" + }, + { + "type": "STRING", + "value": "macro" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_c_macro": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_macro_decl" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_macro_decl": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "macro" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "FIELD", + "name": "parameter", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + } + ] + } + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + "pcal_p_procedure": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_proc_decl" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "STRING", + "value": "end" + }, + { + "type": "STRING", + "value": "procedure" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_c_procedure": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_proc_decl" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_proc_decl": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "procedure" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_proc_var_decl" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "pcal_proc_var_decl" + } + ] + } + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": ")" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_proc_var_decls" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_p_process": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "fair" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "+" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": "process" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=" + }, + { + "type": "SYMBOL", + "name": "set_in" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_var_decls" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "STRING", + "value": "end" + }, + { + "type": "STRING", + "value": "process" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_c_process": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "fair" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "+" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": "process" + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=" + }, + { + "type": "SYMBOL", + "name": "set_in" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_var_decls" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_var_decls": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "variable" + }, + { + "type": "STRING", + "value": "variables" + } + ] + }, + { + "type": "SYMBOL", + "name": "pcal_var_decl" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "STRING", + "value": "," + } + ] + }, + { + "type": "SYMBOL", + "name": "pcal_var_decl" + } + ] + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_var_decl": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=" + }, + { + "type": "SYMBOL", + "name": "set_in" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_proc_var_decls": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "variable" + }, + { + "type": "STRING", + "value": "variables" + } + ] + }, + { + "type": "REPEAT1", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_proc_var_decl" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "STRING", + "value": "," + } + ] + } + ] + } + } + ] + }, + "pcal_proc_var_decl": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "=" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_p_algorithm_body": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "begin" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + } + ] + }, + "_pcal_p_stmts": { + "type": "SEQ", + "members": [ + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_pcal_p_stmt" + }, + { + "type": "STRING", + "value": ";" + } + ] + } + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmt" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_c_algorithm_body": { + "type": "SEQ", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "{" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + } + ] + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": ";" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": "}" + } + ] + } + ] + }, + "_pcal_p_stmt": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_pcal_label" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "SYMBOL", + "name": "_pcal_p_unlabeled_stmt" + } + ] + }, + "_pcal_c_stmt": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_pcal_label" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "_pcal_c_unlabeled_stmt" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_algorithm_body" + }, + "named": true, + "value": "pcal_algorithm_body" + } + ] + } + ] + }, + "_pcal_label": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "label", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "STRING", + "value": ":" + } + ] + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "+" + }, + { + "type": "STRING", + "value": "-" + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "_pcal_p_unlabeled_stmt": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_assign" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_if" + }, + "named": true, + "value": "pcal_if" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_while" + }, + "named": true, + "value": "pcal_while" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_either" + }, + "named": true, + "value": "pcal_either" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_p_with" + }, + "named": true, + "value": "pcal_with" + }, + { + "type": "SYMBOL", + "name": "pcal_await" + }, + { + "type": "SYMBOL", + "name": "pcal_print" + }, + { + "type": "SYMBOL", + "name": "pcal_assert" + }, + { + "type": "SYMBOL", + "name": "pcal_skip" + }, + { + "type": "SYMBOL", + "name": "pcal_return" + }, + { + "type": "SYMBOL", + "name": "pcal_goto" + }, + { + "type": "SYMBOL", + "name": "pcal_proc_call" + }, + { + "type": "SYMBOL", + "name": "pcal_macro_call" + } + ] + }, + "_pcal_c_unlabeled_stmt": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_assign" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_if" + }, + "named": true, + "value": "pcal_if" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_while" + }, + "named": true, + "value": "pcal_while" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_either" + }, + "named": true, + "value": "pcal_either" + }, + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "pcal_c_with" + }, + "named": true, + "value": "pcal_with" + }, + { + "type": "SYMBOL", + "name": "pcal_await" + }, + { + "type": "SYMBOL", + "name": "pcal_print" + }, + { + "type": "SYMBOL", + "name": "pcal_assert" + }, + { + "type": "SYMBOL", + "name": "pcal_skip" + }, + { + "type": "SYMBOL", + "name": "pcal_return" + }, + { + "type": "SYMBOL", + "name": "pcal_goto" + }, + { + "type": "SYMBOL", + "name": "pcal_proc_call" + }, + { + "type": "SYMBOL", + "name": "pcal_macro_call" + } + ] + }, + "pcal_assign": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pcal_lhs" + }, + { + "type": "SYMBOL", + "name": "assign" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "vertvert" + }, + { + "type": "SYMBOL", + "name": "pcal_lhs" + }, + { + "type": "SYMBOL", + "name": "assign" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + "pcal_lhs": { + "type": "SEQ", + "members": [ + { + "type": "ALIAS", + "content": { + "type": "SYMBOL", + "name": "identifier" + }, + "named": true, + "value": "identifier_ref" + }, + { + "type": "REPEAT", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "[" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + }, + { + "type": "STRING", + "value": "]" + } + ] + }, + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "." + }, + { + "type": "SYMBOL", + "name": "identifier" + } + ] + } + ] + } + } + ] + }, + "pcal_p_if": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "if" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "then" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "elsif" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "then" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + } + ] + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "else" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "ALIAS", + "content": { + "type": "STRING", + "value": "end" + }, + "named": true, + "value": "pcal_end_if" + }, + { + "type": "STRING", + "value": "if" + } + ] + }, + "pcal_c_if": { + "type": "PREC_RIGHT", + "value": 0, + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "if" + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "else" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + } + }, + "pcal_p_while": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "while" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": "do" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + }, + { + "type": "ALIAS", + "content": { + "type": "STRING", + "value": "end" + }, + "named": true, + "value": "pcal_end_while" + }, + { + "type": "STRING", + "value": "while" + } + ] + }, + "pcal_c_while": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "while" + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "STRING", + "value": ")" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + } + ] + }, + "pcal_p_either": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "either" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + }, + { + "type": "REPEAT1", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "or" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + } + ] + } + }, + { + "type": "ALIAS", + "content": { + "type": "STRING", + "value": "end" + }, + "named": true, + "value": "pcal_end_either" + }, + { + "type": "STRING", + "value": "either" + } + ] + }, + "pcal_c_either": { + "type": "PREC_RIGHT", + "value": 0, + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "either" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + }, + { + "type": "REPEAT1", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "or" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + } + ] + } + } + ] + } + }, + "pcal_p_with": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "with" + }, + { + "type": "SYMBOL", + "name": "_pcal_with_vars" + }, + { + "type": "STRING", + "value": "do" + }, + { + "type": "SYMBOL", + "name": "_pcal_p_stmts" + }, + { + "type": "ALIAS", + "content": { + "type": "STRING", + "value": "end" + }, + "named": true, + "value": "pcal_end_with" + }, + { + "type": "STRING", + "value": "with" + } + ] + }, + "pcal_c_with": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "with" + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "_pcal_with_vars" + }, + { + "type": "STRING", + "value": ")" + }, + { + "type": "SYMBOL", + "name": "_pcal_c_stmt" + } + ] + }, + "_pcal_with_vars": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=" + }, + { + "type": "SYMBOL", + "name": "set_in" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "STRING", + "value": ";" + } + ] + }, + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=" + }, + { + "type": "SYMBOL", + "name": "set_in" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "STRING", + "value": ";" + } + ] + }, + { + "type": "BLANK" + } + ] + } + ] + }, + "pcal_await": { + "type": "SEQ", + "members": [ + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "await" + }, + { + "type": "STRING", + "value": "when" + } + ] + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "pcal_print": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "print" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "pcal_assert": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "assert" + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + }, + "pcal_skip": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "skip" + } + ] + }, + "pcal_return": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "return" + } + ] + }, + "pcal_goto": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "goto" + }, + { + "type": "FIELD", + "name": "statement", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + } + ] + }, + "pcal_proc_call": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "call" + }, + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + "pcal_macro_call": { + "type": "SEQ", + "members": [ + { + "type": "FIELD", + "name": "name", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": "(" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "_expr" + }, + { + "type": "REPEAT", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "_expr" + } + ] + } + } + ] + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": ")" + } + ] + } + }, + "extras": [ + { + "type": "PATTERN", + "value": "\\s|\\r?\\n" + }, + { + "type": "SYMBOL", + "name": "comment" + }, + { + "type": "SYMBOL", + "name": "block_comment" + } + ], + "conflicts": [ + [ + "minus", + "negative" + ], + [ + "bound_prefix_op", + "prefix_op_symbol" + ], + [ + "bound_op", + "_subscript_expr" + ], + [ + "bound_op", + "prefixed_op" + ], + [ + "_expr", + "label" + ], + [ + "_expr", + "quantifier_bound" + ], + [ + "_expr", + "tuple_of_identifiers" + ], + [ + "_expr", + "operator_definition" + ], + [ + "_expr", + "_id_or_op_declaration", + "label" + ], + [ + "_expr", + "function_definition" + ], + [ + "subexpr_prefix" + ], + [ + "_expr", + "pcal_lhs" + ], + [ + "bound_infix_op", + "pcal_assign" + ] + ], + "precedences": [ + [ + { + "type": "STRING", + "value": "17-17" + }, + { + "type": "STRING", + "value": "16-16" + }, + { + "type": "STRING", + "value": "15-15" + }, + { + "type": "STRING", + "value": "14-14" + }, + { + "type": "STRING", + "value": "13-13" + }, + { + "type": "STRING", + "value": "12-12" + }, + { + "type": "STRING", + "value": "11-11" + }, + { + "type": "STRING", + "value": "10-10" + }, + { + "type": "STRING", + "value": "9-9" + }, + { + "type": "STRING", + "value": "8-8" + }, + { + "type": "STRING", + "value": "7-7" + }, + { + "type": "STRING", + "value": "6-6" + }, + { + "type": "STRING", + "value": "5-5" + }, + { + "type": "STRING", + "value": "4-4" + }, + { + "type": "STRING", + "value": "3-3" + }, + { + "type": "STRING", + "value": "2-2" + }, + { + "type": "STRING", + "value": "1-1" + }, + { + "type": "STRING", + "value": "0-0" + } + ] + ], + "externals": [ + { + "type": "SYMBOL", + "name": "leading_extramodular_text" + }, + { + "type": "SYMBOL", + "name": "trailing_extramodular_text" + }, + { + "type": "SYMBOL", + "name": "_indent" + }, + { + "type": "SYMBOL", + "name": "_bullet" + }, + { + "type": "SYMBOL", + "name": "_dedent" + }, + { + "type": "SYMBOL", + "name": "_begin_proof" + }, + { + "type": "SYMBOL", + "name": "_begin_proof_step" + }, + { + "type": "STRING", + "value": "PROOF" + }, + { + "type": "STRING", + "value": "BY" + }, + { + "type": "STRING", + "value": "OBVIOUS" + }, + { + "type": "STRING", + "value": "OMITTED" + }, + { + "type": "STRING", + "value": "QED" + }, + { + "type": "STRING", + "value": "WF_" + }, + { + "type": "STRING", + "value": "SF_" + }, + { + "type": "SYMBOL", + "name": "_notify_pcal_algorithm_start" + }, + { + "type": "SYMBOL", + "name": "_notify_pcal_algorithm_end" + }, + { + "type": "SYMBOL", + "name": "_error_sentinel" + } + ], + "inline": [], + "supertypes": [ + "_unit", + "_expr", + "_op", + "_proof", + "_number", + "_primitive_value_set" + ] +} + +' +] + +{ #category : #properties } +SBTlaplus class >> highlightQuery [ + + " https://github.com/tlaplus-community/tree-sitter-tlaplus/blob/master/src/queries/highlights.scm " + ^ '; ; Intended for consumption by GitHub and the tree-sitter highlight command +; ; Default capture names found here: +; ; https://github.com/tree-sitter/tree-sitter/blob/f5d1c0b8609f8697861eab352ead44916c068c74/cli/src/highlight.rs#L150-L171 +; ; In this file, captures defined earlier take precedence over captures defined later. + +; TLA⁺ Keywords +[ + "ACTION" + "ASSUME" + "ASSUMPTION" + "AXIOM" + "BY" + "CASE" + "CHOOSE" + "CONSTANT" + "CONSTANTS" + "COROLLARY" + "DEF" + "DEFINE" + "DEFS" + "DOMAIN" + "ELSE" + "ENABLED" + "EXCEPT" + "EXTENDS" + "HAVE" + "HIDE" + "IF" + "IN" + "INSTANCE" + "LAMBDA" + "LEMMA" + "LET" + "LOCAL" + "MODULE" + "NEW" + "OBVIOUS" + "OMITTED" + "ONLY" + "OTHER" + "PICK" + "PROOF" + "PROPOSITION" + "PROVE" + "QED" + "RECURSIVE" + "SF_" + "STATE" + "SUBSET" + "SUFFICES" + "TAKE" + "TEMPORAL" + "THEN" + "THEOREM" + "UNCHANGED" + "UNION" + "USE" + "VARIABLE" + "VARIABLES" + "WF_" + "WITH" + "WITNESS" + (address) + (all_map_to) + (assign) + (case_arrow) + (case_box) + (def_eq) + (exists) + (forall) + (gets) + (label_as) + (maps_to) + (set_in) + (temporal_exists) + (temporal_forall) +] @keyword + +; PlusCal keywords +[ + "algorithm" + "assert" + "await" + "begin" + "call" + "define" + "either" + "else" + "elsif" + "end" + "fair" + "goto" + "if" + "macro" + "or" + "print" + "procedure" + "process" + "return" + "skip" + "variable" + "variables" + "when" + "with" + "then" + (pcal_algorithm_start) + (pcal_end_either) + (pcal_end_if) + (pcal_process ("=")) + (pcal_with ("=")) +] @keyword + +; Literals +(binary_number (format) @keyword) +(binary_number (value) @number) +(boolean) @number +(boolean_set) @type +(hex_number (format) @keyword) +(hex_number (value) @number) +(int_number_set) @type +(nat_number) @number +(nat_number_set) @type +(octal_number (format) @keyword) +(octal_number (value) @number) +(real_number) @number +(real_number_set) @type +(string) @string +(escape_char) @string.special +(string_set) @type + +; Namespaces and includes +(extends (identifier_ref) @module) +(instance (identifier_ref) @module) +(module name: (_) @module) +(pcal_algorithm name: (identifier) @module) + +; Constants and variables +(constant_declaration (identifier) @constant) +(constant_declaration (operator_declaration name: (_) @constant)) +(pcal_var_decl (identifier) @variable.builtin) +(pcal_with (identifier) @variable.parameter) +((".") . (identifier) @attribute) +(record_literal (identifier) @attribute) +(set_of_records (identifier) @attribute) +(variable_declaration (identifier) @variable.builtin) + +; Parameters +(choose (identifier) @variable.parameter) +(choose (tuple_of_identifiers (identifier) @variable.parameter)) +(lambda (identifier) @variable.parameter) +(module_definition (operator_declaration name: (_) @variable.parameter)) +(module_definition parameter: (identifier) @variable.parameter) +(operator_definition (operator_declaration name: (_) @variable.parameter)) +(operator_definition parameter: (identifier) @variable.parameter) +(pcal_macro_decl parameter: (identifier) @variable.parameter) +(pcal_proc_var_decl (identifier) @variable.parameter) +(quantifier_bound (identifier) @variable.parameter) +(quantifier_bound (tuple_of_identifiers (identifier) @variable.parameter)) +(unbounded_quantification (identifier) @variable.parameter) + +; Operators, functions, and macros +(function_definition name: (identifier) @function) +(module_definition name: (_) @module) +(operator_definition name: (_) @operator) +(pcal_macro_decl name: (identifier) @function) +(pcal_macro_call name: (identifier) @function) +(pcal_proc_decl name: (identifier) @function) +(pcal_process name: (identifier) @function) +(recursive_declaration (identifier) @operator) +(recursive_declaration (operator_declaration name: (_) @operator)) + +; Delimiters +[ + (langle_bracket) + (rangle_bracket) + (rangle_bracket_sub) + "{" + "}" + "[" + "]" + "]_" + "(" + ")" +] @punctuation.bracket +[ + "," + ":" + "." + "!" + ";" + (bullet_conj) + (bullet_disj) + (prev_func_val) + (placeholder) +] @punctuation.delimiter + +; Proofs +(assume_prove (new (identifier) @variable.parameter)) +(assume_prove (new (operator_declaration name: (_) @variable.parameter))) +(assumption name: (identifier) @constant) +(pick_proof_step (identifier) @variable.parameter) +(proof_step_id "<" @punctuation.bracket) +(proof_step_id (level) @tag) +(proof_step_id (name) @tag) +(proof_step_id ">" @punctuation.bracket) +(proof_step_ref "<" @punctuation.bracket) +(proof_step_ref (level) @tag) +(proof_step_ref (name) @tag) +(proof_step_ref ">" @punctuation.bracket) +(take_proof_step (identifier) @variable.parameter) +(theorem name: (identifier) @constant) + +; Comments and tags +(block_comment "(*" @comment) +(block_comment "*)" @comment) +(block_comment_text) @comment +(comment) @comment +(single_line) @comment +(_ label: (identifier) @tag) +(label name: (_) @tag) +(pcal_goto statement: (identifier) @tag) + +; Put these last so they are overridden by everything else +(bound_infix_op symbol: (_) @function.builtin) +(bound_nonfix_op symbol: (_) @function.builtin) +(bound_postfix_op symbol: (_) @function.builtin) +(bound_prefix_op symbol: (_) @function.builtin) +((prefix_op_symbol) @function.builtin) +((infix_op_symbol) @function.builtin) +((postfix_op_symbol) @function.builtin) + +; Reference highlighting +(identifier_ref) @variable.reference +((prefix_op_symbol) @variable.reference) +(bound_prefix_op symbol: (_) @variable.reference) +((infix_op_symbol) @variable.reference) +(bound_infix_op symbol: (_) @variable.reference) +((postfix_op_symbol) @variable.reference) +(bound_postfix_op symbol: (_) @variable.reference) +(bound_nonfix_op symbol: (_) @variable.reference) +' +] + +{ #category : #configuration } +SBTlaplus class >> language [ + + ^ #tlaplus +] + +{ #category : #configuration } +SBTlaplus class >> rootRuleName [ + + ^ 'source_file' +] diff --git a/packages/Sandblocks-Tlaplus/package.st b/packages/Sandblocks-Tlaplus/package.st new file mode 100644 index 0000000..f079fb2 --- /dev/null +++ b/packages/Sandblocks-Tlaplus/package.st @@ -0,0 +1 @@ +Package { #name : #'Sandblocks-Tlaplus' } diff --git a/packages/Sandblocks-TreeSitter/SBTSLanguage.class.st b/packages/Sandblocks-TreeSitter/SBTSLanguage.class.st index 498a5fa..b4bdf2e 100644 --- a/packages/Sandblocks-TreeSitter/SBTSLanguage.class.st +++ b/packages/Sandblocks-TreeSitter/SBTSLanguage.class.st @@ -4,6 +4,9 @@ Class { #instVars : [ 'grammar' ], + #classVars : [ + 'RawGrammar' + ], #classInstVars : [ 'instance' ],