Break cross-module SCC 4 (#6897)

* Split backend on TCM-awareness

* Fix broken imports

* Remove unused pragma

* Remove TCMB -> Backend import

* Move IsMain to break accidental module cycle

* Split Interaction.* on TCM-awareness

* Move decls into TCMB to avoid accidental cycle

* Fix easy errors

* Fix typevar ambiguity bug

* Fix TCErr/TCWarning mix-up

* Remove redundant import

* Update import list

* Add back cycle-detection script

* Make find-cycles script build with cabal

* Rename Agda.Compiler.Backend.Boot

* Rename Agda.Interaction.Base.Boot

* Fix whitespace

* Shrink diff vs master's Agda.Interaction.Base

By promoting TCM-aware defs rather than demoting the rest

* Tweak cycle-finding script

* Document cycle-finding script

* Remove find-cycles (now has own repository)

* Rename Agda.Interaction.Boot

* Restore original .gitignore

* Restore accidentally-updated submodules

... to their state on current master (de7f50)

* Cosmetics

---------

Co-authored-by: Andreas Abel <andreas.abel@ifi.lmu.de>

Agda.cabal

@@ -462,6 +462,7 @@ library
       Agda.Auto.Typecheck
       Agda.Benchmarking
       Agda.Compiler.Backend
+      Agda.Compiler.Backend.Base
       Agda.Compiler.Builtin
       Agda.Compiler.CallCompiler
       Agda.Compiler.Common
@@ -518,7 +519,9 @@ library
       Agda.Interaction.Highlighting.LaTeX
       Agda.Interaction.Imports
       Agda.Interaction.InteractionTop
+      Agda.Interaction.Output
       Agda.Interaction.Response
+      Agda.Interaction.Response.Base
       Agda.Interaction.MakeCase
       Agda.Interaction.Monad
       Agda.Interaction.Library

Makefile

@@ -285,6 +285,8 @@ type-check-no-deps :
 	-$(CABAL) $(CABAL_BUILD_CMD) --builddir=$(BUILD_DIR)-no-code \
           --ghc-options=-fno-code \
           --ghc-options=-fwrite-interface \
+		  --ghc-options=-fwrite-ide-info \
+		  --ghc-options=-hiedir=dist-hiefiles \
           2>&1 \
           | $(SED) -e '/.*dist.*build.*: No such file or directory/d' \
                    -e '/.*Warning: the following files would be used as linker inputs, but linking is not being done:.*/d'

src/full/Agda/Compiler/Backend.hs

@@ -1,11 +1,11 @@
 {-# OPTIONS_GHC -Wunused-imports #-}
 
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
 
 -- | Interface for compiler backend writers.
 module Agda.Compiler.Backend
-  ( Backend(..), Backend'(..), Recompile(..), IsMain(..)
+  ( module Agda.Compiler.Backend.Base
+  , Backend, Backend', Recompile(..), IsMain(..)
   , Flag
   , toTreeless
   , module Agda.Syntax.Treeless
@@ -22,6 +22,8 @@ module Agda.Compiler.Backend
   , activeBackend
   ) where
 
+import Agda.Compiler.Backend.Base
+
 import Control.DeepSeq
 import Control.Monad              ( (<=<) )
 import Control.Monad.Trans        ( lift )
@@ -30,14 +32,10 @@ import Control.Monad.Trans.Maybe
 import qualified Data.List as List
 import Data.Maybe
 
-import Data.Map (Map)
 import qualified Data.Map as Map
 
-import GHC.Generics (Generic)
-
 import System.Console.GetOpt
 
-import Agda.Syntax.TopLevelModuleName
 import Agda.Syntax.Treeless
 import Agda.TypeChecking.Errors (getAllWarnings)
 -- Agda.TypeChecking.Monad.Base imports us, relying on the .hs-boot file to
@@ -68,49 +66,9 @@ import Agda.Utils.Impossible
 
 -- Public interface -------------------------------------------------------
 
-data Backend where
-  Backend :: NFData opts => Backend' opts env menv mod def -> Backend
-
-data Backend' opts env menv mod def = Backend'
-  { backendName      :: String
-  , backendVersion   :: Maybe String
-      -- ^ Optional version information to be printed with @--version@.
-  , options          :: opts
-      -- ^ Default options
-  , commandLineFlags :: [OptDescr (Flag opts)]
-      -- ^ Backend-specific command-line flags. Should at minimum contain a
-      --   flag to enable the backend.
-  , isEnabled        :: opts -> Bool
-      -- ^ Unless the backend has been enabled, @runAgda@ will fall back to
-      --   vanilla Agda behaviour.
-  , preCompile       :: opts -> TCM env
-      -- ^ Called after type checking completes, but before compilation starts.
-  , postCompile      :: env -> IsMain -> Map TopLevelModuleName mod ->
-                        TCM ()
-      -- ^ Called after module compilation has completed. The @IsMain@ argument
-      --   is @NotMain@ if the @--no-main@ flag is present.
-  , preModule        :: env -> IsMain -> TopLevelModuleName ->
-                        Maybe FilePath -> TCM (Recompile menv mod)
-      -- ^ Called before compilation of each module. Gets the path to the
-      --   @.agdai@ file to allow up-to-date checking of previously written
-      --   compilation results. Should return @Skip m@ if compilation is not
-      --   required. Will be @Nothing@ if only scope checking.
-  , postModule       :: env -> menv -> IsMain -> TopLevelModuleName ->
-                        [def] -> TCM mod
-      -- ^ Called after all definitions of a module have been compiled.
-  , compileDef       :: env -> menv -> IsMain -> Definition -> TCM def
-      -- ^ Compile a single definition.
-  , scopeCheckingSuffices :: Bool
-      -- ^ True if the backend works if @--only-scope-checking@ is used.
-  , mayEraseType     :: QName -> TCM Bool
-      -- ^ The treeless compiler may ask the Backend if elements
-      --   of the given type maybe possibly erased.
-      --   The answer should be 'False' if the compilation of the type
-      --   is used by a third party, e.g. in a FFI binding.
-  }
-  deriving Generic
-
-data Recompile menv mod = Recompile menv | Skip mod
+type Backend = Backend_boot TCM
+
+type Backend' opts env menv mod def = Backend'_boot TCM opts env menv mod def
 
 -- | Call the 'compilerMain' function of the given backend.
 
@@ -154,23 +112,6 @@ activeBackendMayEraseType q = do
   Backend b <- fromMaybe __IMPOSSIBLE__ <$> activeBackend
   mayEraseType b q
 
-instance NFData Backend where
-  rnf (Backend b) = rnf b
-
-instance NFData opts => NFData (Backend' opts env menv mod def) where
-  rnf (Backend' a b c d e f g h i j k l) =
-    rnf a `seq` rnf b `seq` rnf c `seq` rnf' d `seq` rnf e `seq`
-    rnf f `seq` rnf g `seq` rnf h `seq` rnf i `seq` rnf j `seq`
-    rnf k `seq` rnf l
-    where
-    rnf' []                   = ()
-    rnf' (Option a b c d : e) =
-      rnf a `seq` rnf b `seq` rnf'' c `seq` rnf d `seq` rnf' e
-
-    rnf'' (NoArg a)    = rnf a
-    rnf'' (ReqArg a b) = rnf a `seq` rnf b
-    rnf'' (OptArg a b) = rnf a `seq` rnf b
-
 -- Internals --------------------------------------------------------------
 
 data BackendWithOpts opts where

src/full/Agda/Compiler/Backend.hs-boot

@@ -8,7 +8,7 @@ module Agda.Compiler.Backend
   )
   where
 
-import Control.DeepSeq
+import Agda.Compiler.Backend.Base
 
 -- Explicitly adding the Agda.Syntax.Treeless import to the .hs-boot file
 -- so that the `Args` symbol can be hidden by the `SOURCE` import in
@@ -26,9 +26,7 @@ import Agda.Syntax.Treeless (TTerm, Args)
 import Agda.Syntax.Abstract.Name (QName)
 import {-# SOURCE #-} Agda.TypeChecking.Monad.Base (TCM, BackendName)
 
-data Backend
-
-instance NFData Backend
+type Backend = Backend_boot TCM
 
 activeBackendMayEraseType :: QName -> TCM Bool
 lookupBackend :: BackendName -> TCM (Maybe Backend)

src/full/Agda/Compiler/Backend/Base.hs

@@ -0,0 +1,78 @@
+{-# LANGUAGE GADTs #-}
+{-# OPTIONS_GHC -Wunused-imports #-}
+
+module Agda.Compiler.Backend.Base where
+
+import Agda.Interaction.Options (ArgDescr(..), OptDescr(..), Flag)
+import Agda.Syntax.Abstract.Name (QName)
+import Agda.Syntax.Common (IsMain)
+import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)
+import {-# SOURCE #-} Agda.TypeChecking.Monad.Base (Definition)
+
+
+import Control.DeepSeq (NFData, rnf)
+import Data.Map (Map)
+
+import GHC.Generics (Generic)
+
+data Backend_boot tcm where
+  Backend :: NFData opts => Backend'_boot tcm opts env menv mod def -> Backend_boot tcm
+
+data Backend'_boot tcm opts env menv mod def = Backend'
+  { backendName      :: String
+  , backendVersion   :: Maybe String
+      -- ^ Optional version information to be printed with @--version@.
+  , options          :: opts
+      -- ^ Default options
+  , commandLineFlags :: [OptDescr (Flag opts)]
+      -- ^ Backend-specific command-line flags. Should at minimum contain a
+      --   flag to enable the backend.
+  , isEnabled        :: opts -> Bool
+      -- ^ Unless the backend has been enabled, @runAgda@ will fall back to
+      --   vanilla Agda behaviour.
+  , preCompile       :: opts -> tcm env
+      -- ^ Called after type checking completes, but before compilation starts.
+  , postCompile      :: env -> IsMain -> Map TopLevelModuleName mod ->
+                        tcm ()
+      -- ^ Called after module compilation has completed. The @IsMain@ argument
+      --   is @NotMain@ if the @--no-main@ flag is present.
+  , preModule        :: env -> IsMain -> TopLevelModuleName ->
+                        Maybe FilePath -> tcm (Recompile menv mod)
+      -- ^ Called before compilation of each module. Gets the path to the
+      --   @.agdai@ file to allow up-to-date checking of previously written
+      --   compilation results. Should return @Skip m@ if compilation is not
+      --   required. Will be @Nothing@ if only scope checking.
+  , postModule       :: env -> menv -> IsMain -> TopLevelModuleName ->
+                        [def] -> tcm mod
+      -- ^ Called after all definitions of a module have been compiled.
+  , compileDef       :: env -> menv -> IsMain -> Definition -> tcm def
+      -- ^ Compile a single definition.
+  , scopeCheckingSuffices :: Bool
+      -- ^ True if the backend works if @--only-scope-checking@ is used.
+  , mayEraseType     :: QName -> tcm Bool
+      -- ^ The treeless compiler may ask the Backend if elements
+      --   of the given type maybe possibly erased.
+      --   The answer should be 'False' if the compilation of the type
+      --   is used by a third party, e.g. in a FFI binding.
+  }
+  deriving Generic
+
+data Recompile menv mod = Recompile menv | Skip mod
+
+
+instance NFData (Backend_boot tcm) where
+  rnf (Backend b) = rnf b
+
+instance NFData opts => NFData (Backend'_boot tcm opts env menv mod def) where
+  rnf (Backend' a b c d e f g h i j k l) =
+    rnf a `seq` rnf b `seq` rnf c `seq` rnf' d `seq` rnf e `seq`
+    rnf f `seq` rnf g `seq` rnf h `seq` rnf i `seq` rnf j `seq`
+    rnf k `seq` rnf l
+    where
+    rnf' []                   = ()
+    rnf' (Option a b c d : e) =
+      rnf a `seq` rnf b `seq` rnf'' c `seq` rnf d `seq` rnf' e
+
+    rnf'' (NoArg a)    = rnf a
+    rnf'' (ReqArg a b) = rnf a `seq` rnf b
+    rnf'' (OptArg a b) = rnf a `seq` rnf b

src/full/Agda/Compiler/Common.hs

@@ -1,6 +1,10 @@
 {-# OPTIONS_GHC -Wunused-imports #-}
 
-module Agda.Compiler.Common where
+module Agda.Compiler.Common
+  ( module Agda.Compiler.Common
+  , IsMain(..)
+  )
+  where
 
 import Prelude hiding ((!!))
 
@@ -35,19 +39,6 @@ import Agda.Utils.WithDefault    ( lensCollapseDefault )
 
 import Agda.Utils.Impossible
 
-data IsMain = IsMain | NotMain
-  deriving (Eq, Show)
-
--- | Conjunctive semigroup ('NotMain' is absorbing).
-instance Semigroup IsMain where
-  NotMain <> _ = NotMain
-  _       <> NotMain = NotMain
-  IsMain  <> IsMain = IsMain
-
-instance Monoid IsMain where
-  mempty = IsMain
-  mappend = (<>)
-
 doCompile :: Monoid r => (IsMain -> Interface -> TCM r) -> IsMain -> Interface -> TCM r
 doCompile f isMain i = do
   flip evalStateT Set.empty $ compilePrim $ doCompile' f isMain i

src/full/Agda/Compiler/JS/Compiler.hs

@@ -68,7 +68,7 @@ import Agda.Compiler.Treeless.EliminateLiteralPatterns
 import Agda.Compiler.Treeless.GuardsToPrims
 import Agda.Compiler.Treeless.Erase ( computeErasedConstructorArgs )
 import Agda.Compiler.Treeless.Subst ()
-import Agda.Compiler.Backend (Backend(..), Backend'(..), Recompile(..))
+import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Recompile(..))
 
 import Agda.Compiler.JS.Syntax
   ( Exp(Self,Local,Global,Undefined,Null,String,Char,Integer,Double,Lambda,Object,Array,Apply,Lookup,If,BinOp,PlainJS),

src/full/Agda/Interaction/Base.hs

@@ -17,7 +17,7 @@ import qualified Data.Map                     as Map
 import           Data.Maybe                   (listToMaybe)
 
 import {-# SOURCE #-} Agda.TypeChecking.Monad.Base
-  (HighlightingLevel, HighlightingMethod, TCM, Comparison, Polarity, TCErr)
+  (HighlightingLevel, HighlightingMethod, Comparison, Polarity)
 
 import           Agda.Syntax.Abstract         (QName)
 import           Agda.Syntax.Common           (InteractionId (..), Modality)
@@ -76,12 +76,6 @@ initCommandState commandQueue =
     , commandQueue         = commandQueue
     }
 
--- | Monad for computing answers to interactive commands.
---
---   'CommandM' is 'TCM' extended with state 'CommandState'.
-
-type CommandM = StateT CommandState TCM
-
 -- | Information about the current main module.
 data CurrentFile = CurrentFile
   { currentFilePath  :: AbsolutePath
@@ -462,10 +456,10 @@ data UseForce
   | WithoutForce  -- ^ Don't ignore any checks.
   deriving (Eq, Read, Show)
 
-data OutputForm a b = OutputForm Range [ProblemId] Blocker (OutputConstraint a b)
+data OutputForm_boot tcErr a b = OutputForm Range [ProblemId] Blocker (OutputConstraint_boot tcErr a b)
   deriving (Functor)
 
-data OutputConstraint a b
+data OutputConstraint_boot tcErr a b
       = OfType b a | CmpInType Comparison a b b
                    | CmpElim [Polarity] a [b] [b]
       | JustType b | CmpTypes Comparison b b
@@ -478,7 +472,7 @@ data OutputConstraint a b
       | FindInstanceOF b a [(a,a,a)]
       | ResolveInstanceOF QName
       | PTSInstance b b
-      | PostponedCheckFunDef QName a TCErr
+      | PostponedCheckFunDef QName a tcErr
       | CheckLock b b
       | DataSort QName b
       | UsableAtMod Modality b

src/full/Agda/Interaction/BasicOps.hs

@@ -24,6 +24,7 @@ import Data.Text (Text)
 import qualified Data.Text as T
 
 import Agda.Interaction.Base
+import Agda.Interaction.Output
 import Agda.Interaction.Options
 import Agda.Interaction.Response (Goals, ResponseContextEntry(..))
 
@@ -749,7 +750,8 @@ getConstraints' g f = liftTCM $ do
       withMetaInfo mv $ do
         mi <- interactionIdToMetaId ii
         let m = QuestionMark emptyMetaInfo{ metaNumber = Just mi } ii
-        abstractToConcrete_ $ OutputForm noRange [] alwaysUnblock $ Assign m e
+        let oform = OutputForm noRange [] alwaysUnblock $ Assign m e :: OutputForm Expr Expr
+        abstractToConcrete_ oform
 
 -- | Reify the boundary of an interaction point as something that can be
 -- shown to the user.

src/full/Agda/Interaction/EmacsTop.hs

@@ -27,7 +27,6 @@ import qualified Agda.TypeChecking.Pretty as TCP
 import Agda.TypeChecking.Pretty (prettyTCM)
 import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings, renderTCWarnings')
 import Agda.TypeChecking.Monad
-import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
 import Agda.Interaction.AgdaTop
 import Agda.Interaction.Base
 import Agda.Interaction.BasicOps as B

src/full/Agda/Interaction/Highlighting/Dot/Backend.hs

@@ -27,7 +27,7 @@ import qualified Data.Text.Lazy as L
 
 import GHC.Generics (Generic)
 
-import Agda.Compiler.Backend (Backend(..), Backend'(..), Definition, Recompile(..))
+import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Definition, Recompile(..))
 import Agda.Compiler.Common (curIF, IsMain)
 
 import Agda.Interaction.FindFile (findFile, srcFilePath)

src/full/Agda/Interaction/Highlighting/HTML/Backend.hs

@@ -23,7 +23,7 @@ import Agda.Interaction.Options
     , OptDescr(..)
     , Flag
     )
-import Agda.Compiler.Backend (Backend(..), Backend'(..), Recompile(..))
+import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Recompile(..))
 import Agda.Compiler.Common (IsMain(..), curIF)
 
 import Agda.Syntax.TopLevelModuleName (TopLevelModuleName)

src/full/Agda/Interaction/Highlighting/LaTeX/Backend.hs

@@ -25,7 +25,7 @@ import GHC.Generics (Generic)
 
 import System.FilePath ( (</>) )
 
-import Agda.Compiler.Backend (Backend(..), Backend'(..), Definition, Recompile(..))
+import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Definition, Recompile(..))
 import Agda.Compiler.Common (curIF, IsMain(IsMain, NotMain))
 
 import Agda.Interaction.Options

src/full/Agda/Interaction/InteractionTop.hs

@@ -22,6 +22,7 @@ import Control.Monad.IO.Class       ( MonadIO(..) )
 import Control.Monad.Fail           ( MonadFail )
 import Control.Monad.State          ( MonadState(..), gets, modify, runStateT )
 import Control.Monad.STM
+import Control.Monad.State          ( StateT )
 import Control.Monad.Trans          ( lift )
 
 import qualified Data.Char as Char
@@ -95,6 +96,8 @@ import Agda.Utils.Impossible
 ------------------------------------------------------------------------
 -- The CommandM monad
 
+type CommandM = StateT CommandState TCM
+
 -- | Restore both 'TCState' and 'CommandState'.
 
 localStateCommandM :: CommandM a -> CommandM a