Skip to content

Instantly share code, notes, and snippets.

@FlorianCassayre
Last active May 19, 2021 13:18
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save FlorianCassayre/a31d0d79c732475ec80a7812f94178c7 to your computer and use it in GitHub Desktop.
Some tests on ADTs with Scala 3
import scala.compiletime.constValue
object Logic extends App:
// Definitions
enum Formula:
case Variable[Id <: String & Singleton](val id: Id) extends Formula
case True extends Formula
case False extends Formula
case And[L <: Formula, R <: Formula](left: L, right: R) extends Formula
case Or[L <: Formula, R <: Formula](left: L, right: R) extends Formula
case Not[F <: Formula](formula: F) extends Formula
// Sugar
import Formula._
object Variable:
inline given apply[Id <: String & Singleton]: Variable[Id] = new Variable[Id](constValue[Id])
import Variable.apply
type True = True.type
type False = False.type
type &&[L <: Formula, R <: Formula] = And[L, R]
type ||[L <: Formula, R <: Formula] = Or[L, R]
type ![F <: Formula] = Not[F]
extension [L <: Formula](left: L)
def &&[R <: Formula](right: R): L && R = And(left, right)
def ||[R <: Formula](right: R): L || R = Or(left, right)
def unary_! : ![L] = Not(left)
given [L <: Formula, R <: Formula](using left: L, right: R): (L && R) = left && right
given [L <: Formula, R <: Formula](using left: L, right: R): (L || R) = left || right
given [F <: Formula](using formula: F): ![F] = !formula
given True: Formula.True.type = True
given False: Formula.False.type = False
def $[T <: Formula](using T): T = summon[T]
// Tests
val a: (Variable["a"] && True) || ![False] = $
assert(a == ((Variable["a"] && True) || !False))
println($: False)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment