Add module hierarchy Agda2Hs.Language.Haskell (#413)

Author: HeinrichApfelmus

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