From 8fb210ca42ac16ac6e329c944589ab004e81bbd5 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Mon, 23 Oct 2023 18:29:34 -0400
Subject: [PATCH 1/3] Implement membership in ShallowRefinement

---
 Refinements/ShallowRefinement.class.st | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/Refinements/ShallowRefinement.class.st b/Refinements/ShallowRefinement.class.st
index 538129aea..15eaac674 100644
--- a/Refinements/ShallowRefinement.class.st
+++ b/Refinements/ShallowRefinement.class.st
@@ -15,7 +15,7 @@ ShallowRefinement class >> base: B predicate: e [
 		yourself
 ]
 
-{ #category : #accessing }
+{ #category : #'set theory' }
 ShallowRefinement >> allElements [
 	| nu solver elements |
 	nu := B mkFreshConst: 'nu'.
@@ -33,7 +33,7 @@ ShallowRefinement >> allElements [
 	^elements
 ]
 
-{ #category : #algebra }
+{ #category : #'set theory' }
 ShallowRefinement >> anyOne [
 	| nu solver instance |
 	nu := B mkFreshConst: 'nu'.
@@ -55,6 +55,16 @@ ShallowRefinement >> base: aSort [
 	B := aSort
 ]
 
+{ #category : #'set theory' }
+ShallowRefinement >> includes: x [
+	"Caveat programmator: this is purely a REFINEMENT test,
+	 simply assuming that the sorts agree.
+	 We can't really do much here meaningfully,
+	 because many things can reasonably cast to many other things.
+	 For example, 'a' casts to the integer symbolic constant a."
+	^x∘e
+]
+
 { #category : #accessing }
 ShallowRefinement >> predicate [
 	^e
@@ -81,21 +91,21 @@ ShallowRefinement >> toPredicateOver: varName [
 	^self predicate value: var
 ]
 
-{ #category : #accessing }
+{ #category : #'set theory' }
 ShallowRefinement >> ∩ [ rhs 
 	B = rhs ifTrue: [ ^self ].
 	B = rhs base ifFalse: [ self error: 'Incoherent sorts' ].
 	^B | [ :x | (e value: x) & (rhs predicate value: x) ]
 ]
 
-{ #category : #accessing }
+{ #category : #'set theory' }
 ShallowRefinement >> ∪ [ rhs 
 	B = rhs ifTrue: [ ^self ].
 	B = rhs base ifFalse: [ self error: 'Incoherent sorts' ].
 	^B | [ :x | (e value: x) | (rhs predicate value: x) ]
 ]
 
-{ #category : #algebra }
+{ #category : #'set theory' }
 ShallowRefinement >> ⊆ [ rhs
 	| x solver |
 	self base == rhs base ifFalse: [ self error: 'To compare refinement types, first the base types must already be the same' ].

From 24fec75659c1d1dea811309edd224d5b8d663820 Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Mon, 23 Oct 2023 18:30:24 -0400
Subject: [PATCH 2/3] Add ShallowRefinementTest to CI

---
 .../ShallowRefinementTest.class.st                              | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)
 rename {Refinements-Doodles => Refinements-Tests}/ShallowRefinementTest.class.st (97%)

diff --git a/Refinements-Doodles/ShallowRefinementTest.class.st b/Refinements-Tests/ShallowRefinementTest.class.st
similarity index 97%
rename from Refinements-Doodles/ShallowRefinementTest.class.st
rename to Refinements-Tests/ShallowRefinementTest.class.st
index 1620d0fc1..cfe707a45 100644
--- a/Refinements-Doodles/ShallowRefinementTest.class.st
+++ b/Refinements-Tests/ShallowRefinementTest.class.st
@@ -1,7 +1,7 @@
 Class {
 	#name : #ShallowRefinementTest,
 	#superclass : #TestCaseWithZ3Context,
-	#category : #'Refinements-Doodles'
+	#category : #'Refinements-Tests'
 }
 
 { #category : #'tests - factorial' }

From 9617c0d150970110f69dca976433d21338f4b91f Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Mon, 23 Oct 2023 18:31:13 -0400
Subject: [PATCH 3/3] Add a test for "is element of aShallowRefinement"

---
 Refinements-Tests/ShallowRefinementTest.class.st | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/Refinements-Tests/ShallowRefinementTest.class.st b/Refinements-Tests/ShallowRefinementTest.class.st
index cfe707a45..8c2bce080 100644
--- a/Refinements-Tests/ShallowRefinementTest.class.st
+++ b/Refinements-Tests/ShallowRefinementTest.class.st
@@ -47,6 +47,14 @@ ShallowRefinementTest >> testInvertFactorial [
 		equals: 5
 ]
 
+{ #category : #'tests - factorial' }
+ShallowRefinementTest >> testNincludes1 [
+	| ℕ |
+	ℕ := Int sort | [ :k | k >= 0 ].
+	self assert: 1 ∈ ℕ.
+	self deny:  -1 ∈ ℕ.
+]
+
 { #category : #'tests - sets' }
 ShallowRefinementTest >> testSubset [
 	| gt1 gt0 |