Skip to content

Commit

Permalink
Better handling of deriving equality
Browse files Browse the repository at this point in the history
  • Loading branch information
martinberger committed Jan 9, 2025
1 parent 6a3edab commit e893d29
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 12 deletions.
4 changes: 1 addition & 3 deletions src/main/scala/logic/Kinds.scala
Original file line number Diff line number Diff line change
@@ -1,11 +1,9 @@
package Prover

sealed trait Kind
sealed trait Kind derives CanEqual
case object TyKind extends Kind
case class ConstructorKind(k: Kind) extends Kind

given CanEqual[Kind, Kind] = CanEqual.derived

object TyFunctionKind:
def apply(): Kind = ConstructorKind(TyKind)
def unapply(kind: Kind): Boolean =
Expand Down
4 changes: 1 addition & 3 deletions src/main/scala/logic/Taint.scala
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
package Prover

sealed trait Taint
sealed trait Taint derives CanEqual
case object I extends Taint
case object W extends Taint
case object C extends Taint
case object CH extends Taint

given CanEqual[Taint, Taint] = CanEqual.derived

// Taint semilattice has this order:
//
// CH
Expand Down
4 changes: 1 addition & 3 deletions src/main/scala/logic/Term.scala
Original file line number Diff line number Diff line change
@@ -1,13 +1,11 @@
package Prover

sealed trait Term
sealed trait Term derives CanEqual
case class Var(name: String, ty: Ty) extends Term { override def toString: String = s"${name}" } // ^${ty.toString}" }
case class Const(c: String, ty: Ty) extends Term { override def toString: String = s"${c}" }
case class App(l: Term, r: Term) extends Term { override def toString: String = s"(${l}, ${r})" }
case class Lam(x: Var, body: Term) extends Term

given CanEqual[Term, Term] = CanEqual.derived

object Term:

def ftv(t: Term): Set[TyVar] =
Expand Down
4 changes: 1 addition & 3 deletions src/main/scala/logic/Ty.scala
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
package Prover

sealed trait Ty
sealed trait Ty derives CanEqual
case class TyVar(name: String) extends Ty { override def toString: String = s"${name}" }
case class TyFormer(name: String, kind: Kind) extends Ty { override def toString: String = s"" } //[${name}:${kind.toString}]" }
case class TyApp(l: Ty, r: Ty) extends Ty { override def toString: String = s"(${l}${r})" }

given CanEqual[Ty, Ty] = CanEqual.derived

object Ty:

def ftv(ty: Ty): Set[TyVar] =
Expand Down

0 comments on commit e893d29

Please sign in to comment.