Generalize PAtomEq to PAtom

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

@@ -0,0 +1,30 @@
+Class {
+	#name : #Brel,
+	#superclass : #SharedPool,
+	#classVars : [
+		'Eq',
+		'Ge',
+		'Gt',
+		'Le',
+		'Lt',
+		'Ne',
+		'Ueq',
+		'Une'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'class initialization' }
+Brel class >> initialize [
+	"
+	self initialize
+	"
+	Eq := #===.
+	Ne := #~==.
+	Ge := #>=.
+	Gt := #>.
+	Le := #<=.
+	Lt := #<.
+	Ueq := #====.
+	Une := #~===.
+]

src/Refinements/CstrHead.class.st

@@ -111,7 +111,7 @@ CstrHead >> sol1: k [
 	ys := pred args.
 	k1 = k ifFalse: [ ^#() ].
 	xs := k kArgs: ys.
-	^{ #() -> (xs collectWithIndex: [ :x :j | PAtomEq x: x toEVar y: (ys at: j) toEVar ]). }
+	^{ #() -> (xs collectWithIndex: [ :x :j | PAtom brel: #=== x: x toEVar y: (ys at: j) toEVar ]). }
 ]
 
 { #category : #logic }

src/Refinements/Object.extension.st

@@ -93,7 +93,7 @@ Object >> ≛ [ y
 	 construct the Horn Reft stating the receiver is equal to the
 	 argument. "
 	| atom |
-	atom := PAtomEq x: self expr y: y expr.
+	atom := PAtom brel: #=== x: self expr y: y expr.
 	^HReft expr: atom
 "
 peq :: (F.Expression a, F.Expression b) => a -> b -> H.Pred

src/Refinements/PAtom.class.st

@@ -0,0 +1,139 @@
+"
+data Expr =
+          ...
+          | PAtom  !Brel  !Expr !Expr
+
+data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une
+            deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+Regarding Ueq see remark in Solution.hs about ""we use ~~ because the param
+and value may have different sorts, see: tests/pos/kvar-param-poly-00.hs""
+"
+Class {
+	#name : #PAtom,
+	#superclass : #Expr,
+	#instVars : [
+		'brel',
+		'x',
+		'y'
+	],
+	#pools : [
+		'Brel'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+PAtom class >> brel: aSymbol x: x y: y [
+	^self basicNew
+		brel: aSymbol;
+		x: x;
+		y: y;
+		yourself
+]
+
+{ #category : #'instance creation' }
+PAtom class >> canRepresent: aSelector [
+	^Brel classPool includes: aSelector
+]
+
+{ #category : #'instance creation' }
+PAtom class >> new [
+	self shouldNotImplement
+]
+
+{ #category : #comparing }
+PAtom >> = another [
+	self class = another class ifFalse: [ ^false ].
+	^ (brel = another brel)
+	& (x = another x)
+	& (y = another y)
+]
+
+{ #category : #'term rewriting' }
+PAtom >> accept: aVisitor [
+	^self class
+		brel: brel
+		x: (x accept: aVisitor)
+		y: (y accept: aVisitor)
+]
+
+{ #category : #accessing }
+PAtom >> brel [
+	^ brel
+]
+
+{ #category : #accessing }
+PAtom >> brel: anObject [
+	(self class canRepresent: anObject) ifFalse: [ self error ].
+	brel := anObject
+]
+
+{ #category : #'term rewriting' }
+PAtom >> evaluateIn: aBindEnv ifUndeclared: vndBlock [
+	^(x evaluateIn: aBindEnv ifUndeclared: vndBlock)
+		perform: brel
+		with: (y evaluateIn: aBindEnv ifUndeclared: vndBlock)
+]
+
+{ #category : #comparing }
+PAtom >> hash [
+	^brel hash
+]
+
+{ #category : #'term rewriting' }
+PAtom >> isTautoPred [
+	^brel = Eq and: [ x = y ]
+]
+
+{ #category : #printing }
+PAtom >> printOn: aStream [
+	aStream nextPut: $(.
+	x printOn: aStream.
+	aStream space.
+	aStream nextPutAll: brel.
+	aStream space.
+	y printOn: aStream.
+	aStream nextPut: $).
+]
+
+{ #category : #'term rewriting' }
+PAtom >> subst1: θ [ 
+	^PAtom
+		brel: brel
+		x: (x subst1: θ)
+		y: (y subst1: θ)
+]
+
+{ #category : #'term rewriting' }
+PAtom >> subst: θ [ 
+	^PAtom
+		brel: brel
+		x: (x subst: θ)
+		y: (y subst: θ)
+]
+
+{ #category : #'term rewriting' }
+PAtom >> substPred: oldToNewVarNameAssocs [
+	^self shouldBeImplemented "?"
+]
+
+{ #category : #accessing }
+PAtom >> x [
+	^ x
+]
+
+{ #category : #accessing }
+PAtom >> x: anObject [
+	x := anObject
+]
+
+{ #category : #accessing }
+PAtom >> y [
+	^ y
+]
+
+{ #category : #accessing }
+PAtom >> y: anObject [
+	y := anObject
+]

src/SpriteLang/RType.class.st

@@ -190,7 +190,7 @@ RType >> goReflectTy: f v: v expr: e xs: xs s₀: s₀ [
 	"go xs e t"
 	| body rbody |
 	body := e embed.
-	rbody := KnownReft symbol: v expr: (HReft expr: (PAtomEq x: (EVar of: v) y: body)).
+	rbody := KnownReft symbol: v expr: (HReft expr: (PAtom brel: #=== x: (EVar of: v) y: body)).
 	CGInfo current addReflectVar: f rtype: s₀ xts: xs reversed outputSort: self rtypeSort expr: body.
 	^self strengthenTop: rbody
 ]