module Agda.Compiler.MAlonzo.Compiler where

import Control.Arrow (second)
import Control.DeepSeq
import Control.Monad.Except (throwError)
import Control.Monad.Reader
import Control.Monad.Writer hiding ((<>))

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.FilePath hiding (normalise)

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

--- Command-line flags ---

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

instance NFData GHCFlags

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

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

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

--- Context types ---

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

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

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

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

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

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

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

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

--- Top-level compilation ---

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

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

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

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

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

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

--- Module compilation ---

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Constructor coverage monad
type CC = CCT TCM

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)

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

writeModule :: MonadGHCIO m => HS.Module -> m ()
writeModule :: forall (m :: * -> *). MonadGHCIO m => Module -> m ()
writeModule (HS.Module ModuleName
m [ModulePragma]
ps [ImportDecl]
imp [Decl]
ds) = do
  -- Note that GHC assumes that sources use ASCII or UTF-8.
  FilePath
out <- (FilePath, FilePath) -> FilePath
forall a b. (a, b) -> b
snd ((FilePath, FilePath) -> FilePath)
-> m (FilePath, FilePath) -> m FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> m (FilePath, FilePath)
forall (m :: * -> *).
MonadGHCIO m =>
ModuleName -> m (FilePath, FilePath)
outFileAndDir ModuleName
m
  Bool
strict <- GHCOptions -> Bool
optGhcStrict (GHCOptions -> Bool) -> m GHCOptions -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m GHCOptions
forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  let p :: ModulePragma
p = [Name] -> ModulePragma
HS.LanguagePragma ([Name] -> ModulePragma) -> [Name] -> ModulePragma
forall a b. (a -> b) -> a -> b
$ (FilePath -> Name) -> [FilePath] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
List.map FilePath -> Name
HS.Ident ([FilePath] -> [Name]) -> [FilePath] -> [Name]
forall a b. (a -> b) -> a -> b
$
            [ FilePath
"BangPatterns"
            , FilePath
"EmptyDataDecls"
            , FilePath
"EmptyCase"
            , FilePath
"ExistentialQuantification"
            , FilePath
"ScopedTypeVariables"
            , FilePath
"NoMonomorphismRestriction"
            , FilePath
"RankNTypes"
            , FilePath
"PatternSynonyms"
            , FilePath
"OverloadedStrings"
            ] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
            -- If --ghc-strict is used, then the language extension
            -- QualifiedDo is activated. At the time of writing no
            -- code is generated that depends on this extension
            -- (except for the pragmas), but --ghc-strict is broken
            -- with at least some versions of GHC prior to version 9,
            -- and QualifiedDo was introduced with GHC 9.
            if Bool
strict
            then [FilePath
"QualifiedDo"]
            else []
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
UTF8.writeFile FilePath
out (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
"\n") (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Module -> FilePath
forall a. Pretty a => a -> FilePath
prettyPrint (Module -> FilePath) -> Module -> FilePath
forall a b. (a -> b) -> a -> b
$
    -- TODO: It might make sense to skip bang patterns for the unused
    -- arguments of the "non-stripped" functions.
    (if Bool
strict then Module -> Module
forall a. MakeStrict a => a -> a
makeStrict else Module -> Module
forall a. a -> a
id) (Module -> Module) -> Module -> Module
forall a b. (a -> b) -> a -> b
$
    ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
HS.Module ModuleName
m (ModulePragma
p ModulePragma -> [ModulePragma] -> [ModulePragma]
forall a. a -> [a] -> [a]
: [ModulePragma]
ps) [ImportDecl]
imp [Decl]
ds
  where

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

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

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

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

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

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

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

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

  -- Note: Some versions of GHC use stderr for progress reports. For
  -- those versions of GHC we don't print any progress information
  -- unless an error is encountered.
  let doCall :: Bool
doCall = GHCOptions -> Bool
optGhcCallGhc GHCOptions
opts
  TCM () -> ReaderT GHCModule TCM ()
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> ReaderT GHCModule TCM ())
-> TCM () -> ReaderT GHCModule TCM ()
forall a b. (a -> b) -> a -> b
$ Bool -> FilePath -> [FilePath] -> TCM ()
callCompiler Bool
doCall FilePath
ghcBin [FilePath]
args