diff --git a/src/Agda2Hs/Compile/Imports.hs b/src/Agda2Hs/Compile/Imports.hs index 8a2127ae..d81f5afb 100644 --- a/src/Agda2Hs/Compile/Imports.hs +++ b/src/Agda2Hs/Compile/Imports.hs @@ -20,7 +20,7 @@ import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils -type ImportSpecMap = Map (Hs.Name ()) (Set (Hs.Name ())) +type ImportSpecMap = Map NamespacedName (Set NamespacedName) type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()] @@ -33,14 +33,23 @@ compileImports top is0 = do mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap mergeChildren = Map.unionWith Set.union - makeSingle :: Maybe (Hs.Name ()) -> Hs.Name () -> ImportSpecMap + makeSingle :: Maybe NamespacedName -> NamespacedName -> ImportSpecMap makeSingle Nothing q = Map.singleton q Set.empty makeSingle (Just p) q = Map.singleton p $ Set.singleton q groupModules :: [Import] -> ImportDeclMap groupModules = foldr - (\(Import mod as p q) -> Map.insertWith mergeChildren (mod,as) (makeSingle p q)) + (\(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 -- TODO: avoid having to do this by having a CName instead of a -- Name in the Import datatype @@ -52,10 +61,10 @@ compileImports top is0 = do | head s == ':' = Hs.ConName () n | otherwise = Hs.VarName () n - makeImportSpec :: Hs.Name () -> Set (Hs.Name ()) -> Hs.ImportSpec () - makeImportSpec q qs - | Set.null qs = Hs.IVar () q - | otherwise = Hs.IThingWith () q $ map makeCName $ Set.toList qs + makeImportSpec :: NamespacedName -> Set NamespacedName -> Hs.ImportSpec () + makeImportSpec (NamespacedName namespace q) qs + | Set.null qs = Hs.IAbs () namespace q + | otherwise = Hs.IThingWith () q $ map (makeCName . nnName) $ Set.toList qs makeImportDecl :: Hs.ModuleName () -> Qualifier -> ImportSpecMap -> Hs.ImportDecl () makeImportDecl mod qual specs = Hs.ImportDecl () @@ -66,13 +75,13 @@ compileImports top is0 = do checkClashingImports :: Imports -> TCM () checkClashingImports [] = return () - checkClashingImports (Import mod as p q : is) = + checkClashingImports (Import mod as p q _ : is) = case filter isClashing is of (i : _) -> genericDocError =<< text (mkErrorMsg i) [] -> checkClashingImports is where - isClashing (Import _ as' p' q') = (as' == as) && (p' /= p) && (q' == q) - mkErrorMsg (Import _ _ p' q') = + isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q) + mkErrorMsg (Import _ _ p' q' _) = "Clashing import: " ++ pp q ++ " (both from " ++ prettyShow (pp <$> p) ++ " and " ++ prettyShow (pp <$> p') ++ ")" diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 5fd96020..1b022774 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -14,6 +14,7 @@ import Agda.Compiler.Backend hiding ( topLevelModuleName ) import Agda.Compiler.Common ( topLevelModuleName ) 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 ) @@ -65,7 +66,9 @@ isSpecialName f rules = let pretty = prettyShow f in case lookupRules pretty rul where noImport x = Just (hsName x, Nothing) withImport mod x = - let imp = Import (hsModuleName mod) Unqualified Nothing (hsName x) + let imp = Import (hsModuleName mod) Unqualified Nothing (hsName x) (Hs.NoNamespace ()) + -- ^ TODO: add an option to specify this in the config file (whether it is a type or not) + -- as far as I know, there are no type operators in Prelude, but maybe a self-defined one could cause trouble in Just (hsName x, Just imp) lookupRules :: String -> Rewrites -> Maybe (Hs.Name (), Maybe Import) @@ -104,8 +107,13 @@ compileQName f || prettyShow mod0 `elem` primMonadModules qual <- if | skipModule -> return Unqualified | otherwise -> getQualifier (fromMaybe f parent) mod - let (mod', mimp) = mkImport mod qual par hf - qf = qualify mod' hf qual + -- we only calculate this when dealing with type operators; usually that's where 'type' prefixes are needed in imports + namespace <- (case hf of + Hs.Symbol _ _ -> getNamespace f + Hs.Ident _ _ -> return (Hs.NoNamespace ())) + let + (mod', mimp) = mkImport mod qual par hf namespace + qf = qualify mod' hf qual -- add (possibly qualified) import whenJust (mimpBuiltin <|> mimp) tellImport @@ -147,15 +155,32 @@ compileQName f primModules = ["Agda.Builtin", "Haskell.Prim", "Haskell.Prelude"] primMonadModules = ["Haskell.Prim.Monad.Dont", "Haskell.Prim.Monad.Do"] - mkImport mod qual par hf + -- Determine whether it is a type operator or an "ordinary" operator. + -- _getSort is not for that; e. g. a data has the same sort as its constructor. + getNamespace :: QName -> C (Hs.Namespace ()) + getNamespace qName = do + definition <- getConstInfo qName + case isSort $ unEl $ getResultType $ defType definition of + Just _ -> (reportSDoc "agda2hs.name" 25 $ text $ (prettyShow $ nameCanonical $ qnameName f) + ++ " is a type operator; will add \"type\" prefix before it") >> + return (Hs.TypeNamespace ()) + _ -> return (Hs.NoNamespace ()) + + -- Gets the type of the result of the function (the type after the last "->"). + getResultType :: Type -> Type + getResultType typ = case (unEl typ) of + (Pi _ absType) -> getResultType $ unAbs absType + _ -> typ + + mkImport mod qual par hf maybeIsType -- make sure the Prelude is properly qualified | any (`isPrefixOf` pp mod) primModules = if isQualified qual then let mod' = hsModuleName "Prelude" - in (mod', Just (Import mod' qual Nothing hf)) + in (mod', Just (Import mod' qual Nothing hf maybeIsType)) else (mod, Nothing) | otherwise - = (mod, Just (Import mod qual par hf)) + = (mod, Just (Import mod qual par hf maybeIsType)) hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName () hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 8a9a9c59..3c25a566 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -88,6 +88,10 @@ data Import = Import , 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) } type Imports = [Import] @@ -130,3 +134,9 @@ data DataTarget = ToData | ToDataNewType data RecordTarget = ToRecord [Hs.Deriving ()] | ToRecordNewType [Hs.Deriving ()] | ToClass [String] data InstanceTarget = ToDefinition | ToDerivation (Maybe (Hs.DerivStrategy ())) + +-- Used when compiling imports. If there is a type operator, we can append a "type" namespace here. +data NamespacedName = NamespacedName { nnNamespace :: Hs.Namespace (), + nnName :: Hs.Name () + } + deriving (Eq, Ord) diff --git a/src/Agda2Hs/Render.hs b/src/Agda2Hs/Render.hs index 0dd6cbf0..1f21072a 100644 --- a/src/Agda2Hs/Render.hs +++ b/src/Agda2Hs/Render.hs @@ -84,6 +84,53 @@ moduleSetup _ _ m _ = do ensureDirectory :: FilePath -> IO () ensureDirectory = createDirectoryIfMissing True . takeDirectory +-- We have to rewrite this so that in the IThingAll and IThingWith import specs, +-- the "type" prefixes get before type operators if necessary. +-- But see haskell-src-exts, PR #475. If it gets merged, this will be unnecessary. +prettyShowImportDecl :: Hs.ImportDecl () -> String +prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) = + unwords $ ("import" :) $ + (if src then ("{-# SOURCE #-}" :) else id) $ + (if safe then ("safe" :) else id) $ + (if qual then ("qualified" :) else id) $ + maybeAppend (\ str -> show str) mbPkg $ + (pp m :) $ + maybeAppend (\m' -> "as " ++ pp m') mbName $ + (case mbSpecs of {Just specs -> [prettyShowSpecList specs]; Nothing -> []}) + where + maybeAppend :: (a -> String) -> Maybe a -> ([String] -> [String]) + maybeAppend f (Just a) = (f a :) + maybeAppend _ Nothing = id + + prettyShowSpecList :: Hs.ImportSpecList () -> String + prettyShowSpecList (Hs.ImportSpecList _ b ispecs) = + (if b then "hiding " else "") + ++ parenList (map prettyShowSpec ispecs) + + parenList :: [String] -> String + parenList [] = "" + parenList (x:xs) = '(' : (x ++ go xs) + where + go :: [String] -> String + go [] = ")" + go (x:xs) = ", " ++ x ++ go xs + + -- this is why we have rewritten it + prettyShowSpec :: Hs.ImportSpec () -> String + prettyShowSpec (Hs.IVar _ name ) = pp name + prettyShowSpec (Hs.IAbs _ ns name) = let ppns = pp ns in case ppns of + [] -> pp name -- then we don't write a space before it + _ -> ppns ++ (' ' : pp name) + prettyShowSpec (Hs.IThingAll _ name) = let rest = pp name ++ "(..)" in + case name of + -- if it's a symbol, append a "type" prefix to the beginning + (Hs.Symbol _ _) -> pp (Hs.TypeNamespace ()) ++ (' ' : rest) + (Hs.Ident _ _) -> rest + prettyShowSpec (Hs.IThingWith _ name nameList) = let rest = pp name ++ (parenList . map pp $ nameList) in + case name of + (Hs.Symbol _ _) -> pp (Hs.TypeNamespace ()) ++ (' ' : rest) + (Hs.Ident _ _) -> rest + writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName -> [(CompiledDef, CompileOutput)] -> TCM ModuleRes writeModule opts _ isMain m outs = do @@ -108,7 +155,7 @@ writeModule opts _ isMain m outs = do (pure $ makeManualDecl (Hs.prelude_mod ()) Nothing isImplicit names) <*> compileImports mod filteredImps (True, Auto) -> __IMPOSSIBLE__ - autoImports <- (unlines' . map pp) <$> autoImportList + autoImports <- (unlines' . map prettyShowImportDecl) <$> autoImportList -- The comments make it hard to generate and pretty print a full module hsFile <- moduleFileName opts m let output = concat diff --git a/test/AllTests.agda b/test/AllTests.agda index bbce2111..b1035642 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -52,6 +52,8 @@ import LawfulOrd import Deriving import ErasedLocalDefinitions import TypeOperators +import TypeOperatorExport +import TypeOperatorImport {-# FOREIGN AGDA2HS import Issue14 @@ -102,4 +104,8 @@ import WitnessedFlows import Kinds import LawfulOrd import Deriving +import ErasedLocalDefinitions +import TypeOperators +import TypeOperatorExport +import TypeOperatorImport #-} diff --git a/test/TypeOperatorExport.agda b/test/TypeOperatorExport.agda new file mode 100644 index 00000000..c3ee0601 --- /dev/null +++ b/test/TypeOperatorExport.agda @@ -0,0 +1,21 @@ +module TypeOperatorExport where + +{-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-} + +open import Agda.Primitive + +_<_ : Set -> Set -> Set +a < b = a +{-# COMPILE AGDA2HS _<_ #-} + +data _***_ {i j : Level} (a : Set i) (b : Set j) : Set (i ⊔ j) where + _:*:_ : a -> b -> a *** b +open _***_ public +{-# COMPILE AGDA2HS _***_ #-} + +open import Agda.Builtin.Bool + +_&&&_ : Bool -> Bool -> Bool +false &&& _ = false +_ &&& b2 = b2 +{-# COMPILE AGDA2HS _&&&_ #-} diff --git a/test/TypeOperatorImport.agda b/test/TypeOperatorImport.agda new file mode 100644 index 00000000..42520d1a --- /dev/null +++ b/test/TypeOperatorImport.agda @@ -0,0 +1,20 @@ +module TypeOperatorImport where + +{-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-} + +open import Agda.Builtin.Unit +open import Agda.Builtin.Bool +open import Haskell.Prelude using (_∘_) +open import TypeOperatorExport + +not : Bool → Bool +not true = false +not false = true + +test1 : ⊤ < Bool +test1 = tt +{-# COMPILE AGDA2HS test1 #-} + +test2 : Bool -> Bool -> ⊤ *** Bool +test2 b1 b2 = ((tt :*:_) ∘ not) (b1 &&& b2) +{-# COMPILE AGDA2HS test2 #-} diff --git a/test/golden/AllTests.hs b/test/golden/AllTests.hs index f911ce3c..d3cf5d4a 100644 --- a/test/golden/AllTests.hs +++ b/test/golden/AllTests.hs @@ -48,4 +48,8 @@ import WitnessedFlows import Kinds import LawfulOrd import Deriving +import ErasedLocalDefinitions +import TypeOperators +import TypeOperatorExport +import TypeOperatorImport diff --git a/test/golden/Importer.hs b/test/golden/Importer.hs index d55f793a..17aff23c 100644 --- a/test/golden/Importer.hs +++ b/test/golden/Importer.hs @@ -1,7 +1,6 @@ module Importer where -import Importee - (Foo(MkFoo), Fooable(defaultFoo, doTheFoo), foo, (!#)) +import Importee (Foo(MkFoo), Fooable(defaultFoo, doTheFoo), foo, (!#)) import Numeric.Natural (Natural) import SecondImportee (anotherFoo) diff --git a/test/golden/QualifiedImports.hs b/test/golden/QualifiedImports.hs index 5b55f8c7..7a6a1a8a 100644 --- a/test/golden/QualifiedImports.hs +++ b/test/golden/QualifiedImports.hs @@ -1,8 +1,7 @@ module QualifiedImports where import qualified Importee (Foo(MkFoo), foo) -import qualified QualifiedImportee as Qually - (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#)) +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 e160ebdd..977169e0 100644 --- a/test/golden/RequalifiedImports.hs +++ b/test/golden/RequalifiedImports.hs @@ -1,8 +1,7 @@ module RequalifiedImports where import OtherImportee (OtherFoo(MkFoo)) -import qualified QualifiedImportee as A - (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#)) +import qualified QualifiedImportee as A (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#)) -- ** conflicting imports are all replaced with the "smallest" qualifier -- * the characters are ordered based on their ASCII value (i.e. capitals first) diff --git a/test/golden/TypeOperatorExport.hs b/test/golden/TypeOperatorExport.hs new file mode 100644 index 00000000..ab9c3dc8 --- /dev/null +++ b/test/golden/TypeOperatorExport.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeOperators #-} + +module TypeOperatorExport where + +type (<) a b = a + +data (***) a b = (:*:) a b + +(&&&) :: Bool -> Bool -> Bool +False &&& _ = False +_ &&& b2 = b2 + diff --git a/test/golden/TypeOperatorImport.hs b/test/golden/TypeOperatorImport.hs new file mode 100644 index 00000000..cd0beab7 --- /dev/null +++ b/test/golden/TypeOperatorImport.hs @@ -0,0 +1,12 @@ +{-# LANGUAGE TypeOperators #-} + +module TypeOperatorImport where + +import TypeOperatorExport ((&&&), type (***)((:*:)), type (<)) + +test1 :: (<) () Bool +test1 = () + +test2 :: Bool -> Bool -> (***) () Bool +test2 b1 b2 = ((() :*:) . not) (b1 &&& b2) +