rokopt
commented
1 year ago A note: this bug only affects internal development/testing if someone specifically intentionally exercises the to-poly backend. It shouldn't affect users, such as Juvix, or our usual testing, because the to-poly compilation path has been replaced as the default by to-bitc.
The
to-polyfunction taking Geb morphisms to the Poly category seems to be faulty. The issue this stems from is #93 and has to do with evaluating the identity function on Bool in STLC -(lamb (coprod so1 so1) (index 0))- in the empty context.In particular, the code given by
(to-circuit nil (lamb (coprod so1 so1) (index 0)) :name)accompanied with the entry code and additional constraint for checking such as
name 0 = 0orname 1 = 1will fail during the Vamp-IR verification stage.The interpreters and
uncurryallowed to pinpoint that the fault seems to lie in theto-polycompiler step taking Geb morphisms to Poly. In particular, evaluating the object of poly at 0 and 1 gives(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 0) 1/8(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 1) 3/8(note this code is run in
geb.trans) while the correct application should give(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 0) 1/8(geb.generics:gapply (to-poly (uncurry (coprod so1 so1) (coprod so1 so1) (geb.lambda.trans:compile-checked-term nil (geb.lambda:lamb (coprod so1 so1) (geb.lambda:index 0)) ))) 1) 3/8The use of
gapplyin Geb seems to suggest that the STLC to Geb part of the pipeline works fine, so we need to figure out what is going awry withto-polyand fix it.