Code Generation Targets¶
Idris has been designed such that the compiler can generate code for
different backends upon request. By default
Idris generates a
However, there are third-party code generators out there. Below we
describe some of these backends and how you can use them when
Idris code. If you want to write your own codegen for your language there is a stub project on GitHub that can help point you in the right direction.
The default target of Idris is C. In order to view the generated C code, compile via:
$ idris hello.idr -S -o hello.c
To generate code that is tailored for running in the browser issue the following command:
java -jar compiler.jar --compilation_level ADVANCED_OPTIMIZATIONS --js hello.js
$ idris --codegen node hello.idr -o hello $ ./hello Hello world
These are third-party code generations and may have bit-rotted or do not work with current versions of Idris. Please speak to the project’s maintainers if there are any problems.
CIL (.NET, Mono, Unity)¶
idris --codegen cil Main.idr -o HelloWorld.exe \ && mono HelloWorld.exe
The resulting assemblies can also be used with .NET or Unity.
idris hello.idr --codegen java -o hello.jar
Note: The resulting .jar is automatically prefixed by a header including an .sh script to allow executing it directly.