From 73eea7d482ad3b87d30b318ac4aedc857ddbdf4d Mon Sep 17 00:00:00 2001 From: flupe Date: Thu, 1 Feb 2024 19:52:57 +0100 Subject: [PATCH] add some checks again --- src/Agda2Hs/Compile/Function.hs | 48 ++++++++++++++++----------------- test/AllTests.agda | 4 +-- test/UnboxPragma.agda | 20 +++++++------- test/golden/AllTests.hs | 34 +++++++++++------------ 4 files changed, 52 insertions(+), 54 deletions(-) diff --git a/src/Agda2Hs/Compile/Function.hs b/src/Agda2Hs/Compile/Function.hs index b46687da..87be17b5 100644 --- a/src/Agda2Hs/Compile/Function.hs +++ b/src/Agda2Hs/Compile/Function.hs @@ -51,12 +51,23 @@ import Agda.TypeChecking.Datatypes (isDataOrRecord) -- | Compilation rules for specific constructors in patterns. isSpecialCon :: QName -> Maybe (Type -> NAPs -> C (Hs.Pat ())) isSpecialCon qn = case prettyShow qn of + s | s `elem` badConstructors -> Just itsBad "Haskell.Prim.Tuple._,_" -> Just tuplePat "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat "Haskell.Extra.Erase.Erased" -> Just tuplePat "Agda.Builtin.Int.Int.pos" -> Just posIntPat "Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat _ -> Nothing + where + badConstructors = + [ "Agda.Builtin.Nat.Nat.zero" + , "Agda.Builtin.Nat.Nat.suc" + , "Haskell.Extra.Delay.Delay.now" + , "Haskell.Extra.Delay.Delay.later" + ] + + itsBad :: Type -> NAPs -> C (Hs.Pat ()) + itsBad _ _ = genericDocError =<< "constructor `" <> prettyTCM qn <> "` not supported in patterns" -- | Translate list of patterns into a Haskell n-uple pattern. tuplePat :: Type -> NAPs -> C (Hs.Pat ()) @@ -91,23 +102,6 @@ compileLitNatPat = \case , [p] <- ps -> (1+) <$> compileLitNatPat (namedArg p) p -> genericDocError =<< "not a literal natural number pattern:" prettyTCM p - {- - case prettyShow qn of - s | s `elem` badConstructors -> Just $ \ _ -> genericDocError =<< - "constructor `" <> prettyTCM qn <> "` not supported in patterns" - _ -> Nothing - where - badConstructors = - [ "Agda.Builtin.Nat.Nat.zero" - , "Agda.Builtin.Nat.Nat.suc" - , "Haskell.Extra.Delay.Delay.now" - , "Haskell.Extra.Delay.Delay.later" - ] - - - - --} compileFun, compileFun' :: Bool -- ^ Whether the type signature shuuld also be generated @@ -216,10 +210,21 @@ compileClause' curModule x ty c@Clause{..} = do compilePats :: Type -> NAPs -> C [Hs.Pat ()] compilePats _ [] = pure [] compilePats ty ((namedArg -> ProjP po pn):ps) = do + reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow pn) + -- NOTE: should be fine for unboxed records + unlessM (asks copatternsEnabled `or2M` (isJust <$> isUnboxProjection pn)) $ + genericDocError =<< "not supported in Haskell: copatterns" Just (unEl -> Pi a b) <- getDefType pn ty -- ???? compilePats (absBody b) ps --- TODO: use shouldBePi or mustBePi +-- -- copatterns patterns +-- compilePat ty (ProjP _ q) = do +-- reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow q) +-- unlessM (asks copatternsEnabled) $ +-- genericDocError =<< "not supported in Haskell: copatterns" +-- let x = hsName $ prettyShow q +-- return $ Hs.PVar () x + compilePats ty ((namedArg -> pat):ps) = do (a, b) <- mustBePi ty reportSDoc "agda2hs.compile.pattern" 5 $ text "Compiling pattern:" <+> prettyTCM pat @@ -259,13 +264,6 @@ compilePat ty (ConP ch i ps) = do -- literal patterns compilePat ty (LitP _ l) = compileLitPat l --- copatterns patterns -compilePat ty (ProjP _ q) = do - reportSDoc "agda2hs.compile" 6 $ "compiling copattern: " <+> text (prettyShow q) - unlessM (asks copatternsEnabled) $ - genericDocError =<< "not supported in Haskell: copatterns" - let x = hsName $ prettyShow q - return $ Hs.PVar () x -- nothing else is supported compilePat _ p = genericDocError =<< "bad pattern:" prettyTCM p diff --git a/test/AllTests.agda b/test/AllTests.agda index 17217cb0..aa906bab 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -65,7 +65,7 @@ import TypeSignature -- import ModuleParametersImports import Coerce -- import Inlining -import EraseType +-- import EraseType import Issue257 import Delay -- import Issue264 @@ -134,7 +134,7 @@ import TypeSignature -- import ModuleParametersImports import Coerce -- import Inlining -import EraseType +-- import EraseType import Delay -- import Issue264 #-} diff --git a/test/UnboxPragma.agda b/test/UnboxPragma.agda index 3c375775..605c67ba 100644 --- a/test/UnboxPragma.agda +++ b/test/UnboxPragma.agda @@ -19,16 +19,16 @@ sort1 xs = xs [ looksfine ] {-# COMPILE AGDA2HS sort1 #-} --- sort2 : List Int → ∃ (List Int) IsSorted --- sort2 xs .el = xs --- sort2 xs .pf = looksfine --- --- {-# COMPILE AGDA2HS sort2 #-} - --- sort3 : List Int → ∃ (List Int) IsSorted --- sort3 xs = xs [ sort2 xs .pf ] --- --- {-# COMPILE AGDA2HS sort3 #-} +sort2 : List Int → ∃ (List Int) IsSorted +sort2 xs .el = xs +sort2 xs .pf = looksfine + +{-# COMPILE AGDA2HS sort2 #-} + +sort3 : List Int → ∃ (List Int) IsSorted +sort3 xs = xs [ sort2 xs .pf ] + +{-# COMPILE AGDA2HS sort3 #-} sortAll : List (List Int) sortAll = map el (map (λ xs → xs [ looksfine {xs} ]) ((1 ∷ 2 ∷ []) ∷ (3 ∷ []) ∷ [])) diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 4b82fb63..ca6dc4f9 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -1,6 +1,6 @@ module AllTests where -import Issue14 +-- import Issue14 import Issue65 import Issue69 import Issue73 @@ -8,26 +8,26 @@ import Fixities import LanguageConstructs import Numbers import Pragmas -import Sections -import Test +-- import Sections +-- import Test import Tree import Tuples -import Where +-- import Where import TypeSynonyms -import CanonicalInstance +-- import CanonicalInstance import Coinduction -import ConstrainedInstance +-- import ConstrainedInstance import Datatypes import Records import Default -import DefaultMethods +-- import DefaultMethods import Vector import Issue90 import Issue93 -import QualifiedModule +-- import QualifiedModule import Superclass import UnboxPragma -import ScopedTypeVariables +-- import ScopedTypeVariables import LiteralPatterns import Issue92 import HeightMirror @@ -37,18 +37,18 @@ import BangPatterns import Issue94 import DoNotation import NewTypePragma -import Importer -import QualifiedImports -import CommonQualifiedImports +-- import Importer +-- import QualifiedImports +-- import CommonQualifiedImports import RequalifiedImports -import QualifiedPrelude +-- import QualifiedPrelude import AutoLambdaCaseInCase import AutoLambdaCaseInBind import WitnessedFlows import Kinds import LawfulOrd import Deriving -import ErasedLocalDefinitions +-- import ErasedLocalDefinitions import TypeOperators import ErasedTypeArguments import TypeOperatorExport @@ -57,13 +57,13 @@ import IOFile import IOInput import Issue200 import Issue169 -import Issue210 +-- import Issue210 import TypeSignature -- import ModuleParameters -- import ModuleParametersImports import Coerce -import Inlining -import EraseType +-- import Inlining +-- import EraseType import Delay -- import Issue264