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,
In [1]:
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
}
)
}
Out[1]:
In [2]:
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))
Out[2]:
In [3]:
val lp = LocalProver(ts)
Out[3]:
In [4]:
ts.vars
import TermData._
val datT = termData(lp)
Out[4]:
In [5]:
import monix.execution.Scheduler.Implicits.global
val td = datT.runSyncUnsafe()
Out[5]:
In [6]:
val (ns, eqs) = td
Out[6]:
In [7]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[7]:
In [8]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
Out[8]:
In [9]:
elemTerms.exists(_.dependsOn(A))
Out[9]:
In [10]:
atoms.size
Out[10]:
In [11]:
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[11]:
In [12]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[12]:
In [13]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[13]:
In [14]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[14]:
In [15]:
show(normEqs.take(10).map(_.lhs))
In [16]:
elemTerms == normElemTerms
Out[16]:
In [17]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[17]:
In [18]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[18]:
In [19]:
val termsT = ev.finalTerms
Out[19]:
In [20]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[20]:
In [21]:
val termsN = evN.finalTerms
Out[21]:
In [22]:
termsT.support == termsN.support
Out[22]:
In [23]:
ExpressionEval.mapRatio(termsT.toMap, termsN.toMap)
Out[23]:
In [24]:
val bigT = termsT.support.maxBy(t => termsT(t) / termsN(t))
Out[24]:
In [25]:
termsT(bigT)
termsN(bigT)
Out[25]:
In [26]:
val bigN = termsT.support.maxBy(t => termsN(t) / termsT(t))
Out[26]:
In [27]:
termsT(bigN)
termsN(bigN)
Out[27]:
In [28]:
val ns = lp.nextState.runSyncUnsafe()
Out[28]:
In [29]:
val x = nextVar(A, Vector())
Out[29]:
In [30]:
val ctx = Context.Empty.addVariable(x)
val y = nextVar(A, ctx.variables)
Out[30]:
Even with contexts, variable names are correct. We now investigate type generation.
In [31]:
ns.typs
Out[31]:
In [32]:
val eq0 = lp.equations.runSyncUnsafe()
Out[32]:
In [33]:
import Expression._
val varsEq0 = eq0.map(_.lhs).flatMap(varVals).map(_.variable)
Out[33]:
In [34]:
val elemsEq0 = varsEq0.collect{case el @ Elem(_, _) => el}
Out[34]:
clearly there are types here.
In [35]:
ev.finalTyps
Out[35]:
In [36]:
val typEqs0 = eq0.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[36]:
In [37]:
val ev0 = lp.expressionEval.runSyncUnsafe()
Out[37]:
In [38]:
ev0.equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[38]:
In [39]:
ev0.piExportEquations(a).collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[39]:
In [40]:
ev0.relVariable(a).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[40]:
In [41]:
ExpressionEval.export(ev0, Vector(A, B, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[41]:
In [42]:
ExpressionEval.export(ev0, Vector(B, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[42]:
In [43]:
ExpressionEval.export(ev0, Vector(B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[43]:
In [44]:
ExpressionEval.export(ev0, Vector(A, B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[44]:
In [45]:
ExpressionEval.export(ev0, Vector(A, a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[45]:
In [46]:
ExpressionEval.export(ev0, Vector(a)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[46]:
In [47]:
val ev1 = ExpressionEval.export(ev0, Vector(a))
Out[47]:
In [48]:
ExpressionEval.export(ev1, Vector(B)).equations.collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[48]:
In [49]:
ev1.piExportEquations(B).collect{case eq @ Equation(FinalVal(Elem(_, Typs)), _) => eq}
Out[49]:
In [50]:
ev1.finalTyps
Out[50]:
In [51]:
ev0.init
Out[51]:
In [52]:
ev1.init
Out[52]:
In [53]:
ev1.equations.collect{case eq @ Equation(FinalVal(Elem(A, Typs)), _) => eq}
Out[53]:
In [54]:
ev0.equations.collect{case eq @ Equation(FinalVal(Elem(A, Typs)), _) => eq}
Out[54]:
In [55]:
A.dependsOn(a)
Out[55]:
In [56]:
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))
}
Out[56]:
In [57]:
ev0.equations.size
Out[57]:
In [58]:
ev0.equations.take(20).map(equationDepends(a))
Out[58]:
In [59]:
ev0.equations.take(100).map(equationDepends(a))
Out[59]:
In [60]:
val indepEqs= ev0.equations.filterNot(equationDepends(a))
Out[60]:
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.