Uncurry Pipeline Usage

[agureev]

Now that we tested out uncurry so that our compilation can be intuitively tested pointwise both in Geb and in Poly instead of passing through the additional isomorphisms, we have a question regarding how to actually implement it.

uncurry currently needs three arguments, two for domain and codomain of the exponential object and one for the morphism we are applying it two. The domain/codomain are needed since we don't have accessors to so-hom-obj.

In order to not burden the user with providing explicit types, we will have to figure out (at least initially until higher-order function translation to Vamp-IR is implemented) how to streamline this process.

[rokopt]

Does #107 address this?

[rokopt]

Can this be closed as fixed by #115 ?

[rokopt]

Can this be closed as fixed by #115 ?

Not yet -- Artem is still working on more required indexing changes.

[agureev]

Made improvements in #127. That is, now given a term whose type is an n-iterated fun-type with codomain A such that A is not of type fun-type, it compiles to an n-argument function in Vamp-IR.

However, that does not suffice for general cases. E.g. compiling (pair (unit) (lambda (list (coprod so1 so1)) (index 0))) will still give out a quoted function on the right.

[agureev]

Note that #138 changes the compilation to optimize costly uncurry with a simple replacement strategy.