cleanup imports

Author: flupe

agda2lambox.cabal

@@ -15,9 +15,7 @@ source-repository head
 executable agda2lambox
   hs-source-dirs:      src
   main-is:             Main.hs
-  other-modules:       Agda,
-                       Agda.Lib,
-                       Agda.Utils,
+  other-modules:       Agda.Utils,
                        Agda2Lambox.Compile.Utils,
                        Agda2Lambox.Compile.Term,
                        Agda2Lambox.Compile.Function,

src/Agda.hs

@@ -9,55 +9,21 @@ import Control.Monad ( filterM )
 import Control.Arrow ( first )
 
 import Data.List ( partition )
-import qualified Data.List.NonEmpty as NE ( fromList )
 import Data.Maybe ( isJust, isNothing )
 import Data.Bifunctor ( second )
 
-import Agda.Lib
-import Agda.TypeChecking.Free.Lazy (underBinder)
-import Agda.TypeChecking.Datatypes (getConstructorInfo, ConstructorInfo(..))
+import Agda.Compiler.Backend ( getUniqueCompilerPragma )
+import Agda.Syntax.Abstract.Name
+import Agda.TypeChecking.Monad.Base hiding ( conArity )
+import Agda.TypeChecking.Datatypes ( getConstructorInfo, ConstructorInfo(..) )
+import Agda.TypeChecking.Substitute ( raise )
+import Agda.Syntax.Common.Pretty
+import Agda.Syntax.Treeless
 
--- ** useful monad constraint kinds
-
-type MonadIOEnv m = (MonadIO m, MonadTCEnv m)
-type PureEnvTCM m = (PureTCM m, ReadTCState m, HasConstInfo m, MonadIOEnv m)
-
--- ** pretty-printing
 
 pp :: Pretty a => a -> String
 pp = prettyShow
 
-ppm :: (MonadPretty m, PrettyTCM a) => a -> m Doc
-ppm = prettyTCM
-
-prender :: Doc -> String
-prender = renderStyle (Style OneLineMode 0 0.0)
-
-pinterleave :: (Applicative m, Semigroup (m Doc)) => m Doc -> [m Doc] -> m Doc
-pinterleave sep = fsep . punctuate sep
-
-pbindings :: (MonadPretty m, PrettyTCM a) => [(String, a)] -> [m Doc]
-pbindings = map $ \(n, ty) -> parens $ ppm n <> " : " <> ppm ty
-
-panic :: (Pretty a, Show a) => String -> a -> b
-panic s t = error $
-  "[PANIC] unexpected " <> s <> ": " <> limit (pp t) <> "\n"
-    <> "show: " <> limit (ppShow t)
-  where limit = take 500
-
--- ** typechecking context
-
-currentCtx :: MonadTCEnv m => m [(String, Type)]
-currentCtx = fmap (first pp . unDom) <$> getContext
-
-reportCurrentCtx :: (MonadIO m, MonadTCEnv m) => m ()
-reportCurrentCtx = do
-  ctx <- currentCtx
-  liftIO $ putStrLn $ " currentCtx: " <> pp ctx
-
-unqual :: QName -> String
-unqual = pp . last . qnameToList0
-
 hasPragma :: QName -> TCM Bool
 hasPragma qn = isJust <$> getUniqueCompilerPragma "AGDA2LAMBOX" qn
 

src/Agda/Lib.hs

@@ -11,7 +11,6 @@ import Data.Foldable ( toList )
 import Data.List ( elemIndex )
 import Data.Maybe ( isJust, listToMaybe )
 
-import Agda ( liftTCM )
 import Agda.Syntax.Abstract.Name ( qnameModule, qnameName )
 import Agda.TypeChecking.Monad.Base
 import Agda.TypeChecking.Monad.Env ( withCurrentModule )

src/Agda/Utils.hs

@@ -8,15 +8,15 @@ import Control.Monad ( forM, when )
 import Data.List ( elemIndex )
 import Data.Maybe ( isNothing, fromMaybe )
 
-import Agda.Lib ( (^.), funInline )
 import Agda.Syntax.Abstract.Name ( QName, qnameModule )
 import Agda.TypeChecking.Monad.Base
 import Agda.Compiler.ToTreeless ( toTreeless )
-import Agda.Compiler.Backend ( getConstInfo )
+import Agda.Compiler.Backend ( getConstInfo, funInline )
 import Agda.Syntax.Treeless ( EvaluationStrategy(EagerEvaluation) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Common ( hasQuantityω )
 import Agda.Utils.Monad (guardWithError)
+import Agda.Utils.Lens ( (^.) )
 
 import Agda.Utils ( etaExpandCtor )
 import Agda2Lambox.Compile.Utils

src/Agda2Lambox/Compile/Data.hs

@@ -11,14 +11,14 @@ import Control.Monad.Reader ( ReaderT(runReaderT), local )
 import Data.List ( elemIndex, foldl' )
 import Data.Maybe ( fromMaybe, listToMaybe )
 
-import Agda (TCM , liftTCM, MonadTCEnv, MonadTCM)
 import Agda.Compiler.Backend ( MonadTCState, HasOptions )
 import Agda.Compiler.Backend ( getConstInfo, theDef, pattern Datatype, dataMutual )
 import Agda.Syntax.Abstract.Name ( ModuleName(..), QName(..) )
 import Agda.Syntax.Common ( Erased(..) )
 import Agda.Syntax.Common.Pretty ( prettyShow )
 import Agda.Syntax.Treeless ( TTerm(..), TAlt(..), CaseInfo(..), CaseType(..) )
 import Agda.TypeChecking.Datatypes ( getConstructorData, getConstructors )
+import Agda.TypeChecking.Monad.Base ( TCM , liftTCM, MonadTCEnv, MonadTCM )
 
 import LambdaBox ( Term(..) )
 import LambdaBox qualified as LBox

src/Agda2Lambox/Compile/Function.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
 -- | The agda2lambox Agda backend
-module Main where
+module Main (main) where
 
 import Control.Monad ( unless )
 import Control.Monad.IO.Class ( liftIO )
@@ -16,9 +16,14 @@ import System.FilePath ( (</>) )
 
 import Paths_agda2lambox ( version )
 
-import Agda.Lib
-import Agda.Utils ( pp, hasPragma )
+import Agda.Compiler.Common
+import Agda.Compiler.Backend
+import Agda.Main ( runAgda )
+import Agda.Syntax.TopLevelModuleName ( TopLevelModuleName, moduleNameToFileName )
+import Agda.Syntax.Common.Pretty ( pretty, prettyShow )
+import Agda.Utils.Monad ( whenM )
 
+import Agda.Utils ( pp, hasPragma )
 import Agda2Lambox.Compile.Function ( compileFunction )
 import Agda2Lambox.Compile.Data     ( compileData     )
 import Agda2Lambox.Compile.Record   ( compileRecord   )