Skip to content

Commit 064f004

Browse files
Meowcolm024Meowcolm024
committed
add some test cases
1 parent e24d01e commit 064f004

File tree

5 files changed

+136
-11
lines changed

5 files changed

+136
-11
lines changed

‎shared/src/test/diff/gadt/GADT1.mls

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -40,11 +40,11 @@ fun len(xs: Vec['l, 'a]) = if xs is
4040
//│ fun len: forall 'l0 'a0. Vec['l0, 'a0] -> Int
4141

4242
fun map: ('A -> 'B, Vec['L, 'A]) -> Vec['L, 'B]
43-
fun map[L, A, B](f, xs: Vec[L, A]): Vec[L, 'B] = if xs is
44-
Nil then new Nil : Vec[xs.L, B]
45-
Cons(h, t) then Cons(f(h), map(f, t)) : Vec[xs.L, B]
46-
//│ fun map: forall 'A 'B 'L. ((??T & 'A) -> 'B, xs: Vec['L, 'A]) -> Vec['L, 'B]
47-
//│ fun map: forall 'A0 'B0 'L0. ('A0 -> 'B0, Vec['L0, 'A0]) -> Vec['L0, 'B0]
43+
fun map[L, A, B](f, xs: Vec[L, A]): Vec[xs.L, 'B] = if xs is
44+
Nil then new Nil
45+
Cons(h, t) then Cons(f(h), map(f, t))
46+
//│ fun map: forall 'A 'B 'L 'L0 'B0 'B1. ((??T & 'A) -> 'B, xs: Vec['L, 'A]) -> Vec[in S[in ??H out nothing] & 'L0 | Z & 'L1 | 'L out 'L & (Z & 'L0 | 'L1 & (S[out ??H] | 'L0)), in 'B0 | 'B & 'B1 out 'B0 & ('B | 'B1)]
47+
//│ fun map: forall 'A0 'B2 'L2. ('A0 -> 'B2, Vec['L2, 'A0]) -> Vec['L2, 'B2]
4848

4949
// TODO
5050
fun zipSum: (Vec['L, Int], Vec['L, Int]) -> Vec['L, Int]

‎shared/src/test/diff/gadt/GADT2.mls

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -103,10 +103,10 @@ fun head[T](t: Perfect[T]): Int = if t is
103103
//│ fun head: forall 'T0. Perfect['T0] -> Int
104104

105105
fun flip: Perfect['A] -> Perfect['A]
106-
fun flip[A](t: Perfect[A]): Perfect[A] = if t is
107-
Leaf(a) then Leaf(a) : Perfect[t.T]
108-
Node(l, r) then Node(flip(r), flip(l)) : Perfect[t.T]
109-
//│ fun flip: forall 'A. (t: Perfect['A]) -> Perfect['A]
106+
fun flip[A](t: Perfect[A]): Perfect[t.T] = if t is
107+
Leaf(a) then Leaf(a)
108+
Node(l, r) then Node(flip(r), flip(l))
109+
//│ fun flip: forall 'A 'T. (t: Perfect['A]) -> Perfect[in Int & 'T0 | [nothing, nothing] & 'T | 'A out 'A & ([??A, ??A] & 'T0 | 'T & (Int | 'T0))]
110110
//│ fun flip: forall 'A0. Perfect['A0] -> Perfect['A0]
111111

112112
let test1 = Node(Node(Leaf(1), Leaf(2)), Node(Leaf(3), Leaf(4)))

‎shared/src/test/diff/gadt/GADT5.mls

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ module MkU extends U[()]
1515
fun v1(u: U['a], a: ()) = if u is MkU then a
1616
//│ fun v1: forall 'a. (u: U['a], a: ()) -> ()
1717

18-
fun v2(a, u: U['a]) = if u is MkU then if a is () then () as u.A
19-
//│ fun v2: forall 'a. ((), u: U['a]) -> (() & 'a)
18+
fun v2(a, u: U['a]) = if u is MkU then if a is () then ()
19+
//│ fun v2: forall 'a. ((), u: U['a]) -> ()
2020

2121
fun v3[T](u: U[T]): T = if u is MkU then () as u.A
2222
//│ fun v3: forall 'T. (u: U['T]) -> 'T

‎shared/src/test/diff/gadt/GADT6.mls

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -112,3 +112,40 @@ e2(Refl(), Refl(), true)
112112
//│ true
113113
//│ res
114114
//│ = true
115+
116+
117+
abstract class R[type A]: RI | RB
118+
class RI(x: Int) extends R[Int]
119+
class RB(x: Bool) extends R[Bool]
120+
//│ abstract class R[A]: RB | RI
121+
//│ class RI(x: Int) extends R
122+
//│ class RB(x: Bool) extends R
123+
124+
125+
126+
fun u2[A](x: R[A], y: R[A]) = (if x is
127+
RI(_) then RI as (x.A => R[x.A])
128+
RB(_) then RB as (x.A => R[x.A])
129+
) (if y is
130+
RI(a) then (a as y.A) as x.A
131+
RB(a) then (a as y.A) as x.A
132+
)
133+
//│ fun u2: forall 'A. (x: R['A], y: R['A]) -> R[in Int & 'A0 | 'A | 'A1 & Bool out 'A & (Int & 'A1 | 'A0 & (Bool | 'A1))]
134+
135+
:e
136+
u2(RB(false), RI(1))
137+
//│ ╔══[ERROR] Type mismatch in application:
138+
//│ ║ l.136: u2(RB(false), RI(1))
139+
//│ ║ ^^^^^^^^^^^^^^^^^^^^
140+
//│ ╟── type `Int` is not an instance of type `Bool`
141+
//│ ║ l.118: class RI(x: Int) extends R[Int]
142+
//│ ║ ^^^
143+
//│ ╟── Note: constraint arises from type reference:
144+
//│ ║ l.119: class RB(x: Bool) extends R[Bool]
145+
//│ ║ ^^^^
146+
//│ ╟── Note: method type parameter A is defined at:
147+
//│ ║ l.126: fun u2[A](x: R[A], y: R[A]) = (if x is
148+
//│ ╙── ^
149+
//│ error
150+
//│ res
151+
//│ = RB {}

‎shared/src/test/diff/gadt/HOA.mls

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,88 @@
1+
:NewDefs
2+
3+
abstract class HOA[type T]: Lit[T] | Abs[?,?] | App[?,T]
4+
class Lit[A](x: A) extends HOA[A]
5+
class Abs[A, B](f: A => HOA[B]) extends HOA[A => B]
6+
class App[A, B](f: HOA[A => B], x: HOA[A]) extends HOA[B]
7+
//│ abstract class HOA[T]: Abs[nothing, ?] | App[?, T] | Lit[T]
8+
//│ class Lit[A](x: A) extends HOA
9+
//│ class Abs[A, B](f: A -> HOA[B]) extends HOA
10+
//│ class App[A, B](f: HOA[A -> B], x: HOA[A]) extends HOA
11+
12+
fun eval: forall 'T : HOA['T] -> 'T
13+
fun eval(e: HOA['T]): e.T = if e is
14+
Lit(x) then x
15+
Abs(f) then x => eval(f(x))
16+
App(f, x) then eval(f)(eval(x))
17+
//│ fun eval: forall 'T 'a. (e: HOA['T]) -> 'a
18+
//│ fun eval: forall 'T0. HOA['T0] -> 'T0
19+
//│ where
20+
//│ 'T <: 'a | ~(nothing -> ??B)
21+
22+
eval(App(Abs(x => Lit(x + 1)), Lit(1)))
23+
//│ Int
24+
//│ res
25+
//│ = 2
26+
27+
:e
28+
eval(App(Abs(x => Lit(x + 1)), Lit(true)))
29+
//│ ╔══[ERROR] Type mismatch in application:
30+
//│ ║ l.28: eval(App(Abs(x => Lit(x + 1)), Lit(true)))
31+
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
32+
//│ ╟── reference of type `true` is not an instance of `Int`
33+
//│ ║ l.28: eval(App(Abs(x => Lit(x + 1)), Lit(true)))
34+
//│ ║ ^^^^
35+
//│ ╟── Note: constraint arises from reference:
36+
//│ ║ l.28: eval(App(Abs(x => Lit(x + 1)), Lit(true)))
37+
//│ ║ ^
38+
//│ ╟── Note: type parameter A is defined at:
39+
//│ ║ l.6: class App[A, B](f: HOA[A => B], x: HOA[A]) extends HOA[B]
40+
//│ ╙── ^
41+
//│ Int
42+
//│ res
43+
//│ = 2
44+
45+
abstract class HList[type T]: HNil | HCons[?,?]
46+
module HNil extends HList[[]]
47+
class HCons[type A, type B](h: A, t: HList[B]) extends HList[[A, B]]
48+
//│ abstract class HList[T]: HCons[anything, ?] | HNil
49+
//│ module HNil extends HList
50+
//│ class HCons[A, B](h: A, t: HList[B]) extends HList
51+
52+
// FIXME
53+
fun hhead : HList[['A, 'B]] -> 'A
54+
fun hhead[A, B](xs: HList[[A, B]]): A =
55+
if xs is HCons(h, t) then h : xs.A else error
56+
//│ ╔══[ERROR] Type mismatch in type ascription:
57+
//│ ║ l.55: if xs is HCons(h, t) then h : xs.A else error
58+
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
59+
//│ ╟── type `anything` does not match type `A | ~??A`
60+
//│ ║ l.55: if xs is HCons(h, t) then h : xs.A else error
61+
//│ ║ ^^
62+
//│ ╟── Note: method type parameter A is defined at:
63+
//│ ║ l.54: fun hhead[A, B](xs: HList[[A, B]]): A =
64+
//│ ╙── ^
65+
//│ fun hhead: forall 'A 'B. (xs: HList[['A, 'B]]) -> 'A
66+
//│ fun hhead: forall 'A0 'B0. HList[['A0, 'B0]] -> 'A0
67+
68+
// FIXME
69+
fun htail : HList[['A, 'B]] -> HList['B]
70+
fun htail[A, B](xs: HList[[A, B]]): HList[B] =
71+
if xs is HCons(h, t) then t : HList[xs.B] else error
72+
//│ ╔══[ERROR] Type mismatch in type ascription:
73+
//│ ║ l.71: if xs is HCons(h, t) then t : HList[xs.B] else error
74+
//│ ║ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
75+
//│ ╟── type `B` does not match type `nothing`
76+
//│ ║ l.70: fun htail[A, B](xs: HList[[A, B]]): HList[B] =
77+
//│ ║ ^
78+
//│ ╟── Note: constraint arises from type selection:
79+
//│ ║ l.71: if xs is HCons(h, t) then t : HList[xs.B] else error
80+
//│ ╙── ^^
81+
//│ fun htail: forall 'A 'B. (xs: HList[['A, 'B]]) -> HList['B]
82+
//│ fun htail: forall 'A0 'B0. HList[['A0, 'B0]] -> HList['B0]
83+
84+
fun hlen : HList['A] -> Int
85+
fun hlen(xs: HList['a]): Int =
86+
if xs is HCons(h, t) then 1 + hlen(t) else 0
87+
//│ fun hlen: forall 'a. (xs: HList['a]) -> Int
88+
//│ fun hlen: forall 'A. HList['A] -> Int

0 commit comments

Comments
 (0)