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-4240e21976.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), context = Context.Empty.addVariable(A).addVariable(B).addVariable(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 [24]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[24]:
In [25]:
val termsN = evN.finalTerms
Out[25]:
In [27]:
termsT.support == termsN.support
Out[27]:
In [28]:
ExpressionEval.mapRatio(termsT.toMap, termsN.toMap)
Out[28]:
In [29]:
val bigT = termsT.support.maxBy(t => termsT(t) / termsN(t))
Out[29]:
In [30]:
termsT(bigT)
termsN(bigT)
Out[30]:
In [31]:
val bigN = termsT.support.maxBy(t => termsN(t) / termsT(t))
Out[31]:
In [32]:
termsT(bigN)
termsN(bigN)
Out[32]:
In [33]:
val ns = lp.nextState.runSyncUnsafe()
Out[33]:
In [34]:
val x = nextVar(A, Vector())
Out[34]:
In [35]:
val ctx = Context.Empty.addVariable(x)
val y = nextVar(A, ctx.variables)
Out[35]:
The error may be because of two independent ways in which variables are generated.