We provide an implementation of a subset of the R6RS Formal semantics.
First, install Coq. I used Coq 8.10 - newer versions are likely to work but untested. I recommend using opam for installation, as it is quite simple (and required for the next step).
Then, install the Metalib library in coq/metalib (Note: You may have to change the Coq version in metalib's makefile to correspond to the version of Coq you are using)
Next, create a makefile: coq_makefile -f _CoqProject *.v -o Makefile
Finally, call make to build the project
You can step through some of the examples in Examples.v to see how the semantic model works
We provide a testing framework for showing that the convert-assignments pass is correct for given programs
Install Racket. I recommend using the DrRacket IDE. I used Racket 8.0 when writing this framework.
Run test-transform.rkt to run the test suite
To test a specific program, call test-ca on it to test for one step,
or full-test-ca to test for 10 steps or until the program terminates
You can modify the definition of full-test-ca to change the step limit.
