diff --git a/core/src/main/scala/chester/repl/REPLEngine.scala b/core/src/main/scala/chester/repl/REPLEngine.scala index 8570307d..de121baf 100644 --- a/core/src/main/scala/chester/repl/REPLEngine.scala +++ b/core/src/main/scala/chester/repl/REPLEngine.scala @@ -146,7 +146,7 @@ def REPLEngine[F[_]](using wr: Vector[chester.error.TyckWarning] = Vector() ): F[Unit] = { given sourceReader: SourceReader = SourceReader.default - + for { _ <- er.traverse(x => { InTerminal.writeln( diff --git a/syntax/jvm/src/main/scala/chester/syntax/core/convertToTruffle.scala b/syntax/jvm/src/main/scala/chester/syntax/core/convertToTruffle.scala index 4b63411d..fbfd440d 100644 --- a/syntax/jvm/src/main/scala/chester/syntax/core/convertToTruffle.scala +++ b/syntax/jvm/src/main/scala/chester/syntax/core/convertToTruffle.scala @@ -109,8 +109,8 @@ def convertToTruffle[Term <: TermT[Term]](term: Term): truffle.Term = { case x: ObjectTypeTermC[Term] => truffle.ObjectTypeTerm(objectDef = x.objectDef, meta = x.meta) case x: ObjectStmtTermC[Term] => truffle.ObjectStmtTerm(name = x.name, uniqId = x.uniqId, extendsClause = x.extendsClause, body = x.body, meta = x.meta) - case x: RecordCallTermC[Term] => truffle.RecordCallTerm(recordDef = x.recordDef, telescope = x.telescope, meta = x.meta) + case x: RecordCallTermC[Term] => truffle.RecordCallTerm(recordDef = x.recordDef, telescope = x.telescope, meta = x.meta) case x: FieldAccessTermC[Term] => truffle.FieldAccessTerm(record = x.record, fieldName = x.fieldName, fieldType = x.fieldType, meta = x.meta) - case _ => throw new RuntimeException(s"Unhandled term type in convertToTruffle: ${term.getClass}") + case _ => throw new RuntimeException(s"Unhandled term type in convertToTruffle: ${term.getClass}") } } diff --git a/syntax/shared/src/main/scala/chester/error/Problem.scala b/syntax/shared/src/main/scala/chester/error/Problem.scala index ed37ff5c..e6c77542 100644 --- a/syntax/shared/src/main/scala/chester/error/Problem.scala +++ b/syntax/shared/src/main/scala/chester/error/Problem.scala @@ -57,7 +57,7 @@ extension (p: Problem) { def renderDoc(using options: PrettierOptions, sourceReader: SourceReader): Doc = { p.fullDescription match { case Some(desc) => renderFullDescription(desc)(using options, sourceReader) - case None => renderToDocWithSource(p)(using options, sourceReader) + case None => renderToDocWithSource(p)(using options, sourceReader) } } } @@ -67,7 +67,7 @@ private def renderFullDescription(desc: FullDescription)(using options: Prettier val explanationsDoc = desc.explanations.map { elem => val elemDoc = elem.doc.toDoc elem.sourcePos.flatMap(sourceReader.apply) match { - case Some(lines) => + case Some(lines) => val sourceLines = lines.map { case (lineNumber, line) => Doc.text(t"$lineNumber") <+> Doc.text(line, Styling.BoldOn) } @@ -89,12 +89,12 @@ private def renderFullDescription(desc: FullDescription)(using options: Prettier private def renderToDocWithSource(p: Problem)(using options: PrettierOptions, sourceReader: SourceReader): Doc = { val severityDoc = p.severity match { - case Problem.Severity.Error => Doc.text(t"Error") + case Problem.Severity.Error => Doc.text(t"Error") case Problem.Severity.Warning => Doc.text(t"Warning") - case Problem.Severity.Goal => Doc.text(t"Goal") - case Problem.Severity.Info => Doc.text(t"Info") + case Problem.Severity.Goal => Doc.text(t"Goal") + case Problem.Severity.Info => Doc.text(t"Info") } - + val baseDoc = severityDoc <+> p.toDoc p.sourcePos match { @@ -105,27 +105,30 @@ private def renderToDocWithSource(p: Problem)(using options: PrettierOptions, so Styling.BoldOn ) - val sourceLines = sourceReader(pos).map { lines => - lines.map { case (lineNumber, line) => - Doc.text(t"$lineNumber") <+> Doc.text(line, Styling.BoldOn) + val sourceLines = sourceReader(pos) + .map { lines => + lines.map { case (lineNumber, line) => + Doc.text(t"$lineNumber") <+> Doc.text(line, Styling.BoldOn) + } } - }.getOrElse(Vector.empty) + .getOrElse(Vector.empty) val codeBlock = Doc.group(Doc.concat(sourceLines.map(_.end)*)) baseDoc <|> locationHeader <|> codeBlock - case None => + case None => baseDoc } } + /** A reader for source code that provides line-numbered content. - * - * @param readSource A function that takes a SourcePos and returns line-numbered content. - * The returned Vector contains tuples of (lineNumber, lineContent) where: - * - lineNumber: 1-based line numbers (e.g., lines 3,4,5) - * - lineContent: The actual text content of that line - * Note: While internal line tracking is 0-based, this API returns 1-based line numbers for display + * + * @param readSource + * A function that takes a SourcePos and returns line-numbered content. The returned Vector contains tuples of (lineNumber, lineContent) where: + * - lineNumber: 1-based line numbers (e.g., lines 3,4,5) + * - lineContent: The actual text content of that line Note: While internal line tracking is 0-based, this API returns 1-based line numbers for + * display */ case class SourceReader(readSource: SourcePos => Option[Vector[(Int, String)]]) { def apply(pos: SourcePos): Option[Vector[(Int, String)]] = readSource(pos) diff --git a/syntax/shared/src/main/scala/chester/error/SourcePos.scala b/syntax/shared/src/main/scala/chester/error/SourcePos.scala index 386a462e..0bd6203a 100644 --- a/syntax/shared/src/main/scala/chester/error/SourcePos.scala +++ b/syntax/shared/src/main/scala/chester/error/SourcePos.scala @@ -49,13 +49,13 @@ case class SourcePos(source: SourceOffset, range: RangeInFile) derives ReadWrite val fileName = source.fileName /** Extracts all lines within the range with their line numbers. - * - * @return Option containing a Vector of (lineNumber, lineContent) tuples where: - * - lineNumber: 1-based line numbers for display (e.g., if range spans lines 3-5, - * returns exactly [(3,"line3"), (4,"line4"), (5,"line5")]) - * - lineContent: The actual text content of that line - * Note: While internal line tracking is 0-based, this API returns 1-based line numbers for display - */ + * + * @return + * Option containing a Vector of (lineNumber, lineContent) tuples where: + * - lineNumber: 1-based line numbers for display (e.g., if range spans lines 3-5, returns exactly [(3,"line3"), (4,"line4"), (5,"line5")]) + * - lineContent: The actual text content of that line Note: While internal line tracking is 0-based, this API returns 1-based line numbers for + * display + */ def getLinesInRange: Option[Vector[(Int, String)]] = fileContent map { fileContent => val startLine = range.start.line - fileContent.lineOffset val endLine = range.end.line - fileContent.lineOffset diff --git a/syntax/shared/src/main/scala/chester/syntax/core/convertToSimple.scala b/syntax/shared/src/main/scala/chester/syntax/core/convertToSimple.scala index 683377fe..e3d37547 100644 --- a/syntax/shared/src/main/scala/chester/syntax/core/convertToSimple.scala +++ b/syntax/shared/src/main/scala/chester/syntax/core/convertToSimple.scala @@ -109,8 +109,8 @@ def convertToSimple[Term <: TermT[Term]](term: Term): simple.Term = { case x: ObjectTypeTermC[Term] => simple.ObjectTypeTerm(objectDef = x.objectDef, meta = x.meta) case x: ObjectStmtTermC[Term] => simple.ObjectStmtTerm(name = x.name, uniqId = x.uniqId, extendsClause = x.extendsClause, body = x.body, meta = x.meta) - case x: RecordCallTermC[Term] => simple.RecordCallTerm(recordDef = x.recordDef, telescope = x.telescope, meta = x.meta) + case x: RecordCallTermC[Term] => simple.RecordCallTerm(recordDef = x.recordDef, telescope = x.telescope, meta = x.meta) case x: FieldAccessTermC[Term] => simple.FieldAccessTerm(record = x.record, fieldName = x.fieldName, fieldType = x.fieldType, meta = x.meta) - case _ => throw new RuntimeException(s"Unhandled term type in convertToSimple: ${term.getClass}") + case _ => throw new RuntimeException(s"Unhandled term type in convertToSimple: ${term.getClass}") } } diff --git a/tyck/src/main/scala/chester/tyck/ElaboraterCommon.scala b/tyck/src/main/scala/chester/tyck/ElaboraterCommon.scala index 73fe1955..d8424e1b 100644 --- a/tyck/src/main/scala/chester/tyck/ElaboraterCommon.scala +++ b/tyck/src/main/scala/chester/tyck/ElaboraterCommon.scala @@ -494,10 +494,11 @@ trait ElaboraterCommon extends ProvideCtx with ElaboraterBase with CommonPropaga case class RecordFieldPropagator( recordTy: CellId[Term], - fieldName: Name, + fieldName: Name, expectedTy: CellId[Term], cause: Expr - )(using localCtx: Context) extends Propagator[Tyck] { + )(using localCtx: Context) + extends Propagator[Tyck] { override val readingCells: Set[CIdOf[Cell[?]]] = Set(recordTy) override val writingCells: Set[CIdOf[Cell[?]]] = Set(expectedTy) override val zonkingCells: Set[CIdOf[Cell[?]]] = Set(recordTy, expectedTy) @@ -528,7 +529,7 @@ trait ElaboraterCommon extends ProvideCtx with ElaboraterBase with CommonPropaga override def naiveZonk(needed: Vector[CellIdAny])(using state: StateAbility[Tyck], more: Tyck): ZonkResult = { state.readStable(recordTy) match { case None => ZonkResult.Require(Vector(recordTy)) - case _ => ZonkResult.Done + case _ => ZonkResult.Done } } }