<commit_before>package provingground.learning
import provingground._, HoTT._

import spire.algebra._
import spire.implicits._

import provingground.{FiniteDistribution => FD, ProbabilityDistribution => PD}

import monix.eval._
import math.{log, exp}

import scala.concurrent._, duration._

import translation.FansiShow._

/**
  * A collection of functions to build provers;
  * some are abstract methods for exploring, searching etc., while others generate terms and types, sometimes as derivatives.
  * Some methods combine the two to give a ready to use function.
  * These are based on [[TermEvolver]] and `Monix`.
  */
object ProverTasks {

  /**
    * evolution of types, as a  (task with value) finite distribution;
    * obtained by lazy recursive definition in [[TermEvolver]] and trunctation.
    */
  def typdistTask(fd: FD[Term],
                  tv: TermEvolver,
                  cutoff: Double,
                  maxtime: FiniteDuration,
                  vars: Vector[Term] = Vector()) =
    Truncate
      .task(tv.baseEvolveTyps(fd).map(piClosure(vars)), cutoff, maxtime)
      .memoize

  /**
    * evolution of terms, as a  (task with value) finite distribution;
    * obtained by lazy recursive definition in [[TermEvolver]] and trunctation.
    */
  def termdistTask(fd: FD[Term],
                   tv: TermEvolver,
                   cutoff: Double,
                   maxtime: FiniteDuration,
                   vars: Vector[Term] = Vector()) =
    Truncate
      .task(tv.baseEvolve(fd).map(lambdaClosure(vars)), cutoff, maxtime)
      .memoize

  /**
    * evolution of terms by the ''derivative'', as a  (task with value) finite distribution;
    * obtained by lazy recursive definition in [[TermEvolver]] and trunctation.
    */
  def termdistDerTask(fd: FD[Term],
                      tfd: FD[Term],
                      tv: TermEvolver,
                      cutoff: Double,
                      maxtime: FiniteDuration,
                      vars: Vector[Term] = Vector()) =
    Truncate
      .task(tv.evolve(TangVec(fd, tfd)).vec.map(lambdaClosure(vars)),
            cutoff,
            maxtime)
      .memoize

  /**
    * An entropy measure for parsimonious generation of terms inhabiting types.
    */
  def h0(p: Double, q: Double) = {
    require(q > 0, s"Entropy with p=$p, q = $q")
    -p / (q * log(q))
  }

  /**
    * Exponent of an entropy measure for parsimonious generation of terms inhabiting types;
    * low values correspond to important terms, with the `scale` increasing sensitivity.
    */
  def hExp(p: Double, q: Double, scale: Double) =
    math.exp(-(h0(p, q) - 1) * scale)

  def prsmEntTask(termsTask: Task[FD[Term]],
                  typsTask: Task[FD[Typ[Term]]],
                  scale: Double,
                  vars: Vector[Term] = Vector()) =
    for {
      terms <- termsTask
      typs  <- typsTask
      thmsByPf  = terms.map(_.typ)
      thmsBySt  = typs.filter(thmsByPf(_) > 0)
      pfSet     = terms.flatten.supp.filter((t) => thmsBySt(t.typ) > 0)
      fullPfSet = pfSet.flatMap(partialLambdaClosures(vars))
    } yield
      fullPfSet
        .map { (pf) =>
          (pf,
           hExp(thmsBySt(pf.typ),
                thmsByPf(pf.typ),
                scale * terms(pf) / thmsByPf(pf.typ)))
        }
        .sortBy(_._2)

  def dervecTasks(base: FD[Term],
                  tv: TermEvolver,
                  termsTask: Task[FD[Term]],
                  typsTask: Task[FD[Typ[Term]]],
                  maxtime: FiniteDuration,
                  cutoff: Double,
                  scale: Double,
                  vars: Vector[Term] = Vector()): Task[Vector[Task[FD[Term]]]] =
    prsmEntTask(termsTask, typsTask, scale, vars = vars).map { (vec) =>
      {
        val scales = vec.collect {
          case (v, p) if p > cutoff && cutoff / p > 0 =>
            (v, cutoff / p)
        }
        val tot = scales.map{case (_, x) => -log(x)}.sum
        pprint.log(s"want: ${-log(cutoff)}, actual total: $tot from ${scales.size}")
        scales.map {
          case (v, sc) =>
            termdistDerTask(base, FD.unif(v), tv, sc, maxtime, vars)
        }
      }
    }

  def dervecTraceTasks(base: FD[Term],
                       tv: TermEvolver,
                       termsTask: Task[FD[Term]],
                       typsTask: Task[FD[Typ[Term]]],
                       maxtime: FiniteDuration,
                       cutoff: Double,
                       scale: Double,
                       trace: Vector[Term],
                       vars: Vector[Term] = Vector())
    : Task[Vector[Task[(FD[Term], Vector[Term])]]] =
    prsmEntTask(termsTask, typsTask, scale, vars = vars).map { (vec) =>
      {
        val scales = vec.collect {
          case (v, p) if p > cutoff && cutoff / p > 0 =>
            (v, cutoff / p)
        }
        val tot = scales.map{case (_, x) => -log(x)}.sum
        pprint.log(s"want: ${-log(cutoff)}, actual total: $tot from ${scales.size}")
        scales.map {
          case (v, sc) =>
            for {
              fd <- termdistDerTask(base, FD.unif(v), tv, sc, maxtime, vars)
            } yield (fd, trace :+ v)
        }
      }
    }

