    module Agda.Compiler.MAlonzo.Compiler
      ( ghcBackend
      , ghcInvocationStrings
      )
      where

    import Control.Arrow (second)
    import Control.DeepSeq
    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.Options

    import Agda.Syntax.Common
    import Agda.Syntax.Common.Pretty (prettyShow, render)
    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.Syntax.TopLevelModuleName

    import Agda.TypeChecking.Datatypes
    import Agda.TypeChecking.Primitive (getBuiltinName)
    import Agda.TypeChecking.Pretty
    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 qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe
    import Agda.Utils.Monad
    import Agda.Utils.Singleton
    import qualified Agda.Utils.IO.UTF8 as UTF8

    import Agda.Setup ( getDataDir )

    import Agda.Utils.Impossible

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

    ghcBackend :: Backend
    ghcBackend :: Backend
    ghcBackend = Backend'_boot
      Definition TCM GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    -> Backend
    forall opts definition (tcm :: * -> *) env menv mod def.
    NFData opts =>
    Backend'_boot definition tcm opts env menv mod def
    -> Backend_boot definition tcm
    Backend Backend'_boot
      Definition TCM GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    ghcBackend'

    ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    ghcBackend' :: Backend'_boot
      Definition TCM GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
    ghcBackend' = Backend'
      { backendName :: BackendName
    backendName           = BackendName
    "GHC"
      , backendVersion :: Maybe BackendName
    backendVersion        = Maybe BackendName
    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 -> TCMT IO GHCEnv
    preCompile            = GHCFlags -> TCMT IO GHCEnv
    ghcPreCompile
      , postCompile :: GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCMT IO ()
    postCompile           = GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCMT IO ()
    ghcPostCompile
      , preModule :: GHCEnv
    -> IsMain
    -> TopLevelModuleName
    -> Maybe [Char]
    -> TCMT IO (Recompile GHCModuleEnv GHCModule)
    preModule             = GHCEnv
    -> IsMain
    -> TopLevelModuleName
    -> Maybe [Char]
    -> TCMT IO (Recompile GHCModuleEnv GHCModule)
    ghcPreModule
      , postModule :: GHCEnv
    -> GHCModuleEnv
    -> IsMain
    -> TopLevelModuleName
    -> [GHCDefinition]
    -> TCMT IO GHCModule
    postModule            = GHCEnv
    -> GHCModuleEnv
    -> IsMain
    -> TopLevelModuleName
    -> [GHCDefinition]
    -> TCMT IO GHCModule
    ghcPostModule
      , compileDef :: GHCEnv
    -> GHCModuleEnv -> IsMain -> Definition -> TCMT IO GHCDefinition
    compileDef            = GHCEnv
    -> GHCModuleEnv -> IsMain -> Definition -> TCMT IO GHCDefinition
    ghcCompileDef
      , scopeCheckingSuffices :: Bool
    scopeCheckingSuffices = Bool
    False
      , mayEraseType :: QName -> TCMT IO Bool
    mayEraseType          = QName -> TCMT IO Bool
    ghcMayEraseType
      , backendInteractTop :: Maybe (BackendCommandTop TCM)
    backendInteractTop    = Maybe (BackendCommandTop TCM)
    forall a. Maybe a
    Nothing
      , backendInteractHole :: Maybe (BackendCommandHole TCM)
    backendInteractHole   = Maybe (BackendCommandHole TCM)
    forall a. Maybe a
    Nothing
      }

    --- Command-line flags ---

    data GHCFlags = GHCFlags
      { GHCFlags -> Bool
    flagGhcCompile :: Bool
      , GHCFlags -> Bool
    flagGhcCallGhc :: Bool
      , GHCFlags -> Maybe [Char]
    flagGhcBin     :: Maybe FilePath
        -- ^ Use the compiler at PATH instead of "ghc"
      , GHCFlags -> [[Char]]
    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
    $cfrom :: forall x. GHCFlags -> Rep GHCFlags x
    from :: forall x. GHCFlags -> Rep GHCFlags x
    $cto :: forall x. Rep GHCFlags x -> GHCFlags
    to :: forall x. Rep GHCFlags x -> GHCFlags
    Generic

    instance NFData GHCFlags

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

    -- | The option to activate the GHC backend.
    --
    ghcInvocationFlag :: OptDescr (Flag GHCFlags)
    ghcInvocationFlag :: OptDescr (Flag GHCFlags)
    ghcInvocationFlag =
          [Char]
    -> [[Char]]
    -> ArgDescr (Flag GHCFlags)
    -> [Char]
    -> OptDescr (Flag GHCFlags)
    forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a
    Option [Char
    'c']  [[Char]
    "compile", [Char]
    "ghc"] (Flag GHCFlags -> ArgDescr (Flag GHCFlags)
    forall a. a -> ArgDescr a
    NoArg Flag GHCFlags
    forall {f :: * -> *}. Applicative f => GHCFlags -> f GHCFlags
    enable)
                        [Char]
    "compile program using the GHC backend"
      where
        enable :: GHCFlags -> f GHCFlags
    enable      GHCFlags
    o = GHCFlags -> f GHCFlags
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure GHCFlags
    o{ flagGhcCompile    = True }

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

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

    -- | Option strings to activate the GHC backend.
    --
    ghcInvocationStrings :: [String]
    ghcInvocationStrings :: [[Char]]
    ghcInvocationStrings = OptDescr (Flag GHCFlags) -> [[Char]]
    forall a. OptDescr a -> [[Char]]
    optionStrings OptDescr (Flag GHCFlags)
    ghcInvocationFlag

    -- | Get all flags that activate the given option.
    --
    optionStrings :: OptDescr a -> [String]
    optionStrings :: forall a. OptDescr a -> [[Char]]
    optionStrings (Option [Char]
    short [[Char]]
    long ArgDescr a
    _ [Char]
    _) = (Char -> [Char]) -> [Char] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Char
    c -> Char
    '-' Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : Char
    c Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    : []) [Char]
    short [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++ [[Char]]
    long

    --- 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 TopLevelModuleName
    ghcDefImports    :: Set TopLevelModuleName
      }

    --- Top-level compilation ---

    ghcPreCompile :: GHCFlags -> TCM GHCEnv
    ghcPreCompile :: GHCFlags -> TCMT IO GHCEnv
    ghcPreCompile GHCFlags
    flags = do
      TCMT IO (Maybe Cubical) -> (Cubical -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a.
    Monad m =>
    m (Maybe a) -> (a -> m ()) -> m ()
    whenJustM TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption \case
        Cubical
    CErased -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        Cubical
    CFull   -> TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Cubical -> TypeError
    CubicalCompilationNotSupported Cubical
    CFull

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

      mbool       <- getBuiltinName builtinBool
      mtrue       <- getBuiltinName builtinTrue
      mfalse      <- getBuiltinName builtinFalse
      mlist       <- getBuiltinName builtinList
      mnil        <- getBuiltinName builtinNil
      mcons       <- getBuiltinName builtinCons
      mmaybe      <- getBuiltinName builtinMaybe
      mnothing    <- getBuiltinName builtinNothing
      mjust       <- getBuiltinName builtinJust
      mnat        <- getBuiltinName builtinNat
      minteger    <- getBuiltinName builtinInteger
      mword64     <- getBuiltinName builtinWord64
      minf        <- getBuiltinName builtinInf
      msharp      <- getBuiltinName builtinSharp
      mflat       <- getBuiltinName builtinFlat
      minterval   <- getBuiltinName builtinInterval
      mizero      <- getBuiltinName builtinIZero
      mione       <- getBuiltinName builtinIOne
      misone      <- getBuiltinName builtinIsOne
      mitisone    <- getBuiltinName builtinItIsOne
      misone1     <- getBuiltinName builtinIsOne1
      misone2     <- getBuiltinName builtinIsOne2
      misoneempty <- getBuiltinName builtinIsOneEmpty
      mpathp      <- getBuiltinName builtinPathP
      msub        <- getBuiltinName builtinSub
      msubin      <- getBuiltinName builtinSubIn

      istcbuiltin <- do
        builtins <- mapM getBuiltinName
          [ builtinAgdaTCMReturn
          , builtinAgdaTCMBind
          , builtinAgdaTCMUnify
          , builtinAgdaTCMTypeError
          , builtinAgdaTCMInferType
          , builtinAgdaTCMCheckType
          , builtinAgdaTCMNormalise
          , builtinAgdaTCMReduce
          , builtinAgdaTCMCatchError
          , builtinAgdaTCMQuoteTerm
          , builtinAgdaTCMUnquoteTerm
          , builtinAgdaTCMQuoteOmegaTerm
          , builtinAgdaTCMGetContext
          , builtinAgdaTCMExtendContext
          , builtinAgdaTCMInContext
          , builtinAgdaTCMFreshName
          , builtinAgdaTCMDeclareDef
          , builtinAgdaTCMDeclarePostulate
          , builtinAgdaTCMDeclareData
          , builtinAgdaTCMDefineData
          , builtinAgdaTCMDefineFun
          , builtinAgdaTCMGetType
          , builtinAgdaTCMGetDefinition
          , builtinAgdaTCMBlock
          , builtinAgdaTCMCommit
          , builtinAgdaTCMIsMacro
          , builtinAgdaTCMWithNormalisation
          , builtinAgdaTCMWithReconstructed
          , builtinAgdaTCMWithExpandLast
          , builtinAgdaTCMWithReduceDefs
          , builtinAgdaTCMAskNormalisation
          , builtinAgdaTCMAskReconstructed
          , builtinAgdaTCMAskExpandLast
          , builtinAgdaTCMAskReduceDefs
          , builtinAgdaTCMFormatErrorParts
          , builtinAgdaTCMDebugPrint
          , builtinAgdaTCMNoConstraints
          , builtinAgdaTCMWorkOnTypes
          , builtinAgdaTCMRunSpeculative
          , builtinAgdaTCMExec
          , builtinAgdaTCMCheckFromString
          , builtinAgdaTCMGetInstances
          , builtinAgdaTCMSolveInstances
          , builtinAgdaTCMPragmaForeign
          , builtinAgdaTCMPragmaCompile
          , builtinAgdaBlocker
          , builtinAgdaBlockerAll
          , builtinAgdaBlockerAny
          , builtinAgdaBlockerMeta
          ]
        return $
          flip HashSet.member $
          HashSet.fromList $
          catMaybes builtins

      let defArity QName
    q = Type -> Nat
    arity (Type -> Nat) -> (Definition -> Type) -> Definition -> Nat
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Type
    defType (Definition -> Nat) -> f Definition -> f Nat
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> f Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      listArity <- traverse defArity mlist
      maybeArity <- traverse defArity mmaybe

      return $ GHCEnv
        { ghcEnvOpts        = ghcOpts
        , ghcEnvBool        = mbool
        , ghcEnvTrue        = mtrue
        , ghcEnvFalse       = mfalse
        , ghcEnvMaybe       = mmaybe
        , ghcEnvNothing     = mnothing
        , ghcEnvJust        = mjust
        , ghcEnvList        = mlist
        , ghcEnvNil         = mnil
        , ghcEnvCons        = mcons
        , ghcEnvNat         = mnat
        , ghcEnvInteger     = minteger
        , ghcEnvWord64      = mword64
        , ghcEnvInf         = minf
        , ghcEnvSharp       = msharp
        , ghcEnvFlat        = mflat
        , ghcEnvInterval    = minterval
        , ghcEnvIZero       = mizero
        , ghcEnvIOne        = mione
        , ghcEnvIsOne       = misone
        , ghcEnvItIsOne     = mitisone
        , ghcEnvIsOne1      = misone1
        , ghcEnvIsOne2      = misone2
        , ghcEnvIsOneEmpty  = misoneempty
        , ghcEnvPathP       = mpathp
        , ghcEnvSub         = msub
        , ghcEnvSubIn       = msubin
        , ghcEnvIsTCBuiltin = istcbuiltin
        , ghcEnvListArity   = listArity
        , ghcEnvMaybeArity  = maybeArity
        }

    ghcPostCompile ::
      GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCM ()
    ghcPostCompile :: GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCMT IO ()
    ghcPostCompile GHCEnv
    _cenv IsMain
    _isMain Map TopLevelModuleName 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).
      rootModuleName <- TCMT IO TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
      -- Mario, 2024-10-16: cannot trigger this error:
      -- genericError $ "Module " <> prettyShow rootModuleName <> " was not compiled!"
      let rootModule = GHCModule
    -> TopLevelModuleName
    -> Map TopLevelModuleName GHCModule
    -> GHCModule
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault GHCModule
    forall a. HasCallStack => a
    __IMPOSSIBLE__ TopLevelModuleName
    rootModuleName Map TopLevelModuleName GHCModule
    mods
      flip runReaderT rootModule $ do
        copyRTEModules
        callGHC

    --- Module compilation ---

    ghcPreModule
      :: GHCEnv
      -> IsMain      -- ^ Are we looking at the main module?
      -> TopLevelModuleName
      -> Maybe FilePath    -- ^ Path to the @.agdai@ file.
      -> TCM (Recompile GHCModuleEnv GHCModule)
                     -- ^ Could we confirm the existence of a main function?
    ghcPreModule :: GHCEnv
    -> IsMain
    -> TopLevelModuleName
    -> Maybe [Char]
    -> TCMT IO (Recompile GHCModuleEnv GHCModule)
    ghcPreModule GHCEnv
    cenv IsMain
    isMain TopLevelModuleName
    m Maybe [Char]
    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
          cubical <- ReaderT GHCModuleEnv TCM (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
          case 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 -> TCMT IO (Recompile GHCModuleEnv GHCModule)
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    `runReaderT` GHCEnv -> HsModuleEnv -> GHCModuleEnv
    GHCModuleEnv GHCEnv
    cenv (TopLevelModuleName -> Bool -> HsModuleEnv
    HsModuleEnv TopLevelModuleName
    m (IsMain
    isMain IsMain -> IsMain -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsMain
    IsMain))
      where
        uptodate :: ReaderT GHCModuleEnv TCM Bool
    uptodate = case Maybe [Char]
    mifile of
          Maybe [Char]
    Nothing -> Bool -> ReaderT GHCModuleEnv TCM Bool
    forall a. a -> ReaderT GHCModuleEnv TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
          Just [Char]
    ifile -> IO Bool -> ReaderT GHCModuleEnv TCM Bool
    forall a. IO a -> ReaderT GHCModuleEnv TCM a
    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
    =<< [Char] -> [Char] -> IO Bool
    isNewerThan ([Char] -> [Char] -> IO Bool)
    -> ReaderT GHCModuleEnv TCM [Char]
    -> ReaderT GHCModuleEnv TCM ([Char] -> IO Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv TCM [Char]
    forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m [Char]
    curOutFile ReaderT GHCModuleEnv TCM ([Char] -> IO Bool)
    -> ReaderT GHCModuleEnv TCM [Char]
    -> ReaderT GHCModuleEnv TCM (IO Bool)
    forall a b.
    ReaderT GHCModuleEnv TCM (a -> b)
    -> ReaderT GHCModuleEnv TCM a -> ReaderT GHCModuleEnv TCM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Char] -> ReaderT GHCModuleEnv TCM [Char]
    forall a. a -> ReaderT GHCModuleEnv TCM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Char]
    ifile
        ifileDesc :: [Char]
    ifileDesc = [Char] -> Maybe [Char] -> [Char]
    forall a. a -> Maybe a -> a
    fromMaybe [Char]
    "(memory)" Maybe [Char]
    mifile

        noComp :: ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
    noComp = do
          [Char] -> Nat -> [Char] -> ReaderT GHCModuleEnv TCM ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> [Char] -> m ()
    reportSLn [Char]
    "compile.ghc" Nat
    2 ([Char] -> ReaderT GHCModuleEnv TCM ())
    -> (TopLevelModuleName -> [Char])
    -> TopLevelModuleName
    -> ReaderT GHCModuleEnv TCM ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .
            ([Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " : no compilation is needed.") ([Char] -> [Char])
    -> (TopLevelModuleName -> [Char]) -> TopLevelModuleName -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (TopLevelModuleName -> ReaderT GHCModuleEnv TCM ())
    -> ReaderT GHCModuleEnv TCM TopLevelModuleName
    -> ReaderT GHCModuleEnv TCM ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ReaderT GHCModuleEnv TCM TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
          menv <- ReaderT GHCModuleEnv TCM GHCModuleEnv
    forall r (m :: * -> *). MonadReader r m => m r
    ask
          mainDefs <- ifM curIsMainModule
                             (mainFunctionDefs <$> curIF)
                             (pure [])
          return . Skip $ GHCModule menv mainDefs

        yesComp :: ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
    yesComp = do
          m   <- TopLevelModuleName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (TopLevelModuleName -> [Char])
    -> ReaderT GHCModuleEnv TCM TopLevelModuleName
    -> ReaderT GHCModuleEnv TCM [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReaderT GHCModuleEnv TCM TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
          out <- curOutFile
          alwaysReportSLn "compile.ghc" 1 $ repl [m, ifileDesc, out] "Compiling <<0>> in <<1>> to <<2>>"
          asks Recompile

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

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

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

      i <- curIF

      -- Get content of FOREIGN pragmas.
      let (headerPragmas, hsImps, code) = foreignHaskell i

      flip runReaderT menv $ do
        hsModuleName <- curHsMod
        writeModule $ HS.Module
          hsModuleName
          (map HS.OtherPragma $ List.nub headerPragmas)
          imps
          (map fakeDecl (List.nub hsImps ++ code) ++ decls)

      return $ GHCModule menv mainDefs

    ghcCompileDef :: GHCEnv -> GHCModuleEnv -> IsMain -> Definition -> TCM GHCDefinition
    ghcCompileDef :: GHCEnv
    -> GHCModuleEnv -> IsMain -> Definition -> TCMT IO GHCDefinition
    ghcCompileDef GHCEnv
    _cenv GHCModuleEnv
    menv IsMain
    _isMain Definition
    def = do
      ((usesFloat, decls, mainFuncDef), (HsCompileState imps)) <-
        Definition
    -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    definition Definition
    def HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    -> GHCModuleEnv
    -> TCMT
         IO
         ((UsesFloat, [Decl], Maybe CheckedMainFunctionDef), HsCompileState)
    forall (m :: * -> *) a.
    HsCompileT m a -> GHCModuleEnv -> m (a, HsCompileState)
    `runHsCompileT` GHCModuleEnv
    menv
      return $ GHCDefinition usesFloat decls def (checkedMainDef <$> mainFuncDef) 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 -> TCMT IO Bool
    ghcMayEraseType QName
    q = QName -> TCM (Maybe HaskellPragma)
    getHaskellPragma QName
    q TCM (Maybe HaskellPragma)
    -> (Maybe HaskellPragma -> Bool) -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f 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 -> Set TopLevelModuleName -> [Definition] ->
      [HS.ImportDecl]
    imports :: BuiltinThings
    -> Set TopLevelModuleName -> [Definition] -> [ImportDecl]
    imports BuiltinThings
    builtinThings Set TopLevelModuleName
    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
    $ [Char] -> Name
    HS.Ident [Char]
    x
                          | [Char]
    x <- [[Char]
    mazCoerceName, [Char]
    mazErasedName, [Char]
    mazAnyTypeName] [[Char]] -> [[Char]] -> [[Char]]
    forall a. [a] -> [a] -> [a]
    ++
                                 (TPrim -> [Char]) -> [TPrim] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map TPrim -> [Char]
    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 -> [Definition] -> [ModuleName]
    importsForPrim BuiltinThings
    builtinThings [Definition]
    defs [ModuleName] -> [ModuleName] -> [ModuleName]
    forall a. [a] -> [a] -> [a]
    ++ (TopLevelModuleName -> ModuleName)
    -> [TopLevelModuleName] -> [ModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    map TopLevelModuleName -> ModuleName
    mazMod [TopLevelModuleName]
    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 :: [TopLevelModuleName]
      mnames :: [TopLevelModuleName]
    mnames = Set TopLevelModuleName -> [TopLevelModuleName]
    forall a. Set a -> [a]
    Set.elems Set TopLevelModuleName
    usedModules

      uniq :: [HS.ModuleName] -> [HS.ModuleName]
      uniq :: [ModuleName] -> [ModuleName]
    uniq = (NonEmpty ModuleName -> ModuleName)
    -> [NonEmpty ModuleName] -> [ModuleName]
    forall a b. (a -> b) -> [a] -> [b]
    List.map NonEmpty ModuleName -> ModuleName
    forall a. NonEmpty a -> a
    List1.head ([NonEmpty ModuleName] -> [ModuleName])
    -> ([ModuleName] -> [NonEmpty ModuleName])
    -> [ModuleName]
    -> [ModuleName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ModuleName] -> [NonEmpty ModuleName]
    forall (f :: * -> *) a. (Foldable f, Eq a) => f a -> [NonEmpty a]
    List1.group ([ModuleName] -> [NonEmpty ModuleName])
    -> ([ModuleName] -> [ModuleName])
    -> [ModuleName]
    -> [NonEmpty 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
    $c== :: UsesFloat -> UsesFloat -> Bool
    == :: UsesFloat -> UsesFloat -> Bool
    $c/= :: UsesFloat -> UsesFloat -> Bool
    /= :: UsesFloat -> UsesFloat -> Bool
    Eq, Nat -> UsesFloat -> [Char] -> [Char]
    [UsesFloat] -> [Char] -> [Char]
    UsesFloat -> [Char]
    (Nat -> UsesFloat -> [Char] -> [Char])
    -> (UsesFloat -> [Char])
    -> ([UsesFloat] -> [Char] -> [Char])
    -> Show UsesFloat
    forall a.
    (Nat -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: Nat -> UsesFloat -> [Char] -> [Char]
    showsPrec :: Nat -> UsesFloat -> [Char] -> [Char]
    $cshow :: UsesFloat -> [Char]
    show :: UsesFloat -> [Char]
    $cshowList :: [UsesFloat] -> [Char] -> [Char]
    showList :: [UsesFloat] -> [Char] -> [Char]
    Show)

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

    pattern NoFloat :: UsesFloat
    pattern $mNoFloat :: forall {r}. UsesFloat -> ((# #) -> r) -> ((# #) -> r) -> r
    $bNoFloat :: UsesFloat
    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
    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
      [Char]
    -> Nat
    -> TCM Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCM Doc -> m ()
    reportSDoc [Char]
    "compile.ghc.definition" Nat
    10 (TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $
        (TCM Doc
    "Not compiling" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q) TCM Doc -> TCM Doc -> TCM Doc
    forall a. Semigroup a => a -> a -> a
    <> TCM Doc
    "."
      (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    -> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
    forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
      [Char]
    -> Nat
    -> TCM Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCM Doc -> m ()
    reportSDoc [Char]
    "compile.ghc.definition" Nat
    10 (TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    vcat
        [ (TCM Doc
    "Compiling" TCM Doc -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCM Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q) TCM Doc -> TCM Doc -> TCM Doc
    forall a. Semigroup a => a -> a -> a
    <> TCM Doc
    ":"
        , Nat -> TCM Doc -> TCM Doc
    forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
    nest Nat
    2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $ Defn -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Defn
    d
        ]
      pragma <- TCM (Maybe HaskellPragma)
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
      env <- askGHCEnv
      let 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
      typeCheckedMainDef <- checkTypeOfMain def
      let 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
    ds = (a, b) -> m (a, b)
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    forall a. Monoid a => a
    mempty, b
    ds)
      (uncurry (,,typeCheckedMainDef)) . second ((mainDecl ++) . infodecl q) <$>
        case d of

          Defn
    _ | Just (HsDefn Range
    r [Char]
    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
    $ do
                -- Make sure we have imports for all names mentioned in the type.
                hsty <- QName -> HsCompileM Type
    haskellType QName
    q
                mapM_ (`xqual` HS.Ident "_") (namesIn ty :: Set QName)

              -- Check that the function isn't INLINE (since that will make this
              -- definition pointless).
                inline <- (^. funInline) . theDef <$> getConstInfo q
                when inline $ warning $ UselessInline q

                retDecls $ fbWithType hsty (fakeExp 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 true  <- BuiltinId
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    builtinTrue
            Just false <- getBuiltinName builtinFalse
            cs <- mapM (compiledcondecl Nothing) [false, true]
            retDecls $ [ compiledTypeSynonym q "Bool" 0
                       , HS.FunBind [HS.Match d [] (HS.UnGuardedRhs HS.unit_con) emptyBinds] ] ++
                       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
    -> (HaskellPragma
        -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe HaskellPragma
    pragma ((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
    PragmaCompileList
            let d :: Name
    d = QName -> Name
    dname QName
    q
                t :: Name
    t = NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q
            Just nil  <- BuiltinId
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    builtinNil
            Just cons <- getBuiltinName builtinCons
            let 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]
            cs <- mapM (compiledcondecl Nothing) [nil, cons]
            retDecls $ [ HS.TypeDecl t (vars HS.UnkindedVar (np - 1)) (HS.FakeType "[]")
                       , HS.FunBind [HS.Match d (vars HS.PVar np) (HS.UnGuardedRhs HS.unit_con) emptyBinds] ] ++
                       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
    -> (HaskellPragma
        -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
    whenJust Maybe HaskellPragma
    pragma ((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
    PragmaCompileMaybe
            let d :: Name
    d = QName -> Name
    dname QName
    q
                t :: Name
    t = NameKind -> QName -> Name
    unqhname NameKind
    TypeK QName
    q
            Just nothing <- BuiltinId
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    builtinNothing
            Just just    <- getBuiltinName builtinJust
            let 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]
            cs <- mapM (compiledcondecl Nothing) [nothing, just]
            retDecls $ [ HS.TypeDecl t (vars HS.UnkindedVar (np - 1)) (HS.FakeType "Maybe")
                       , HS.FunBind [HS.Match d (vars HS.PVar np) (HS.UnGuardedRhs HS.unit_con) emptyBinds] ] ++
                       cs

          -- Compiling Inf
          Defn
    _ | (GHCEnv -> Maybe QName) -> Bool
    is GHCEnv -> Maybe QName
    ghcEnvInf -> do
            _ <- 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 sharp <- getBuiltinName builtinSharp
            sharpC     <- (compiledcondecl Nothing) sharp
            let d   = QName -> Name
    dname QName
    q
                err = [Char]
    "No term-level implementation of the INFINITY builtin."
            retDecls $ [ compiledTypeSynonym q "MAlonzo.RTE.Infinity" 2
                       , HS.FunBind [HS.Match d [HS.PVar (ihname A 0)]
                           (HS.UnGuardedRhs (HS.FakeExp ("error " ++ show err)))
                           emptyBinds]
                       , 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 i0 <- BuiltinId
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    builtinIZero
            Just i1 <- getBuiltinName builtinIOne
            cs      <- mapM (compiledcondecl (Just 0)) [i0, i1]
            retDecls $
              [ compiledTypeSynonym q "Bool" 0
              , HS.FunBind
                  [HS.Match (dname q) []
                     (HS.UnGuardedRhs HS.unit_con) emptyBinds]
              ] ++
              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)]
                  ([Char] -> Type
    HS.FakeType [Char]
    "()")
              , [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 ([Char] -> Exp
    HS.FakeExp [Char]
    "\\_ _ _ -> ()"))
                     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 ([Char] -> Exp
    HS.FakeExp [Char]
    "\\_ 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 int <- BuiltinId
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    BuiltinId -> m (Maybe QName)
    getBuiltinName BuiltinId
    builtinInterval
            int      <- xhqn TypeK int
            retDecls $
              [ HS.TypeDecl (unqhname TypeK q)
                  [HS.UnkindedVar (ihname A i) | i <- [0..3]]
                  (HS.TyFun (HS.TyCon int) mazAnyType)
              , HS.FunBind
                  [HS.Match (dname q) []
                     (HS.UnGuardedRhs (HS.FakeExp "\\_ _ _ _ -> ()"))
                     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 ([Char] -> Exp
    HS.FakeExp [Char]
    "\\_ _ _ _ -> ()"))
                     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 ([Char] -> Exp
    HS.FakeExp [Char]
    "\\_ _ _ x -> x"))
                     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 ([Char] -> Exp
    HS.FakeExp [Char]
    mazErasedName))
                     Maybe Binds
    emptyBinds]
              ]

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

          Axiom{} -> do
            ar <- TCMT IO Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Nat
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat)
    -> TCMT IO Nat
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a b. (a -> b) -> a -> b
    $ Type -> TCMT IO Nat
    typeArity Type
    ty
            retDecls $ [ compiledTypeSynonym q ty ar | Just (HsType r ty) <- [pragma] ] ++
                       fb axiomErr
          Primitive{ primName :: Defn -> PrimitiveId
    primName = PrimitiveId
    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 a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Exp -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp)
    -> (PrimitiveId -> TCM Exp)
    -> PrimitiveId
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimitiveId -> TCM Exp
    forall (m :: * -> *). MonadTCError m => PrimitiveId -> m Exp
    primBody) PrimitiveId
    s

          PrimitiveSort{} -> [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 [Char]
    ty [[Char]]
    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
            [Char]
    -> Nat
    -> TCM Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> Nat -> TCM Doc -> m ()
    reportSDoc [Char]
    "compile.ghc.definition" Nat
    40 (TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ [TCM Doc] -> TCM Doc
    forall (m :: * -> *) (t :: * -> *).
    (Applicative m, Foldable t) =>
    t (m Doc) -> m Doc
    hsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
    forall a b. (a -> b) -> a -> b
    $
              [ TCM Doc
    "Compiling data type with COMPILE pragma ...", HaskellPragma -> TCM Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty HaskellPragma
    hsdata ]
            TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
            cs <- TCM [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
            ccscov <- constructorCoverageCode q (np + ni) cs ty hsCons
            cds <- mapM (compiledcondecl Nothing) cs
            let 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 -> [Char] -> Nat -> Decl
    compiledTypeSynonym QName
    q [Char]
    ty Nat
    np ]
                  , [Decl]
    cds
                  , [Decl]
    ccscov
                  ]
            retDecls 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
            TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
            cs <- TCM [QName]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
            cds <- mapM (flip condecl Inductive) cs
            retDecls $ tvaldecl q Inductive (np + ni) cds 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 [Char]
    ty [[Char]]
    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]
                TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
                ccscov <- QName
    -> Nat
    -> [QName]
    -> [Char]
    -> [[Char]]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    constructorCoverageCode QName
    q Nat
    np [QName]
    cs [Char]
    ty [[Char]]
    hsCons
                cds <- mapM (compiledcondecl Nothing) cs
                retDecls $
                  tvaldecl q inductionKind np [] (Just __IMPOSSIBLE__) ++
                  [compiledTypeSynonym q ty np] ++ cds ++ ccscov
              Maybe HaskellPragma
    _ -> do
                TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> TCMT IO ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
                cd <- QName
    -> Induction
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    condecl (ConHead -> QName
    conName ConHead
    con) Induction
    inductionKind
                retDecls $ tvaldecl q inductionKind (I.arity ty) [cd] 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
        (imp, ccls) <- ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    fun
        case mhe of
          Just (HsExport Range
    r [Char]
    name) -> do
              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 = [Name] -> Type -> Decl
    HS.TypeSig [[Char] -> Name
    HS.Ident [Char]
    name] Type
    t

                  def :: HS.Decl
                  def = [Match] -> Decl
    HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
    HS.Match ([Char] -> Name
    HS.Ident [Char]
    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]
              return (imp, [tsig,def] ++ ccls)
          Maybe HaskellPragma
    _ -> (UsesFloat, [Decl])
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
    forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
        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 = if Bool
    strict then EvaluationStrategy
    EagerEvaluation else EvaluationStrategy
    LazyEvaluation
        caseMaybeM (liftTCM $ toTreeless eval q) (pure mempty) $ \ TTerm
    treeless -> do

          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 = ArgUsage
    ArgUnused ArgUsage -> [ArgUsage] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [ArgUsage]
    used

          -- Compute the type approximation
          def <- getConstInfo q
          (argTypes0, resType) <- hsTelApproximation $ defType def
          let pars = case Definition -> Defn
    theDef Definition
    def of
                       Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Right 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  = Nat -> [Type] -> [Type]
    forall a. Nat -> [a] -> [a]
    drop Nat
    pars [Type]
    argTypes0
              argTypesS = [ArgUsage] -> [Type] -> [Type]
    forall a. [ArgUsage] -> [a] -> [a]
    filterUsed [ArgUsage]
    used [Type]
    argTypes

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

              tydecl  Name
    f t Type
    ts Type
    t = [Name] -> Type -> Decl
    HS.TypeSig [Name
    f] ((Type -> Type -> Type) -> Type -> t Type -> Type
    forall a b. (a -> b -> b) -> b -> t a -> b
    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
    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
    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 a. [a] -> 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 a. [a] -> 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
          (ps0, _) <- lamView <$> closedTerm_ (foldr ($) T.TErased $ replicate (length used) T.TLam)
          let b0 = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
    forall b a. (b -> a -> b) -> b -> [a] -> b
    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 -> 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

          return (useFloat,
                  if dostrip
                    then tyfunbind (dname q) argTypes resType ps0' b0 ++
                         tyfunbind (duname q) argTypesS resType ps b
                    else tyfunbind (dname q) argTypes resType ps 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 = BackendName -> Exp
    rtmError (BackendName -> Exp) -> BackendName -> Exp
    forall a b. (a -> b) -> a -> b
    $ [Char] -> BackendName
    Text.pack ([Char] -> BackendName) -> [Char] -> BackendName
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "postulate evaluated: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    q

    constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> HsCompileM [HS.Decl]
    constructorCoverageCode :: QName
    -> Nat
    -> [QName]
    -> [Char]
    -> [[Char]]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    constructorCoverageCode QName
    q Nat
    np [QName]
    cs [Char]
    hsTy [[Char]]
    hsCons = do
      -- Check that number of constructors matches up.
      Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    unless ([QName] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [QName]
    cs Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == [[Char]] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [[Char]]
    hsCons) (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
    $
        GHCBackendError
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    GHCBackendError -> m a
    ghcBackendError (GHCBackendError
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
    -> GHCBackendError
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
    forall a b. (a -> b) -> a -> b
    $ QName -> [QName] -> [[Char]] -> GHCBackendError
    ConstructorCountMismatch QName
    q [QName]
    cs [[Char]]
    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 (TCMT IO Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Bool
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool)
    -> TCMT IO Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Bool
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    QName -> m Bool
    noCheckCover QName
    q) ([Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
        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
     -> [Char]
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
    -> [QName]
    -> [[Char]]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [[Decl]]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM QName
    -> [Char]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    checkConstructorType [QName]
    cs [[Char]]
    hsCons
        cov <- liftTCM $ checkCover q hsTy np cs hsCons
        return $ ccs ++ 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' CCEnv NameSupply
    ccNameSupply :: Lens' CCEnv [Name]
    ccNameSupply [Name] -> f [Name]
    f CCEnv
    e =  (\ [Name]
    ns' -> CCEnv
    e { _ccNameSupply = 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' CCEnv CCContext
    ccContext :: Lens' CCEnv [Name]
    ccContext [Name] -> f [Name]
    f CCEnv
    e = (\ [Name]
    cxt -> CCEnv
    e { _ccContext = 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
      { _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 (HsCompileT m) a
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (WriterT UsesFloat (HsCompileT m) a
     -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a)
    -> (HsCompileT m a -> WriterT UsesFloat (HsCompileT m) a)
    -> HsCompileT m a
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . HsCompileT m a -> WriterT UsesFloat (HsCompileT m) a
    forall (m :: * -> *) a. Monad m => m a -> WriterT UsesFloat 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
      (xs, 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' CCEnv [Name]
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) [Name]
    forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
    view ([Name] -> f [Name]) -> CCEnv -> f CCEnv
    Lens' CCEnv [Name]
    ccNameSupply
      local (over ccNameSupply (const rest)) $ cont 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 a.
    (CCEnv -> CCEnv)
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local (Lens' CCEnv [Name] -> LensMap CCEnv [Name]
    forall o i. Lens' o i -> LensMap o i
    over ([Name] -> f [Name]) -> CCEnv -> f CCEnv
    Lens' CCEnv [Name]
    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
    -> [Char]
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
    checkConstructorType QName
    q [Char]
    hs = do
      ty <- QName -> HsCompileM Type
    haskellType QName
    q
      return [ HS.TypeSig [unqhname CheckK q] ty
             , HS.FunBind [HS.Match (unqhname CheckK q) []
                                    (HS.UnGuardedRhs $ fakeExp hs) emptyBinds]
             ]

    checkCover :: HasConstInfo m => QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> m [HS.Decl]
    checkCover :: forall (m :: * -> *).
    HasConstInfo m =>
    QName -> [Char] -> Nat -> [QName] -> [[Char]] -> m [Decl]
    checkCover QName
    q [Char]
    ty Nat
    n [QName]
    cs [[Char]]
    hsCons = do
      let tvs :: [[Char]]
    tvs = [ [Char]
    "a" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Nat -> [Char]
    forall a. Show a => a -> [Char]
    show Nat
    i | Nat
    i <- [Nat
    1..Nat
    n] ]
          makeClause :: QName -> [Char] -> m Alt
    makeClause QName
    c [Char]
    hsc = do
            a <- QName -> m Nat
    forall {f :: * -> *}. HasConstInfo f => QName -> f Nat
    erasedArity QName
    c
            let pat = QName -> [Pat] -> Pat
    HS.PApp (Name -> QName
    HS.UnQual (Name -> QName) -> Name -> QName
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Name
    HS.Ident [Char]
    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
            return $ HS.Alt pat (HS.UnGuardedRhs $ HS.unit_con) emptyBinds

      cs <- (QName -> [Char] -> m Alt) -> [QName] -> [[Char]] -> m [Alt]
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m [c]
    zipWithM QName -> [Char] -> m Alt
    forall {m :: * -> *}. HasConstInfo m => QName -> [Char] -> m Alt
    makeClause [QName]
    cs [[Char]]
    hsCons
      let 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
    $ [Char] -> Name
    HS.Ident [Char]
    "x") [Alt]
    cs

      return [ HS.TypeSig [unqhname CoverK q] $ fakeType $ unwords (ty : tvs) ++ " -> ()"
             , HS.FunBind [HS.Match (unqhname CoverK q) [HS.PVar $ HS.Ident "x"]
                                    (HS.UnGuardedRhs rhs) 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
      v <- TCM TTerm -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) TTerm
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    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
      runWriterT (term v `runReaderT` 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
      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
    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
    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 | isTrue c1, isFalse c2 -> return $ T.tIfThenElse (TCoerce $ TVar e) b1 b2
         | isTrue c2, isFalse c1 -> return $ T.tIfThenElse (TCoerce $ TVar e) b2 b1
         | otherwise             -> return t
    mkIf TTerm
    t = TTerm -> CC TTerm
    forall a.
    a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    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 a b.
    ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      a
    -> (a
        -> ReaderT
             CCEnv
             (WriterT
                UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
             b)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         b
    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 b a. IsBool b => b -> (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 a b.
    ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      (a -> b)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         b
    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 a b.
    ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      (a -> b)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         b
    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
          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
          isCompiled <- liftTCM $ isJust <$> getHaskellPragma f
          let given   = [TTerm] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [TTerm]
    ts
              needed  = [ArgUsage] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [ArgUsage]
    used
              missing = Nat -> [ArgUsage] -> [ArgUsage]
    forall a. Nat -> [a] -> [a]
    drop Nat
    given [ArgUsage]
    used
          if not isCompiled && ArgUnused `elem` used
            then if ArgUnused `elem` missing then term (etaExpand (needed - given) tm0) else do
              f <- liftCC $ HS.Var <$> xhqn (FunK NoUnused) 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.)
              hsCoerce f `apps` filterUsed used ts
            else do
              f <- liftCC $ HS.Var <$> xhqn (FunK PossiblyUnused) f
                                       -- use original (non-stripped) function
              coe f `apps` ts

        (T.TCon QName
    c, [TTerm]
    ts) -> do
          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 = Nat -> [Bool] -> [Bool]
    forall a. Nat -> [a] -> [a]
    drop ([TTerm] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [TTerm]
    ts) [Bool]
    erased
              notErased = Bool -> Bool
    not
          if all notErased missing
            then do
                    f <- liftCC $ HS.Con <$> conhqn c
                    hsCoerce f `apps` [ t | (t, False) <- zip ts erased ]
            else do
                    let n = [Bool] -> Nat
    forall a. [a] -> Nat
    forall (t :: * -> *) a. Foldable t => t a -> Nat
    length [Bool]
    missing
                    unless (n >= 1) __IMPOSSIBLE__  -- We will add at least on TLam, not getting a busy loop here.
                    term $ etaExpand (length missing) 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 a b.
    ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      a
    -> (a
        -> ReaderT
             CCEnv
             (WriterT
                UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
             b)
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         b
    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' CCEnv [Name]
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         [Name]
    forall o (m :: * -> *) i. MonadReader o m => Lens' o i -> m i
    view ([Name] -> f [Name]) -> CCEnv -> f CCEnv
    Lens' CCEnv [Name]
    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
        t1' <- TTerm -> CC Exp
    term TTerm
    t1
        intros 1 $ \[Name
    x] -> do
          Name -> Exp -> Exp -> Exp
    hsLet Name
    x Exp
    t1' (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Exp -> Exp
    hsCoerce (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
        sc'   <- TTerm -> CC Exp
    term (TTerm -> CC Exp) -> TTerm -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ Nat -> TTerm
    T.TVar Nat
    sc
        alts' <- traverse (alt sc) alts
        def'  <- term def
        let defAlt = Pat -> Rhs -> Maybe Binds -> Alt
    HS.Alt Pat
    HS.PWildCard (Exp -> Rhs
    HS.UnGuardedRhs Exp
    def') Maybe Binds
    emptyBinds
        return $ HS.Case (hsCoerce sc') (alts' ++ [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 a.
    a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    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 a.
    a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    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 a.
    a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    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 a.
    a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    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
    $ [Char] -> Name
    HS.Ident [Char]
    mazErasedName
      T.TError TError
    e  -> Exp -> CC Exp
    forall a.
    a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         a
    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 [Char]
    s      -> [Char] -> Exp
    rtmHole [Char]
    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
    $ [Char] -> QName
    hsName ([Char] -> QName) -> [Char] -> QName
    forall a b. (a -> b) -> a -> b
    $ TPrim -> [Char]
    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
            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
            env    <- liftCC askGHCEnv
            hConNm <-
              if | Just c == ghcEnvNil env ->
                   return $ HS.UnQual $ HS.Ident "[]"
                 | Just c == ghcEnvCons env ->
                   return $ HS.UnQual $ HS.Symbol ":"
                 | otherwise -> liftCC $ conhqn c
            mkAlt (HS.PApp hConNm $ [HS.PVar x | (x, False) <- zip xs erased])
        T.TAGuard TTerm
    g TTerm
    b -> do
          g <- TTerm -> CC Exp
    term TTerm
    g
          b <- term b
          return $ HS.Alt HS.PWildCard
                          (HS.GuardedRhss [HS.GuardedRhs [HS.Qualifier g] b])
                          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 = LitMeta TopLevelModuleName
    _ MetaId
    m } -> Pat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkAlt (MetaId -> Pat
    litmetapat MetaId
    m)
        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
          l <- Literal -> CC Exp
    forall (m :: * -> *). Monad m => Literal -> CCT m Exp
    literal Literal
    l
          mkGuarded (treelessPrimName T.PEqF) l b
        T.TALit { aLit :: TAlt -> Literal
    T.aLit = LitString BackendName
    s , aBody :: TAlt -> TTerm
    T.aBody = TTerm
    b } -> [Char]
    -> Exp
    -> TTerm
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkGuarded [Char]
    "(==)" (BackendName -> Exp
    litString BackendName
    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 :: [Char]
    -> Exp
    -> TTerm
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkGuarded [Char]
    eq Exp
    lit TTerm
    b = do
          b  <- TTerm -> CC Exp
    term TTerm
    b
          let varName = [Char] -> Name
    HS.Ident [Char]
    "l" -- only used locally in the guard
              pv = Name -> Pat
    HS.PVar Name
    varName
              v  = Name -> Exp
    hsVarUQ Name
    varName
              guard =
                QName -> Exp
    HS.Var (Name -> QName
    HS.UnQual ([Char] -> Name
    HS.Ident [Char]
    eq)) Exp -> Exp -> Exp
    `HS.App`
                  Exp
    v Exp -> Exp -> Exp
    `HS.App` Exp
    lit
          return $ HS.Alt pv
                          (HS.GuardedRhss [HS.GuardedRhs [HS.Qualifier guard] b])
                          emptyBinds

        mkAlt :: HS.Pat -> CC HS.Alt
        mkAlt :: Pat
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt
    mkAlt Pat
    pat = do
            body' <- TTerm -> CC Exp
    term (TTerm -> CC Exp) -> TTerm -> CC Exp
    forall a b. (a -> b) -> a -> b
    $ TAlt -> TTerm
    T.aBody TAlt
    a
            let body'' = case Exp
    body' of
                           HS.Lambda{} -> Exp -> Exp
    hsCoerce Exp
    body'
                           Exp
    _           -> Exp
    body'
            return $ HS.Alt pat (HS.UnGuardedRhs body'') 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 a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Exp
    typed [Char]
    "Integer"
      LitWord64 Word64
    _   -> Exp -> CCT m Exp
    forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Exp
    typed [Char]
    "MAlonzo.RTE.Word64"
      LitFloat  Double
    x   -> Double -> [Char] -> CCT m Exp
    floatExp Double
    x [Char]
    "Double"
      LitQName  QName
    x   -> Exp -> CCT m Exp
    forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    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 BackendName
    s   -> Exp -> CCT m Exp
    forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ BackendName -> Exp
    litString BackendName
    s
      LitMeta TopLevelModuleName
    _ MetaId
    m   ->
        Exp -> CCT m Exp
    forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Exp
    HS.FakeExp [Char]
    "(,)" Exp -> Exp -> Exp
    `HS.App`
                 Word64 -> Exp
    forall a. Integral a => a -> Exp
    hsTypedInt (MetaId -> Word64
    metaId MetaId
    m) Exp -> Exp -> Exp
    `HS.App`
                 (Word64 -> Exp
    forall a. Integral a => a -> Exp
    hsTypedInt (ModuleNameHash -> Word64
    moduleNameHash (ModuleNameHash -> Word64) -> ModuleNameHash -> Word64
    forall a b. (a -> b) -> a -> b
    $ MetaId -> ModuleNameHash
    metaModule MetaId
    m))
      Literal
    _             -> Exp -> CCT m Exp
    forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    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 :: [Char] -> Exp
    typed = Exp -> Type -> Exp
    HS.ExpTypeSig Exp
    l' (Type -> Exp) -> ([Char] -> Type) -> [Char] -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Type
    HS.TyCon (QName -> Type) -> ([Char] -> QName) -> [Char] -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> QName
    rtmQual

        -- ASR (2016-09-14): See Issue #2169.
        -- Ulf, 2016-09-28: and #2218.
        floatExp :: Double -> String -> CCT m HS.Exp
        floatExp :: Double -> [Char] -> CCT m Exp
    floatExp Double
    x [Char]
    s
          | Double -> Bool
    isPosInf  Double
    x = [Char] -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => [Char] -> m Exp
    rte [Char]
    "positiveInfinity"
          | Double -> Bool
    isNegInf  Double
    x = [Char] -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => [Char] -> m Exp
    rte [Char]
    "negativeInfinity"
          | Double -> Bool
    isNegZero Double
    x = [Char] -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => [Char] -> m Exp
    rte [Char]
    "negativeZero"
          | Double -> Bool
    forall a. RealFloat a => a -> Bool
    isNaN     Double
    x = [Char] -> CCT m Exp
    forall {m :: * -> *}. MonadWriter UsesFloat m => [Char] -> m Exp
    rte [Char]
    "nan"
          | Bool
    otherwise   = Exp -> CCT m Exp
    forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Exp
    typed [Char]
    s
          where
            rte :: [Char] -> m Exp
    rte [Char]
    s = do UsesFloat -> m ()
    forall w (m :: * -> *). MonadWriter w m => w -> m ()
    tell UsesFloat
    YesFloat; Exp -> m Exp
    forall a. a -> m a
    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
    $ [Char] -> Name
    HS.Ident [Char]
    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 BackendName
    _ -> Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      LitMeta{}   -> Literal
    forall a. HasCallStack => a
    __IMPOSSIBLE__

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

    litqname :: QName -> HS.Exp
    litqname :: QName -> Exp
    litqname QName
    x =
      [Char] -> Exp
    rteCon [Char]
    "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
    $ BackendName -> Literal
    HS.String (BackendName -> Literal) -> BackendName -> Literal
    forall a b. (a -> b) -> a -> b
    $ [Char] -> BackendName
    Text.pack ([Char] -> BackendName) -> [Char] -> BackendName
    forall a b. (a -> b) -> a -> b
    $ QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow QName
    x
      , [Char] -> Exp
    rteCon [Char]
    "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 b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Exp -> Exp -> Exp
    HS.App
        rteCon :: [Char] -> Exp
    rteCon [Char]
    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
    $ [Char] -> Name
    HS.Ident [Char]
    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   = [Char] -> Exp
    rteCon [Char]
    "NonAssoc"
        litAssoc Associativity
    LeftAssoc  = [Char] -> Exp
    rteCon [Char]
    "LeftAssoc"
        litAssoc Associativity
    RightAssoc = [Char] -> Exp
    rteCon [Char]
    "RightAssoc"

        litPrec :: FixityLevel -> Exp
    litPrec FixityLevel
    Unrelated   = [Char] -> Exp
    rteCon [Char]
    "Unrelated"
        litPrec (Related Double
    l) = [Char] -> Exp
    rteCon [Char]
    "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
    $ [Char] -> Name
    HS.Ident [Char]
    "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

    litmetapat :: MetaId -> HS.Pat
    litmetapat :: MetaId -> Pat
    litmetapat (MetaId Word64
    m ModuleNameHash
    h) =
      QName -> [Pat] -> Pat
    HS.PApp ([Char] -> QName
    hsName [Char]
    "(,)")
              [ 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)
              , 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 -> Integer) -> Word64 -> Integer
    forall a b. (a -> b) -> a -> b
    $ ModuleNameHash -> Word64
    moduleNameHash ModuleNameHash
    h) ]

    condecl :: QName -> Induction -> HsCompileM HS.ConDecl
    condecl :: QName
    -> Induction
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
    condecl QName
    q Induction
    _ind = do
      opts <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      def <- getConstInfo q
      let Constructor{ conPars = np, conSrcCon, conErased = erased } = theDef def
      (argTypes0, _) <- hsTelApproximation (defType def)
      let strict     = if ConHead -> Induction
    conInductive ConHead
    conSrcCon 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   = [ (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)
                       ]
      return $ HS.ConDecl (unqhname ConK q) 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
      ar <- case Maybe Nat
    mar of
        Maybe Nat
    Nothing -> TCMT IO Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a.
    TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCMT IO Nat
     -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat)
    -> TCMT IO Nat
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a b. (a -> b) -> a -> b
    $ QName -> TCMT IO Nat
    forall {f :: * -> *}. HasConstInfo f => QName -> f Nat
    erasedArity QName
    q
        Just Nat
    ar -> Nat -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Nat
    forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Nat
    ar
      hsCon <- fromMaybe __IMPOSSIBLE__ <$> getHaskellConstructor q
      let 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]
      return $ HS.PatSyn (HS.PApp (HS.UnQual $ unqhname ConK q) patVars)
                 (HS.PApp (hsName hsCon) patVars)

    compiledTypeSynonym :: QName -> String -> Nat -> HS.Decl
    compiledTypeSynonym :: QName -> [Char] -> Nat -> Decl
    compiledTypeSynonym QName
    q [Char]
    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 b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Type -> Type -> Type
    HS.TyApp ([Char] -> Type
    HS.FakeType [Char]
    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 = [Char] -> Decl
    HS.Comment (QName -> [Char]
    forall a. Pretty a => a -> [Char]
    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
      dataDir <- IO [Char] -> m [Char]
    forall a. IO a -> m a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO IO [Char]
    getDataDir
      let srcDir = [Char]
    dataDir [Char] -> [Char] -> [Char]
    </> [Char]
    "MAlonzo" [Char] -> [Char] -> [Char]
    </> [Char]
    "src"
      dstDir <- optGhcCompileDir <$> askGhcOpts
      liftIO $ copyDirContent srcDir 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.
      out <- ([Char], [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd (([Char], [Char]) -> [Char]) -> m ([Char], [Char]) -> m [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> m ([Char], [Char])
    forall (m :: * -> *).
    MonadGHCIO m =>
    ModuleName -> m ([Char], [Char])
    outFileAndDir ModuleName
    m
      strict <- optGhcStrict <$> askGhcOpts
      let languagePragmas =
            ([Char] -> ModulePragma) -> [[Char]] -> [ModulePragma]
    forall a b. (a -> b) -> [a] -> [b]
    List.map ([Name] -> ModulePragma
    HS.LanguagePragma ([Name] -> ModulePragma)
    -> ([Char] -> [Name]) -> [Char] -> ModulePragma
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> [Name]
    forall el coll. Singleton el coll => el -> coll
    singleton (Name -> [Name]) -> ([Char] -> Name) -> [Char] -> [Name]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> Name
    HS.Ident) ([[Char]] -> [ModulePragma]) -> [[Char]] -> [ModulePragma]
    forall a b. (a -> b) -> a -> b
    $
              [[Char]] -> [[Char]]
    forall a. Ord a => [a] -> [a]
    List.sort ([[Char]] -> [[Char]]) -> [[Char]] -> [[Char]]
    forall a b. (a -> b) -> a -> b
    $
                [ [Char]
    "QualifiedDo" | Bool
    strict ] [[Char]] -> [[Char]] -> [[Char]]
    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.
                [ [Char]
    "BangPatterns"
                , [Char]
    "EmptyDataDecls"
                , [Char]
    "EmptyCase"
                , [Char]
    "ExistentialQuantification"
                , [Char]
    "ScopedTypeVariables"
                , [Char]
    "NoMonomorphismRestriction"
                , [Char]
    "RankNTypes"
                , [Char]
    "PatternSynonyms"
                , [Char]
    "OverloadedStrings"
                ]
      let ghcOptions =
            ([Char] -> ModulePragma) -> [[Char]] -> [ModulePragma]
    forall a b. (a -> b) -> [a] -> [b]
    List.map [Char] -> ModulePragma
    HS.OtherPragma
              [ [Char]
    ""  -- to separate from LANGUAGE pragmas
              , [Char]
    "{-# 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.)
              ]
      liftIO $ UTF8.writeFile out $ (++ "\n") $ prettyPrint $
        -- TODO: It might make sense to skip bang patterns for the unused
        -- arguments of the "non-stripped" functions.
        applyWhen strict makeStrict $
        HS.Module m (concat [languagePragmas, ghcOptions, ps]) imp ds

    outFileAndDir :: MonadGHCIO m => HS.ModuleName -> m (FilePath, FilePath)
    outFileAndDir :: forall (m :: * -> *).
    MonadGHCIO m =>
    ModuleName -> m ([Char], [Char])
    outFileAndDir ModuleName
    m = do
      mdir <- GHCOptions -> [Char]
    optGhcCompileDir (GHCOptions -> [Char]) -> m GHCOptions -> m [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      let (fdir, fn) = splitFileName $ repldot pathSeparator $
                       prettyPrint m
      let dir = [Char]
    mdir [Char] -> [Char] -> [Char]
    </> [Char]
    fdir
          fp  = [Char]
    dir [Char] -> [Char] -> [Char]
    </> [Char] -> [Char] -> [Char]
    replaceExtension [Char]
    fn [Char]
    "hs"
      liftIO $ createDirectoryIfMissing True dir
      return (mdir, fp)
      where
      repldot :: Char -> [Char] -> [Char]
    repldot Char
    c = (Char -> Char) -> [Char] -> [Char]
    forall a b. (a -> b) -> [a] -> [b]
    List.map ((Char -> Char) -> [Char] -> [Char])
    -> (Char -> Char) -> [Char] -> [Char]
    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 ([Char], [Char])
    curOutFileAndDir = ModuleName -> m ([Char], [Char])
    forall (m :: * -> *).
    MonadGHCIO m =>
    ModuleName -> m ([Char], [Char])
    outFileAndDir (ModuleName -> m ([Char], [Char]))
    -> m ModuleName -> m ([Char], [Char])
    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 [Char]
    curOutFile = ([Char], [Char]) -> [Char]
    forall a b. (a, b) -> b
    snd (([Char], [Char]) -> [Char]) -> m ([Char], [Char]) -> m [Char]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m ([Char], [Char])
    forall (m :: * -> *).
    (MonadGHCIO m, ReadGHCModuleEnv m) =>
    m ([Char], [Char])
    curOutFileAndDir

    callGHC :: ReaderT GHCModule TCM ()
    callGHC :: ReaderT GHCModule TCM ()
    callGHC = do
      opts     <- ReaderT GHCModule TCM GHCOptions
    forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
    askGhcOpts
      agdaOpts <- lift commandLineOptions
      hsmod    <- prettyPrint <$> curHsMod
      agdaMod  <- curAgdaMod
      let outputName = BackendName -> [Char]
    Text.unpack (BackendName -> [Char]) -> BackendName -> [Char]
    forall a b. (a -> b) -> a -> b
    $ NonEmpty BackendName -> BackendName
    forall a. NonEmpty a -> a
    List1.last (NonEmpty BackendName -> BackendName)
    -> NonEmpty BackendName -> BackendName
    forall a b. (a -> b) -> a -> b
    $ TopLevelModuleName -> NonEmpty BackendName
    forall range. TopLevelModuleName' range -> NonEmpty BackendName
    moduleNameParts TopLevelModuleName
    agdaMod
      (mdir, fp) <- curOutFileAndDir
      let ghcopts = GHCOptions -> [[Char]]
    optGhcFlags GHCOptions
    opts

      modIsMain <- curIsMainModule
      modHasMainFunc <- asks (not . null . ghcModMainFuncs)
      let isMain = Bool
    modIsMain Bool -> Bool -> Bool
    && Bool
    modHasMainFunc  -- both need to be IsMain

      -- Warn if no main function and not --no-main
      when (modIsMain /= isMain) $ warning $ NoMain agdaMod

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

      let ghcBin = GHCOptions -> [Char]
    optGhcBin GHCOptions
    opts

      -- Make GHC use UTF-8 when writing to stdout and stderr.
      liftIO $ setEnv "GHC_CHARENC" "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 = GHCOptions -> Bool
    optGhcCallGhc GHCOptions
    opts
          cwd    = if CommandLineOptions -> Bool
    optGHCiInteraction CommandLineOptions
    agdaOpts Bool -> Bool -> Bool
    ||
                      CommandLineOptions -> Bool
    optJSONInteraction CommandLineOptions
    agdaOpts
                   then [Char] -> Maybe [Char]
    forall a. a -> Maybe a
    Just [Char]
    mdir
                   else Maybe [Char]
    forall a. Maybe a
    Nothing
      liftTCM $ callCompiler doCall ghcBin args cwd (Just utf8)