    module Agda.Compiler.MAlonzo.Compiler where

    import Control.Arrow (second)
    import Control.DeepSeq
    import Control.Monad
    import Control.Monad.Except   ( throwError )
    import Control.Monad.IO.Class ( MonadIO(..) )
    import Control.Monad.Reader   ( MonadReader(..), asks, ReaderT, runReaderT, withReaderT)
    import Control.Monad.Trans    ( lift )
    import Control.Monad.Writer   ( MonadWriter(..), WriterT, runWriterT )

    import qualified Data.HashSet as HashSet
    import qualified Data.List as List
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Text (Text)
    import qualified Data.Text as Text
    import Data.Monoid (Monoid, mempty, mappend)
    import Data.Semigroup ((<>))

    import GHC.Generics (Generic)

    import qualified Agda.Utils.Haskell.Syntax as HS

    import System.Directory (createDirectoryIfMissing)
    import System.Environment (setEnv)
    import System.FilePath hiding (normalise)
    import System.IO (utf8)

    import Agda.Compiler.CallCompiler
    import Agda.Compiler.Common
    import Agda.Compiler.MAlonzo.Coerce
    import Agda.Compiler.MAlonzo.Misc
    import Agda.Compiler.MAlonzo.Pretty
    import Agda.Compiler.MAlonzo.Primitives
    import Agda.Compiler.MAlonzo.HaskellTypes
    import Agda.Compiler.MAlonzo.Pragmas
    import Agda.Compiler.MAlonzo.Strict
    import Agda.Compiler.ToTreeless
    import Agda.Compiler.Treeless.Unused
    import Agda.Compiler.Treeless.Erase
    import Agda.Compiler.Backend

    import Agda.Interaction.Imports
    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import qualified Agda.Syntax.Abstract.Name as A
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Names (namesIn)
    import qualified Agda.Syntax.Treeless as T
    import Agda.Syntax.Literal

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Primitive (getBuiltinName)
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Pretty hiding ((<>))
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Warnings

    import Agda.Utils.FileName (isNewerThan)
    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Float
    import Agda.Utils.IO.Directory
    import Agda.Utils.Lens
    import Agda.Utils.List
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Pretty (prettyShow, render)
    import Agda.Utils.Singleton
    import qualified Agda.Utils.IO.UTF8 as UTF8
    import Agda.Utils.String

    import Paths_Agda

    import Agda.Utils.Impossible

    -- The backend callbacks --------------------------------------------------

    ghcBackend :: Backend
    ghcBackend :: Backend
    ghcBackend = Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    -> Backend
    forall opts env menv mod def.
    NFData opts =>
    Backend' opts env menv mod def -> Backend
    Backend Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    ghcBackend'

    ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    ghcBackend' = Backend' :: forall opts env menv mod def.
    FilePath
    -> Maybe FilePath
    -> opts
    -> [OptDescr (Flag opts)]
    -> (opts -> Bool)
    -> (opts -> TCM env)
    -> (env -> IsMain -> Map ModuleName mod -> TCM ())
    -> (env
        -> IsMain
        -> ModuleName
        -> Maybe FilePath
        -> TCM (Recompile menv mod))
    -> (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod)
    -> (env -> menv -> IsMain -> Definition -> TCM def)
    -> Bool
    -> (QName -> TCM Bool)
    -> Backend' opts env menv mod def
    Backend'
      { backendName :: FilePath
    backendName           = FilePath
    "GHC"
      , backendVersion :: Maybe FilePath
    backendVersion        = Maybe FilePath
    forall a. Maybe a
    Nothing
      , options :: GHCFlags
    options               = GHCFlags
    defaultGHCFlags
      , commandLineFlags :: [OptDescr (Flag GHCFlags)]
    commandLineFlags      = [OptDescr (Flag GHCFlags)]
    ghcCommandLineFlags
      , isEnabled :: GHCFlags -> Bool
    isEnabled             = GHCFlags -> Bool
    flagGhcCompile
      , preCompile :: GHCFlags -> TCM GHCEnv
    preCompile            = GHCFlags -> TCM GHCEnv
    ghcPreCompile
      , postCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
    postCompile           = GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
    ghcPostCompile
      , preModule :: GHCEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile GHCModuleEnv GHCModule)
    preModule             = GHCEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile GHCModuleEnv GHCModule)
    ghcPreModule
      , postModule :: GHCEnv
    -> GHCModuleEnv
    -> IsMain
    -> ModuleName
    -> [GHCDefinition]
    -> TCM GHCModule
    postModule            = GHCEnv
    -> GHCModuleEnv
    -> IsMain
    -> ModuleName
    -> [GHCDefinition]
    -> TCM GHCModule
    ghcPostModule
      , compileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
    compileDef            = GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
    ghcCompileDef
      , scopeCheckingSuffices :: Bool
    scopeCheckingSuffices = Bool
    False
      , mayEraseType :: QName -> TCM Bool
    mayEraseType          = QName -> TCM Bool
    ghcMayEraseType
      }

    --- Command-line flags ---

    data GHCFlags = GHCFlags
      { GHCFlags -> Bool
    flagGhcCompile :: Bool
      , GHCFlags -> Bool
    flagGhcCallGhc :: Bool
      , GHCFlags -> Maybe FilePath
    flagGhcBin     :: Maybe FilePath
        -- ^ Use the compiler at PATH instead of "ghc"
      , GHCFlags -> [FilePath]
    flagGhcFlags      :: [String]
      , GHCFlags -> Bool
    flagGhcStrictData :: Bool
        -- ^ Make inductive constructors strict?
      , GHCFlags -> Bool
    flagGhcStrict :: Bool
        -- ^ Make functions strict?
      }
      deriving (forall x. GHCFlags -> Rep GHCFlags x)
    -> (forall x. Rep GHCFlags x -> GHCFlags) -> Generic GHCFlags
    forall x. Rep GHCFlags x -> GHCFlags
    forall x. GHCFlags -> Rep GHCFlags x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep GHCFlags x -> GHCFlags
    $cfrom :: forall x. GHCFlags -> Rep GHCFlags x
    Generic

    instance NFData GHCFlags

    defaultGHCFlags :: GHCFlags
    defaultGHCFlags :: GHCFlags
    defaultGHCFlags = GHCFlags :: Bool
    -> Bool -> Maybe FilePath -> [FilePath] -> Bool -> Bool -> GHCFlags
    GHCFlags
      { flagGhcCompile :: Bool
    flagGhcCompile    = Bool
    False
      , flagGhcCallGhc :: Bool
    flagGhcCallGhc    = Bool
    True
      , flagGhcBin :: Maybe FilePath
    flagGhcBin        = Maybe FilePath
    forall a. Maybe a
    Nothing
      , flagGhcFlags :: [FilePath]
    flagGhcFlags      = []
      , flagGhcStrictData :: Bool
    flagGhcStrictData = Bool
    False
      , flagGhcStrict :: Bool
    flagGhcStrict     = Bool
    False
      }

    ghcCommandLineFlags :: [OptDescr (Flag GHCFlags)]
    ghcCommandLineFlags :: [OptDescr (Flag GHCFlags)]
    ghcCommandLineFlags =
        [ FilePath
    -> [FilePath]
    -> ArgDescr (Flag GHCFlags)
    -> FilePath
    -> OptDescr (Flag GHCFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option [Char
    'c']  [FilePath
    "compile", FilePath
    "ghc"] (Flag GHCFlags -> ArgDescr (Flag GHCFlags)
    forall a. a -> ArgDescr a
    NoArg Flag GHCFlags
    forall {f :: * -> *}. Applicative f => GHCFlags -> f GHCFlags
    enable)
                        FilePath
    "compile program using the GHC backend"
        , FilePath
    -> [FilePath]
    -> ArgDescr (Flag GHCFlags)
    -> FilePath
    -> OptDescr (Flag GHCFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "ghc-dont-call-ghc"] (Flag GHCFlags -> ArgDescr (Flag GHCFlags)
    forall a. a -> ArgDescr a
    NoArg Flag GHCFlags
    forall {f :: * -> *}. Applicative f => GHCFlags -> f GHCFlags
    dontCallGHC)
                        FilePath
    "don't call GHC, just write the GHC Haskell files."
        , FilePath
    -> [FilePath]
    -> ArgDescr (Flag GHCFlags)
    -> FilePath
    -> OptDescr (Flag GHCFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "ghc-flag"] ((FilePath -> Flag GHCFlags) -> FilePath -> ArgDescr (Flag GHCFlags)
    forall a. (FilePath -> a) -> FilePath -> ArgDescr a
    ReqArg FilePath -> Flag GHCFlags
    forall {f :: * -> *}.
    Applicative f =>
    FilePath -> GHCFlags -> f GHCFlags
    ghcFlag FilePath
    "GHC-FLAG")
                        FilePath
    "give the flag GHC-FLAG to GHC"
        , FilePath
    -> [FilePath]
    -> ArgDescr (Flag GHCFlags)
    -> FilePath
    -> OptDescr (Flag GHCFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "with-compiler"] ((FilePath -> Flag GHCFlags) -> FilePath -> ArgDescr (Flag GHCFlags)
    forall a. (FilePath -> a) -> FilePath -> ArgDescr a
    ReqArg FilePath -> Flag GHCFlags
    withCompilerFlag FilePath
    "PATH")
                        FilePath
    "use the compiler available at PATH"
        , FilePath
    -> [FilePath]
    -> ArgDescr (Flag GHCFlags)
    -> FilePath
    -> OptDescr (Flag GHCFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "ghc-strict-data"] (Flag GHCFlags -> ArgDescr (Flag GHCFlags)
    forall a. a -> ArgDescr a
    NoArg Flag GHCFlags
    forall {f :: * -> *}. Applicative f => GHCFlags -> f GHCFlags
    strictData)
                        FilePath
    "make inductive constructors strict"
        , FilePath
    -> [FilePath]
    -> ArgDescr (Flag GHCFlags)
    -> FilePath
    -> OptDescr (Flag GHCFlags)
    forall a.
    FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
    Option []     [FilePath
    "ghc-strict"] (Flag GHCFlags -> ArgDescr (Flag GHCFlags)
    forall a. a -> ArgDescr a
    NoArg Flag GHCFlags
    forall {f :: * -> *}. Applicative f => GHCFlags -> f GHCFlags
    strict)
                        FilePath
    "make functions strict"
        ]
      where
        enable :: GHCFlags -> f GHCFlags
    enable      GHCFlags
    o = GHCFlags -> f GHCFlags
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o{ flagGhcCompile :: Bool
    flagGhcCompile    = Bool
    True }
        dontCallGHC :: GHCFlags -> f GHCFlags
    dontCallGHC GHCFlags
    o = GHCFlags -> f GHCFlags
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o{ flagGhcCallGhc :: Bool
    flagGhcCallGhc    = Bool
    False }
        ghcFlag :: FilePath -> GHCFlags -> f GHCFlags
    ghcFlag FilePath
    f   GHCFlags
    o = GHCFlags -> f GHCFlags
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o{ flagGhcFlags :: [FilePath]
    flagGhcFlags      = GHCFlags -> [FilePath]
    flagGhcFlags GHCFlags
    o [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ [FilePath
    f] }
        strictData :: GHCFlags -> f GHCFlags
    strictData  GHCFlags
    o = GHCFlags -> f GHCFlags
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o{ flagGhcStrictData :: Bool
    flagGhcStrictData = Bool
    True }
        strict :: GHCFlags -> f GHCFlags
    strict      GHCFlags
    o = GHCFlags -> f GHCFlags
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o{ flagGhcStrictData :: Bool
    flagGhcStrictData = Bool
    True
                              , flagGhcStrict :: Bool
    flagGhcStrict     = Bool
    True
                              }

    withCompilerFlag :: FilePath -> Flag GHCFlags
    withCompilerFlag :: FilePath -> Flag GHCFlags
    withCompilerFlag FilePath
    fp GHCFlags
    o = case GHCFlags -> Maybe FilePath
    flagGhcBin GHCFlags
    o of
     Maybe FilePath
    Nothing -> Flag GHCFlags
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o { flagGhcBin :: Maybe FilePath
    flagGhcBin = FilePath -> Maybe FilePath
    forall a. a -> Maybe a
    Just FilePath
    fp }
     Just{}  -> FilePath -> OptM GHCFlags
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError FilePath
    "only one compiler path allowed"

    --- Context types ---

    -- | Monads that can read @GHCOptions@
    class Monad m => ReadGHCOpts m where
      askGhcOpts :: m GHCOptions

    instance Monad m => ReadGHCOpts (ReaderT GHCOptions m) where
      askGhcOpts :: ReaderT GHCOptions m GHCOptions
    askGhcOpts = ReaderT GHCOptions m GHCOptions
    forall r (m :: * -> *). MonadReader r m => m r
    ask

    instance Monad m => ReadGHCOpts (ReaderT GHCEnv m) where
      askGhcOpts :: ReaderT GHCEnv m GHCOptions
    askGhcOpts = (GHCEnv -> GHCOptions)
    -> ReaderT GHCOptions m GHCOptions -> ReaderT GHCEnv m GHCOptions
    forall r' r (m :: * -> *) a.
    (r' -> r) -> ReaderT r m a -> ReaderT r' m a
    withReaderT GHCEnv -> GHCOptions
    ghcEnvOpts ReaderT GHCOptions m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts

    instance Monad m => ReadGHCOpts (ReaderT GHCModuleEnv m) where
      askGhcOpts :: ReaderT GHCModuleEnv m GHCOptions
    askGhcOpts = (GHCModuleEnv -> GHCEnv)
    -> ReaderT GHCEnv m GHCOptions -> ReaderT GHCModuleEnv m GHCOptions
    forall r' r (m :: * -> *) a.
    (r' -> r) -> ReaderT r m a -> ReaderT r' m a
    withReaderT GHCModuleEnv -> GHCEnv
    ghcModEnv ReaderT GHCEnv m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts

    data GHCModule = GHCModule
      { GHCModule -> GHCModuleEnv
    ghcModModuleEnv :: GHCModuleEnv
      , GHCModule -> [MainFunctionDef]
    ghcModMainFuncs :: [MainFunctionDef]
      -- ^ The `main` function definition(s), if both the module is
      --   the @IsMain@ module (root/focused) and a suitable `main`
      --   function was defined.
      }

    instance Monad m => ReadGHCOpts (ReaderT GHCModule m) where
      askGhcOpts :: ReaderT GHCModule m GHCOptions
    askGhcOpts = (GHCModule -> GHCModuleEnv)
    -> ReaderT GHCModuleEnv m GHCOptions
    -> ReaderT GHCModule m GHCOptions
    forall r' r (m :: * -> *) a.
    (r' -> r) -> ReaderT r m a -> ReaderT r' m a
    withReaderT GHCModule -> GHCModuleEnv
    ghcModModuleEnv ReaderT GHCModuleEnv m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts

    instance Monad m => ReadGHCModuleEnv (ReaderT GHCModule m) where
      askGHCModuleEnv :: ReaderT GHCModule m GHCModuleEnv
    askGHCModuleEnv = (GHCModule -> GHCModuleEnv)
    -> ReaderT GHCModuleEnv m GHCModuleEnv
    -> ReaderT GHCModule m GHCModuleEnv
    forall r' r (m :: * -> *) a.
    (r' -> r) -> ReaderT r m a -> ReaderT r' m a
    withReaderT GHCModule -> GHCModuleEnv
    ghcModModuleEnv ReaderT GHCModuleEnv m GHCModuleEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m GHCModuleEnv
    askGHCModuleEnv

    data GHCDefinition = GHCDefinition
      { GHCDefinition -> UsesFloat
    ghcDefUsesFloat  :: UsesFloat
      , GHCDefinition -> [Decl]
    ghcDefDecls      :: [HS.Decl]
      , GHCDefinition -> Definition
    ghcDefDefinition :: Definition
      , GHCDefinition -> Maybe MainFunctionDef
    ghcDefMainDef    :: Maybe MainFunctionDef
      , GHCDefinition -> Set ModuleName
    ghcDefImports    :: Set ModuleName
      }

    --- Top-level compilation ---

    ghcPreCompile :: GHCFlags -> TCM GHCEnv
    ghcPreCompile :: GHCFlags -> TCM GHCEnv
    ghcPreCompile GHCFlags
    flags = do
      Maybe Cubical
    cubical <- PragmaOptions -> Maybe Cubical
    optCubical (PragmaOptions -> Maybe Cubical)
    -> TCMT IO PragmaOptions -> TCMT IO (Maybe Cubical)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      let notSupported :: FilePath -> m a
    notSupported FilePath
    s =
            TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ FilePath -> TypeError
    GenericError (FilePath -> TypeError) -> FilePath -> TypeError
    forall a b. (a -> b) -> a -> b
    $
              FilePath
    "Compilation of code that uses " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    s FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " is not supported."
      case Maybe Cubical
    cubical of
        Maybe Cubical
    Nothing      -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Just Cubical
    CErased -> () -> TCM ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Just Cubical
    CFull   -> FilePath -> TCM ()
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    FilePath -> m a
    notSupported FilePath
    "--cubical"

      FilePath
    outDir <- TCMT IO FilePath
    forall (m :: * -> *). HasOptions m => m FilePath
    compileDir
      let ghcOpts :: GHCOptions
    ghcOpts = GHCOptions :: Bool
    -> FilePath -> [FilePath] -> FilePath -> Bool -> Bool -> GHCOptions
    GHCOptions
                    { optGhcCallGhc :: Bool
    optGhcCallGhc    = GHCFlags -> Bool
    flagGhcCallGhc GHCFlags
    flags
                    , optGhcBin :: FilePath
    optGhcBin        = FilePath -> Maybe FilePath -> FilePath
    forall a. a -> Maybe a -> a
    fromMaybe FilePath
    "ghc" (GHCFlags -> Maybe FilePath
    flagGhcBin GHCFlags
    flags)
                    , optGhcFlags :: [FilePath]
    optGhcFlags      = GHCFlags -> [FilePath]
    flagGhcFlags GHCFlags
    flags
                    , optGhcCompileDir :: FilePath
    optGhcCompileDir = FilePath
    outDir
                    , optGhcStrictData :: Bool
    optGhcStrictData = GHCFlags -> Bool
    flagGhcStrictData GHCFlags
    flags
                    , optGhcStrict :: Bool
    optGhcStrict     = GHCFlags -> Bool
    flagGhcStrict GHCFlags
    flags
                    }

      Maybe QName
    mbool       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinBool
      Maybe QName
    mtrue       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinTrue
      Maybe QName
    mfalse      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinFalse
      Maybe QName
    mlist       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinList
      Maybe QName
    mnil        <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinNil
      Maybe QName
    mcons       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinCons
      Maybe QName
    mmaybe      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinMaybe
      Maybe QName
    mnothing    <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinNothing
      Maybe QName
    mjust       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinJust
      Maybe QName
    mnat        <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinNat
      Maybe QName
    minteger    <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinInteger
      Maybe QName
    mword64     <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinWord64
      Maybe QName
    minf        <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinInf
      Maybe QName
    msharp      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinSharp
      Maybe QName
    mflat       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinFlat
      Maybe QName
    minterval   <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinInterval
      Maybe QName
    mizero      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIZero
      Maybe QName
    mione       <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIOne
      Maybe QName
    misone      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIsOne
      Maybe QName
    mitisone    <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinItIsOne
      Maybe QName
    misone1     <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIsOne1
      Maybe QName
    misone2     <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIsOne2
      Maybe QName
    misoneempty <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIsOneEmpty
      Maybe QName
    mpathp      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinPathP
      Maybe QName
    msub        <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinSub
      Maybe QName
    msubin      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinSubIn
      Maybe QName
    mid         <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinId
      Maybe QName
    mconid      <- FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinConId

      QName -> Bool
    istcbuiltin <- do
        [Maybe QName]
    builtins <- (FilePath -> TCMT IO (Maybe QName))
    -> [FilePath] -> TCMT IO [Maybe QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM FilePath -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName
          [ FilePath
    builtinAgdaTCMReturn
          , FilePath
    builtinAgdaTCMBind
          , FilePath
    builtinAgdaTCMUnify
          , FilePath
    builtinAgdaTCMTypeError
          , FilePath
    builtinAgdaTCMInferType
          , FilePath
    builtinAgdaTCMCheckType
          , FilePath
    builtinAgdaTCMNormalise
          , FilePath
    builtinAgdaTCMReduce
          , FilePath
    builtinAgdaTCMCatchError
          , FilePath
    builtinAgdaTCMQuoteTerm
          , FilePath
    builtinAgdaTCMUnquoteTerm
          , FilePath
    builtinAgdaTCMQuoteOmegaTerm
          , FilePath
    builtinAgdaTCMGetContext
          , FilePath
    builtinAgdaTCMExtendContext
          , FilePath
    builtinAgdaTCMInContext
          , FilePath
    builtinAgdaTCMFreshName
          , FilePath
    builtinAgdaTCMDeclareDef
          , FilePath
    builtinAgdaTCMDeclarePostulate
          , FilePath
    builtinAgdaTCMDefineFun
          , FilePath
    builtinAgdaTCMGetType
          , FilePath
    builtinAgdaTCMGetDefinition
          , FilePath
    builtinAgdaTCMBlockOnMeta
          , FilePath
    builtinAgdaTCMCommit
          , FilePath
    builtinAgdaTCMIsMacro
          , FilePath
    builtinAgdaTCMWithNormalisation
          , FilePath
    builtinAgdaTCMWithReconsParams
          , FilePath
    builtinAgdaTCMDebugPrint
          , FilePath
    builtinAgdaTCMOnlyReduceDefs
          , FilePath
    builtinAgdaTCMDontReduceDefs
          , FilePath
    builtinAgdaTCMNoConstraints
          , FilePath
    builtinAgdaTCMRunSpeculative
          , FilePath
    builtinAgdaTCMExec
          ]
        (QName -> Bool) -> TCMT IO (QName -> Bool)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName -> Bool) -> TCMT IO (QName -> Bool))
    -> (QName -> Bool) -> TCMT IO (QName -> Bool)
    forall a b. (a -> b) -> a -> b
    $
          (QName -> HashSet QName -> Bool) -> HashSet QName -> QName -> Bool
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip QName -> HashSet QName -> Bool
    forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
    HashSet.member (HashSet QName -> QName -> Bool) -> HashSet QName -> QName -> Bool
    forall a b. (a -> b) -> a -> b
    $
          [QName] -> HashSet QName
    forall a. (Eq a, Hashable a) => [a] -> HashSet a
    HashSet.fromList ([QName] -> HashSet QName) -> [QName] -> HashSet QName
    forall a b. (a -> b) -> a -> b
    $
          [Maybe QName] -> [QName]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe QName]
    builtins

      GHCEnv -> TCM GHCEnv
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GHCEnv -> TCM GHCEnv) -> GHCEnv -> TCM GHCEnv
    forall a b. (a -> b) -> a -> b
    $ GHCEnv :: GHCOptions
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> Maybe QName
    -> (QName -> Bool)
    -> GHCEnv
    GHCEnv
        { ghcEnvOpts :: GHCOptions
    ghcEnvOpts        = GHCOptions
    ghcOpts
        , ghcEnvBool :: Maybe QName
    ghcEnvBool        = Maybe QName
    mbool
        , ghcEnvTrue :: Maybe QName
    ghcEnvTrue        = Maybe QName
    mtrue
        , ghcEnvFalse :: Maybe QName
    ghcEnvFalse       = Maybe QName
    mfalse
        , ghcEnvMaybe :: Maybe QName
    ghcEnvMaybe       = Maybe QName
    mmaybe
        , ghcEnvNothing :: Maybe QName
    ghcEnvNothing     = Maybe QName
    mnothing
        , ghcEnvJust :: Maybe QName
    ghcEnvJust        = Maybe QName
    mjust
        , ghcEnvList :: Maybe QName
    ghcEnvList        = Maybe QName
    mlist
        , ghcEnvNil :: Maybe QName
    ghcEnvNil         = Maybe QName
    mnil
        , ghcEnvCons :: Maybe QName
    ghcEnvCons        = Maybe QName
    mcons
        , ghcEnvNat :: Maybe QName
    ghcEnvNat         = Maybe QName
    mnat
        , ghcEnvInteger :: Maybe QName
    ghcEnvInteger     = Maybe QName
    minteger
        , ghcEnvWord64 :: Maybe QName
    ghcEnvWord64      = Maybe QName
    mword64
        , ghcEnvInf :: Maybe QName
    ghcEnvInf         = Maybe QName
    minf
        , ghcEnvSharp :: Maybe QName
    ghcEnvSharp       = Maybe QName
    msharp
        , ghcEnvFlat :: Maybe QName
    ghcEnvFlat        = Maybe QName
    mflat
        , ghcEnvInterval :: Maybe QName
    ghcEnvInterval    = Maybe QName
    minterval
        , ghcEnvIZero :: Maybe QName
    ghcEnvIZero       = Maybe QName
    mizero
        , ghcEnvIOne :: Maybe QName
    ghcEnvIOne        = Maybe QName
    mione
        , ghcEnvIsOne :: Maybe QName
    ghcEnvIsOne       = Maybe QName
    misone
        , ghcEnvItIsOne :: Maybe QName
    ghcEnvItIsOne     = Maybe QName
    mitisone
        , ghcEnvIsOne1 :: Maybe QName
    ghcEnvIsOne1      = Maybe QName
    misone1
        , ghcEnvIsOne2 :: Maybe QName
    ghcEnvIsOne2      = Maybe QName
    misone2
        , ghcEnvIsOneEmpty :: Maybe QName
    ghcEnvIsOneEmpty  = Maybe QName
    misoneempty
        , ghcEnvPathP :: Maybe QName
    ghcEnvPathP       = Maybe QName
    mpathp
        , ghcEnvSub :: Maybe QName
    ghcEnvSub         = Maybe QName
    msub
        , ghcEnvSubIn :: Maybe QName
    ghcEnvSubIn       = Maybe QName
    msubin
        , ghcEnvId :: Maybe QName
    ghcEnvId          = Maybe QName
    mid
        , ghcEnvConId :: Maybe QName
    ghcEnvConId       = Maybe QName
    mconid
        , ghcEnvIsTCBuiltin :: QName -> Bool
    ghcEnvIsTCBuiltin = QName -> Bool
    istcbuiltin
        }

    ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
    ghcPostCompile :: GHCEnv -> IsMain -> Map ModuleName GHCModule -> TCM ()
    ghcPostCompile GHCEnv
    _cenv IsMain
    _isMain Map ModuleName GHCModule
    mods = do
      -- FIXME: @curMName@ and @curIF@ are evil TCM state, but there does not appear to be
      --------- another way to retrieve the compilation root ("main" module or interaction focused).
      ModuleName
    rootModuleName <- TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
      GHCModule
    rootModule <- Maybe GHCModule
    -> (GHCModule -> TCM GHCModule) -> TCM GHCModule -> TCM GHCModule
    forall a b. Maybe a -> (a -> b) -> b -> b
    ifJust (ModuleName -> Map ModuleName GHCModule -> Maybe GHCModule
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup ModuleName
    rootModuleName Map ModuleName GHCModule
    mods) GHCModule -> TCM GHCModule
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                    (TCM GHCModule -> TCM GHCModule) -> TCM GHCModule -> TCM GHCModule
    forall a b. (a -> b) -> a -> b
    $ FilePath -> TCM GHCModule
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    FilePath -> m a
    genericError (FilePath -> TCM GHCModule) -> FilePath -> TCM GHCModule
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "Module " FilePath -> FilePath -> FilePath
    forall a. Semigroup a => a -> a -> a
    <> ModuleName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow ModuleName
    rootModuleName FilePath -> FilePath -> FilePath
    forall a. Semigroup a => a -> a -> a
    <> FilePath
    " was not compiled!"
      (ReaderT GHCModule TCM () -> GHCModule -> TCM ())
    -> GHCModule -> ReaderT GHCModule TCM () -> TCM ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ReaderT GHCModule TCM () -> GHCModule -> TCM ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT GHCModule
    rootModule (ReaderT GHCModule TCM () -> TCM ())
    -> ReaderT GHCModule TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        ReaderT GHCModule TCM ()
    forall (m :: * -> *). MonadGHCIO m => m ()
    copyRTEModules
        ReaderT GHCModule TCM ()
    callGHC

    --- Module compilation ---

    ghcPreModule
      :: GHCEnv
      -> IsMain      -- ^ Are we looking at the main module?
      -> ModuleName
      -> Maybe FilePath    -- ^ Path to the @.agdai@ file.
      -> TCM (Recompile GHCModuleEnv GHCModule)
                     -- ^ Could we confirm the existence of a main function?
    ghcPreModule :: GHCEnv
    -> IsMain
    -> ModuleName
    -> Maybe FilePath
    -> TCM (Recompile GHCModuleEnv GHCModule)
    ghcPreModule GHCEnv
    cenv IsMain
    isMain ModuleName
    m Maybe FilePath
    mifile =
      (do let check :: ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    check = ReaderT GHCModuleEnv TCM Bool
    -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ReaderT GHCModuleEnv TCM Bool
    uptodate ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    forall {menv}. ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    noComp ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    yesComp
          Maybe Cubical
    cubical <- PragmaOptions -> Maybe Cubical
    optCubical (PragmaOptions -> Maybe Cubical)
    -> ReaderT GHCModuleEnv TCM PragmaOptions
    -> ReaderT GHCModuleEnv TCM (Maybe Cubical)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv TCM PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
          case Maybe Cubical
    cubical of
            -- Code that uses --cubical is not compiled.
            Just Cubical
    CFull   -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    forall {menv}. ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    noComp
            Just Cubical
    CErased -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    check
            Maybe Cubical
    Nothing      -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    check)
        ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    -> GHCModuleEnv -> TCM (Recompile GHCModuleEnv GHCModule)
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` GHCEnv -> HsModuleEnv -> GHCModuleEnv
    GHCModuleEnv GHCEnv
    cenv (ModuleName -> Bool -> HsModuleEnv
    HsModuleEnv ModuleName
    m (IsMain
    isMain IsMain -> IsMain -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsMain
    IsMain))
      where
        uptodate :: ReaderT GHCModuleEnv TCM Bool
    uptodate = case Maybe FilePath
    mifile of
          Maybe FilePath
    Nothing -> Bool -> ReaderT GHCModuleEnv TCM Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
          Just FilePath
    ifile -> IO Bool -> ReaderT GHCModuleEnv TCM Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> ReaderT GHCModuleEnv TCM Bool)
    -> ReaderT GHCModuleEnv TCM (IO Bool)
    -> ReaderT GHCModuleEnv TCM Bool
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< FilePath -> FilePath -> IO Bool
    isNewerThan (FilePath -> FilePath -> IO Bool)
    -> ReaderT GHCModuleEnv TCM FilePath
    -> ReaderT GHCModuleEnv TCM (FilePath -> IO Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv TCM FilePath
    forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m FilePath
    curOutFile ReaderT GHCModuleEnv TCM (FilePath -> IO Bool)
    -> ReaderT GHCModuleEnv TCM FilePath
    -> ReaderT GHCModuleEnv TCM (IO Bool)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> FilePath -> ReaderT GHCModuleEnv TCM FilePath
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure FilePath
    ifile
        ifileDesc :: FilePath
    ifileDesc = FilePath -> Maybe FilePath -> FilePath
    forall a. a -> Maybe a -> a
    fromMaybe FilePath
    "(memory)" Maybe FilePath
    mifile

        noComp :: ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    noComp = do
          FilePath -> Nat -> FilePath -> ReaderT GHCModuleEnv TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    FilePath -> Nat -> FilePath -> m ()
    reportSLn FilePath
    "compile.ghc" Nat
    2 (FilePath -> ReaderT GHCModuleEnv TCM ())
    -> (ModuleName -> FilePath)
    -> ModuleName
    -> ReaderT GHCModuleEnv TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " : no compilation is needed.") (FilePath -> FilePath)
    -> (ModuleName -> FilePath) -> ModuleName -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow (QName -> FilePath)
    -> (ModuleName -> QName) -> ModuleName -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> QName
    A.mnameToConcrete (ModuleName -> ReaderT GHCModuleEnv TCM ())
    -> ReaderT GHCModuleEnv TCM ModuleName
    -> ReaderT GHCModuleEnv TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT GHCModuleEnv TCM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
          GHCModuleEnv
    menv <- ReaderT GHCModuleEnv TCM GHCModuleEnv
    forall r (m :: * -> *). MonadReader r m => m r
    ask
          [MainFunctionDef]
    mainDefs <- ReaderT GHCModuleEnv TCM Bool
    -> ReaderT GHCModuleEnv TCM [MainFunctionDef]
    -> ReaderT GHCModuleEnv TCM [MainFunctionDef]
    -> ReaderT GHCModuleEnv TCM [MainFunctionDef]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM ReaderT GHCModuleEnv TCM Bool
    forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
    curIsMainModule
                             (Interface -> [MainFunctionDef]
    mainFunctionDefs (Interface -> [MainFunctionDef])
    -> ReaderT GHCModuleEnv TCM Interface
    -> ReaderT GHCModuleEnv TCM [MainFunctionDef]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv TCM Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF)
                             ([MainFunctionDef] -> ReaderT GHCModuleEnv TCM [MainFunctionDef]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [])
          Recompile menv GHCModule
    -> ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Recompile menv GHCModule
     -> ReaderT GHCModuleEnv TCM (Recompile menv GHCModule))
    -> (GHCModule -> Recompile menv GHCModule)
    -> GHCModule
    -> ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GHCModule -> Recompile menv GHCModule
    forall menv mod. mod -> Recompile menv mod
    Skip (GHCModule -> ReaderT GHCModuleEnv TCM (Recompile menv GHCModule))
    -> GHCModule -> ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    forall a b. (a -> b) -> a -> b
    $ GHCModuleEnv -> [MainFunctionDef] -> GHCModule
    GHCModule GHCModuleEnv
    menv [MainFunctionDef]
    mainDefs

        yesComp :: ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    yesComp = do
          FilePath
    m   <- QName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow (QName -> FilePath)
    -> (ModuleName -> QName) -> ModuleName -> FilePath
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> QName
    A.mnameToConcrete (ModuleName -> FilePath)
    -> ReaderT GHCModuleEnv TCM ModuleName
    -> ReaderT GHCModuleEnv TCM FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv TCM ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
          FilePath
    out <- ReaderT GHCModuleEnv TCM FilePath
    forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m FilePath
    curOutFile
          FilePath -> Nat -> FilePath -> ReaderT GHCModuleEnv TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    FilePath -> Nat -> FilePath -> m ()
    reportSLn FilePath
    "compile.ghc" Nat
    1 (FilePath -> ReaderT GHCModuleEnv TCM ())
    -> FilePath -> ReaderT GHCModuleEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $ [FilePath] -> FilePath -> FilePath
    repl [FilePath
    m, FilePath
    ifileDesc, FilePath
    out] FilePath
    "Compiling <<0>> in <<1>> to <<2>>"
          (GHCModuleEnv -> Recompile GHCModuleEnv GHCModule)
    -> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks GHCModuleEnv -> Recompile GHCModuleEnv GHCModule
    forall menv mod. menv -> Recompile menv mod
    Recompile

    ghcPostModule
      :: GHCEnv
      -> GHCModuleEnv
      -> IsMain        -- ^ Are we looking at the main module?
      -> ModuleName
      -> [GHCDefinition]   -- ^ Compiled module content.
      -> TCM GHCModule
    ghcPostModule :: GHCEnv
    -> GHCModuleEnv
    -> IsMain
    -> ModuleName
    -> [GHCDefinition]
    -> TCM GHCModule
    ghcPostModule GHCEnv
    _cenv GHCModuleEnv
    menv IsMain
    _isMain ModuleName
    _moduleName [GHCDefinition]
    ghcDefs = do
      BuiltinThings PrimFun
    builtinThings <- (TCState -> BuiltinThings PrimFun)
    -> TCMT IO (BuiltinThings PrimFun)
    forall (m :: * -> *) a. ReadTCState m => (TCState -> a) -> m a
    getsTC TCState -> BuiltinThings PrimFun
    stBuiltinThings

      -- Accumulate all of the modules, definitions, declarations, etc.
      let (UsesFloat
    usedFloat, [Decl]
    decls, [Definition]
    defs, [MainFunctionDef]
    mainDefs, Set ModuleName
    usedModules) = [(UsesFloat, [Decl], [Definition], [MainFunctionDef],
      Set ModuleName)]
    -> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
        Set ModuleName)
    forall a. Monoid a => [a] -> a
    mconcat ([(UsesFloat, [Decl], [Definition], [MainFunctionDef],
       Set ModuleName)]
     -> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
         Set ModuleName))
    -> [(UsesFloat, [Decl], [Definition], [MainFunctionDef],
         Set ModuleName)]
    -> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
        Set ModuleName)
    forall a b. (a -> b) -> a -> b
    $
            (\(GHCDefinition UsesFloat
    useFloat' [Decl]
    decls' Definition
    def' Maybe MainFunctionDef
    md' Set ModuleName
    imps')
             -> (UsesFloat
    useFloat', [Decl]
    decls', [Definition
    def'], Maybe MainFunctionDef -> [MainFunctionDef]
    forall a. Maybe a -> [a]
    maybeToList Maybe MainFunctionDef
    md', Set ModuleName
    imps'))
            (GHCDefinition
     -> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
         Set ModuleName))
    -> [GHCDefinition]
    -> [(UsesFloat, [Decl], [Definition], [MainFunctionDef],
         Set ModuleName)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [GHCDefinition]
    ghcDefs

      let imps :: [ImportDecl]
    imps = UsesFloat -> [ImportDecl]
    mazRTEFloatImport UsesFloat
    usedFloat [ImportDecl] -> [ImportDecl] -> [ImportDecl]
    forall a. [a] -> [a] -> [a]
    ++ BuiltinThings PrimFun
    -> Set ModuleName -> [Definition] -> [ImportDecl]
    imports BuiltinThings PrimFun
    builtinThings Set ModuleName
    usedModules [Definition]
    defs

      Interface
    i <- TCMT IO Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF

      -- Get content of FOREIGN pragmas.
      let ([FilePath]
    headerPragmas, [FilePath]
    hsImps, [FilePath]
    code) = Interface -> ([FilePath], [FilePath], [FilePath])
    foreignHaskell Interface
    i

      (ReaderT GHCModuleEnv TCM () -> GHCModuleEnv -> TCM ())
    -> GHCModuleEnv -> ReaderT GHCModuleEnv TCM () -> TCM ()
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ReaderT GHCModuleEnv TCM () -> GHCModuleEnv -> TCM ()
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT GHCModuleEnv
    menv (ReaderT GHCModuleEnv TCM () -> TCM ())
    -> ReaderT GHCModuleEnv TCM () -> TCM ()
    forall a b. (a -> b) -> a -> b
    $ do
        ModuleName
    hsModuleName <- ReaderT GHCModuleEnv TCM ModuleName
    forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curHsMod
        Module -> ReaderT GHCModuleEnv TCM ()
    forall (m :: * -> *). MonadGHCIO m => Module -> m ()
    writeModule (Module -> ReaderT GHCModuleEnv TCM ())
    -> Module -> ReaderT GHCModuleEnv TCM ()
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
    HS.Module
          ModuleName
    hsModuleName
          ((FilePath -> ModulePragma) -> [FilePath] -> [ModulePragma]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> ModulePragma
    HS.OtherPragma [FilePath]
    headerPragmas)
          [ImportDecl]
    imps
          ((FilePath -> Decl) -> [FilePath] -> [Decl]
    forall a b. (a -> b) -> [a] -> [b]
    map FilePath -> Decl
    fakeDecl ([FilePath]
    hsImps [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ [FilePath]
    code) [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++ [Decl]
    decls)

      GHCModule -> TCM GHCModule
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GHCModule -> TCM GHCModule) -> GHCModule -> TCM GHCModule
    forall a b. (a -> b) -> a -> b
    $ GHCModuleEnv -> [MainFunctionDef] -> GHCModule
    GHCModule GHCModuleEnv
    menv [MainFunctionDef]
    mainDefs

    ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
    ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
    ghcCompileDef GHCEnv
    _cenv GHCModuleEnv
    menv IsMain
    _isMain Definition
    def = do
      ((UsesFloat
    usesFloat, [Decl]
    decls, Maybe CheckedMainFunctionDef
    mainFuncDef), (HsCompileState Set ModuleName
    imps)) <-
        Definition
    -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    definition Definition
    def HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    -> GHCModuleEnv
    -> TCM
         ((UsesFloat, [Decl], Maybe CheckedMainFunctionDef), HsCompileState)
    forall (m :: * -> *) a.
    HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
    `runHsCompileT` GHCModuleEnv
    menv
      GHCDefinition -> TCM GHCDefinition
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GHCDefinition -> TCM GHCDefinition)
    -> GHCDefinition -> TCM GHCDefinition
    forall a b. (a -> b) -> a -> b
    $ UsesFloat
    -> [Decl]
    -> Definition
    -> Maybe MainFunctionDef
    -> Set ModuleName
    -> GHCDefinition
    GHCDefinition UsesFloat
    usesFloat [Decl]
    decls Definition
    def (CheckedMainFunctionDef -> MainFunctionDef
    checkedMainDef (CheckedMainFunctionDef -> MainFunctionDef)
    -> Maybe CheckedMainFunctionDef -> Maybe MainFunctionDef
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CheckedMainFunctionDef
    mainFuncDef) Set ModuleName
    imps

    -- | We do not erase types that have a 'HsData' pragma.
    --   This is to ensure a stable interface to third-party code.
    ghcMayEraseType :: QName -> TCM Bool
    ghcMayEraseType :: QName -> TCM Bool
    ghcMayEraseType QName
    q = QName -> TCM (Maybe HaskellPragma)
    getHaskellPragma QName
    q TCM (Maybe HaskellPragma)
    -> (Maybe HaskellPragma -> Bool) -> TCM Bool
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \case
      -- Andreas, 2019-05-09, issue #3732.
      -- We restrict this to 'HsData' since types like @Size@, @Level@
      -- should be erased although they have a 'HsType' binding to the
      -- Haskell unit type.
      Just HsData{} -> Bool
    False
      Maybe HaskellPragma
    _ -> Bool
    True

    -- Compilation ------------------------------------------------------------

    imports :: BuiltinThings PrimFun -> Set ModuleName -> [Definition] -> [HS.ImportDecl]
    imports :: BuiltinThings PrimFun
    -> Set ModuleName -> [Definition] -> [ImportDecl]
    imports BuiltinThings PrimFun
    builtinThings Set ModuleName
    usedModules [Definition]
    defs = [ImportDecl]
    hsImps [ImportDecl] -> [ImportDecl] -> [ImportDecl]
    forall a. [a] -> [a] -> [a]
    ++ [ImportDecl]
    imps where
      hsImps :: [HS.ImportDecl]
      hsImps :: [ImportDecl]
    hsImps = [ImportDecl
    unqualRTE, ModuleName -> ImportDecl
    decl ModuleName
    mazRTE]

      unqualRTE :: HS.ImportDecl
      unqualRTE :: ImportDecl
    unqualRTE = ModuleName -> Bool -> Maybe (Bool, [ImportSpec]) -> ImportDecl
    HS.ImportDecl ModuleName
    mazRTE Bool
    False (Maybe (Bool, [ImportSpec]) -> ImportDecl)
    -> Maybe (Bool, [ImportSpec]) -> ImportDecl
    forall a b. (a -> b) -> a -> b
    $ (Bool, [ImportSpec]) -> Maybe (Bool, [ImportSpec])
    forall a. a -> Maybe a
    Just ((Bool, [ImportSpec]) -> Maybe (Bool, [ImportSpec]))
    -> (Bool, [ImportSpec]) -> Maybe (Bool, [ImportSpec])
    forall a b. (a -> b) -> a -> b
    $
                  (Bool
    False, [ Name -> ImportSpec
    HS.IVar (Name -> ImportSpec) -> Name -> ImportSpec
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    x
                          | FilePath
    x <- [FilePath
    mazCoerceName, FilePath
    mazErasedName, FilePath
    mazAnyTypeName] [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++
                                 (TPrim -> FilePath) -> [TPrim] -> [FilePath]
    forall a b. (a -> b) -> [a] -> [b]
    map TPrim -> FilePath
    treelessPrimName [TPrim]
    rtePrims ])

      rtePrims :: [TPrim]
    rtePrims = [TPrim
    T.PAdd, TPrim
    T.PSub, TPrim
    T.PMul, TPrim
    T.PQuot, TPrim
    T.PRem, TPrim
    T.PGeq, TPrim
    T.PLt, TPrim
    T.PEqI,
                  TPrim
    T.PAdd64, TPrim
    T.PSub64, TPrim
    T.PMul64, TPrim
    T.PQuot64, TPrim
    T.PRem64, TPrim
    T.PLt64, TPrim
    T.PEq64,
                  TPrim
    T.PITo64, TPrim
    T.P64ToI] -- Excludes T.PEqF, which is defined in MAlonzo.RTE.Float

      imps :: [HS.ImportDecl]
      imps :: [ImportDecl]
    imps = (ModuleName -> ImportDecl) -> [ModuleName] -> [ImportDecl]
    forall a b. (a -> b) -> [a] -> [b]
    map ModuleName -> ImportDecl
    decl ([ModuleName] -> [ImportDecl]) -> [ModuleName] -> [ImportDecl]
    forall a b. (a -> b) -> a -> b
    $ [ModuleName] -> [ModuleName]
    uniq ([ModuleName] -> [ModuleName]) -> [ModuleName] -> [ModuleName]
    forall a b. (a -> b) -> a -> b
    $ BuiltinThings PrimFun -> [Definition] -> [ModuleName]
    importsForPrim BuiltinThings PrimFun
    builtinThings [Definition]
    defs [ModuleName] -> [ModuleName] -> [ModuleName]
    forall a. [a] -> [a] -> [a]
    ++ (ModuleName -> ModuleName) -> [ModuleName] -> [ModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    map ModuleName -> ModuleName
    mazMod [ModuleName]
    mnames

      decl :: HS.ModuleName -> HS.ImportDecl
      decl :: ModuleName -> ImportDecl
    decl ModuleName
    m = ModuleName -> Bool -> Maybe (Bool, [ImportSpec]) -> ImportDecl
    HS.ImportDecl ModuleName
    m Bool
    True Maybe (Bool, [ImportSpec])
    forall a. Maybe a
    Nothing

      mnames :: [ModuleName]
      mnames :: [ModuleName]
    mnames = Set ModuleName -> [ModuleName]
    forall a. Set a -> [a]
    Set.elems Set ModuleName
    usedModules

      uniq :: [HS.ModuleName] -> [HS.ModuleName]
      uniq :: [ModuleName] -> [ModuleName]
    uniq = ([ModuleName] -> ModuleName) -> [[ModuleName]] -> [ModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    List.map [ModuleName] -> ModuleName
    forall a. [a] -> a
    head ([[ModuleName]] -> [ModuleName])
    -> ([ModuleName] -> [[ModuleName]]) -> [ModuleName] -> [ModuleName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ModuleName] -> [[ModuleName]]
    forall a. Eq a => [a] -> [[a]]
    List.group ([ModuleName] -> [[ModuleName]])
    -> ([ModuleName] -> [ModuleName]) -> [ModuleName] -> [[ModuleName]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ModuleName] -> [ModuleName]
    forall a. Ord a => [a] -> [a]
    List.sort

    -- Should we import MAlonzo.RTE.Float
    newtype UsesFloat = UsesFloat Bool deriving (UsesFloat -> UsesFloat -> Bool
    (UsesFloat -> UsesFloat -> Bool)
    -> (UsesFloat -> UsesFloat -> Bool) -> Eq UsesFloat
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: UsesFloat -> UsesFloat -> Bool
    $c/= :: UsesFloat -> UsesFloat -> Bool
    == :: UsesFloat -> UsesFloat -> Bool
    $c== :: UsesFloat -> UsesFloat -> Bool
    Eq, Nat -> UsesFloat -> FilePath -> FilePath
    [UsesFloat] -> FilePath -> FilePath
    UsesFloat -> FilePath
    (Nat -> UsesFloat -> FilePath -> FilePath)
    -> (UsesFloat -> FilePath)
    -> ([UsesFloat] -> FilePath -> FilePath)
    -> Show UsesFloat
    forall a.
    (Nat -> a -> FilePath -> FilePath)
    -> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
    showList :: [UsesFloat] -> FilePath -> FilePath
    $cshowList :: [UsesFloat] -> FilePath -> FilePath
    show :: UsesFloat -> FilePath
    $cshow :: UsesFloat -> FilePath
    showsPrec :: Nat -> UsesFloat -> FilePath -> FilePath
    $cshowsPrec :: Nat -> UsesFloat -> FilePath -> FilePath
    Show)

    pattern YesFloat :: UsesFloat
    pattern $bYesFloat :: UsesFloat
    $mYesFloat :: forall {r}. UsesFloat -> (Void# -> r) -> (Void# -> r) -> r
    YesFloat = UsesFloat True

    pattern NoFloat :: UsesFloat
    pattern $bNoFloat :: UsesFloat
    $mNoFloat :: forall {r}. UsesFloat -> (Void# -> r) -> (Void# -> r) -> r
    NoFloat = UsesFloat False

    instance Semigroup UsesFloat where
      UsesFloat Bool
    a <> :: UsesFloat -> UsesFloat -> UsesFloat
    <> UsesFloat Bool
    b = Bool -> UsesFloat
    UsesFloat (Bool
    a Bool -> Bool -> Bool
    || Bool
    b)

    instance Monoid UsesFloat where
      mempty :: UsesFloat
    mempty  = UsesFloat
    NoFloat
      mappend :: UsesFloat -> UsesFloat -> UsesFloat
    mappend = UsesFloat -> UsesFloat -> UsesFloat
    forall a. Semigroup a => a -> a -> a
    (<>)

    mazRTEFloatImport :: UsesFloat -> [HS.ImportDecl]
    mazRTEFloatImport :: UsesFloat -> [ImportDecl]
    mazRTEFloatImport (UsesFloat Bool
    b) = [ ModuleName -> Bool -> Maybe (Bool, [ImportSpec]) -> ImportDecl
    HS.ImportDecl ModuleName
    mazRTEFloat Bool
    True Maybe (Bool, [ImportSpec])
    forall a. Maybe a
    Nothing | Bool
    b ]

    --------------------------------------------------
    -- Main compiling clauses
    --------------------------------------------------

    definition :: Definition -> HsCompileM (UsesFloat, [HS.Decl], Maybe CheckedMainFunctionDef)
    -- ignore irrelevant definitions
    {- Andreas, 2012-10-02: Invariant no longer holds
    definition kit (Defn NonStrict _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
    -}
    definition :: Definition
    -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    definition Defn{defArgInfo :: Definition -> ArgInfo
    defArgInfo = ArgInfo
    info, defName :: Definition -> QName
    defName = QName
    q} | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ ArgInfo -> Bool
    forall a. LensModality a => a -> Bool
    usableModality ArgInfo
    info = do
      FilePath
    -> Nat
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    MonadDebug m =>
    FilePath -> Nat -> TCMT IO Doc -> m ()
    reportSDoc FilePath
    "compile.ghc.definition" Nat
    10 (TCMT IO Doc
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $
        (TCMT IO Doc
    "Not compiling" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    "."
      (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UsesFloat
    forall a. Monoid a => a
    mempty, [Decl]
    forall a. Monoid a => a
    mempty, Maybe CheckedMainFunctionDef
    forall a. Maybe a
    Nothing)
    definition def :: Definition
    def@Defn{defName :: Definition -> QName
    defName = QName
    q, defType :: Definition -> Type
    defType = Type
    ty, theDef :: Definition -> Defn
    theDef = Defn
    d} = do
      FilePath
    -> Nat
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    MonadDebug m =>
    FilePath -> Nat -> TCMT IO Doc -> m ()
    reportSDoc FilePath
    "compile.ghc.definition" Nat
    10 (TCMT IO Doc
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ (TCMT IO Doc
    "Compiling" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM QName
    q) TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall a. Semigroup a => a -> a -> a
    <> TCMT IO Doc
    ":"
        , Nat -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $ Defn -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Defn
    d
        ]
      Maybe HaskellPragma
    pragma <- TCM (Maybe HaskellPragma)
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe HaskellPragma)
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma))
    -> TCM (Maybe HaskellPragma)
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM (Maybe HaskellPragma)
    getHaskellPragma QName
    q
      GHCEnv
    env <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
    askGHCEnv
      let is :: (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    p = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    p GHCEnv
    env
      Maybe CheckedMainFunctionDef
    typeCheckedMainDef <- Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
    checkTypeOfMain Definition
    def
      let mainDecl :: [Decl]
    mainDecl = Maybe Decl -> [Decl]
    forall a. Maybe a -> [a]
    maybeToList (Maybe Decl -> [Decl]) -> Maybe Decl -> [Decl]
    forall a b. (a -> b) -> a -> b
    $ CheckedMainFunctionDef -> Decl
    checkedMainDecl (CheckedMainFunctionDef -> Decl)
    -> Maybe CheckedMainFunctionDef -> Maybe Decl
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Maybe CheckedMainFunctionDef
    typeCheckedMainDef
      let retDecls :: b -> m (a, b)
    retDecls b
    ds = (a, b) -> m (a, b)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    forall a. Monoid a => a
    mempty, b
    ds)
      ((UsesFloat
     -> [Decl] -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef))
    -> (UsesFloat, [Decl])
    -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry (,,Maybe CheckedMainFunctionDef
    typeCheckedMainDef)) ((UsesFloat, [Decl])
     -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef))
    -> ((UsesFloat, [Decl]) -> (UsesFloat, [Decl]))
    -> (UsesFloat, [Decl])
    -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ([Decl] -> [Decl]) -> (UsesFloat, [Decl]) -> (UsesFloat, [Decl])
    forall (a :: * -> * -> *) b c d.
    Arrow a =>
    a b c -> a (d, b) (d, c)
    second (([Decl]
    mainDecl [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++) ([Decl] -> [Decl]) -> ([Decl] -> [Decl]) -> [Decl] -> [Decl]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> [Decl] -> [Decl]
    infodecl QName
    q) ((UsesFloat, [Decl])
     -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
        case Defn
    d of

          Defn
    _ | Just (HsDefn Range
    r FilePath
    hs) <- Maybe HaskellPragma
    pragma -> Range
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (ReaderT
       GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              if (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvFlat
              then FilePath
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    FilePath -> m a
    genericError
                    FilePath
    "\"COMPILE GHC\" pragmas are not allowed for the FLAT builtin."
              else do
                -- Make sure we have imports for all names mentioned in the type.
                Type
    hsty <- QName -> HsCompileM Type
    haskellType QName
    q
                (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName)
    -> Set QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (QName
    -> Name -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    `xqual` FilePath -> Name
    HS.Ident FilePath
    "_") (Type -> Set QName
    forall a m. (NamesIn a, Collection QName m) => a -> m
    namesIn Type
    ty :: Set QName)

              -- Check that the function isn't INLINE (since that will make this
              -- definition pointless).
                Bool
    inline <- (Defn -> Lens' Bool Defn -> Bool
    forall o i. o -> Lens' i o -> i
    ^. Lens' Bool Defn
    funInline) (Defn -> Bool) -> (Definition -> Defn) -> Definition -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> Bool)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
                Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when Bool
    inline (ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> Warning
    UselessInline QName
    q

                [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ Type -> Exp -> [Decl]
    fbWithType Type
    hsty (FilePath -> Exp
    fakeExp FilePath
    hs)

          -- Compiling Bool
          Datatype{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvBool -> do
            ()
    _ <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primTrue, ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primFalse] -- Just to get the proper error for missing TRUE/FALSE
            let d :: Name
    d = QName -> Name
    dname QName
    q
            Just QName
    true  <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinTrue
            Just QName
    false <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinFalse
            [Decl]
    cs <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    forall a. Maybe a
    Nothing) [QName
    false, QName
    true]
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ [ QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    "Bool" Nat
    0
                       , [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    d [] (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds] ] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
                       [Decl]
    cs

          -- Compiling List
          Datatype{ dataPars :: Defn -> Nat
    dataPars = Nat
    np } | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvList -> do
            ()
    _ <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNil, ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primCons] -- Just to get the proper error for missing NIL/CONS
            Maybe HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> (HaskellPragma
        -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe HaskellPragma
    pragma (() -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((HaskellPragma
      -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> (HaskellPragma
        -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ \ HaskellPragma
    p -> HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange HaskellPragma
    p (ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> (Doc -> Warning)
    -> Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Warning
    GenericWarning (Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc)
    -> [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
    forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
    pwords FilePath
    "Ignoring GHC pragma for builtin lists; they always compile to Haskell lists."
            let d :: Name
    d = QName -> Name
    dname QName
    q
                t :: Name
    t = NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q
            Just QName
    nil  <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinNil
            Just QName
    cons <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinCons
            let vars :: (Name -> b) -> Nat -> [b]
    vars Name -> b
    f Nat
    n = (Nat -> b) -> [Nat] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> b
    f (Name -> b) -> (Nat -> Name) -> Nat -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VariableKind -> Nat -> Name
    ihname VariableKind
    A) [Nat
    0 .. Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
            [Decl]
    cs <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    forall a. Maybe a
    Nothing) [QName
    nil, QName
    cons]
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ [ Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl Name
    t ((Name -> TyVarBind) -> Nat -> [TyVarBind]
    forall {b}. (Name -> b) -> Nat -> [b]
    vars Name -> TyVarBind
    HS.UnkindedVar (Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)) (FilePath -> Type
    HS.FakeType FilePath
    "[]")
                       , [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    d ((Name -> Pat) -> Nat -> [Pat]
    forall {b}. (Name -> b) -> Nat -> [b]
    vars Name -> Pat
    HS.PVar Nat
    np) (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds] ] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
                       [Decl]
    cs

          -- Compiling Maybe
          Datatype{ dataPars :: Defn -> Nat
    dataPars = Nat
    np } | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvMaybe -> do
            ()
    _ <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primNothing, ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primJust] -- Just to get the proper error for missing NOTHING/JUST
            Maybe HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> (HaskellPragma
        -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. Maybe a -> b -> (a -> b) -> b
    caseMaybe Maybe HaskellPragma
    pragma (() -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((HaskellPragma
      -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> (HaskellPragma
        -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ \ HaskellPragma
    p -> HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange HaskellPragma
    p (ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> (Doc -> Warning)
    -> Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc -> Warning
    GenericWarning (Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
              [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep ([ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc)
    -> [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc
    forall a b. (a -> b) -> a -> b
    $ FilePath -> [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
    forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
    pwords FilePath
    "Ignoring GHC pragma for builtin maybe; they always compile to Haskell lists."
            let d :: Name
    d = QName -> Name
    dname QName
    q
                t :: Name
    t = NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q
            Just QName
    nothing <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinNothing
            Just QName
    just    <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinJust
            let vars :: (Name -> b) -> Nat -> [b]
    vars Name -> b
    f Nat
    n = (Nat -> b) -> [Nat] -> [b]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> b
    f (Name -> b) -> (Nat -> Name) -> Nat -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VariableKind -> Nat -> Name
    ihname VariableKind
    A) [Nat
    0 .. Nat
    n Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
            [Decl]
    cs <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    forall a. Maybe a
    Nothing) [QName
    nothing, QName
    just]
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ [ Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl Name
    t ((Name -> TyVarBind) -> Nat -> [TyVarBind]
    forall {b}. (Name -> b) -> Nat -> [b]
    vars Name -> TyVarBind
    HS.UnkindedVar (Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1)) (FilePath -> Type
    HS.FakeType FilePath
    "Maybe")
                       , [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    d ((Name -> Pat) -> Nat -> [Pat]
    forall {b}. (Name -> b) -> Nat -> [b]
    vars Name -> Pat
    HS.PVar Nat
    np) (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds] ] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
                       [Decl]
    cs

          -- Compiling Inf
          Defn
    _ | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvInf -> do
            Term
    _ <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primSharp -- To get a proper error for missing SHARP.
            Just QName
    sharp <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinSharp
            Decl
    sharpC     <- (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    forall a. Maybe a
    Nothing) QName
    sharp
            let d :: Name
    d   = QName -> Name
    dname QName
    q
                err :: FilePath
    err = FilePath
    "No term-level implementation of the INFINITY builtin."
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ [ QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    "MAlonzo.RTE.Infinity" Nat
    2
                       , [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    d [Name -> Pat
    HS.PVar (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    0)]
                           (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp (FilePath
    "error " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath -> FilePath
    forall a. Show a => a -> FilePath
    show FilePath
    err)))
                           Maybe Binds
    emptyBinds]
                       , Decl
    sharpC
                       ]

          -- The interval is compiled as the type of booleans: 0 is
          -- compiled as False and 1 as True.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvInterval -> do
            ()
    _       <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIZero, ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primIOne]
            Just QName
    i0 <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIZero
            Just QName
    i1 <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinIOne
            [Decl]
    cs      <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl (Nat -> Maybe Nat
    forall a. a -> Maybe a
    Just Nat
    0)) [QName
    i0, QName
    i1]
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    "Bool" Nat
    0
              , [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds]
              ] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
              [Decl]
    cs

          -- IsOne is compiled as the constant function to the unit type.
          -- Partial/PartialP are compiled as functions from the unit type
          -- to the underlying type.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvIsOne -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl (NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q) [Name -> TyVarBind
    HS.UnkindedVar (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    0)]
                  (FilePath -> Type
    HS.FakeType FilePath
    "()")
              , [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds]
              ]

          -- itIsOne.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvItIsOne -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds]
              ]

          -- IsOne1/IsOne2.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvIsOne1 Bool -> Bool -> Bool
    || (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvIsOne2 -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    "\\_ _ _ -> ()"))
                     Maybe Binds
    emptyBinds]
              ]

          -- isOneEmpty.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvIsOneEmpty -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    "\\_ x _ -> x ()"))
                     Maybe Binds
    emptyBinds]
              ]

          -- PathP is compiled as a function from the interval (booleans)
          -- to the underlying type.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvPathP -> do
            ()
    _        <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInterval]
            Just QName
    int <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinInterval
            QName
    int      <- NameKind
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    xhqn NameKind
    TypeK QName
    int
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl (NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q)
                  [Name -> TyVarBind
    HS.UnkindedVar (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    i) | Nat
    i <- [Nat
    0..Nat
    3]]
                  (Type -> Type -> Type
    HS.TyFun (QName -> Type
    HS.TyCon QName
    int) Type
    mazAnyType)
              , [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    "\\_ _ _ _ -> ()"))
                     Maybe Binds
    emptyBinds]
              ]

          -- Sub is compiled as the underlying type.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvSub -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl (NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q)
                  [Name -> TyVarBind
    HS.UnkindedVar (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    i) | Nat
    i <- [Nat
    0..Nat
    3]]
                  (Name -> Type
    HS.TyVar (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    1))
              , [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    "\\_ _ _ _ -> ()"))
                     Maybe Binds
    emptyBinds]
              ]

          -- subIn.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvSubIn -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    "\\_ _ _ x -> x"))
                     Maybe Binds
    emptyBinds]
              ]

          -- Id x y is compiled as a pair of a boolean and whatever
          -- Path x y is compiled to.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvId -> do
            ()
    _        <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (t :: * -> *) (m :: * -> *) a.
    (Foldable t, Monad m) =>
    t (m a) -> m ()
    sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primInterval]
            Just QName
    int <- FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    FilePath -> m (Maybe QName)
    getBuiltinName FilePath
    builtinInterval
            QName
    int      <- NameKind
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    xhqn NameKind
    TypeK QName
    int
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl (NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q)
                  [Name -> TyVarBind
    HS.UnkindedVar (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    i) | Nat
    i <- [Nat
    0..Nat
    3]]
                  (Type -> Type -> Type
    HS.TyApp (FilePath -> Type
    HS.FakeType FilePath
    "(,) Bool")
                     (Type -> Type -> Type
    HS.TyFun (QName -> Type
    HS.TyCon QName
    int) Type
    mazAnyType))
              , [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    "\\_ _ _ _ -> ()"))
                     Maybe Binds
    emptyBinds]
              ]

          -- conid.
          Axiom{} | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvConId -> do
            Bool
    strict <- GHCOptions -> Bool
    optGhcStrictData (GHCOptions -> Bool)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
            let var :: Name -> Pat
    var = (if Bool
    strict then Pat -> Pat
    HS.PBangPat else Pat -> Pat
    forall a. a -> a
    id) (Pat -> Pat) -> (Name -> Pat) -> Name -> Pat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Pat
    HS.PVar
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q)
                     [ Name -> Pat
    var (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    i) | Nat
    i <- [Nat
    0..Nat
    1] ]
                     (Exp -> Rhs
    HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
    forall a b. (a -> b) -> a -> b
    $
                      Exp -> Exp -> Exp
    HS.App (Exp -> Exp -> Exp
    HS.App (FilePath -> Exp
    HS.FakeExp FilePath
    "(,)")
                                (QName -> Exp
    HS.Var (Name -> QName
    HS.UnQual (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    0))))
                        (QName -> Exp
    HS.Var (Name -> QName
    HS.UnQual (VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    1))))
                     Maybe Binds
    emptyBinds]
              ]

          -- TC builtins are compiled to erased, which is an ∞-ary
          -- function.
          Axiom{} | GHCEnv -> QName -> Bool
    ghcEnvIsTCBuiltin GHCEnv
    env QName
    q -> do
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
              [ [Match] -> Decl
    HS.FunBind
                  [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                     (Exp -> Rhs
    HS.UnGuardedRhs (FilePath -> Exp
    HS.FakeExp FilePath
    mazErasedName))
                     Maybe Binds
    emptyBinds]
              ]

          DataOrRecSig{} -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          Axiom{} -> do
            Nat
    ar <- TCM Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat)
    -> TCM Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a b. (a -> b) -> a -> b
    $ Type -> TCM Nat
    typeArity Type
    ty
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ [ QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    ty Nat
    ar | Just (HsType Range
    r FilePath
    ty) <- [Maybe HaskellPragma
    pragma] ] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
                       Exp -> [Decl]
    fb Exp
    axiomErr
          Primitive{ primName :: Defn -> FilePath
    primName = FilePath
    s } -> (UsesFloat
    forall a. Monoid a => a
    mempty,) ([Decl] -> (UsesFloat, [Decl]))
    -> (Exp -> [Decl]) -> Exp -> (UsesFloat, [Decl])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Exp -> [Decl]
    fb (Exp -> (UsesFloat, [Decl]))
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TCM Exp -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Exp -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp)
    -> (FilePath -> TCM Exp)
    -> FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FilePath -> TCM Exp
    forall (m :: * -> *). MonadTCError m => FilePath -> m Exp
    primBody) FilePath
    s

          PrimitiveSort{ primName :: Defn -> FilePath
    primName = FilePath
    s } -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls []

          Function{} -> Maybe HaskellPragma
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    function Maybe HaskellPragma
    pragma (ReaderT
       GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ QName
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    functionViaTreeless QName
    q

          Datatype{ dataPars :: Defn -> Nat
    dataPars = Nat
    np, dataIxs :: Defn -> Nat
    dataIxs = Nat
    ni, dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    cl
                  , dataPathCons :: Defn -> [QName]
    dataPathCons = [QName]
    pcs
                  } | Just hsdata :: HaskellPragma
    hsdata@(HsData Range
    r FilePath
    ty [FilePath]
    hsCons) <- Maybe HaskellPragma
    pragma ->
            Range
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (ReaderT
       GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ do
            FilePath
    -> Nat
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    MonadDebug m =>
    FilePath -> Nat -> TCMT IO Doc -> m ()
    reportSDoc FilePath
    "compile.ghc.definition" Nat
    40 (TCMT IO Doc
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ [TCMT IO Doc] -> TCMT IO Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
    forall a b. (a -> b) -> a -> b
    $
              [ TCMT IO Doc
    "Compiling data type with COMPILE pragma ...", HaskellPragma -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty HaskellPragma
    hsdata ]
            TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM ()
    computeErasedConstructorArgs QName
    q
            [QName]
    cs <- TCM [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [QName]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName])
    -> TCM [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM [QName]
    getNotErasedConstructors QName
    q
            [Decl]
    ccscov <- QName
    -> Nat
    -> [QName]
    -> FilePath
    -> [FilePath]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    constructorCoverageCode QName
    q (Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    ni) [QName]
    cs FilePath
    ty [FilePath]
    hsCons
            [Decl]
    cds <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    forall a. Maybe a
    Nothing) [QName]
    cs
            let result :: [Decl]
    result = [[Decl]] -> [Decl]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Decl]] -> [Decl]) -> [[Decl]] -> [Decl]
    forall a b. (a -> b) -> a -> b
    $
                  [ QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
    tvaldecl QName
    q Induction
    Inductive (Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    ni) [] (Clause -> Maybe Clause
    forall a. a -> Maybe a
    Just Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__)
                  , [ QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    ty Nat
    np ]
                  , [Decl]
    cds
                  , [Decl]
    ccscov
                  ]
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls [Decl]
    result
          Datatype{ dataPars :: Defn -> Nat
    dataPars = Nat
    np, dataIxs :: Defn -> Nat
    dataIxs = Nat
    ni, dataClause :: Defn -> Maybe Clause
    dataClause = Maybe Clause
    cl
                  , dataPathCons :: Defn -> [QName]
    dataPathCons = [QName]
    pcs
                  } -> do
            TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM ()
    computeErasedConstructorArgs QName
    q
            [QName]
    cs <- TCM [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [QName]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName])
    -> TCM [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM [QName]
    getNotErasedConstructors QName
    q
            [ConDecl]
    cds <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [ConDecl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM ((QName
     -> Induction
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl)
    -> Induction
    -> QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip QName
    -> Induction
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    condecl Induction
    Inductive) [QName]
    cs
            [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
    tvaldecl QName
    q Induction
    Inductive (Nat
    np Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    + Nat
    ni) [ConDecl]
    cds Maybe Clause
    cl
          Constructor{} -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls []
          GeneralizableVar{} -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls []
          Record{ recPars :: Defn -> Nat
    recPars = Nat
    np, recClause :: Defn -> Maybe Clause
    recClause = Maybe Clause
    cl, recConHead :: Defn -> ConHead
    recConHead = ConHead
    con,
                  recInduction :: Defn -> Maybe Induction
    recInduction = Maybe Induction
    ind } ->
            let -- Non-recursive record types are treated as being
                -- inductive.
                inductionKind :: Induction
    inductionKind = Induction -> Maybe Induction -> Induction
    forall a. a -> Maybe a -> a
    fromMaybe Induction
    Inductive Maybe Induction
    ind
            in case Maybe HaskellPragma
    pragma of
              Just (HsData Range
    r FilePath
    ty [FilePath]
    hsCons) -> Range
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (ReaderT
       GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ do
                let cs :: [QName]
    cs = [ConHead -> QName
    conName ConHead
    con]
                TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM ()
    computeErasedConstructorArgs QName
    q
                [Decl]
    ccscov <- QName
    -> Nat
    -> [QName]
    -> FilePath
    -> [FilePath]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    constructorCoverageCode QName
    q Nat
    np [QName]
    cs FilePath
    ty [FilePath]
    hsCons
                [Decl]
    cds <- (QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    forall a. Maybe a
    Nothing) [QName]
    cs
                [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $
                  QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
    tvaldecl QName
    q Induction
    inductionKind Nat
    np [] (Clause -> Maybe Clause
    forall a. a -> Maybe a
    Just Clause
    forall a. HasCallStack => a
    __IMPOSSIBLE__) [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
                  [QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    ty Nat
    np] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++ [Decl]
    cds [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++ [Decl]
    ccscov
              Maybe HaskellPragma
    _ -> do
                TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM ()
    computeErasedConstructorArgs QName
    q
                ConDecl
    cd <- QName
    -> Induction
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    condecl (ConHead -> QName
    conName ConHead
    con) Induction
    inductionKind
                [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
    retDecls ([Decl]
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> [Decl]
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
    tvaldecl QName
    q Induction
    inductionKind (Type -> Nat
    I.arity Type
    ty) [ConDecl
    cd] Maybe Clause
    cl
          AbstractDefn{} -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
      function :: Maybe HaskellPragma -> HsCompileM (UsesFloat, [HS.Decl]) -> HsCompileM (UsesFloat, [HS.Decl])
      function :: Maybe HaskellPragma
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    function Maybe HaskellPragma
    mhe ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    fun = do
        (UsesFloat
    imp, [Decl]
    ccls) <- ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    fun
        case Maybe HaskellPragma
    mhe of
          Just (HsExport Range
    r FilePath
    name) -> Range
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (ReaderT
       GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ do
            GHCEnv
    env <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
    askGHCEnv
            if QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    ghcEnvFlat GHCEnv
    env
            then FilePath
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    FilePath -> m a
    genericError
                  FilePath
    "\"COMPILE GHC as\" pragmas are not allowed for the FLAT builtin."
            else do
              Type
    t <- Range -> HsCompileM Type -> HsCompileM Type
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (HsCompileM Type -> HsCompileM Type)
    -> HsCompileM Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ QName -> HsCompileM Type
    haskellType QName
    q
              let tsig :: HS.Decl
                  tsig :: Decl
    tsig = [Name] -> Type -> Decl
    HS.TypeSig [FilePath -> Name
    HS.Ident FilePath
    name] Type
    t

                  def :: HS.Decl
                  def :: Decl
    def = [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (FilePath -> Name
    HS.Ident FilePath
    name) [] (Exp -> Rhs
    HS.UnGuardedRhs (Exp -> Exp
    hsCoerce (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Name -> Exp
    hsVarUQ (Name -> Exp) -> Name -> Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    dname QName
    q)) Maybe Binds
    emptyBinds]
              (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UsesFloat
    imp, [Decl
    tsig,Decl
    def] [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++ [Decl]
    ccls)
          Maybe HaskellPragma
    _ -> (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UsesFloat
    imp, [Decl]
    ccls)

      functionViaTreeless :: QName -> HsCompileM (UsesFloat, [HS.Decl])
      functionViaTreeless :: QName
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    functionViaTreeless QName
    q = do
        Bool
    strict <- GHCOptions -> Bool
    optGhcStrict (GHCOptions -> Bool)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
        let eval :: EvaluationStrategy
    eval = if Bool
    strict then EvaluationStrategy
    EagerEvaluation else EvaluationStrategy
    LazyEvaluation
        ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe TTerm)
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    -> (TTerm
        -> ReaderT
             GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (TCM (Maybe TTerm)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe TTerm)
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe TTerm)
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe TTerm))
    -> TCM (Maybe TTerm)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe TTerm)
    forall a b. (a -> b) -> a -> b
    $ EvaluationStrategy -> QName -> TCM (Maybe TTerm)
    toTreeless EvaluationStrategy
    eval QName
    q) ((UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (UsesFloat, [Decl])
    forall a. Monoid a => a
    mempty) ((TTerm
      -> ReaderT
           GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
     -> ReaderT
          GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> (TTerm
        -> ReaderT
             GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a b. (a -> b) -> a -> b
    $ \ TTerm
    treeless -> do

          [ArgUsage]
    used <- [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe [ArgUsage])
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [ArgUsage]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe [ArgUsage])
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe [ArgUsage])
    getCompiledArgUse QName
    q
          let dostrip :: Bool
    dostrip = ArgUsage
    ArgUnused ArgUsage -> [ArgUsage] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ArgUsage]
    used

          -- Compute the type approximation
          Definition
    def <- QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
          ([Type]
    argTypes0, Type
    resType) <- Type -> HsCompileM ([Type], Type)
    hsTelApproximation (Type -> HsCompileM ([Type], Type))
    -> Type -> HsCompileM ([Type], Type)
    forall a b. (a -> b) -> a -> b
    $ Definition -> Type
    defType Definition
    def
          let pars :: Nat
    pars = case Definition -> Defn
    theDef Definition
    def of
                       Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just Projection{ projIndex :: Projection -> Nat
    projIndex = Nat
    i } } | Nat
    i Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    > Nat
    0 -> Nat
    i Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1
                       Defn
    _ -> Nat
    0
              argTypes :: [Type]
    argTypes  = Nat -> [Type] -> [Type]
    forall a. Nat -> [a] -> [a]
    drop Nat
    pars [Type]
    argTypes0
              argTypesS :: [Type]
    argTypesS = [ArgUsage] -> [Type] -> [Type]
    forall a. [ArgUsage] -> [a] -> [a]
    filterUsed [ArgUsage]
    used [Type]
    argTypes

          (Exp
    e, UsesFloat
    useFloat) <- if Bool
    dostrip then TTerm -> HsCompileM (Exp, UsesFloat)
    closedTerm ([ArgUsage] -> TTerm -> TTerm
    stripUnusedArguments [ArgUsage]
    used TTerm
    treeless)
                                      else TTerm -> HsCompileM (Exp, UsesFloat)
    closedTerm TTerm
    treeless
          let ([Pat]
    ps, Exp
    b) = Exp -> ([Pat], Exp)
    lamView Exp
    e
              lamView :: Exp -> ([Pat], Exp)
    lamView Exp
    e =
                case Exp
    e of
                  HS.Lambda [Pat]
    ps Exp
    b -> ([Pat]
    ps, Exp
    b)
                  Exp
    b              -> ([], Exp
    b)

              tydecl :: Name -> t Type -> Type -> Decl
    tydecl  Name
    f t Type
    ts Type
    t = [Name] -> Type -> Decl
    HS.TypeSig [Name
    f] ((Type -> Type -> Type) -> Type -> t Type -> Type
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Type -> Type -> Type
    HS.TyFun Type
    t t Type
    ts)
              funbind :: Name -> [Pat] -> Exp -> Decl
    funbind Name
    f [Pat]
    ps Exp
    b = [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    f [Pat]
    ps (Exp -> Rhs
    HS.UnGuardedRhs Exp
    b) Maybe Binds
    emptyBinds]
              tyfunbind :: Name -> [Type] -> Type -> [Pat] -> Exp -> [Decl]
    tyfunbind Name
    f [Type]
    ts Type
    t [Pat]
    ps Exp
    b =
                let ts' :: [Type]
    ts' = [Type]
    ts [Type] -> [Type] -> [Type]
    forall a. [a] -> [a] -> [a]
    ++ (Nat -> Type -> [Type]
    forall a. Nat -> a -> [a]
    replicate ([Pat] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Pat]
    ps Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - [Type] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Type]
    ts) Type
    mazAnyType)
                in [Name -> [Type] -> Type -> Decl
    forall {t :: * -> *}. Foldable t => Name -> t Type -> Type -> Decl
    tydecl Name
    f [Type]
    ts' Type
    t, Name -> [Pat] -> Exp -> Decl
    funbind Name
    f [Pat]
    ps Exp
    b]

          -- The definition of the non-stripped function
          ([Pat]
    ps0, Exp
    _) <- Exp -> ([Pat], Exp)
    lamView (Exp -> ([Pat], Exp))
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ([Pat], Exp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    closedTerm_ (((TTerm -> TTerm) -> TTerm -> TTerm)
    -> TTerm -> [TTerm -> TTerm] -> TTerm
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    ($) TTerm
    T.TErased ([TTerm -> TTerm] -> TTerm) -> [TTerm -> TTerm] -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Nat -> (TTerm -> TTerm) -> [TTerm -> TTerm]
    forall a. Nat -> a -> [a]
    replicate ([ArgUsage] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [ArgUsage]
    used) TTerm -> TTerm
    T.TLam)
          let b0 :: Exp
    b0 = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Exp -> Exp -> Exp
    HS.App (Name -> Exp
    hsVarUQ (Name -> Exp) -> Name -> Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    duname QName
    q) [ Name -> Exp
    hsVarUQ Name
    x | (~(HS.PVar Name
    x), ArgUsage
    ArgUsed) <- [Pat] -> [ArgUsage] -> [(Pat, ArgUsage)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Pat]
    ps0 [ArgUsage]
    used ]
              ps0' :: [Pat]
    ps0' = (Pat -> ArgUsage -> Pat) -> [Pat] -> [ArgUsage] -> [Pat]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith (\Pat
    p ArgUsage
    u -> case ArgUsage
    u of
                                        ArgUsage
    ArgUsed   -> Pat
    p
                                        ArgUsage
    ArgUnused -> Pat -> Pat
    HS.PIrrPat Pat
    p)
                       [Pat]
    ps0 [ArgUsage]
    used

          (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (UsesFloat
    useFloat,
                  if Bool
    dostrip
                    then Name -> [Type] -> Type -> [Pat] -> Exp -> [Decl]
    tyfunbind (QName -> Name
    dname QName
    q) [Type]
    argTypes Type
    resType [Pat]
    ps0' Exp
    b0 [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++
                         Name -> [Type] -> Type -> [Pat] -> Exp -> [Decl]
    tyfunbind (QName -> Name
    duname QName
    q) [Type]
    argTypesS Type
    resType [Pat]
    ps Exp
    b
                    else Name -> [Type] -> Type -> [Pat] -> Exp -> [Decl]
    tyfunbind (QName -> Name
    dname QName
    q) [Type]
    argTypes Type
    resType [Pat]
    ps Exp
    b)

      fbWithType :: HS.Type -> HS.Exp -> [HS.Decl]
      fbWithType :: Type -> Exp -> [Decl]
    fbWithType Type
    ty Exp
    e =
        [Name] -> Type -> Decl
    HS.TypeSig [QName -> Name
    dname QName
    q] Type
    ty Decl -> [Decl] -> [Decl]
    forall a. a -> [a] -> [a]
    : Exp -> [Decl]
    fb Exp
    e

      fb :: HS.Exp -> [HS.Decl]
      fb :: Exp -> [Decl]
    fb Exp
    e  = [[Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (QName -> Name
    dname QName
    q) []
                                    (Exp -> Rhs
    HS.UnGuardedRhs Exp
    e) Maybe Binds
    emptyBinds]]

      axiomErr :: HS.Exp
      axiomErr :: Exp
    axiomErr = Text -> Exp
    rtmError (Text -> Exp) -> Text -> Exp
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Text
    Text.pack (FilePath -> Text) -> FilePath -> Text
    forall a b. (a -> b) -> a -> b
    $ FilePath
    "postulate evaluated: " FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ QName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow QName
    q

    constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> HsCompileM [HS.Decl]
    constructorCoverageCode :: QName
    -> Nat
    -> [QName]
    -> FilePath
    -> [FilePath]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    constructorCoverageCode QName
    q Nat
    np [QName]
    cs FilePath
    hsTy [FilePath]
    hsCons = do
      TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> [FilePath] -> TCM ()
    checkConstructorCount QName
    q [QName]
    cs [FilePath]
    hsCons
      ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (TCM Bool -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool)
    -> TCM Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM Bool
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> m Bool
    noCheckCover QName
    q) ([Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []) (ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall a b. (a -> b) -> a -> b
    $ do
        [Decl]
    ccs <- [[Decl]] -> [Decl]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    List.concat ([[Decl]] -> [Decl])
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [[Decl]]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (QName
     -> FilePath
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
    -> [QName]
    -> [FilePath]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [[Decl]]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM QName
    -> FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    checkConstructorType [QName]
    cs [FilePath]
    hsCons
        [Decl]
    cov <- TCM [Decl]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM [Decl]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
    -> TCM [Decl]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall a b. (a -> b) -> a -> b
    $ QName -> FilePath -> Nat -> [QName] -> [FilePath] -> TCM [Decl]
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> FilePath -> Nat -> [QName] -> [FilePath] -> m [Decl]
    checkCover QName
    q FilePath
    hsTy Nat
    np [QName]
    cs [FilePath]
    hsCons
        [Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
    -> [Decl]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall a b. (a -> b) -> a -> b
    $ [Decl]
    ccs [Decl] -> [Decl] -> [Decl]
    forall a. [a] -> [a] -> [a]
    ++ [Decl]
    cov

    -- | Environment for naming of local variables.
    --   Invariant: @reverse ccCxt ++ ccNameSupply@
    data CCEnv = CCEnv
      { CCEnv -> [Name]
    _ccNameSupply :: NameSupply  -- ^ Supply of fresh names
      , CCEnv -> [Name]
    _ccContext    :: CCContext   -- ^ Names currently in scope
      }

    type NameSupply = [HS.Name]
    type CCContext  = [HS.Name]

    ccNameSupply :: Lens' NameSupply CCEnv
    ccNameSupply :: Lens' [Name] CCEnv
    ccNameSupply [Name] -> f [Name]
    f CCEnv
    e =  (\ [Name]
    ns' -> CCEnv
    e { _ccNameSupply :: [Name]
    _ccNameSupply = [Name]
    ns' }) ([Name] -> CCEnv) -> f [Name] -> f CCEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Name] -> f [Name]
    f (CCEnv -> [Name]
    _ccNameSupply CCEnv
    e)

    ccContext :: Lens' CCContext CCEnv
    ccContext :: Lens' [Name] CCEnv
    ccContext [Name] -> f [Name]
    f CCEnv
    e = (\ [Name]
    cxt -> CCEnv
    e { _ccContext :: [Name]
    _ccContext = [Name]
    cxt }) ([Name] -> CCEnv) -> f [Name] -> f CCEnv
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Name] -> f [Name]
    f (CCEnv -> [Name]
    _ccContext CCEnv
    e)

    -- | Initial environment for expression generation.
    initCCEnv :: CCEnv
    initCCEnv :: CCEnv
    initCCEnv = CCEnv :: [Name] -> [Name] -> CCEnv
    CCEnv
      { _ccNameSupply :: [Name]
    _ccNameSupply = (Nat -> Name) -> [Nat] -> [Name]
    forall a b. (a -> b) -> [a] -> [b]
    map (VariableKind -> Nat -> Name
    ihname VariableKind
    V) [Nat
    0..]  -- DON'T CHANGE THESE NAMES!
      , _ccContext :: [Name]
    _ccContext    = []
      }

    -- | Term variables are de Bruijn indices.
    lookupIndex :: Int -> CCContext -> HS.Name
    lookupIndex :: Nat -> [Name] -> Name
    lookupIndex Nat
    i [Name]
    xs = Name -> Maybe Name -> Name
    forall a. a -> Maybe a -> a
    fromMaybe Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Name -> Name) -> Maybe Name -> Name
    forall a b. (a -> b) -> a -> b
    $ [Name]
    xs [Name] -> Nat -> Maybe Name
    forall a. [a] -> Nat -> Maybe a
    !!! Nat
    i

    -- | Constructor coverage monad transformer
    type CCT m = ReaderT CCEnv (WriterT UsesFloat (HsCompileT m))

    -- | Constructor coverage monad
    type CC = CCT TCM

    liftCC :: Monad m => HsCompileT m a -> CCT m a
    liftCC :: forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC = WriterT
      UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)) a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)))
         a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT
       UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)) a
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)))
          a)
    -> (ReaderT GHCModuleEnv (StateT HsCompileState m) a
        -> WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)) a)
    -> ReaderT GHCModuleEnv (StateT HsCompileState m) a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)))
         a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ReaderT GHCModuleEnv (StateT HsCompileState m) a
    -> WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState m)) a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift

    freshNames :: Monad m => Int -> ([HS.Name] -> CCT m a) -> CCT m a
    freshNames :: forall (m :: * -> *) a.
    Monad m =>
    Nat -> ([Name] -> CCT m a) -> CCT m a
    freshNames Nat
    n [Name] -> CCT m a
    _ | Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    < Nat
    0 = CCT m a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
    freshNames Nat
    n [Name] -> CCT m a
    cont = do
      ([Name]
    xs, [Name]
    rest) <- Nat -> [Name] -> ([Name], [Name])
    forall a. Nat -> [a] -> ([a], [a])
    splitAt Nat
    n ([Name] -> ([Name], [Name]))
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) [Name]
    -> ReaderT
         CCEnv (WriterT UsesFloat (HsCompileT m)) ([Name], [Name])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' [Name] CCEnv
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) [Name]
    forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
    view Lens' [Name] CCEnv
    ccNameSupply
      (CCEnv -> CCEnv) -> CCT m a -> CCT m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (Lens' [Name] CCEnv -> LensMap [Name] CCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' [Name] CCEnv
    ccNameSupply ([Name] -> [Name] -> [Name]
    forall a b. a -> b -> a
    const [Name]
    rest)) (CCT m a -> CCT m a) -> CCT m a -> CCT m a
    forall a b. (a -> b) -> a -> b
    $ [Name] -> CCT m a
    cont [Name]
    xs

    -- | Introduce n variables into the context.
    intros :: Monad m => Int -> ([HS.Name] -> CCT m a) -> CCT m a
    intros :: forall (m :: * -> *) a.
    Monad m =>
    Nat -> ([Name] -> CCT m a) -> CCT m a
    intros Nat
    n [Name] -> CCT m a
    cont = Nat -> ([Name] -> CCT m a) -> CCT m a
    forall (m :: * -> *) a.
    Monad m =>
    Nat -> ([Name] -> CCT m a) -> CCT m a
    freshNames Nat
    n (([Name] -> CCT m a) -> CCT m a) -> ([Name] -> CCT m a) -> CCT m a
    forall a b. (a -> b) -> a -> b
    $ \[Name]
    xs ->
      (CCEnv -> CCEnv) -> CCT m a -> CCT m a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (Lens' [Name] CCEnv -> LensMap [Name] CCEnv
    forall i o. Lens' i o -> LensMap i o
    over Lens' [Name] CCEnv
    ccContext ([Name] -> [Name]
    forall a. [a] -> [a]
    reverse [Name]
    xs [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++)) (CCT m a -> CCT m a) -> CCT m a -> CCT m a
    forall a b. (a -> b) -> a -> b
    $ [Name] -> CCT m a
    cont [Name]
    xs

    checkConstructorType :: QName -> HaskellCode -> HsCompileM [HS.Decl]
    checkConstructorType :: QName
    -> FilePath
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    checkConstructorType QName
    q FilePath
    hs = do
      Type
    ty <- QName -> HsCompileM Type
    haskellType QName
    q
      [Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Name] -> Type -> Decl
    HS.TypeSig [NameKind -> QName -> Name
    unqhname NameKind
    CheckK QName
    q] Type
    ty
             , [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (NameKind -> QName -> Name
    unqhname NameKind
    CheckK QName
    q) []
                                    (Exp -> Rhs
    HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Exp
    fakeExp FilePath
    hs) Maybe Binds
    emptyBinds]
             ]

    checkCover :: HasConstInfo m => QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> m [HS.Decl]
    checkCover :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> FilePath -> Nat -> [QName] -> [FilePath] -> m [Decl]
    checkCover QName
    q FilePath
    ty Nat
    n [QName]
    cs [FilePath]
    hsCons = do
      let tvs :: [FilePath]
    tvs = [ FilePath
    "a" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ Nat -> FilePath
    forall a. Show a => a -> FilePath
    show Nat
    i | Nat
    i <- [Nat
    1..Nat
    n] ]
          makeClause :: QName -> FilePath -> m Alt
    makeClause QName
    c FilePath
    hsc = do
            Nat
    a <- QName -> m Nat
    forall (m :: * -> *). HasConstInfo m => QName -> m Nat
    erasedArity QName
    c
            let pat :: Pat
    pat = QName -> [Pat] -> Pat
    HS.PApp (Name -> QName
    HS.UnQual (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    hsc) ([Pat] -> Pat) -> [Pat] -> Pat
    forall a b. (a -> b) -> a -> b
    $ Nat -> Pat -> [Pat]
    forall a. Nat -> a -> [a]
    replicate Nat
    a Pat
    HS.PWildCard
            Alt -> m Alt
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Alt -> m Alt) -> Alt -> m Alt
    forall a b. (a -> b) -> a -> b
    $ Pat -> Rhs -> Maybe Binds -> Alt
    HS.Alt Pat
    pat (Exp -> Rhs
    HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
    forall a b. (a -> b) -> a -> b
    $ Exp
    HS.unit_con) Maybe Binds
    emptyBinds

      [Alt]
    cs <- (QName -> FilePath -> m Alt) -> [QName] -> [FilePath] -> m [Alt]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM QName -> FilePath -> m Alt
    forall {m :: * -> *}. HasConstInfo m => QName -> FilePath -> m Alt
    makeClause [QName]
    cs [FilePath]
    hsCons
      let rhs :: Exp
    rhs = Exp -> [Alt] -> Exp
    HS.Case (QName -> Exp
    HS.Var (QName -> Exp) -> QName -> Exp
    forall a b. (a -> b) -> a -> b
    $ Name -> QName
    HS.UnQual (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    "x") [Alt]
    cs

      [Decl] -> m [Decl]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [ [Name] -> Type -> Decl
    HS.TypeSig [NameKind -> QName -> Name
    unqhname NameKind
    CoverK QName
    q] (Type -> Decl) -> Type -> Decl
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Type
    fakeType (FilePath -> Type) -> FilePath -> Type
    forall a b. (a -> b) -> a -> b
    $ [FilePath] -> FilePath
    unwords (FilePath
    ty FilePath -> [FilePath] -> [FilePath]
    forall a. a -> [a] -> [a]
    : [FilePath]
    tvs) FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    " -> ()"
             , [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match (NameKind -> QName -> Name
    unqhname NameKind
    CoverK QName
    q) [Name -> Pat
    HS.PVar (Name -> Pat) -> Name -> Pat
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    "x"]
                                    (Exp -> Rhs
    HS.UnGuardedRhs Exp
    rhs) Maybe Binds
    emptyBinds]
             ]

    closedTerm_ :: T.TTerm -> HsCompileM HS.Exp
    closedTerm_ :: TTerm -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    closedTerm_ TTerm
    t = (Exp, UsesFloat) -> Exp
    forall a b. (a, b) -> a
    fst ((Exp, UsesFloat) -> Exp)
    -> HsCompileM (Exp, UsesFloat)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> HsCompileM (Exp, UsesFloat)
    closedTerm TTerm
    t

    closedTerm :: T.TTerm -> HsCompileM (HS.Exp, UsesFloat)
    closedTerm :: TTerm -> HsCompileM (Exp, UsesFloat)
    closedTerm TTerm
    v = do
      TTerm
    v <- TCM TTerm -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) TTerm
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM TTerm
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) TTerm)
    -> TCM TTerm
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TCM TTerm
    forall (m :: * -> *). HasConstInfo m => TTerm -> m TTerm
    addCoercions TTerm
    v
      WriterT
      UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)) Exp
    -> HsCompileM (Exp, UsesFloat)
    forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
    runWriterT (TTerm -> CC Exp
    term TTerm
    v CC Exp
    -> CCEnv
    -> WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)) Exp
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` CCEnv
    initCCEnv)

    -- Translate case on bool to if
    mkIf :: T.TTerm -> CC T.TTerm
    mkIf :: TTerm -> CC TTerm
    mkIf t :: TTerm
    t@(TCase Nat
    e CaseInfo
    _ TTerm
    d [TACon QName
    c1 Nat
    0 TTerm
    b1, TACon QName
    c2 Nat
    0 TTerm
    b2]) | TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    T.isUnreachable TTerm
    d = do
      GHCEnv
    env <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
    -> CCT TCM GHCEnv
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
    askGHCEnv
      let isTrue :: QName -> Bool
    isTrue  QName
    c = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    ghcEnvTrue  GHCEnv
    env
          isFalse :: QName -> Bool
    isFalse QName
    c = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    ghcEnvFalse GHCEnv
    env
      if | QName -> Bool
    isTrue QName
    c1, QName -> Bool
    isFalse QName
    c2 -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> CC TTerm) -> TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm -> TTerm
    T.tIfThenElse (TTerm -> TTerm
    TCoerce (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Nat -> TTerm
    TVar Nat
    e) TTerm
    b1 TTerm
    b2
         | QName -> Bool
    isTrue QName
    c2, QName -> Bool
    isFalse QName
    c1 -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> CC TTerm) -> TTerm -> CC TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm -> TTerm
    T.tIfThenElse (TTerm -> TTerm
    TCoerce (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Nat -> TTerm
    TVar Nat
    e) TTerm
    b2 TTerm
    b1
         | Bool
    otherwise             -> TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
    mkIf TTerm
    t = TTerm -> CC TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t

    -- | Extract Agda term to Haskell expression.
    --   Erased arguments are extracted as @()@.
    --   Types are extracted as @()@.
    term :: T.TTerm -> CC HS.Exp
    term :: TTerm -> CC Exp
    term TTerm
    tm0 = TTerm -> CC TTerm
    mkIf TTerm
    tm0 CC TTerm -> (TTerm -> CC Exp) -> CC Exp
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ TTerm
    tm0 -> do
      let ((Bool
    hasCoerce, TTerm
    t), [TTerm]
    ts) = TTerm -> ((Bool, TTerm), [TTerm])
    coerceAppView TTerm
    tm0
      -- let (t0, ts)       = tAppView tm0
      -- let (hasCoerce, t) = coerceView t0
      let coe :: Exp -> Exp
    coe            = Bool -> (Exp -> Exp) -> Exp -> Exp
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen Bool
    hasCoerce Exp -> Exp
    hsCoerce
      case (TTerm
    t, [TTerm]
    ts) of
        (T.TPrim TPrim
    T.PIf, [TTerm
    c, TTerm
    x, TTerm
    y]) -> Exp -> Exp
    coe (Exp -> Exp) -> CC Exp -> CC Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do Exp -> Exp -> Exp -> Exp
    HS.If (Exp -> Exp -> Exp -> Exp)
    -> CC Exp
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         (Exp -> Exp -> Exp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> CC Exp
    term TTerm
    c ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      (Exp -> Exp -> Exp)
    -> CC Exp
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         (Exp -> Exp)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> CC Exp
    term TTerm
    x ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      (Exp -> Exp)
    -> CC Exp -> CC Exp
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> CC Exp
    term TTerm
    y

        (T.TDef QName
    f, [TTerm]
    ts) -> do
          [ArgUsage]
    used <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) [ArgUsage]
    -> CCT TCM [ArgUsage]
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (ReaderT GHCModuleEnv (StateT HsCompileState TCM) [ArgUsage]
     -> CCT TCM [ArgUsage])
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [ArgUsage]
    -> CCT TCM [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe [ArgUsage])
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [ArgUsage]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe [ArgUsage])
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe [ArgUsage])
    getCompiledArgUse QName
    f
          -- #2248: no unused argument pruning for COMPILE'd functions
          Bool
    isCompiled <- TCM Bool
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Bool
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Bool
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          Bool)
    -> TCM Bool
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Bool
    forall a b. (a -> b) -> a -> b
    $ Maybe HaskellPragma -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe HaskellPragma -> Bool)
    -> TCM (Maybe HaskellPragma) -> TCM Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Maybe HaskellPragma)
    getHaskellPragma QName
    f
          let given :: Nat
    given   = [TTerm] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [TTerm]
    ts
              needed :: Nat
    needed  = [ArgUsage] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [ArgUsage]
    used
              missing :: [ArgUsage]
    missing = Nat -> [ArgUsage] -> [ArgUsage]
    forall a. Nat -> [a] -> [a]
    drop Nat
    given [ArgUsage]
    used
          if Bool -> Bool
    not Bool
    isCompiled Bool -> Bool -> Bool
    && ArgUsage
    ArgUnused ArgUsage -> [ArgUsage] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ArgUsage]
    used
            then if ArgUsage
    ArgUnused ArgUsage -> [ArgUsage] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ArgUsage]
    missing then TTerm -> CC Exp
    term (Nat -> TTerm -> TTerm
    etaExpand (Nat
    needed Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    given) TTerm
    tm0) else do
              Exp
    f <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Exp
    HS.Var (QName -> Exp)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameKind
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    xhqn (FunctionKind -> NameKind
    FunK FunctionKind
    NoUnused) QName
    f
                                       -- use stripped function
              -- Andreas, 2019-11-07, issue #4169.
              -- Insert coercion unconditionally as erasure of arguments
              -- that are matched upon might remove the unfolding of codomain types.
              -- (Hard to explain, see test/Compiler/simple/Issue4169.)
              Exp -> Exp
    hsCoerce Exp
    f Exp -> [TTerm] -> CC Exp
    `apps` [ArgUsage] -> [TTerm] -> [TTerm]
    forall a. [ArgUsage] -> [a] -> [a]
    filterUsed [ArgUsage]
    used [TTerm]
    ts
            else do
              Exp
    f <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Exp
    HS.Var (QName -> Exp)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameKind
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    xhqn (FunctionKind -> NameKind
    FunK FunctionKind
    PossiblyUnused) QName
    f
                                       -- use original (non-stripped) function
              Exp -> Exp
    coe Exp
    f Exp -> [TTerm] -> CC Exp
    `apps` [TTerm]
    ts

        (T.TCon QName
    c, [TTerm]
    ts) -> do
          [Bool]
    erased  <- HsCompileT TCM [Bool] -> CCT TCM [Bool]
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (HsCompileT TCM [Bool] -> CCT TCM [Bool])
    -> HsCompileT TCM [Bool] -> CCT TCM [Bool]
    forall a b. (a -> b) -> a -> b
    $ QName -> HsCompileT TCM [Bool]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
    getErasedConArgs QName
    c
          let missing :: [Bool]
    missing = Nat -> [Bool] -> [Bool]
    forall a. Nat -> [a] -> [a]
    drop ([TTerm] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [TTerm]
    ts) [Bool]
    erased
              notErased :: Bool -> Bool
    notErased = Bool -> Bool
    not
          if (Bool -> Bool) -> [Bool] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Bool -> Bool
    notErased [Bool]
    missing
            then do
                    Exp
    f <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Exp
    HS.Con (QName -> Exp)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    conhqn QName
    c
                    Exp -> Exp
    hsCoerce Exp
    f Exp -> [TTerm] -> CC Exp
    `apps` [ TTerm
    t | (TTerm
    t, Bool
    False) <- [TTerm] -> [Bool] -> [(TTerm, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [TTerm]
    ts [Bool]
    erased ]
            else do
                    let n :: Nat
    n = [Bool] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Bool]
    missing
                    Bool
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         ()
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Nat
    n Nat -> Nat -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Nat
    1) ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__  -- We will add at least on TLam, not getting a busy loop here.
                    TTerm -> CC Exp
    term (TTerm -> CC Exp) -> TTerm -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Nat -> TTerm -> TTerm
    etaExpand ([Bool] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Bool]
    missing) TTerm
    tm0

        -- Other kind of application: fall back to apps.
        (TTerm
    t, [TTerm]
    ts) -> TTerm -> CC Exp
    noApplication TTerm
    t CC Exp -> (Exp -> CC Exp) -> CC Exp
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \ Exp
    t' -> Exp -> Exp
    coe Exp
    t' Exp -> [TTerm] -> CC Exp
    `apps` [TTerm]
    ts
      where
      apps :: Exp -> [TTerm] -> CC Exp
    apps = (Exp -> TTerm -> CC Exp) -> Exp -> [TTerm] -> CC Exp
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (\ Exp
    h TTerm
    a -> Exp -> Exp -> Exp
    HS.App Exp
    h (Exp -> Exp) -> CC Exp -> CC Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> CC Exp
    term TTerm
    a)
      etaExpand :: Nat -> TTerm -> TTerm
    etaExpand Nat
    n TTerm
    t = Nat -> TTerm -> TTerm
    mkTLam Nat
    n (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Nat -> TTerm -> TTerm
    forall a. Subst a => Nat -> a -> a
    raise Nat
    n TTerm
    t TTerm -> [TTerm] -> TTerm
    `T.mkTApp` (Nat -> TTerm) -> [Nat] -> [TTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map Nat -> TTerm
    T.TVar (Nat -> [Nat]
    forall a. Integral a => a -> [a]
    downFrom Nat
    n)

    -- | Translate a non-application, non-coercion, non-constructor, non-definition term.
    noApplication :: T.TTerm -> CC HS.Exp
    noApplication :: TTerm -> CC Exp
    noApplication = \case
      T.TApp{}    -> CC Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      T.TCoerce{} -> CC Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      T.TCon{}    -> CC Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      T.TDef{}    -> CC Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__

      T.TVar Nat
    i    -> Name -> Exp
    hsVarUQ (Name -> Exp) -> ([Name] -> Name) -> [Name] -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Nat -> [Name] -> Name
    lookupIndex Nat
    i ([Name] -> Exp)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         [Name]
    -> CC Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Lens' [Name] CCEnv
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         [Name]
    forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
    view Lens' [Name] CCEnv
    ccContext
      T.TLam TTerm
    t    -> Nat -> ([Name] -> CC Exp) -> CC Exp
    forall (m :: * -> *) a.
    Monad m =>
    Nat -> ([Name] -> CCT m a) -> CCT m a
    intros Nat
    1 (([Name] -> CC Exp) -> CC Exp) -> ([Name] -> CC Exp) -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ \ [Name
    x] -> [Pat] -> Exp -> Exp
    hsLambda [Name -> Pat
    HS.PVar Name
    x] (Exp -> Exp) -> CC Exp -> CC Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> CC Exp
    term TTerm
    t

      T.TLet TTerm
    t1 TTerm
    t2 -> do
        Exp
    t1' <- TTerm -> CC Exp
    term TTerm
    t1
        Nat -> ([Name] -> CC Exp) -> CC Exp
    forall (m :: * -> *) a.
    Monad m =>
    Nat -> ([Name] -> CCT m a) -> CCT m a
    intros Nat
    1 (([Name] -> CC Exp) -> CC Exp) -> ([Name] -> CC Exp) -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ \[Name
    x] -> do
          Name -> Exp -> Exp -> Exp
    hsLet Name
    x Exp
    t1' (Exp -> Exp) -> CC Exp -> CC Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> CC Exp
    term TTerm
    t2

      T.TCase Nat
    sc CaseInfo
    ct TTerm
    def [TAlt]
    alts -> do
        Exp
    sc'   <- TTerm -> CC Exp
    term (TTerm -> CC Exp) -> TTerm -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Nat -> TTerm
    T.TVar Nat
    sc
        [Alt]
    alts' <- (TAlt
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          Alt)
    -> [TAlt]
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         [Alt]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (Nat
    -> TAlt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    alt Nat
    sc) [TAlt]
    alts
        Exp
    def'  <- TTerm -> CC Exp
    term TTerm
    def
        let defAlt :: Alt
    defAlt = Pat -> Rhs -> Maybe Binds -> Alt
    HS.Alt Pat
    HS.PWildCard (Exp -> Rhs
    HS.UnGuardedRhs Exp
    def') Maybe Binds
    emptyBinds
        Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CC Exp) -> Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Alt] -> Exp
    HS.Case (Exp -> Exp
    hsCoerce Exp
    sc') ([Alt]
    alts' [Alt] -> [Alt] -> [Alt]
    forall a. [a] -> [a] -> [a]
    ++ [Alt
    defAlt])

      T.TLit Literal
    l    -> Literal -> CC Exp
    forall (m :: * -> *). Monad m => Literal -> CCT m Exp
    literal Literal
    l
      T.TPrim TPrim
    p   -> Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CC Exp) -> Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ TPrim -> Exp
    compilePrim TPrim
    p
      TTerm
    T.TUnit     -> Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CC Exp) -> Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Exp
    HS.unit_con
      TTerm
    T.TSort     -> Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CC Exp) -> Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Exp
    HS.unit_con
      TTerm
    T.TErased   -> Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CC Exp) -> Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Name -> Exp
    hsVarUQ (Name -> Exp) -> Name -> Exp
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    mazErasedName
      T.TError TError
    e  -> Exp -> CC Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CC Exp) -> Exp -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ case TError
    e of
        TError
    T.TUnreachable -> Exp
    rtmUnreachableError
        T.TMeta FilePath
    s      -> FilePath -> Exp
    rtmHole FilePath
    s

    hsCoerce :: HS.Exp -> HS.Exp
    hsCoerce :: Exp -> Exp
    hsCoerce Exp
    t = Exp -> Exp -> Exp
    HS.App Exp
    mazCoerce Exp
    t

    compilePrim :: T.TPrim -> HS.Exp
    compilePrim :: TPrim -> Exp
    compilePrim TPrim
    s = QName -> Exp
    HS.Var (QName -> Exp) -> QName -> Exp
    forall a b. (a -> b) -> a -> b
    $ FilePath -> QName
    hsName (FilePath -> QName) -> FilePath -> QName
    forall a b. (a -> b) -> a -> b
    $ TPrim -> FilePath
    treelessPrimName TPrim
    s

    alt :: Int -> T.TAlt -> CC HS.Alt
    alt :: Nat
    -> TAlt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    alt Nat
    sc TAlt
    a = do
      case TAlt
    a of
        T.TACon {aCon :: TAlt -> QName
    T.aCon = QName
    c} -> do
          Nat
    -> ([Name]
        -> ReaderT
             CCEnv
             (WriterT
                UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
             Alt)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall (m :: * -> *) a.
    Monad m =>
    Nat -> ([Name] -> CCT m a) -> CCT m a
    intros (TAlt -> Nat
    T.aArity TAlt
    a) (([Name]
      -> ReaderT
           CCEnv
           (WriterT
              UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
           Alt)
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          Alt)
    -> ([Name]
        -> ReaderT
             CCEnv
             (WriterT
                UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
             Alt)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall a b. (a -> b) -> a -> b
    $ \ [Name]
    xs -> do
            [Bool]
    erased <- HsCompileT TCM [Bool] -> CCT TCM [Bool]
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (HsCompileT TCM [Bool] -> CCT TCM [Bool])
    -> HsCompileT TCM [Bool] -> CCT TCM [Bool]
    forall a b. (a -> b) -> a -> b
    $ QName -> HsCompileT TCM [Bool]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
    getErasedConArgs QName
    c
            GHCEnv
    env    <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
    -> CCT TCM GHCEnv
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
    askGHCEnv
            QName
    hConNm <-
              if | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    ghcEnvNil GHCEnv
    env ->
                   QName
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          QName)
    -> QName
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         QName
    forall a b. (a -> b) -> a -> b
    $ Name -> QName
    HS.UnQual (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    "[]"
                 | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    c Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    ghcEnvCons GHCEnv
    env ->
                   QName
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QName
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          QName)
    -> QName
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         QName
    forall a b. (a -> b) -> a -> b
    $ Name -> QName
    HS.UnQual (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Symbol FilePath
    ":"
                 | Bool
    otherwise -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         QName
    forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
    liftCC (ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          QName)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         QName
    forall a b. (a -> b) -> a -> b
    $ QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
    conhqn QName
    c
            Pat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkAlt (QName -> [Pat] -> Pat
    HS.PApp QName
    hConNm ([Pat] -> Pat) -> [Pat] -> Pat
    forall a b. (a -> b) -> a -> b
    $ [Name -> Pat
    HS.PVar Name
    x | (Name
    x, Bool
    False) <- [Name] -> [Bool] -> [(Name, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    xs [Bool]
    erased])
        T.TAGuard TTerm
    g TTerm
    b -> do
          Exp
    g <- TTerm -> CC Exp
    term TTerm
    g
          Exp
    b <- TTerm -> CC Exp
    term TTerm
    b
          Alt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Alt
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          Alt)
    -> Alt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall a b. (a -> b) -> a -> b
    $ Pat -> Rhs -> Maybe Binds -> Alt
    HS.Alt Pat
    HS.PWildCard
                          ([GuardedRhs] -> Rhs
    HS.GuardedRhss [[Stmt] -> Exp -> GuardedRhs
    HS.GuardedRhs [Exp -> Stmt
    HS.Qualifier Exp
    g] Exp
    b])
                          Maybe Binds
    emptyBinds
        T.TALit { aLit :: TAlt -> Literal
    T.aLit = LitQName QName
    q } -> Pat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkAlt (QName -> Pat
    litqnamepat QName
    q)
        T.TALit { aLit :: TAlt -> Literal
    T.aLit = l :: Literal
    l@LitFloat{}, aBody :: TAlt -> TTerm
    T.aBody = TTerm
    b } -> do
          UsesFloat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell UsesFloat
    YesFloat
          Exp
    l <- Literal -> CC Exp
    forall (m :: * -> *). Monad m => Literal -> CCT m Exp
    literal Literal
    l
          FilePath
    -> Exp
    -> TTerm
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkGuarded (TPrim -> FilePath
    treelessPrimName TPrim
    T.PEqF) Exp
    l TTerm
    b
        T.TALit { aLit :: TAlt -> Literal
    T.aLit = LitString Text
    s , aBody :: TAlt -> TTerm
    T.aBody = TTerm
    b } -> FilePath
    -> Exp
    -> TTerm
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkGuarded FilePath
    "(==)" (Text -> Exp
    litString Text
    s) TTerm
    b
        T.TALit {} -> Pat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkAlt (Literal -> Pat
    HS.PLit (Literal -> Pat) -> Literal -> Pat
    forall a b. (a -> b) -> a -> b
    $ Literal -> Literal
    hslit (Literal -> Literal) -> Literal -> Literal
    forall a b. (a -> b) -> a -> b
    $ TAlt -> Literal
    T.aLit TAlt
    a)
      where
        mkGuarded :: FilePath
    -> Exp
    -> TTerm
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkGuarded FilePath
    eq Exp
    lit TTerm
    b = do
          Exp
    b  <- TTerm -> CC Exp
    term TTerm
    b
          let varName :: Name
    varName = FilePath -> Name
    HS.Ident FilePath
    "l" -- only used locally in the guard
              pv :: Pat
    pv = Name -> Pat
    HS.PVar Name
    varName
              v :: Exp
    v  = Name -> Exp
    hsVarUQ Name
    varName
              guard :: Exp
    guard =
                QName -> Exp
    HS.Var (Name -> QName
    HS.UnQual (FilePath -> Name
    HS.Ident FilePath
    eq)) Exp -> Exp -> Exp
    `HS.App`
                  Exp
    v Exp -> Exp -> Exp
    `HS.App` Exp
    lit
          Alt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Alt
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          Alt)
    -> Alt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall a b. (a -> b) -> a -> b
    $ Pat -> Rhs -> Maybe Binds -> Alt
    HS.Alt Pat
    pv
                          ([GuardedRhs] -> Rhs
    HS.GuardedRhss [[Stmt] -> Exp -> GuardedRhs
    HS.GuardedRhs [Exp -> Stmt
    HS.Qualifier Exp
    guard] Exp
    b])
                          Maybe Binds
    emptyBinds

        mkAlt :: HS.Pat -> CC HS.Alt
        mkAlt :: Pat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkAlt Pat
    pat = do
            Exp
    body' <- TTerm -> CC Exp
    term (TTerm -> CC Exp) -> TTerm -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ TAlt -> TTerm
    T.aBody TAlt
    a
            Alt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Alt
     -> ReaderT
          CCEnv
          (WriterT
             UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
          Alt)
    -> Alt
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    forall a b. (a -> b) -> a -> b
    $ Pat -> Rhs -> Maybe Binds -> Alt
    HS.Alt Pat
    pat (Exp -> Rhs
    HS.UnGuardedRhs Exp
    body') Maybe Binds
    emptyBinds

    literal :: forall m. Monad m => Literal -> CCT m HS.Exp
    literal :: forall (m :: * -> *). Monad m => Literal -> CCT m Exp
    literal Literal
    l = case Literal
    l of
      LitNat    Integer
    _   -> Exp -> CCT m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Exp
    typed FilePath
    "Integer"
      LitWord64 Word64
    _   -> Exp -> CCT m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Exp
    typed FilePath
    "MAlonzo.RTE.Word64"
      LitFloat  Double
    x   -> Double -> FilePath -> CCT m Exp
    floatExp Double
    x FilePath
    "Double"
      LitQName  QName
    x   -> Exp -> CCT m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Exp
    litqname QName
    x
      LitString Text
    s   -> Exp -> CCT m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ Text -> Exp
    litString Text
    s
      Literal
    _             -> Exp -> CCT m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ Exp
    l'
      where
        l' :: Exp
    l'    = Literal -> Exp
    HS.Lit (Literal -> Exp) -> Literal -> Exp
    forall a b. (a -> b) -> a -> b
    $ Literal -> Literal
    hslit Literal
    l
        typed :: FilePath -> Exp
    typed = Exp -> Type -> Exp
    HS.ExpTypeSig Exp
    l' (Type -> Exp) -> (FilePath -> Type) -> FilePath -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Type
    HS.TyCon (QName -> Type) -> (FilePath -> QName) -> FilePath -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FilePath -> QName
    rtmQual

        -- ASR (2016-09-14): See Issue #2169.
        -- Ulf, 2016-09-28: and #2218.
        floatExp :: Double -> String -> CCT m HS.Exp
        floatExp :: Double -> FilePath -> CCT m Exp
    floatExp Double
    x FilePath
    s
          | Double -> Bool
    isPosInf  Double
    x = FilePath -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => FilePath -> m Exp
    rte FilePath
    "positiveInfinity"
          | Double -> Bool
    isNegInf  Double
    x = FilePath -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => FilePath -> m Exp
    rte FilePath
    "negativeInfinity"
          | Double -> Bool
    isNegZero Double
    x = FilePath -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => FilePath -> m Exp
    rte FilePath
    "negativeZero"
          | Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN     Double
    x = FilePath -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => FilePath -> m Exp
    rte FilePath
    "nan"
          | Bool
    otherwise   = Exp -> CCT m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Exp
    typed FilePath
    s
          where
            rte :: FilePath -> m Exp
    rte FilePath
    s = do UsesFloat -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell UsesFloat
    YesFloat; Exp -> m Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> m Exp) -> Exp -> m Exp
    forall a b. (a -> b) -> a -> b
    $ QName -> Exp
    HS.Var (QName -> Exp) -> QName -> Exp
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Name -> QName
    HS.Qual ModuleName
    mazRTEFloat (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    s

    hslit :: Literal -> HS.Literal
    hslit :: Literal -> Literal
    hslit = \case
      LitNat    Integer
    x -> Integer -> Literal
    HS.Int    Integer
    x
      LitWord64 Word64
    x -> Integer -> Literal
    HS.Int    (Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    x)
      LitFloat  Double
    x -> Rational -> Literal
    HS.Frac   (Double -> Rational
    forall a. Real a => a -> Rational
    toRational Double
    x)
      LitChar   Char
    x -> Char -> Literal
    HS.Char   Char
    x
      LitQName  QName
    x -> Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      LitString Text
    _ -> Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      LitMeta{}   -> Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    litString :: Text -> HS.Exp
    litString :: Text -> Exp
    litString Text
    s = Exp -> Type -> Exp
    HS.Ann (Literal -> Exp
    HS.Lit (Text -> Literal
    HS.String Text
    s))
                         (QName -> Type
    HS.TyCon (ModuleName -> Name -> QName
    HS.Qual (FilePath -> ModuleName
    HS.ModuleName FilePath
    "Data.Text") (FilePath -> Name
    HS.Ident FilePath
    "Text")))

    litqname :: QName -> HS.Exp
    litqname :: QName -> Exp
    litqname QName
    x =
      FilePath -> Exp
    rteCon FilePath
    "QName" Exp -> [Exp] -> Exp
    `apps`
      [ Word64 -> Exp
    forall a. Integral a => a -> Exp
    hsTypedInt Word64
    n
      , Word64 -> Exp
    forall a. Integral a => a -> Exp
    hsTypedInt Word64
    m
      , Literal -> Exp
    HS.Lit (Literal -> Exp) -> Literal -> Exp
    forall a b. (a -> b) -> a -> b
    $ Text -> Literal
    HS.String (Text -> Literal) -> Text -> Literal
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Text
    Text.pack (FilePath -> Text) -> FilePath -> Text
    forall a b. (a -> b) -> a -> b
    $ QName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow QName
    x
      , FilePath -> Exp
    rteCon FilePath
    "Fixity" Exp -> [Exp] -> Exp
    `apps`
        [ Associativity -> Exp
    litAssoc (Fixity -> Associativity
    fixityAssoc Fixity
    fx)
        , FixityLevel -> Exp
    litPrec  (Fixity -> FixityLevel
    fixityLevel Fixity
    fx)
        ]
      ]
      where
        apps :: Exp -> [Exp] -> Exp
    apps = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Exp -> Exp -> Exp
    HS.App
        rteCon :: FilePath -> Exp
    rteCon FilePath
    name = QName -> Exp
    HS.Con (QName -> Exp) -> QName -> Exp
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Name -> QName
    HS.Qual ModuleName
    mazRTE (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    name
        NameId Word64
    n (ModuleNameHash Word64
    m) = Name -> NameId
    nameId (Name -> NameId) -> Name -> NameId
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x
        fx :: Fixity
    fx = Fixity' -> Fixity
    theFixity (Fixity' -> Fixity) -> Fixity' -> Fixity
    forall a b. (a -> b) -> a -> b
    $ Name -> Fixity'
    nameFixity (Name -> Fixity') -> Name -> Fixity'
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x

        litAssoc :: Associativity -> Exp
    litAssoc Associativity
    NonAssoc   = FilePath -> Exp
    rteCon FilePath
    "NonAssoc"
        litAssoc Associativity
    LeftAssoc  = FilePath -> Exp
    rteCon FilePath
    "LeftAssoc"
        litAssoc Associativity
    RightAssoc = FilePath -> Exp
    rteCon FilePath
    "RightAssoc"

        litPrec :: FixityLevel -> Exp
    litPrec FixityLevel
    Unrelated   = FilePath -> Exp
    rteCon FilePath
    "Unrelated"
        litPrec (Related Double
    l) = FilePath -> Exp
    rteCon FilePath
    "Related" Exp -> Exp -> Exp
    `HS.App` Double -> Exp
    forall a. Real a => a -> Exp
    hsTypedDouble Double
    l

    litqnamepat :: QName -> HS.Pat
    litqnamepat :: QName -> Pat
    litqnamepat QName
    x =
      QName -> [Pat] -> Pat
    HS.PApp (ModuleName -> Name -> QName
    HS.Qual ModuleName
    mazRTE (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ FilePath -> Name
    HS.Ident FilePath
    "QName")
              [ Literal -> Pat
    HS.PLit (Integer -> Literal
    HS.Int (Integer -> Literal) -> Integer -> Literal
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n)
              , Literal -> Pat
    HS.PLit (Integer -> Literal
    HS.Int (Integer -> Literal) -> Integer -> Literal
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    m)
              , Pat
    HS.PWildCard, Pat
    HS.PWildCard ]
      where
        NameId Word64
    n (ModuleNameHash Word64
    m) = Name -> NameId
    nameId (Name -> NameId) -> Name -> NameId
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    x

    condecl :: QName -> Induction -> HsCompileM HS.ConDecl
    condecl :: QName
    -> Induction
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    condecl QName
    q Induction
    _ind = do
      GHCOptions
    opts <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      Definition
    def <- QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let Constructor{ conPars :: Defn -> Nat
    conPars = Nat
    np, conErased :: Defn -> Maybe [Bool]
    conErased = Maybe [Bool]
    erased } = Definition -> Defn
    theDef Definition
    def
      ([Type]
    argTypes0, Type
    _) <- Type -> HsCompileM ([Type], Type)
    hsTelApproximation (Definition -> Type
    defType Definition
    def)
      let strict :: Strictness
    strict     = if Defn -> Induction
    conInd (Definition -> Defn
    theDef Definition
    def) Induction -> Induction -> Bool
    forall a. Eq a => a -> a -> Bool
    == Induction
    Inductive Bool -> Bool -> Bool
    &&
                          GHCOptions -> Bool
    optGhcStrictData GHCOptions
    opts
                       then Strictness
    HS.Strict
                       else Strictness
    HS.Lazy
          argTypes :: [(Maybe Strictness, Type)]
    argTypes   = [ (Strictness -> Maybe Strictness
    forall a. a -> Maybe a
    Just Strictness
    strict, Type
    t)
                       | (Type
    t, Bool
    False) <- [Type] -> [Bool] -> [(Type, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Nat -> [Type] -> [Type]
    forall a. Nat -> [a] -> [a]
    drop Nat
    np [Type]
    argTypes0)
                                           ([Bool] -> Maybe [Bool] -> [Bool]
    forall a. a -> Maybe a -> a
    fromMaybe [] Maybe [Bool]
    erased [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    False)
                       ]
      ConDecl -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    forall (m :: * -> *) a. Monad m => a -> m a
    return (ConDecl
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl)
    -> ConDecl
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    forall a b. (a -> b) -> a -> b
    $ Name -> [(Maybe Strictness, Type)] -> ConDecl
    HS.ConDecl (NameKind -> QName -> Name
    unqhname NameKind
    ConK QName
    q) [(Maybe Strictness, Type)]
    argTypes

    compiledcondecl
      :: Maybe Nat  -- ^ The constructor's arity (after erasure).
      -> QName -> HsCompileM HS.Decl
    compiledcondecl :: Maybe Nat
    -> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    compiledcondecl Maybe Nat
    mar QName
    q = do
      Nat
    ar <- case Maybe Nat
    mar of
        Maybe Nat
    Nothing -> TCM Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat)
    -> TCM Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM Nat
    forall (m :: * -> *). HasConstInfo m => QName -> m Nat
    erasedArity QName
    q
        Just Nat
    ar -> Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    ar
      FilePath
    hsCon <- FilePath -> Maybe FilePath -> FilePath
    forall a. a -> Maybe a -> a
    fromMaybe FilePath
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe FilePath -> FilePath)
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe FilePath)
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe FilePath)
    getHaskellConstructor QName
    q
      let patVars :: [Pat]
    patVars = (Nat -> Pat) -> [Nat] -> [Pat]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name -> Pat
    HS.PVar (Name -> Pat) -> (Nat -> Name) -> Nat -> Pat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VariableKind -> Nat -> Name
    ihname VariableKind
    A) [Nat
    0 .. Nat
    ar Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]
      Decl -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Decl -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl)
    -> Decl -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Decl
    forall a b. (a -> b) -> a -> b
    $ Pat -> Pat -> Decl
    HS.PatSyn (QName -> [Pat] -> Pat
    HS.PApp (Name -> QName
    HS.UnQual (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ NameKind -> QName -> Name
    unqhname NameKind
    ConK QName
    q) [Pat]
    patVars)
                 (QName -> [Pat] -> Pat
    HS.PApp (FilePath -> QName
    hsName FilePath
    hsCon) [Pat]
    patVars)

    compiledTypeSynonym :: QName -> String -> Nat -> HS.Decl
    compiledTypeSynonym :: QName -> FilePath -> Nat -> Decl
    compiledTypeSynonym QName
    q FilePath
    hsT Nat
    arity =
      Name -> [TyVarBind] -> Type -> Decl
    HS.TypeDecl (NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q) ((Name -> TyVarBind) -> [Name] -> [TyVarBind]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> TyVarBind
    HS.UnkindedVar [Name]
    vs)
                  ((Type -> Type -> Type) -> Type -> [Type] -> Type
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Type -> Type -> Type
    HS.TyApp (FilePath -> Type
    HS.FakeType FilePath
    hsT) ([Type] -> Type) -> [Type] -> Type
    forall a b. (a -> b) -> a -> b
    $ (Name -> Type) -> [Name] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Type
    HS.TyVar [Name]
    vs)
      where
        vs :: [Name]
    vs = [ VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    i | Nat
    i <- [Nat
    0 .. Nat
    arity Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]]

    tvaldecl :: QName
             -> Induction
                -- ^ Is the type inductive or coinductive?
             -> Nat -> [HS.ConDecl] -> Maybe Clause -> [HS.Decl]
    tvaldecl :: QName -> Induction -> Nat -> [ConDecl] -> Maybe Clause -> [Decl]
    tvaldecl QName
    q Induction
    ind Nat
    npar [ConDecl]
    cds Maybe Clause
    cl =
      [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match Name
    vn [Pat]
    pvs (Exp -> Rhs
    HS.UnGuardedRhs Exp
    HS.unit_con) Maybe Binds
    emptyBinds] Decl -> [Decl] -> [Decl]
    forall a. a -> [a] -> [a]
    :
      [Decl] -> (Clause -> [Decl]) -> Maybe Clause -> [Decl]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [DataOrNew -> Name -> [TyVarBind] -> [ConDecl] -> [Deriving] -> Decl
    HS.DataDecl DataOrNew
    kind Name
    tn [] [ConDecl]
    cds' []]
            ([Decl] -> Clause -> [Decl]
    forall a b. a -> b -> a
    const []) Maybe Clause
    cl
      where
      (Name
    tn, Name
    vn) = (NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q, QName -> Name
    dname QName
    q)
      pvs :: [Pat]
    pvs = [ Name -> Pat
    HS.PVar (Name -> Pat) -> Name -> Pat
    forall a b. (a -> b) -> a -> b
    $ VariableKind -> Nat -> Name
    ihname VariableKind
    A Nat
    i | Nat
    i <- [Nat
    0 .. Nat
    npar Nat -> Nat -> Nat
    forall a. Num a => a -> a -> a
    - Nat
    1]]

      -- Inductive data types consisting of a single constructor with a
      -- single argument are translated into newtypes.
      (DataOrNew
    kind, [ConDecl]
    cds') = case (Induction
    ind, [ConDecl]
    cds) of
        (Induction
    Inductive, [HS.ConDecl Name
    c [(Maybe Strictness
    _, Type
    t)]]) ->
          (DataOrNew
    HS.NewType, [Name -> [(Maybe Strictness, Type)] -> ConDecl
    HS.ConDecl Name
    c [(Maybe Strictness
    forall a. Maybe a
    Nothing, Type
    t)]])
          -- The strictness annotations are removed for newtype
          -- constructors.
        (Induction, [ConDecl])
    _ -> (DataOrNew
    HS.DataType, [ConDecl]
    cds)

    infodecl :: QName -> [HS.Decl] -> [HS.Decl]
    infodecl :: QName -> [Decl] -> [Decl]
    infodecl QName
    _ [] = []
    infodecl QName
    q [Decl]
    ds = FilePath -> Decl
    HS.Comment (QName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow QName
    q) Decl -> [Decl] -> [Decl]
    forall a. a -> [a] -> [a]
    : [Decl]
    ds

    --------------------------------------------------
    -- Writing out a haskell module
    --------------------------------------------------

    type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)

    copyRTEModules :: MonadGHCIO m => m ()
    copyRTEModules :: forall (m :: * -> *). MonadGHCIO m => m ()
    copyRTEModules = do
      FilePath
    dataDir <- IO FilePath -> m FilePath
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO FilePath
    getDataDir
      let srcDir :: FilePath
    srcDir = FilePath
    dataDir FilePath -> FilePath -> FilePath
    </> FilePath
    "MAlonzo" FilePath -> FilePath -> FilePath
    </> FilePath
    "src"
      FilePath
    dstDir <- GHCOptions -> FilePath
    optGhcCompileDir (GHCOptions -> FilePath) -> m GHCOptions -> m FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> IO ()
    copyDirContent FilePath
    srcDir FilePath
    dstDir

    writeModule :: MonadGHCIO m => HS.Module -> m ()
    writeModule :: forall (m :: * -> *). MonadGHCIO m => Module -> m ()
    writeModule (HS.Module ModuleName
    m [ModulePragma]
    ps [ImportDecl]
    imp [Decl]
    ds) = do
      -- Note that GHC assumes that sources use ASCII or UTF-8.
      FilePath
    out <- (FilePath, FilePath) -> FilePath
    forall a b. (a, b) -> b
    snd ((FilePath, FilePath) -> FilePath)
    -> m (FilePath, FilePath) -> m FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m (FilePath, FilePath)
    forall (m :: * -> *).
    MonadGHCIO m =>
    ModuleName -> m (FilePath, FilePath)
    outFileAndDir ModuleName
    m
      Bool
    strict <- GHCOptions -> Bool
    optGhcStrict (GHCOptions -> Bool) -> m GHCOptions -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      let languagePragmas :: [ModulePragma]
    languagePragmas =
            (FilePath -> ModulePragma) -> [FilePath] -> [ModulePragma]
    forall a b. (a -> b) -> [a] -> [b]
    List.map ([Name] -> ModulePragma
    HS.LanguagePragma ([Name] -> ModulePragma)
    -> (FilePath -> [Name]) -> FilePath -> ModulePragma
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Name]
    forall el coll. Singleton el coll => el -> coll
    singleton (Name -> [Name]) -> (FilePath -> Name) -> FilePath -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FilePath -> Name
    HS.Ident) ([FilePath] -> [ModulePragma]) -> [FilePath] -> [ModulePragma]
    forall a b. (a -> b) -> a -> b
    $
              [FilePath] -> [FilePath]
    forall a. Ord a => [a] -> [a]
    List.sort ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
    forall a b. (a -> b) -> a -> b
    $
                [ FilePath
    "QualifiedDo" | Bool
    strict ] [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++
                    -- If --ghc-strict is used, then the language extension
                    -- QualifiedDo is activated. At the time of writing no
                    -- code is generated that depends on this extension
                    -- (except for the pragmas), but --ghc-strict is broken
                    -- with at least some versions of GHC prior to version 9,
                    -- and QualifiedDo was introduced with GHC 9.
                [ FilePath
    "BangPatterns"
                , FilePath
    "EmptyDataDecls"
                , FilePath
    "EmptyCase"
                , FilePath
    "ExistentialQuantification"
                , FilePath
    "ScopedTypeVariables"
                , FilePath
    "NoMonomorphismRestriction"
                , FilePath
    "RankNTypes"
                , FilePath
    "PatternSynonyms"
                , FilePath
    "OverloadedStrings"
                ]
      let ghcOptions :: [ModulePragma]
    ghcOptions =
            (FilePath -> ModulePragma) -> [FilePath] -> [ModulePragma]
    forall a b. (a -> b) -> [a] -> [b]
    List.map FilePath -> ModulePragma
    HS.OtherPragma
              [ FilePath
    ""  -- to separate from LANGUAGE pragmas
              , FilePath
    "{-# OPTIONS_GHC -Wno-overlapping-patterns #-}"
                  -- Andreas, 2022-01-26, issue #5758:
                  -- Place this in generated file rather than
                  -- passing it only when calling GHC from within Agda.
                  -- This will silence the warning for the Agda-generated .hs
                  -- files while it can be on for other .hs files in the same
                  -- project.  (E.g., when using cabal/stack to compile.)
              ]
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> IO ()
    UTF8.writeFile FilePath
    out (FilePath -> IO ()) -> FilePath -> IO ()
    forall a b. (a -> b) -> a -> b
    $ (FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    "\n") (FilePath -> FilePath) -> FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $ Module -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyPrint (Module -> FilePath) -> Module -> FilePath
    forall a b. (a -> b) -> a -> b
    $
        -- TODO: It might make sense to skip bang patterns for the unused
        -- arguments of the "non-stripped" functions.
        Bool -> (Module -> Module) -> Module -> Module
    forall a. Bool -> (a -> a) -> a -> a
    applyWhen Bool
    strict Module -> Module
    forall a. MakeStrict a => a -> a
    makeStrict (Module -> Module) -> Module -> Module
    forall a b. (a -> b) -> a -> b
    $
        ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
    HS.Module ModuleName
    m ([[ModulePragma]] -> [ModulePragma]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[ModulePragma]
    languagePragmas, [ModulePragma]
    ghcOptions, [ModulePragma]
    ps]) [ImportDecl]
    imp [Decl]
    ds

    outFileAndDir :: MonadGHCIO m => HS.ModuleName -> m (FilePath, FilePath)
    outFileAndDir :: forall (m :: * -> *).
    MonadGHCIO m =>
    ModuleName -> m (FilePath, FilePath)
    outFileAndDir ModuleName
    m = do
      FilePath
    mdir <- GHCOptions -> FilePath
    optGhcCompileDir (GHCOptions -> FilePath) -> m GHCOptions -> m FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      let (FilePath
    fdir, FilePath
    fn) = FilePath -> (FilePath, FilePath)
    splitFileName (FilePath -> (FilePath, FilePath))
    -> FilePath -> (FilePath, FilePath)
    forall a b. (a -> b) -> a -> b
    $ Char -> FilePath -> FilePath
    repldot Char
    pathSeparator (FilePath -> FilePath) -> FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $
                       ModuleName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyPrint ModuleName
    m
      let dir :: FilePath
    dir = FilePath
    mdir FilePath -> FilePath -> FilePath
    </> FilePath
    fdir
          fp :: FilePath
    fp  = FilePath
    dir FilePath -> FilePath -> FilePath
    </> FilePath -> FilePath -> FilePath
    replaceExtension FilePath
    fn FilePath
    "hs"
      IO () -> m ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> m ()) -> IO () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> FilePath -> IO ()
    createDirectoryIfMissing Bool
    True FilePath
    dir
      (FilePath, FilePath) -> m (FilePath, FilePath)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePath
    mdir, FilePath
    fp)
      where
      repldot :: Char -> FilePath -> FilePath
    repldot Char
    c = (Char -> Char) -> FilePath -> FilePath
    forall a b. (a -> b) -> [a] -> [b]
    List.map ((Char -> Char) -> FilePath -> FilePath)
    -> (Char -> Char) -> FilePath -> FilePath
    forall a b. (a -> b) -> a -> b
    $ \ Char
    c' -> if Char
    c' Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '.' then Char
    c else Char
    c'

    curOutFileAndDir :: (MonadGHCIO m, ReadGHCModuleEnv m) => m (FilePath, FilePath)
    curOutFileAndDir :: forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m (FilePath, FilePath)
    curOutFileAndDir = ModuleName -> m (FilePath, FilePath)
    forall (m :: * -> *).
    MonadGHCIO m =>
    ModuleName -> m (FilePath, FilePath)
    outFileAndDir (ModuleName -> m (FilePath, FilePath))
    -> m ModuleName -> m (FilePath, FilePath)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< m ModuleName
    forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curHsMod

    curOutFile :: (MonadGHCIO m, ReadGHCModuleEnv m) => m FilePath
    curOutFile :: forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m FilePath
    curOutFile = (FilePath, FilePath) -> FilePath
    forall a b. (a, b) -> b
    snd ((FilePath, FilePath) -> FilePath)
    -> m (FilePath, FilePath) -> m FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m (FilePath, FilePath)
    forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m (FilePath, FilePath)
    curOutFileAndDir

    callGHC :: ReaderT GHCModule TCM ()
    callGHC :: ReaderT GHCModule TCM ()
    callGHC = do
      GHCOptions
    opts    <- ReaderT GHCModule TCM GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      FilePath
    hsmod   <- ModuleName -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyPrint (ModuleName -> FilePath)
    -> ReaderT GHCModule TCM ModuleName
    -> ReaderT GHCModule TCM FilePath
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModule TCM ModuleName
    forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curHsMod
      ModuleName
    agdaMod <- ReaderT GHCModule TCM ModuleName
    forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
    curAgdaMod
      let outputName :: Name
    outputName = Name -> [Name] -> Name
    forall a. a -> [a] -> a
    lastWithDefault Name
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([Name] -> Name) -> [Name] -> Name
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> [Name]
    mnameToList ModuleName
    agdaMod
      (FilePath
    mdir, FilePath
    fp) <- ReaderT GHCModule TCM (FilePath, FilePath)
    forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m (FilePath, FilePath)
    curOutFileAndDir
      let ghcopts :: [FilePath]
    ghcopts = GHCOptions -> [FilePath]
    optGhcFlags GHCOptions
    opts

      Bool
    modIsMain <- ReaderT GHCModule TCM Bool
    forall (m :: * -> *). ReadGHCModuleEnv m => m Bool
    curIsMainModule
      Bool
    modHasMainFunc <- (GHCModule -> Bool) -> ReaderT GHCModule TCM Bool
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (Bool -> Bool
    not (Bool -> Bool) -> (GHCModule -> Bool) -> GHCModule -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [MainFunctionDef] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null ([MainFunctionDef] -> Bool)
    -> (GHCModule -> [MainFunctionDef]) -> GHCModule -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . GHCModule -> [MainFunctionDef]
    ghcModMainFuncs)
      let isMain :: Bool
    isMain = Bool
    modIsMain Bool -> Bool -> Bool
    && Bool
    modHasMainFunc  -- both need to be IsMain

      -- Warn if no main function and not --no-main
      Bool -> ReaderT GHCModule TCM () -> ReaderT GHCModule TCM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool
    modIsMain Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Bool
    isMain) (ReaderT GHCModule TCM () -> ReaderT GHCModule TCM ())
    -> ReaderT GHCModule TCM () -> ReaderT GHCModule TCM ()
    forall a b. (a -> b) -> a -> b
    $
        Doc -> ReaderT GHCModule TCM ()
    forall (m :: * -> *). MonadWarning m => Doc -> m ()
    genericWarning (Doc -> ReaderT GHCModule TCM ())
    -> ReaderT GHCModule TCM Doc -> ReaderT GHCModule TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< [ReaderT GHCModule TCM Doc] -> ReaderT GHCModule TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    fsep (FilePath -> [ReaderT GHCModule TCM Doc]
    forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
    pwords FilePath
    "No main function defined in" [ReaderT GHCModule TCM Doc]
    -> [ReaderT GHCModule TCM Doc] -> [ReaderT GHCModule TCM Doc]
    forall a. [a] -> [a] -> [a]
    ++ [ModuleName -> ReaderT GHCModule TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    prettyTCM ModuleName
    agdaMod ReaderT GHCModule TCM Doc
    -> ReaderT GHCModule TCM Doc -> ReaderT GHCModule TCM Doc
    forall a. Semigroup a => a -> a -> a
    <> ReaderT GHCModule TCM Doc
    "."] [ReaderT GHCModule TCM Doc]
    -> [ReaderT GHCModule TCM Doc] -> [ReaderT GHCModule TCM Doc]
    forall a. [a] -> [a] -> [a]
    ++
                                 FilePath -> [ReaderT GHCModule TCM Doc]
    forall (m :: * -> *). Applicative m => FilePath -> [m Doc]
    pwords FilePath
    "Use --no-main to suppress this warning.")

      let overridableArgs :: [FilePath]
    overridableArgs =
            [ FilePath
    "-O"] [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++
            (if Bool
    isMain then [FilePath
    "-o", FilePath
    mdir FilePath -> FilePath -> FilePath
    </> Name -> FilePath
    forall a. Pretty a => a -> FilePath
    prettyShow (Name -> Name
    nameConcrete Name
    outputName)] else []) [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++
            [ FilePath
    "-Werror"]
          otherArgs :: [FilePath]
    otherArgs       =
            [ FilePath
    "-i" FilePath -> FilePath -> FilePath
    forall a. [a] -> [a] -> [a]
    ++ FilePath
    mdir] [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++
            (if Bool
    isMain then [FilePath
    "-main-is", FilePath
    hsmod] else []) [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++
            [ FilePath
    fp
            , FilePath
    "--make"
            , FilePath
    "-fwarn-incomplete-patterns"
            ]
          args :: [FilePath]
    args     = [FilePath]
    overridableArgs [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ [FilePath]
    ghcopts [FilePath] -> [FilePath] -> [FilePath]
    forall a. [a] -> [a] -> [a]
    ++ [FilePath]
    otherArgs

      let ghcBin :: FilePath
    ghcBin = GHCOptions -> FilePath
    optGhcBin GHCOptions
    opts

      -- Make GHC use UTF-8 when writing to stdout and stderr.
      IO () -> ReaderT GHCModule TCM ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> ReaderT GHCModule TCM ())
    -> IO () -> ReaderT GHCModule TCM ()
    forall a b. (a -> b) -> a -> b
    $ FilePath -> FilePath -> IO ()
    setEnv FilePath
    "GHC_CHARENC" FilePath
    "UTF-8"
      -- Note: Some versions of GHC use stderr for progress reports. For
      -- those versions of GHC we don't print any progress information
      -- unless an error is encountered.
      let doCall :: Bool
    doCall = GHCOptions -> Bool
    optGhcCallGhc GHCOptions
    opts
      TCM () -> ReaderT GHCModule TCM ()
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM () -> ReaderT GHCModule TCM ())
    -> TCM () -> ReaderT GHCModule TCM ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> FilePath -> [FilePath] -> Maybe TextEncoding -> TCM ()
    callCompiler Bool
    doCall FilePath
    ghcBin [FilePath]
    args (TextEncoding -> Maybe TextEncoding
    forall a. a -> Maybe a
    Just TextEncoding
    utf8)