Building and Running

I’ve had some issues getting the chez scheme backend to work on my computer, so I build the project using the racket backend with the following command:

idris2 --cg racket --build ./Bus.ipkg

This will build the executable file ./build/exec/runTests, which will perform the synthesis when run.

You can also build and run the project in one step by running run.sh.

Project Structure

The implementation is broken up into a few files:

• Language.idr, which describes how to define languages
• Bus.idr, which implements the algorithm itself
• Math.idr and Lists.idr, which implement math and list languages
• Array.idr, which parameterizes languages as implicitly working over vectors
• Tests.idr, which defines an executable which tests the implementation

Implementation Notes

The algorithm itself only works on a single input-output example for a given language. To get around this, you can use the Array function, which maps a language over a given type to a language over an n-ary vector over that type. This allows the user to phrase n input-output pairs as one input-output pair over n-ary vectors.