Geb to Poly Compilation Bug

[agureev]

The to-poly function 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 = 0 or name 1 = 1 will fail during the Vamp-IR verification stage.

The interpreters and uncurry allowed to pinpoint that the fault seems to lie in the to-poly compiler 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/8

The use of gapply in 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 with to-poly and fix it.

[rokopt]

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.