  def dervecWeightedTraceTasks(base: FD[Term],
                               tv: TermEvolver,
                               termsTask: Task[FD[Term]],
                               typsTask: Task[FD[Typ[Term]]],
                               maxtime: FiniteDuration,
                               cutoff: Double,
                               scale: Double,
                               trace: Vector[(Term, Double)],
                               vars: Vector[Term] = Vector())
    : Task[Vector[Task[(FD[Term], Vector[(Term, Double)])]]] =
    prsmEntTask(termsTask, typsTask, scale, vars = vars).map { (vec) =>
      {
        val scales = vec.collect {
          case (v, p) if p > cutoff && cutoff / p > 0 =>
            (v, p, cutoff / p)
        }
        val tot = scales.map{case (_, _, x) => -log(x)}.sum
        pprint.log(s"want: ${-log(cutoff)}, actual total: $tot from ${scales.size}")
        scales.map {
          case (v, p, sc) =>
            for {
              fd <- termdistDerTask(base, FD.unif(v), tv, sc, maxtime, vars)
            } yield (fd, trace :+ (v -> p))
        }
      }
    }

  def inTaskVec[X, Y](tv: Task[Vector[X]], p: X => Option[Y]): Task[Option[Y]] =
    tv.flatMap {
      case Vector() => Task.pure(None)
      case x +: ys =>
        Task.eval(p(x)).flatMap {
          case Some(z) => Task.pure(Some(z))
          case None    => inTaskVec(Task.eval(ys), p)
        }
    }

