Add Datatype tests coming from SpriteHorn doodles

shingarov · Oct 13, 2024 · 47e4476 · 47e4476
1 parent 788526b
commit 47e4476
Show file tree

Hide file tree

Showing 2 changed files with 104 additions and 0 deletions.
diff --git a/src/SpriteLang-Tests/SpriteHornNegTest.class.st b/src/SpriteLang-Tests/SpriteHornNegTest.class.st
@@ -489,3 +489,56 @@ SpriteHornNegTest >> testL6maxlist01 [
 
 '
 ]
+
+{ #category : #'tests-L8' }
+SpriteHornNegTest >> testL8uniqueVoid2Constructors [
+	self proveNeg: '
+(data V 0 = [
+        | One {}
+        | Two {}
+      ])
+ 
+(constraint
+    (forall ((a V) (Bool true))
+      (forall ((b V) (Bool true))
+          ((a === b)))))
+'
+]
+
+{ #category : #'tests-L8' }
+SpriteHornNegTest >> testL8uniqueVoidNoADT [
+	self proveNeg: '
+(constraint
+    (forall ((a `v) (Bool true))
+      (forall ((b `v) (Bool true))
+          ((a === b)))))
+'
+]
+
+{ #category : #'tests-L8' }
+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-L8' }
+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
@@ -1217,6 +1217,42 @@ SpriteHornPosTest >> testL5tuple00 [
 
 ]
 
+{ #category : #'tests-L5' }
+SpriteHornPosTest >> testL5tuple00L8 [
+	self provePos: '
+IMPLEMENT ME; the Fixpoint Doodle is already pushed.
+'
+
+]
+
+{ #category : #'tests-L5' }
+SpriteHornPosTest >> testL5tuple00L8poly [
+	self provePos: '
+(var $k1 ((int) (int) ((C int int)) (int) (int)))
+
+(data C 2 = [
+        | C {C0 : @(0), C1 : @(1)}
+      ])
+
+(constraint
+  (and
+    (forall ((n int) (Bool true))
+      (forall ((n1 int) (n+1 === n1))
+         (forall ((v int) ((n+1 === v) & (v === n1))) ((n < v)))))
+    (forall ((m int) (Bool true))
+      (forall ((p (C int int)) (Bool true))
+        (forall ((px int)  (Bool true))
+          (forall ((py int) (px < py))
+           (forall ((p (C int int)) (Bool true))
+            (and
+              (forall ((VV int)  (VV === px)) (($k1 VV m p px py)))
+              (forall ((v int) ((px < v) & (v === py))) (($k1 v m p px py)))
+              (forall ((ok bool) (ok <=> (px < py)))
+                (forall ((v bool) ((v <=> (px < py)) & (v === ok))) ((v))))))))))))
+'
+
+]
+
 { #category : #'tests-L6' }
 SpriteHornPosTest >> testL6compose00 [
 	self provePos: '
@@ -1663,3 +1699,18 @@ SpriteHornPosTest >> testL8uniqueVoid [
           ((a === b)))))
 '
 ]
+
+{ #category : #'tests-L8' }
+SpriteHornPosTest >> testL8uniqueVoidExplicitDistinction [
+	self provePos: '
+(data V 0 = [
+        | One {}
+        | Two {}
+      ])
+ 
+(constraint
+    (forall ((a V) (a === One))
+      (forall ((b V) (b === One))
+          ((a === b)))))
+'
+]