module Agda.Compiler.MAlonzo.Compiler where

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

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

import GHC.Generics (Generic)

import qualified Agda.Utils.Haskell.Syntax as HS

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

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

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

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

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 qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty (prettyShow, render)
import Agda.Utils.Singleton
import qualified Agda.Utils.IO.UTF8 as UTF8
import Agda.Utils.String

import Paths_Agda

import Agda.Utils.Impossible

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

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

ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
ghcBackend' = Backend'
  { backendName :: [Char]
backendName           = [Char]
"GHC"
  , backendVersion :: Maybe [Char]
backendVersion        = Maybe [Char]
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 TopLevelModuleName GHCModule -> TCM ()
postCompile           = GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCM ()
ghcPostCompile
  , preModule :: GHCEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> TCM (Recompile GHCModuleEnv GHCModule)
preModule             = GHCEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> TCM (Recompile GHCModuleEnv GHCModule)
ghcPreModule
  , postModule :: GHCEnv
-> GHCModuleEnv
-> IsMain
-> TopLevelModuleName
-> [GHCDefinition]
-> TCM GHCModule
postModule            = GHCEnv
-> GHCModuleEnv
-> IsMain
-> TopLevelModuleName
-> [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 [Char]
flagGhcBin     :: Maybe FilePath
    -- ^ Use the compiler at PATH instead of "ghc"
  , GHCFlags -> [[Char]]
flagGhcFlags      :: [String]
  , GHCFlags -> Bool
flagGhcStrictData :: Bool
    -- ^ Make inductive constructors strict?
  , GHCFlags -> Bool
flagGhcStrict :: Bool
    -- ^ Make functions strict?
  }
  deriving (forall x. GHCFlags -> Rep GHCFlags x)
-> (forall x. Rep GHCFlags x -> GHCFlags) -> Generic GHCFlags
forall x. Rep GHCFlags x -> GHCFlags
forall x. GHCFlags -> Rep GHCFlags x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. GHCFlags -> Rep GHCFlags x
from :: forall x. GHCFlags -> Rep GHCFlags x
$cto :: forall x. Rep GHCFlags x -> GHCFlags
to :: forall x. Rep GHCFlags x -> GHCFlags
Generic

instance NFData GHCFlags

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

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

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

--- Context types ---

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

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

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

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

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

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

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

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

--- Top-level compilation ---

ghcPreCompile :: GHCFlags -> TCM GHCEnv
ghcPreCompile :: GHCFlags -> 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 :: [Char] -> m a
notSupported [Char]
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
$ [Char] -> TypeError
GenericError ([Char] -> TypeError) -> [Char] -> TypeError
forall a b. (a -> b) -> a -> b
$
          [Char]
"Compilation of code that uses " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
s [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not supported."
  case Maybe Cubical
cubical of
    Maybe Cubical
Nothing      -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CErased -> () -> TCM ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CFull   -> [Char] -> TCM ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
notSupported [Char]
"--cubical"

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

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

  QName -> Bool
istcbuiltin <- do
    [Maybe QName]
builtins <- ([Char] -> TCMT IO (Maybe QName))
-> [[Char]] -> TCMT IO [Maybe QName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM [Char] -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName
      [ [Char]
builtinAgdaTCMReturn
      , [Char]
builtinAgdaTCMBind
      , [Char]
builtinAgdaTCMUnify
      , [Char]
builtinAgdaTCMTypeError
      , [Char]
builtinAgdaTCMInferType
      , [Char]
builtinAgdaTCMCheckType
      , [Char]
builtinAgdaTCMNormalise
      , [Char]
builtinAgdaTCMReduce
      , [Char]
builtinAgdaTCMCatchError
      , [Char]
builtinAgdaTCMQuoteTerm
      , [Char]
builtinAgdaTCMUnquoteTerm
      , [Char]
builtinAgdaTCMQuoteOmegaTerm
      , [Char]
builtinAgdaTCMGetContext
      , [Char]
builtinAgdaTCMExtendContext
      , [Char]
builtinAgdaTCMInContext
      , [Char]
builtinAgdaTCMFreshName
      , [Char]
builtinAgdaTCMDeclareDef
      , [Char]
builtinAgdaTCMDeclarePostulate
      , [Char]
builtinAgdaTCMDeclareData
      , [Char]
builtinAgdaTCMDefineData
      , [Char]
builtinAgdaTCMDefineFun
      , [Char]
builtinAgdaTCMGetType
      , [Char]
builtinAgdaTCMGetDefinition
      , [Char]
builtinAgdaTCMBlockOnMeta
      , [Char]
builtinAgdaTCMCommit
      , [Char]
builtinAgdaTCMIsMacro
      , [Char]
builtinAgdaTCMWithNormalisation
      , [Char]
builtinAgdaTCMWithReconsParams
      , [Char]
builtinAgdaTCMFormatErrorParts
      , [Char]
builtinAgdaTCMDebugPrint
      , [Char]
builtinAgdaTCMOnlyReduceDefs
      , [Char]
builtinAgdaTCMDontReduceDefs
      , [Char]
builtinAgdaTCMNoConstraints
      , [Char]
builtinAgdaTCMRunSpeculative
      , [Char]
builtinAgdaTCMExec
      , [Char]
builtinAgdaTCMGetInstances
      ]
    (QName -> Bool) -> TCMT IO (QName -> Bool)
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
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 TopLevelModuleName GHCModule -> TCM ()
ghcPostCompile :: GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCM ()
ghcPostCompile GHCEnv
_cenv IsMain
_isMain Map TopLevelModuleName GHCModule
mods = do
  -- FIXME: @curMName@ and @curIF@ are evil TCM state, but there does not appear to be
  --------- another way to retrieve the compilation root ("main" module or interaction focused).
  TopLevelModuleName
rootModuleName <- TCMT IO TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
  GHCModule
rootModule <- Maybe GHCModule
-> (GHCModule -> TCM GHCModule) -> TCM GHCModule -> TCM GHCModule
forall a b. Maybe a -> (a -> b) -> b -> b
ifJust (TopLevelModuleName
-> Map TopLevelModuleName GHCModule -> Maybe GHCModule
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TopLevelModuleName
rootModuleName Map TopLevelModuleName GHCModule
mods) GHCModule -> TCM GHCModule
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                (TCM GHCModule -> TCM GHCModule) -> TCM GHCModule -> TCM GHCModule
forall a b. (a -> b) -> a -> b
$ [Char] -> TCM GHCModule
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError ([Char] -> TCM GHCModule) -> [Char] -> TCM GHCModule
forall a b. (a -> b) -> a -> b
$ [Char]
"Module " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow TopLevelModuleName
rootModuleName [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" 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?
  -> TopLevelModuleName
  -> Maybe FilePath    -- ^ Path to the @.agdai@ file.
  -> TCM (Recompile GHCModuleEnv GHCModule)
                 -- ^ Could we confirm the existence of a main function?
ghcPreModule :: GHCEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> TCM (Recompile GHCModuleEnv GHCModule)
ghcPreModule GHCEnv
cenv IsMain
isMain TopLevelModuleName
m Maybe [Char]
mifile =
  (do let check :: ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
check = ReaderT GHCModuleEnv TCM Bool
-> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
-> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
-> ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM ReaderT GHCModuleEnv TCM Bool
uptodate ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
forall {menv}. ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
noComp ReaderT GHCModuleEnv TCM (Recompile GHCModuleEnv GHCModule)
yesComp
      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 (TopLevelModuleName -> Bool -> HsModuleEnv
HsModuleEnv TopLevelModuleName
m (IsMain
isMain IsMain -> IsMain -> Bool
forall a. Eq a => a -> a -> Bool
== IsMain
IsMain))
  where
    uptodate :: ReaderT GHCModuleEnv TCM Bool
uptodate = case Maybe [Char]
mifile of
      Maybe [Char]
Nothing -> Bool -> ReaderT GHCModuleEnv TCM Bool
forall a. a -> ReaderT GHCModuleEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      Just [Char]
ifile -> IO Bool -> ReaderT GHCModuleEnv TCM Bool
forall a. IO a -> ReaderT GHCModuleEnv TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> ReaderT GHCModuleEnv TCM Bool)
-> ReaderT GHCModuleEnv TCM (IO Bool)
-> ReaderT GHCModuleEnv TCM Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [Char] -> [Char] -> IO Bool
isNewerThan ([Char] -> [Char] -> IO Bool)
-> ReaderT GHCModuleEnv TCM [Char]
-> ReaderT GHCModuleEnv TCM ([Char] -> IO Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT GHCModuleEnv TCM [Char]
forall (m :: * -> *).
(MonadGHCIO m, ReadGHCModuleEnv m) =>
m [Char]
curOutFile ReaderT GHCModuleEnv TCM ([Char] -> IO Bool)
-> ReaderT GHCModuleEnv TCM [Char]
-> ReaderT GHCModuleEnv TCM (IO Bool)
forall a b.
ReaderT GHCModuleEnv TCM (a -> b)
-> ReaderT GHCModuleEnv TCM a -> ReaderT GHCModuleEnv TCM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Char] -> ReaderT GHCModuleEnv TCM [Char]
forall a. a -> ReaderT GHCModuleEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Char]
ifile
    ifileDesc :: [Char]
ifileDesc = [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
"(memory)" Maybe [Char]
mifile

    noComp :: ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
noComp = do
      [Char] -> Nat -> [Char] -> ReaderT GHCModuleEnv TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"compile.ghc" Nat
2 ([Char] -> ReaderT GHCModuleEnv TCM ())
-> (TopLevelModuleName -> [Char])
-> TopLevelModuleName
-> ReaderT GHCModuleEnv TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        ([Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" : no compilation is needed.") ([Char] -> [Char])
-> (TopLevelModuleName -> [Char]) -> TopLevelModuleName -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (TopLevelModuleName -> ReaderT GHCModuleEnv TCM ())
-> ReaderT GHCModuleEnv TCM TopLevelModuleName
-> ReaderT GHCModuleEnv TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ReaderT GHCModuleEnv TCM TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
      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 a. a -> ReaderT GHCModuleEnv TCM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])
      Recompile menv GHCModule
-> ReaderT GHCModuleEnv TCM (Recompile menv GHCModule)
forall a. a -> ReaderT GHCModuleEnv TCM a
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
      [Char]
m   <- TopLevelModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow (TopLevelModuleName -> [Char])
-> ReaderT GHCModuleEnv TCM TopLevelModuleName
-> ReaderT GHCModuleEnv TCM [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT GHCModuleEnv TCM TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
      [Char]
out <- ReaderT GHCModuleEnv TCM [Char]
forall (m :: * -> *).
(MonadGHCIO m, ReadGHCModuleEnv m) =>
m [Char]
curOutFile
      [Char] -> Nat -> [Char] -> ReaderT GHCModuleEnv TCM ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> [Char] -> m ()
reportSLn [Char]
"compile.ghc" Nat
1 ([Char] -> ReaderT GHCModuleEnv TCM ())
-> [Char] -> ReaderT GHCModuleEnv TCM ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char] -> [Char]
repl [[Char]
m, [Char]
ifileDesc, [Char]
out] [Char]
"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?
  -> TopLevelModuleName
  -> [GHCDefinition]   -- ^ Compiled module content.
  -> TCM GHCModule
ghcPostModule :: GHCEnv
-> GHCModuleEnv
-> IsMain
-> TopLevelModuleName
-> [GHCDefinition]
-> TCM GHCModule
ghcPostModule GHCEnv
_cenv GHCModuleEnv
menv IsMain
_isMain TopLevelModuleName
_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 TopLevelModuleName
usedModules) = [(UsesFloat, [Decl], [Definition], [MainFunctionDef],
  Set TopLevelModuleName)]
-> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
    Set TopLevelModuleName)
forall a. Monoid a => [a] -> a
mconcat ([(UsesFloat, [Decl], [Definition], [MainFunctionDef],
   Set TopLevelModuleName)]
 -> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
     Set TopLevelModuleName))
-> [(UsesFloat, [Decl], [Definition], [MainFunctionDef],
     Set TopLevelModuleName)]
-> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
    Set TopLevelModuleName)
forall a b. (a -> b) -> a -> b
$
        (\(GHCDefinition UsesFloat
useFloat' [Decl]
decls' Definition
def' Maybe MainFunctionDef
md' Set TopLevelModuleName
imps')
         -> (UsesFloat
useFloat', [Decl]
decls', [Definition
def'], Maybe MainFunctionDef -> [MainFunctionDef]
forall a. Maybe a -> [a]
maybeToList Maybe MainFunctionDef
md', Set TopLevelModuleName
imps'))
        (GHCDefinition
 -> (UsesFloat, [Decl], [Definition], [MainFunctionDef],
     Set TopLevelModuleName))
-> [GHCDefinition]
-> [(UsesFloat, [Decl], [Definition], [MainFunctionDef],
     Set TopLevelModuleName)]
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 TopLevelModuleName -> [Definition] -> [ImportDecl]
imports BuiltinThings PrimFun
builtinThings Set TopLevelModuleName
usedModules [Definition]
defs

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

  -- Get content of FOREIGN pragmas.
  let ([[Char]]
headerPragmas, [[Char]]
hsImps, [[Char]]
code) = Interface -> ([[Char]], [[Char]], [[Char]])
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
      (([Char] -> ModulePragma) -> [[Char]] -> [ModulePragma]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> ModulePragma
HS.OtherPragma [[Char]]
headerPragmas)
      [ImportDecl]
imps
      (([Char] -> Decl) -> [[Char]] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map [Char] -> Decl
fakeDecl ([[Char]]
hsImps [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]]
code) [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Decl]
decls)

  GHCModule -> TCM GHCModule
forall a. a -> TCMT IO a
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 TopLevelModuleName
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 a. a -> TCMT IO a
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 TopLevelModuleName
-> 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 TopLevelModuleName
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 TopLevelModuleName -> [Definition] ->
  [HS.ImportDecl]
imports :: BuiltinThings PrimFun
-> Set TopLevelModuleName -> [Definition] -> [ImportDecl]
imports BuiltinThings PrimFun
builtinThings Set TopLevelModuleName
usedModules [Definition]
defs = [ImportDecl]
hsImps [ImportDecl] -> [ImportDecl] -> [ImportDecl]
forall a. [a] -> [a] -> [a]
++ [ImportDecl]
imps where
  hsImps :: [HS.ImportDecl]
  hsImps :: [ImportDecl]
hsImps = [ImportDecl
unqualRTE, ModuleName -> ImportDecl
decl ModuleName
mazRTE]

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

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

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

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

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

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

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

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

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

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

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

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

definition :: Definition -> HsCompileM (UsesFloat, [HS.Decl], Maybe CheckedMainFunctionDef)
-- ignore irrelevant definitions
{- 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
  [Char]
-> Nat
-> TCM Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM Doc -> m ()
reportSDoc [Char]
"compile.ghc.definition" Nat
10 (TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$
    (TCM Doc
"Not compiling" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
"."
  (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
-> HsCompileM (UsesFloat, [Decl], Maybe CheckedMainFunctionDef)
forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UsesFloat
forall a. Monoid a => a
mempty, [Decl]
forall a. Monoid a => a
mempty, Maybe CheckedMainFunctionDef
forall a. Maybe a
Nothing)
definition def :: Definition
def@Defn{defName :: Definition -> QName
defName = QName
q, defType :: Definition -> Type
defType = Type
ty, theDef :: Definition -> Defn
theDef = Defn
d} = do
  [Char]
-> Nat
-> TCM Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM Doc -> m ()
reportSDoc [Char]
"compile.ghc.definition" Nat
10 (TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ (TCM Doc
"Compiling" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":"
    , Nat -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Defn -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Defn
d
    ]
  Maybe HaskellPragma
pragma <- TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q
  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 a. a -> m a
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 [Char]
hs) <- Maybe HaskellPragma
pragma -> Range
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (ReaderT
   GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall a b. (a -> b) -> a -> b
$
          if (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvFlat
          then [Char]
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError
                [Char]
"\"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` [Char] -> Name
HS.Ident [Char]
"_") (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
^. (Bool -> f Bool) -> Defn -> f Defn
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 ([Char] -> Exp
fakeExp [Char]
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  <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinTrue
        Just QName
false <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> [Char] -> Nat -> Decl
compiledTypeSynonym QName
q [Char]
"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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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
$ [Char] -> [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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  <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinNil
        Just QName
cons <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)) ([Char] -> Type
HS.FakeType [Char]
"[]")
                   , [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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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
$ [Char] -> [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"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 <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinNothing
        Just QName
just    <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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)) ([Char] -> Type
HS.FakeType [Char]
"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 <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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 :: [Char]
err = [Char]
"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 -> [Char] -> Nat -> Decl
compiledTypeSynonym QName
q [Char]
"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 ([Char] -> Exp
HS.FakeExp ([Char]
"error " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [Char]
forall a. Show a => a -> [Char]
show [Char]
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 <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinIZero
        Just QName
i1 <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> [Char] -> Nat -> Decl
compiledTypeSynonym QName
q [Char]
"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)]
              ([Char] -> Type
HS.FakeType [Char]
"()")
          , [Match] -> Decl
HS.FunBind
              [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match (QName -> Name
dname QName
q) []
                 (Exp -> Rhs
HS.UnGuardedRhs Exp
HS.unit_con) Maybe Binds
emptyBinds]
          ]

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

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

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

      -- PathP is compiled as a function from the interval (booleans)
      -- to the underlying type.
      Axiom{} | (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvPathP -> do
        ()
_        <- [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval]
        Just QName
int <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
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 ([Char] -> Exp
HS.FakeExp [Char]
"\\_ _ _ _ -> ()"))
                 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 ([Char] -> Exp
HS.FakeExp [Char]
"\\_ _ _ _ -> ()"))
                 Maybe Binds
emptyBinds]
          ]

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

      -- Id x y is compiled as a pair of a boolean and whatever
      -- Path x y is compiled to.
      Datatype{} | (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 <- [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
[Char] -> m (Maybe QName)
getBuiltinName [Char]
builtinInterval
        QName
int      <- NameKind
-> QName -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) QName
xhqn NameKind
TypeK QName
int
        -- re  #3733: implement reflId
        [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)
              [] -- [HS.UnkindedVar (ihname A i) | i <- [0..3]]
              (Type -> Type -> Type
HS.TyApp ([Char] -> Type
HS.FakeType [Char]
"(,) 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 ([Char] -> Exp
HS.FakeExp [Char]
"\\_ _ _ _ -> ()"))
                 Maybe Binds
emptyBinds]
          ]

      -- conid.
      Primitive{} | (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 ([Char] -> Exp
HS.FakeExp [Char]
"(,)")
                            (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 ([Char] -> Exp
HS.FakeExp [Char]
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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 -> [Char] -> Nat -> Decl
compiledTypeSynonym QName
q [Char]
ty Nat
ar | Just (HsType Range
r [Char]
ty) <- [Maybe HaskellPragma
pragma] ] [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++
                   Exp -> [Decl]
fb Exp
axiomErr
      Primitive{ primName :: Defn -> [Char]
primName = [Char]
s } -> (UsesFloat
forall a. Monoid a => a
mempty,) ([Decl] -> (UsesFloat, [Decl]))
-> (Exp -> [Decl]) -> Exp -> (UsesFloat, [Decl])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> [Decl]
fb (Exp -> (UsesFloat, [Decl]))
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCM Exp -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM Exp -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp)
-> ([Char] -> TCM Exp)
-> [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> TCM Exp
forall (m :: * -> *). MonadTCError m => [Char] -> m Exp
primBody) [Char]
s

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

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

      Datatype{ dataPars :: Defn -> Nat
dataPars = Nat
np, dataIxs :: Defn -> Nat
dataIxs = Nat
ni, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl
              , dataPathCons :: Defn -> [QName]
dataPathCons = [QName]
pcs
              } | Just hsdata :: HaskellPragma
hsdata@(HsData Range
r [Char]
ty [[Char]]
hsCons) <- Maybe HaskellPragma
pragma ->
        Range
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (ReaderT
   GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall a b. (a -> b) -> a -> b
$ do
        [Char]
-> Nat
-> TCM Doc
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Nat -> TCM Doc -> m ()
reportSDoc [Char]
"compile.ghc.definition" Nat
40 (TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> TCM Doc -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
hsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          [ TCM Doc
"Compiling data type with COMPILE pragma ...", HaskellPragma -> TCM Doc
forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty HaskellPragma
hsdata ]
        TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [QName]
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName])
-> TCM [QName]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [QName]
getNotErasedConstructors QName
q
        [Decl]
ccscov <- QName
-> Nat
-> [QName]
-> [Char]
-> [[Char]]
-> 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 [Char]
ty [[Char]]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> [Char] -> Nat -> Decl
compiledTypeSynonym QName
q [Char]
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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM [QName]
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName])
-> TCM [QName]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [QName]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [QName]
getNotErasedConstructors QName
q
        [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 [Char]
ty [[Char]]
hsCons) -> Range
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (ReaderT
   GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall a b. (a -> b) -> a -> b
$ do
            let cs :: [QName]
cs = [ConHead -> QName
conName ConHead
con]
            TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (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]
-> [Char]
-> [[Char]]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
constructorCoverageCode QName
q Nat
np [QName]
cs [Char]
ty [[Char]]
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 -> [Char] -> Nat -> Decl
compiledTypeSynonym QName
q [Char]
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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 [Char]
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 [Char]
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError
              [Char]
"\"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 [[Char] -> Name
HS.Ident [Char]
name] Type
t

              def :: HS.Decl
              def :: Decl
def = [Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match ([Char] -> Name
HS.Ident [Char]
name) [] (Exp -> Rhs
HS.UnGuardedRhs (Exp -> Exp
hsCoerce (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
hsVarUQ (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ QName -> Name
dname QName
q)) Maybe Binds
emptyBinds]
          (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UsesFloat
imp, [Decl
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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UsesFloat
imp, [Decl]
ccls)

  functionViaTreeless :: QName -> HsCompileM (UsesFloat, [HS.Decl])
  functionViaTreeless :: QName
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
functionViaTreeless QName
q = do
    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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 a. Eq a => a -> [a] -> 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 -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projIndex :: Projection -> Nat
projIndex = Nat
i } } | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
0 -> Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
                   Defn
_ -> Nat
0
          argTypes :: [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 a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
HS.TyFun Type
t t Type
ts)
          funbind :: Name -> [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 a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Pat]
ps Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- [Type] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Type]
ts) Type
mazAnyType)
            in [Name -> [Type] -> Type -> Decl
forall {t :: * -> *}. Foldable t => Name -> t Type -> Type -> Decl
tydecl Name
f [Type]
ts' Type
t, Name -> [Pat] -> Exp -> Decl
funbind Name
f [Pat]
ps Exp
b]

      -- The definition of the non-stripped function
      ([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 a b. (a -> b -> b) -> b -> [a] -> b
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 a. [a] -> 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 b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
HS.App (Name -> Exp
hsVarUQ (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ QName -> Name
duname QName
q) [ Name -> Exp
hsVarUQ Name
x | (~(HS.PVar Name
x), ArgUsage
ArgUsed) <- [Pat] -> [ArgUsage] -> [(Pat, ArgUsage)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Pat]
ps0 [ArgUsage]
used ]
          ps0' :: [Pat]
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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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
$ [Char] -> Text
Text.pack ([Char] -> Text) -> [Char] -> Text
forall a b. (a -> b) -> a -> b
$ [Char]
"postulate evaluated: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q

constructorCoverageCode :: QName -> Int -> [QName] -> HaskellType -> [HaskellCode] -> HsCompileM [HS.Decl]
constructorCoverageCode :: QName
-> Nat
-> [QName]
-> [Char]
-> [[Char]]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
constructorCoverageCode QName
q Nat
np [QName]
cs [Char]
hsTy [[Char]]
hsCons = do
  TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> TCM () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> [[Char]] -> TCM ()
checkConstructorCount QName
q [QName]
cs [[Char]]
hsCons
  ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (TCM Bool -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return []) (ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall a b. (a -> b) -> a -> b
$ do
    [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
 -> [Char]
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
-> [QName]
-> [[Char]]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [[Decl]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM QName
-> [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
checkConstructorType [QName]
cs [[Char]]
hsCons
    [Decl]
cov <- TCM [Decl]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 -> [Char] -> Nat -> [QName] -> [[Char]] -> TCM [Decl]
forall (m :: * -> *).
HasConstInfo m =>
QName -> [Char] -> Nat -> [QName] -> [[Char]] -> m [Decl]
checkCover QName
q [Char]
hsTy Nat
np [QName]
cs [[Char]]
hsCons
    [Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([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 (m :: * -> *) a. Monad m => m a -> ReaderT CCEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (WriterT UsesFloat (HsCompileT m) a
 -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a)
-> (HsCompileT m a -> WriterT UsesFloat (HsCompileT m) a)
-> HsCompileT m a
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HsCompileT m a -> WriterT UsesFloat (HsCompileT m) a
forall (m :: * -> *) a. Monad m => m a -> WriterT UsesFloat m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

freshNames :: Monad m => Int -> ([HS.Name] -> CCT m a) -> CCT m a
freshNames :: forall (m :: * -> *) a.
Monad m =>
Nat -> ([Name] -> CCT m a) -> CCT m a
freshNames Nat
n [Name] -> CCT m a
_ | Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
0 = CCT m a
forall a. HasCallStack => a
__IMPOSSIBLE__
freshNames Nat
n [Name] -> CCT m a
cont = do
  ([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 ([Name] -> f [Name]) -> CCEnv -> f CCEnv
Lens' [Name] CCEnv
ccNameSupply
  (CCEnv -> CCEnv) -> CCT m a -> CCT m a
forall a.
(CCEnv -> CCEnv)
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Lens' [Name] CCEnv -> LensMap [Name] CCEnv
forall i o. Lens' i o -> LensMap i o
over ([Name] -> f [Name]) -> CCEnv -> f CCEnv
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 a.
(CCEnv -> CCEnv)
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
-> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (Lens' [Name] CCEnv -> LensMap [Name] CCEnv
forall i o. Lens' i o -> LensMap i o
over ([Name] -> f [Name]) -> CCEnv -> f CCEnv
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
-> [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
checkConstructorType QName
q [Char]
hs = do
  Type
ty <- QName -> HsCompileM Type
haskellType QName
q
  [Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [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
$ [Char] -> Exp
fakeExp [Char]
hs) Maybe Binds
emptyBinds]
         ]

checkCover :: HasConstInfo m => QName -> HaskellType -> Nat -> [QName] -> [HaskellCode] -> m [HS.Decl]
checkCover :: forall (m :: * -> *).
HasConstInfo m =>
QName -> [Char] -> Nat -> [QName] -> [[Char]] -> m [Decl]
checkCover QName
q [Char]
ty Nat
n [QName]
cs [[Char]]
hsCons = do
  let tvs :: [[Char]]
tvs = [ [Char]
"a" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Nat -> [Char]
forall a. Show a => a -> [Char]
show Nat
i | Nat
i <- [Nat
1..Nat
n] ]
      makeClause :: QName -> [Char] -> m Alt
makeClause QName
c [Char]
hsc = do
        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
$ [Char] -> Name
HS.Ident [Char]
hsc) ([Pat] -> Pat) -> [Pat] -> Pat
forall a b. (a -> b) -> a -> b
$ Nat -> Pat -> [Pat]
forall a. Nat -> a -> [a]
replicate Nat
a Pat
HS.PWildCard
        Alt -> m Alt
forall a. a -> m a
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 -> [Char] -> m Alt) -> [QName] -> [[Char]] -> m [Alt]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM QName -> [Char] -> m Alt
forall {m :: * -> *}. HasConstInfo m => QName -> [Char] -> m Alt
makeClause [QName]
cs [[Char]]
hsCons
  let rhs :: Exp
rhs = Exp -> [Alt] -> Exp
HS.Case (QName -> Exp
HS.Var (QName -> Exp) -> QName -> Exp
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ [Char] -> Name
HS.Ident [Char]
"x") [Alt]
cs

  [Decl] -> m [Decl]
forall a. a -> m a
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
$ [Char] -> Type
fakeType ([Char] -> Type) -> [Char] -> Type
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unwords ([Char]
ty [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: [[Char]]
tvs) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" -> ()"
         , [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
$ [Char] -> Name
HS.Ident [Char]
"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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM TTerm
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) TTerm)
-> TCM TTerm
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> TCM TTerm
forall (m :: * -> *). HasConstInfo m => TTerm -> m TTerm
addCoercions TTerm
v
  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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
mkIf TTerm
t = TTerm -> CC TTerm
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t

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

    (T.TDef QName
f, [TTerm]
ts) -> do
      [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 a.
TCM a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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 a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [TTerm]
ts
          needed :: Nat
needed  = [ArgUsage] -> Nat
forall a. [a] -> 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 a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ArgUsage]
used
        then if ArgUsage
ArgUnused ArgUsage -> [ArgUsage] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ArgUsage]
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 a. [a] -> 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 a. [a] -> 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 a. [a] -> 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 a b.
ReaderT
  CCEnv
  (WriterT
     UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
  a
-> (a
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         b)
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ Exp
t' -> Exp -> Exp
coe Exp
t' Exp -> [TTerm] -> CC Exp
`apps` [TTerm]
ts
  where
  apps :: Exp -> [TTerm] -> CC Exp
apps = (Exp -> TTerm -> CC Exp) -> Exp -> [TTerm] -> CC Exp
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\ Exp
h TTerm
a -> Exp -> Exp -> Exp
HS.App Exp
h (Exp -> Exp) -> CC Exp -> CC Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> CC Exp
term TTerm
a)
  etaExpand :: Nat -> TTerm -> TTerm
etaExpand Nat
n TTerm
t = Nat -> TTerm -> TTerm
mkTLam Nat
n (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ Nat -> TTerm -> TTerm
forall a. Subst a => Nat -> a -> a
raise Nat
n TTerm
t TTerm -> [TTerm] -> TTerm
`T.mkTApp` (Nat -> TTerm) -> [Nat] -> [TTerm]
forall a b. (a -> b) -> [a] -> [b]
map Nat -> TTerm
T.TVar (Nat -> [Nat]
forall a. Integral a => a -> [a]
downFrom Nat
n)

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

  T.TVar Nat
i    -> Name -> Exp
hsVarUQ (Name -> Exp) -> ([Name] -> Name) -> [Name] -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Name] -> Name
lookupIndex Nat
i ([Name] -> Exp)
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     [Name]
-> CC Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' [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 ([Name] -> f [Name]) -> CCEnv -> f CCEnv
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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ TPrim -> Exp
compilePrim TPrim
p
  TTerm
T.TUnit     -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Exp
HS.unit_con
  TTerm
T.TSort     -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Exp
HS.unit_con
  TTerm
T.TErased   -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
hsVarUQ (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Name
HS.Ident [Char]
mazErasedName
  T.TError TError
e  -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ case TError
e of
    TError
T.TUnreachable -> Exp
rtmUnreachableError
    T.TMeta [Char]
s      -> [Char] -> Exp
rtmHole [Char]
s

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

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

alt :: Int -> T.TAlt -> CC HS.Alt
alt :: Nat
-> TAlt
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
alt Nat
sc TAlt
a = do
  case TAlt
a of
    T.TACon {aCon :: TAlt -> QName
T.aCon = QName
c} -> do
      Nat
-> ([Name]
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt)
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
forall (m :: * -> *) a.
Monad m =>
Nat -> ([Name] -> CCT m a) -> CCT m a
intros (TAlt -> Nat
T.aArity TAlt
a) (([Name]
  -> ReaderT
       CCEnv
       (WriterT
          UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
       Alt)
 -> ReaderT
      CCEnv
      (WriterT
         UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
      Alt)
-> ([Name]
    -> ReaderT
         CCEnv
         (WriterT
            UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
         Alt)
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
forall a b. (a -> b) -> a -> b
$ \ [Name]
xs -> do
        [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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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
$ [Char] -> Name
HS.Ident [Char]
"[]"
             | 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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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
$ [Char] -> Name
HS.Symbol [Char]
":"
             | 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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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 = LitMeta TopLevelModuleName
_ MetaId
m } -> Pat
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
mkAlt (MetaId -> Pat
litmetapat MetaId
m)
    T.TALit { aLit :: TAlt -> Literal
T.aLit = l :: Literal
l@LitFloat{}, aBody :: TAlt -> TTerm
T.aBody = TTerm
b } -> do
      UsesFloat
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell UsesFloat
YesFloat
      Exp
l <- Literal -> CC Exp
forall (m :: * -> *). Monad m => Literal -> CCT m Exp
literal Literal
l
      [Char]
-> Exp
-> TTerm
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
mkGuarded (TPrim -> [Char]
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 } -> [Char]
-> Exp
-> TTerm
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
mkGuarded [Char]
"(==)" (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 :: [Char]
-> Exp
-> TTerm
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
mkGuarded [Char]
eq Exp
lit TTerm
b = do
      Exp
b  <- TTerm -> CC Exp
term TTerm
b
      let varName :: Name
varName = [Char] -> Name
HS.Ident [Char]
"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 ([Char] -> Name
HS.Ident [Char]
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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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 a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
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 a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp
typed [Char]
"Integer"
  LitWord64 Word64
_   -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp
typed [Char]
"MAlonzo.RTE.Word64"
  LitFloat  Double
x   -> Double -> [Char] -> CCT m Exp
floatExp Double
x [Char]
"Double"
  LitQName  QName
x   -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ QName -> Exp
litqname QName
x
  LitString Text
s   -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ Text -> Exp
litString Text
s
  LitMeta TopLevelModuleName
_ MetaId
m   ->
    Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp
HS.FakeExp [Char]
"(,)" Exp -> Exp -> Exp
`HS.App`
             Word64 -> Exp
forall a. Integral a => a -> Exp
hsTypedInt (MetaId -> Word64
metaId MetaId
m) Exp -> Exp -> Exp
`HS.App`
             (Word64 -> Exp
forall a. Integral a => a -> Exp
hsTypedInt (ModuleNameHash -> Word64
moduleNameHash (ModuleNameHash -> Word64) -> ModuleNameHash -> Word64
forall a b. (a -> b) -> a -> b
$ MetaId -> ModuleNameHash
metaModule MetaId
m))
  Literal
_             -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ Exp
l'
  where
    l' :: Exp
l'    = Literal -> Exp
HS.Lit (Literal -> Exp) -> Literal -> Exp
forall a b. (a -> b) -> a -> b
$ Literal -> Literal
hslit Literal
l
    typed :: [Char] -> Exp
typed = Exp -> Type -> Exp
HS.ExpTypeSig Exp
l' (Type -> Exp) -> ([Char] -> Type) -> [Char] -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Type
HS.TyCon (QName -> Type) -> ([Char] -> QName) -> [Char] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> QName
rtmQual

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

hslit :: Literal -> HS.Literal
hslit :: Literal -> Literal
hslit = \case
  LitNat    Integer
x -> Integer -> Literal
HS.Int    Integer
x
  LitWord64 Word64
x -> Integer -> Literal
HS.Int    (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
x)
  LitFloat  Double
x -> Rational -> Literal
HS.Frac   (Double -> Rational
forall a. Real a => a -> Rational
toRational Double
x)
  LitChar   Char
x -> Char -> Literal
HS.Char   Char
x
  LitQName  QName
x -> Literal
forall a. HasCallStack => a
__IMPOSSIBLE__
  LitString 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 ([Char] -> ModuleName
HS.ModuleName [Char]
"Data.Text") ([Char] -> Name
HS.Ident [Char]
"Text")))

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

    litAssoc :: Associativity -> Exp
litAssoc Associativity
NonAssoc   = [Char] -> Exp
rteCon [Char]
"NonAssoc"
    litAssoc Associativity
LeftAssoc  = [Char] -> Exp
rteCon [Char]
"LeftAssoc"
    litAssoc Associativity
RightAssoc = [Char] -> Exp
rteCon [Char]
"RightAssoc"

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

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

litmetapat :: MetaId -> HS.Pat
litmetapat :: MetaId -> Pat
litmetapat (MetaId Word64
m ModuleNameHash
h) =
  QName -> [Pat] -> Pat
HS.PApp ([Char] -> QName
hsName [Char]
"(,)")
          [ Literal -> Pat
HS.PLit (Integer -> Literal
HS.Int (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
m)
          , Literal -> Pat
HS.PLit (Integer -> Literal
HS.Int (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Integer) -> Word64 -> Integer
forall a b. (a -> b) -> a -> b
$ ModuleNameHash -> Word64
moduleNameHash ModuleNameHash
h) ]

condecl :: QName -> Induction -> HsCompileM HS.ConDecl
condecl :: QName
-> Induction
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ConDecl
condecl QName
q Induction
_ind = do
  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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return Nat
ar
  [Char]
hsCon <- [Char] -> Maybe [Char] -> [Char]
forall a. a -> Maybe a -> a
fromMaybe [Char]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Char] -> [Char])
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe [Char])
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe [Char])
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 a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
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 ([Char] -> QName
hsName [Char]
hsCon) [Pat]
patVars)

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

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

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

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

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

type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)

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

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

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

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

callGHC :: ReaderT GHCModule TCM ()
callGHC :: ReaderT GHCModule TCM ()
callGHC = do
  GHCOptions
opts     <- ReaderT GHCModule TCM GHCOptions
forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  CommandLineOptions
agdaOpts <- TCM CommandLineOptions -> ReaderT GHCModule TCM CommandLineOptions
forall (m :: * -> *) a. Monad m => m a -> ReaderT GHCModule m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  [Char]
hsmod    <- ModuleName -> [Char]
forall a. Pretty a => a -> [Char]
prettyPrint (ModuleName -> [Char])
-> ReaderT GHCModule TCM ModuleName -> ReaderT GHCModule TCM [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT GHCModule TCM ModuleName
forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
curHsMod
  TopLevelModuleName
agdaMod  <- ReaderT GHCModule TCM TopLevelModuleName
forall (m :: * -> *). ReadGHCModuleEnv m => m TopLevelModuleName
curAgdaMod
  let outputName :: [Char]
outputName = Text -> [Char]
Text.unpack (Text -> [Char]) -> Text -> [Char]
forall a b. (a -> b) -> a -> b
$ NonEmpty Text -> Text
forall a. NonEmpty a -> a
List1.last (NonEmpty Text -> Text) -> NonEmpty Text -> Text
forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> NonEmpty Text
moduleNameParts TopLevelModuleName
agdaMod
  ([Char]
mdir, [Char]
fp) <- ReaderT GHCModule TCM ([Char], [Char])
forall (m :: * -> *).
(MonadGHCIO m, ReadGHCModuleEnv m) =>
m ([Char], [Char])
curOutFileAndDir
  let ghcopts :: [[Char]]
ghcopts = GHCOptions -> [[Char]]
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 a. [a] -> 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 ([Char] -> [ReaderT GHCModule TCM Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"No main function defined in" [ReaderT GHCModule TCM Doc]
-> [ReaderT GHCModule TCM Doc] -> [ReaderT GHCModule TCM Doc]
forall a. [a] -> [a] -> [a]
++ [TopLevelModuleName -> ReaderT GHCModule TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => TopLevelModuleName -> m Doc
prettyTCM TopLevelModuleName
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]
++
                             [Char] -> [ReaderT GHCModule TCM Doc]
forall (m :: * -> *). Applicative m => [Char] -> [m Doc]
pwords [Char]
"Use --no-main to suppress this warning.")

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

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

  -- Make GHC use UTF-8 when writing to stdout and stderr.
  IO () -> ReaderT GHCModule TCM ()
forall a. IO a -> ReaderT GHCModule TCM a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ReaderT GHCModule TCM ())
-> IO () -> ReaderT GHCModule TCM ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> IO ()
setEnv [Char]
"GHC_CHARENC" [Char]
"UTF-8"
  -- Note: Some versions of GHC use stderr for progress reports. For
  -- those versions of GHC we don't print any progress information
  -- unless an error is encountered.
  let doCall :: Bool
doCall = GHCOptions -> Bool
optGhcCallGhc GHCOptions
opts
      cwd :: Maybe [Char]
cwd    = if CommandLineOptions -> Bool
optGHCiInteraction CommandLineOptions
agdaOpts Bool -> Bool -> Bool
||
                  CommandLineOptions -> Bool
optJSONInteraction CommandLineOptions
agdaOpts
               then [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
mdir
               else Maybe [Char]
forall a. Maybe a
Nothing
  TCM () -> ReaderT GHCModule TCM ()
forall a. TCM a -> ReaderT GHCModule TCM a
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
-> [Char]
-> [[Char]]
-> Maybe [Char]
-> Maybe TextEncoding
-> TCM ()
callCompiler Bool
doCall [Char]
ghcBin [[Char]]
args Maybe [Char]
cwd (TextEncoding -> Maybe TextEncoding
forall a. a -> Maybe a
Just TextEncoding
utf8)