A tiny discrete language.
bin/
defines the binary. You shouldn't need to change anything here.lib
: contains the core of the codebasesyntax.ml
: defines the external user-facing grammar, which is the parser targetcore_grammar.ml
: contains an internal grammar that is desugared from the external grammar. This is the main grammar that you will be interacting with. It has a functionsubst
that lets you substitute expressions in for free variables in a superexpression.lexer.mll
andparser.mly
: these define the parser and lexer for the project using menhir. You do not need to edit these files for the project.enumerate.ml
is where you'll implement the exhaustive enumeration big-step semantics.kc.ml
is where you'll implement the Boolean compilation semantics.util.ml
contains various convenience utilities used across different parts of the library
programs/
: contains sample programs for you to tinker with.tests/
: contains the test suite.
Make sure you have OCaml (<5.0.0), opam, and dune. They can be all installed through a package manager of your choice.
opam dependencies: menhir
, ounit
, qcheck
, bignum
, core
, core_unix
, rsdd
After cloning, cd
into the folder and run opam install . --deps-only
to install dependencies.
Then run dune build
. If it gives errors on missing packages, install them using opam install $PACKAGE_NAME
.
After you build using dune build
, an executable will be available under _build/
. Alternatively, you can also do dune exec -- disc $FILE $FLAGS
.
Try it out with some of the sample programs in the programs
folder, with no flags raised. It should say that the program parsed, but no inference strategy was selected.
After you implement both inference strategies, you can compare values using dune test
.
The top-level syntax is in monadic-style:
e ::=
| x <- e; e
| observe e; e
| flip q // q is a rational value
| if e then e else e
| return e
| true | false
| e && e | e || e | ! e |
| ( e )
p ::= e