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-68f2b038f1.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]:
show(nonDetOpt)
In [9]:
show(nonDetOpt.map(eq => TermData.isleNormalize(eq)))
In [10]:
val atoms = (eqs.map(_.rhs).flatMap(Expression.varVals(_)) union eqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[10]:
In [11]:
import TermRandomVars._, GeneratorVariables._
val elemTerms = atoms.collect{case Elem(t: Term, Terms) => t}
Out[11]:
In [12]:
elemTerms.exists(_.dependsOn(A))
Out[12]:
In [13]:
atoms.size
Out[13]:
In [14]:
val elemTyps = atoms.collect{case Elem(t: Typ[Term], Typs) => t}
Out[14]:
In [15]:
val normEqs = eqs.map(eq => TermData.isleNormalize(eq))
Out[15]:
In [16]:
val normAtoms = (normEqs.map(_.rhs).flatMap(Expression.varVals(_)) union normEqs.map(_.lhs).flatMap(Expression.varVals(_))).map(_.variable)
Out[16]:
In [17]:
val normElemTerms = normAtoms.collect{case Elem(t: Term, Terms) => t}
Out[17]:
In [18]:
elemTerms == normElemTerms
Out[18]:
In [19]:
val ts0 = TermState(FiniteDistribution.empty, FiniteDistribution.unif(Type))
Out[19]:
In [20]:
val ev = ExpressionEval.fromInitEqs(ts0, Equation.group(eqs), TermGenParams(), decayS = 0.95)
Out[20]:
In [21]:
val termsT = ev.finalTerms
Out[21]:
In [22]:
val evN = ExpressionEval.fromInitEqs(ts0, Equation.group(normEqs), TermGenParams(), decayS = 0.95)
Out[22]:
In [22]:
// val termsN = evN.finalTerms
In [23]:
evN.init
Out[23]:
In [24]:
import ExpressionEval._
Out[24]:
In [25]:
evN.equations
Out[25]:
In [26]:
val m1 = nextMap(evN.init, evN.equations)
Out[26]:
In [27]:
m1.values
Out[27]:
In [28]:
val exp = m1.find(_._2 < 0).get._1
Out[28]:
In [29]:
val rhs = evN.equations.find(_.lhs == exp).map(_.rhs).get
Out[29]:
In [30]:
normEqs.filter(_.lhs == exp)
Out[30]:
In [31]:
normEqs.filter(_.lhs == exp).size
Out[31]:
In [32]:
val baseEqs = eqs.filter(eq => TermData.isleNormalize(eq).lhs == exp)
Out[32]:
In [33]:
baseEqs.size
Out[33]:
In [34]:
show(baseEqs.map(_.rhs))
In [35]:
val mm1 = nextMap(ev.init, ev.equations)
Out[35]:
In [36]:
mm1.values
Out[36]:
In [37]:
mm1.filter(_._2 < 0)
Out[37]:
In [40]:
baseEqs.map(_.mapVars(v => TermRandomVars.isleNormalizeVars(v, Vector()))
).map(_.rhs)
Out[40]:
In [41]:
normEqs.filter(_.lhs == exp).map(_.rhs)
Out[41]:
In [42]:
evN.equations.filter(_.lhs == exp).map(_.rhs)
Out[42]:
In [43]:
baseEqs.map(_.lhs).size
Out[43]:
In [44]:
baseEqs.map(_.rhs)
Out[44]:
In [46]:
baseEqs.map(_.rhs).map(e => recExp(ev.init, e))
Out[46]:
In [47]:
val imEqs = normEqs.filter(_.lhs == exp)
Out[47]:
In [48]:
imEqs.map(_.rhs).map(e => recExp(evN.init, e))
Out[48]:
In [49]:
evN.equations.find(_.lhs == exp).size
Out[49]:
In [57]:
val eqq = evN.equations.find(_.lhs == exp).head
Out[57]:
In [58]:
recExp(evN.init, eqq.rhs)
Out[58]:
In [55]:
evN.init.get(exp)
Out[55]:
In [56]:
stabRecExp(evN.init, exp, None)
Out[56]:
In [54]:
m1(exp)
Out[54]:
In [ ]:
nextMap(evN.init, evN.equations, )
In [39]:
baseEqs.head
Out[39]:
In [59]:
imEqs.map(_.rhs).map(e => e -> recExp(evN.init, e))
Out[59]:
In [60]:
baseEqs.map(_.rhs).map(e => e -> recExp(ev.init, e))
Out[60]:
In [61]:
eqq.rhs
Out[61]:
In [62]:
show(baseEqs.map(_.lhs))
Literal(1) on the right-hand side.IsleScale(@b, Elem(@b, Terms) and IsleScale(@a, Elem(@a, Terms) do not merge.mapVars and instead recurse over expressions with substitutions, including IsleScale in an obvious ways.