Skip to content

Commit 4a6ea21

Browse files
viktorcsimmaviktorcsimma
authored
Adding "type" prefix before type operator imports (#194)
* Initial version; the function deciding about the namespace does not work yet * Fixing the function determining the namespace of an operator * Rewriting the rendering of imports so that type operators always get their prefixes * Fixing an issue where there were multiple imports of the same identifier * Adding test and updating old ones (unfortunately, now it cannot break long lines) * Adding NamespacedName data * Using the built-in "isSort" function * Updating AllTests.agda
1 parent fcd2885 commit 4a6ea21

File tree

13 files changed

+186
-23
lines changed

13 files changed

+186
-23
lines changed

‎src/Agda2Hs/Compile/Imports.hs‎

Lines changed: 19 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ import Agda2Hs.Compile.Types
2020
import Agda2Hs.Compile.Utils
2121
import Agda2Hs.HsUtils
2222

23-
type ImportSpecMap = Map (Hs.Name ()) (Set (Hs.Name ()))
23+
type ImportSpecMap = Map NamespacedName (Set NamespacedName)
2424
type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap
2525

2626
compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()]
@@ -33,14 +33,23 @@ compileImports top is0 = do
3333
mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap
3434
mergeChildren = Map.unionWith Set.union
3535

36-
makeSingle :: Maybe (Hs.Name ()) -> Hs.Name () -> ImportSpecMap
36+
makeSingle :: Maybe NamespacedName -> NamespacedName -> ImportSpecMap
3737
makeSingle Nothing q = Map.singleton q Set.empty
3838
makeSingle (Just p) q = Map.singleton p $ Set.singleton q
3939

4040
groupModules :: [Import] -> ImportDeclMap
4141
groupModules = foldr
42-
(\(Import mod as p q) -> Map.insertWith mergeChildren (mod,as) (makeSingle p q))
42+
(\(Import mod as p q ns) -> Map.insertWith mergeChildren (mod,as)
43+
(makeSingle (parentNN p) (NamespacedName ns q)))
4344
Map.empty
45+
where
46+
parentNN :: Maybe (Hs.Name ()) -> Maybe NamespacedName
47+
parentNN (Just name@(Hs.Symbol _ _)) = Just $ NamespacedName (Hs.TypeNamespace ()) name
48+
-- ^ for parents, if they are operators, we assume they are type operators
49+
-- but actually, this will get lost anyway because of the structure of ImportSpec
50+
-- the point is that there should not be two tuples with the same name and diffenrent namespaces
51+
parentNN (Just name) = Just $ NamespacedName (Hs.NoNamespace ()) name
52+
parentNN Nothing = Nothing
4453

4554
-- TODO: avoid having to do this by having a CName instead of a
4655
-- Name in the Import datatype
@@ -52,10 +61,10 @@ compileImports top is0 = do
5261
| head s == ':' = Hs.ConName () n
5362
| otherwise = Hs.VarName () n
5463

55-
makeImportSpec :: Hs.Name () -> Set (Hs.Name ()) -> Hs.ImportSpec ()
56-
makeImportSpec q qs
57-
| Set.null qs = Hs.IVar () q
58-
| otherwise = Hs.IThingWith () q $ map makeCName $ Set.toList qs
64+
makeImportSpec :: NamespacedName -> Set NamespacedName -> Hs.ImportSpec ()
65+
makeImportSpec (NamespacedName namespace q) qs
66+
| Set.null qs = Hs.IAbs () namespace q
67+
| otherwise = Hs.IThingWith () q $ map (makeCName . nnName) $ Set.toList qs
5968

6069
makeImportDecl :: Hs.ModuleName () -> Qualifier -> ImportSpecMap -> Hs.ImportDecl ()
6170
makeImportDecl mod qual specs = Hs.ImportDecl ()
@@ -66,13 +75,13 @@ compileImports top is0 = do
6675

