From 8452c87a444678ca9cf89d44094f1f29384dc55a Mon Sep 17 00:00:00 2001
From: Boris Shingarov <shingarov@labware.com>
Date: Tue, 12 Nov 2024 23:33:56 -0500
Subject: [PATCH] Add first/simplest SpriteHorn-level Datatype tests

---
 .../SpriteHornNegTest.class.st                | 28 ++++++
 .../SpriteHornPosTest.class.st                | 90 +++++++++++++++++++
 2 files changed, 118 insertions(+)

diff --git a/src/SpriteLang-Tests/SpriteHornNegTest.class.st b/src/SpriteLang-Tests/SpriteHornNegTest.class.st
index 9c88b2da5..26ac6c763 100644
--- a/src/SpriteLang-Tests/SpriteHornNegTest.class.st
+++ b/src/SpriteLang-Tests/SpriteHornNegTest.class.st
@@ -489,3 +489,31 @@ SpriteHornNegTest >> testL6maxlist01 [
 
 '
 ]
+
+{ #category : #'tests-L6' }
+SpriteHornNegTest >> testL8uniqueVoidParam [
+	self proveNeg: '
+(data V 0 = [
+        | One {Cons0 : int}
+      ])
+ 
+(constraint
+    (forall ((a V) (Bool true))
+      (forall ((b V) (Bool true))
+          ((a === b)))))
+'
+]
+
+{ #category : #'tests-L6' }
+SpriteHornNegTest >> testL8uniqueVoidParamPoly [
+	self proveNeg: '
+(data V 1 = [
+        | One {Cons0 : @(0)}
+      ])
+ 
+(constraint
+    (forall ((a (V int)) (Bool true))
+      (forall ((b (V int)) (Bool true))
+          ((a === b)))))
+'
+]
diff --git a/src/SpriteLang-Tests/SpriteHornPosTest.class.st b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
index bf961dc93..a2d417bcb 100644
--- a/src/SpriteLang-Tests/SpriteHornPosTest.class.st
+++ b/src/SpriteLang-Tests/SpriteHornPosTest.class.st
@@ -746,6 +746,34 @@ SpriteHornPosTest >> testL5cons00 [
 
 ]
 
+{ #category : #'tests-L5data' }
+SpriteHornPosTest >> testL5cons00data [
+	self
+		provePos:
+			'
+(var $k3 ((`a) ((L `a)) (`a)))
+(var $k1 ((`a) (`a)))
+
+(constant len (func(1 , [(L @(0)); int])))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+  (forall ((x `a) (Bool true))
+   (forall ((t (L `a)) ((len value: t) === 0))
+     (and
+      (forall ((VV `a) (VV === x))
+       (($k3 VV t x)))
+      (forall ((VV0 `a)  ($k1 VV0 x))
+        (($k3 VV0 a x)))
+      (forall ((v (L `a)) ((len value: v) === (1 + (len value: t))))
+       ((((len value: v) === 1))))))))
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5foldRight00 [
 	self provePos: '
@@ -798,6 +826,35 @@ SpriteHornPosTest >> testL5head00 [
 '
 ]
 
+{ #category : #'tests-L5data' }
+SpriteHornPosTest >> testL5head00data [
+	self provePos: '
+(var $k9 ((int) ((L int)) (int)))
+(var $k7 ((int) (int)))
+(var $k5 ((`a) ((L `a))))
+(var $k3 ((`a) ((L `a)) (`a)))
+(var $k1 ((`a) (`a)))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+ (and
+   (forall ((x `a)  (Bool true))
+     (forall ((t (L `a))  (Bool true))
+       (forall ((VV `a)  (VV === x)) (($k3 VV t x)))))
+   (forall ((z int)  (0 <= z))
+     (and
+       (forall ((v int) (and  (0 <= v) (v === z))) (($k7 v z)))
+       (forall ((l (L int))  (Bool true))
+        (and
+          (forall ((VV6 int)  ($k7 VV6 z)) (($k9 VV6 l z)))
+          (forall ((VV8 int)  ($k9 VV8 l z)) (((0 <= VV8))))))))))
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5head01 [
 	self provePos: '
@@ -1025,6 +1082,24 @@ SpriteHornPosTest >> testL5nil00 [
 
 ]
 
+{ #category : #'tests-L5data' }
+SpriteHornPosTest >> testL5nil00data [
+	self provePos: '
+(constant len (func(1 , [(L @(0)); int])))
+
+(data L 1 = [
+        | Nil {}
+        | Cons {Cons0 : @(0), Cons1 : (L @(0))}
+      ])
+
+(constraint
+   (forall ((x `a) (Bool true))
+    (forall ((t (L `a))  ((len value: t) === 0))
+      (forall ((v (L `a)) (and ((len value: v) === 0) (v === t))) ((((len value: v) === 0)))))))
+
+'
+]
+
 { #category : #'tests-L5' }
 SpriteHornPosTest >> testL5olist00 [
 	self provePos: '
@@ -1603,3 +1678,18 @@ SpriteHornPosTest >> testL7sumAcc [
                    & (v < n))))))))))))))
 '
 ]
+
+{ #category : #'tests-L8' }
+SpriteHornPosTest >> testL8uniqueVoid [
+	"Cf. liquid-fixpoint/doodles/L8uniqueVoid.smt2 on branch experiment-z3datatypes"
+	self provePos: '
+(data V 0 = [
+        | Nil {}
+      ])
+ 
+(constraint
+    (forall ((a V) (Bool true))
+      (forall ((b V) (Bool true))
+          ((a === b)))))
+'
+]