module Agda2Hs.Compile.Data where import qualified Language.Haskell.Exts.Syntax as Hs import Agda.Compiler.Backend import Agda.Syntax.Common import Agda.Syntax.Internal import Agda.Syntax.Common.Pretty ( prettyShow ) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Reduce import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) import Agda2Hs.Compile.Type ( compileDom, compileTeleBinds ) import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C () checkNewtype name cs = do checkSingleElement name cs "Newtype must have exactly one constructor in definition" case head cs of Hs.QualConDecl () _ _ (Hs.ConDecl () cName types) -> checkSingleElement cName types "Newtype must have exactly one field in constructor" compileData :: DataTarget -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()] compileData target ds def = setCurrentRange (nameBindingSite $ qnameName $ defName def) $ do let d = hsName $ prettyShow $ qnameName $ defName def checkValidTypeName d case theDef def of Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} -> do TelV tel t <- telViewUpTo n (defType def) reportSDoc "agda2hs.data" 10 $ text "Datatype telescope:" <+> prettyTCM tel allIndicesErased t let params = teleArgs tel addContext tel $ do binds <- compileTeleBinds tel cs <- mapM (compileConstructor params) cs let hd = foldl (Hs.DHApp ()) (Hs.DHead () d) binds case target of ToData -> return [Hs.DataDecl () (Hs.DataType ()) Nothing hd cs ds] ToDataNewType -> do checkNewtype d cs return [Hs.DataDecl () (Hs.NewType ()) Nothing hd cs ds] _ -> __IMPOSSIBLE__ where allIndicesErased :: Type -> C () allIndicesErased t = reduce (unEl t) >>= \case Pi dom t -> compileDom (absName t) dom >>= \case DomDropped -> allIndicesErased (unAbs t) DomType{} -> genericDocError =<< text "Not supported: indexed datatypes" DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types" _ -> return () compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ()) compileConstructor params c = checkingVars $ do reportSDoc "agda2hs.data.con" 15 $ text "compileConstructor" <+> prettyTCM c reportSDoc "agda2hs.data.con" 20 $ text " params = " <+> prettyTCM params ty <- (`piApplyM` params) . defType =<< getConstInfo c reportSDoc "agda2hs.data.con" 20 $ text " ty = " <+> prettyTCM ty TelV tel _ <- telView ty let conName = hsName $ prettyShow $ qnameName c checkValidConName conName args <- compileConstructorArgs tel return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args compileConstructorArgs :: Telescope -> C [Hs.Type ()] compileConstructorArgs EmptyTel = return [] compileConstructorArgs (ExtendTel a tel) = compileDom (absName tel) a >>= \case DomType s hsA -> do ty <- addTyBang s hsA (ty :) <$> underAbstraction a tel compileConstructorArgs DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints" DomDropped -> underAbstraction a tel compileConstructorArgs