6776
checkClashingImports :: Imports -> TCM ()
6877
checkClashingImports [] = return ()
69-
checkClashingImports (Import mod as p q : is) =
78+
checkClashingImports (Import mod as p q _ : is) =
7079
case filter isClashing is of
7180
(i : _) -> genericDocError =<< text (mkErrorMsg i)
7281
[] -> checkClashingImports is
7382
where
74-
isClashing (Import _ as' p' q') = (as' == as) && (p' /= p) && (q' == q)
75-
mkErrorMsg (Import _ _ p' q') =
83+
isClashing (Import _ as' p' q' _) = (as' == as) && (p' /= p) && (q' == q)
84+
mkErrorMsg (Import _ _ p' q' _) =
7685
"Clashing import: " ++ pp q ++ " (both from "
7786
++ prettyShow (pp <$> p) ++ " and "
7887
++ prettyShow (pp <$> p') ++ ")"

‎src/Agda2Hs/Compile/Name.hs‎

Lines changed: 31 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ import Agda.Compiler.Backend hiding ( topLevelModuleName )
1414
import Agda.Compiler.Common ( topLevelModuleName )
1515

1616
import Agda.Syntax.Common
17+
import Agda.Syntax.Internal
1718
import Agda.Syntax.Position
1819
import qualified Agda.Syntax.Concrete as C
1920
import Agda.Syntax.Scope.Base ( inverseScopeLookupName )
@@ -65,7 +66,9 @@ isSpecialName f rules = let pretty = prettyShow f in case lookupRules pretty rul
6566
where
6667
noImport x = Just (hsName x, Nothing)
6768
withImport mod x =
68-
let imp = Import (hsModuleName mod) Unqualified Nothing (hsName x)
69+
let imp = Import (hsModuleName mod) Unqualified Nothing (hsName x) (Hs.NoNamespace ())
70+
-- ^ TODO: add an option to specify this in the config file (whether it is a type or not)
71+
-- as far as I know, there are no type operators in Prelude, but maybe a self-defined one could cause trouble
6972
in Just (hsName x, Just imp)
7073

7174
lookupRules :: String -> Rewrites -> Maybe (Hs.Name (), Maybe Import)
@@ -104,8 +107,13 @@ compileQName f
104107
|| prettyShow mod0 `elem` primMonadModules
105108
qual <- if | skipModule -> return Unqualified
106109
| otherwise -> getQualifier (fromMaybe f parent) mod
107-
let (mod', mimp) = mkImport mod qual par hf
108-
qf = qualify mod' hf qual
110+
-- we only calculate this when dealing with type operators; usually that's where 'type' prefixes are needed in imports
111+
namespace <- (case hf of
112+
Hs.Symbol _ _ -> getNamespace f
113+
Hs.Ident _ _ -> return (Hs.NoNamespace ()))
114+
let
115+
(mod', mimp) = mkImport mod qual par hf namespace
116+
qf = qualify mod' hf qual
109117

110118
-- add (possibly qualified) import
111119
whenJust (mimpBuiltin <|> mimp) tellImport
@@ -147,15 +155,32 @@ compileQName f
147155
primModules = ["Agda.Builtin", "Haskell.Prim", "Haskell.Prelude"]
148156
primMonadModules = ["Haskell.Prim.Monad.Dont", "Haskell.Prim.Monad.Do"]
149157

150-
mkImport mod qual par hf
158+
-- Determine whether it is a type operator or an "ordinary" operator.
159+
-- _getSort is not for that; e. g. a data has the same sort as its constructor.
160+
getNamespace :: QName -> C (Hs.Namespace ())
161+
getNamespace qName = do
162+
definition <- getConstInfo qName
163+
case isSort $ unEl $ getResultType $ defType definition of
164+
Just _ -> (reportSDoc "agda2hs.name" 25 $ text $ (prettyShow $ nameCanonical $ qnameName f)
165+
++ " is a type operator; will add \"type\" prefix before it") >>
166+
return (Hs.TypeNamespace ())
167+
_ -> return (Hs.NoNamespace ())
168+
169+
-- Gets the type of the result of the function (the type after the last "->").
170+
getResultType :: Type -> Type
171+
getResultType typ = case (unEl typ) of
172+
(Pi _ absType) -> getResultType $ unAbs absType
173+
_ -> typ
174+
175+
mkImport mod qual par hf maybeIsType
151176
-- make sure the Prelude is properly qualified
152177
| any (`isPrefixOf` pp mod) primModules
153178
= if isQualified qual then
154179
let mod' = hsModuleName "Prelude"
155-
in (mod', Just (Import mod' qual Nothing hf))
180+
in (mod', Just (Import mod' qual Nothing hf maybeIsType))
156181
else (mod, Nothing)
157182
| otherwise
158-
= (mod, Just (Import mod qual par hf))
183+
= (mod, Just (Import mod qual par hf maybeIsType))
159184

160185
hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName ()
161186
hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack

‎src/Agda2Hs/Compile/Types.hs‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -88,6 +88,10 @@ data Import = Import
8888
, importQualified :: Qualifier
8989
, importParent :: Maybe (Hs.Name ())
9090
, importName :: Hs.Name ()
91+
, importNamespace :: Hs.Namespace ()
92+
-- ^^ if this is a type or something like that, we can add a namespace qualifier to the import spec
93+
-- now it's only useful for differentiating type operators; so for others we always put Hs.NoNamespace () here
94+
-- (we don't calculate it if it's not necessary)
9195
}
9296
type Imports = [Import]
9397

