Idris2-Erlang
Idris2-Erlang copied to clipboard
chrrasmussen
Erlang code generator for Idris 2
[`Data.IORef`](https://github.com/chrrasmussen/Idris2-Erlang/blob/ff9499539d41c1e659a814895d7b02355b759d02/idris2/libs/base/Data/IORef.idr), [`Data.IOArray`](https://github.com/chrrasmussen/Idris2-Erlang/blob/ff9499539d41c1e659a814895d7b02355b759d02/idris2/libs/base/Data/IOArray.idr) (Built on top of `Data.IORef`) and [`Data.Buffer`](https://github.com/chrrasmussen/Idris2-Erlang/blob/ff9499539d41c1e659a814895d7b02355b759d02/idris2/libs/base/Data/Buffer.idr) are all abstractions that provide mutability. Implementing them in Erlang turns out to be not so easy (to me, at least)....
> Looking at the workflow checks, it seems like the Nix workflow does not run the tests. Could you possibly add a step that runs `make bootstrap-test` as well? _Originally...
I noticed that I have forgot to add the `putChar` and `getChar` primitives. They are available in the `Prelude.IO` module as `%foreign` primitives: https://github.com/chrrasmussen/Idris2-Erlang/blob/master/idris2/libs/prelude/Prelude/IO.idr#L63-L66 The implementation would go here: https://github.com/chrrasmussen/Idris2-Erlang/blob/master/idris2/src/Compiler/Erlang/Codegen/NamedCExpToErlExpr.idr#L492-L498,...
The generated Erlang code is not optimal in terms of performance. As a comparison: - Running the Idris 2 compiler on Erlang and compiling the Idris 2 codebase takes about...
The Erlang code generator include some changes to the Idris 2 compiler that need to be removed or upstreamed in order for the code generator to become standalone. The biggest...
Thanks!
I'm very interested in this. Somewhere, I have a totally bitrotten attempt at a Core Erlang backend for Idris 1.x, but this seems much more promising. Realistically, I probably only...
Is there interest in including this codegen in the Pack package collection? If so, I'd be open to making the PR adding it to the collection and seeing if it...
