Add first Fx datatype tests

shingarov · Oct 29, 2024 · 24986ff · 24986ff
1 parent b56bfb8
commit 24986ff
Show file tree

Hide file tree

Showing 3 changed files with 65 additions and 0 deletions.
diff --git a/src/Refinements-Tests/FQPosTest.class.st b/src/Refinements-Tests/FQPosTest.class.st
@@ -31,3 +31,25 @@ constraint:
   tag [1]
 '
 ]
+
+{ #category : #tests }
+FQPosTest >> testEqConstr1 [
+	self provePos: '
+data Thing 0 = [
+  | Cons {}
+]
+
+bind 0 a : {v: Thing | Bool true }
+bind 1 x : {v: Thing | Bool true }
+bind 2 y : {v: `a    | Bool true }
+
+constraint:
+  env [0; 1; 2]
+  lhs {v:int | x === y }
+  rhs {v:int | y === x }
+  id 1
+  tag [1]
+'.
+
+
+]
diff --git 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
@@ -1603,3 +1603,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)))))
+'
+]