In [1]:
import $ivy.`io.github.siddhartha-gadgil::provingground-core-jvm:0.1.0`
Out[1]:
In [2]:
import provingground._ , interface._, HoTT._
import provingground.{FiniteDistribution => FD}
import learning._
Out[2]:
We define the inductive structure on the natural numbers.
In [3]:
val Nat = Type.sym
val zero = Nat.sym
val succ = (Nat ->: Nat).sym
val natIntros = Vector(zero, succ)
Out[3]:
In [4]:
import induction._
val natStr = provingground.induction.ExstInducStrucs.get(Nat, natIntros)
Out[4]:
In [5]:
val natDef = ExstInducDefn(Nat, natIntros, natStr)
Out[5]:
Next, we set up for generation
In [6]:
val ts = TermState(FD.unif(Nat, zero, succ), FD.unif(Nat, Type), inds = FD.unif(natDef))
val tg = TermGenParams()
Out[6]:
In [7]:
val mfd = tg.monixFD
Out[7]:
A check that inductive types are picked up from the initial distribution.
In [8]:
import TermRandomVars._
val idT = mfd.varDist(ts)(InducDefns, 0.1)
Out[8]:
In [9]:
import monix.execution.Scheduler.Implicits.global
repl.pprinter.bind(translation.FansiShow.fansiPrint)
val inducFD = idT.runSyncUnsafe()
Out[9]:
In [10]:
val domT = mfd.varDist(ts)(domForInduc(natDef), 0.1)
Out[10]:
In [11]:
val domFD = domT.runSyncUnsafe()
Out[11]:
In [12]:
val ndT = mfd.nodeDist(ts)(tg.Gen.recFuncFoldedNode, 0.001)
Out[12]:
In [13]:
val nfd = ndT.runSyncUnsafe()
Out[13]:
In [14]:
val nnT = mfd.varDist(ts)(termsWithTyp(Nat ->: Nat), 0.1)
Out[14]:
In [15]:
val nnD = nnT.runSyncUnsafe()
Out[15]:
In [16]:
nfd.map(_.typ).flatten
Out[16]:
In [17]:
val nidT = mfd.nodeDist(ts)(tg.Gen.inducFuncFoldedNode, 0.00001)
Out[17]:
In [18]:
val nifd = nidT.runSyncUnsafe()
Out[18]:
In [19]:
nifd.map(_.typ).flatten
Out[19]:
In [20]:
termsWithTyp(typFamilyTarget(Nat).get)
val tfT = mfd.varDist(ts)(termsWithTyp(typFamilyTarget(Nat).get), 0.001)
Out[20]:
In [21]:
val tfD = tfT.runSyncUnsafe()
Out[21]:
In [22]:
val n = Nat.sym
val rel = (Nat ->: Type).sym
val allRel = (n ~>: rel(n)).sym
val ts1 = TermState(FD.unif(Nat, zero, succ, rel, allRel), FD.unif(Nat, Type), inds = FD.unif(natDef))
Out[22]:
In [23]:
val tfT1 = mfd.varDist(ts1)(termsWithTyp(typFamilyTarget(Nat).get), 0.001)
Out[23]:
In [24]:
val tfD1 = tfT1.runSyncUnsafe()
Out[24]:
In [25]:
val nidT1 = mfd.nodeDist(ts1)(tg.Gen.inducFuncFoldedNode, 0.000005)
val nifd1 = nidT1.runSyncUnsafe()
Out[25]:
In [26]:
nifd1.map(_.typ).flatten
Out[26]:
In [27]:
val indF = natStr.inducOpt(Nat, n :-> rel(n)).get
Out[27]:
In [28]:
indF.typ
Out[28]:
In [29]:
nifd1.filter(_.typ == n ~>: rel(n))
Out[29]:
In [30]:
val A = "A" :: Type
val List = "List" :: Type ->: Type
val nil = "nil" :: (A ~>: List(A))
val cons = "cons" :: A ~>: (A ->: List(A) ->: List(A))
Out[30]:
In [31]:
val listAIntros = Vector(nil(A), cons(A))
val listAStr = ExstInducStrucs.get(List(A), listAIntros)
Out[31]:
In [32]:
val listStr = ExstInducStrucs.LambdaInduc(A, listAStr)
Out[32]:
In [33]:
val listDef = ExstInducDefn(List, Vector(nil, cons) ,listStr)
Out[33]:
In [34]:
val tsL = TermState(FD.unif(Nat, zero, succ, List, nil, cons), FD.unif(Nat, Type), inds = FD.unif(natDef, listDef))
Out[34]:
In [ ]:
In [35]:
val domLT = mfd.varDist(ts)(domForInduc(listDef), 0.00001)
Out[35]:
In [36]:
val domLD = domLT.runSyncUnsafe()
Out[36]:
In [37]:
val ndLT = mfd.nodeDist(tsL)(tg.Gen.recFuncFoldedNode, 0.0001)
Out[37]:
In [38]:
val ndLD = ndLT.runSyncUnsafe()
Out[38]:
In [39]:
ndLD.map(_.typ).flatten
Out[39]:
In [40]:
ndLD.support.size
Out[40]:
In [41]:
val fns = ndLD.support.groupBy(_.typ)
Out[41]:
In [42]:
val lToL = fns(List(Nat) ->: List(Nat))
Out[42]:
In [43]:
nil(Nat).typ
cons(Nat).typ
Out[43]:
In [44]:
val l0 = cons(Nat)(zero)(nil(Nat))
Out[44]:
In [45]:
val l1 = cons(Nat)(succ(zero))(l0)
Out[45]:
In [46]:
import Fold._
lToL.map(fn => fn(l1))
Out[46]:
In [47]:
val Vec = "Vec" :: Type ->: Nat ->: Type
val vnil = "vnil" :: (A ~>: Vec(A)(zero))
val vcons = "vcons" :: A ~>: (n ~>: (A ->: Vec(A)(n) ->: Vec(A)(succ(n))))
Out[47]:
In [48]:
val vecAIntros = Vector(vnil(A), vcons(A))
val vecAStr = ExstInducStrucs.getIndexed(Vec(A), vecAIntros)
Out[48]:
In [49]:
val vecStr = ExstInducStrucs.LambdaInduc(A, vecAStr)
Out[49]:
In [50]:
val vecDef = ExstInducDefn(Vec, Vector(vnil, vcons) ,vecStr)
val tsV = TermState(FD.unif(Nat, zero, succ, Vec, vnil, vcons), FD.unif(Nat, Type), inds = FD.unif(vecDef))
Out[50]:
In [51]:
val domVT = mfd.varDist(ts)(domForInduc(vecDef), 0.00001)
Out[51]:
In [52]:
val domVD = domVT.runSyncUnsafe()
Out[52]:
In [53]:
val ndVT = mfd.nodeDist(tsV)(tg.Gen.recFuncFoldedNode, 0.0001)
Out[53]:
In [54]:
val ndVD = ndVT.runSyncUnsafe()
Out[54]:
In [55]:
ndVD.map(_.typ)
Out[55]:
In [56]:
val vfn = vecStr.recOpt(Vec(Nat), A).get
Out[56]:
In [57]:
vfn.typ
Out[57]:
In [58]:
vfn("a" :: A)
Out[58]:
In [59]:
val a = "a" :: A
vfn(a).typ
Out[59]:
In [60]:
val B = "B" :: Type
vecAStr.recOpt(Vec(A), B)
Out[60]:
In [61]:
vecStr.recOpt(Vec(A), B)
Out[61]:
In [62]:
vecStr.recOpt(Vec(B), Nat)
Out[62]:
In [63]:
val ok = vecStr.recOpt(Vec(A), Nat).get
Out[63]:
In [64]:
val bok = ok.replace(A, B)
Out[64]:
In [65]:
bok.typ
Out[65]:
In [66]:
val nok = vecStr.recOpt(Vec(B), Nat).get
Out[66]:
In [67]:
vecAStr.subs(A, B).recOpt(Vec(B), Nat)
Out[67]:
In [68]:
vecAStr
vecAStr.subs(A, B)
Out[68]:
In [69]:
val ndViT = mfd.nodeDist(tsV)(tg.Gen.inducFuncFoldedNode, 0.0001)
Out[69]:
In [70]:
val ndViD = ndViT.runSyncUnsafe()
Out[70]:
In [71]:
ndViD.map(_.typ).flatten
Out[71]:
In [72]:
val tgVT = mfd.nodeDist(tsV)(tg.Gen.codomainNode(Vec(Nat)(succ(zero))), 0.0001)
Out[72]:
In [73]:
val tgVD = tgVT.runSyncUnsafe()
Out[73]:
In [74]:
tgVD.map(_.typ).flatten
Out[74]:
In [75]:
Unify.targetCodomain(vcons, Vec(Nat)(succ(zero)))
Out[75]:
In [76]:
Unify.unify(vcons.typ, Vec(Nat)(succ(zero)), (t) => false)
Out[76]:
In [77]:
val tgtVT = mfd.nodeDist(tsV)(tg.Gen.foldedTargetFunctionNode(Vec(Nat)(succ(zero))), 0.001)
Out[77]:
In [78]:
val tgtVD = tgtVT.runSyncUnsafe()
Out[78]:
In [79]:
val tgtNT = mfd.nodeDist(tsV)(tg.Gen.foldedTargetFunctionNode(Nat ->: Nat), 0.001)
Out[79]:
In [80]:
val tgtND = tgtNT.runSyncUnsafe()
Out[80]:
In [81]:
val node = tg.Gen.foldFuncTarget(succ, Nat, Terms).get
Out[81]:
In [82]:
val fd = mfd.nodeDist(tsV)(node, 0.0001).runSyncUnsafe()
Out[82]:
In [83]:
val nfd = mfd.nodeDist(tsV)(tg.Gen.codomainNode(Nat ->: Nat), 0.001).runSyncUnsafe()
Out[83]:
In [84]:
val ffd = mfd.varDist(tsV)(funcForCod(Nat ->: Nat), 0.0001).runSyncUnsafe()
Out[84]:
In [92]:
val indTargT = mfd.nodeDist(ts1)(tg.Gen.targetInducNode(Nat ->: Nat), 0.0001)
Out[92]:
In [93]:
indTargT.runSyncUnsafe()
Out[93]:
In [ ]: