Anchor imports at Agda2Hs.Language.Haskell

Author: HeinrichApfelmus

src/Agda2Hs/Compile.hs

@@ -31,9 +31,7 @@ import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Pragma
 
-import qualified Language.Haskell.Exts.Extension as Hs
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Pretty as Hs
+import qualified Agda2Hs.Language.Haskell as Hs
 
 
 initCompileEnv :: TopLevelModuleName -> SpecialRules -> CompileEnv

src/Agda2Hs/Compile/ClassInstance.hs

@@ -8,9 +8,6 @@ import Data.List ( nub )
 import Data.Maybe ( isNothing, mapMaybe )
 import qualified Data.HashMap.Strict as HMap
 
-import qualified Language.Haskell.Exts.Extension as Hs
-import qualified Language.Haskell.Exts.Syntax as Hs
-
 import Agda.Compiler.Backend
 import Agda.Compiler.Common ( curDefs, sortDefs )
 
@@ -40,7 +37,8 @@ import Agda2Hs.Compile.Term
 import Agda2Hs.Compile.Type
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.Language.Haskell.Utils
+
+import qualified Agda2Hs.Language.Haskell as Hs
 
 
 enableCopatterns :: C a -> C a
@@ -94,7 +92,7 @@ compileInstance ToDefinition def@Defn{..} =
                 <$> mapM (\c -> withClauseLocals mod c $ compileInstanceClause mod ty c) clauses
         reportSDoc "agda2hs.compile.instance" 20 $ vcat $
           text "compileInstance compiled clauses: " :
-          map (nest 2 . text . pp) ds
+          map (nest 2 . text . Hs.pp) ds
         when (length (nub rs) > 1) $
           genericDocError =<< fsep (pwords "More than one minimal record used.")
         return $ Hs.InstDecl () Nothing ir (Just ds)
@@ -214,7 +212,7 @@ compileInstanceClause' curModule ty (p:ps) c
     ls <- asks locals
     reportSDoc "agda2hs.compile.instance" 18 $ text "Clause locals:" <+> prettyTCM ls
 
-    let uf = hsName $ prettyShow $ nameConcrete $ qnameName q
+    let uf = Hs.hsName $ prettyShow $ nameConcrete $ qnameName q
 
     let
       (.~) :: QName -> QName -> Bool
