This tool was implemented as part of a bachelor thesis (by Malte Clement at Kiel University) and should be considered as a alpha version of a prototype.
This is a tool to translate different language features of Haskell into simpler expressions.
-
It translates pattern matching on left hand sides into explicit pattern matching on right sides using Wadlers Algorithm for compiling pattern matching.
-
Guards are transformed into
case
-expression using their semantics as described in the Haskell-report. -
Partially defined functions are completed such that pattern mismatches do not occur.
- The thesis that describes the transformations can be found in the
LaTeX
-directory.
The repository consists of two directories
-
src
contains the source code of the projectsrc/test
contains modules that have been translated to test certain featuressrc/Examples
contains two modules which can be used for local debugging with theApplication.hs
module containing atest
-function to work with these local modules.
-
Examples
contains some examples that have been transformed by hand using Wadler's algorithm.Additionally, it contains some special examples that were used to test the haskell-to-coq-compiler
The tool is written in Haskell and uses Cabal to manage the dependencies. To build it, the GHC and Cabal are required. The tool has been tested with GHC, version 8.4.3 and Cabal, version 2.2.0.1.
In order to install the library and the executable navigate to the root directory of the project and run
cabal install CodeTransformation
To transform a Haskell module navigate to ./dist/build
and run
CodeTransformation -I [InputFile]
The generated code is printed to the console. If you want to specify the output directory use the -o
flag.
For more information on the different flags you can use the -h
flag.