From 014243d088406355acbdd7a577160fb782410cd9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E6=BE=AA?= Date: Sun, 27 Oct 2024 16:05:16 +1300 Subject: [PATCH] fmt --- project/plugins.sbt | 2 +- .../src/main/scala/chester/syntax/Tree.scala | 8 +- .../main/scala/chester/syntax/core/Term.scala | 86 +++++++++++-------- .../src/main/scala/chester/tyck/Context.scala | 44 +++++----- .../chester/tyck/api/SemanticCollector.scala | 40 ++++----- .../main/scala/chester/tyck/Elaborater.scala | 2 +- 6 files changed, 96 insertions(+), 86 deletions(-) diff --git a/project/plugins.sbt b/project/plugins.sbt index d17e10ae..75f93df8 100644 --- a/project/plugins.sbt +++ b/project/plugins.sbt @@ -27,4 +27,4 @@ addDependencyTreePlugin addSbtPlugin("com.timushev.sbt" % "sbt-updates" % "0.6.3") addSbtPlugin("org.scalameta" % "sbt-scalafmt" % "2.5.2") addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.13.0+9-d2c99b38-SNAPSHOT") -addSbtPlugin("com.github.sbt" % "sbt-license-report" % "1.6.1") \ No newline at end of file +addSbtPlugin("com.github.sbt" % "sbt-license-report" % "1.6.1") diff --git a/syntax/src/main/scala/chester/syntax/Tree.scala b/syntax/src/main/scala/chester/syntax/Tree.scala index 20e11048..b8d6f4ba 100644 --- a/syntax/src/main/scala/chester/syntax/Tree.scala +++ b/syntax/src/main/scala/chester/syntax/Tree.scala @@ -58,7 +58,7 @@ trait TreeMap[Tre <: Tree[Tre]] { final def apply[T <: Tre](x: T): T = use(x).asInstanceOf[T] } -implicit def convertSpecialMap2[A <: Tree[A], T <: A]( f: TreeMap[A]): Tree[A] => T = x => f.use(x.asInstanceOf[T]).asInstanceOf[T] -implicit def conversion1[A <: Tree[A], T <: Tree[A], U <:T](x:Vector[T]): Vector[U] = x.asInstanceOf[Vector[U]] -implicit def conversion11[A <: Tree[A], T <: Tree[A], U <:T](x:T): U = x.asInstanceOf[U] -//implicit def conversion2[A <: Tree[A], T <: Tree[A]](x:T): A&T = x.asInstanceOf[A&T] \ No newline at end of file +implicit def convertSpecialMap2[A <: Tree[A], T <: A](f: TreeMap[A]): Tree[A] => T = x => f.use(x.asInstanceOf[T]).asInstanceOf[T] +implicit def conversion1[A <: Tree[A], T <: Tree[A], U <: T](x: Vector[T]): Vector[U] = x.asInstanceOf[Vector[U]] +implicit def conversion11[A <: Tree[A], T <: Tree[A], U <: T](x: T): U = x.asInstanceOf[U] +//implicit def conversion2[A <: Tree[A], T <: Tree[A]](x:T): A&T = x.asInstanceOf[A&T] diff --git a/syntax/src/main/scala/chester/syntax/core/Term.scala b/syntax/src/main/scala/chester/syntax/core/Term.scala index fd23136b..52a90e8c 100644 --- a/syntax/src/main/scala/chester/syntax/core/Term.scala +++ b/syntax/src/main/scala/chester/syntax/core/Term.scala @@ -36,7 +36,7 @@ trait CallingArgTermC[Rec <: TermT[Rec]] extends WHNFT[Rec] { def vararg: Boolean override def toTerm: CallingArgTerm = CallingArgTerm(value.toTerm, ty.toTerm, name, vararg, meta) def cons: CallingArgTermF[Rec, ThisTree] - + override def toDoc(using options: PrettierOptions): Doc = { val varargDoc = if (vararg) Docs.`...` else Doc.empty val nameDoc = name.map(_.toDoc <+> Docs.`:`).getOrElse(Doc.empty) @@ -57,7 +57,8 @@ case class CallingArgTerm( name: Option[Name] = None, vararg: Boolean = false, meta: OptionTermMeta -) extends WHNF with CallingArgTermC[Term] derives ReadWriter { +) extends WHNF + with CallingArgTermC[Term] derives ReadWriter { override def cons = this.copy override type ThisTree = CallingArgTerm override def descent(f: Term => Term, g: TreeMap[Term]): CallingArgTerm = @@ -74,8 +75,8 @@ trait CallingC[Rec <: TermT[Rec]] extends WHNFT[Rec] { def args: Vector[CallingArgTermC[Rec]] def implicitly: Boolean override def toTerm: Calling = Calling(args.map(_.toTerm), implicitly, meta) - def cons: CallingF[Rec, ThisTree] - + def cons: CallingF[Rec, ThisTree] + override def toDoc(using options: PrettierOptions): Doc = { val argsDoc = args.map(_.toDoc).reduce(_ <+> _) if (implicitly) Docs.`(` <> argsDoc <> Docs.`)` else argsDoc @@ -93,7 +94,8 @@ case class Calling( args: Vector[CallingArgTerm], implicitly: Boolean = false, meta: OptionTermMeta -) extends WHNF with CallingC[Term] derives ReadWriter { +) extends WHNF + with CallingC[Term] derives ReadWriter { override type ThisTree = Calling override def cons = this.copy override def descent(f: Term => Term, g: TreeMap[Term]): Calling = copy(args = args.map(g)) @@ -110,7 +112,7 @@ trait FCallTermC[Rec <: TermT[Rec]] extends WHNFT[Rec] { def args: Vector[CallingC[Rec]] override def toTerm: FCallTerm = FCallTerm(f.toTerm, args.map(_.toTerm), meta) def cons: FCallTermF[Rec, ThisTree] - + override def toDoc(using options: PrettierOptions): Doc = { val fDoc = f.toDoc val argsDoc = args.map(_.toDoc).reduce(_ <+> _) @@ -129,7 +131,8 @@ case class FCallTerm( f: Term, args: Vector[Calling], meta: OptionTermMeta -) extends WHNF with FCallTermC[Term] { +) extends WHNF + with FCallTermC[Term] { override type ThisTree = FCallTerm override def cons = this.copy override def descent(a: Term => Term, g: TreeMap[Term]): FCallTerm = thisOr( @@ -172,7 +175,8 @@ case class Bind( bind: LocalV, ty: Term, meta: OptionTermMeta -) extends Pat with BindC[Term] { +) extends Pat + with BindC[Term] { override type ThisTree = Bind override def cons = this.copy @@ -463,7 +467,7 @@ case class Prop(level: Term, meta: OptionTermMeta) extends Sort with PropC[Term] trait FTypeC[Rec <: TermT[Rec]] extends SortT[Rec] { override type ThisTree <: FTypeC[Rec] def level: Rec - def copy(level: Rec = level, meta: OptionTermMeta = meta): ThisTree + def copy(level: Rec = level, meta: OptionTermMeta = meta): ThisTree override def toTerm: FType = FType(level.toTerm, meta) override def descent(f: Rec => Rec, g: TreeMap[Rec]): Rec = thisOr(copy(level = f(level))) @@ -829,7 +833,8 @@ case class ArgTerm( default: Option[Term] = None, vararg: Boolean = false, meta: OptionTermMeta -) extends WHNF with ArgTermC[Term] { +) extends WHNF + with ArgTermC[Term] { override type ThisTree = ArgTerm override def cons = this.copy @@ -847,9 +852,9 @@ object ArgTerm { @FunctionalInterface trait TelescopeTermF[Rec <: TermT[Rec], ThisTree <: TelescopeTermC[Rec]] { def apply( - args: Vector[ArgTermC[Rec]], - implicitly: Boolean, - meta: OptionTermMeta + args: Vector[ArgTermC[Rec]], + implicitly: Boolean, + meta: OptionTermMeta ): ThisTree } @@ -860,7 +865,7 @@ trait TelescopeTermC[Rec <: TermT[Rec]] extends WHNFT[Rec] { def cons: TelescopeTermF[Rec, 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) @@ -872,9 +877,9 @@ trait TelescopeTermC[Rec <: TermT[Rec]] extends WHNFT[Rec] { } def cpy( - args: Vector[ArgTermC[Rec]] = args, - implicitly: Boolean = implicitly, - meta: OptionTermMeta = meta + args: Vector[ArgTermC[Rec]] = args, + implicitly: Boolean = implicitly, + meta: OptionTermMeta = meta ): ThisTree = cons.apply(args, implicitly, meta) override def descent(f: Rec => Rec, g: TreeMap[Rec]): Rec = thisOr( @@ -891,7 +896,8 @@ case class TelescopeTerm( args: Vector[ArgTerm], implicitly: Boolean = false, meta: OptionTermMeta -) extends WHNF with TelescopeTermC[Term] { +) extends WHNF + with TelescopeTermC[Term] { override type ThisTree = TelescopeTerm override def cons = this.copy @@ -935,7 +941,8 @@ case class Function( ty: FunctionType, body: Term, meta: OptionTermMeta -) extends WHNF with FunctionC[Term] { +) extends WHNF + with FunctionC[Term] { override type ThisTree = Function override def cons = this.copy @@ -961,10 +968,10 @@ case class Matching( @FunctionalInterface trait FunctionTypeF[Rec <: TermT[Rec], ThisTree <: FunctionTypeC[Rec]] { def apply( - telescope: Vector[TelescopeTermC[Rec]], - resultTy: Rec, - effects: EffectsM, - meta: OptionTermMeta + telescope: Vector[TelescopeTermC[Rec]], + resultTy: Rec, + effects: EffectsM, + meta: OptionTermMeta ): ThisTree } @@ -995,10 +1002,10 @@ trait FunctionTypeC[Rec <: TermT[Rec]] extends WHNFT[Rec] { } def cpy( - telescope: Vector[TelescopeTermC[Rec]] = telescope, - resultTy: Rec = resultTy, - effects: EffectsM = effects, - meta: OptionTermMeta = meta + telescope: Vector[TelescopeTermC[Rec]] = telescope, + resultTy: Rec = resultTy, + effects: EffectsM = effects, + meta: OptionTermMeta = meta ): ThisTree = cons.apply(telescope, resultTy, effects, meta) override def descent(f: Rec => Rec, g: TreeMap[Rec]): Rec = thisOr( @@ -1011,11 +1018,12 @@ trait FunctionTypeC[Rec <: TermT[Rec]] extends WHNFT[Rec] { } case class FunctionType( - telescope: Vector[TelescopeTerm], - resultTy: Term, - effects: EffectsM = NoEffect, - meta: OptionTermMeta -) extends WHNF with FunctionTypeC[Term] { + telescope: Vector[TelescopeTerm], + resultTy: Term, + effects: EffectsM = NoEffect, + meta: OptionTermMeta +) extends WHNF + with FunctionTypeC[Term] { override type ThisTree = FunctionType override def cons = this.copy @@ -1180,7 +1188,7 @@ sealed trait Effect extends WHNF derives ReadWriter { case class Effects(effects: Map[LocalV, Term] = HashMap.empty, meta: OptionTermMeta) extends WHNF with EffectsM derives ReadWriter { override type ThisTree = Effects override def descent(f: Term => Term, g: TreeMap[Term]): Effects = thisOr( - copy(effects = effects.map { case (k, v) => (g(k) , f(v)) }) + copy(effects = effects.map { case (k, v) => (g(k), f(v)) }) ) override def toDoc(using options: PrettierOptions): Doc = @@ -1196,7 +1204,7 @@ case class Effects(effects: Map[LocalV, Term] = HashMap.empty, meta: OptionTermM effects.flatMap((a, b) => a.collectMeta ++ b.collectMeta).toVector override def replaceMeta(f: MetaTerm => Term): Effects = copy(effects = effects.map { case (a, b) => - (a.replaceMeta(f).asInstanceOf[LocalV] , b.replaceMeta(f)) + (a.replaceMeta(f).asInstanceOf[LocalV], b.replaceMeta(f)) }) } @@ -1262,14 +1270,15 @@ trait LocalVC[Rec <: TermT[Rec]] extends ReferenceCallC[Rec] { override def descent(f: Rec => Rec, g: TreeMap[Rec]): Rec = thisOr(cpy(ty = f(ty))) } -implicit def LocalVConversion[Rec <: TermT[Rec]] (x: UniqidOf[LocalVC[Rec]]): UniqidOf[LocalV] = x.asInstanceOf[UniqidOf[LocalV]] +implicit def LocalVConversion[Rec <: TermT[Rec]](x: UniqidOf[LocalVC[Rec]]): UniqidOf[LocalV] = x.asInstanceOf[UniqidOf[LocalV]] case class LocalV( name: Name, ty: Term, uniqId: UniqidOf[LocalV], meta: OptionTermMeta -) extends ReferenceCall with LocalVC[Term] { +) extends ReferenceCall + with LocalVC[Term] { override type ThisTree = LocalV override def cons = this.copy @@ -1306,14 +1315,15 @@ trait ToplevelVC[Rec <: TermT[Rec]] extends ReferenceCallC[Rec] { def name = id.name } -implicit def conversionTop[Rec <: TermT[Rec]] (x: UniqidOf[ToplevelVC[Rec]]): UniqidOf[ToplevelV] = x.asInstanceOf[UniqidOf[ToplevelV]] +implicit def conversionTop[Rec <: TermT[Rec]](x: UniqidOf[ToplevelVC[Rec]]): UniqidOf[ToplevelV] = x.asInstanceOf[UniqidOf[ToplevelV]] case class ToplevelV( id: AbsoluteRef, ty: Term, uniqId: UniqidOf[ToplevelV], meta: OptionTermMeta -) extends ReferenceCall with ToplevelVC[Term] { +) extends ReferenceCall + with ToplevelVC[Term] { override type ThisTree = ToplevelV override def cons = this.copy diff --git a/tyck-base/src/main/scala/chester/tyck/Context.scala b/tyck-base/src/main/scala/chester/tyck/Context.scala index 119e1467..fe7db911 100644 --- a/tyck-base/src/main/scala/chester/tyck/Context.scala +++ b/tyck-base/src/main/scala/chester/tyck/Context.scala @@ -7,20 +7,20 @@ import chester.tyck.api.SymbolCollector import chester.uniqid.UniqidOf case class TyAndVal( - ty: Term, - value: Term - ) {} + ty: Term, + value: Term +) {} object TyAndVal {} /** for pure values only like let and def. record is not included */ case class ContextItem( - name: Name, - uniqId: UniqidOf[ReferenceCall], - ref: ReferenceCall, - ty: Term, - reference: Option[SymbolCollector] = None - ) + name: Name, + uniqId: UniqidOf[ReferenceCall], + ref: ReferenceCall, + ty: Term, + reference: Option[SymbolCollector] = None +) object ContextItem {} case class Imports() @@ -29,17 +29,17 @@ object Imports { } case class Context( - map: Map[Name, UniqidOf[ReferenceCall]] = Map.empty[Name, UniqidOf[ReferenceCall]], // empty[...] are needed because compiler bugs - contextItems: Map[UniqidOf[ReferenceCall], ContextItem] = - Map.empty[UniqidOf[ReferenceCall], ContextItem], // empty[...] are needed because compiler bugs - knownMap: Map[UniqidOf[ReferenceCall], TyAndVal] = Map.empty[UniqidOf[ReferenceCall], TyAndVal], // empty[...] are needed because compiler bugs - typeDefinitionNames: Map[Name, UniqidOf[TypeDefinition]] = Map.empty, - typeDefinitions: Map[UniqidOf[TypeDefinition], TypeDefinition] = Map.empty, - imports: Imports = Imports.Empty, - loadedModules: LoadedModules = LoadedModules.Empty, - operators: OperatorsContext = OperatorsContext.Default, - currentModule: ModuleRef = DefaultModule - ) { + map: Map[Name, UniqidOf[ReferenceCall]] = Map.empty[Name, UniqidOf[ReferenceCall]], // empty[...] are needed because compiler bugs + contextItems: Map[UniqidOf[ReferenceCall], ContextItem] = + Map.empty[UniqidOf[ReferenceCall], ContextItem], // empty[...] are needed because compiler bugs + knownMap: Map[UniqidOf[ReferenceCall], TyAndVal] = Map.empty[UniqidOf[ReferenceCall], TyAndVal], // empty[...] are needed because compiler bugs + typeDefinitionNames: Map[Name, UniqidOf[TypeDefinition]] = Map.empty, + typeDefinitions: Map[UniqidOf[TypeDefinition], TypeDefinition] = Map.empty, + imports: Imports = Imports.Empty, + loadedModules: LoadedModules = LoadedModules.Empty, + operators: OperatorsContext = OperatorsContext.Default, + currentModule: ModuleRef = DefaultModule +) { def updateModule(module: ModuleRef): Context = copy(currentModule = module) def getKnown(x: ReferenceCall): Option[TyAndVal] = @@ -52,8 +52,8 @@ case class Context( knownAdd(Seq(id -> y)) def knownAdd( - seq: Seq[(UniqidOf[ReferenceCall], TyAndVal)] - ): Context = { + seq: Seq[(UniqidOf[ReferenceCall], TyAndVal)] + ): Context = { val newKnownMap = seq.foldLeft(knownMap) { (acc, item) => assert(!acc.contains(item._1), s"Duplicate key ${item._1}") acc + item diff --git a/tyck-base/src/main/scala/chester/tyck/api/SemanticCollector.scala b/tyck-base/src/main/scala/chester/tyck/api/SemanticCollector.scala index 31dded5c..2eed9f50 100644 --- a/tyck-base/src/main/scala/chester/tyck/api/SemanticCollector.scala +++ b/tyck-base/src/main/scala/chester/tyck/api/SemanticCollector.scala @@ -21,11 +21,11 @@ trait SemanticCollector { def highlightLiteral(expr: Expr): Unit = () def newSymbol( - call: ReferenceCall, - id: UniqidOf[ReferenceCall], - definedOn: Expr, - localCtx: Context - ): SymbolCollector = NoopSymbolCollector + call: ReferenceCall, + id: UniqidOf[ReferenceCall], + definedOn: Expr, + localCtx: Context + ): SymbolCollector = NoopSymbolCollector def metaFinished(replace: MetaTerm => Term): Unit = () } @@ -35,11 +35,11 @@ private implicit inline def rwUniqIDOfVar[T]: ReadWriter[UniqidOf[ReferenceCall] // TODO: handle when call's ty is MetaTerm case class CollectedSymbol( - call: ReferenceCall, - id: UniqidOf[ReferenceCall], - definedOn: Expr, - referencedOn: Vector[Expr] - ) derives ReadWriter { + call: ReferenceCall, + id: UniqidOf[ReferenceCall], + definedOn: Expr, + referencedOn: Vector[Expr] +) derives ReadWriter { def name: Name = call.name def metaFinished(replace: MetaTerm => Term): CollectedSymbol = { @@ -51,11 +51,11 @@ class VectorSemanticCollector extends SemanticCollector { private var builder: mutable.ArrayDeque[CollectedSymbol] = new mutable.ArrayDeque[CollectedSymbol]() override def newSymbol( - call: ReferenceCall, - id: UniqidOf[ReferenceCall], - definedOn: Expr, - localCtx: Context - ): SymbolCollector = { + call: ReferenceCall, + id: UniqidOf[ReferenceCall], + definedOn: Expr, + localCtx: Context + ): SymbolCollector = { val index = builder.length builder.append(CollectedSymbol(call, id, definedOn, Vector())) assert(builder.length == index + 1) @@ -78,11 +78,11 @@ object NoopSemanticCollector extends SemanticCollector {} class UnusedVariableWarningWrapper(x: SemanticCollector) extends SemanticCollector { private var unusedVariables: Vector[CollectedSymbol] = Vector() override def newSymbol( - call: ReferenceCall, - id: UniqidOf[ReferenceCall], - definedOn: Expr, - localCtx: Context - ): SymbolCollector = { + call: ReferenceCall, + id: UniqidOf[ReferenceCall], + definedOn: Expr, + localCtx: Context + ): SymbolCollector = { val symbolCollector = x.newSymbol(call, id, definedOn, localCtx) val c = CollectedSymbol(call, id, definedOn, Vector()) unusedVariables = unusedVariables :+ c diff --git a/tyck/src/main/scala/chester/tyck/Elaborater.scala b/tyck/src/main/scala/chester/tyck/Elaborater.scala index a0052c00..ce19213e 100644 --- a/tyck/src/main/scala/chester/tyck/Elaborater.scala +++ b/tyck/src/main/scala/chester/tyck/Elaborater.scala @@ -195,7 +195,7 @@ trait ProvideElaborater extends ProvideCtx with Elaborater with ElaboraterFuncti val elaboratedKey = elab(keyExpr, newType, effects) val fieldType = newType val elaboratedValue = elab(valueExpr, fieldType, effects) - val _ = fieldTypeVars.put(elaboratedKey , fieldType) + val _ = fieldTypeVars.put(elaboratedKey, fieldType) Some(ObjectClauseValueTerm(elaboratedKey, elaboratedValue, convertMeta(expr.meta))) // Handle other possible clauses case _ => ???