agda2scheme
agda2scheme copied to clipboard
jespercockx
Compiler backend for generating Scheme code
Hello, In test directory there are golden tests, but there is no code that actually illustrate how to run them. Since this repo works as example how to build backend,...
Here is how I am running my benchmarks so far: ``` cd test agda2scheme --lazy Triples.agda echo '(display (test1)) (display "\n")' >> Triples.ss echo '(compile-file "Triples.ss")' | chezscheme -q time...
It would be cool if we could detect automatically types that are sufficiently like natural numbers or integers, and represent them using actual integers in the compiled code. As a...
Currently compiling code with the `--lazy` flag incurs a quite heavy performance overhead (e.g. the slowdown is over 10x on Triples.agda). If we could analyze which arguments are always used...
Currently constructors always store a tag, even when there is only a single option. As a stretch goal, we could even skip the constructor tag if there are several constructors,...
Arrays give constant-time access to their elements so they might be more efficient, especially for record types with many fields. We could also consider using arrays to represent argument lists...
Instead of matching, we could instead just project out the fields of the record directly.
The following built-in types of Agda are not yet supported: - [ ] Integers - [ ] Floats - [ ] Chars - [ ] Strings - [ ] Word64...