From a1ae5c1beaf2389ebb49947a1d0535bfffce93eb Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Thu, 17 Oct 2024 03:10:35 -0400
Subject: [PATCH] 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
---
 .../DecidableRefinement.extension.st          |   7 +
 .../FixpointParser.class.st                   | 105 ++++++++
 src/Refinements-Parsing/NNFParser.class.st    | 255 ++++--------------
 src/Refinements-Tests/HornPosTest.class.st    |  23 --
 src/SpriteLang/RefinementParser.class.st      |   4 +-
 5 files changed, 162 insertions(+), 232 deletions(-)
 create mode 100644 src/Refinements-Parsing/DecidableRefinement.extension.st
 create mode 100644 src/Refinements-Parsing/FixpointParser.class.st

diff --git a/src/Refinements-Parsing/DecidableRefinement.extension.st b/src/Refinements-Parsing/DecidableRefinement.extension.st
new file mode 100644
index 000000000..a27a960c7
--- /dev/null
+++ b/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 ]
+]
diff --git a/src/Refinements-Parsing/FixpointParser.class.st b/src/Refinements-Parsing/FixpointParser.class.st
new file mode 100644
index 000000000..0931d5136
--- /dev/null
+++ b/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 ]
+]
diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st
index 1aaf90e60..c0d34494c 100644
--- a/src/Refinements-Parsing/NNFParser.class.st
+++ b/src/Refinements-Parsing/NNFParser.class.st
@@ -1,199 +1,66 @@
 Class {
 	#name : #NNFParser,
-	#superclass : #PPCompositeParser,
+	#superclass : #FixpointParser,
 	#instVars : [
-		'fixpoint',
-		'constraint',
-		'tok',
-		'thing',
-		'cstrAnd',
-		'forall',
-		'exists',
-		'cstr',
-		'var',
-		'sort',
-		'qualif',
-		'constant',
+		'hCstr',
 		'hBind',
 		'symSort',
-		'pred',
-		'kappaApp',
-		'kappa',
-		'predAnd',
-		'decidablePred',
-		'matchedParen',
-		'cstrPred',
-		'funcSort',
-		'sortArg',
+		'hPred',
 		'define'
 	],
 	#category : #'Refinements-Parsing'
 }
 
-{ #category : #grammar }
-NNFParser class >> lowerId [
-	^(#lowercase asParser, (#word asParser / $_ asParser) star) flatten
-]
-
-{ #category : #grammar }
-NNFParser class >> upperId [
-	^(#uppercase asParser, (#word asParser / $_ asParser) star) flatten
-]
-
-{ #category : #grammar }
-NNFParser >> constant [
-	^'constant' asParser trim,
-	tok trim, "name"
-	sort
-	==> [ :x | HCon symbol: x second sort: x third ]
-	
-]
-
-{ #category : #grammar }
-NNFParser >> constraint [
-	^'constraint' asParser trim,
-	cstr parens
-	==> [ :x | x second ]
-	
-]
-
-{ #category : #grammar }
-NNFParser >> cstr [
-	^cstrAnd / forall / exists / cstrPred
-]
-
-{ #category : #grammar }
-NNFParser >> cstrAnd [
-	^'and' asParser trim,
-	cstr parens trim star ==> [ :x | CstrAnd of: x second ]
-]
-
-{ #category : #grammar }
-NNFParser >> cstrPred [
-	^pred parens ==> [ :x | CstrHead pred: x ]
-]
-
-{ #category : #grammar }
-NNFParser >> decidablePred [
-	^matchedParen
-	==> [ :x | HReft expr: (DecidableRefinement text: x) ]
-]
-
 { #category : #grammar }
 NNFParser >> define [
 	"Function definition equations (PLE).
 	 Cf. top-level Parse.hs"
 	^'define' asParser trim,
-	tok trim, "name"
-	(tok trim, $: asParser trim, sort ==> [ :eachArg | eachArg first -> eachArg last ]) commaList trim,
+	self tok trim, "name"
+	(self tok trim, $: asParser trim, sort ==> [ :eachArg | eachArg first -> eachArg last ]) commaList trim,
 	$: asParser trim,
 	sort,
 	'=' asParser trim,
-	(RefinementExpressionParser new braces ==> [ :seq | seq formattedCode ])
+	(DecidableRefinement parser braces)
 	==> [ :x | Equation
 					mkEquation: x second
 					args: x third
-					expr: (DecidableRefinement text: x seventh)
+					expr: x seventh
 					sort: x fifth ]
 ]
 
-{ #category : #grammar }
-NNFParser >> exists [
-	^'exists' asParser trim,
-	hBind parens trim,
-	cstr parens trim
-	"'(and)' asParser"
-	==> [ :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 >> 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 }
-NNFParser >> forall [
-	^'forall' asParser trim,
-	hBind parens trim,
-	cstr parens
-	==> [ :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
+	^(symSort trim, hPred) parens
 	==> [ :x | HBind x: x first first τ: x first second p: x second ]
 ]
 
 { #category : #grammar }
-NNFParser >> kappa [
-	^('$' asParser,
-	($# asParser ==> [:x|$º] / #word asParser / $_ asParser) plus)
-	==> [ :x | String withAll: x second ]
-]
-
-{ #category : #grammar }
-NNFParser >> kappaApp [
-	^(kappa,
-	((#blank asParser plus), tok ==> [:x| x second]) plus) trim
-	==> [ :x | RefVarApp var: x first args: x second ]
-]
-
-{ #category : #'grammar - util' }
-NNFParser >> matchedParen [
-	^(PPParser nonParen / matchedParen parens) plus flatten
-]
-
-{ #category : #grammar }
-NNFParser >> pred [
-	^predAnd / kappaApp / decidablePred
+NNFParser >> hCstr [
+	^(
+		  ('and' asParser trim, hCstr trim star ==> [ :x | CstrAnd of: x second ])
+		/ ('forall' asParser trim, hBind trim, hCstr trim ==> [ :x | CstrAll bind: x second p: x third ])
+		/ ('exists' asParser trim, hBind trim, hCstr trim ==> [ :x | CstrAny bind: x second p: x third ])
+		"TODO: / tag"
+		/ (hPred ==> [ :x | CstrHead pred: x ])
+	) parens
 ]
 
 { #category : #grammar }
-NNFParser >> predAnd [
-	^'and' asParser,
-	(#blank asParser plus, pred parens ==> [:x| x second]) star 
-	==> [ :x | HPredAnd of: x second ]
+NNFParser >> hPred [
+	^(
+		  ('and' asParser, 	(#blank asParser plus, hPred ==> #second) star ==> [ :x | HPredAnd of: x second ])
+		/ (self kvSym, ((#blank asParser plus), self tok ==> [:x| x second]) plus ==> [ :x | RefVarApp var: x first args: x second ])
+		/ (pred ==> [ :x | HReft expr: x ])
+	) parens
 ]
 
 { #category : #grammar }
-NNFParser >> qualif [
+NNFParser >> hQualifier [
 	^'qualif' asParser trim,
 	NNFParser upperId trim, "name"
-	symSort parens trim plus parens trim, "params"
-	pred parens "body"
+	symSort trim plus parens trim, "params"
+	hPred "body"
 	==> [ :x | Qualifier
 		name: x second
 		params: (x third collect: [ :p | QualParam symbol: p first sort: p second ])
@@ -202,67 +69,41 @@ NNFParser >> qualif [
 ]
 
 { #category : #grammar }
-NNFParser >> sort [
-	^ self sort′: sortArg trim star
+NNFParser >> hThing [
+	^(
+		  ('constraint' asParser trim, hCstr ==> #second)
+		/ self hVar
+		/ self hQualifier
+		/ ('constant' asParser trim, self tok trim, sort ==> [ :x | HCon symbol: x second sort: x third ])
+		/ self fixpoint
+		/ define
+		" / match"
+		" / data"
+	) parens
 ]
 
 { #category : #grammar }
-NNFParser >> sortArg [
-	^ self sort′: nil asParser
+NNFParser >> hVar [
+	^'var' asParser trim,
+	self kvSym trim,
+	sort parens trim plus parens
+	==> [ :x | HVar name: x second argSorts: x third ]
+	
 ]
 
 { #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 ])
+NNFParser >> kvSym [
+	^('$' asParser,
+	($# asParser ==> [:x|$º] / #word asParser / $_ asParser) plus)
+	==> [ :x | String withAll: x second ]
 ]
 
 { #category : #grammar }
 NNFParser >> start [
-	^thing trim star end ==> [ :x | HornQuery fromThings: x ]
+	^self hThing trim star end ==> [ :x | HornQuery fromThings: x ]
 ]
 
 { #category : #'grammar - util' }
 NNFParser >> symSort [
-	^tok trim, sort
-]
-
-{ #category : #grammar }
-NNFParser >> thing [
-	^(constraint / var / qualif / constant / fixpoint / define "match data") parens
-]
-
-{ #category : #'grammar - util' }
-NNFParser >> tok [
-	^(PPPredicateObjectParser
-		on: (PPCharSetPredicate on: [ :ch |
-					(ch isSeparator or: [ ch == $( or: [ ch == $) ]]) not ])
-		message: 'Token expected') plus flatten
-		
-]
-
-{ #category : #grammar }
-NNFParser >> tvar [
-	^ self varSort
-	/ ($` asParser, #lowercase asParser ==> [ :x | Z3Sort uninterpretedSortNamed: (String with: x second) ])
-]
-
-{ #category : #grammar }
-NNFParser >> var [
-	^'var' asParser trim,
-	kappa trim,
-	sort parens trim plus parens
-	==> [ :x | HVar name: x second argSorts: x third ]
-	
-]
-
-{ #category : #grammar }
-NNFParser >> varSort [
-	^'@(' asParser, PPParser decimalInteger, ')' asParser
-	==> [ :x | FVar new: x second ]
+	^(self tok trim, sort) parens
 ]
diff --git a/src/Refinements-Tests/HornPosTest.class.st b/src/Refinements-Tests/HornPosTest.class.st
index 63477c51d..f7450d7b4 100644
--- a/src/Refinements-Tests/HornPosTest.class.st
+++ b/src/Refinements-Tests/HornPosTest.class.st
@@ -634,29 +634,6 @@ Cf. Horn/Transformations.hs:
 	 to experiment with, than a test."
 ]
 
-{ #category : #'tests - sol1' }
-HornPosTest >> testSol1_3 [
-"
-Cf. Horn/Transformations.hs:
--- >> let c = doParse' hCstrP '' '(forall ((a Int) (p a)) (forall ((b Int) (q b)) (and (($k a)) (($k b)))))'
--- >> sol1 'k' c
--- [[((a int) (p a)),((b int) (q b)),((_ bool) (κarg$k#1 == a))],[((a int) (p a)),((b int) (q b)),((_ bool) (κarg$k#1 == b))]]
-"
-	| c sol sa sb |
-	c := (NNFParser new productionAt: #forall) parse: 'forall ((a Int) (p a)) (forall ((b Int) (q b)) (and (($k a)) (($k b))))'.
-	self deny: c isPetitFailure.
-	sol := c sol1: 'k'.  "-> [([Bind], [F.Expr])]"
-	self assert: sol size equals: 2.
-	
-	"the 'κarg$k#1 = a' solution:"
-	sa := sol detect: [ :s | s value anySatisfy: [ :eq | eq y sym = 'a' ] ].
-	self assert: sa key size equals: 2.
-	
-	"the 'κarg$k#1 = b' solution:"
-	sb := sol detect: [ :s | s value anySatisfy: [ :eq | eq y sym = 'b' ] ].
-	self assert: sb key size equals: 2.
-]
-
 { #category : #'tests - safety' }
 HornPosTest >> testSumRec [
 	self provePos: self sumRec
diff --git a/src/SpriteLang/RefinementParser.class.st b/src/SpriteLang/RefinementParser.class.st
index 8139eb1d1..22855367d 100644
--- a/src/SpriteLang/RefinementParser.class.st
+++ b/src/SpriteLang/RefinementParser.class.st
@@ -49,12 +49,12 @@ RefinementParser >> concReftB [
 			| id pred |
 			id := id_pred first.
 			pred := id_pred last.
-			(Reft symbol: id expr: (DecidableRefinement text: pred)) known ]
+			(Reft symbol: id expr: pred) known ]
 ]
 
 { #category : #grammar }
 RefinementParser >> concReftBExpr [
-	^RefinementExpressionParser new ==> [ :seq | seq formattedCode ]
+	^DecidableRefinement parser
 ]
 
 { #category : #grammar }