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-38c4a5770c.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 nonDetOpt = eqs.find(eq => TermData.isleNormalize(eq) != TermData.isleNormalize(eq))
Out[7]:
In [8]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[8]:
In [9]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
Out[9]:
In [10]:
elemTerms.exists(_.dependsOn(A))
Out[10]:
In [11]:
atoms.size
Out[11]:
In [12]:
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[12]:
In [13]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[13]:
In [14]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[14]:
In [15]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[15]:
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 [20]:
// val termsN = evN.finalTerms
In [21]:
import ExpressionEval._
Out[21]:
In [22]:
val m1 = nextMap(evN.init, evN.equations)
Out[22]:
In [23]:
m1.values
Out[23]:
In [24]:
val exp = m1.find(_._2 < 0).get._1
Out[24]:
In [25]:
val rhs = evN.equations.find(_.lhs == exp).map(_.rhs).get
Out[25]:
In [26]:
normEqs.filter(_.lhs == exp)
Out[26]:
In [27]:
normEqs.filter(_.lhs == exp).size
Out[27]:
In [28]:
val baseEqs = eqs.filter(eq => TermData.isleNormalize(eq).lhs == exp)
Out[28]:
In [29]:
baseEqs.size
Out[29]:
In [30]:
show(baseEqs.map(_.rhs))
In [31]:
show(baseEqs.map(_.lhs))
In [32]:
show(normEqs.filter(_.lhs == exp))
In [33]:
val baseGps = baseEqs.groupBy(eq => TermData.isleNormalize(eq))
Out[33]:
In [34]:
show(baseGps.head)
In [35]:
baseGps.head._2.size
Out[35]:
In [36]:
baseGps.size
Out[36]:
In [37]:
baseGps.values.map(_.size)
Out[37]:
In [38]:
show(baseGps.tail.head)
In [39]:
show(baseGps.tail.tail.head)
In [40]:
import TermRandomVars._, TermGeneratorNodes._
val rvA = termsWithTyp(A)
Out[40]:
In [41]:
randomVarSubs(A, B)(rvA)
Out[41]:
In [43]:
val eqn = baseGps.toVector(2)._2.head
Out[43]:
In [44]:
TermData.isleNormalize(eqn)
Out[44]: