This is after correcting the issue with context variables. There are still a couple of things to test and correct.
When we have variables such as $A: Type$, $a : A$ and $B: Type$, we test whether we correctly:
This time the test is more refined. Namely,
import $cp.bin.`provingground-core-jvm-68f2b038f1.fat.jar`
import provingground._ , interface._, HoTT._, learning._
repl.pprinter() = {
val p = repl.pprinter()
p.copy(
additionalHandlers = p.additionalHandlers.orElse {
translation.FansiShow.fansiHandler
}
)
}
val A = "A" :: Type
val B = "B" :: Type
val a = "a" :: A
val ts = TermState(FiniteDistribution.unif(a), FiniteDistribution.unif(A, B), vars = Vector(A, B, a))
val lp = LocalProver(ts)
ts.vars
import TermData._
val datT = termData(lp)
import monix.execution.Scheduler.Implicits.global
val td = datT.runSyncUnsafe()
val (ns, eqs) = td
val nonDetOpt = eqs.find(eq => TermData.isleNormalize(eq) != TermData.isleNormalize(eq))
show(nonDetOpt)
show(nonDetOpt.map(eq => TermData.isleNormalize(eq)))
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
elemTerms.exists(_.dependsOn(A))
atoms.size
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
elemTerms == normElemTerms
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
val termsT = ev.finalTerms
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
// val termsN = evN.finalTerms
evN.init
import ExpressionEval._
evN.equations
val m1 = nextMap(evN.init, evN.equations)
m1.values
val exp = m1.find(_._2 < 0).get._1
val rhs = evN.equations.find(_.lhs == exp).map(_.rhs).get
normEqs.filter(_.lhs == exp)
normEqs.filter(_.lhs == exp).size
val baseEqs = eqs.filter(eq => TermData.isleNormalize(eq).lhs == exp)
baseEqs.size
show(baseEqs.map(_.rhs))
val mm1 = nextMap(ev.init, ev.equations)
mm1.values
mm1.filter(_._2 < 0)
baseEqs.map(_.mapVars(v => TermRandomVars.isleNormalizeVars(v, Vector()))
).map(_.rhs)
normEqs.filter(_.lhs == exp).map(_.rhs)
evN.equations.filter(_.lhs == exp).map(_.rhs)
baseEqs.map(_.lhs).size
baseEqs.map(_.rhs)
baseEqs.map(_.rhs).map(e => recExp(ev.init, e))
val imEqs = normEqs.filter(_.lhs == exp)
imEqs.map(_.rhs).map(e => recExp(evN.init, e))
evN.equations.find(_.lhs == exp).size
val eqq = evN.equations.find(_.lhs == exp).head
recExp(evN.init, eqq.rhs)
evN.init.get(exp)
stabRecExp(evN.init, exp, None)
m1(exp)
nextMap(evN.init, evN.equations, )
baseEqs.head
imEqs.map(_.rhs).map(e => e -> recExp(evN.init, e))
baseEqs.map(_.rhs).map(e => e -> recExp(ev.init, e))
eqq.rhs
show(baseEqs.map(_.lhs))
Literal(1) on the right-hand side.IsleScale(@b, Elem(@b, Terms) and IsleScale(@a, Elem(@a, Terms) do not merge.mapVars and instead recurse over expressions with substitutions, including IsleScale in an obvious ways.