-- | This module contains functions for converting Haskell types to Coq. module FreeC.Backend.Coq.Converter.Type where import Control.Monad ( (>=>) ) import qualified FreeC.Backend.Coq.Base as Coq.Base import FreeC.Backend.Coq.Converter.Free import qualified FreeC.Backend.Coq.Syntax as Coq import FreeC.Environment.LookupOrFail import qualified FreeC.IR.Syntax as IR import FreeC.LiftedIR.Converter.Type import qualified FreeC.LiftedIR.Syntax as LIR import FreeC.Monad.Converter ------------------------------------------------------------------------------- -- IR to Coq Translation -- ------------------------------------------------------------------------------- -- | Converts a type from IR to Coq, lifting it into the @Free@ monad. -- -- [\(\tau^\dagger = Free\,Shape\,Pos\,\tau^*\)] -- A type \(\tau\) is converted by lifting it into the @Free@ monad and -- recursively converting the argument and return types of functions -- using 'convertType''. convertType :: IR.Type -> Converter Coq.Term convertType = liftType >=> convertLiftedType -- | Converts a type from IR to Coq. -- -- In contrast to 'convertType', the type itself is not lifted into the -- @Free@ monad. Only the argument and return types of the contained function -- type constructors are lifted recursively. -- -- [\(\alpha^* = \alpha'\)] -- A type variable \(\alpha\) is translated by looking up the corresponding -- Coq identifier \(\alpha'\). -- -- [\(T^* = T'\,Shape\,Pos\)] -- A type constructor \(T\) is translated by looking up the corresponding -- Coq identifier \(T'\) and adding the parameters \(Shape\) and \(Pos\). -- -- [\((\tau_1\,\tau_2)^* = \tau_1^*\,\tau_2^*\)] -- Type constructor applications are translated recursively but -- remain unchanged otherwise. -- -- [\((\tau_1 \rightarrow \tau_2)^* = \tau_1^\dagger \rightarrow \tau_2^\dagger\)] -- Type constructor applications are translated recursively but -- remain unchanged otherwise. convertType' :: IR.Type -> Converter Coq.Term convertType' = liftType' >=> convertLiftedType ------------------------------------------------------------------------------- -- Lifted IR to Coq Translation -- ------------------------------------------------------------------------------- -- | Converts a given type in the lifted IR to a Coq term. convertLiftedType :: LIR.Type -> Converter Coq.Term convertLiftedType (LIR.TypeVar srcSpan ident) = do qualid <- lookupIdentOrFail srcSpan IR.TypeScope (IR.UnQual (IR.Ident ident)) return $ Coq.Qualid qualid convertLiftedType (LIR.TypeCon srcSpan name args _) = do qualid <- lookupIdentOrFail srcSpan IR.TypeScope name args' <- mapM convertLiftedType args return $ genericApply qualid [] [] args' convertLiftedType (LIR.FuncType _ l r) = do l' <- convertLiftedType l r' <- convertLiftedType r return $ Coq.Arrow l' r' convertLiftedType (LIR.FreeTypeCon _ t) = do t' <- convertLiftedType t return $ genericApply Coq.Base.free [] [] [t']