From aa386f2e794a41bf263eab20e255e9ceea8eed99 Mon Sep 17 00:00:00 2001
From: Sam Vervaeck <samvv@pm.me>
Date: Fri, 11 Aug 2023 12:27:28 +0200
Subject: [PATCH] Add tests to source control

---
 compiler/src/test/eager-solving-global.bolt   |   6 +
 compiler/src/test/enum-declaration-app.bolt   |  15 +
 compiler/src/test/enum-declaration-maybe.bolt |  10 +
 compiler/src/test/mutual-recursion-2.bolt     |  16 ++
 compiler/src/test/mutual-recursion.bolt       |   8 +
 compiler/src/test/nested-definitions.bolt     |   6 +
 .../src/test/return-types-polymorphic.bolt    |   6 +
 compiler/src/test/tuple-access.bolt           |   5 +
 compiler/src/test/typecheck.md                | 271 ++++++++++++++++++
 compiler/src/test/unify-similar-records.bolt  |  18 ++
 10 files changed, 361 insertions(+)
 create mode 100644 compiler/src/test/eager-solving-global.bolt
 create mode 100644 compiler/src/test/enum-declaration-app.bolt
 create mode 100644 compiler/src/test/enum-declaration-maybe.bolt
 create mode 100644 compiler/src/test/mutual-recursion-2.bolt
 create mode 100644 compiler/src/test/mutual-recursion.bolt
 create mode 100644 compiler/src/test/nested-definitions.bolt
 create mode 100644 compiler/src/test/return-types-polymorphic.bolt
 create mode 100644 compiler/src/test/tuple-access.bolt
 create mode 100644 compiler/src/test/typecheck.md
 create mode 100644 compiler/src/test/unify-similar-records.bolt

diff --git a/compiler/src/test/eager-solving-global.bolt b/compiler/src/test/eager-solving-global.bolt
new file mode 100644
index 000000000..948ac4b39
--- /dev/null
+++ b/compiler/src/test/eager-solving-global.bolt
@@ -0,0 +1,6 @@
+
+let foo n.
+  # @expect_diagnostic "TypeMismatch"
+  let f : String = 1
+  return n
+
diff --git a/compiler/src/test/enum-declaration-app.bolt b/compiler/src/test/enum-declaration-app.bolt
new file mode 100644
index 000000000..0964bf264
--- /dev/null
+++ b/compiler/src/test/enum-declaration-app.bolt
@@ -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"))
diff --git a/compiler/src/test/enum-declaration-maybe.bolt b/compiler/src/test/enum-declaration-maybe.bolt
new file mode 100644
index 000000000..a03e808c0
--- /dev/null
+++ b/compiler/src/test/enum-declaration-maybe.bolt
@@ -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"
+
diff --git a/compiler/src/test/mutual-recursion-2.bolt b/compiler/src/test/mutual-recursion-2.bolt
new file mode 100644
index 000000000..8c6ae999f
--- /dev/null
+++ b/compiler/src/test/mutual-recursion-2.bolt
@@ -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
diff --git a/compiler/src/test/mutual-recursion.bolt b/compiler/src/test/mutual-recursion.bolt
new file mode 100644
index 000000000..6e8d41d2d
--- /dev/null
+++ b/compiler/src/test/mutual-recursion.bolt
@@ -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
diff --git a/compiler/src/test/nested-definitions.bolt b/compiler/src/test/nested-definitions.bolt
new file mode 100644
index 000000000..3047a0c66
--- /dev/null
+++ b/compiler/src/test/nested-definitions.bolt
@@ -0,0 +1,6 @@
+
+let foo x.
+  let bar y z = y + z - x
+  return bar 1 2
+
+@:Int foo 3
diff --git a/compiler/src/test/return-types-polymorphic.bolt b/compiler/src/test/return-types-polymorphic.bolt
new file mode 100644
index 000000000..d6ee4bb74
--- /dev/null
+++ b/compiler/src/test/return-types-polymorphic.bolt
@@ -0,0 +1,6 @@
+
+let id x = x
+
+@:Int id 1
+@:String id "foo"
+@:Bool id True
diff --git a/compiler/src/test/tuple-access.bolt b/compiler/src/test/tuple-access.bolt
new file mode 100644
index 000000000..0a66acd87
--- /dev/null
+++ b/compiler/src/test/tuple-access.bolt
@@ -0,0 +1,5 @@
+
+let t1 = (1, True)
+
+@:Int t1.0
+@:Bool t1.1
diff --git a/compiler/src/test/typecheck.md b/compiler/src/test/typecheck.md
new file mode 100644
index 000000000..89af92632
--- /dev/null
+++ b/compiler/src/test/typecheck.md
@@ -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 }
+```
diff --git a/compiler/src/test/unify-similar-records.bolt b/compiler/src/test/unify-similar-records.bolt
new file mode 100644
index 000000000..5fb205d3b
--- /dev/null
+++ b/compiler/src/test/unify-similar-records.bolt
@@ -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