From 9e920ea157cb4248aad5d80d39fb8798fa4e10ae Mon Sep 17 00:00:00 2001 From: Boris Shingarov Date: Fri, 9 Aug 2024 14:19:51 -0400 Subject: [PATCH] =?UTF-8?q?Implement=20parsing=20of=20(data=E2=80=A6)=20in?= =?UTF-8?q?=20NNF=20queries?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Refinements-Parsing/NNFParser.class.st | 34 ++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st index 37a34b53f..7848fe56b 100644 --- a/src/Refinements-Parsing/NNFParser.class.st +++ b/src/Refinements-Parsing/NNFParser.class.st @@ -25,7 +25,8 @@ Class { 'cstrPred', 'funcSort', 'sortArg', - 'define' + 'define', + 'data' ], #category : #'Refinements-Parsing' } @@ -79,6 +80,35 @@ NNFParser >> cstrPred [ ^pred parens ==> [ :x | CstrHead pred: x ] ] +{ #category : #grammar } +NNFParser >> data [ + ^'data' asParser trim, + self fTyCon trim, + (#digit asParser plus flatten trim ==> #asInteger), + $= asParser trim, + ($| asParser trim, self dataCtor trim ==> #second) star brackets + ==> [ :x | DataDecl + ddTyCon: x second + ddVars: x third + ddCtors: x fifth ] + +] + +{ #category : #grammar } +NNFParser >> dataCtor [ + ^NNFParser upperId trim, + (self dataField commaSeparated optional ==> [ :x | x ifNil: [#()] ifNotNil: [x] ]) braces + ==> [ :x | DataCtor dcName: x first dcFields: x second ] +] + +{ #category : #grammar } +NNFParser >> dataField [ + ^ NNFParser upperId trim, + $: asParser trim, + sort + ==> [ :x | DataField dfName: x first dfSort: x last ] +] + { #category : #grammar } NNFParser >> decidablePred [ ^matchedParen @@ -234,7 +264,7 @@ NNFParser >> symSort [ { #category : #grammar } NNFParser >> thing [ - ^(constraint / var / qualif / constant / fixpoint / define "match data") parens + ^(constraint / var / qualif / constant / fixpoint / define "/ match" / data) parens ] { #category : #'grammar - util' }