Add module hierarchy Agda2Hs.Language.Haskell

agda2hs.cabal

@@ -45,7 +45,8 @@ executable agda2hs
                        Agda2Hs.Compile.Utils,
                        Agda2Hs.Compile.Var,
                        Agda2Hs.Config,
-                       Agda2Hs.HsUtils,
+                       Agda2Hs.Language.Haskell,
+                       Agda2Hs.Language.Haskell.Utils,
                        Agda2Hs.Pragma,
                        Agda2Hs.Render,
                        AgdaInternals,

src/Agda2Hs/Compile.hs

@@ -21,8 +21,6 @@ import Agda.Utils.List
 import Agda.Utils.Null
 import Agda.Utils.Monad ( whenM, anyM, when, unless )
 
-import qualified Language.Haskell.Exts.Extension as Hs
-
 import Agda2Hs.Compile.ClassInstance ( compileInstance )
 import Agda2Hs.Compile.Data ( compileData )
 import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma, checkInlinePragma )
@@ -32,9 +30,8 @@ import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Pragma
-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
 initCompileEnv tlm rewrites = 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 as Hs
-import Language.Haskell.Exts.Extension as Hs
-
 import Agda.Compiler.Backend
 import Agda.Compiler.Common ( curDefs, sortDefs )
 
@@ -40,8 +37,9 @@ import Agda2Hs.Compile.Term
 import Agda2Hs.Compile.Type
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.HsUtils
 
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( hsName, pp, replaceName, unQual )
 
 enableCopatterns :: C a -> C a
 enableCopatterns = local $ \e -> e { copatternsEnabled = True }

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,9 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.HsUtils
+
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( hsName )
 
 checkNewtype :: Hs.Name () -> [Hs.QualConDecl ()] -> C ()
 checkNewtype name cs = do

src/Agda2Hs/Compile/Function.hs

@@ -10,8 +10,6 @@ import Data.List
 import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text
 
-import qualified Language.Haskell.Exts as Hs
-
 import Agda.Compiler.Backend
 import Agda.Compiler.Common
 
@@ -46,8 +44,10 @@ import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
-import Agda2Hs.HsUtils
 
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils
+  ( Strictness, hsName, pApp, patToExp, constrainType, qualifyType )
 
 -- | Compilation rules for specific constructors in patterns.
 isSpecialCon :: QName -> Maybe (Type -> NAPs -> C (Hs.Pat ()))

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,12 +2,14 @@ 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 as Hs
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( validVarId, validConId, pp )
 
 import Agda.Compiler.Backend
 import Agda.TypeChecking.Pretty ( text )
@@ -17,8 +19,6 @@ import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.HsUtils
-import qualified Data.List as L
 
 type ImportSpecMap = Map NamespacedName (Set NamespacedName)
 type ImportDeclMap = Map (Hs.ModuleName (), Qualifier) ImportSpecMap

src/Agda2Hs/Compile/Name.hs

@@ -12,8 +12,6 @@ import Data.List ( intercalate, isPrefixOf, stripPrefix )
 import Data.Text ( unpack )
 import qualified Data.Map.Strict as Map
 
-import qualified Language.Haskell.Exts as Hs
-
 import Agda.Compiler.Backend hiding ( topLevelModuleName )
 import Agda.Compiler.Common ( topLevelModuleName )
 
@@ -34,14 +32,15 @@ import Agda.TypeChecking.Records ( isRecordConstructor )
 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.HsUtils
+
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( hsName, hsModuleName, pp )
 
 
 isSpecialCon :: QName -> Maybe (Hs.QName ())

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,7 +8,9 @@ import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda2Hs.Compile.Type ( compileType )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.HsUtils
+
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( hsName, pp, hsError ) 
 
 compilePostulate :: Definition -> C [Hs.Decl ()]
 compilePostulate def = do

src/Agda2Hs/Compile/Record.hs

@@ -8,8 +8,6 @@ import Data.List.NonEmpty ( NonEmpty(..) )
 import Data.Map ( Map )
 import qualified Data.Map as Map
 
-import qualified Language.Haskell.Exts as Hs
-
 import Agda.Compiler.Backend
 
 import Agda.Syntax.Common ( Arg(unArg), defaultArg )
@@ -29,7 +27,9 @@ import Agda2Hs.Compile.Function ( compileFun )
 import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
-import Agda2Hs.HsUtils
+
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( hsName, definedName, pp )
 
 -- | Primitive fields and default implementations
 type MinRecord = ([Hs.Name ()], Map (Hs.Name ()) (Hs.Decl ()))

src/Agda2Hs/Compile/Term.hs

@@ -12,8 +12,6 @@ import Data.Maybe ( fromMaybe, isJust )
 import qualified Data.Text as Text ( unpack )
 import qualified Data.Set as Set ( singleton )
 
-import qualified Language.Haskell.Exts as Hs
-
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import qualified Agda.Syntax.Common.Pretty as P
 import Agda.Syntax.Common
@@ -47,7 +45,10 @@ import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTel
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
-import Agda2Hs.HsUtils
+
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils
+  ( hsName, pp, eApp, hsLambda, hsUnqualName, hsVar )
 
 import {-# SOURCE #-} Agda2Hs.Compile.Function ( compileClause' )
 import qualified Data.List as L

src/Agda2Hs/Compile/Type.hs

@@ -11,10 +11,6 @@ import Data.List ( find )
 import Data.Maybe ( mapMaybe, isJust )
 import qualified Data.Set as Set ( singleton )
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Extension as Hs
-import qualified Language.Haskell.Exts.Pretty as Hs
-
 import Agda.Compiler.Backend hiding ( Args )
 
 import Agda.Syntax.Common
@@ -38,7 +34,9 @@ import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var
 import Agda2Hs.AgdaUtils
-import Agda2Hs.HsUtils
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils
+  ( Strictness(Lazy), hsName, tApp, constrainType, qualifyType )
 
 
 -- | Type definitions from the prelude that get special translation rules.

src/Agda2Hs/Compile/TypeDefinition.hs

@@ -4,8 +4,6 @@ import Control.Monad ( unless )
 
 import Data.Maybe ( fromMaybe )
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-
 import Agda.Compiler.Backend
 
 import Agda.Syntax.Common ( namedArg )
@@ -21,10 +19,11 @@ import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTyp
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
-import Agda2Hs.HsUtils
 import Agda.Syntax.Common.Pretty (prettyShow)
 import Agda.TypeChecking.Substitute
 
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( hsName )
 
 compileTypeDef :: Hs.Name () -> Definition -> C [Hs.Decl ()]
 compileTypeDef name (Defn {..}) = do

src/Agda2Hs/Compile/Types.hs

@@ -14,19 +14,15 @@ import Data.Set ( Set )
 import Data.Map ( Map )
 import Data.String ( IsString(..) )
 
-import qualified Language.Haskell.Exts.SrcLoc as Hs
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Extension as Hs
-import qualified Language.Haskell.Exts.Comments as Hs
-
 import Agda.Compiler.Backend
 import Agda.Syntax.Position ( Range )
 import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName )
 import Agda.TypeChecking.Warnings ( MonadWarning )
 import Agda.Utils.Null
 import Agda.Utils.Impossible
 
-import Agda2Hs.HsUtils ( Strictness )
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( Strictness )
 
 type ModuleEnv   = TopLevelModuleName
 type ModuleRes   = ()

src/Agda2Hs/Compile/Utils.hs

@@ -11,8 +11,6 @@ import Data.List ( isPrefixOf, stripPrefix )
 import Data.Maybe ( isJust )
 import qualified Data.Map as M
 
-import qualified Language.Haskell.Exts as Hs
-
 import Agda.Compiler.Backend hiding ( Args )
 
 import Agda.Syntax.Common
@@ -45,11 +43,14 @@ import Agda.Utils.Singleton
 import AgdaInternals
 import Agda2Hs.AgdaUtils ( (~~) )
 import Agda2Hs.Compile.Types
-import Agda2Hs.HsUtils
 import Agda2Hs.Pragma
 import qualified Data.List as L
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils
+  ( Strictness(..), validVarName, validTypeName, validConName, hsName, pp )
+
 data HsModuleKind
   = PrimModule
   | HsModule

src/Agda2Hs/Language/Haskell.hs

@@ -0,0 +1,28 @@
+-- | Haskell syntax, parsing, pretty printing.
+--
+-- This module contains those elements of the Haskell language
+-- that are needed by Agda2hs.
+--
+-- We are mainly re-exporting @haskell-src-exts@.
+module Agda2Hs.Language.Haskell
+  ( module Language.Haskell.Exts.Build
+  , module Language.Haskell.Exts.Comments
+  , module Language.Haskell.Exts.ExactPrint
+  , module Language.Haskell.Exts.Extension
+  , module Language.Haskell.Exts.Parser
+  , module Language.Haskell.Exts.Pretty
+  , module Language.Haskell.Exts.SrcLoc
+  , module Language.Haskell.Exts.Syntax
+  , module Agda2Hs.Language.Haskell.Utils
+  ) where
+
+import Agda2Hs.Language.Haskell.Utils
+
+import Language.Haskell.Exts.Comments (Comment)
+import Language.Haskell.Exts.Build hiding (pApp)
+import Language.Haskell.Exts.ExactPrint (exactPrint)
+import Language.Haskell.Exts.Extension hiding (Strict, Lazy)
+import Language.Haskell.Exts.Parser
+import Language.Haskell.Exts.Pretty
+import Language.Haskell.Exts.SrcLoc (SrcSpanInfo)
+import Language.Haskell.Exts.Syntax

src/Agda2Hs/HsUtils.hs → src/Agda2Hs/Language/Haskell/Utils.hs

@@ -1,5 +1,5 @@
 
-module Agda2Hs.HsUtils where
+module Agda2Hs.Language.Haskell.Utils where
 
 import Control.Monad ( guard )
 

src/Agda2Hs/Pragma.hs

@@ -4,10 +4,6 @@ import Data.List ( isPrefixOf )
 import Data.Maybe ( fromMaybe )
 import qualified Data.Map as Map
 
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Parser as Hs
-import qualified Language.Haskell.Exts.Extension as Hs
-
 import Agda.Compiler.Backend
 import Agda.Compiler.Common ( curIF )
 
@@ -16,9 +12,11 @@ import Agda.Syntax.Position
 import Agda.Utils.FileName ( filePath )
 import Agda.Utils.Maybe.Strict ( toLazy )
 
-import Agda2Hs.HsUtils
 import Agda2Hs.Compile.Types
 
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils ( Strictness(..), srcLocToRange )
+
 pragmaName :: String
 pragmaName = "AGDA2HS"
 

src/Agda2Hs/Render.hs

@@ -12,12 +12,6 @@ import qualified Data.Set as Set
 import System.FilePath ( takeDirectory, (</>) )
 import System.Directory ( createDirectoryIfMissing )
 
-import qualified Language.Haskell.Exts.SrcLoc as Hs
-import qualified Language.Haskell.Exts.Syntax as Hs
-import qualified Language.Haskell.Exts.Build as Hs
-import qualified Language.Haskell.Exts.ExactPrint as Hs
-import qualified Language.Haskell.Exts.Extension as Hs
-
 import Agda.Compiler.Backend
 import Agda.Compiler.Common ( compileDir )
 
@@ -33,11 +27,11 @@ import Agda2Hs.Compile
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Imports
 import Agda2Hs.Compile.Utils ( primModules )
-import Agda2Hs.HsUtils
+import qualified Agda2Hs.Language.Haskell as Hs
+import Agda2Hs.Language.Haskell.Utils
+  ( extToName, pp, moveToTop, insertParens )
 import Agda2Hs.Pragma ( getForeignPragmas )
 
-import Language.Haskell.Exts as Hs (prettyPrint, prelude_mod)
-
 -- Rendering --------------------------------------------------------------
 
 type Block = Ranged [String]