Add tests to source control
This commit is contained in:
parent
27d25fb849
commit
aa386f2e79
10 changed files with 361 additions and 0 deletions
6
compiler/src/test/eager-solving-global.bolt
Normal file
6
compiler/src/test/eager-solving-global.bolt
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
|
||||||
|
let foo n.
|
||||||
|
# @expect_diagnostic "TypeMismatch"
|
||||||
|
let f : String = 1
|
||||||
|
return n
|
||||||
|
|
15
compiler/src/test/enum-declaration-app.bolt
Normal file
15
compiler/src/test/enum-declaration-app.bolt
Normal file
|
@ -0,0 +1,15 @@
|
||||||
|
|
||||||
|
enum Maybe a.
|
||||||
|
Just a
|
||||||
|
Nothing
|
||||||
|
|
||||||
|
enum App a b.
|
||||||
|
MkApp (a b)
|
||||||
|
|
||||||
|
enum Foo.
|
||||||
|
MkFoo (App Maybe Int)
|
||||||
|
|
||||||
|
let f : Foo = MkFoo (MkApp (Just 1))
|
||||||
|
|
||||||
|
# @expect_diagnostic "TypeMismatch"
|
||||||
|
let g : Foo = MkFoo (MkApp (Just "foo"))
|
10
compiler/src/test/enum-declaration-maybe.bolt
Normal file
10
compiler/src/test/enum-declaration-maybe.bolt
Normal file
|
@ -0,0 +1,10 @@
|
||||||
|
|
||||||
|
enum Maybe a.
|
||||||
|
Just a
|
||||||
|
Nothing
|
||||||
|
|
||||||
|
let right_1 : Maybe Int = Just 1
|
||||||
|
let right_2 : Maybe String = Just "foo"
|
||||||
|
# @expect_diagnostic "TypeMismatch"
|
||||||
|
let wrong : Maybe Int = Just "foo"
|
||||||
|
|
16
compiler/src/test/mutual-recursion-2.bolt
Normal file
16
compiler/src/test/mutual-recursion-2.bolt
Normal file
|
@ -0,0 +1,16 @@
|
||||||
|
|
||||||
|
let is_even x.
|
||||||
|
if x == 0.
|
||||||
|
return True
|
||||||
|
else.
|
||||||
|
return is_odd (x-1)
|
||||||
|
|
||||||
|
let is_odd x.
|
||||||
|
if x == 1.
|
||||||
|
return False
|
||||||
|
else.
|
||||||
|
return is_even (x-1)
|
||||||
|
|
||||||
|
@:Bool is_even 1
|
||||||
|
# @expect_diagnostic "TypeMismatch"
|
||||||
|
is_even True
|
8
compiler/src/test/mutual-recursion.bolt
Normal file
8
compiler/src/test/mutual-recursion.bolt
Normal file
|
@ -0,0 +1,8 @@
|
||||||
|
|
||||||
|
let fac n = fac_2 n
|
||||||
|
|
||||||
|
let fac_2 n = fac_3 n + fac n
|
||||||
|
|
||||||
|
let fac_3 n = fac_2 (n-1)
|
||||||
|
|
||||||
|
@:Int fac 1
|
6
compiler/src/test/nested-definitions.bolt
Normal file
6
compiler/src/test/nested-definitions.bolt
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
|
||||||
|
let foo x.
|
||||||
|
let bar y z = y + z - x
|
||||||
|
return bar 1 2
|
||||||
|
|
||||||
|
@:Int foo 3
|
6
compiler/src/test/return-types-polymorphic.bolt
Normal file
6
compiler/src/test/return-types-polymorphic.bolt
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
|
||||||
|
let id x = x
|
||||||
|
|
||||||
|
@:Int id 1
|
||||||
|
@:String id "foo"
|
||||||
|
@:Bool id True
|
5
compiler/src/test/tuple-access.bolt
Normal file
5
compiler/src/test/tuple-access.bolt
Normal file
|
@ -0,0 +1,5 @@
|
||||||
|
|
||||||
|
let t1 = (1, True)
|
||||||
|
|
||||||
|
@:Int t1.0
|
||||||
|
@:Bool t1.1
|
271
compiler/src/test/typecheck.md
Normal file
271
compiler/src/test/typecheck.md
Normal file
|
@ -0,0 +1,271 @@
|
||||||
|
|
||||||
|
## Record types can be unified without causing an error
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Person.
|
||||||
|
email: String
|
||||||
|
age: Int
|
||||||
|
|
||||||
|
let bert
|
||||||
|
= Person {
|
||||||
|
email = "bar@boo.com",
|
||||||
|
age = 32
|
||||||
|
}
|
||||||
|
let bob
|
||||||
|
= Person {
|
||||||
|
email = "boo",
|
||||||
|
age = 43
|
||||||
|
}
|
||||||
|
|
||||||
|
bert == bob
|
||||||
|
```
|
||||||
|
|
||||||
|
## Return types are polymorphic
|
||||||
|
|
||||||
|
```
|
||||||
|
let id x = x
|
||||||
|
|
||||||
|
id 1
|
||||||
|
id "foo"
|
||||||
|
id True
|
||||||
|
```
|
||||||
|
|
||||||
|
## Nested definitions work
|
||||||
|
|
||||||
|
```
|
||||||
|
let foo x.
|
||||||
|
let bar y z = y + z - x
|
||||||
|
bar
|
||||||
|
|
||||||
|
foo True
|
||||||
|
```
|
||||||
|
|
||||||
|
## Everything that can be type-checked will be type-checked
|
||||||
|
|
||||||
|
```
|
||||||
|
let foo n.
|
||||||
|
let f : String = 1
|
||||||
|
return n
|
||||||
|
```
|
||||||
|
|
||||||
|
## Recursive definitions do not cause infinite loops in the type-checker
|
||||||
|
|
||||||
|
```
|
||||||
|
let fac n = fac_2 n
|
||||||
|
|
||||||
|
let fac_2 n = fac_3 n + fac n
|
||||||
|
|
||||||
|
let fac_3 n = fac_2 (n-1)
|
||||||
|
|
||||||
|
not (fac 1)
|
||||||
|
```
|
||||||
|
|
||||||
|
## Example with mutual recursion works
|
||||||
|
|
||||||
|
```
|
||||||
|
let is_even x.
|
||||||
|
if x == 0.
|
||||||
|
return True
|
||||||
|
else.
|
||||||
|
return is_odd (x-1)
|
||||||
|
|
||||||
|
let is_odd x.
|
||||||
|
if x == 1.
|
||||||
|
return False
|
||||||
|
else.
|
||||||
|
return is_even (x-1)
|
||||||
|
|
||||||
|
not (is_even True)
|
||||||
|
```
|
||||||
|
|
||||||
|
## Polymorphic records can be partially typed
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Timestamped a b.
|
||||||
|
first: a
|
||||||
|
second: b
|
||||||
|
timestamp: Int
|
||||||
|
|
||||||
|
type Foo = Timestamped Int
|
||||||
|
|
||||||
|
type Bar = Foo Int
|
||||||
|
|
||||||
|
let t : Bar = Timestamped { first = "bar", second = 1, timestamp = 12345 }
|
||||||
|
```
|
||||||
|
|
||||||
|
## Extensible records work
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Timestamped a.
|
||||||
|
data: a
|
||||||
|
timestamp: Int
|
||||||
|
|
||||||
|
let t = Timestamped { data = "foo", timestamp = 12345 }
|
||||||
|
|
||||||
|
t.data == 1
|
||||||
|
t.data == "foo"
|
||||||
|
|
||||||
|
let u = Timestamped { data = True, timestamp = 12345 }
|
||||||
|
|
||||||
|
u.data == "foo"
|
||||||
|
u.data == False
|
||||||
|
```
|
||||||
|
|
||||||
|
## A recursive function is automatically instantiated
|
||||||
|
|
||||||
|
```
|
||||||
|
let fac n.
|
||||||
|
if n == 0.
|
||||||
|
return 1
|
||||||
|
else.
|
||||||
|
return n * fac (n-"foo")
|
||||||
|
```
|
||||||
|
|
||||||
|
## Enum-declarations are correctly typed
|
||||||
|
|
||||||
|
```
|
||||||
|
enum Maybe a.
|
||||||
|
Just a
|
||||||
|
Nothing
|
||||||
|
|
||||||
|
let right_1 : Maybe Int = Just 1
|
||||||
|
let right_2 : Maybe String = Just "foo"
|
||||||
|
let wrong : Maybe Int = Just "foo"
|
||||||
|
```
|
||||||
|
|
||||||
|
## Kind inference works
|
||||||
|
|
||||||
|
```
|
||||||
|
enum Maybe a.
|
||||||
|
Just a
|
||||||
|
Nothing
|
||||||
|
|
||||||
|
let foo_1 : Maybe
|
||||||
|
let foo_2 : Maybe Int
|
||||||
|
let foo_3 : Maybe Int Int
|
||||||
|
let foo_4 : Maybe Int Int Int
|
||||||
|
```
|
||||||
|
|
||||||
|
## Can indirectly apply a polymorphic datatype to some type
|
||||||
|
|
||||||
|
```
|
||||||
|
enum Maybe a.
|
||||||
|
Just a
|
||||||
|
Nothing
|
||||||
|
|
||||||
|
enum App a b.
|
||||||
|
MkApp (a b)
|
||||||
|
|
||||||
|
enum Foo.
|
||||||
|
MkFoo (App Maybe Int)
|
||||||
|
|
||||||
|
let f : Foo = MkFoo (MkApp (Just 1))
|
||||||
|
```
|
||||||
|
|
||||||
|
## Record-declarations inside enum-declarations work
|
||||||
|
|
||||||
|
```
|
||||||
|
enum Shape.
|
||||||
|
Circle.
|
||||||
|
radius: Int
|
||||||
|
Rect.
|
||||||
|
width: Int
|
||||||
|
height: Int
|
||||||
|
|
||||||
|
let z = Circle { radius = 12 }
|
||||||
|
let a = Rect { width = 12, height = 12 }
|
||||||
|
|
||||||
|
a == z
|
||||||
|
```
|
||||||
|
|
||||||
|
## Tuple types are correctly inferred and unified
|
||||||
|
|
||||||
|
```
|
||||||
|
let foo_1 : (Int, Int, Int) = (1, 2, 3)
|
||||||
|
let foo_2 : (Int, Int, Int) = (1, 2, "foo")
|
||||||
|
```
|
||||||
|
|
||||||
|
## Module references work
|
||||||
|
|
||||||
|
```
|
||||||
|
mod CD.
|
||||||
|
mod A.
|
||||||
|
struct Foo
|
||||||
|
mod B.
|
||||||
|
let alpha: A.Foo
|
||||||
|
```
|
||||||
|
|
||||||
|
## Rest-expressions on extensible records work
|
||||||
|
|
||||||
|
```
|
||||||
|
let foo { x, y, .. } = x + y
|
||||||
|
|
||||||
|
foo { x = 1, y = 2 }
|
||||||
|
foo { x = 1, y = 2, z = 3 }
|
||||||
|
foo { x = 1, y = 2, z = 3, a = 4 }
|
||||||
|
```
|
||||||
|
|
||||||
|
## A polymorphic function is properly generalized when assigned to a new variable
|
||||||
|
|
||||||
|
```
|
||||||
|
let id x = x
|
||||||
|
let id2 = id
|
||||||
|
let id3 = id
|
||||||
|
|
||||||
|
id3 1
|
||||||
|
id3 "bla"
|
||||||
|
|
||||||
|
id2 1
|
||||||
|
id2 "bla"
|
||||||
|
````
|
||||||
|
|
||||||
|
## Can omit a field from a record type
|
||||||
|
|
||||||
|
```
|
||||||
|
let remove_x { x, ..rest } = rest
|
||||||
|
let p1 = { x = 1, y = 2, z = 3 }
|
||||||
|
(remove_x p1).x
|
||||||
|
```
|
||||||
|
|
||||||
|
## Can project a field from some other fields
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Point.
|
||||||
|
x: Int
|
||||||
|
y: Int
|
||||||
|
|
||||||
|
let project { x, y, .. } = { x, y }
|
||||||
|
|
||||||
|
let p2 : Point = project { x = 1, y = 2 }
|
||||||
|
let p3 : Point = project { x = 1, y = 2, z = 3 }
|
||||||
|
let p3 : Point = project { x = 1, y = 2, z = 3, a = 4 }
|
||||||
|
```
|
||||||
|
|
||||||
|
## Can assign records to a struct-type
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Vec2.
|
||||||
|
x: Int
|
||||||
|
y: Int
|
||||||
|
|
||||||
|
let p1 : Vec2 = { x = 1, y = 2 }
|
||||||
|
```
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Vec3.
|
||||||
|
x: Int
|
||||||
|
y: Int
|
||||||
|
z: Int
|
||||||
|
|
||||||
|
let p1 : Vec3 = { x = 1, y = 2, z = 3 }
|
||||||
|
```
|
||||||
|
|
||||||
|
This one should fail:
|
||||||
|
|
||||||
|
```
|
||||||
|
struct Vec2.
|
||||||
|
x: Int
|
||||||
|
y: Int
|
||||||
|
|
||||||
|
let p1 : Vec2 = { x = 1, y = 2, z = 3 }
|
||||||
|
```
|
18
compiler/src/test/unify-similar-records.bolt
Normal file
18
compiler/src/test/unify-similar-records.bolt
Normal file
|
@ -0,0 +1,18 @@
|
||||||
|
|
||||||
|
struct Person.
|
||||||
|
email: String
|
||||||
|
age: Int
|
||||||
|
|
||||||
|
let bert
|
||||||
|
= Person {
|
||||||
|
email = "bar@boo.com",
|
||||||
|
age = 32
|
||||||
|
}
|
||||||
|
let bob
|
||||||
|
= Person {
|
||||||
|
email = "boo",
|
||||||
|
age = 43
|
||||||
|
}
|
||||||
|
|
||||||
|
# @expect_diagnostic TypeMismatch
|
||||||
|
bert == bob
|
Loading…
Reference in a new issue