Overhaul NNFParser

The initial objective of this work has been to factor common (non-Horn)
elements ouf of NNFParser to FixpointParser (so that the latter would
serve as a common superclass for NNFParser and FQParser, see #363).
As the work progressed, two other defects became evident: nomenclature
inconsistent with LiquidFixpoint, and the use of (extremely broken)
matchedParen even though we already have RefinementExpressionParser.
This commit addresses all three issues.

This is a combination of 23 commits:
Introduce FixpointParser which will serve as the common superclass of NNFParser/FQParser
Pull 'fixpoint' up to FixpointParser
Pull matchedParen and tok up to FixpointParser
Pull lowerId, upperId up to FixpointParser class
Consistently name hThing
Place parens in symSort (not its senders) for consistency with LF
Use naming for hCstr consistent with LF
Inline cstrAnd for consistency with LF
Parenthesize hBind consistently with LF
Inline #forall, #exists for consistency with LF
[cosmetic] Add "tag" TODO
Use naming for hCstr consistent with LF
Use naming for hPred consistent with LF
Inline predAnd for consistency with LF
Inline kappaApp, use kvSym for consistency with LF
Clear up confusion between pred, hPred and decidablePred
Inline #constant for consistency with LF
Rename qualif to hQualifier for consistency and to avoid confusion with F.qualifierP
Inline #constraint for consistency with LF
Rename var to hVar for consistency with LF
Pull common (i.e. non-Horn) elements from NNFParser to FixpointParser
Remove #matchedParen in favor of consistent use of RefinementExpressionParser
Route uses of RefinementExpressionParser through DecidableRefinement

src/Refinements-Parsing/DecidableRefinement.extension.st

@@ -0,0 +1,7 @@
+Extension { #name : #DecidableRefinement }
+
+{ #category : #'*Refinements-Parsing' }
+DecidableRefinement class >> parser [
+	^ RefinementExpressionParser new
+	==> [ :x | self text: x formattedCode ]
+]

src/Refinements-Parsing/FixpointParser.class.st

@@ -0,0 +1,105 @@
+Class {
+	#name : #FixpointParser,
+	#superclass : #PPCompositeParser,
+	#instVars : [
+		'sort',
+		'sortArg',
+		'funcSort',
+		'pred'
+	],
+	#category : #'Refinements-Parsing'
+}
+
+{ #category : #grammar }
+FixpointParser class >> lowerId [
+	^(#lowercase asParser, (#word asParser / $_ asParser) star) flatten
+]
+
+{ #category : #grammar }
+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 ==> #symbolFTycon)
+]
+
+{ #category : #grammar }
+FixpointParser >> fixpoint [
+	^'fixpoint' asParser trim,
+	'"--' asParser,
+	('eliminate' asParser / 'rewrite' asParser / 'save' asParser / 'fuel' asParser),
+	($= asParser, #word asParser plus flatten) optional,
+	$" asParser
+	==> [ :x |
+		| selector |
+		selector := x third asSymbol.
+		x fourth isNil
+			ifTrue: [ HOpt perform: selector ]
+			ifFalse: [ HOpt perform: selector, ':' with: x fourth second ]
+	]
+	
+]
+
+{ #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 }
+FixpointParser >> pred [
+	^DecidableRefinement parser
+]
+
+{ #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 }
+FixpointParser >> tok [
+	^(PPPredicateObjectParser
+		on: (PPCharSetPredicate on: [ :ch |
+					(ch isSeparator or: [ ch == $( or: [ ch == $) ]]) not ])
+		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 ]
+]