anoma / geb

A Categorical View of Computation
https://anoma.github.io/geb/
GNU General Public License v3.0
28 stars 10 forks source link

Change Variable Wire Printing for Compiled VampIR Function #170

Closed agureev closed 10 months ago

agureev commented 11 months ago

Previously a Lambda function taking natural number arguments A1 to An would be compiled to a circuit with arguments x1 to x(n+1) where argument xi in the circuit for i<(n+1) stands for argument A(n-i) and x(n+1) stands as an unused variable.

Current change omits the final variable and reverses the rest, so that the compiled circuit will have arguments xn to x1 in that order.

Hence one gets results such as:

TRANS> (to-circuit (lamb (list int) (lamb (list int) (plus (index 0) (index 1)))) :name)
(def name x2 x1 = {
   (x1 + x2)
 };)
TRANS> (to-circuit (unit) :name)
(def name = {
   ()
 };)

Note that this changes how to input coproduct type circuit variables.