From d66b9e5d696ae07151dd7d227c2aed1bb8b02e53 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Thu, 11 Jul 2024 18:00:09 +0200 Subject: [PATCH 1/4] Whitespace --- src/Agda2Hs/Compile/ClassInstance.hs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs index 993b10e8..dee24025 100644 --- a/src/Agda2Hs/Compile/ClassInstance.hs +++ b/src/Agda2Hs/Compile/ClassInstance.hs @@ -65,7 +65,7 @@ compileInstance :: InstanceTarget -> Definition -> C (Hs.Decl ()) compileInstance (ToDerivation strategy) def@Defn{..} = setCurrentRangeQ defName $ do - reportSDoc "agda2hs.compile.instance" 13 $ + reportSDoc "agda2hs.compile.instance" 13 $ text "compiling instance" <+> prettyTCM defName <+> text "to standalone deriving" tellExtension Hs.StandaloneDeriving enableStrategy strategy @@ -74,7 +74,7 @@ compileInstance (ToDerivation strategy) def@Defn{..} = compileInstance ToDefinition def@Defn{..} = enableCopatterns $ setCurrentRangeQ defName $ do - reportSDoc "agda2hs.compile.instance" 13 $ + reportSDoc "agda2hs.compile.instance" 13 $ text "compiling instance" <+> prettyTCM defName <+> text "to instance definition" ir <- compileInstRule [] (unEl defType) withFunctionLocals defName $ do @@ -181,7 +181,7 @@ compileInstanceClause' curModule ty (p:ps) c -- reached record projection | ProjP _ q <- namedArg p = do - -- we put back the remaining patterns in the original clause + -- we put back the remaining patterns in the original clause let c' = c {namedClausePats = ps} -- We want the actual field name, not the instance-opened projection. @@ -198,9 +198,9 @@ compileInstanceClause' curModule ty (p:ps) c -- retrieve the type of the projection Just (unEl -> Pi a b) <- getDefType q ty -- We don't really have the information available to reconstruct the instance - -- head. However, all dependencies on the instance head are in erased positions, + -- head. However, all dependencies on the instance head are in erased positions, -- so we can just use a dummy term instead - let instanceHead = __DUMMY_TERM__ + let instanceHead = __DUMMY_TERM__ ty' = b `absApp` instanceHead reportSDoc "agda2hs.compile.instance" 15 $ @@ -245,7 +245,7 @@ compileInstanceClause' curModule ty (p:ps) c text $ "raw name: " ++ prettyShow (Def n []) d@Defn{..} <- getConstInfo n let mod = if isExtendedLambdaName defName then curModule else qnameModule defName - (fc, rs) <- withCurrentModule mod $ + (fc, rs) <- withCurrentModule mod $ concatUnzip <$> mapM (compileInstanceClause mod defType) (funClauses theDef) let hd = hsName $ prettyShow $ nameConcrete $ qnameName defName let fc' = {- dropPatterns 1 $ -} replaceName hd uf fc From cf6c9808f654d505d526f6c27dcd6f5ea6b6816e Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Thu, 11 Jul 2024 18:00:25 +0200 Subject: [PATCH 2/4] [ fix #338 ] Only filter out imports of current module, not other modules with current module as prefix --- src/Agda2Hs/Compile/Imports.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Agda2Hs/Compile/Imports.hs b/src/Agda2Hs/Compile/Imports.hs index 251fbb27..d8aef387 100644 --- a/src/Agda2Hs/Compile/Imports.hs +++ b/src/Agda2Hs/Compile/Imports.hs @@ -25,7 +25,7 @@ type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()] compileImports top is0 = do - let is = filter (not . (top `isPrefixOf`) . Hs.prettyPrint . importModule) is0 + let is = filter (not . (top ==) . Hs.prettyPrint . importModule) is0 checkClashingImports is let imps = Map.toList $ groupModules is return $ map (uncurry $ uncurry makeImportDecl) imps From f2fef22d382db918656995327908d7ab88283282 Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Thu, 11 Jul 2024 18:01:42 +0200 Subject: [PATCH 3/4] [ refactor ] Factor out function `isPrimModule` --- src/Agda2Hs/Compile/Utils.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index 6d8ef53f..4193f1af 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -7,6 +7,7 @@ import Control.Monad.Reader import Control.Monad.Writer ( tell ) import Control.Monad.State ( put, modify ) +import Data.List ( isPrefixOf ) import Data.Maybe ( isJust ) import qualified Data.Map as M import Data.List ( isPrefixOf ) From 59d8c2a63f51d7d2467fee9c1bead9906d80cd8e Mon Sep 17 00:00:00 2001 From: Jesper Cockx Date: Fri, 13 Dec 2024 15:26:52 +0100 Subject: [PATCH 4/4] [ fix #324 ] Keep track of instance-only imports --- src/Agda2Hs/Compile/ClassInstance.hs | 1 + src/Agda2Hs/Compile/Imports.hs | 34 +++++++++++-------- src/Agda2Hs/Compile/Name.hs | 7 ++++ src/Agda2Hs/Compile/Term.hs | 49 ++++++++++++++++++++++++++-- src/Agda2Hs/Compile/Types.hs | 15 ++++++--- src/Agda2Hs/Compile/Utils.hs | 37 --------------------- src/Agda2Hs/Render.hs | 2 +- test/AllTests.agda | 2 ++ test/Issue324.agda | 8 +++++ test/Issue324instance.agda | 9 +++++ test/golden/AllTests.hs | 1 + test/golden/Issue324.hs | 7 ++++ test/golden/Issue324instance.hs | 5 +++ test/golden/QualifiedImports.hs | 1 + test/golden/RequalifiedImports.hs | 1 + 15 files changed, 120 insertions(+), 59 deletions(-) create mode 100644 test/Issue324.agda create mode 100644 test/Issue324instance.agda create mode 100644 test/golden/Issue324.hs create mode 100644 test/golden/Issue324instance.hs diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs index dee24025..c6595686 100644 --- a/src/Agda2Hs/Compile/ClassInstance.hs +++ b/src/Agda2Hs/Compile/ClassInstance.hs @@ -36,6 +36,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ ) import Agda2Hs.AgdaUtils import Agda2Hs.Compile.Function import Agda2Hs.Compile.Name +import Agda2Hs.Compile.Term import Agda2Hs.Compile.Type import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils diff --git a/src/Agda2Hs/Compile/Imports.hs b/src/Agda2Hs/Compile/Imports.hs index d8aef387..e7a0ffc3 100644 --- a/src/Agda2Hs/Compile/Imports.hs +++ b/src/Agda2Hs/Compile/Imports.hs @@ -25,10 +25,12 @@ type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()] compileImports top is0 = do - let is = filter (not . (top ==) . Hs.prettyPrint . importModule) is0 + let is = filter ((top /=) . Hs.prettyPrint . importModule) is0 checkClashingImports is let imps = Map.toList $ groupModules is - return $ map (uncurry $ uncurry makeImportDecl) imps + reportSLn "agda2hs.import" 10 $ "All imported modules: " ++ show (map (pp . fst . fst) imps) + let decls = map (uncurry $ uncurry makeImportDecl) imps + return decls where mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap mergeChildren = Map.unionWith Set.union @@ -38,18 +40,20 @@ compileImports top is0 = do makeSingle (Just p) q = Map.singleton p $ Set.singleton q groupModules :: [Import] -> ImportDeclMap - groupModules = foldr - (\(Import mod as p q ns) -> Map.insertWith mergeChildren (mod,as) - (makeSingle (parentNN p) (NamespacedName ns q))) - Map.empty - where - parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName - parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name - -- ^ for parents, if they are operators, we assume they are type operators - -- but actually, this will get lost anyway because of the structure of ImportSpec - -- the point is that there should not be two tuples with the same name and diffenrent namespaces - parentNN (Just name) = Just $ NamespacedName (Hs.NoNamespace ()) name - parentNN Nothing = Nothing + groupModules = flip foldr Map.empty $ \case + (Import mod as p q ns) -> + Map.insertWith mergeChildren (mod,as) + (makeSingle (parentNN p) (NamespacedName ns q)) + (ImportInstances mod) -> + Map.insertWith mergeChildren (mod,Unqualified) Map.empty + where + parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName + parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name + -- ^ for parents, if they are operators, we assume they are type operators + -- but actually, this will get lost anyway because of the structure of ImportSpec + -- the point is that there should not be two tuples with the same name and diffenrent namespaces + parentNN (Just name) = Just $ NamespacedName (Hs.NoNamespace ()) name + parentNN Nothing = Nothing -- TODO: avoid having to do this by having a CName instead of a -- Name in the Import datatype @@ -81,11 +85,13 @@ compileImports top is0 = do [] -> checkClashingImports is where isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q) + isClashing ImportInstances{} = False mkErrorMsg (Import _ _ p' q' _) = "Clashing import: " ++ pp q ++ " (both from " ++ prettyShow (pp <$> p) ++ " and " ++ prettyShow (pp <$> p') ++ ")" -- TODO: no range information as we only have Haskell names at this point + checkClashingImports (ImportInstances mod : is) = checkClashingImports is -- | Generate a prelude import considering prelude config options (hiding, implicit, etc). diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 0e1f7cf0..0a2e3dfc 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -230,3 +230,10 @@ compileModuleName m = do text "Top-level module name for" <+> prettyTCM m <+> text "is" <+> text (pp tlm) return tlm + +importInstance :: QName -> C () +importInstance f = do + mod <- compileModuleName $ qnameModule f + unless (isPrimModule mod) $ do + reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ pp mod + tellImport $ ImportInstances mod diff --git a/src/Agda2Hs/Compile/Term.hs b/src/Agda2Hs/Compile/Term.hs index e9a85db3..1e260508 100644 --- a/src/Agda2Hs/Compile/Term.hs +++ b/src/Agda2Hs/Compile/Term.hs @@ -2,6 +2,7 @@ module Agda2Hs.Compile.Term where import Control.Arrow ( (>>>), (&&&), second ) import Control.Monad ( unless, zipWithM ) +import Control.Monad.Except import Control.Monad.Reader import Data.Foldable ( toList ) @@ -19,11 +20,16 @@ import Agda.Syntax.Common import Agda.Syntax.Literal import Agda.Syntax.Internal +import Agda.TypeChecking.CheckInternal ( infer ) +import Agda.TypeChecking.Constraints ( noConstraints ) +import Agda.TypeChecking.Conversion ( equalTerm ) +import Agda.TypeChecking.InstanceArguments ( findInstance ) +import Agda.TypeChecking.MetaVars ( newInstanceMeta ) import Agda.TypeChecking.Monad import Agda.TypeChecking.Pretty import Agda.TypeChecking.Records ( shouldBeProjectible, isRecordType, recordFieldNames ) import Agda.TypeChecking.Datatypes ( getConType ) -import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate ) +import Agda.TypeChecking.Reduce ( unfoldDefinitionStep, instantiate, reduce ) import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope ( telView, mustBePi, piApplyM, flattenTel ) import Agda.TypeChecking.ProjectionLike ( reduceProjectionLike ) @@ -35,7 +41,7 @@ import Agda.Utils.Monad import Agda.Utils.Size import Agda2Hs.AgdaUtils -import Agda2Hs.Compile.Name ( compileQName ) +import Agda2Hs.Compile.Name ( compileQName, importInstance ) import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize ) import Agda2Hs.Compile.Types @@ -615,3 +621,42 @@ compileLiteral (LitChar c) = return $ Hs.charE c compileLiteral (LitString t) = return $ Hs.Lit () $ Hs.String () s s where s = Text.unpack t compileLiteral l = genericDocError =<< text "bad term:" prettyTCM (Lit l) + + +checkInstance :: Term -> C () +checkInstance u = do + reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u + reduce u >>= \case + Var x es -> do + unlessM (isInstance <$> domOfBV x) illegalInstance + checkInstanceElims es + Def f es -> do + unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance + importInstance f + checkInstanceElims es + -- We need to compile applications of `fromNat`, `fromNeg`, and + -- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally + -- this constraint would be marked as erased but this would involve + -- changing Agda builtins. + Con c _ _ + | prettyShow (conName c) == "Agda.Builtin.Unit.tt" || + prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" || + prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return () + _ -> illegalInstance + + where + illegalInstance :: C () + illegalInstance = do + reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u + genericDocError =<< text "illegal instance: " <+> prettyTCM u + + checkInstanceElims :: Elims -> C () + checkInstanceElims = mapM_ checkInstanceElim + + checkInstanceElim :: Elim -> C () + checkInstanceElim (Apply v) = + when (isInstance v && usableQuantity v) $ + checkInstance $ unArg v + checkInstanceElim IApply{} = illegalInstance + checkInstanceElim (Proj _ f) = + unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 473c34c6..2a51c178 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -108,15 +108,20 @@ qualifiedAs = join -- | Encoding of a Haskell module import statement. data Import = Import - { importModule :: Hs.ModuleName () - , importQualified :: Qualifier - , importParent :: Maybe (Hs.Name ()) - , importName :: Hs.Name () - , importNamespace :: Hs.Namespace () + { _importModule :: Hs.ModuleName () + , _importQualified :: Qualifier + , _importParent :: Maybe (Hs.Name ()) + , _importName :: Hs.Name () + , _importNamespace :: Hs.Namespace () -- ^^ if this is a type or something like that, we can add a namespace qualifier to the import spec -- now it's only useful for differentiating type operators; so for others we always put Hs.NoNamespace () here -- (we don't calculate it if it's not necessary) } + | ImportInstances (Hs.ModuleName ()) + +importModule :: Import -> Hs.ModuleName () +importModule (Import{ _importModule = mod }) = mod +importModule (ImportInstances mod) = mod type Imports = [Import] diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index 4193f1af..53dadd4d 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -253,43 +253,6 @@ isInlinedFunction q = do (InlinePragma ==) <$> processPragma r _ -> return False -checkInstance :: Term -> C () -checkInstance u = do - reportSDoc "agda2hs.checkInstance" 12 $ text "checkInstance" <+> prettyTCM u - reduce u >>= \case - Var x es -> do - unlessM (isInstance <$> domOfBV x) illegalInstance - checkInstanceElims es - Def f es -> do - unlessM (isJust . defInstance <$> getConstInfo f) illegalInstance - checkInstanceElims es - -- We need to compile applications of `fromNat`, `fromNeg`, and - -- `fromString` where the constraint type is ⊤ or IsTrue .... Ideally - -- this constraint would be marked as erased but this would involve - -- changing Agda builtins. - Con c _ _ - | prettyShow (conName c) == "Agda.Builtin.Unit.tt" || - prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" || - prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return () - _ -> illegalInstance - - where - illegalInstance :: C () - illegalInstance = do - reportSDoc "agda2hs.checkInstance" 15 $ text "illegal instance: " <+> pretty u - genericDocError =<< text "illegal instance: " <+> prettyTCM u - - checkInstanceElims :: Elims -> C () - checkInstanceElims = mapM_ checkInstanceElim - - checkInstanceElim :: Elim -> C () - checkInstanceElim (Apply v) = - when (isInstance v && usableQuantity v) $ - checkInstance $ unArg v - checkInstanceElim IApply{} = illegalInstance - checkInstanceElim (Proj _ f) = - unlessM (isInstance . defArgInfo <$> getConstInfo f) illegalInstance - withNestedType :: C a -> C a withNestedType = local $ \e -> e { isNestedInType = True } diff --git a/src/Agda2Hs/Render.hs b/src/Agda2Hs/Render.hs index 4cd979d2..d430bfc7 100644 --- a/src/Agda2Hs/Render.hs +++ b/src/Agda2Hs/Render.hs @@ -104,7 +104,7 @@ prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) = ++ parenList (map prettyShowSpec ispecs) parenList :: [String] -> String - parenList [] = "" + parenList [] = "()" parenList (x:xs) = '(' : (x ++ go xs) where go :: [String] -> String diff --git a/test/AllTests.agda b/test/AllTests.agda index 721e2fd6..84a701d2 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -92,6 +92,7 @@ import CustomTuples import ProjectionLike import FunCon import Issue308 +import Issue324 {-# FOREIGN AGDA2HS import Issue14 @@ -181,4 +182,5 @@ import CustomTuples import ProjectionLike import FunCon import Issue308 +import Issue324 #-} diff --git a/test/Issue324.agda b/test/Issue324.agda new file mode 100644 index 00000000..ce5ba72f --- /dev/null +++ b/test/Issue324.agda @@ -0,0 +1,8 @@ + +open import Haskell.Prelude +open import Issue324instance + +test : Bool +test = not == id + +{-# COMPILE AGDA2HS test #-} diff --git a/test/Issue324instance.agda b/test/Issue324instance.agda new file mode 100644 index 00000000..2cc4235a --- /dev/null +++ b/test/Issue324instance.agda @@ -0,0 +1,9 @@ + +open import Haskell.Prelude + +instance + eqBoolFun : Eq (Bool → Bool) + eqBoolFun ._==_ x y = x True == y True && x False == y False + +{-# COMPILE AGDA2HS eqBoolFun #-} + diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index 0f7d8576..bb75ed92 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -87,4 +87,5 @@ import CustomTuples import ProjectionLike import FunCon import Issue308 +import Issue324 diff --git a/test/golden/Issue324.hs b/test/golden/Issue324.hs new file mode 100644 index 00000000..786ec0d4 --- /dev/null +++ b/test/golden/Issue324.hs @@ -0,0 +1,7 @@ +module Issue324 where + +import Issue324instance () + +test :: Bool +test = not == id + diff --git a/test/golden/Issue324instance.hs b/test/golden/Issue324instance.hs new file mode 100644 index 00000000..0d9a7ecc --- /dev/null +++ b/test/golden/Issue324instance.hs @@ -0,0 +1,5 @@ +module Issue324instance where + +instance Eq (Bool -> Bool) where + x == y = x True == y True && x False == y False + diff --git a/test/golden/QualifiedImports.hs b/test/golden/QualifiedImports.hs index 96c2c666..48650f0c 100644 --- a/test/golden/QualifiedImports.hs +++ b/test/golden/QualifiedImports.hs @@ -1,6 +1,7 @@ module QualifiedImports where import qualified Importee (Foo(MkFoo), foo) +import QualifiedImportee () import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#)) -- ** simple qualification diff --git a/test/golden/RequalifiedImports.hs b/test/golden/RequalifiedImports.hs index 977169e0..86132144 100644 --- a/test/golden/RequalifiedImports.hs +++ b/test/golden/RequalifiedImports.hs @@ -1,6 +1,7 @@ module RequalifiedImports where import OtherImportee (OtherFoo(MkFoo)) +import QualifiedImportee () import qualified QualifiedImportee as A (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#)) -- ** conflicting imports are all replaced with the "smallest" qualifier