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-a0afa6a903.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]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[11]:
In [12]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[12]:
In [13]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[13]:
In [14]:
elemTerms == normElemTerms
Out[14]:
In [15]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[15]:
In [16]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[16]:
In [17]:
val termsT = ev.finalTerms
Out[17]:
In [18]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[18]:
In [ ]:
// val termsN = evN.finalTerms
In [19]:
evN.init
Out[19]:
In [20]:
import ExpressionEval._
Out[20]:
In [ ]:
evN.equations
In [21]:
val m1 = nextMap(evN.init, evN.equations)
Out[21]:
In [23]:
val exp = m1.find(_._2 < 0)
Out[23]:
In [24]:
val termsN = evN.finalTerms
Out[24]:
In [25]:
evN.finalDist
Out[25]:
In [26]:
evN.finalDist.keys
Out[26]:
In [28]:
import Expression._
evN.finalDist.get(FinalVal(Elem(Type, Typs)))
Out[28]:
In [29]:
normEqs.filter(_.lhs == FinalVal(Elem(Type, Typs)))
Out[29]:
In [30]:
eqs.filter(_.lhs == FinalVal(Elem(Type, Typs)))
Out[30]:
In [31]:
ev.finalDist.get(FinalVal(Elem(Type, Typs)))
Out[31]:
In [32]:
val t = termsT.support.head
Out[32]:
In [33]:
eqs.find(_.lhs == Elem(t, Terms))
Out[33]:
In [34]:
eqs.collect{case eqq @ EquationNode(FinalVal(Elem(_, _)), _) => eqq}
Out[34]:
In [37]:
val eqn0 = eqs.find(_.lhs == FinalVal(Elem(t, Terms))).get
Out[37]:
In [38]:
TermRandomVars.isleNormalize(eqn0)
Out[38]:
In [40]:
val rhs0 = varVals(eqn0.rhs).head
Out[40]:
In [41]:
ev.finalDist.get(rhs0)
Out[41]:
In [45]:
val eqn1 = eqs.filter(_.lhs == rhs0).head
Out[45]:
In [46]:
import TermRandomVars._
isleNormalize(eqn1)
Out[46]:
In [47]:
normEqs.filter(_.lhs == FinalVal(Elem(t, Terms)))
Out[47]:
There is still an equation at this stage. May not be one at the next stage.
In [48]:
val rhsN= normEqs.filter(_.lhs == FinalVal(Elem(t, Terms))).head.rhs
Out[48]: