From 8f68418449d0af1616c0c340b1e5b60822aea2f1 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Fri, 18 Oct 2024 09:38:41 -0400
Subject: [PATCH] Route uses of RefinementExpressionParser through
 DecidableRefinement

---
 src/Refinements-Parsing/DecidableRefinement.extension.st | 7 +++++++
 src/Refinements-Parsing/FixpointParser.class.st          | 3 +--
 src/Refinements-Parsing/NNFParser.class.st               | 4 ++--
 src/SpriteLang/RefinementParser.class.st                 | 4 ++--
 4 files changed, 12 insertions(+), 6 deletions(-)
 create mode 100644 src/Refinements-Parsing/DecidableRefinement.extension.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
index d4e7535b0..0931d5136 100644
--- a/src/Refinements-Parsing/FixpointParser.class.st
+++ b/src/Refinements-Parsing/FixpointParser.class.st
@@ -59,8 +59,7 @@ FixpointParser >> funcSort [
 
 { #category : #grammar }
 FixpointParser >> pred [
-	^ RefinementExpressionParser new
-	==> [ :x | DecidableRefinement text: x formattedCode ]
+	^DecidableRefinement parser
 ]
 
 { #category : #grammar }
diff --git a/src/Refinements-Parsing/NNFParser.class.st b/src/Refinements-Parsing/NNFParser.class.st
index 59bc25199..c0d34494c 100644
--- a/src/Refinements-Parsing/NNFParser.class.st
+++ b/src/Refinements-Parsing/NNFParser.class.st
@@ -21,11 +21,11 @@ NNFParser >> define [
 	$: 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 ]
 ]
 
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 }