module FreeC.Backend.Coq.Converter.FuncDecl.Rec.WithSections
( convertRecFuncDeclsWithSection
) where
import Control.Monad
( forM, mapAndUnzipM, zipWithM )
import Control.Monad.Extra
( concatMapM, mapMaybeM )
import Data.List
( (\\), elemIndex, intercalate, nub )
import Data.Map.Strict ( Map )
import qualified Data.Map.Strict as Map
import Data.Maybe
( catMaybes, fromJust, fromMaybe, mapMaybe, maybeToList )
import qualified Data.Set as Set
import FreeC.Backend.Coq.Analysis.ConstantArguments
import qualified FreeC.Backend.Coq.Base as Coq.Base
import FreeC.Backend.Coq.Converter.Free
import FreeC.Backend.Coq.Converter.FuncDecl.Common
import FreeC.Backend.Coq.Converter.FuncDecl.Rec.WithHelpers
import FreeC.Backend.Coq.Converter.Type
import qualified FreeC.Backend.Coq.Syntax as Coq
import FreeC.Environment
import FreeC.Environment.Entry
import FreeC.Environment.Fresh
import FreeC.Environment.LookupOrFail
import FreeC.Environment.Renamer
import FreeC.IR.Reference
( freeTypeVarSet, freeVarSet )
import FreeC.IR.SrcSpan
import FreeC.IR.Subst
import qualified FreeC.IR.Syntax as IR
import FreeC.IR.Unification
import FreeC.Monad.Converter
import FreeC.Monad.Reporter
import FreeC.Pretty
convertRecFuncDeclsWithSection
:: [ConstArg] -> [IR.FuncDecl] -> Converter [Coq.Sentence]
convertRecFuncDeclsWithSection constArgs decls = do
(renamedDecls, nameMap) <- renameFuncDecls decls
let renamedConstArgs = map (renameConstArg nameMap) constArgs
renamedTypeArgs = map (map IR.typeVarDeclIdent . IR.funcDeclTypeArgs)
renamedDecls
(argTypeMaps, returnTypeMaps)
<- mapAndUnzipM argAndReturnTypeMaps renamedDecls
let argTypeMap = Map.unions argTypeMaps
returnTypeMap = Map.unions returnTypeMaps
(constArgTypes, mgus) <- mapAndUnzipM (lookupConstArgType argTypeMap)
renamedConstArgs
let mgu = composeSubsts mgus
typeArgIdents = Set.toList (Set.unions (map freeTypeVarSet constArgTypes))
let renamedDecls' = applySubst mgu renamedDecls
sectionDecls <- mapM (removeConstArgsFromFuncDecl renamedConstArgs)
renamedDecls'
let isConstArgUsed = map (flip any sectionDecls . isConstArgUsedBy)
constArgs
usedConstArgTypes
= map snd $ filter fst $ zip isConstArgUsed constArgTypes
isTypeArgUsed v = any (Set.member v . freeTypeVarSet) usedConstArgTypes
usedTypeArgIdents = filter isTypeArgUsed typeArgIdents
removedConstTypeArgs <- mapM
(updateTypeSig mgu usedTypeArgIdents argTypeMap returnTypeMap) sectionDecls
sectionDecls' <- mapM (removeConstTypeArgsFromFuncDecl removedConstTypeArgs)
sectionDecls
section <- localEnv $ do
let funcNames = map IR.funcDeclQName decls
funcIdents = mapMaybe IR.identFromQName funcNames
sectionIdent <- freshCoqIdent (intercalate "_" ("section" : funcIdents))
maybeTypeArgSentence <- generateConstTypeArgSentence usedTypeArgIdents
usedTypeArgIdents' <- mapMaybeM
(inEnv . lookupIdent IR.TypeScope . IR.UnQual . IR.Ident)
usedTypeArgIdents
effects <- nub <$> concatMapM (inEnv . lookupEffects) funcNames
let typedBinders = concatMap
(flip Coq.Base.selectTypedBinders usedTypeArgIdents') effects
varSentences <- zipWithM generateConstArgVariable
(map fst $ filter snd $ zip renamedConstArgs isConstArgUsed)
(map fst $ filter snd $ zip constArgTypes isConstArgUsed)
(helperDecls', mainDecls') <- convertRecFuncDeclsWithHelpers' sectionDecls'
return
(Coq.SectionSentence
(Coq.Section (Coq.ident sectionIdent)
(Coq.comment ("Constant arguments for " ++ intercalate ", " funcIdents)
: genericArgVariables
++ maybeToList maybeTypeArgSentence
++ map Coq.context typedBinders
++ varSentences
++ Coq.comment ("Helper functions for " ++ intercalate ", " funcIdents)
: helperDecls'
++ Coq.comment ("Main functions for " ++ intercalate ", " funcIdents)
: mainDecls')))
interfaceDecls'
<- zipWithM (generateInterfaceDecl constArgs isConstArgUsed nameMap mgu
usedTypeArgIdents) renamedTypeArgs decls
return (section : interfaceDecls')
renameFuncDecls
:: [IR.FuncDecl] -> Converter ([IR.FuncDecl], Map IR.QName IR.QName)
renameFuncDecls decls = do
let names = map IR.funcDeclQName decls
names' <- mapM freshHaskellQName names
let nameMap = Map.fromList (zip names names')
subst = composeSubsts $ zipWith mkVarSubst names names'
decls' <- forM decls
$ \(IR.FuncDecl srcSpan (IR.DeclIdent srcSpan' name) typeArgs args
maybeRetType rhs) -> do
let Just name' = Map.lookup name nameMap
let typeArgIdents = map IR.typeVarDeclIdent typeArgs
typeArgIdents' <- mapM freshHaskellIdent typeArgIdents
let typeArgs' = zipWith IR.TypeVarDecl
(map IR.typeVarDeclSrcSpan typeArgs) typeArgIdents'
typeVarSubst = composeSubsts
(zipWith mkTypeVarSubst typeArgIdents typeArgIdents')
args' = applySubst typeVarSubst args
maybeRetType' = applySubst typeVarSubst maybeRetType
entry <- lookupEntryOrFail srcSpan' IR.ValueScope name
_ <- renameAndAddEntry entry
{ entryName = name'
, entryTypeArgs = typeArgIdents'
, entryArgTypes = map (fromJust . IR.varPatType) args'
, entryReturnType = fromJust maybeRetType'
}
maybeDecArg <- inEnv $ lookupDecArg name
case maybeDecArg of
Just (decArgIndex, decArgIdent) ->
modifyEnv $ defineDecArg name' decArgIndex decArgIdent
Nothing -> return ()
let rhs' = applySubst typeVarSubst (applySubst subst rhs)
return (IR.FuncDecl srcSpan (IR.DeclIdent srcSpan' name') typeArgs' args'
maybeRetType' rhs')
return (decls', nameMap)
renameConstArg :: Map IR.QName IR.QName -> ConstArg -> ConstArg
renameConstArg nameMap constArg = constArg
{ constArgIdents = renameKeys (constArgIdents constArg)
, constArgIndicies = renameKeys (constArgIndicies constArg)
}
where
renameKeys :: Map IR.QName v -> Map IR.QName v
renameKeys = Map.mapKeys (fromJust . flip Map.lookup nameMap)
argAndReturnTypeMaps
:: IR.FuncDecl
-> Converter (Map (IR.QName, String) IR.Type, Map IR.QName IR.Type)
argAndReturnTypeMaps (IR.FuncDecl _ (IR.DeclIdent _ name) _ args maybeRetType _)
= return (argTypeMap, returnTypeMap)
where
argTypeMap = Map.fromList
[((name, IR.varPatIdent arg), argType)
| arg <- args
, argType <- maybeToList (IR.varPatType arg)
]
returnTypeMap
= Map.fromList [(name, retType) | retType <- maybeToList maybeRetType]
lookupConstArgType :: Map (IR.QName, String) IR.Type
-> ConstArg
-> Converter (IR.Type, Subst IR.Type)
lookupConstArgType argTypeMap constArg = do
let idents = Map.assocs (constArgIdents constArg)
types = mapMaybe (flip Map.lookup argTypeMap) idents
srcSpan = IR.typeSrcSpan (head types)
mgu <- unifyAllOrFail srcSpan types
let constArgType = applySubst mgu (head types)
return (constArgType, mgu)
isConstArgUsedBy :: ConstArg -> IR.FuncDecl -> Bool
isConstArgUsedBy constArg funcDecl = IR.UnQual
(IR.Ident (constArgFreshIdent constArg))
`Set.member` freeVarSet (IR.funcDeclRhs funcDecl)
generateConstTypeArgSentence
:: [IR.TypeVarIdent] -> Converter (Maybe Coq.Sentence)
generateConstTypeArgSentence typeVarIdents
| null typeVarIdents = return Nothing
| otherwise = do
let srcSpans = repeat NoSrcSpan
typeVarIdents' <- zipWithM renameAndDefineTypeVar srcSpans typeVarIdents
return (Just (Coq.variable typeVarIdents' Coq.sortType))
generateConstArgVariable :: ConstArg -> IR.Type -> Converter Coq.Sentence
generateConstArgVariable constArg constArgType = do
let ident = constArgFreshIdent constArg
constArgType' <- convertType constArgType
ident' <- renameAndDefineVar NoSrcSpan False ident (Just constArgType)
return (Coq.variable [ident'] constArgType')
removeConstArgsFromFuncDecl
:: [ConstArg] -> IR.FuncDecl -> Converter IR.FuncDecl
removeConstArgsFromFuncDecl constArgs
(IR.FuncDecl srcSpan declIdent typeArgs args maybeRetType rhs) = do
let name = IR.declIdentName declIdent
removedArgs = fromJust
$ Map.lookup name
$ Map.unionsWith (++)
$ map (Map.map return . constArgIdents) constArgs
freshArgs = map constArgFreshIdent constArgs
args'
= [arg | arg <- args, IR.varPatIdent arg `notElem` removedArgs]
subst = composeSubsts
[mkVarSubst (IR.UnQual (IR.Ident removedArg))
(IR.UnQual (IR.Ident freshArg))
| (removedArg, freshArg) <- zip removedArgs freshArgs
]
rhs' <- removeConstArgsFromExpr constArgs (applySubst subst rhs)
return (IR.FuncDecl srcSpan declIdent typeArgs args' maybeRetType rhs')
removeConstArgsFromExpr :: [ConstArg] -> IR.Expr -> Converter IR.Expr
removeConstArgsFromExpr constArgs rootExpr = do
(rootExpr', []) <- removeConstArgsFromExpr' rootExpr
return rootExpr'
where
constArgIndicesMap :: Map IR.QName [Int]
constArgIndicesMap = Map.unionsWith (++)
$ map (Map.map return . constArgIndicies) constArgs
lookupConstArgIndicies :: IR.QName -> Converter [Int]
lookupConstArgIndicies name = do
function <- inEnv $ isFunction name
return (if function then lookupConstArgIndicies' name else [])
lookupConstArgIndicies' :: IR.QName -> [Int]
lookupConstArgIndicies' = fromMaybe [] . flip Map.lookup constArgIndicesMap
removeConstArgsFromExpr'
:: IR.Expr
-> Converter (IR.Expr, [Int])
removeConstArgsFromExpr' expr@(IR.Var _ name _) = do
indices <- lookupConstArgIndicies name
return (expr, indices)
removeConstArgsFromExpr' (IR.App srcSpan e1 e2 exprType) = do
(e1', indices) <- removeConstArgsFromExpr' e1
let indices' = map (subtract 1) (filter (> 0) indices)
if 0 `elem` indices then return (e1', indices') else do
(e2', []) <- removeConstArgsFromExpr' e2
return (IR.App srcSpan e1' e2' exprType, indices')
removeConstArgsFromExpr' (IR.TypeAppExpr srcSpan expr typeExpr exprType) = do
(expr', indices) <- removeConstArgsFromExpr' expr
return (IR.TypeAppExpr srcSpan expr' typeExpr exprType, indices)
removeConstArgsFromExpr' (IR.Lambda srcSpan varPats expr exprType)
= shadowVarPats varPats $ do
(expr', []) <- removeConstArgsFromExpr' expr
return (IR.Lambda srcSpan varPats expr' exprType, [])
removeConstArgsFromExpr' (IR.If srcSpan e1 e2 e3 exprType) = do
(e1', []) <- removeConstArgsFromExpr' e1
(e2', []) <- removeConstArgsFromExpr' e2
(e3', []) <- removeConstArgsFromExpr' e3
return (IR.If srcSpan e1' e2' e3' exprType, [])
removeConstArgsFromExpr' (IR.Case srcSpan expr alts exprType) = do
(expr', []) <- removeConstArgsFromExpr' expr
alts' <- mapM removeConstArgsFromAlt alts
return (IR.Case srcSpan expr' alts' exprType, [])
removeConstArgsFromExpr' (IR.Let srcSpan binds expr exprType)
= shadowVarPats (map IR.bindVarPat binds) $ do
binds' <- mapM removeConstArgsFromBind binds
(expr', []) <- removeConstArgsFromExpr' expr
return (IR.Let srcSpan binds' expr' exprType, [])
removeConstArgsFromExpr' (IR.Trace srcSpan msg expr exprType) = do
(expr', []) <- removeConstArgsFromExpr' expr
return (IR.Trace srcSpan msg expr' exprType, [])
removeConstArgsFromExpr' expr@(IR.Con _ _ _) = return (expr, [])
removeConstArgsFromExpr' expr@(IR.Undefined _ _) = return (expr, [])
removeConstArgsFromExpr' expr@(IR.ErrorExpr _ _ _) = return (expr, [])
removeConstArgsFromExpr' expr@(IR.IntLiteral _ _ _) = return (expr, [])
removeConstArgsFromAlt :: IR.Alt -> Converter IR.Alt
removeConstArgsFromAlt (IR.Alt srcSpan conPat varPats expr)
= shadowVarPats varPats $ do
(expr', []) <- removeConstArgsFromExpr' expr
return (IR.Alt srcSpan conPat varPats expr')
removeConstArgsFromBind :: IR.Bind -> Converter IR.Bind
removeConstArgsFromBind (IR.Bind srcSpan varPat expr) = do
(expr', []) <- removeConstArgsFromExpr' expr
return (IR.Bind srcSpan varPat expr')
updateTypeSig
:: Subst IR.Type
-> [IR.TypeVarIdent]
-> Map (IR.QName, String) IR.Type
-> Map IR.QName IR.Type
-> IR.FuncDecl
-> Converter (IR.QName, [Int])
updateTypeSig mgu constTypeVars argTypeMap returnTypeMap funcDecl = do
let name = IR.funcDeclQName funcDecl
args = IR.funcDeclArgs funcDecl
Just entry <- inEnv $ lookupEntry IR.ValueScope name
let argIdents = map IR.varPatIdent args
funcArgs = zip (repeat name) argIdents
typeArgVars = applySubst mgu
(map (IR.TypeVar NoSrcSpan) (entryTypeArgs entry))
argTypes = applySubst mgu (map (flip Map.lookup argTypeMap) funcArgs)
returnType = applySubst mgu (Map.lookup name returnTypeMap)
let allTypeArgs = map IR.typeVarIdent typeArgVars
entry' = entry { entryArity = length args
, entryTypeArgs = allTypeArgs \\ constTypeVars
, entryArgTypes = map fromJust argTypes
, entryReturnType = fromJust returnType
, entryNeedsFreeArgs = False
}
modifyEnv $ addEntry entry'
maybeDecArgIdent <- inEnv $ lookupDecArgIdent name
case maybeDecArgIdent of
Just decArgIdent -> do
let Just decArgIndex = elemIndex decArgIdent argIdents
modifyEnv $ defineDecArg name decArgIndex decArgIdent
Nothing -> return ()
let removedTypeArgIndices = mapMaybe (`elemIndex` allTypeArgs) constTypeVars
return (name, removedTypeArgIndices)
removeConstTypeArgsFromFuncDecl
:: [(IR.QName, [Int])] -> IR.FuncDecl -> Converter IR.FuncDecl
removeConstTypeArgsFromFuncDecl constTypeVars funcDecl = do
let rhs = IR.funcDeclRhs funcDecl
Just indices = lookup (IR.funcDeclQName funcDecl) constTypeVars
typeArgs' = removeIndicies indices (IR.funcDeclTypeArgs funcDecl)
rhs' <- removeConstTypeArgsFromExpr constTypeVars rhs
return funcDecl { IR.funcDeclTypeArgs = typeArgs', IR.funcDeclRhs = rhs' }
removeIndicies :: [Int] -> [a] -> [a]
removeIndicies _ [] = []
removeIndicies indices (x : xs) | 0 `elem` indices = xs'
| otherwise = x : xs'
where
indices' = map (subtract 1) (filter (> 0) indices)
xs' = removeIndicies indices' xs
removeConstTypeArgsFromExpr
:: [(IR.QName, [Int])] -> IR.Expr -> Converter IR.Expr
removeConstTypeArgsFromExpr constTypeVars rootExpr = do
(rootExpr', []) <- removeConstTypeArgsFromExpr' rootExpr
return rootExpr'
where
constTypeVarMap :: Map IR.QName [Int]
constTypeVarMap = Map.fromList constTypeVars
lookupConstTypeArgIndicies :: IR.QName -> Converter [Int]
lookupConstTypeArgIndicies name = do
function <- inEnv $ isFunction name
return (if function then lookupConstTypeArgIndicies' name else [])
lookupConstTypeArgIndicies' :: IR.QName -> [Int]
lookupConstTypeArgIndicies' = fromMaybe [] . flip Map.lookup constTypeVarMap
removeConstTypeArgsFromExpr' :: IR.Expr -> Converter (IR.Expr, [Int])
removeConstTypeArgsFromExpr' expr@(IR.Var _ varName _) = do
indices <- lookupConstTypeArgIndicies varName
return (expr, indices)
removeConstTypeArgsFromExpr' (IR.TypeAppExpr srcSpan expr typeExpr exprType)
= do
(expr', indices) <- removeConstTypeArgsFromExpr' expr
let indices' = map (subtract 1) (filter (> 0) indices)
if 0 `elem` indices
then return (expr', indices')
else return (IR.TypeAppExpr srcSpan expr' typeExpr exprType, indices')
removeConstTypeArgsFromExpr' (IR.App srcSpan e1 e2 exprType) = do
(e1', []) <- removeConstTypeArgsFromExpr' e1
(e2', []) <- removeConstTypeArgsFromExpr' e2
return (IR.App srcSpan e1' e2' exprType, [])
removeConstTypeArgsFromExpr' (IR.If srcSpan e1 e2 e3 exprType) = do
(e1', []) <- removeConstTypeArgsFromExpr' e1
(e2', []) <- removeConstTypeArgsFromExpr' e2
(e3', []) <- removeConstTypeArgsFromExpr' e3
return (IR.If srcSpan e1' e2' e3' exprType, [])
removeConstTypeArgsFromExpr' (IR.Case srcSpan expr alts exprType) = do
(expr', []) <- removeConstTypeArgsFromExpr' expr
alts' <- mapM removeConstTypeArgsFromAlt alts
return (IR.Case srcSpan expr' alts' exprType, [])
removeConstTypeArgsFromExpr' (IR.Lambda srcSpan args expr exprType)
= shadowVarPats args $ do
(expr', []) <- removeConstTypeArgsFromExpr' expr
return (IR.Lambda srcSpan args expr' exprType, [])
removeConstTypeArgsFromExpr' (IR.Let srcSpan binds expr exprType)
= shadowVarPats (map IR.bindVarPat binds) $ do
binds' <- mapM removeConstTypeArgsFromBind binds
(expr', []) <- removeConstTypeArgsFromExpr' expr
return (IR.Let srcSpan binds' expr' exprType, [])
removeConstTypeArgsFromExpr' (IR.Trace srcSpan msg expr exprType) = do
(expr', []) <- removeConstTypeArgsFromExpr' expr
return (IR.Trace srcSpan msg expr' exprType, [])
removeConstTypeArgsFromExpr' expr@(IR.Con _ _ _) = return (expr, [])
removeConstTypeArgsFromExpr' expr@(IR.Undefined _ _) = return (expr, [])
removeConstTypeArgsFromExpr' expr@(IR.ErrorExpr _ _ _) = return (expr, [])
removeConstTypeArgsFromExpr' expr@(IR.IntLiteral _ _ _) = return (expr, [])
removeConstTypeArgsFromAlt :: IR.Alt -> Converter IR.Alt
removeConstTypeArgsFromAlt (IR.Alt srcSpan conPat varPats expr)
= shadowVarPats varPats $ do
(expr', []) <- removeConstTypeArgsFromExpr' expr
return (IR.Alt srcSpan conPat varPats expr')
removeConstTypeArgsFromBind :: IR.Bind -> Converter IR.Bind
removeConstTypeArgsFromBind (IR.Bind srcSpan varPat expr) = do
(expr', []) <- removeConstTypeArgsFromExpr' expr
return (IR.Bind srcSpan varPat expr')
generateInterfaceDecl
:: [ConstArg]
-> [Bool]
-> Map IR.QName IR.QName
-> Subst IR.Type
-> [IR.TypeVarIdent]
-> [IR.TypeVarIdent]
-> IR.FuncDecl
-> Converter Coq.Sentence
generateInterfaceDecl constArgs isConstArgUsed nameMap mgu sectionTypeArgs
renamedTypeArgs funcDecl = localEnv $ do
let args = IR.funcDeclArgs funcDecl
name = IR.funcDeclQName funcDecl
constArgNames = map (IR.UnQual . IR.Ident)
$ mapMaybe (Map.lookup name . constArgIdents) constArgs
usedConstArgNames
= map fst $ filter snd $ zip constArgNames isConstArgUsed
(qualid, binders, returnType') <- convertFuncHead funcDecl
let Just name' = Map.lookup name nameMap
Just qualid' <- inEnv $ lookupIdent IR.ValueScope name'
let typeArgIdents = map IR.typeVarDeclIdent (IR.funcDeclTypeArgs funcDecl)
typeArgNames <- mapM
(lookupTypeArgName typeArgIdents (zip renamedTypeArgs [0 ..]))
sectionTypeArgs
typeArgNames' <- catMaybes
<$> mapM (inEnv . lookupIdent IR.TypeScope) typeArgNames
constArgNames' <- catMaybes
<$> mapM (inEnv . lookupIdent IR.ValueScope) usedConstArgNames
effects <- inEnv $ lookupEffects name
let effectArgs = concatMap Coq.Base.selectExplicitArgs effects
nonConstArgNames = map IR.varPatQName args \\ constArgNames
nonConstArgNames' <- catMaybes
<$> mapM (inEnv . lookupIdent IR.ValueScope) nonConstArgNames
let argNames' = map Coq.Qualid (typeArgNames' ++ constArgNames')
++ effectArgs
++ map Coq.Qualid nonConstArgNames'
rhs' = genericApply qualid' [] [] argNames'
return (Coq.definitionSentence qualid binders returnType' rhs')
where
lookupTypeArgName
:: [IR.TypeVarIdent]
-> [(IR.TypeVarIdent, Int)]
-> IR.TypeVarIdent
-> Converter IR.QName
lookupTypeArgName _ [] u = reportFatal
$ Message (IR.funcDeclSrcSpan funcDecl) Error
$ "Cannot find name of section type argument "
++ u
++ " for "
++ showPretty (IR.funcDeclQName funcDecl)
lookupTypeArgName ws ((v, i) : vs) u = do
let IR.TypeVar _ v' = applySubst mgu (IR.TypeVar NoSrcSpan v)
if v' == u then do
let w = ws !! i
return (IR.UnQual (IR.Ident w)) else lookupTypeArgName ws vs u