diff --git a/eval/src/main/scala/chester/eval/Eval.scala b/eval/src/main/scala/chester/eval/Eval.scala index ce7e5a1e..a920156a 100644 --- a/eval/src/main/scala/chester/eval/Eval.scala +++ b/eval/src/main/scala/chester/eval/Eval.scala @@ -2,6 +2,7 @@ package chester.eval import chester.runtime.Value import chester.syntax.core.* +import chester.syntax.core.interface.{BooleanTermC, TermT} case class EvalContext() diff --git a/syntax/shared/src/main/scala/chester/syntax/core/abstract/Term.scala b/syntax/shared/src/main/scala/chester/syntax/core/interface/Term.scala similarity index 88% rename from syntax/shared/src/main/scala/chester/syntax/core/abstract/Term.scala rename to syntax/shared/src/main/scala/chester/syntax/core/interface/Term.scala index 2b1706d5..d988efbd 100644 --- a/syntax/shared/src/main/scala/chester/syntax/core/abstract/Term.scala +++ b/syntax/shared/src/main/scala/chester/syntax/core/interface/Term.scala @@ -1,11 +1,12 @@ // TODO: More correctly implement toDoc -package chester.syntax.core +package chester.syntax.core.interface import chester.doc.* import chester.doc.const.{ColorProfile, Docs} import chester.error.* import chester.syntax.* import chester.syntax.core.orm.* +import chester.syntax.core.simple.{EffectsM, LocalV, ObjectStmtTerm, TelescopeTermF} import chester.uniqid.* import chester.utils.* import chester.utils.doc.* @@ -53,7 +54,7 @@ trait CallingArgTermC[Term <: TermT[Term]] extends WHNFT[Term] { def ty: Term def name: Option[Name] def vararg: Boolean - override def toTerm: CallingArgTerm = CallingArgTerm(value.toTerm, ty.toTerm, name, vararg, meta) + def cons: CallingArgTermF[Term, ThisTree] override def toDoc(using options: PrettierOptions): Doc = { @@ -85,7 +86,7 @@ trait CallingC[Term <: TermT[Term]] extends WHNFT[Term] { override type ThisTree <: CallingC[Term] def args: Vector[CallingArgTermC[Term]] def implicitly: Boolean - override def toTerm: Calling = Calling(args.map(_.toTerm), implicitly, meta) + def cons: CallingF[Term, ThisTree] override def toDoc(using options: PrettierOptions): Doc = { @@ -114,7 +115,7 @@ trait FCallTermC[Term <: TermT[Term]] extends WHNFT[Term] { override type ThisTree <: FCallTermC[Term] def f: Term def args: Vector[CallingC[Term]] - override def toTerm: FCallTerm = FCallTerm(f.toTerm, args.map(_.toTerm), meta) + def cons: FCallTermF[Term, ThisTree] override def toDoc(using options: PrettierOptions): Doc = { @@ -147,8 +148,6 @@ trait BindC[Term <: TermT[Term]] extends PatT[Term] { def ty: Term def cons: BindF[Term, ThisTree] - override def toTerm: Bind = Bind(bind.toTerm, ty.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = bind.toDoc <+> Docs.`:` <+> ty.toDoc def cpy(bind: LocalVC[Term] = bind, ty: Term = ty, meta: OptionTermMeta = meta): ThisTree = cons.newBind(bind, ty, meta) @@ -172,10 +171,7 @@ trait TermT[Term <: TermT[Term]] extends Any with ToDoc with Tree[Term] { def meta: OptionTermMeta def whnf: Trilean - def toTerm: simple.Term = { - assert(this.isInstanceOf[simple.Term], "forgot to implement toTerm?") - this.asInstanceOf[simple.Term] - } + def sourcePos: Option[SourcePos] = meta.map(_.sourcePos) } @@ -208,7 +204,7 @@ trait EffectsMT[Term <: TermT[Term]] extends TermT[Term] { trait MetaTermC[Term <: TermT[Term]] extends TermT[Term] with EffectsMT[Term] with SpecialTermT[Term] { override type ThisTree <: MetaTermC[Term] def impl: HoldNotReadable[?] - override def toTerm: MetaTerm = MetaTerm(impl, meta) + override def toDoc(using options: PrettierOptions): Doc = Doc.group("Meta" <> Doc.text(impl.toString)) @@ -220,7 +216,6 @@ trait MetaTermC[Term <: TermT[Term]] extends TermT[Term] with EffectsMT[Term] wi trait ListTermC[Term <: TermT[Term]] extends TermT[Term] with WHNFT[Term] { override type ThisTree <: ListTermC[Term] def terms: Vector[Term] - override def toTerm: ListTerm = ListTerm(terms.map(_.toTerm), meta) } trait TypeTermT[Term <: TermT[Term]] extends WHNFT[Term] { @@ -235,12 +230,10 @@ trait SortT[Term <: TermT[Term]] extends TypeTermT[Term] { trait TypeT[Term <: TermT[Term]] extends SortT[Term] { override type ThisTree <: TypeT[Term] def level: Term - override def toTerm: Type = Type(level.toTerm, meta) } trait LevelTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: LevelTypeC[Term] - override def toTerm: LevelType = LevelType(meta) } trait LevelT[Term <: TermT[Term]] extends TypeTermT[Term] with WHNFT[Term] { @@ -250,12 +243,10 @@ trait LevelT[Term <: TermT[Term]] extends TypeTermT[Term] with WHNFT[Term] { trait LevelFiniteC[Term <: TermT[Term]] extends LevelT[Term] { override type ThisTree <: LevelFiniteC[Term] def n: Term - override def toTerm: LevelFinite = LevelFinite(n.toTerm, meta) } trait LevelUnrestrictedC[Term <: TermT[Term]] extends LevelT[Term] { override type ThisTree <: LevelUnrestrictedC[Term] - override def toTerm: LevelUnrestricted = LevelUnrestricted(meta) } enum Usage derives ReadWriter { @@ -265,14 +256,13 @@ enum Usage derives ReadWriter { trait PropC[Term <: TermT[Term]] extends SortT[Term] { override type ThisTree <: PropC[Term] def level: Term - override def toTerm: Prop = Prop(level.toTerm, meta) } trait FTypeC[Term <: TermT[Term]] extends SortT[Term] { override type ThisTree <: FTypeC[Term] def level: Term def copy(level: Term = level, meta: OptionTermMeta = meta): ThisTree - override def toTerm: FType = FType(level.toTerm, meta) + override def descent(f: Term => Term, g: TreeMap[Term]): Term = thisOr(copy(level = f(level))) override def toDoc(using options: PrettierOptions): Doc = @@ -290,13 +280,11 @@ trait AbstractIntTermT[Term <: TermT[Term]] extends LiteralTermT[Term] { trait IntTermC[Term <: TermT[Term]] extends LiteralTermT[Term] with AbstractIntTermT[Term] { override type ThisTree <: IntTermC[Term] def value: Int - override def toTerm: IntTerm = IntTerm(value, meta) } trait IntegerTermC[Term <: TermT[Term]] extends LiteralTermT[Term] with AbstractIntTermT[Term] { override type ThisTree <: IntegerTermC[Term] def value: BigInt - override def toTerm: IntegerTerm = IntegerTerm(value, meta) } trait WithTypeT[Term <: TermT[Term]] extends TermT[Term] { @@ -306,34 +294,28 @@ trait WithTypeT[Term <: TermT[Term]] extends TermT[Term] { trait IntegerTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: IntegerTypeC[Term] - override def toTerm: IntegerType = IntegerType(meta) } trait IntTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: IntTypeC[Term] - override def toTerm: IntType = IntType(meta) } trait UIntTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: UIntTypeC[Term] - override def toTerm: UIntType = UIntType(meta) } trait NaturalTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: NaturalTypeC[Term] - override def toTerm: NaturalType = NaturalType(meta) } trait RationalTermC[Term <: TermT[Term]] extends LiteralTermT[Term] { override type ThisTree <: RationalTermC[Term] def value: Rational - override def toTerm: RationalTerm = RationalTerm(value, meta) } trait BooleanTermC[Term <: TermT[Term]] extends LiteralTermT[Term] { override type ThisTree <: BooleanTermC[Term] def value: Boolean - override def toTerm: BooleanTerm = BooleanTerm(value, meta) override def descent(f: Term => Term, g: TreeMap[Term]): Term = this @@ -343,56 +325,46 @@ trait BooleanTermC[Term <: TermT[Term]] extends LiteralTermT[Term] { trait BooleanTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: BooleanTypeC[Term] - override def toTerm: BooleanType = BooleanType(meta) } trait StringTermC[Term <: TermT[Term]] extends LiteralTermT[Term] { override type ThisTree <: StringTermC[Term] def value: String - override def toTerm: StringTerm = StringTerm(value, meta) } trait SymbolTermC[Term <: TermT[Term]] extends LiteralTermT[Term] { override type ThisTree <: SymbolTermC[Term] def value: String - override def toTerm: SymbolTerm = SymbolTerm(value, meta) } trait RationalTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: RationalTypeC[Term] - override def toTerm: RationalType = RationalType(meta) } trait FloatTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: FloatTypeC[Term] - override def toTerm: FloatType = FloatType(meta) } trait StringTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: StringTypeC[Term] - override def toTerm: StringType = StringType(meta) } trait SymbolTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: SymbolTypeC[Term] - override def toTerm: SymbolType = SymbolType(meta) } trait AnyTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: AnyTypeC[Term] def level: Term - override def toTerm: AnyType = AnyType(level.toTerm, meta) } trait NothingTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: NothingTypeC[Term] - override def toTerm: NothingType = NothingType(meta) } trait LiteralTypeC[Term <: TermT[Term]] extends TypeTermT[Term] with WithTypeT[Term] { override type ThisTree <: LiteralTypeC[Term] def literal: LiteralTermT[Term] - override def toTerm: LiteralType = LiteralType(literal.toTerm.asInstanceOf[LiteralTerm], meta) } @FunctionalInterface @@ -409,8 +381,6 @@ trait ArgTermC[Term <: TermT[Term]] extends WHNFT[Term] { def vararg: Boolean def cons: ArgTermF[Term, ThisTree] - override def toTerm: ArgTerm = ArgTerm(bind, ty.toTerm, default.map(_.toTerm), vararg, meta) - override def toDoc(using options: PrettierOptions): Doc = { val varargDoc = if (vararg) Docs.`...` else Doc.empty val defaultDoc = default.map(d => Docs.`=` <+> d.toDoc).getOrElse(Doc.empty) @@ -433,8 +403,6 @@ trait TelescopeTermC[Term <: TermT[Term]] extends WHNFT[Term] { def implicitly: Boolean def cons: TelescopeTermF[Term, ThisTree] - override def toTerm: TelescopeTerm = TelescopeTerm(args.map(_.toTerm), implicitly, meta) - override def toDoc(using options: PrettierOptions): Doc = { val argsDoc = args.map(_.toDoc).reduceLeftOption(_ <+> _).getOrElse(Doc.empty) @@ -468,8 +436,6 @@ trait FunctionC[Term <: TermT[Term]] extends WHNFT[Term] { def body: Term def cons: FunctionF[Term, ThisTree] - override def toTerm: Function = Function(ty.toTerm, body.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = { val paramsDoc = ty.telescope.map(_.toDoc).reduceLeftOption(_ <+> _).getOrElse(Doc.empty) val returnTypeDoc = Docs.`:` <+> ty.resultTy.toDoc @@ -505,13 +471,6 @@ trait FunctionTypeC[Term <: TermT[Term]] extends WHNFT[Term] { def effects: EffectsM def cons: FunctionTypeF[Term, ThisTree] - override def toTerm: FunctionType = FunctionType( - telescope.map(_.toTerm), - resultTy.toTerm, - effects, - meta - ) - override def toDoc(using options: PrettierOptions): Doc = { val telescopeDoc = telescope.map(_.toDoc).reduceLeftOption(_ <+> _).getOrElse(Doc.empty) @@ -550,8 +509,6 @@ trait ObjectClauseValueTermC[Term <: TermT[Term]] extends WHNFT[Term] { def value: Term def cons: ObjectClauseValueTermF[Term, ThisTree] - override def toTerm: ObjectClauseValueTerm = ObjectClauseValueTerm(key.toTerm, value.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = group( key.toDoc <+> Doc.text("=") <+> value.toDoc ) @@ -574,8 +531,6 @@ trait ObjectTermC[Term <: TermT[Term]] extends WHNFT[Term] { def clauses: Vector[ObjectClauseValueTermC[Term]] def cons: ObjectTermF[Term, ThisTree] - override def toTerm: ObjectTerm = ObjectTerm(clauses.map(_.toTerm), meta) - override def toDoc(using options: PrettierOptions): Doc = Doc.wrapperlist(Docs.`{`, Docs.`}`, ",")(clauses.map(_.toDoc)) @@ -599,8 +554,6 @@ trait ObjectTypeC[Term <: TermT[Term]] extends WHNFT[Term] { def exactFields: Boolean def cons: ObjectTypeF[Term, ThisTree] - override def toTerm: ObjectType = ObjectType(fieldTypes.map(_.toTerm), exactFields, meta) - override def toDoc(using options: PrettierOptions): Doc = Doc.wrapperlist("Object" Docs.`{`, Docs.`}`, ",")( fieldTypes.map(_.toDoc) @@ -637,8 +590,6 @@ trait LocalVC[Term <: TermT[Term]] extends ReferenceCallC[Term] { def uniqId: UniqidOf[LocalVC[Term]] def cons: LocalVF[Term, ThisTree] - override def toTerm: LocalV = LocalV(name, ty.toTerm, uniqId, meta) - override def toDoc(using options: PrettierOptions): Doc = Doc.text(name) def cpy(name: Name = name, ty: Term = ty, uniqId: UniqidOf[LocalVC[Term]] = uniqId, meta: OptionTermMeta = meta): ThisTree = @@ -660,8 +611,6 @@ trait ToplevelVC[Term <: TermT[Term]] extends ReferenceCallC[Term] { def uniqId: UniqidOf[ToplevelVC[Term]] def cons: ToplevelVF[Term, ThisTree] - override def toTerm: ToplevelV = ToplevelV(id, ty.toTerm, uniqId, meta) - override def toDoc(using options: PrettierOptions): Doc = group( id.toDoc <+> Docs.`.` <+> ty.toDoc ) @@ -678,7 +627,6 @@ trait ToplevelVC[Term <: TermT[Term]] extends ReferenceCallC[Term] { trait ErrorTermC[Term <: TermT[Term]] extends SpecialTermT[Term] { override type ThisTree <: ErrorTermC[Term] def problem: Problem - override def toTerm: ErrorTerm = ErrorTerm(problem, meta) override def toDoc(using options: PrettierOptions): Doc = problem.toDoc @@ -700,7 +648,6 @@ trait LetStmtTermC[Term <: TermT[Term]] extends StmtTermT[Term] { def value: Term def ty: Term def cons: LetStmtTermF[Term, ThisTree] - override def toTerm: LetStmtTerm = LetStmtTerm(localv.toTerm, value.toTerm, ty.toTerm, meta) override def toDoc(using options: PrettierOptions): Doc = { Doc.text("let ") <> localv.toDoc <> Doc.text(": ") <> ty.toDoc <> Doc.text(" = ") <> value.toDoc @@ -729,7 +676,6 @@ trait DefStmtTermC[Term <: TermT[Term]] extends StmtTermT[Term] { def value: Term def ty: Term def cons: DefStmtTermF[Term, ThisTree] - override def toTerm: DefStmtTerm = DefStmtTerm(localv.toTerm, value.toTerm, ty.toTerm, meta) override def toDoc(using options: PrettierOptions): Doc = { Doc.text("def ") <> localv.toDoc <> Doc.text(": ") <> ty.toDoc <> Doc.text(" = ") <> value.toDoc @@ -758,8 +704,6 @@ trait ExprStmtTermC[Term <: TermT[Term]] extends StmtTermT[Term] { def ty: Term def cons: ExprStmtTermF[Term, ThisTree] - override def toTerm: ExprStmtTerm = ExprStmtTerm(expr.toTerm, ty.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = expr.toDoc def cpy(expr: Term = expr, ty: Term = ty, meta: OptionTermMeta = meta): ThisTree = @@ -780,8 +724,6 @@ trait NonlocalOrLocalReturnC[Term <: TermT[Term]] extends StmtTermT[Term] { def value: Term def cons: NonlocalOrLocalReturnF[Term, ThisTree] - override def toTerm: NonlocalOrLocalReturn = NonlocalOrLocalReturn(value.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = Doc.text("return") <+> value.toDoc @@ -796,7 +738,6 @@ trait NonlocalOrLocalReturnC[Term <: TermT[Term]] extends StmtTermT[Term] { trait TupleTypeC[Term <: TermT[Term]] extends TypeTermT[Term] { override type ThisTree <: TupleTypeC[Term] def types: Vector[Term] - override def toTerm: TupleType = TupleType(types.map(_.toTerm), meta) override def toDoc(using options: PrettierOptions): Doc = { Doc.wrapperlist("Tuple" <> Docs.`[`, Docs.`]`, ",")(types) @@ -820,7 +761,6 @@ trait TupleTypeF[Term <: TermT[Term], ThisTree <: TupleTypeC[Term]] { trait TupleTermC[Term <: TermT[Term]] extends WHNFT[Term] { override type ThisTree <: TupleTermC[Term] def values: Vector[Term] - override def toTerm: TupleTerm = TupleTerm(values.map(_.toTerm), meta) override def toDoc(using options: PrettierOptions): Doc = { Doc.wrapperlist(Docs.`(`, Docs.`)`, ",")(values) @@ -852,8 +792,6 @@ trait BlockTermC[Term <: TermT[Term]] extends UnevalT[Term] { def result: Term def cons: BlockTermF[Term, ThisTree] - override def toTerm: BlockTerm = BlockTerm(statements.map(_.toTerm), result.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = { Doc.wrapperlist(Docs.`{`, Docs.`}`, ";")( (statements.map(_.toDoc) :+ result.toDoc) @@ -883,8 +821,6 @@ trait AnnotationC[Term <: TermT[Term]] extends UnevalT[Term] { def effects: Option[EffectsM] def cons: AnnotationF[Term, ThisTree] - override def toTerm: Annotation = Annotation(term.toTerm, ty.map(_.toTerm), effects, meta) - override def toDoc(using options: PrettierOptions): Doc = { val tyDoc = ty.map(Docs.`:` <+> _.toDoc).getOrElse(Doc.empty) val effectsDoc = effects.map(Docs.`/` <+> _.toDoc).getOrElse(Doc.empty) @@ -908,7 +844,6 @@ trait FieldTermC[Term <: TermT[Term]] extends WHNFT[Term] { def name: Name def ty: Term def cons: FieldTermF[Term, ThisTree] - override def toTerm: FieldTerm = FieldTerm(name, ty.toTerm, meta) override def toDoc(using options: PrettierOptions): Doc = Doc.text(name) <> Doc.text(": ") <> ty.toDoc @@ -950,8 +885,6 @@ trait RecordStmtTermC[Term <: TermT[Term]] extends TypeDefinitionT[Term] with St def fields: Vector[FieldTermC[Term]] def body: Option[BlockTermC[Term]] def cons: RecordStmtTermF[Term, ThisTree] - override def toTerm: RecordStmtTerm = - RecordStmtTerm(name, uniqId.asInstanceOf[UniqidOf[RecordStmtTerm]], fields.map(_.toTerm), body.map(_.toTerm), meta) override def toDoc(using options: PrettierOptions): Doc = { val fieldsDoc = fields.map(_.toDoc).reduceOption(_ <> Doc.text(", ") <> _).getOrElse(Doc.empty) @@ -992,8 +925,6 @@ trait ObjectCallTermC[Term <: TermT[Term]] extends UnevalT[Term] { def objectRef: Term def cons: ObjectCallTermF[Term, ThisTree] - override def toTerm: ObjectCallTerm = ObjectCallTerm(objectRef.toTerm, meta) - override def toDoc(using options: PrettierOptions): Doc = group("ObjectCall" <+> objectRef.toDoc) @@ -1015,8 +946,6 @@ trait ObjectTypeTermC[Term <: TermT[Term]] extends TypeTermT[Term] { def objectDef: ObjectStmtTerm def cons: ObjectTypeTermF[Term, ThisTree] - override def toTerm: ObjectTypeTerm = ObjectTypeTerm(objectDef, meta) - override def toDoc(using options: PrettierOptions): Doc = Doc.text("ObjectType(") <> objectDef.name.toDoc <> Doc.text(")") diff --git a/syntax/shared/src/main/scala/chester/syntax/core/simple.scala b/syntax/shared/src/main/scala/chester/syntax/core/simple.scala index 5ed5cb44..6e32b063 100644 --- a/syntax/shared/src/main/scala/chester/syntax/core/simple.scala +++ b/syntax/shared/src/main/scala/chester/syntax/core/simple.scala @@ -3,17 +3,17 @@ package chester.syntax.core import chester.doc.* import chester.error.* import chester.error.ProblemUpickle.* -import chester.utils.{given} +import chester.utils.given import chester.utils.impls.* import upickle.default.* import scala.language.implicitConversions - import cats.data.* import chester.doc.const.* import chester.error.Problem import chester.syntax.* import chester.syntax.core.* +import chester.syntax.core.interface.* import chester.uniqid.* import chester.utils.* import chester.utils.doc.* diff --git a/tyck-base/src/main/scala/chester/tyck/convertMeta.scala b/tyck-base/src/main/scala/chester/tyck/convertMeta.scala index d6a51ed3..73ff8936 100644 --- a/tyck-base/src/main/scala/chester/tyck/convertMeta.scala +++ b/tyck-base/src/main/scala/chester/tyck/convertMeta.scala @@ -1,7 +1,7 @@ package chester.tyck import chester.syntax.concrete.ExprMeta -import chester.syntax.core.TermMeta +import chester.syntax.core.interface.TermMeta def convertMeta(meta: Option[ExprMeta]): Option[TermMeta] = for { m <- meta