Skip to content

Commit

Permalink
update EffectsM
Browse files Browse the repository at this point in the history
  • Loading branch information
mio-19 committed Oct 24, 2024
1 parent 80c6edb commit 0a7ef3c
Show file tree
Hide file tree
Showing 4 changed files with 17 additions and 13 deletions.
23 changes: 14 additions & 9 deletions syntax/src/main/scala/chester/syntax/core/Term.scala
Original file line number Diff line number Diff line change
Expand Up @@ -258,13 +258,21 @@ sealed trait TermWithUniqid extends Term with TermWithUniqidT[Term] derives Read
def switchUniqId(r: UReplacer): TermWithUniqid
}

trait MetaTermC[+Rec <: TermT[Rec]] extends TermT[Rec] {
sealed trait EffectsMT[+Rec <: TermT[Rec]] extends TermT[Rec] {
override type ThisTree <: EffectsMT[Rec]
}

sealed trait EffectsM extends Term with EffectsMT[Term] derives ReadWriter {
override type ThisTree <: EffectsM
}

trait MetaTermC[+Rec <: TermT[Rec]] extends TermT[Rec] with EffectsMT[Rec] {
override type ThisTree <: MetaTermC[Rec]
def impl: HoldNotReadable[?]
override def toTerm: MetaTerm = MetaTerm(impl, meta)
}

case class MetaTerm(impl: HoldNotReadable[?], meta: OptionTermMeta) extends Term with MetaTermC[Term] {
case class MetaTerm(impl: HoldNotReadable[?], meta: OptionTermMeta) extends Term with MetaTermC[Term] with EffectsM {
override type ThisTree = MetaTerm
def unsafeRead[T]: T = impl.inner.asInstanceOf[T]

Expand Down Expand Up @@ -792,14 +800,12 @@ case class Matching(
case class FunctionType(
telescope: Vector[TelescopeTerm],
resultTy: Term,
effects0: Term = NoEffect,
effects: EffectsM = NoEffect,
meta: OptionTermMeta
) extends Term {
require(EffectsM.is(effects0))
def effects: EffectsM = effects0.asInstanceOf[EffectsM]
override type ThisTree = FunctionType
override def descent(f: Term => Term, g: SpecialMap): FunctionType = thisOr(
copy(telescope = telescope.map(g), resultTy = f(resultTy), effects0 = g(effects))
copy(telescope = telescope.map(g), resultTy = f(resultTy), effects = g(effects))
)

override def toDoc(using options: PrettierOptions): Doc = {
Expand Down Expand Up @@ -963,7 +969,7 @@ sealed trait Effect extends Term derives ReadWriter {
override def toDoc(using options: PrettierOptions): Doc = Doc.text(name)
}

case class Effects(effects: Map[LocalV, Term] = HashMap.empty, meta: OptionTermMeta) extends Term derives ReadWriter {
case class Effects(effects: Map[LocalV, Term] = HashMap.empty, meta: OptionTermMeta) extends Term with EffectsM derives ReadWriter {
override type ThisTree = Effects
override def descent(f: Term => Term, g: SpecialMap): Effects = thisOr(
copy(effects = effects.map { case (k, v) => g(k) -> f(v) })
Expand Down Expand Up @@ -1177,10 +1183,9 @@ case class BlockTerm(
case class Annotation(
term: Term,
ty: Option[Term],
effects: Option[Term],
effects: Option[EffectsM],
meta: OptionTermMeta
) extends Term {
effects.foreach(x => require(EffectsM.is(x)))
override type ThisTree = Annotation
override def descent(f: Term => Term, g: SpecialMap): Annotation = thisOr(
copy(
Expand Down
4 changes: 2 additions & 2 deletions syntax/src/main/scala/chester/syntax/core/orm/OrM.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ import scala.language.implicitConversions

/** note that this disallow non normal form terms, so avoid using it when non normal form terms are allowed */
type OrM[T <: Term] = (T | MetaTerm)

/*
// This type can't be used if scala2.13 interoperability is required
type EffectsM = OrM[Effects]
Expand All @@ -18,7 +18,7 @@ object EffectsM {
case _ => false
}
}

*/
given OrMRW[T <: Term](using rw: ReadWriter[Term]): ReadWriter[OrM[T]] =
rw.asInstanceOf[ReadWriter[OrM[T]]]

Expand Down
1 change: 0 additions & 1 deletion tyck/src/main/scala/chester/tyck/ElaboraterCommon.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,6 @@ import chester.resolve.{SimpleDesalt, resolveOpSeq}
import chester.syntax.Name
import chester.syntax.concrete.*
import chester.syntax.core.*
import chester.syntax.core.orm.EffectsM
import chester.utils.*
import chester.utils.propagator.CommonPropagator
import chester.uniqid.*
Expand Down
2 changes: 1 addition & 1 deletion tyck/src/main/scala/chester/tyck/ElaboraterFunction.scala
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ trait ProvideElaboraterFunction extends ElaboraterFunction {

// Build the function type by folding over the telescopes
val functionType =
FunctionType(telescopeTerms, returnType, effects0 = toTerm(effects), meta = None)
FunctionType(telescopeTerms, returnType, effects = toTerm(effects), meta = None)

// Unify the expected type with the constructed function type
unify(ty, functionType, expr)
Expand Down

0 comments on commit 0a7ef3c

Please sign in to comment.