Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module exports functions for generating Agda that uses the Free
monad from out intermediate representation.
Synopsis
- convertModule :: Module -> Converter Declaration
- convertFuncDecls :: DependencyComponent FuncDecl -> Converter [Declaration]
- convertTypeDecls :: DependencyComponent TypeDecl -> Converter [Declaration]
Documentation
convertModule :: Module -> Converter Declaration Source #
Converts an IR module to an Agda declaration.
convertFuncDecls :: DependencyComponent FuncDecl -> Converter [Declaration] Source #
Converts a strongly connected component of the function dependency graph. TODO: Handle mutually recursive functions.
convertTypeDecls :: DependencyComponent TypeDecl -> Converter [Declaration] Source #
Converts a strongly connected component of the type dependency graph. TODO: handle mutual recursive types