module FreeC.Backend.Coq.Converter.Module where
import Control.Monad.Extra ( concatMapM )
import Data.List.Extra ( concatUnzip )
import qualified Data.Set as Set
import qualified FreeC.Backend.Coq.Base as Coq.Base
import FreeC.Backend.Coq.Converter.FuncDecl
import FreeC.Backend.Coq.Converter.TypeDecl
import qualified FreeC.Backend.Coq.Syntax as Coq
import FreeC.Environment.Entry
( EnvEntry(ConEntry), entryName )
import FreeC.Environment.LookupOrFail
import FreeC.Environment.ModuleInterface
import FreeC.IR.DependencyGraph
import FreeC.IR.SrcSpan
import qualified FreeC.IR.Syntax as IR
import FreeC.Monad.Converter
import FreeC.Pretty
convertModule :: IR.Module -> Converter [Coq.Sentence]
convertModule haskellAst = do
imports' <- convertImportDecls (IR.modImports haskellAst)
decls' <- convertDecls (IR.modTypeDecls haskellAst)
(IR.modFuncDecls haskellAst)
return (Coq.comment ("module " ++ IR.modName haskellAst) : imports' ++ decls')
convertDecls :: [IR.TypeDecl] -> [IR.FuncDecl] -> Converter [Coq.Sentence]
convertDecls typeDecls funcDecls = do
typeDecls' <- convertTypeDecls typeDecls
funcDecls' <- convertFuncDecls funcDecls
return (typeDecls' ++ funcDecls')
convertTypeDecls :: [IR.TypeDecl] -> Converter [Coq.Sentence]
convertTypeDecls typeDecls = do
let components = typeDependencyComponents typeDecls
(sentences, qualSmartCons)
<- concatUnzip <$> mapM convertTypeComponent components
let
qualNotModule = if null qualSmartCons
then []
else [ Coq.comment "Qualified smart constructors"
, Coq.LocalModuleSentence
$ Coq.LocalModule Coq.Base.qualifiedSmartConstructorModule
qualSmartCons
]
return $ sentences ++ qualNotModule
convertImportDecls :: [IR.ImportDecl] -> Converter [Coq.Sentence]
convertImportDecls imports = do
imports' <- concatMapM convertImportDecl imports
return (Coq.Base.imports : imports')
convertImportDecl :: IR.ImportDecl -> Converter [Coq.Sentence]
convertImportDecl (IR.ImportDecl srcSpan modName) = do
iface <- lookupAvailableModuleOrFail srcSpan modName
generateImport (interfaceLibName iface) modName
generateImport :: Coq.ModuleIdent -> IR.ModName -> Converter [Coq.Sentence]
generateImport libName modName = do
iface <- lookupAvailableModuleOrFail NoSrcSpan modName
return (mkImportSentences (Coq.ident (showPretty modName)) iface)
where
mkImportSentences :: Coq.ModuleIdent -> ModuleInterface -> [Coq.Sentence]
mkImportSentences modIdent modInterface
| libName
== Coq.Base.baseLibName = [Coq.requireImportFrom libName [modIdent]]
| otherwise = Coq.requireFrom libName [modIdent]
: ([Coq.moduleExport
[ Coq.access libName
$ Coq.access modIdent Coq.Base.qualifiedSmartConstructorModule
]
| hasConstructor modInterface
])
hasConstructor :: ModuleInterface -> Bool
hasConstructor interface
= let modName' = interfaceModName interface
entries = interfaceEntries interface
in not (Set.null (Set.filter (isLocalConstructor modName') entries))
isLocalConstructor :: IR.ModName -> EnvEntry -> Bool
isLocalConstructor modName' ConEntry { entryName = IR.Qual modName'' _ }
= modName'' == modName'
isLocalConstructor _ _ = False