@@ -248,11 +246,11 @@ compileInstanceClause' curModule ty (p:ps) c
         let mod = if isExtendedLambdaName defName then curModule else qnameModule defName
         (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
+        let hd = Hs.hsName $ prettyShow $ nameConcrete $ qnameName defName
+        let fc' = {- dropPatterns 1 $ -} Hs.replaceName hd uf fc
         reportSDoc "agda2hs.compile.instance" 6 $ vcat $
           text "compileInstanceClause compiled clause: " :
-          map (nest 2 . text . pp) fc'
+          map (nest 2 . text . Hs.pp) fc'
         return (fc', n:rs)
 
        -- Projection of a default implementation: drop while making sure these are drawn from the
@@ -291,7 +289,7 @@ compileInstanceClause' curModule ty (p:ps) c
         let cc = Hs.FunBind () (toList ms)
         reportSDoc "agda2hs.compile.instance" 20 $ vcat
           [ text "compileInstanceClause compiled clause"
-          , nest 2 $ text $ pp cc
+          , nest 2 $ text $ Hs.pp cc
           ]
         return ([Hs.InsDecl () cc], [])
 
@@ -340,5 +338,5 @@ lookupDefaultImplementations recName fields = do
 classMemberNames :: Definition -> C [Hs.Name ()]
 classMemberNames def =
   case theDef def of
-    Record{recFields = fs} -> fmap unQual <$> traverse compileQName (map unDom fs)
+    Record{recFields = fs} -> fmap Hs.unQual <$> traverse compileQName (map unDom fs)
     _ -> genericDocError =<< text "Not a record:" <+> prettyTCM (defName def)

src/Agda2Hs/Compile/Data.hs

@@ -1,7 +1,5 @@
 module Agda2Hs.Compile.Data where
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-
 import Control.Monad ( when )
 import Agda.Compiler.Backend
 import Agda.Syntax.Common
@@ -18,7 +16,8 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.Language.Haskell.Utils
+
+import qualified Agda2Hs.Language.Haskell as Hs
 
 checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C ()
 checkNewtype name cs = do
@@ -29,7 +28,7 @@ checkNewtype name cs = do
 
 compileData :: AsNewType -> [Hs.Deriving ()] -> Definition -> C [Hs.Decl ()]
 compileData newtyp ds def = do
-  let d = hsName $ prettyShow $ qnameName $ defName def
+  let d = Hs.hsName $ prettyShow $ qnameName $ defName def
   checkValidTypeName d
   let Datatype{dataPars = n, dataIxs = numIxs, dataCons = cs} = theDef def
   TelV tel t <- telViewUpTo n (defType def)
@@ -63,7 +62,7 @@ compileConstructor params c = do
   ty <- (`piApplyM` params) . defType =<< getConstInfo c
   reportSDoc "agda2hs.data.con" 20 $ text "  ty = " <+> prettyTCM ty
   TelV tel _ <- telView ty
-  let conName = hsName $ prettyShow $ qnameName c
+  let conName = Hs.hsName $ prettyShow $ qnameName c
   checkValidConName conName
   args <- compileConstructorArgs tel
   return $ Hs.QualConDecl () Nothing Nothing $ Hs.ConDecl () conName args

src/Agda2Hs/Compile/Function.hs

@@ -10,10 +10,6 @@ import Data.List
 import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text
 
-import qualified Language.Haskell.Exts.Build as Hs (charP)
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Pretty as Hs
-
 import Agda.Compiler.Backend
 import Agda.Compiler.Common
 
@@ -48,8 +44,8 @@ import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
-import Agda2Hs.Language.Haskell.Utils
 
+import qualified Agda2Hs.Language.Haskell as Hs
 
 -- | Compilation rules for specific constructors in patterns.
 isSpecialCon :: QName -> Maybe (Type -> NAPs -> C (Hs.Pat ()))
@@ -166,7 +162,7 @@ compileFun' withSig def@Defn{..} = inTopContext $ withCurrentModule m $ do
     Function{..} = theDef
     m = qnameModule defName
     n = qnameName defName
-    x = hsName $ prettyShow n
+    x = Hs.hsName $ prettyShow n
     err = "Not supported: type definition with `where` clauses"
 
     addPats :: [Hs.Pat ()] -> Hs.Match () -> Hs.Match ()
@@ -179,10 +175,10 @@ compileModuleParams EmptyTel = return (id, [])
 compileModuleParams (ExtendTel a tel) = do
   (f , p) <- compileDomType (absName tel) a >>= \case
     DomDropped -> return (id, [])
-    DomConstraint c -> return (constrainType c, [])
-    DomForall a -> return (qualifyType a, [])
+    DomConstraint c -> return (Hs.constrainType c, [])
+    DomForall a -> return (Hs.qualifyType a, [])
     DomType s a -> do
-      let n = hsName $ absName tel
+      let n = Hs.hsName $ absName tel
       checkValidVarName n
       return (Hs.TyFun () a, [Hs.PVar () n])
   ((f .) *** (p++)) <$> underAbstraction a tel compileModuleParams
@@ -290,7 +286,7 @@ compilePat :: Type -> DeBruijnPattern -> C (Hs.Pat ())
 compilePat ty p@(VarP o x)
   | PatOWild <- patOrigin o = return $ Hs.PWildCard ()
   | otherwise = do
-      n <- hsName <$> compileDBVar (dbPatVarIndex x)
+      n <- Hs.hsName <$> compileDBVar (dbPatVarIndex x)
       checkValidVarName n
       return $ Hs.PVar () n
 
@@ -304,7 +300,7 @@ compilePat ty (ConP ch i ps) = do
   ifJustM (isTupleConstructor c) (\b -> compileTupleConP ty b ps) $ do
     ps <- compilePats ty ps
     c <- compileQName (conName ch)
-    return $ pApp c ps
+    return $ Hs.pApp c ps
 
 -- literal patterns
 compilePat ty (LitP _ l) = compileLitPat l
@@ -314,7 +310,7 @@ compilePat ty (LitP _ l) = compileLitPat l
 compilePat _ p = genericDocError =<< "bad pattern:" <?> prettyTCM p
 
 
-compileErasedConP :: Type -> Strictness -> NAPs -> C (Hs.Pat ())
+compileErasedConP :: Type -> Hs.Strictness -> NAPs -> C (Hs.Pat ())
 compileErasedConP ty s ps = compilePats ty ps >>= \case
   [p] -> addPatBang s p
   _   -> __IMPOSSIBLE__
@@ -384,7 +380,7 @@ checkTransparentPragma def = compileFun False def >>= \case
   where
     checkTransparentClause :: Hs.Match () -> C ()
     checkTransparentClause = \case
-      Hs.Match _ _ [p] (Hs.UnGuardedRhs _ e) _ | patToExp p == Just e -> return ()
+      Hs.Match _ _ [p] (Hs.UnGuardedRhs _ e) _ | Hs.patToExp p == Just e -> return ()
       _ -> errNotTransparent
 
     checkTransparentTypeDef :: Hs.DeclHead () -> Hs.Type () -> C ()

src/Agda2Hs/Compile/Function.hs-boot

@@ -1,6 +1,6 @@
 module Agda2Hs.Compile.Function where
 
-import qualified Language.Haskell.Exts.Syntax as Hs ( Match, Name )
+import qualified Agda2Hs.Language.Haskell as Hs ( Match, Name )
 import Agda.Syntax.Internal ( Clause, ModuleName, QName, Type )
 import Agda2Hs.Compile.Types ( C )
 

src/Agda2Hs/Compile/Imports.hs

@@ -2,13 +2,13 @@ module Agda2Hs.Compile.Imports ( compileImports, preludeImportDecl ) where
 
 import Data.Char ( isUpper )
 import Data.List ( isPrefixOf )
+import qualified Data.List as L
 import Data.Map ( Map )
 import qualified Data.Map as Map
 import Data.Set ( Set )
 import qualified Data.Set as Set
 
-import qualified Language.Haskell.Exts.Pretty as Hs
-import qualified Language.Haskell.Exts.Syntax as Hs
+import qualified Agda2Hs.Language.Haskell as Hs
 
 import Agda.Compiler.Backend
 import Agda.TypeChecking.Pretty ( text )
@@ -18,8 +18,6 @@ import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.Language.Haskell.Utils
-import qualified Data.List as L
 
 type ImportSpecMap = Map NamespacedName (Set NamespacedName)
 type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap
@@ -29,7 +27,7 @@ compileImports top is0 = do
   let is = filter ((top /=) . Hs.prettyPrint . importModule) is0
   checkClashingImports is
   let imps = Map.toList $ groupModules is
-  reportSLn "agda2hs.import" 10 $ "All imported modules: " ++ show (map (pp . fst . fst) imps)
+  reportSLn "agda2hs.import" 10 $ "All imported modules: " ++ show (map (Hs.pp . fst . fst) imps)
   let decls = map (uncurry $ uncurry makeImportDecl) imps
   return decls
   where
@@ -88,17 +86,17 @@ compileImports top is0 = do
         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') ++ ")"
+             "Clashing import: " ++ Hs.pp q ++ " (both from "
+          ++ prettyShow (Hs.pp <$> p) ++ " and "
+          ++ prettyShow (Hs.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).
 preludeImportDecl :: PreludeOptions -> Hs.ImportDecl ()
 preludeImportDecl (PreludeOpts{..}) =
-  let toName s | validVarId s || validConId s = Hs.Ident () s
+  let toName s | Hs.validVarId s || Hs.validConId s = Hs.Ident () s
       toName s = Hs.Symbol () s
 
       -- if the prelude is implicit, we use the provided hiding list.

src/Agda2Hs/Compile/Name.hs

@@ -12,9 +12,6 @@ import Data.List ( intercalate, isPrefixOf, stripPrefix )
 import Data.Text ( unpack )
 import qualified Data.Map.Strict as Map
 
-import qualified Language.Haskell.Exts.Pretty as Hs
-import qualified Language.Haskell.Exts.Syntax as Hs
-
 import Agda.Compiler.Backend hiding ( topLevelModuleName )
 import Agda.Compiler.Common ( topLevelModuleName )
 
@@ -37,12 +34,13 @@ import Agda.TypeChecking.Warnings ( warning )
 import qualified Agda.Utils.List1 as List1
 import Agda.Utils.Monad
 import Agda.Utils.Maybe ( isJust, isNothing, whenJust, fromMaybe, caseMaybeM )
-import Agda.Utils.Monad ( whenM )
+import Agda.Utils.Monad ( orM, whenM )
 
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.Language.Haskell.Utils
+
+import qualified Agda2Hs.Language.Haskell as Hs
 
 
 isSpecialCon :: QName -> Maybe (Hs.QName ())
@@ -57,10 +55,10 @@ isSpecialCon = prettyShow >>> \case
 
 -- | Convert identifier and import module strings into the Haskell equivalent syntax.
 toNameImport :: String -> Maybe String -> (Hs.Name (), Maybe Import)
-toNameImport x Nothing = (hsName x, Nothing)
+toNameImport x Nothing = (Hs.hsName x, Nothing)
 toNameImport x (Just mod) =
-  ( hsName x
-  , Just $ Import (hsModuleName mod) Unqualified Nothing (hsName x) (Hs.NoNamespace ())
+  ( Hs.hsName x
+  , Just $ Import (Hs.hsModuleName mod) Unqualified Nothing (Hs.hsName x) (Hs.NoNamespace ())
   )
 
 -- | Default rewrite rules.
@@ -89,7 +87,7 @@ isSpecialName :: QName -> C (Maybe (Hs.Name (), Maybe Import))
 isSpecialName f = asks (Map.lookup (prettyShow f) . rewrites)
 
 compileName :: Applicative m => Name -> m (Hs.Name ())
-compileName n = hsName . show <$> pretty (nameConcrete n)
+compileName n = Hs.hsName . show <$> pretty (nameConcrete n)
 
 compileQName :: QName -> C (Hs.QName ())
 compileQName f
@@ -157,8 +155,8 @@ compileQName f
       ++ "\nmod0: " ++ prettyShow mod0
       ++ "\nmodule name: " ++ Hs.prettyPrint mod
       ++ "\ncurrent module: " ++ Hs.prettyPrint currMod
-      ++ "\nqualifier: " ++ prettyShow (fmap (fmap pp) qual)
-      ++ "\n(qualified) haskell name: " ++ pp qf
+      ++ "\nqualifier: " ++ prettyShow (fmap (fmap Hs.pp) qual)
+      ++ "\n(qualified) haskell name: " ++ Hs.pp qf
     return qf
   where
     parentName :: QName -> C (Maybe QName)
@@ -174,7 +172,7 @@ compileQName f
       (inverseScopeLookupName f <$> getScope) >>= \case
         (C.QName{} : _) -> return Unqualified
         (C.Qual as C.QName{} : _) -> liftTCM $ do
-          let qual = hsModuleName $ prettyShow as
+          let qual = Hs.hsModuleName $ prettyShow as
           lookupModuleInCurrentModule as >>= \case
             (x:_) | qual /= mod -> do
               isDataMod <- isJust <$> isDatatypeModule (amodName x)
@@ -213,7 +211,7 @@ isWhereFunction f = do
   return $ any (qnameModule f `isLeChildModuleOf`) whereMods
 
 hsTopLevelModuleName :: TopLevelModuleName -> Hs.ModuleName ()
-hsTopLevelModuleName = hsModuleName . intercalate "." . map unpack
+hsTopLevelModuleName = Hs.hsModuleName . intercalate "." . map unpack
                      . List1.toList . moduleNameParts
 
 -- | Given a module name (assumed to be a toplevel module),
@@ -223,7 +221,7 @@ compileModuleName m = do
   tlm <- liftTCM $ hsTopLevelModuleName <$> getTopLevelModuleForModuleName m
   reportSDoc "agda2hs.name" 25 $
     text "Top-level module name for" <+> prettyTCM m <+>
-    text "is" <+> text (pp tlm)
+    text "is" <+> text (Hs.pp tlm)
   case hsModuleKind tlm of
     PrimModule -> return (PrimModule, Hs.ModuleName () "Prelude")
     HsModule   -> return (HsModule, dropHaskellPrefix tlm)
@@ -233,5 +231,5 @@ importInstance :: QName -> C ()
 importInstance f = do
   (kind, mod) <- compileModuleName $ qnameModule f
   unless (kind == PrimModule) $ do
-    reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ pp mod
+    reportSLn "agda2hs.import" 20 $ "Importing instances from " ++ Hs.pp mod
     tellImport $ ImportInstances mod

src/Agda2Hs/Compile/Postulate.hs

@@ -1,7 +1,5 @@
 module Agda2Hs.Compile.Postulate where
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-
 import Agda.Compiler.Backend
 
 import Agda.Syntax.Internal
@@ -10,15 +8,16 @@ import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda2Hs.Compile.Type ( compileType )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.Language.Haskell.Utils
+
+import qualified Agda2Hs.Language.Haskell as Hs
 
 compilePostulate :: Definition -> C [Hs.Decl ()]
 compilePostulate def = do
   let n = qnameName (defName def)
-      x = hsName $ prettyShow n
+      x = Hs.hsName $ prettyShow n
   checkValidFunName x
   setCurrentRange (nameBindingSite n) $ do
     ty <- compileType (unEl $ defType def)
-    let body = hsError $ "postulate: " ++ pp ty
+    let body = Hs.hsError $ "postulate: " ++ Hs.pp ty
     return [ Hs.TypeSig () [x] ty
            , Hs.FunBind () [Hs.Match () x [] (Hs.UnGuardedRhs () body) Nothing] ]