From 31462999d4c068e8edcfd41cff5024d224de3b49 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Fri, 6 Oct 2023 16:14:55 +0200 Subject: [PATCH 1/2] [ re #169 ] Don't consider data/record modules as qualified imports --- src/Agda2Hs/AgdaUtils.hs | 8 ++++++++ src/Agda2Hs/Compile/Name.hs | 26 ++++++++++++++++++-------- test/AllTests.agda | 2 ++ test/Issue169.agda | 19 +++++++++++++++++++ test/golden/AllTests.hs | 1 + test/golden/Issue169.hs | 12 ++++++++++++ test/golden/QualifiedImports.hs | 8 ++++---- 7 files changed, 64 insertions(+), 12 deletions(-) create mode 100644 test/Issue169.agda create mode 100644 test/golden/Issue169.hs diff --git a/src/Agda2Hs/AgdaUtils.hs b/src/Agda2Hs/AgdaUtils.hs index 56d93e65..88393de1 100644 --- a/src/Agda2Hs/AgdaUtils.hs +++ b/src/Agda2Hs/AgdaUtils.hs @@ -2,6 +2,7 @@ module Agda2Hs.AgdaUtils where import Data.Data import Data.Monoid ( Any(..) ) +import qualified Data.Map as Map import Data.Maybe ( fromMaybe ) import Agda.Compiler.Backend hiding ( Args ) @@ -9,8 +10,11 @@ import Agda.Compiler.Backend hiding ( Args ) import Agda.Interaction.FindFile ( findFile' ) import Agda.Syntax.Common ( Arg, defaultArg ) +import qualified Agda.Syntax.Concrete as C import Agda.Syntax.Internal import Agda.Syntax.Internal.Names +import Agda.Syntax.Scope.Base +import Agda.Syntax.Scope.Monad import Agda.Syntax.TopLevelModuleName import Agda.TypeChecking.Monad ( topLevelModuleName ) @@ -92,3 +96,7 @@ getTopLevelModuleForModuleName = loop . mnameToList getTopLevelModuleForQName :: QName -> TCM (Maybe TopLevelModuleName) getTopLevelModuleForQName = getTopLevelModuleForModuleName . qnameModule + +lookupModuleInCurrentModule :: C.Name -> TCM [AbstractModule] +lookupModuleInCurrentModule x = + fromMaybe [] . Map.lookup x . nsModules . thingsInScope [PublicNS, PrivateNS] <$> getCurrentScope diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 1b022774..36744772 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -3,8 +3,10 @@ module Agda2Hs.Compile.Name where import Control.Arrow ( (>>>) ) import Control.Applicative ( (<|>) ) import Control.Monad +import Control.Monad.Except ( catchError ) import Control.Monad.Reader +import Data.Functor ( (<&>) ) import Data.List ( intercalate, isPrefixOf ) import Data.Text ( unpack ) @@ -13,18 +15,21 @@ import qualified Language.Haskell.Exts as Hs import Agda.Compiler.Backend hiding ( topLevelModuleName ) import Agda.Compiler.Common ( topLevelModuleName ) +import qualified Agda.Syntax.Abstract as A import Agda.Syntax.Common import Agda.Syntax.Internal import Agda.Syntax.Position import qualified Agda.Syntax.Concrete as C -import Agda.Syntax.Scope.Base ( inverseScopeLookupName ) +import Agda.Syntax.Scope.Base ( inverseScopeLookupName, amodName ) +import Agda.Syntax.Scope.Monad ( resolveName, isDatatypeModule ) import Agda.Syntax.TopLevelModuleName +import Agda.TypeChecking.Datatypes ( isDataOrRecordType ) import Agda.TypeChecking.Pretty import Agda.TypeChecking.Records ( isRecordConstructor ) import qualified Agda.Utils.List1 as List1 -import Agda.Utils.Maybe ( isJust, whenJust, fromMaybe, caseMaybeM ) +import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM ) import Agda.Utils.Pretty ( prettyShow ) import qualified Agda.Utils.Pretty as P ( Pretty(pretty) ) @@ -140,12 +145,17 @@ compileQName f getQualifier :: QName -> Hs.ModuleName () -> C Qualifier getQualifier f mod = - (inverseScopeLookupName f <$> getScope) >>= return . \case - (C.Qual as C.QName{} : _) - | qual <- hsModuleName $ prettyShow as, qual /= mod - -> QualifiedAs (Just qual) - (C.Qual{} : _) -> QualifiedAs Nothing - _ -> Unqualified + (inverseScopeLookupName f <$> getScope) >>= \case + (C.QName{} : _) -> return Unqualified + (C.Qual as C.QName{} : _) -> liftTCM $ do + let qual = hsModuleName $ prettyShow as + lookupModuleInCurrentModule as >>= \case + (x:_) | qual /= mod -> isDatatypeModule (amodName x) >>= \case + Just{} -> return $ QualifiedAs Nothing + Nothing -> return $ QualifiedAs $ Just qual + _ -> return Nothing + `catchError` \_ -> return $ QualifiedAs Nothing + _ -> return $ QualifiedAs Nothing qualify :: Hs.ModuleName () -> Hs.Name () -> Qualifier -> Hs.QName () qualify mod n = \case diff --git a/test/AllTests.agda b/test/AllTests.agda index 49e41985..00953790 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -55,6 +55,7 @@ import TypeOperators import ErasedTypeArguments import TypeOperatorExport import TypeOperatorImport +import Issue169 {-# FOREIGN AGDA2HS import Issue14 @@ -110,4 +111,5 @@ import TypeOperators import ErasedTypeArguments import TypeOperatorExport import TypeOperatorImport +import Issue169 #-} diff --git a/test/Issue169.agda b/test/Issue169.agda new file mode 100644 index 00000000..cce7fd8c --- /dev/null +++ b/test/Issue169.agda @@ -0,0 +1,19 @@ +open import Haskell.Prelude + +record Identity (a : Set) : Set where + field + runIdentity : a +open Identity public + +{-# COMPILE AGDA2HS Identity newtype #-} + +showIdentity : ⦃ Show a ⦄ → Identity a → String +showIdentity record { runIdentity = id } = "Id < " ++ show id ++ " >" + +{-# COMPILE AGDA2HS showIdentity #-} + +instance + iIdentityShow : ⦃ Show a ⦄ → Show (Identity a) + iIdentityShow = record {Show₂ record {show = showIdentity}} + +{-# COMPILE AGDA2HS iIdentityShow #-} diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 574fd13a..8c8b1464 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -53,4 +53,5 @@ import TypeOperators import ErasedTypeArguments import TypeOperatorExport import TypeOperatorImport +import Issue169 diff --git a/test/golden/Issue169.hs b/test/golden/Issue169.hs new file mode 100644 index 00000000..a2218e03 --- /dev/null +++ b/test/golden/Issue169.hs @@ -0,0 +1,12 @@ +module Issue169 where + +newtype Identity a = Identity{runIdentity :: a} + +showIdentity :: Show a => Identity a -> String +showIdentity (Identity id) = "Id < " ++ show id ++ " >" + +instance (Show a) => Show (Identity a) where + showsPrec = showsPrec + showList = showList + show = showIdentity + diff --git a/test/golden/QualifiedImports.hs b/test/golden/QualifiedImports.hs index 7a6a1a8a..4e334e1e 100644 --- a/test/golden/QualifiedImports.hs +++ b/test/golden/QualifiedImports.hs @@ -1,15 +1,15 @@ module QualifiedImports where -import qualified Importee (Foo(MkFoo), foo) +import Importee (Foo(MkFoo), foo) import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#)) -- ** simple qualification simpqualBar :: Int -simpqualBar = Importee.foo +simpqualBar = foo -simpfoo :: Importee.Foo -simpfoo = Importee.MkFoo +simpfoo :: Foo +simpfoo = MkFoo -- ** qualified imports From 027c67abbb9b0788d327b90b5f2a31d6a6893548 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Tue, 10 Oct 2023 18:01:11 +0200 Subject: [PATCH 2/2] [ fix #169 ] Throw error when minimal record does not use named definition or \where --- src/Agda2Hs/Compile/ClassInstance.hs | 48 ++++++++++++++++++---------- test/Fail/Issue169-record.agda | 25 +++++++++++++++ test/Issue169.agda | 2 +- test/golden/Issue169-record.err | 2 ++ test/golden/Issue169.hs | 2 -- 5 files changed, 60 insertions(+), 19 deletions(-) create mode 100644 test/Fail/Issue169-record.agda create mode 100644 test/golden/Issue169-record.err diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs index 195f582c..c208b8c1 100644 --- a/src/Agda2Hs/Compile/ClassInstance.hs +++ b/src/Agda2Hs/Compile/ClassInstance.hs @@ -137,6 +137,10 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do -- We want the actual field name, not the instance-opened projection. (q, _, _) <- origProjection q arg <- fieldArgInfo q + + reportSDoc "agda2hs.compile.instance" 15 $ + text "Compiling instance clause for" <+> prettyTCM (Arg arg $ Def q []) + let uf = hsName $ prettyShow $ nameConcrete $ qnameName q let @@ -168,25 +172,37 @@ compileInstanceClause curModule c = withClauseLocals curModule c $ do -- Projection of a primitive field: chase down definition and inline as instance clause. | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c' , [(_, f)] <- mapMaybe isProjElim es - , f .~ q - -> do d <- chaseDef n - fc <- compileFun False d - let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d - let fc' = dropPatterns 1 $ replaceName hd uf fc - return (map (Hs.InsDecl ()) fc', [n]) + , f .~ q -> do + reportSDoc "agda2hs.compile.instance" 20 $ + text "Instance clause is projected from" <+> prettyTCM (Def n []) + reportSDoc "agda2hs.compile.instance" 20 $ + text $ "raw projection:" ++ prettyShow (Def n []) + d <- chaseDef n + fc <- compileFun False d + let hd = hsName $ prettyShow $ nameConcrete $ qnameName $ defName d + let fc' = dropPatterns 1 $ replaceName hd uf fc + return (map (Hs.InsDecl ()) fc', [n]) -- Projection of a default implementation: drop while making sure these are drawn from the -- same (minimal) dictionary as the primitive fields. - | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c' - , n .~ q - , Just [ Def n' _ ] <- map unArg . filter keepArg <$> allApplyElims es - -> do n' <- resolveExtendedLambda n' - return ([], [n']) - - -- No minimal dictionary used, proceed with compiling as a regular clause. - | otherwise - -> do ms <- disableCopatterns $ compileClause curModule uf c' - return ([Hs.InsDecl () (Hs.FunBind () [ms]) | keepArg arg], []) + | Clause {namedClausePats = [], clauseBody = Just (Def n es)} <- c' + , n .~ q -> do + case map unArg . filter keepArg <$> allApplyElims es of + Just [ Def f _ ] -> do + reportSDoc "agda2hs.compile.instance" 20 $ vcat + [ text "Dropping default instance clause" <+> prettyTCM c' + , text "with minimal dictionary" <+> prettyTCM f + ] + reportSDoc "agda2hs.compile.instance" 40 $ + text $ "raw dictionary:" ++ prettyShow f + return ([], [f]) + _ -> genericDocError =<< text "illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`." + + -- No minimal dictionary used, proceed with compiling as a regular clause. + | otherwise -> do + reportSDoc "agda2hs.compile.instance" 20 $ text "Compiling instance clause" <+> prettyTCM c' + ms <- disableCopatterns $ compileClause curModule uf c' + return ([Hs.InsDecl () (Hs.FunBind () [ms])], []) fieldArgInfo :: QName -> C ArgInfo fieldArgInfo f = do diff --git a/test/Fail/Issue169-record.agda b/test/Fail/Issue169-record.agda new file mode 100644 index 00000000..8f8065c5 --- /dev/null +++ b/test/Fail/Issue169-record.agda @@ -0,0 +1,25 @@ +-- Using a default method implementation for an instance declaration currently +-- requires a named definition or an anonymous `λ where` on the Agda side, so a +-- record is not allowed. + +module Fail.Issue169-record where + +open import Haskell.Prelude + +record Identity (a : Set) : Set where + field + runIdentity : a +open Identity public + +{-# COMPILE AGDA2HS Identity newtype #-} + +showIdentity : ⦃ Show a ⦄ → Identity a → String +showIdentity record { runIdentity = id } = "Id < " ++ show id ++ " >" + +{-# COMPILE AGDA2HS showIdentity #-} + +instance + iIdentityShow : ⦃ Show a ⦄ → Show (Identity a) + iIdentityShow = record {Show₂ record {show = showIdentity}} + +{-# COMPILE AGDA2HS iIdentityShow #-} diff --git a/test/Issue169.agda b/test/Issue169.agda index cce7fd8c..bc005606 100644 --- a/test/Issue169.agda +++ b/test/Issue169.agda @@ -14,6 +14,6 @@ showIdentity record { runIdentity = id } = "Id < " ++ show id ++ " >" instance iIdentityShow : ⦃ Show a ⦄ → Show (Identity a) - iIdentityShow = record {Show₂ record {show = showIdentity}} + iIdentityShow = record {Show₂ (λ where .Show₂.show → showIdentity)} {-# COMPILE AGDA2HS iIdentityShow #-} diff --git a/test/golden/Issue169-record.err b/test/golden/Issue169-record.err new file mode 100644 index 00000000..0a6f399d --- /dev/null +++ b/test/golden/Issue169-record.err @@ -0,0 +1,2 @@ +test/Fail/Issue169-record.agda:22,3-16 +illegal instance declaration: instances using default methods should use a named definition or an anonymous `λ where`. diff --git a/test/golden/Issue169.hs b/test/golden/Issue169.hs index a2218e03..4577a9fb 100644 --- a/test/golden/Issue169.hs +++ b/test/golden/Issue169.hs @@ -6,7 +6,5 @@ showIdentity :: Show a => Identity a -> String showIdentity (Identity id) = "Id < " ++ show id ++ " >" instance (Show a) => Show (Identity a) where - showsPrec = showsPrec - showList = showList show = showIdentity