Skip to content

melted/idris-chez

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

65 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

idris-chez

A ChezScheme backend for Idris

Usage

A Chez Scheme installation is a prerequisite to use idris-chez. It uses Chez Scheme extensions and would need to be modified to work with other Scheme flavors.

Run cabal install to install idris-chez.

Then idris-chez is invoked when running idris with --codegen chez like

idris --codegen chez example.idr -o example.ss

scheme --script example.ss

Files are compiled only to Scheme source for now, if desired they can be built into object files using Chez Scheme.

Features

  • Speed!
  • C FFI
  • A compatibility layer for the base libraries dependence on the C rts. for example, the C calls in Prelude.Files are substituted by Scheme calls.
  • Chez Scheme provides excellent stack handling and garbage collection

To do

  • Scheme FFI (In progress!)
  • Map some common but non-primitive Idris types like lists and bools to the corresponding primitives in Scheme.
  • Stabilization

Directives

%lib chez "<shared lib>"

In the chez backend %lib names dynamic libs that should be loaded at startup. The functions in that lib will then be available for FFI. See test/samples/loadshared.idr for an example.

%include chez "<any scheme code>"

In the chez backend %include includes arbitrary Scheme code into the resulting program. Chez Scheme's load or import can be used in an %include directive to actually include code from another file.

Benchmarks

Let's run the pidigits benchmark from idris' benchmarks folder!

idris-chez

$ time ./pidigits.ss 5000 > /dev/null

real    0m3.219s
user    0m0.000s
sys     0m0.030s

C backend

$ time ./pidigits.exe 5000 > /dev/null

real    0m10.005s
user    0m0.000s
sys     0m0.000s

Lets try 10000....

idris-chez

$ time ./pidigits.ss 10000 > /dev/null

real    0m12.900s
user    0m0.030s
sys     0m0.000s

C backend

$ time ./pidigits.exe 10000 > /dev/null
Segmentation fault

real    1m17.884s
user    0m0.016s
sys     0m0.000s

Ooops....

About

An idris backend compiling to chez scheme

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published