module Agda.Compiler.MAlonzo.Compiler where

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

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

import GHC.Generics (Generic)

import qualified Agda.Utils.Haskell.Syntax as HS

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

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

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

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

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

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

import Paths_Agda

import Agda.Utils.Impossible

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

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

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

--- Command-line flags ---

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

instance NFData GHCFlags

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

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

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

--- Context types ---

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

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

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

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

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

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

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

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

--- Top-level compilation ---

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

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

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

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

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

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

--- Module compilation ---

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

definition :: Definition -> HsCompileM (UsesFloat, [HS.Decl], Maybe CheckedMainFunctionDef)
-- ignore irrelevant definitions
{- Andreas, 2012-10-02: Invariant no longer holds
definition kit (Defn NonStrict _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
-}
definition :: Definition
-> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
definition Defn{defArgInfo :: Definition -> ArgInfo
defArgInfo = ArgInfo
info, defName :: Definition -> QName
defName = QName
q} | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality ArgInfo
info = do
  String
-> VerboseLevel
-> TCM Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"compile.ghc.definition" VerboseLevel
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
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 (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
  String
-> VerboseLevel
-> TCM Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"compile.ghc.definition" VerboseLevel
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
prettyTCM QName
q) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
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
    ]
  Maybe HaskellPragma
pragma <- TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q
  GHCEnv
env <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCEnv
forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
p = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
p GHCEnv
env
  Maybe CheckedMainFunctionDef
typeCheckedMainDef <- Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
checkTypeOfMain Definition
def
  let mainDecl :: [Decl]
mainDecl = Maybe Decl -> [Decl]
forall a. Maybe a -> [a]
maybeToList (Maybe Decl -> [Decl]) -> Maybe Decl -> [Decl]
forall a b. (a -> b) -> a -> b
$ CheckedMainFunctionDef -> Decl
checkedMainDecl (CheckedMainFunctionDef -> Decl)
-> Maybe CheckedMainFunctionDef -> Maybe Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CheckedMainFunctionDef
typeCheckedMainDef
  let retDecls :: b -> m (a, b)
retDecls b
ds = (a, b) -> m (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
forall a. Monoid a => a
mempty, b
ds)
  ((UsesFloat
 -> [Decl] -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef))
-> (UsesFloat, [Decl])
-> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (,,Maybe CheckedMainFunctionDef
typeCheckedMainDef)) ((UsesFloat, [Decl])
 -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef))
-> ((UsesFloat, [Decl]) -> (UsesFloat, [Decl]))
-> (UsesFloat, [Decl])
-> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Decl] -> [Decl]) -> (UsesFloat, [Decl]) -> (UsesFloat, [Decl])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (([Decl]
mainDecl [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++) ([Decl] -> [Decl]) -> ([Decl] -> [Decl]) -> [Decl] -> [Decl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Decl] -> [Decl]
infodecl QName
q) ((UsesFloat, [Decl])
 -> (UsesFloat, [Decl], Maybe CheckedMainFunctionDef))
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    case Defn
d of

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

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

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

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

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

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

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

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

      -- IsOne is compiled as the constant function to the unit type.
      -- Partial/PartialP are compiled as functions from the unit type
      -- to the underlying type.
      Axiom{} | (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvIsOne -> do
        [Decl]
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) a b. (Monad m, Monoid a) => b -> m (a, b)
retDecls ([Decl]
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
-> [Decl]
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall a b. (a -> b) -> a -> b
$
          [ Name -> [TyVarBind] -> Type -> Decl
HS.TypeDecl (NameKind -> QName -> Name
unqhname NameKind
TypeK QName
q) [Name -> TyVarBind
HS.UnkindedVar (VariableKind -> VerboseLevel -> Name
ihname VariableKind
A VerboseLevel
0)]
              (String -> Type
HS.FakeType String
"()")
          , [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 (String -> Exp
HS.FakeExp String
"\\_ _ _ -> ()"))
                 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 (String -> Exp
HS.FakeExp String
"\\_ x _ -> x ()"))
                 Maybe Binds
emptyBinds]
          ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Term variables are de Bruijn indices.
lookupIndex :: Int -> CCContext -> HS.Name
lookupIndex :: VerboseLevel -> [Name] -> Name
lookupIndex VerboseLevel
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] -> VerboseLevel -> Maybe Name
forall a. [a] -> VerboseLevel -> Maybe a
!!! VerboseLevel
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 :: HsCompileT m a -> CCT m a
liftCC = WriterT UsesFloat (HsCompileT m) a -> CCT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT UsesFloat (HsCompileT m) a -> CCT m a)
-> (HsCompileT m a -> WriterT UsesFloat (HsCompileT m) a)
-> HsCompileT m a
-> CCT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsCompileT m a -> WriterT UsesFloat (HsCompileT 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 :: VerboseLevel -> ([Name] -> CCT m a) -> CCT m a
freshNames VerboseLevel
n [Name] -> CCT m a
_ | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< VerboseLevel
0 = CCT m a
forall a. HasCallStack => a
__IMPOSSIBLE__
freshNames VerboseLevel
n [Name] -> CCT m a
cont = do
  ([Name]
xs, [Name]
rest) <- VerboseLevel -> [Name] -> ([Name], [Name])
forall a. VerboseLevel -> [a] -> ([a], [a])
splitAt VerboseLevel
n ([Name] -> ([Name], [Name]))
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) [Name]
-> ReaderT
     CCEnv (WriterT UsesFloat (HsCompileT m)) ([Name], [Name])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' [Name] CCEnv
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) [Name]
forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view Lens' [Name] CCEnv
ccNameSupply
  (CCEnv -> CCEnv) -> CCT m a -> CCT m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Lens' [Name] CCEnv -> LensMap [Name] CCEnv
