Skip to content

Commit

Permalink
Add first/simplest SpriteHorn-level Datatype tests
Browse files Browse the repository at this point in the history
  • Loading branch information
shingarov committed Nov 17, 2024
1 parent c4da38f commit 8452c87
Show file tree
Hide file tree
Showing 2 changed files with 118 additions and 0 deletions.
28 changes: 28 additions & 0 deletions src/SpriteLang-Tests/SpriteHornNegTest.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -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)))))
'
]
90 changes: 90 additions & 0 deletions src/SpriteLang-Tests/SpriteHornPosTest.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -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: '
Expand Down Expand Up @@ -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: '
Expand Down Expand Up @@ -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: '
Expand Down Expand Up @@ -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)))))
'
]

0 comments on commit 8452c87

Please sign in to comment.