From d33702feb2c753cc8e3dc776bebd195be17a819c Mon Sep 17 00:00:00 2001 From: flupe Date: Thu, 15 Aug 2024 19:10:03 +0200 Subject: [PATCH] proper checks for unboxed datatypes --- src/Agda2Hs/Compile.hs | 8 ++--- src/Agda2Hs/Compile/Data.hs | 62 ++++++++++++++++++++++++++++------- src/Agda2Hs/Compile/Record.hs | 8 ++--- 3 files changed, 59 insertions(+), 19 deletions(-) diff --git a/src/Agda2Hs/Compile.hs b/src/Agda2Hs/Compile.hs index b3172924..d363ab55 100644 --- a/src/Agda2Hs/Compile.hs +++ b/src/Agda2Hs/Compile.hs @@ -20,10 +20,10 @@ import Agda.Utils.Monad ( whenM, anyM, when ) import qualified Language.Haskell.Exts.Extension as Hs import Agda2Hs.Compile.ClassInstance ( compileInstance ) -import Agda2Hs.Compile.Data ( compileData ) +import Agda2Hs.Compile.Data ( compileData, checkUnboxedDataPragma ) import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma ) import Agda2Hs.Compile.Postulate ( compilePostulate ) -import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma ) +import Agda2Hs.Compile.Record ( compileRecord, checkUnboxedRecordPragma ) import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils ( setCurrentRangeQ, tellExtension, primModules, isClassName ) import Agda2Hs.Pragma @@ -88,8 +88,8 @@ compile opts tlm _ def = case (p , theDef def) of (NoPragma , _ ) -> return [] (ExistingClassPragma , _ ) -> return [] - (UnboxPragma s , Record{} ) -> [] <$ checkUnboxPragma def - (UnboxPragma s , Datatype{}) -> [] <$ checkUnboxPragma def + (UnboxPragma s , Record{} ) -> [] <$ checkUnboxedRecordPragma def + (UnboxPragma s , Datatype{}) -> [] <$ checkUnboxedDataPragma def (TransparentPragma , Function{}) -> [] <$ checkTransparentPragma def (InlinePragma , Function{}) -> [] <$ checkInlinePragma def (TuplePragma b , Record{} ) -> return [] diff --git a/src/Agda2Hs/Compile/Data.hs b/src/Agda2Hs/Compile/Data.hs index 3a544a0a..2bccd01b 100644 --- a/src/Agda2Hs/Compile/Data.hs +++ b/src/Agda2Hs/Compile/Data.hs @@ -2,7 +2,7 @@ module Agda2Hs.Compile.Data where import qualified Language.Haskell.Exts.Syntax as Hs -import Control.Monad ( when ) +import Control.Monad ( unless, when ) import Agda.Compiler.Backend import Agda.Syntax.Common import Agda.Syntax.Internal @@ -14,8 +14,9 @@ import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) +import Agda.Utils.Monad ( mapMaybeM ) -import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds ) +import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) ) import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils @@ -46,15 +47,15 @@ compileData newtyp ds def = do when newtyp (checkNewtype d cs) return [Hs.DataDecl () target Nothing hd cs ds] - where - allIndicesErased :: Type -> C () - allIndicesErased t = reduce (unEl t) >>= \case - Pi dom t -> compileDomType (absName t) dom >>= \case - DomDropped -> allIndicesErased (unAbs t) - DomType{} -> genericDocError =<< text "Not supported: indexed datatypes" - DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types" - DomForall{} -> genericDocError =<< text "Not supported: indexed datatypes" - _ -> return () + +allIndicesErased :: Type -> C () +allIndicesErased t = reduce (unEl t) >>= \case + Pi dom t -> compileDomType (absName t) dom >>= \case + DomDropped -> allIndicesErased (unAbs t) + DomType{} -> genericDocError =<< text "Not supported: indexed datatypes" + DomConstraint{} -> genericDocError =<< text "Not supported: constraints in types" + DomForall{} -> genericDocError =<< text "Not supported: indexed datatypes" + _ -> return () compileConstructor :: [Arg Term] -> QName -> C (Hs.QualConDecl ()) compileConstructor params c = do @@ -77,3 +78,42 @@ compileConstructorArgs (ExtendTel a tel) = compileDomType (absName tel) a >>= \c DomConstraint hsA -> genericDocError =<< text "Not supported: constructors with class constraints" DomDropped -> underAbstraction a tel compileConstructorArgs DomForall{} -> __IMPOSSIBLE__ + + +checkUnboxedDataPragma :: Definition -> C () +checkUnboxedDataPragma def = do + let Datatype{..} = theDef def + + -- unboxed datatypes shouldn't be recursive + unless (all null dataMutual) $ genericDocError + =<< text "Unboxed datatype" <+> prettyTCM (defName def) + <+> text "cannot be recursive" + + TelV tel t <- telViewUpTo dataPars (defType def) + let params :: [Arg Term] = teleArgs tel + + allIndicesErased t + + case dataCons of + [con] -> do + info <- getConstInfo con + let Constructor {..} = theDef info + ty <- defType info `piApplyM` params + TelV conTel _ <- telView ty + args <- nonErasedArgs conTel + unless (length args == 1) $ genericDocError + =<< text "Unboxed datatype" <+> prettyTCM (defName def) + <+> text "should have a single constructor with exactly one non-erased argument." + + _ -> genericDocError =<< text "Unboxed datatype" <+> prettyTCM (defName def) + <+> text "must have exactly one constructor." + + where + nonErasedArgs :: Telescope -> C [String] + nonErasedArgs EmptyTel = return [] + nonErasedArgs (ExtendTel a tel) = compileDom a >>= \case + DODropped -> underAbstraction a tel nonErasedArgs + DOType -> genericDocError =<< text "Type argument in unboxed datatype not supported" + DOInstance -> genericDocError =<< text "Instance argument in unboxed datatype not supported" + DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedArgs + diff --git a/src/Agda2Hs/Compile/Record.hs b/src/Agda2Hs/Compile/Record.hs index 1045bc59..8c7ca63d 100644 --- a/src/Agda2Hs/Compile/Record.hs +++ b/src/Agda2Hs/Compile/Record.hs @@ -29,6 +29,7 @@ import Agda2Hs.Compile.Function ( compileFun ) import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) ) import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils +import Agda2Hs.Compile.Data ( allIndicesErased ) import Agda2Hs.HsUtils -- | Primitive fields and default implementations @@ -170,8 +171,9 @@ compileRecord target def = do let conDecl = Hs.QualConDecl () Nothing Nothing $ Hs.RecDecl () cName fieldDecls return $ Hs.DataDecl () don Nothing hd [conDecl] ds -checkUnboxPragma :: Definition -> C () -checkUnboxPragma def | Record{..} <- theDef def = do +checkUnboxedRecordPragma :: Definition -> C () +checkUnboxedRecordPragma def = do + let Record{..} = theDef def -- recRecursive can be used again after agda 2.6.4.2 is released -- see agda/agda#7042 unless (all null recMutual) $ genericDocError @@ -196,5 +198,3 @@ checkUnboxPragma def | Record{..} <- theDef def = do DOInstance -> genericDocError =<< text "Instance field in unboxed record not supported" DOTerm -> (absName tel:) <$> underAbstraction a tel nonErasedFields -checkUnboxPragma def | Datatype{..} <- theDef def = do - pure () -- TOOD(flupe):