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

@@ -59,8 +59,7 @@ FixpointParser >> funcSort [
 
 { #category : #grammar }
 FixpointParser >> pred [
-	^ RefinementExpressionParser new
-	==> [ :x | DecidableRefinement text: x formattedCode ]
+	^DecidableRefinement parser
 ]
 
 { #category : #grammar }

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 ]
 ]
 

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 }