-- | This module contains functions for generating Coq function, constructor -- and type arguments from our intermediate representation. module FreeC.Backend.Coq.Converter.Arg where import FreeC.Backend.Coq.Converter.Type import qualified FreeC.Backend.Coq.Syntax as Coq import FreeC.Environment.Fresh import FreeC.Environment.Renamer import qualified FreeC.IR.Syntax as IR import FreeC.Monad.Converter ------------------------------------------------------------------------------- -- Type Arguments -- ------------------------------------------------------------------------------- -- | Converts the declarations of type variables in the head of a data type or -- type synonym declaration to a Coq binder for a set of explicit or implicit -- type arguments. -- -- E.g. the declaration of the type variable @a@ in @data D a = ...@ is -- translated to the binder @(a : Type)@. If there are multiple type variable -- declarations as in @data D a b = ...@ they are grouped into a single -- binder @(a b : Type)@, because we assume all Haskell type variables to be -- of kind @*@. -- -- The first argument controls whether the generated binders are explicit -- (e.g. @(a : Type)@) or implicit (e.g. @{a : Type}@). convertTypeVarDecls :: Coq.Explicitness -- ^ Whether to generate an explicit or implicit binder. -> [IR.TypeVarDecl] -- ^ The type variable declarations. -> Converter [Coq.Binder] convertTypeVarDecls explicitness typeVarDecls = snd <$> convertTypeVarDecls' explicitness typeVarDecls -- | Like 'convertTypeVarDecls' but also returns the Coq identifiers of the -- bound variables. convertTypeVarDecls' :: Coq.Explicitness -- ^ Whether to generate an explicit or implicit binder. -> [IR.TypeVarDecl] -- ^ The type variable declarations. -> Converter ([Coq.Qualid], [Coq.Binder]) convertTypeVarDecls' explicitness typeVarDecls | null typeVarDecls = return ([], []) | otherwise = do idents' <- mapM convertTypeVarDecl typeVarDecls return $ ( idents' , [ Coq.typedBinder Coq.Ungeneralizable explicitness idents' Coq.sortType ] ) where -- | Converts a type variable declaration by adding an entry to the -- environment. -- -- Returns the Coq identifier of the type variable. convertTypeVarDecl :: IR.TypeVarDecl -> Converter Coq.Qualid convertTypeVarDecl (IR.TypeVarDecl srcSpan ident) = renameAndDefineTypeVar srcSpan ident ------------------------------------------------------------------------------- -- Function Arguments -- ------------------------------------------------------------------------------- -- | Converts the argument of a function (a variable pattern) to an explicit -- Coq binder. -- -- If the variable pattern has a type annotation, the generated binder is -- annotated with the converted type. If the variable pattern is strict, the -- variable is marked as non-monadic and the converted type is not -- lifted to the @Free@ monad. convertArg :: IR.VarPat -> Converter Coq.Binder convertArg (IR.VarPat srcSpan ident maybeArgType isStrict) = do ident' <- renameAndDefineVar srcSpan isStrict ident maybeArgType maybeArgType' <- mapM (if isStrict then convertType' else convertType) maybeArgType generateArgBinder ident' maybeArgType' -- | Generates an explicit Coq binder for a function argument with the given -- name and optional Coq type. -- -- If no type is provided, it will be inferred by Coq. generateArgBinder :: Coq.Qualid -> Maybe Coq.Term -> Converter Coq.Binder generateArgBinder ident' Nothing = return (Coq.Inferred Coq.Explicit (Coq.Ident ident')) generateArgBinder ident' (Just argType') = return (Coq.typedBinder' Coq.Ungeneralizable Coq.Explicit ident' argType') -- | Converts the argument of an artificially generated function to an explicit -- Coq binder. A fresh Coq identifier is selected for the argument -- and returned together with the binder. convertAnonymousArg :: Maybe IR.Type -> Converter (Coq.Qualid, Coq.Binder) convertAnonymousArg mArgType = do ident' <- freshCoqQualid freshArgPrefix mArgType' <- mapM convertType mArgType binder <- generateArgBinder ident' mArgType' return (ident', binder)