From 941c41db74833ade3830b54715877fa893f8edaa Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Sat, 22 Jul 2023 18:06:28 +0200 Subject: [PATCH 1/8] Initial version; the function deciding about the namespace does not work yet --- src/Agda2Hs/Compile/Imports.hs | 29 +++++++++++++++++++---------- src/Agda2Hs/Compile/Name.hs | 33 ++++++++++++++++++++++++++++----- src/Agda2Hs/Compile/Types.hs | 4 ++++ test/AllTests.agda | 2 ++ test/TypeOperatorExport.agda | 21 +++++++++++++++++++++ test/TypeOperatorImport.agda | 15 +++++++++++++++ 6 files changed, 89 insertions(+), 15 deletions(-) create mode 100644 test/TypeOperatorExport.agda create mode 100644 test/TypeOperatorImport.agda diff --git a/src/Agda2Hs/Compile/Imports.hs b/src/Agda2Hs/Compile/Imports.hs index 8a2127ae..b0d7e804 100644 --- a/src/Agda2Hs/Compile/Imports.hs +++ b/src/Agda2Hs/Compile/Imports.hs @@ -20,7 +20,9 @@ import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils -type ImportSpecMap = Map (Hs.Name ()) (Set (Hs.Name ())) +type MaybeNamespace = Maybe (Hs.Namespace ()) -- just for shortening + +type ImportSpecMap = Map (Hs.Name (), MaybeNamespace) (Set (Hs.Name (), MaybeNamespace)) type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()] @@ -33,14 +35,19 @@ compileImports top is0 = do mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap mergeChildren = Map.unionWith Set.union - makeSingle :: Maybe (Hs.Name ()) -> Hs.Name () -> ImportSpecMap + makeSingle :: Maybe (Hs.Name (), MaybeNamespace) -> (Hs.Name (), MaybeNamespace) -> 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 mIT) -> Map.insertWith mergeChildren (mod,as) + (makeSingle (parentTuple p) (q, mIT))) Map.empty + where + parentTuple :: Maybe (Hs.Name ()) -> Maybe (Hs.Name (), MaybeNamespace) + parentTuple (Just name) = Just (name, Just (Hs.TypeNamespace ())) -- for parents, we assume they are typeclasses or datatypes + parentTuple Nothing = Nothing -- TODO: avoid having to do this by having a CName instead of a -- Name in the Import datatype @@ -52,10 +59,12 @@ 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 (), MaybeNamespace) -> Set (Hs.Name (), MaybeNamespace) -> Hs.ImportSpec () + makeImportSpec (q, maybeNamespace) qs + | Set.null qs = case maybeNamespace of + Just namespace -> Hs.IAbs () namespace q + _ -> Hs.IVar () q -- if we don't know, we treat it as a value + | 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') ++ ")" diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 5fd96020..8c02ec00 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,8 @@ 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) Nothing + -- ^ maybe we should add an option to specify this in the config file (whether it is a type or not) in Just (hsName x, Just imp) lookupRules :: String -> Rewrites -> Maybe (Hs.Name (), Maybe Import) @@ -104,7 +106,11 @@ 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 + -- we only calculate this when dealing with type operators; usually that's where 'type' prefixes are needed in imports + maybeNamespace <- (case hf of + Hs.Symbol _ _ -> Just <$> getNamespace f + Hs.Ident _ _ -> return Nothing) + let (mod', mimp) = mkImport mod qual par hf maybeNamespace qf = qualify mod' hf qual -- add (possibly qualified) import @@ -147,15 +153,32 @@ compileQName f primModules = ["Agda.Builtin", "Haskell.Prim", "Haskell.Prelude"] primMonadModules = ["Haskell.Prim.Monad.Dont", "Haskell.Prim.Monad.Do"] - mkImport mod qual par hf + getNamespace :: QName -> C (Hs.Namespace ()) + getNamespace qName = do + definition <- getConstInfo qName + let sort = _getSort $ defType definition + -- TODO: this doesn't work well + -- maybe it believes Prelude functions to have a higher level than in reality + return (case sort of + Type (Max l _) -> intToNamespace l + Prop (Max l _) -> intToNamespace l + SSet (Max l _) -> intToNamespace l + a -> Hs.TypeNamespace ()) -- error $ show a ++ show f) -- we do not try to elaborate further at this point + where + intToNamespace :: Integer -> Hs.Namespace () + intToNamespace l + | l <= 1 = Hs.NoNamespace () -- is this the way of checking whether it's a value? I'm not sure + | otherwise = Hs.TypeNamespace () + + 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..4500f4c3 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 :: Maybe (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; hence the "Maybe" + -- (we don't calculate it if it's not necessary) } type Imports = [Import] diff --git a/test/AllTests.agda b/test/AllTests.agda index bbce2111..15e39de4 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 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..142cb1ac --- /dev/null +++ b/test/TypeOperatorImport.agda @@ -0,0 +1,15 @@ +module TypeOperatorImport where + +{-# FOREIGN AGDA2HS {-# LANGUAGE TypeOperators #-} #-} + +open import Agda.Builtin.Unit +open import Agda.Builtin.Bool +open import TypeOperatorExport + +test1 : ⊤ < Bool +test1 = tt +{-# COMPILE AGDA2HS test1 #-} + +test2 : Bool -> Bool -> ⊤ *** Bool +test2 b1 b2 = tt :*: (b1 &&& b2) +{-# COMPILE AGDA2HS test2 #-} From 091369643d323106f2d71d8ca951a56c1795a6d7 Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Sun, 23 Jul 2023 11:41:45 +0200 Subject: [PATCH 2/8] Fixing the function determining the namespace of an operator --- src/Agda2Hs/Compile/Name.hs | 31 ++++++++++++++++++------------- 1 file changed, 18 insertions(+), 13 deletions(-) diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 8c02ec00..c03e4b9e 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -153,22 +153,27 @@ compileQName f primModules = ["Agda.Builtin", "Haskell.Prim", "Haskell.Prelude"] primMonadModules = ["Haskell.Prim.Monad.Dont", "Haskell.Prim.Monad.Do"] + -- 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 sort = _getSort $ defType definition - -- TODO: this doesn't work well - -- maybe it believes Prelude functions to have a higher level than in reality - return (case sort of - Type (Max l _) -> intToNamespace l - Prop (Max l _) -> intToNamespace l - SSet (Max l _) -> intToNamespace l - a -> Hs.TypeNamespace ()) -- error $ show a ++ show f) -- we do not try to elaborate further at this point - where - intToNamespace :: Integer -> Hs.Namespace () - intToNamespace l - | l <= 1 = Hs.NoNamespace () -- is this the way of checking whether it's a value? I'm not sure - | otherwise = Hs.TypeNamespace () + 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 From 09a3588ef24066f0ee3d23b20f6ce087f7d6862a Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Sun, 23 Jul 2023 12:31:53 +0200 Subject: [PATCH 3/8] Rewriting the rendering of imports so that type operators always get their prefixes --- src/Agda2Hs/Render.hs | 49 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 48 insertions(+), 1 deletion(-) 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 From e36bcbeaa6bc6549e1b4b6d56f3c082a29154f71 Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Mon, 24 Jul 2023 10:50:02 +0200 Subject: [PATCH 4/8] Fixing an issue where there were multiple imports of the same identifier --- src/Agda2Hs/Compile/Imports.hs | 26 +++++++++++++------------- src/Agda2Hs/Compile/Name.hs | 16 +++++++++------- src/Agda2Hs/Compile/Types.hs | 4 ++-- 3 files changed, 24 insertions(+), 22 deletions(-) diff --git a/src/Agda2Hs/Compile/Imports.hs b/src/Agda2Hs/Compile/Imports.hs index b0d7e804..ae9a0694 100644 --- a/src/Agda2Hs/Compile/Imports.hs +++ b/src/Agda2Hs/Compile/Imports.hs @@ -20,9 +20,7 @@ import Agda2Hs.Compile.Types import Agda2Hs.Compile.Utils import Agda2Hs.HsUtils -type MaybeNamespace = Maybe (Hs.Namespace ()) -- just for shortening - -type ImportSpecMap = Map (Hs.Name (), MaybeNamespace) (Set (Hs.Name (), MaybeNamespace)) +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 ()] @@ -35,18 +33,22 @@ compileImports top is0 = do mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap mergeChildren = Map.unionWith Set.union - makeSingle :: Maybe (Hs.Name (), MaybeNamespace) -> (Hs.Name (), MaybeNamespace) -> 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 mIT) -> Map.insertWith mergeChildren (mod,as) - (makeSingle (parentTuple p) (q, mIT))) + (\(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 (), MaybeNamespace) - parentTuple (Just name) = Just (name, Just (Hs.TypeNamespace ())) -- for parents, we assume they are typeclasses or datatypes + 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 @@ -59,11 +61,9 @@ compileImports top is0 = do | head s == ':' = Hs.ConName () n | otherwise = Hs.VarName () n - makeImportSpec :: (Hs.Name (), MaybeNamespace) -> Set (Hs.Name (), MaybeNamespace) -> Hs.ImportSpec () - makeImportSpec (q, maybeNamespace) qs - | Set.null qs = case maybeNamespace of - Just namespace -> Hs.IAbs () namespace q - _ -> Hs.IVar () q -- if we don't know, we treat it as a value + 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 () diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index c03e4b9e..595a2ca2 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -66,8 +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) Nothing - -- ^ maybe we should add an option to specify this in the config file (whether it is a type or not) + 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) @@ -107,11 +108,12 @@ compileQName f qual <- if | skipModule -> return Unqualified | otherwise -> getQualifier (fromMaybe f parent) mod -- we only calculate this when dealing with type operators; usually that's where 'type' prefixes are needed in imports - maybeNamespace <- (case hf of - Hs.Symbol _ _ -> Just <$> getNamespace f - Hs.Ident _ _ -> return Nothing) - let (mod', mimp) = mkImport mod qual par hf maybeNamespace - qf = qualify mod' hf qual + 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 diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 4500f4c3..8aada58e 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -88,9 +88,9 @@ data Import = Import , importQualified :: Qualifier , importParent :: Maybe (Hs.Name ()) , importName :: Hs.Name () - , importNamespace :: Maybe (Hs.Namespace ()) + , 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; hence the "Maybe" + -- 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] From b5f671e3fd0d2f50ccd3b92ae0aa5a2643000bc4 Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Mon, 24 Jul 2023 10:51:00 +0200 Subject: [PATCH 5/8] Adding test and updating old ones (unfortunately, now it cannot break long lines) --- test/TypeOperatorImport.agda | 7 ++++++- test/golden/Importer.hs | 3 +-- test/golden/QualifiedImports.hs | 3 +-- test/golden/RequalifiedImports.hs | 3 +-- test/golden/TypeOperatorExport.hs | 12 ++++++++++++ test/golden/TypeOperatorImport.hs | 12 ++++++++++++ 6 files changed, 33 insertions(+), 7 deletions(-) create mode 100644 test/golden/TypeOperatorExport.hs create mode 100644 test/golden/TypeOperatorImport.hs diff --git a/test/TypeOperatorImport.agda b/test/TypeOperatorImport.agda index 142cb1ac..42520d1a 100644 --- a/test/TypeOperatorImport.agda +++ b/test/TypeOperatorImport.agda @@ -4,12 +4,17 @@ module TypeOperatorImport where 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 :*: (b1 &&& b2) +test2 b1 b2 = ((tt :*:_) ∘ not) (b1 &&& b2) {-# COMPILE AGDA2HS test2 #-} 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) + From d7a16a72644776800b20f999b276aac130d5ea57 Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Tue, 25 Jul 2023 12:03:08 +0200 Subject: [PATCH 6/8] Adding NamespacedName data --- src/Agda2Hs/Compile/Imports.hs | 26 +++++++++++++------------- src/Agda2Hs/Compile/Types.hs | 6 ++++++ 2 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/Agda2Hs/Compile/Imports.hs b/src/Agda2Hs/Compile/Imports.hs index ae9a0694..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 (), Hs.Namespace ()) (Set (Hs.Name (), Hs.Namespace ())) +type ImportSpecMap = Map NamespacedName (Set NamespacedName) type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap compileImports :: String -> Imports -> TCM [Hs.ImportDecl ()] @@ -33,23 +33,23 @@ compileImports top is0 = do mergeChildren :: ImportSpecMap -> ImportSpecMap -> ImportSpecMap mergeChildren = Map.unionWith Set.union - makeSingle :: Maybe (Hs.Name (), Hs.Namespace ()) -> (Hs.Name (), Hs.Namespace ()) -> 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 ns) -> Map.insertWith mergeChildren (mod,as) - (makeSingle (parentTuple p) (q, ns))) + (makeSingle (parentNN p) (NamespacedName ns q))) 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 + 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 @@ -61,10 +61,10 @@ compileImports top is0 = do | head s == ':' = Hs.ConName () n | otherwise = Hs.VarName () n - makeImportSpec :: (Hs.Name (), Hs.Namespace ()) -> Set (Hs.Name (), Hs.Namespace ()) -> Hs.ImportSpec () - makeImportSpec (q, namespace) 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 . fst) $ Set.toList qs + | otherwise = Hs.IThingWith () q $ map (makeCName . nnName) $ Set.toList qs makeImportDecl :: Hs.ModuleName () -> Qualifier -> ImportSpecMap -> Hs.ImportDecl () makeImportDecl mod qual specs = Hs.ImportDecl () diff --git a/src/Agda2Hs/Compile/Types.hs b/src/Agda2Hs/Compile/Types.hs index 8aada58e..3c25a566 100644 --- a/src/Agda2Hs/Compile/Types.hs +++ b/src/Agda2Hs/Compile/Types.hs @@ -134,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) From 4687be8cbbe3251eb3db13d5a92fc8e8af6548be Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Thu, 27 Jul 2023 12:40:19 +0200 Subject: [PATCH 7/8] Using the built-in "isSort" function --- src/Agda2Hs/Compile/Name.hs | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/Agda2Hs/Compile/Name.hs b/src/Agda2Hs/Compile/Name.hs index 595a2ca2..1b022774 100644 --- a/src/Agda2Hs/Compile/Name.hs +++ b/src/Agda2Hs/Compile/Name.hs @@ -160,10 +160,11 @@ compileQName f 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 ()) + 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 @@ -171,12 +172,6 @@ compileQName f (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 From 5767b4fedb6e9e4363184c7d265508c6c1606138 Mon Sep 17 00:00:00 2001 From: viktorcsimma Date: Thu, 27 Jul 2023 12:41:41 +0200 Subject: [PATCH 8/8] Updating AllTests.agda --- test/AllTests.agda | 4 ++++ test/golden/AllTests.hs | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/test/AllTests.agda b/test/AllTests.agda index 15e39de4..b1035642 100644 --- a/test/AllTests.agda +++ b/test/AllTests.agda @@ -104,4 +104,8 @@ import WitnessedFlows import Kinds import LawfulOrd import Deriving +import ErasedLocalDefinitions +import TypeOperators +import TypeOperatorExport +import TypeOperatorImport #-} 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