Malfunction backend for Idris with a FFI to OCaml
This is an experimental code generation backend for Idris that compiles it to a slightly modified version of Malfunction that has basic support for accessing identifiers outside the OCaml standard library.
This project also represents work in progress towards allowing Idris and OCaml to interoperate by implementing a ''Foreign Function Interface'' between the two languages using Idris' New FFI (described in Edwin Brady's paper and documented here).
Clone this repository:
$ git clone --recurse-submodules https://github.com/ioanluca/real-world-idris.git
$ cd real-world-idris/
$ stack build
or, if you want to install the binaries globally:
$ stack install
$ stack install idris
All idris
commands can be executed in the Stack
sandbox by prepending them with stack exec --
In the root of the repository:
$ cd malfunction/
$ opam install .
ocaml
Idris packageIn the root of the repository:
$ cd lib/
$ idris --install ocaml.ipkg
This needs to be used in Idris programs to access the FFI to OCaml.
idrisobj
OCaml packageIn the root of the repository:
$ cd rts/
$ opam install .
This is a runtime support library.
It is a wrapper around the OCaml
Obj module.
The plan is to get rid of it and implement
the required functions from Obj
using Idris primitives.
$ idris Source.idr --codegen malfunction -p ocaml --cg-opt '-op ocamllib1 -op ocamllib2' -o a.out
$ ./a.out
-op
is short for --ocamlpackage
Alternatively, %lib malfunction "ocamllib"
can be used in an Idris file to link an OCaml library.
Some test programs can be found in test-idris.
To compile the graphics example:
$ cd test-idris/
$ cd graphics/
$ idris IdrCamlGrphics.idr --codegen malfunction -p ocaml --cg-opt '-op graphics' -o CamlGraphics.out
$ ./CamlGraphics.out
Note that the above example is linking the
OCaml graphics module
using the --cg-opt '-op graphics'
flags.
Alternatively, graphics
could also be linked by having the
following line in IdrCamlGraphics.idr:
%lib malfunction "graphics"
Some example programs can be found in benchmark.
It seems to go pretty fast compared to the default C backend:
$ idris pythag.idr -o pythag-idris
$ idris pythag.idr --codegen malfunction -o pythag-malfunction
$ time ./pythag-idris > /dev/null
real 0m4.548s
user 0m4.528s
sys 0m0.016s
$ time ./pythag-malfunction > /dev/null
real 0m0.654s
user 0m0.652s
sys 0m0.000s
Tested on:
16.04.4 LTS 64-bit
1.2.0
v0.2.1
4.05.0+flambda
.cmi
filesContributions are welcome!