forall i o. Lens' i o -> LensMap i o
over Lens' [Name] CCEnv
ccNameSupply ([Name] -> [Name] -> [Name]
forall a b. a -> b -> a
const [Name]
rest)) (CCT m a -> CCT m a) -> CCT m a -> CCT m a
forall a b. (a -> b) -> a -> b
$ [Name] -> CCT m a
cont [Name]
xs

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

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

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

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

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

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

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

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

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

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

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

    -- Other kind of application: fall back to apps.
    (TTerm
t, [TTerm]
ts) -> TTerm -> CC Exp
noApplication TTerm
t CC Exp -> (Exp -> CC Exp) -> CC Exp
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Exp
t' -> Exp -> Exp
coe Exp
t' Exp -> [TTerm] -> CC Exp
`apps` [TTerm]
ts
  where
  apps :: Exp -> [TTerm] -> CC Exp
apps = (Exp -> TTerm -> CC Exp) -> Exp -> [TTerm] -> CC Exp
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ Exp
h TTerm
a -> Exp -> Exp -> Exp
HS.App Exp
h (Exp -> Exp) -> CC Exp -> CC Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> CC Exp
term TTerm
a)
  etaExpand :: VerboseLevel -> TTerm -> TTerm
etaExpand VerboseLevel
n TTerm
t = VerboseLevel -> TTerm -> TTerm
mkTLam VerboseLevel
n (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TTerm -> TTerm
forall a. Subst a => VerboseLevel -> a -> a
raise VerboseLevel
n TTerm
t TTerm -> [TTerm] -> TTerm
`T.mkTApp` (VerboseLevel -> TTerm) -> [VerboseLevel] -> [TTerm]
forall a b. (a -> b) -> [a] -> [b]
map VerboseLevel -> TTerm
T.TVar (VerboseLevel -> [VerboseLevel]
forall a. Integral a => a -> [a]
downFrom VerboseLevel
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 VerboseLevel
i    -> Name -> Exp
hsVarUQ (Name -> Exp) -> ([Name] -> Name) -> [Name] -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VerboseLevel -> [Name] -> Name
lookupIndex VerboseLevel
i ([Name] -> Exp)
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT TCM)) [Name]
-> CC Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' [Name] CCEnv
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT TCM)) [Name]
forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view Lens' [Name] CCEnv
ccContext
  T.TLam TTerm
t    -> VerboseLevel -> ([Name] -> CC Exp) -> CC Exp
forall (m :: * -> *) a.
Monad m =>
VerboseLevel -> ([Name] -> CCT m a) -> CCT m a
intros VerboseLevel
1 (([Name] -> CC Exp) -> CC Exp) -> ([Name] -> CC Exp) -> CC Exp
forall a b. (a -> b) -> a -> b
$ \ [Name
x] -> [Pat] -> Exp -> Exp
hsLambda [Name -> Pat
HS.PVar Name
x] (Exp -> Exp) -> CC Exp -> CC Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> CC Exp
term TTerm
t

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

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

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

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

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

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

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

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

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

litqname :: QName -> HS.Exp
litqname :: QName -> Exp
litqname QName
x =
  String -> Exp
rteCon String
"QName" Exp -> [Exp] -> Exp
`apps`
  [ Word64 -> Exp
forall a. Integral a => a -> Exp
hsTypedInt Word64
n
  , Word64 -> Exp
forall a. Integral a => a -> Exp
hsTypedInt Word64
m
  , Literal -> Exp
HS.Lit (Literal -> Exp) -> Literal -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Literal
HS.String (Text -> Literal) -> Text -> Literal
forall a b. (a -> b) -> a -> b
$ String -> Text
Text.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
x
  , String -> Exp
rteCon String
"Fixity" Exp -> [Exp] -> Exp
`apps`
    [ Associativity -> Exp
litAssoc (Fixity -> Associativity
fixityAssoc Fixity
fx)
    , FixityLevel -> Exp
litPrec  (Fixity -> FixityLevel
fixityLevel Fixity
fx)
    ]
  ]
  where
    apps :: Exp -> [Exp] -> Exp
apps = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
HS.App
    rteCon :: String -> Exp
rteCon String
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
$ String -> Name
HS.Ident String
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   = String -> Exp
rteCon String
"NonAssoc"
    litAssoc Associativity
LeftAssoc  = String -> Exp
rteCon String
"LeftAssoc"
    litAssoc Associativity