  def inTaskVecTask[X, Y](tv: Task[Vector[Task[X]]],
                          p: X => Option[Y]): Task[Option[Y]] =
    tv.flatMap {
      case Vector() => Task.pure(None)
      case x +: ys =>
        x.map(p).flatMap {
          case Some(z) => Task.pure(Some(z))
          case None    => inTaskVecTask(Task.eval(ys), p)<commit_msg>cutoff reciprocal scaling; nothing broken<commit_after>package provingground.learning
import provingground._, HoTT._

import spire.algebra._
import spire.implicits._

import provingground.{FiniteDistribution => FD, ProbabilityDistribution => PD}

import monix.eval._
import math._

import scala.concurrent._, duration._

import translation.FansiShow._

/**
  * A collection of functions to build provers;
  * some are abstract methods for exploring, searching etc., while others generate terms and types, sometimes as derivatives.
  * Some methods combine the two to give a ready to use function.
  * These are based on [[TermEvolver]] and `Monix`.
  */
object ProverTasks {

  /**
    * evolution of types, as a  (task with value) finite distribution;
    * obtained by lazy recursive definition in [[TermEvolver]] and trunctation.
    */
  def typdistTask(fd: FD[Term],
                  tv: TermEvolver,
                  cutoff: Double,
                  maxtime: FiniteDuration,
                  vars: Vector[Term] = Vector()) =
    Truncate
      .task(tv.baseEvolveTyps(fd).map(piClosure(vars)), cutoff, maxtime)
      .memoize

  /**
    * evolution of terms, as a  (task with value) finite distribution;
    * obtained by lazy recursive definition in [[TermEvolver]] and trunctation.
    */
  def termdistTask(fd: FD[Term],
                   tv: TermEvolver,
                   cutoff: Double,
                   maxtime: FiniteDuration,
                   vars: Vector[Term] = Vector()) =
    Truncate
      .task(tv.baseEvolve(fd).map(lambdaClosure(vars)), cutoff, maxtime)
      .memoize

  /**
    * evolution of terms by the ''derivative'', as a  (task with value) finite distribution;
    * obtained by lazy recursive definition in [[TermEvolver]] and trunctation.
    */
  def termdistDerTask(fd: FD[Term],
                      tfd: FD[Term],
                      tv: TermEvolver,
                      cutoff: Double,
                      maxtime: FiniteDuration,
                      vars: Vector[Term] = Vector()) =
    Truncate
      .task(tv.evolve(TangVec(fd, tfd)).vec.map(lambdaClosure(vars)),
            cutoff,
            maxtime)
      .memoize

  /**
    * An entropy measure for parsimonious generation of terms inhabiting types.
    */
  def h0(p: Double, q: Double) = {
    require(q > 0, s"Entropy with p=$p, q = $q")
    -p / (q * log(q))
  }

  /**
    * Exponent of an entropy measure for parsimonious generation of terms inhabiting types;
    * low values correspond to important terms, with the `scale` increasing sensitivity.
    */
  def hExp(p: Double, q: Double, scale: Double) =
    math.exp(-(h0(p, q) - 1) * scale)

  def prsmEntTask(termsTask: Task[FD[Term]],
                  typsTask: Task[FD[Typ[Term]]],
                  scale: Double,
                  vars: Vector[Term] = Vector()) =
    for {
      terms <- termsTask
      typs  <- typsTask
      thmsByPf  = terms.map(_.typ)
      thmsBySt  = typs.filter(thmsByPf(_) > 0)
      pfSet     = terms.flatten.supp.filter((t) => thmsBySt(t.typ) > 0)
      fullPfSet = pfSet.flatMap(partialLambdaClosures(vars))
    } yield
      fullPfSet
        .map { (pf) =>
          (pf,
           hExp(thmsBySt(pf.typ),
                thmsByPf(pf.typ),
                scale * terms(pf) / thmsByPf(pf.typ)))
        }
        .sortBy(_._2)

  def dervecTasks(base: FD[Term],
                  tv: TermEvolver,
                  termsTask: Task[FD[Term]],
                  typsTask: Task[FD[Typ[Term]]],
                  maxtime: FiniteDuration,
                  cutoff: Double,
                  scale: Double,
                  vars: Vector[Term] = Vector()): Task[Vector[Task[FD[Term]]]] =
    prsmEntTask(termsTask, typsTask, scale, vars = vars).map { (vec) =>
      {
        val scales = vec.collect {
          case (v, p) if p > cutoff && cutoff / p > 0 =>
            (v, cutoff / p)
        }
        val tot = scales.map{case (_, x) => 1/x}.sum
        val ratio = max(tot * cutoff, 1.0)
        // pprint.log(s"want: ${1/cutoff}, actual total: $tot from ${scales.size}")
        scales.map {
          case (v, sc) =>
            termdistDerTask(base, FD.unif(v), tv, sc * ratio, maxtime, vars)
        }
      }
    }

  def dervecTraceTasks(base: FD[Term],
                       tv: TermEvolver,
                       termsTask: Task[FD[Term]],
                       typsTask: Task[FD[Typ[Term]]],
                       maxtime: FiniteDuration,
                       cutoff: Double,
                       scale: Double,
                       trace: Vector[Term],
                       vars: Vector[Term] = Vector())
    : Task[Vector[Task[(FD[Term], Vector[Term])]]] =
    prsmEntTask(termsTask, typsTask, scale, vars = vars).map { (vec) =>
      {
        val scales = vec.collect {
          case (v, p) if p > cutoff && cutoff / p > 0 =>
            (v, cutoff / p)
        }
        val tot = scales.map{case (_, x) => 1/x}.sum
        val ratio = max(tot * cutoff, 1.0)
        // pprint.log(s"want: ${1/cutoff}, actual total: $tot from ${scales.size}")
        scales.map {
          case (v, sc) =>
            for {
              fd <- termdistDerTask(base, FD.unif(v), tv, sc * ratio, maxtime, vars)
            } yield (fd, trace :+ v)
        }
      }
    }

  def dervecWeightedTraceTasks(base: FD[Term],
                               tv: TermEvolver,
                               termsTask: Task[FD[Term]],
                               typsTask: Task[FD[Typ[Term]]],
                               maxtime: FiniteDuration,
                               cutoff: Double,
                               scale: Double,
                               trace: Vector[(Term, Double)],
                               vars: Vector[Term] = Vector())
    : Task[Vector[Task[(FD[Term], Vector[(Term, Double)])]]] =
    prsmEntTask(termsTask, typsTask, scale, vars = vars).map { (vec) =>
      {
        val scales = vec.collect {
          case (v, p) if p > cutoff && cutoff / p > 0 =>
            (v, p, cutoff / p)
        }
        val tot = scales.map{case (_, _, x) => 1/x}.sum
        val ratio = max(tot * cutoff, 1.0)
        // pprint.log(s"want: ${1/cutoff}, actual total: $tot from ${scales.size}")
        scales.map {
          case (v, p, sc) =>
            for {
              fd <- termdistDerTask(base, FD.unif(v), tv, sc * ratio, maxtime, vars)
            } yield (fd, trace :+ (v -> p))
        }
      }
    }

  def inTaskVec[X, Y](tv: Task[Vector[X]], p: X => Option[Y]): Task[Option[Y]] =
    tv.flatMap {
      case Vector() => Task.pure(None)
      case x +: ys =>
        Task.eval(p(x)).flatMap {
          case Some(z) => Task.pure(Some(z))
          case None    => inTaskVec(Task.eval(ys), p)
        }
    }

  def inTaskVecTask[X, Y](tv: Task[Vector[Task[X]]],
                          p: X => Option[Y]): Task[Option[Y]] =
    tv.flatMap {
      case Vector() => Task.pure(None)
      case x +: ys =>
        x.map(p).flatMap {
          case Some(z) => Task.pure(Some(z))
          case None    => inTaskVecTask(Task.eval(ys), p)
{'fraction_non_alphanumeric': 0.1322743785169884, 'fraction_numerical': 0.002279364627110193, 'mean_word_length': 1.7119953641104888, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 75, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2402111', 'n_tokens_mistral': 4528, 'n_tokens_neox': 4288, 'n_words': 1088}