pull up a bunch of NNFParser methods to FixpointParser

shingarov · Oct 16, 2024 · 150cd2c · 150cd2c
1 parent 10ca107
commit 150cd2c
Show file tree

Hide file tree

Showing 2 changed files with 54 additions and 54 deletions.
diff --git a/src/Refinements-Parsing/FixpointParser.class.st b/src/Refinements-Parsing/FixpointParser.class.st
@@ -20,6 +20,15 @@ FixpointParser class >> upperId [
 	^(#uppercase asParser, (#word asParser / $_ asParser) star) flatten
 ]
 
+{ #category : #grammar }
+FixpointParser >> fTyCon [
+	^ ('Int' asParser ==> [ :x | Int tyCon ])
+	/ ('int' asParser ==> [ :x | Int tyCon ])
+	/ ('Bool' asParser ==> [ :x | Bool tyCon ])
+	/ ('bool' asParser ==> [ :x | Bool tyCon ])
+	/ (NNFParser upperId ==> [ :x | x symbolFTycon ])
+]
+
 { #category : #grammar }
 FixpointParser >> fixpoint [
 	^'fixpoint' asParser trim,
@@ -37,11 +46,43 @@ FixpointParser >> fixpoint [
 	
 ]
 
+{ #category : #grammar }
+FixpointParser >> funcSort [
+	"Parser for function sorts without the 'func' keyword"
+	^(
+	PPParser decimalNat,
+	$, asParser trim,
+	sort semicolonSeparated brackets
+	) parens
+	==> [ :x | Z3Sort mkFFunc: x first sorts: x third ]
+]
+
 { #category : #'grammar - util' }
 FixpointParser >> matchedParen [
 	^(PPParser nonParen / matchedParen parens) plus flatten
 ]
 
+{ #category : #grammar }
+FixpointParser >> sort [
+	^ self sort′: sortArg trim star
+]
+
+{ #category : #grammar }
+FixpointParser >> sortArg [
+	^ self sort′: nil asParser
+]
+
+{ #category : #grammar }
+FixpointParser >> sort′: aSortArgParser [
+	| sap |
+	sap := aSortArgParser ==> [ :args | args ifNil: [ #() ] ]. "aSortArgParser can be EpsilonParser"
+	^ sort parens
+	/ ('func' asParser, funcSort ==> [ :x | x second ])
+	/ (sort brackets ==> [ :x | x shouldBeImplemented listFTyCon  ])
+	/ (self fTyCon trim, sap ==> [ :x | x first fAppTC: x second ])
+	/ (self tvar trim, sap ==> [ :x | x first fApp: x second ])
+]
+
 { #category : #'grammar - util' }
 FixpointParser >> tok [
 	^(PPPredicateObjectParser
@@ -50,3 +91,15 @@ FixpointParser >> tok [
 		message: 'Token expected') plus flatten
 		
 ]
+
+{ #category : #grammar }
+FixpointParser >> tvar [
+	^ self varSort
+	/ ($` asParser, #lowercase asParser ==> [ :x | Z3Sort uninterpretedSortNamed: (String with: x second) ])
+]
+
+{ #category : #grammar }
+FixpointParser >> varSort [
+	^'@(' asParser, PPParser decimalInteger, ')' asParser
+	==> [ :x | FVar new: x second ]
+]
diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st
@@ -90,15 +90,6 @@ NNFParser >> exists [
 	==> [ :x | CstrAny bind: x second p: x third ]
 ]
 
-{ #category : #grammar }
-NNFParser >> fTyCon [
-	^ ('Int' asParser ==> [ :x | Int tyCon ])
-	/ ('int' asParser ==> [ :x | Int tyCon ])
-	/ ('Bool' asParser ==> [ :x | Bool tyCon ])
-	/ ('bool' asParser ==> [ :x | Bool tyCon ])
-	/ (NNFParser upperId ==> [ :x | x symbolFTycon ])
-]
-
 { #category : #grammar }
 NNFParser >> forall [
 	^'forall' asParser trim,
@@ -107,17 +98,6 @@ NNFParser >> forall [
 	==> [ :x | CstrAll bind: x second p: x third ]
 ]
 
-{ #category : #grammar }
-NNFParser >> funcSort [
-	"Parser for function sorts without the 'func' keyword"
-	^(
-	PPParser decimalNat,
-	$, asParser trim,
-	sort semicolonSeparated brackets
-	) parens
-	==> [ :x | Z3Sort mkFFunc: x first sorts: x third ]
-]
-
 { #category : #grammar }
 NNFParser >> hBind [
 	^symSort parens trim, pred parens
@@ -163,33 +143,12 @@ NNFParser >> qualif [
 
 ]
 
-{ #category : #grammar }
-NNFParser >> sort [
-	^ self sort′: sortArg trim star
-]
-
-{ #category : #grammar }
-NNFParser >> sortArg [
-	^ self sort′: nil asParser
-]
-
-{ #category : #grammar }
-NNFParser >> sort′: aSortArgParser [
-	| sap |
-	sap := aSortArgParser ==> [ :args | args ifNil: [ #() ] ]. "aSortArgParser can be EpsilonParser"
-	^ sort parens
-	/ ('func' asParser, funcSort ==> [ :x | x second ])
-	/ (sort brackets ==> [ :x | x shouldBeImplemented listFTyCon  ])
-	/ (self fTyCon trim, sap ==> [ :x | x first fAppTC: x second ])
-	/ (self tvar trim, sap ==> [ :x | x first fApp: x second ])
-]
-
 { #category : #grammar }
 NNFParser >> start [
 	^thing trim star end ==> [ :x | HornQuery fromThings: x ]
 ]
 
-{ #category : #'grammar - util' }
+{ #category : #grammar }
 NNFParser >> symSort [
 	^self tok trim, sort
 ]
@@ -199,12 +158,6 @@ NNFParser >> thing [
 	^(constraint / var / qualif / constant / self fixpoint / define "match data") parens
 ]
 
-{ #category : #grammar }
-NNFParser >> tvar [
-	^ self varSort
-	/ ($` asParser, #lowercase asParser ==> [ :x | Z3Sort uninterpretedSortNamed: (String with: x second) ])
-]
-
 { #category : #grammar }
 NNFParser >> var [
 	^'var' asParser trim,
@@ -213,9 +166,3 @@ NNFParser >> var [
 	==> [ :x | HVar name: x second argSorts: x third ]
 
 ]
-
-{ #category : #grammar }
-NNFParser >> varSort [
-	^'@(' asParser, PPParser decimalInteger, ')' asParser
-	==> [ :x | FVar new: x second ]
-]