A compiler for the monadic translation of Haskell programs to Coq or Agda that uses the Free monad as presented by Dylus et al. to model partiality and other ambient effects.
Sharing is modeled in Coq as an effect based on the master's thesis by Niels Bunkenburg.
This compiler was originally developed as part of a bachelor's thesis. The compiler has been extended with additional features and its architecture changed compared to the version presented in the thesis, but the explanation of the monadic translation in the thesis is still mostly up to date. Read the changelog for more information on what has changed since the initial release.
The compiler's source code is documented using Haddock. The documentation of each component of the compiler is automatically built by our CI pipeline and deployed at the links below.
- Documentation for modules in
src/exe - Documentation for modules in
src/lib - Documentation for modules in
src/test
Additional documentation can be found in the doc/ directory.
This repository is structured as follows.
-
./The root directory of the Free Compiler is home to important Markdown documents and central configuration files (e.g., Cabal configuration files).
-
./.githubThis directory contains GitHub-related files such as issue and pull request templates as well as the configuration of the CI pipeline.
-
./base/agdaThis directory contains the Agda base library of the compiler. The Agda base library is a collection of Agda files that are required by the generated code. This includes the definition of the
Freemonad as well as thePreludeimplementation. -
./base/coqThis directory contains the Coq base library of the compiler. The Coq base library is a collection of Coq files that are required by the generated code. This includes the definition of the
Freemonad as well as thePreludeandTest.QuickCheckimplementation. -
./docThis directory contains Markdown documentation of the compiler. The documentation in this directory is mainly intended for users and not so much for developers of the compiler. Documentation for more technical aspects such as module interfaces and the intermediate representation can also be found here.
-
./exampleThis directory contains examples for Haskell modules that can (or cannot) be compiled with the Free Compiler. Examples that don't compile are commented out. If multiple examples belong together, they are placed in a common subdirectory. There are two
.gitignored subdirectories,./example/transformedand./example/generated../example/generatedis intended to be used as the--outputdirectory of the compiler when testing the compiler../example/transformedis used to dump the output of the pattern matching compiler.
There are also Coq files (
.vfiles) for proofs about translated examples. In contrast to the Coq files placed by the compiler into./example/generated, they are not.gitignored. The./example/_CoqProjectfile configures Coq such that the versioned Coq files can discover the generated Coq code and the base library. -
./imgThis directory contains images that are embedded into the README or other Markdown documents.
-
./srcThis directory contains the Haskell source code of the compiler. There are three subdirectories.
./src/execontains the code for the command line interface../src/libcontains the code for the actual compiler../src/testcontains test cases for the modules located in./src/lib.- By convention modules containing test cases have the same name as the module they are testing but
Testsis appended to the module name. For example, the moduleFreeC.Pass.TypeInferencePassTestscontains test cases for theFreeC.Pass.TypeInferencePassmodule. - For tests of modules with a common prefix, there is often a
Tests.hsfile that simply invokes all tests of all modules with that prefix. For example, there is noFreeC.IRmodule but aFreeC.IR.Testsmodule that runs all tests for modules starting with theFreeC.IRprefix (e.g.,FreeC.IR.ReferenceTests,FreeC.IR.SubstTests, etc.) - The
Specmodule serves as an entry point or "main module" for the unit tests. It invokes the unit tests in the other test modules.
- By convention modules containing test cases have the same name as the module they are testing but
Except for the main modules
MainandSpec, the names of all modules that belong to the Free Compiler start with theFreeCprefix. Modules are organized hierarchically based on their function. Common prefixes are listed below.FreeC.Backendcontains modules that are concerned with the translation from the intermediate representation to a target language.FreeC.Frontendcontains modules that are concerned with the translation of an input language to the intermediate representation. This includes a front end for the intermediate representation itself.FreeC.IRcontains modules that define data types and operations for the intermediate representation such as the AST or commonly used operations on the AST.FreeC.LiftedIRcontains modules that define data types and operations for the lifted intermediate representation such as the AST or commonly used operations on the AST. The lifted intermediate representation is used store the transformed program before Coq or Agda code is generated.FreeC.Monadcontains modules that define monads that are used throughout the compiler (e.g., for error reporting or stateful operations).FreeC.Monad.Classcontains type classes for monads.FreeC.Passcontains one module for each compiler pass. A compiler pass is a transformation on the intermediate representation and environment.FreeC.Testcontains modules for writing unit tests.FreeC.Utilcontains modules for utility functions.
Additionally, if there is a module
FreeC.X, related modules start with the prefixFreeC.X. -
./toolThis directory contains Bash scripts for common actions that need to be performed during development. The scripts are intended to be executed from the root directory of this repository.
./tool/run.sh --help
However, most scripts will make sure that they change into the correct working directory beforehand. For example, the compiler runs in
/path/to/free-compilerwhen invoked using the following command./path/to/free-compiler/tool/run.sh ./example/Data/List.hs
As a consequence,
./example/Data/List.hsrefers to/path/to/free-compiler/example/Data/List.hsand not to$(pwd)/example/Data/List.hsin the example above.If there are other directories named
toolin this repository, the contained scripts are intended to be executed from the directory containing thetooldirectory by convention.
The Free Compiler is written in Haskell and uses Cabal to manage its dependencies. To build the compiler, the GHC and Cabal are required. To use the Coq code generated by our compiler, the Coq proof assistant must be installed. The compiler has been tested with the following software versions on a Debian based operating system.
- GHC, version 8.6.5
- Cabal, version 3.4.0.0
- Coq, versions 8.10 through 8.12
- Agda, versions 2.6.1
- Agda Standard Library, version 1.3
In order to use the Coq code generated by the Free Compiler, the Coq base library that accompanies the Free Compiler needs to be compiled first. Make sure to compile the base library before installing the compiler. We provide a shell script for the compilation of Coq files. To compile the base library with that shell script, run the following command in the root directory of the compiler.
./tool/compile-coq.sh base/coqNote: If you add or remove files from the
base/coqlibrary (or any other directory that contains Coq code that you wish to compile using the script above), the automatically generated Makefile needs to be updated. For this purpose the script provides the command line option--recompile../tool/compile-coq.sh --recompile base/coq
In order to use the Agda code generated by the Free Compiler, the Agda base library and its dependencies have to be installed.
- Install the Agda Standard Library according to its installation instructions.
- Register the base library by adding the path to
base/agda/base.agda-libto$HOME/.agda/libraries.
First, make sure that the Cabal package lists are up to date by running the following command.
cabal new-updateTo build and install the compiler and its dependencies, change into the compiler’s root directory and run the following command.
cabal new-install freecNote: Due to the dependency on the Agda compiler as a library, the first compilation of the Free Compiler can take over half an hour.
The command above copies the base library and the compiler’s executable to Cabal’s installation directory and creates a symbolic link to the executable in
~/.cabal/bin.
To test whether the installation was successful, make sure that ~/.cabal/bin is in your PATH environment variable and run the following command.
freec --versionIf you want to run the compiler without installing it on your machine (e.g., for debugging purposes), execute the following command in the root directory of the compiler instead of the freec command.
cabal new-run freec -- [options...] <input-files...>The two dashes are needed to separate the arguments to pass to the compiler from Cabal’s arguments.
Alternatively, you can use the ./tool/run.sh bash script.
./tool/run.sh [options...] <input-files...>Besides invoking Cabal and forwarding its command line arguments to the compiler, the script also sets the -Wwarn flag of the GHC automatically.
This overwrites the -Werror flag of the GHC that is set in addition to the -Wall flag by default.
The default configuration causes compilation to fail when there are unhandled warnings in the source code.
As a result, the CI pipeline rejects commits that introduce such warnings.
While it is important that no warnings are reported in a production setting, fatal warnings can be disrupting when debugging.
Thus, we recommend using the ./tool/run.sh script during development and running ./tool/full-test.sh (which uses the default settings) once before pushing your local changes.
During development you may want to test or debug your code interactively. One option is to use one of the following Cabal commands to open a GHCi prompt.
cabal new-repl freec
cabal new-repl freec-internalUnfortunately, it is not possible to load both freec (i.e., all modules in ./src/exe) and freec-internal (i.e., all modules in ./src/lib) in interpreted mode at the same time.
This restriction is sometimes inconvenient, since you would have to restart GHCi whenever you make changes to the freec-internal component when the freec component is loaded.
Furthermore it is not possible to set a break point across component boundaries.
Thus, we provide the following bash script to open a GHCi prompt.
./tool/repl.shThe command invokes GHCi such that all modules from the src directory are loaded in interpreted mode and sets the context for expression evaluation to the Main module.
Use the :m command to switch to another module.
To compile a Haskell module, pass the file name of the module to freec.
For example, to compile the examples from the Data.List module, run the following command.
freec ./example/Data/List.hsIn order to compile multiple modules which import each other, multiple file names can be passed as an argument.
freec ./example/Data/List.hs ./example/Data/Function.hsBoth commands above print the generated Coq code directly to the console.
See the --output option below for how to write the generated Coq code into files instead.
By default, generated Coq code is printed to the console.
To write to a file instead, specify an output directory using the --output option.
A file X/Y/Z.v is placed into the output directory for every module X.Y.Z that is compiled.
For example, the following command creates the files example/generated/Data/List.v and example/generated/Data/Function.v
freec -o ./example/generated ./example/Data/*.hsIn addition to the .v files, .json files are generated as well.
The JSON files contain the module interfaces for the translated modules.
The module interface files can be used to import modules that have been translated already without specifying them on the command line.
For example, if Data.List and Data.Functor have been translated already, the ListFunctor example can be compiled on its own since its imports can be served from the module interface files.
freec -o ./example/generated ./example/ListFunctor.hsThe compiler searches for module interfaces in the output directory (see --output option) and the current working directory by default.
If you want to compile modules that import files that have been written to a different output directory, you can use the --import command line option to specify additional paths to search for module interfaces in.
For example, if Data.List and Data.Functor have been translated already and their output has been written to ./examples/generated, you can translate ListFunctor and print its output to the console as follows.
freec -i ./example/generated ./example/ListFunctor.hsTo add multiple import paths just add one --import option for each path.
There can be arbitrarily many import paths and the --import and --output options can be mixed.
./tool/run.sh -o <dir0> -i <dir1> -i <dir2> … <input-files...>In the example above, the compiler would search for a module interface file first in the current working directory and then in the directories in the order they have been specified on the command line (i.e., first ., then <dir0>, then <dir1>, then <dir2> and so on).
Predefined data types and operations are not built directly into the compiler but are part of the base library that accompanies the compiler. To load module dependencies from the base library, the compiler uses the same mechanism, i.e., module interface files, which is used to load module dependencies. In contrast to automatically generated module interface files, the base library does not use the JSON file format. Since the module interfaces of the base library are maintained manually, the more user-friendly format TOML is used.
The module interface file format is documented in doc/ModuleInterfaceFileFormat.md.
In order for the compiler to locate the Prelude.toml module interface file, the location of the base library must be known.
If the compiler is installed as described above or executed using cabal, it will usually be able to locate the base library automatically.
Otherwise, it may be necessary to tell the compiler where the base library can be found using the --base-library option.
freec -b ./base ./example/Data/List.hsWhen an output directory has been specified using the --output option and the output directory does not contain a _CoqProject file, it is created automatically.
The _CoqProject file tells Coq where to find the compiler’s base library and assigns the logical name Generated to the directory that contains the generated Coq code.
The file has the following format where <base-library> is the path to the base library (see --base-library command line option).
-R <base-library> Base
-R . Generated
The logical names Base and Generated are used in the generated import sentences.
For example, a generated file could contain the following lines.
From Base Require Import Prelude.
From Generated Require Export Data.List.You can safely edit the _CoqProject file or supply your own configuration as long as Coq is still able to locate the .v files under their logical prefixes.
The compiler will not overwrite your changes since the _CoqProject file is only written to if it does not exist.
If you don't want the _CoqProject file to be generated at all, you can add the --no-coq-project flag.
However, note that you may not be able to compile the generated Coq code if the _CoqProject file is missing.
When an output directory has been specified using the --output option and the output directory does not contain a .agda-lib file, it is created automatically.
The name of the .agda-lib file is the same as the output directory.
The .agda-lib file tells Agda that generated code depends on the compilers base library and the Agda standard library.
You can safely edit the .agda-lib file or supply your own configuration as long as the dependencies remain intact.
The compiler will not overwrite your changes since the .agda-lib file is only written to if it does not exist.
If you don't want the .agda-lib file to be generated at all, you can add the --no-agda-lib flag.
However, note that you may not be able to compile the generated Agda code if the .agda-lib file is missing.
To check which version of the Free Compiler is currently installed on your system, run the following command.
freec --versionTo see a list of all available command line options, use the following command.
freec --helpBy default the compiler translates from Haskell to Coq.
The --from and --to options select a different frontend and backend respectively.
Currently the haskell frontend and the coq and agda backend are available.
For debugging purposes there also exists a ir frontend and backend that parses or prints the intermediate representation used by the compiler respectively.
For example, to print the intermediate representation of a Haskell file, run the following command.
freec --from haskell --to ir ./example/Data/List.hsThe main goal for the translation of Haskell code to Coq is to prove properties of the Haskell program in Coq. In order to do so, we have to formulate the properties to prove first. Due to the overhead involved with our translation, stating propositions in Coq directly is very tedious. Therefore, we provide a mechanism for deriving Coq properties from QuickCheck properties. This allows us to state the proposition in Haskell instead of Coq.
Consult doc/ProvingQuickCheckProperties.md for more details and examples.
By default the compiler does support a limited subset of the Haskell programming language only.
There is experimental support to relax some of those restrictions.
Add the --transform-pattern-matching command line option to automatically transform the input modules using a pattern matching compiler library for haskell-src-exts before they are translated by our compiler.
For example, the PatternMatching example can be translated as follows.
freec --transform-pattern-matching ./example/PatternMatching.hsConsult doc/ExperimentalFeatures/PatternMatchingCompilation.md for more details and examples.
Feature requests, enhancement proposals, bug reports, pull requests and all other contributions are welcome! Have a look at our contributing guidelines for more information on how to contribute.
The Free Compiler is licensed under The 3-Clause BSD License. See the LICENSE file for details.