Apostolis Xekoukoulotakis
2018-11-05 21:43:58 UTC
agda-ocaml is an experimental OCaml backend that uses Stephen Dolan's
malfunction package to target OCaml's internal flambda representation. It
is an extension of previous work by Frederik HanghÞj Iversen and Jan Mas
Rovira.
The main features of this version is that it supports pragmas. You can use
OCaml from Agda or export agda code as an OCaml module.
The internal representation of agda mimics the internal representation of
OCaml, so that any OCaml data type or function is easily accessible from
Agda and the opposite.
If you are interested in testing it, I managed to write some documentation
in its github repository as well as its current limitations.
https://github.com/xekoukou/agda-ocaml
malfunction package to target OCaml's internal flambda representation. It
is an extension of previous work by Frederik HanghÞj Iversen and Jan Mas
Rovira.
The main features of this version is that it supports pragmas. You can use
OCaml from Agda or export agda code as an OCaml module.
The internal representation of agda mimics the internal representation of
OCaml, so that any OCaml data type or function is easily accessible from
Agda and the opposite.
If you are interested in testing it, I managed to write some documentation
in its github repository as well as its current limitations.
https://github.com/xekoukou/agda-ocaml