free-compiler-0.3.0.0: A Haskell to Coq compiler.

Safe HaskellNone
LanguageHaskell2010

FreeC.Backend.Agda.Converter

Description

This module exports functions for generating Agda that uses the Free monad from out intermediate representation.

Synopsis

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