<commit_before>/* Copyright 2009-2016 EPFL, Lausanne */

package stainless
package termination

import inox.utils.ASCIIHelpers.{ Cell, Row }
import stainless.utils.JsonConvertions._

import io.circe._
import io.circe.syntax._
import io.circe.generic.semiauto._

import scala.util.{ Right, Left }

object TerminationReport {

  sealed abstract class Status {
    def isUnknown = this == Unknown
    def isTerminating = this == Terminating
    def isNonTerminating = this == NonTerminating
  }

  case object Unknown extends Status
  case object Terminating extends Status
  case object NonTerminating extends Status

  implicit val statusDecoder: Decoder[Status] = deriveDecoder
  implicit val statusEncoder: Encoder[Status] = deriveEncoder

  case class Record(
    id: Identifier, pos: inox.utils.Position, time: Long,
    status: Status, verdict: String, kind: String,
    generation: Long = 0 // "age" of the record, usefull to determine which ones are "NEW".
  ) extends AbstractReportHelper.Record

  implicit val recordDecoder: Decoder[Record] = deriveDecoder
  implicit val recordEncoder: Encoder[Record] = deriveEncoder

  def parse(json: Json): TerminationReport = json.as[(Seq[Record], Long)] match {
    case Right((records, lastGen)) => new TerminationReport(records, lastGen + 1)
    case Left(error) => throw error
  }

}

// Variant of the report without the checker, where all the data is mapped to text
class TerminationReport(val results: Seq[TerminationReport.Record], lastGen: Long = 0)
  extends AbstractReport[TerminationReport] {
  import TerminationReport._

  override val name: String = TerminationComponent.name

  override def ~(other: TerminationReport) = {
    def updater(nextGen: Long)(r: Record) = r.copy(generation = nextGen)
    val (fused, nextGen) = AbstractReportHelper.merge(this.results, other.results, lastGen, updater)
    new TerminationReport(fused, nextGen)
  }

  override def filter(ids: Set[Identifier]) = {
    val (filtered, nextGen) = AbstractReportHelper.filter(results, ids, lastGen)
    new TerminationReport(filtered, nextGen)
  }

  override def emitRowsAndStats: Option[(Seq[Row], ReportStats)] = if (results.isEmpty) None else {
    val rows = for { Record(id, pos, time, status, verdict, kind, gen) <- results } yield Row(Seq(
      Cell(if (gen == lastGen) "NEW" else ""),
      Cell(id.name),
      Cell((if (status.isTerminating) "\u2713" else "\u2717") + " " + verdict),
      Cell(f"${time / 1000d}%3.3f")
    ))

    val valid = results count { _.status.isTerminating }
    val validFromCache = 0
    val invalid = results count { _.status.isNonTerminating }
    val unknown = results count { _.status.isUnknown }
    val time = (results map { _.time }).sum

    val stats = ReportStats(results.size, time, valid, validFromCache, invalid, unknown)

    Some((rows, stats))
  }

  override def emitJson: Json = results.asJson

}
<commit_msg>Fix TerminationReport.emitJson<commit_after>/* Copyright 2009-2016 EPFL, Lausanne */

package stainless
package termination

import inox.utils.ASCIIHelpers.{ Cell, Row }
import stainless.utils.JsonConvertions._

import io.circe._
import io.circe.syntax._
import io.circe.generic.semiauto._

import scala.util.{ Right, Left }

object TerminationReport {

  sealed abstract class Status {
    def isUnknown = this == Unknown
    def isTerminating = this == Terminating
    def isNonTerminating = this == NonTerminating
  }

  case object Unknown extends Status
  case object Terminating extends Status
  case object NonTerminating extends Status

  implicit val statusDecoder: Decoder[Status] = deriveDecoder
  implicit val statusEncoder: Encoder[Status] = deriveEncoder

  case class Record(
    id: Identifier, pos: inox.utils.Position, time: Long,
    status: Status, verdict: String, kind: String,
    generation: Long = 0 // "age" of the record, usefull to determine which ones are "NEW".
  ) extends AbstractReportHelper.Record

  implicit val recordDecoder: Decoder[Record] = deriveDecoder
  implicit val recordEncoder: Encoder[Record] = deriveEncoder

  def parse(json: Json): TerminationReport = json.as[(Seq[Record], Long)] match {
    case Right((records, lastGen)) => new TerminationReport(records, lastGen + 1)
    case Left(error) => throw error
  }

}

// Variant of the report without the checker, where all the data is mapped to text
class TerminationReport(val results: Seq[TerminationReport.Record], lastGen: Long = 0)
  extends AbstractReport[TerminationReport] {
  import TerminationReport._

  override val name: String = TerminationComponent.name

  override def ~(other: TerminationReport) = {
    def updater(nextGen: Long)(r: Record) = r.copy(generation = nextGen)
    val (fused, nextGen) = AbstractReportHelper.merge(this.results, other.results, lastGen, updater)
    new TerminationReport(fused, nextGen)
  }

  override def filter(ids: Set[Identifier]) = {
    val (filtered, nextGen) = AbstractReportHelper.filter(results, ids, lastGen)
    new TerminationReport(filtered, nextGen)
  }

  override def emitRowsAndStats: Option[(Seq[Row], ReportStats)] = if (results.isEmpty) None else {
    val rows = for { Record(id, pos, time, status, verdict, kind, gen) <- results } yield Row(Seq(
      Cell(if (gen == lastGen) "NEW" else ""),
      Cell(id.name),
      Cell((if (status.isTerminating) "\u2713" else "\u2717") + " " + verdict),
      Cell(f"${time / 1000d}%3.3f")
    ))

    val valid = results count { _.status.isTerminating }
    val validFromCache = 0
    val invalid = results count { _.status.isNonTerminating }
    val unknown = results count { _.status.isUnknown }
    val time = (results map { _.time }).sum

    val stats = ReportStats(results.size, time, valid, validFromCache, invalid, unknown)

    Some((rows, stats))
  }

  override def emitJson: Json = (results, lastGen).asJson

}

{'fraction_non_alphanumeric': 0.10517300445358, 'fraction_numerical': 0.008907159986296678, 'mean_word_length': 4.0951134380453755, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '257584', 'n_tokens_mistral': 1775, 'n_tokens_neox': 1696, 'n_words': 534}