Skip to content

Latest commit

 

History

History
25 lines (16 loc) · 1.16 KB

README.org

File metadata and controls

25 lines (16 loc) · 1.16 KB
Raw

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.