Adding "type" prefix before type operator imports

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 (Hs.Name (), Hs.Namespace ()) (Set (Hs.Name (), Hs.Namespace ()))
 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 (Hs.Name (), Hs.Namespace ()) -> (Hs.Name (), Hs.Namespace ()) -> 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 (parentTuple p) (q, ns)))
       Map.empty
+        where
+          parentTuple :: Maybe (Hs.Name ()) -> Maybe (Hs.Name (), Hs.Namespace ())
+          parentTuple (Just name@(Hs.Symbol _ _)) = Just (name, Hs.TypeNamespace ())
+                                                             -- ^ 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
+          parentTuple (Just name)                 = Just (name, Hs.NoNamespace ())
+          parentTuple 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 :: (Hs.Name (), Hs.Namespace ()) -> Set (Hs.Name (), Hs.Namespace ()) -> Hs.ImportSpec ()
+    makeImportSpec (q, namespace) qs
+      | Set.null qs = Hs.IAbs () namespace q
+      | otherwise   = Hs.IThingWith () q $ map (makeCName . fst) $ 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') ++ ")"

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,37 @@ 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
+      let isQNameSet = isSet $ getResultType $ defType definition
+      reportSDoc "agda2hs.name" 25 $ text $ "Checking whether " ++ (prettyShow $ nameCanonical $ qnameName f)
+                                              ++ "is a type operator: " ++ show isQNameSet
+      if isQNameSet then return (Hs.TypeNamespace ()) else 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
+
+    -- I'm not sure whether this is the correct way to determine whether it's a Set/Prop;
+    -- but this is my best bet.
+    isSet :: Type -> Bool
+    isSet (El _ (Sort _)) = True
+    isSet _               = False
+
+    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

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]
 

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

test/AllTests.agda

@@ -52,6 +52,8 @@ import LawfulOrd
 import Deriving
 import ErasedLocalDefinitions
 import TypeOperators
+import TypeOperatorExport
+import TypeOperatorImport
 
 {-# FOREIGN AGDA2HS
 import Issue14

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 _&&&_ #-}

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 #-}

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)
 

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
 

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)

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
+

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)
+