| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FreeC.Backend.Coq.Converter.Module
Description
This module contains functions for converting Haskell modules to Coq.
Synopsis
- convertModule :: Module -> Converter [Sentence]
- convertDecls :: [TypeDecl] -> [FuncDecl] -> Converter [Sentence]
- convertTypeDecls :: [TypeDecl] -> Converter [Sentence]
- convertImportDecls :: [ImportDecl] -> Converter [Sentence]
- convertImportDecl :: ImportDecl -> Converter [Sentence]
- generateImport :: ModuleIdent -> ModName -> Converter [Sentence]
Documentation
convertModule :: Module -> Converter [Sentence] Source #
Converts an IR module to Gallina sentences.
convertDecls :: [TypeDecl] -> [FuncDecl] -> Converter [Sentence] Source #
Converts the given declarations of an IR module.
convertTypeDecls :: [TypeDecl] -> Converter [Sentence] Source #
Converts the given data type or type synonym declarations.
convertImportDecls :: [ImportDecl] -> Converter [Sentence] Source #
Converts the given import declarations to Coq.
convertImportDecl :: ImportDecl -> Converter [Sentence] Source #
Convert an import declaration.
generateImport :: ModuleIdent -> ModName -> Converter [Sentence] Source #
Generates a Coq import sentence for the module with the given name from the given library.
Modules from the base library are imported via From Base Require Import
sentences. Other external modules are imported via From … Require
sentences, which means that references to these modules' contents must
be qualified in the code. For such an external module there is also an
Export … .QualifiedSmartConstructorModule sentence added if necessary,
to give access to the notations for qualified smart constructors.