RightAssoc = String -> Exp
rteCon String
"RightAssoc"

    litPrec :: FixityLevel -> Exp
litPrec FixityLevel
Unrelated   = String -> Exp
rteCon String
"Unrelated"
    litPrec (Related Double
l) = String -> Exp
rteCon String
"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
$ String -> Name
HS.Ident String
"QName")
          [ Literal -> Pat
HS.PLit (Integer -> Literal
HS.Int (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n)
          , Literal -> Pat
HS.PLit (Integer -> Literal
HS.Int (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
m)
          , Pat
HS.PWildCard, Pat
HS.PWildCard ]
  where
    NameId Word64
n (ModuleNameHash Word64
m) = Name -> NameId
nameId (Name -> NameId) -> Name -> NameId
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
x

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

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

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

tvaldecl :: QName
         -> Induction
            -- ^ Is the type inductive or coinductive?
         -> Nat -> [HS.ConDecl] -> Maybe Clause -> [HS.Decl]
tvaldecl :: QName
-> Induction -> VerboseLevel -> [ConDecl] -> Maybe Clause -> [Decl]
tvaldecl QName
q Induction
ind VerboseLevel
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 -> VerboseLevel -> Name
ihname VariableKind
A VerboseLevel
i | VerboseLevel
i <- [VerboseLevel
0 .. VerboseLevel
npar VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
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 = String -> Decl
HS.Comment (QName -> String
forall a. Pretty a => a -> String
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 :: m ()
copyRTEModules = do
  String
dataDir <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getDataDir
  let srcDir :: String
srcDir = String
dataDir String -> String -> String
</> String
"MAlonzo" String -> String -> String
</> String
"src"
  String
dstDir <- GHCOptions -> String
optGhcCompileDir (GHCOptions -> String) -> m GHCOptions -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCOptions
forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
copyDirContent String
srcDir String
dstDir

writeModule :: MonadGHCIO m => HS.Module -> m ()
writeModule :: 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.
  String
out <- (String, String) -> String
forall a b. (a, b) -> b
snd ((String, String) -> String) -> m (String, String) -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (String, String)
forall (m :: * -> *).
MonadGHCIO m =>
ModuleName -> m (String, String)
outFileAndDir ModuleName
m
  Bool
strict <- GHCOptions -> Bool
optGhcStrict (GHCOptions -> Bool) -> m GHCOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCOptions
forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  let languagePragmas :: [ModulePragma]
languagePragmas =
        (String -> ModulePragma) -> [String] -> [ModulePragma]
forall a b. (a -> b) -> [a] -> [b]
List.map ([Name] -> ModulePragma
HS.LanguagePragma ([Name] -> ModulePragma)
-> (String -> [Name]) -> String -> ModulePragma
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Name]
forall el coll. Singleton el coll => el -> coll
singleton (Name -> [Name]) -> (String -> Name) -> String -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident) ([String] -> [ModulePragma]) -> [String] -> [ModulePragma]
forall a b. (a -> b) -> a -> b
$
          [String] -> [String]
forall a. Ord a => [a] -> [a]
List.sort ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
            [ String
"QualifiedDo" | Bool
strict ] [String] -> [String] -> [String]
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.
            [ String
"BangPatterns"
            , String
"EmptyDataDecls"
            , String
"EmptyCase"
            , String
"ExistentialQuantification"
            , String
"ScopedTypeVariables"
            , String
"NoMonomorphismRestriction"
            , String
"RankNTypes"
            , String
"PatternSynonyms"
            , String
"OverloadedStrings"
            ]
  let ghcOptions :: [ModulePragma]
ghcOptions =
        (String -> ModulePragma) -> [String] -> [ModulePragma]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> ModulePragma
HS.OtherPragma
          [ String
""  -- to separate from LANGUAGE pragmas
          , String
"{-# OPTIONS_GHC -Wno-overlapping-patterns #-}"
              -- Andreas, 2022-01-26, issue #5758:
              -- Place this in generated file rather than
              -- passing it only when calling GHC from within Agda.
              -- This will silence the warning for the Agda-generated .hs
              -- files while it can be on for other .hs files in the same
              -- project.  (E.g., when using cabal/stack to compile.)
          ]
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
UTF8.writeFile String
out (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Module -> String
forall a. Pretty a => a -> String
prettyPrint (Module -> String) -> Module -> String
forall a b. (a -> b) -> a -> b
$
    -- TODO: It might make sense to skip bang patterns for the unused
    -- arguments of the "non-stripped" functions.
    Bool -> (Module -> Module) -> Module -> Module
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
strict Module -> Module
forall a. MakeStrict a => a -> a
makeStrict (Module -> Module) -> Module -> Module
forall a b. (a -> b) -> a -> b
$
    ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
HS.Module ModuleName
m ([[ModulePragma]] -> [ModulePragma]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[ModulePragma]
languagePragmas, [ModulePragma]
ghcOptions, [ModulePragma]
ps]) [ImportDecl]
imp [Decl]
ds

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

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

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

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

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

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

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