Skip to content

Commit 6543a8a

Browse files
committed
basic implementation of adding cases to Sum
1 parent b07ff86 commit 6543a8a

1 file changed

Lines changed: 75 additions & 3 deletions

File tree

forja/src/Lang.scala

Lines changed: 75 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,12 +43,15 @@ object Lang:
4343

4444
abstract class Sum extends Node:
4545
type Case <: Node
46+
class HasInner[I <: Sum]
4647
object Opaque:
4748
into opaque type T = Any
4849
extension (t: T)
49-
inline def ex(using
50+
transparent inline def ex(using
5051
inline ng: NotGiven[ReplaceWith[?]],
51-
)(using et: Sum.EffectiveType[Case]): et.T =
52+
)(using et: Sum.EffectiveType[Case])(using
53+
ei: Sum.EffectiveInnerType[Sum.this.type],
54+
): et.T | ei.T =
5255
t.asInstanceOf
5356
end ex
5457
end extension
@@ -57,10 +60,31 @@ object Lang:
5760

5861
inline given subtype: [T] => (inline ng: NotGiven[ReplaceWith[?]])
5962
=> (et: Sum.EffectiveType[Case])
60-
=> InlineConversion.ByCast[et.T, this.T] = InlineConversion.ByCast()
63+
=> (ei: Sum.EffectiveInnerType[Sum.this.type])
64+
=> InlineConversion.ByCast[et.T | ei.T, this.T] = InlineConversion.ByCast()
6165
end Sum
6266

6367
object Sum:
68+
sealed trait EffectiveInnerType[S <: Sum] extends Instanceless:
69+
type T
70+
end EffectiveInnerType
71+
object EffectiveInnerType:
72+
type Aux[S <: Sum, T0] = EffectiveInnerType[S] { type T = T0 }
73+
74+
inline given noInner: [S <: Sum] => (S: S)
75+
=> (inline ng: NotGiven[S.HasInner[?]])
76+
=> Aux[S, Nothing] =
77+
Instanceless[Aux[S, Nothing]]
78+
79+
inline given hasInner: [S <: Sum, I <: Sum] => (S: S)
80+
=> S.HasInner[I]
81+
=> (I: I)
82+
=> (et: Sum.EffectiveType[I.Case])
83+
=> (ie: EffectiveInnerType[I])
84+
=> Aux[S, et.T | ie.T] =
85+
Instanceless[Aux[S, et.T | ie.T]]
86+
end EffectiveInnerType
87+
6488
sealed trait EffectiveType[C <: Sum#Case] extends Instanceless:
6589
type T
6690
end EffectiveType
@@ -269,5 +293,53 @@ object Test:
269293
// case L2.Ping.Bob(s, opt) =>
270294
// println("bob")
271295
end match
296+
297+
innerSumTest()
272298
end main
299+
300+
def innerSumTest(): Unit =
301+
trait L1 extends Lang:
302+
object Foo extends Lang.Term[(i: Int, j: Int)]
303+
304+
object Ping extends Lang.Sum:
305+
sealed trait Case extends Lang.Node
306+
object Pong extends Lang.Term[(k: Int, foo: Foo.T)], Case
307+
object Bob extends Lang.Term[(k: Int, foo: Foo.T)], Case
308+
end Ping
309+
end L1
310+
object L1 extends L1
311+
312+
trait L2 extends Lang.Extend[L1]:
313+
export up.{Foo as _, Ping as _, *}
314+
object Bar extends Lang.Term[(s: String, opt: Option[up.Foo.T])]
315+
object Ping extends Lang.Sum:
316+
given HasInner[up.Ping.type]()
317+
export up.Ping.{Case as _, Opaque as _, *}
318+
sealed trait Case extends Lang.Node
319+
object NewCase extends Lang.Term[(s: String, opt: Option[up.Foo.T])], Case
320+
end Ping
321+
322+
given up.Foo.ReplaceWith[Bar.type]()
323+
given up.Ping.ReplaceWith[Ping.type]()
324+
end L2
325+
object L2 extends L2
326+
327+
val nc: L2.Ping.T = L2.Ping.NewCase(s = "hello", opt = None)
328+
println(nc)
329+
330+
val pong: L2.Ping.T = L2.Ping.Pong(k = 12, foo = L2.Bar(s = "x", opt = None))
331+
println(pong)
332+
333+
nc.ex match
334+
case L2.Ping.NewCase(s, opt) => println(s"NewCase: $s")
335+
case L2.Ping.Pong(k, foo) => println(s"Pong: $k")
336+
case L2.Ping.Bob(k, foo) => println(s"Bob: $k")
337+
end match
338+
339+
pong.ex match
340+
case L2.Ping.NewCase(s, opt) => println(s"NewCase: $s")
341+
case L2.Ping.Pong(k, foo) => println(s"Pong: $k")
342+
case L2.Ping.Bob(k, foo) => println(s"Bob: $k")
343+
end match
344+
end innerSumTest
273345
end Test

0 commit comments

Comments
 (0)