// ---
// jupyter:
//   jupytext:
//     text_representation:
//       extension: .scala
//       format_name: light
//       format_version: '1.5'
//       jupytext_version: 1.14.4
//   kernelspec:
//     display_name: Scala
//     language: scala
//     name: scala
// ---

// ## Goal chomping
//
// * We run the most basic _strategic_ prover - a _goal chomper_ that keeps trying a succession of goals.
// * Termination is when a goal fails or all goals are finished.
// * Proving is only by generation, with the generation including backward reasoning rules.
// * So far the goal chomper is untested; we test this.
// * We also test updating displays etc.
//
//
// ### The goals and proving.
//
// * To generate the goals, we start with just `Type`.
// * To prove them, we include also `Zero`, `One` and `Star`

import $cp.bin.`provingground-core-jvm-d7193b6a8f.fat.jar`
import provingground._ , interface._, HoTT._, learning._ 
repl.pprinter() = {
  val p = repl.pprinter()
  p.copy(
    additionalHandlers = p.additionalHandlers.orElse {
      translation.FansiShow.fansiHandler
    }
  )
}


val terms = FiniteDistribution.unif[Term](Unit, Zero, Star)
val typs = FiniteDistribution.unif[Typ[Term]](Type, Unit, Zero)
val ts = TermState(terms, typs)
val ts0 = TermState(FiniteDistribution(), FiniteDistribution.unif(Type))

import monix.execution.Scheduler.Implicits.global
val lp = LocalProver(ts).sharpen(10)
val lp0 = LocalProver(ts0).sharpen(10)

val unknownsT = lp0.unknownStatements.map(_.entropyVec.map(_.elem)).memoize
val unF = unknownsT.runToFuture

import StrategicProvers._

import almond.display._
val chompView = Markdown("## Results from Goal chomping\n")

val chT = unknownsT.flatMap(typs => goalChomper(lp, typs)).memoize

val chF = chT.runToFuture

currentGoal
successes.size
unF.map(_.size)
successes.reverse

chF.foreach(s => chompView.withContent(s"## Goal chomping done\n\n * chomped: ${successes.size}").update())

chF.value

chF.map(_._3.headOption)

// ## Conclusions
//
// * Plenty of goals were chomped until the first failure.
// * The failure could be avoided by strategic backward reasoning.
// * Learning would also probably avoid this.
// * For a better test, we should run a liberal chomper that keeps going till there are no unknowns left, recroding both successes and failures.

StarcoderdataJupyterScriptsDedupFiltered