@@ -130,3 +134,9 @@ data DataTarget = ToData | ToDataNewType
130134
data RecordTarget = ToRecord [Hs.Deriving ()] | ToRecordNewType [Hs.Deriving ()] | ToClass [String]
131135

132136
data InstanceTarget = ToDefinition | ToDerivation (Maybe (Hs.DerivStrategy ()))
137+
138+
-- Used when compiling imports. If there is a type operator, we can append a "type" namespace here.
139+
data NamespacedName = NamespacedName { nnNamespace :: Hs.Namespace (),
140+
nnName :: Hs.Name ()
141+
}
142+
deriving (Eq, Ord)

‎src/Agda2Hs/Render.hs‎

Lines changed: 48 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,53 @@ moduleSetup _ _ m _ = do
8484
ensureDirectory :: FilePath -> IO ()
8585
ensureDirectory = createDirectoryIfMissing True . takeDirectory
8686

87+
-- We have to rewrite this so that in the IThingAll and IThingWith import specs,
88+
-- the "type" prefixes get before type operators if necessary.
89+
-- But see haskell-src-exts, PR #475. If it gets merged, this will be unnecessary.
90+
prettyShowImportDecl :: Hs.ImportDecl () -> String
91+
prettyShowImportDecl (Hs.ImportDecl _ m qual src safe mbPkg mbName mbSpecs) =
92+
unwords $ ("import" :) $
93+
(if src then ("{-# SOURCE #-}" :) else id) $
94+
(if safe then ("safe" :) else id) $
95+
(if qual then ("qualified" :) else id) $
96+
maybeAppend (\ str -> show str) mbPkg $
97+
(pp m :) $
98+
maybeAppend (\m' -> "as " ++ pp m') mbName $
99+
(case mbSpecs of {Just specs -> [prettyShowSpecList specs]; Nothing -> []})
100+
where
101+
maybeAppend :: (a -> String) -> Maybe a -> ([String] -> [String])
102+
maybeAppend f (Just a) = (f a :)
103+
maybeAppend _ Nothing = id
104+
105+
prettyShowSpecList :: Hs.ImportSpecList () -> String
106+
prettyShowSpecList (Hs.ImportSpecList _ b ispecs) =
107+
(if b then "hiding " else "")
108+
++ parenList (map prettyShowSpec ispecs)
109+
110+
parenList :: [String] -> String
111+
parenList [] = ""
112+
parenList (x:xs) = '(' : (x ++ go xs)
113+
where
114+
go :: [String] -> String
115+
go [] = ")"
116+
go (x:xs) = ", " ++ x ++ go xs
117+
118+
-- this is why we have rewritten it
119+
prettyShowSpec :: Hs.ImportSpec () -> String
120+
prettyShowSpec (Hs.IVar _ name ) = pp name
121+
prettyShowSpec (Hs.IAbs _ ns name) = let ppns = pp ns in case ppns of
122+
[] -> pp name -- then we don't write a space before it
123+
_ -> ppns ++ (' ' : pp name)
124+
prettyShowSpec (Hs.IThingAll _ name) = let rest = pp name ++ "(..)" in
125+
case name of
126+
-- if it's a symbol, append a "type" prefix to the beginning
127+
(Hs.Symbol _ _) -> pp (Hs.TypeNamespace ()) ++ (' ' : rest)
128+
(Hs.Ident _ _) -> rest
129+
prettyShowSpec (Hs.IThingWith _ name nameList) = let rest = pp name ++ (parenList . map pp $ nameList) in
130+
case name of
131+
(Hs.Symbol _ _) -> pp (Hs.TypeNamespace ()) ++ (' ' : rest)
132+
(Hs.Ident _ _) -> rest
133+
87134
writeModule :: Options -> ModuleEnv -> IsMain -> TopLevelModuleName
88135
-> [(CompiledDef, CompileOutput)] -> TCM ModuleRes
89136
writeModule opts _ isMain m outs = do
@@ -108,7 +155,7 @@ writeModule opts _ isMain m outs = do
108155
(pure $ makeManualDecl (Hs.prelude_mod ()) Nothing isImplicit names) <*>
109156
compileImports mod filteredImps
110157
(True, Auto) -> __IMPOSSIBLE__
111-
autoImports <- (unlines' . map pp) <$> autoImportList
158+
autoImports <- (unlines' . map prettyShowImportDecl) <$> autoImportList
112159
-- The comments make it hard to generate and pretty print a full module
113160
hsFile <- moduleFileName opts m
114161
let output = concat

‎test/AllTests.agda‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,8 @@ import LawfulOrd
5252
import Deriving
5353
import ErasedLocalDefinitions
5454
import TypeOperators
55+
import TypeOperatorExport
56+
import TypeOperatorImport
5557

5658
{-# FOREIGN AGDA2HS
5759
import Issue14
@@ -102,4 +104,8 @@ import WitnessedFlows
102104
import Kinds
103105
import LawfulOrd
104106
import Deriving
107+
import ErasedLocalDefinitions
108+
import TypeOperators
109+
import TypeOperatorExport
110+
import TypeOperatorImport
105111
#-}

‎test/TypeOperatorExport.agda‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
module TypeOperatorExport where
2+
3+
{-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-}
4+
5+
open import Agda.Primitive
6+
7+
_<_ : Set -> Set -> Set
8+
a < b = a
9+
{-# COMPILE AGDA2HS _<_ #-}
10+
11+
data _***_ {i j : Level} (a : Set i) (b : Set j) : Set (i ⊔ j) where
12+
_:*:_ : a -> b -> a *** b
13+
open _***_ public
14+
{-# COMPILE AGDA2HS _***_ #-}
15+
16+
open import Agda.Builtin.Bool
17+
18+
_&&&_ : Bool -> Bool -> Bool
19+
false &&& _ = false
20+
_ &&& b2 = b2
21+
{-# COMPILE AGDA2HS _&&&_ #-}

‎test/TypeOperatorImport.agda‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
module TypeOperatorImport where
2+
3+
{-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-}
4+
5+
open import Agda.Builtin.Unit
6+
open import Agda.Builtin.Bool
7+
open import Haskell.Prelude using (_∘_)
8+
open import TypeOperatorExport
9+
10+
not : Bool → Bool
11+
not true = false
12+
not false = true
13+
14+
test1 : ⊤ < Bool
15+
test1 = tt
16+
{-# COMPILE AGDA2HS test1 #-}
17+
18+
test2 : Bool -> Bool -> ⊤ *** Bool
19+
test2 b1 b2 = ((tt :*:_) ∘ not) (b1 &&& b2)
20+
{-# COMPILE AGDA2HS test2 #-}

‎test/golden/AllTests.hs‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -48,4 +48,8 @@ import WitnessedFlows
4848
import Kinds
4949
import LawfulOrd
5050
import Deriving
51+
import ErasedLocalDefinitions
52+
import TypeOperators
53+
import TypeOperatorExport
54+
import TypeOperatorImport
5155

‎test/golden/Importer.hs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
module Importer where
22

3-
import Importee
4-
(Foo(MkFoo), Fooable(defaultFoo, doTheFoo), foo, (!#))
3+
import Importee (Foo(MkFoo), Fooable(defaultFoo, doTheFoo), foo, (!#))
54
import Numeric.Natural (Natural)
65
import SecondImportee (anotherFoo)
76

‎test/golden/QualifiedImports.hs‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
module QualifiedImports where
22

33
import qualified Importee (Foo(MkFoo), foo)
4-
import qualified QualifiedImportee as Qually
5-
(Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
4+
import qualified QualifiedImportee as Qually (Foo, Fooable(defaultFoo, doTheFoo), foo, (!#))
65

76
-- ** simple qualification
87

0 commit comments

Comments
 (0)