Thorin 1.9.0
The Higher ORder INtermediate representation
|
Support | |
License | |
Requirements | |
Tests |
Thorin is an extensible compiler intermediate representation that is based upon the Calculus of Constructions (CoC). This means:
In contrast to other CoC-based program representations such as Coq or Lean, Thorin is not a theorem prover but focuses on generating efficient code. For this reason, Thorin explicitly features mutable state and models imperative control flow with continuation-passing style (CPS).
You can use Thorin either via it's C++-API or the command-line utility.
If you have a GitHub account setup with SSH, just do this:
Otherwise, clone via HTTPS:
Then, build with:
For a Release
build simply use -DCMAKE_BUILD_TYPE=Release
.
If you want to install Thorin, specify an install prefix and build the target install
:
CMake Switch | Options | Default | Comment |
---|---|---|---|
CMAKE_BUILD_TYPE | Debug | Release | RelWithDebInfo | Debug | Build type. |
CMAKE_INSTALL_PREFIX | /usr/local | Install prefix. | |
THORIN_BUILD_DOCS | ON | OFF | OFF | If ON , Thorin will build the documentation (requires Doxygen). |
THORIN_BUILD_EXAMPLES | ON | OFF | OFF | If ON , Thorin will build the examples. |
THORIN_BUILD_TESTING | ON | OFF | OFF | If ON , Thorin will build all of Thorin's own tests. |
THORIN_ENABLE_CHECKS | ON | OFF | ON | If ON , enables expensive runtime checks (requires CMAKE_BUILD_TYPE=Debug ). |
In addition to the provided submodules: