Generalize PAtomEq to PAtom

src/PLE/Equation.extension.st

@@ -19,7 +19,7 @@ instance Normalizable Equation where
 		x suffixSymbol: (eqName intSymbol: i) ].
 	evalEnv := EvalEnv ofSorts: (SEnv newFromAssociations: eqArgs), sEnv naturalTransformations.
 	body′ := eqBody evaluateIn: evalEnv.
-	body′ := body′ smt2: sEnv.
+	body′ := [ body′ smt2 ] runReader: #symbolEnv initialState: sEnv.
 	su := Dictionary newFromAssociations:  (xs zip: xs′).
 	body′ := body′ renameVariables: su.
 	body′ := body′ normalizeBody: eqName.

src/Refinements-Doodles/FlatConstraintTest.class.st

@@ -7,7 +7,7 @@ Class {
 { #category : #'tests - tauto expr' }
 FlatConstraintTest >> testConjunctsOfTautoPreds [
 	| p |
-	p := PAnd of: { Expr PTrue . (PAtomEq x: 'a' y: 'a') }.
+	p := PAnd of: { Expr PTrue . (PAtom brel: #=== x: 'a' y: 'a') }.
 	self assert: p conjuncts isEmpty
 ]
 
@@ -47,7 +47,7 @@ FlatConstraintTest >> testPFalseNotTautoPred [
 { #category : #'tests - tauto expr' }
 FlatConstraintTest >> testRefaConjunctsOfTautoPreds [
 	| p |
-	p := PAnd of: { Expr PTrue . (PAtomEq x: 'a' y: 'a') }.
+	p := PAnd of: { Expr PTrue . (PAtom brel: #=== x: 'a' y: 'a') }.
 	self assert: p refaConjuncts isEmpty
 ]
 

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/FQParser.class.st

@@ -0,0 +1,107 @@
+Class {
+	#name : #FQParser,
+	#superclass : #FixpointParser,
+	#instVars : [
+		'subC',
+		'bind',
+		'refa',
+		'sortedReft'
+	],
+	#category : #'Refinements-Parsing'
+}
+
+{ #category : #grammar }
+FQParser >> bind [
+	^ self class lowerId trim,
+	$: asParser
+	==> #first
+]
+
+{ #category : #grammar }
+FQParser >> constraint [
+	^ 'constraint:' asParser trim
+	, subC
+	==> #second
+]
+
+{ #category : #grammar }
+FQParser >> def [
+	^ self fixpoint
+	/ self constraint
+	/ 'everything else' asParser
+]
+
+{ #category : #grammar }
+FQParser >> fInfo [
+	^ self def trim plus
+	==> [ :x | FInfo defsFInfo: x ]
+]
+
+{ #category : #grammar }
+FQParser >> ref: kind [
+"
+-- | (Sorted) Refinements
+"
+	^self refBind: bind rp: refa kind: kind
+]
+
+{ #category : #grammar }
+FQParser >> refBind: bp rp: rp kind: kindP [
+"
+-- (Sorted) Refinements with configurable sub-parsers
+"
+	^(
+		bp trim,
+		kindP trim,
+		'|' asParser trim,
+		rp
+	) braces
+	==> [ :x | x second value: (Reft symbol: x first expr: x fourth) ]
+]
+
+{ #category : #grammar }
+FQParser >> refa [
+"
+-- | Refa
+refaP :: Parser Expr
+refaP =  try (pAnd <$> brackets (sepBy predP semi))
+     <|> predP
+Cf. top-level Parse.hs
+"
+	^".... and .... | "
+	pred
+]
+
+{ #category : #grammar }
+FQParser >> sortedReft [
+	^ self ref: (sort ==> [ :aSort | [ :r | SortedReft sort: aSort reft: r ]])
+]
+
+{ #category : #grammar }
+FQParser >> start [
+	^self fInfo trim end
+]
+
+{ #category : #grammar }
+FQParser >> subC [
+	^ ('env []' asParser trim ==> [ :_ | IBindEnv empty])
+	, 'lhs' asParser trim, sortedReft trim
+	, 'rhs' asParser trim, sortedReft trim
+	, 'id'  asParser, Character space asParser plus, PPParser decimalNat trim
+	, self tag
+	==> [ :x | SubC
+			mkSubC: x first
+			lhs: x third
+			rhs: x fifth
+			i: x eighth
+			tag: x ninth
+	]
+]
+
+{ #category : #grammar }
+FQParser >> tag [
+	^ 'tag' asParser
+	, Character space asParser
+	, PPParser decimalNat semicolonSeparated brackets
+	==> [ :x | x third ]
+]

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