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-294d1cadfc.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 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}
show(normEqs.take(10).map(_.lhs))
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
termsT.support == termsN.support
ExpressionEval.mapRatio(termsT.toMap, termsN.toMap)
val bigT = termsT.support.maxBy(t => termsT(t) / termsN(t))
termsT(bigT)
termsN(bigT)
val bigN = termsT.support.maxBy(t => termsN(t) / termsT(t))
termsT(bigN)
termsN(bigN)
val ns = lp.nextState.runSyncUnsafe()
val x = nextVar(A, Vector())
val ctx = Context.Empty.addVariable(x)
val y = nextVar(A, ctx.variables)
Even with contexts, variable names are correct. We now investigate type generation.
ns.typs
val eq0 = lp.equations.runSyncUnsafe()
import Expression._
val varsEq0 = eq0.map(_.lhs).flatMap(varVals).map(_.variable)
val elemsEq0 = varsEq0.collect{case el @ Elem(_, _) => el}
clearly there are types here.
ev.finalTyps
val typEqs0 = eq0.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
val ev0 = lp.expressionEval.runSyncUnsafe()
ev0.equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ev0.piExportEquations(a).collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ev0.relVariable(a).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ExpressionEval.export(ev0, Vector(A, B, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ExpressionEval.export(ev0, Vector(B, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ExpressionEval.export(ev0, Vector(B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ExpressionEval.export(ev0, Vector(A, B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ExpressionEval.export(ev0, Vector(A, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ExpressionEval.export(ev0, Vector(a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
val ev1 = ExpressionEval.export(ev0, Vector(a))
ExpressionEval.export(ev1, Vector(B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ev1.piExportEquations(B).collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
ev1.finalTyps
ev0.init
ev1.init
ev1.equations.collect{case eq @ Equation(FinalVal(Elem(A, Typs)), _) => eq}
ev0.equations.collect{case eq @ Equation(FinalVal(Elem(A, Typs)), _) => eq}
A.dependsOn(a)
FinalVal(Elem(A, Typs)) once we export by a, as all equations are assumed to be in island.def varDepends(t: Term)(v: Variable[_]) : Boolean =
v match {
case Elem(element: Term, randomVar) => element.dependsOn(t)
case Elem(element, randomVar) => false
case Event(base, sort) => false
case InIsle(isleVar, boat, isle) => varDepends(t)(isleVar)
case PairEvent(base1, base2, sort) => false
}
def equationDepends(t: Term)(eq : Equation) : Boolean = {
import Expression.varVals
val genvars = varVals(eq.lhs).map(_.variable) union varVals(eq.lhs).map(_.variable)
genvars.exists(v => varDepends(t)(v))
}
ev0.equations.size
ev0.equations.take(20).map(equationDepends(a))
ev0.equations.take(100).map(equationDepends(a))
val indepEqs= ev0.equations.filterNot(equationDepends(a))
This was computed fast. The previous shortcut based attempt made things slow. For safety, we will run the update in a copy of this notebook.