From 62a4c7e61cdfd052c37c35fd837baaabee9c9594 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=BE=AA?= Date: Sun, 27 Oct 2024 15:36:13 +1300 Subject: [PATCH] save --- .../main/scala/chester/syntax/core/Term.scala | 16 +++++----------- 1 file changed, 5 insertions(+), 11 deletions(-) diff --git a/syntax/src/main/scala/chester/syntax/core/Term.scala b/syntax/src/main/scala/chester/syntax/core/Term.scala index aa7d40b5..859138ee 100644 --- a/syntax/src/main/scala/chester/syntax/core/Term.scala +++ b/syntax/src/main/scala/chester/syntax/core/Term.scala @@ -80,7 +80,7 @@ trait CallingC[Rec <: TermT[Rec]] extends WHNFT[Rec] { val argsDoc = args.map(_.toDoc).reduce(_ <+> _) if (implicitly) Docs.`(` <> argsDoc <> Docs.`)` else argsDoc } - + def cpy(args: Vector[CallingArgTermC[Rec]] = args, implicitly: Boolean = implicitly, meta: OptionTermMeta = meta): ThisTree = cons.apply(args, implicitly, meta) @@ -116,7 +116,7 @@ trait FCallTermC[Rec <: TermT[Rec]] extends WHNFT[Rec] { val argsDoc = args.map(_.toDoc).reduce(_ <+> _) group(fDoc <+> argsDoc) } - + def cpy(f: Rec = f, args: Vector[CallingC[Rec]] = args, meta: OptionTermMeta = meta): ThisTree = cons.apply(f, args, meta) @@ -139,18 +139,12 @@ case class FCallTerm( object FCallTerm {} -sealed trait Pat extends ToDoc derives ReadWriter { - override def toDoc(using options: PrettierOptions): Doc = toString - - def descent(patOp: Pat => Pat, termOp: Term => Term): Pat = this - - def thisOr(x: Pat): this.type = reuse(this, x.asInstanceOf[this.type]) +sealed trait Pat extends SpecialTerm derives ReadWriter { } case class Bind(bind: LocalV, ty: Term, meta: OptionTermMeta) extends Pat { - override def descent(patOp: Pat => Pat, termOp: Term => Term): Pat = thisOr( - copy(ty = termOp(ty)) - ) + override def toDoc(using options: PrettierOptions): Doc = bind.toDoc <+> Docs.`:` <+> ty.toDoc + override def descent(f: Term => Term, g: TreeMap[Term]): Term = thisOr(copy(bind=g(bind), ty = f(ty))) } object Bind {