module Agda.Compiler.MAlonzo.Compiler
  ( ghcBackend
  , ghcInvocationStrings
  )
  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.Options

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty (prettyShow, render)
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Names (namesIn)
import qualified Agda.Syntax.Treeless as T
import Agda.Syntax.Literal
import Agda.Syntax.TopLevelModuleName

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

import Paths_Agda

import Agda.Utils.Impossible

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

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

ghcBackend' :: Backend' GHCFlags GHCEnv GHCModuleEnv GHCModule GHCDefinition
ghcBackend' :: Backend'_boot
  TCM 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 -> TCMT IO GHCEnv
preCompile            = GHCFlags -> TCMT IO GHCEnv
ghcPreCompile
  , postCompile :: GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCMT IO ()
postCompile           = GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCMT IO ()
ghcPostCompile
  , preModule :: GHCEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> TCMT IO (Recompile GHCModuleEnv GHCModule)
preModule             = GHCEnv
-> IsMain
-> TopLevelModuleName
-> Maybe [Char]
-> TCMT IO (Recompile GHCModuleEnv GHCModule)
ghcPreModule
  , postModule :: GHCEnv
-> GHCModuleEnv
-> IsMain
-> TopLevelModuleName
-> [GHCDefinition]
-> TCMT IO GHCModule
postModule            = GHCEnv
-> GHCModuleEnv
-> IsMain
-> TopLevelModuleName
-> [GHCDefinition]
-> TCMT IO GHCModule
ghcPostModule
  , compileDef :: GHCEnv
-> GHCModuleEnv -> IsMain -> Definition -> TCMT IO GHCDefinition
compileDef            = GHCEnv
-> GHCModuleEnv -> IsMain -> Definition -> TCMT IO GHCDefinition
ghcCompileDef
  , scopeCheckingSuffices :: Bool
scopeCheckingSuffices = Bool
False
  , mayEraseType :: QName -> TCMT IO Bool
mayEraseType          = QName -> TCMT IO Bool
ghcMayEraseType
  }

--- Command-line flags ---

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

instance NFData GHCFlags

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

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

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

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

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

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

--- Context types ---

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

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

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

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

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

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

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

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

--- Top-level compilation ---

ghcPreCompile :: GHCFlags -> TCM GHCEnv
ghcPreCompile :: GHCFlags -> TCMT IO GHCEnv
ghcPreCompile GHCFlags
flags = do
  cubical <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
  let 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 cubical of
    Maybe Cubical
Nothing      -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CErased -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CFull   -> [Char] -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
[Char] -> m a
notSupported [Char]
"--cubical"

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

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

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

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

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

ghcPostCompile ::
  GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCM ()
ghcPostCompile :: GHCEnv -> IsMain -> Map TopLevelModuleName GHCModule -> TCMT IO ()
ghcPostCompile GHCEnv
_cenv IsMain
_isMain Map TopLevelModuleName GHCModule
mods = do
  -- FIXME: @curMName@ and @curIF@ are evil TCM state, but there does not appear to be
  --------- another way to retrieve the compilation root ("main" module or interaction focused).
  rootModuleName <- TCMT IO TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
  rootModule <- ifJust (Map.lookup rootModuleName mods) pure
                $ genericError $ "Module " <> prettyShow rootModuleName <> " was not compiled!"
  flip runReaderT rootModule $ do
    copyRTEModules
    callGHC

--- Module compilation ---

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

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

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

ghcPostModule
  :: GHCEnv
  -> GHCModuleEnv
  -> IsMain        -- ^ Are we looking at the main module?
  -> TopLevelModuleName
  -> [GHCDefinition]   -- ^ Compiled module content.
  -> TCM GHCModule
ghcPostModule :: GHCEnv
-> GHCModuleEnv
-> IsMain
-> TopLevelModuleName
-> [GHCDefinition]
-> TCMT IO GHCModule
ghcPostModule GHCEnv
_cenv GHCModuleEnv
menv IsMain
_isMain TopLevelModuleName
_moduleName [GHCDefinition]
ghcDefs = do
  builtinThings <- (TCState -> BuiltinThings 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 (usedFloat, decls, defs, mainDefs, usedModules) = mconcat $
        (\(GHCDefinition UsesFloat
useFloat' [Decl]
decls' Definition
def' Maybe MainFunctionDef
md' Set TopLevelModuleName
imps')
         -> (UsesFloat
useFloat', [Decl]
decls', [Definition
def'], Maybe MainFunctionDef -> [MainFunctionDef]
forall a. Maybe a -> [a]
maybeToList Maybe MainFunctionDef
md', Set TopLevelModuleName
imps'))
        <$> ghcDefs

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

  i <- curIF

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

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

  return $ GHCModule menv mainDefs

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

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

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

imports ::
  BuiltinThings 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 = (NonEmpty ModuleName -> ModuleName)
-> [NonEmpty ModuleName] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
List.map NonEmpty ModuleName -> ModuleName
forall a. NonEmpty a -> a
List1.head ([NonEmpty ModuleName] -> [ModuleName])
-> ([ModuleName] -> [NonEmpty ModuleName])
-> [ModuleName]
-> [ModuleName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ModuleName] -> [NonEmpty ModuleName]
forall (f :: * -> *) a. (Foldable f, Eq a) => f a -> [NonEmpty a]
List1.group ([ModuleName] -> [NonEmpty ModuleName])
-> ([ModuleName] -> [ModuleName])
-> [ModuleName]
-> [NonEmpty ModuleName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ModuleName] -> [ModuleName]
forall a. Ord a => [a] -> [a]
List.sort

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

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

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

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

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

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

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

definition :: Definition -> HsCompileM (UsesFloat, [HS.Decl], Maybe CheckedMainFunctionDef)
-- ignore irrelevant definitions
{- 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
    ]
  pragma <- TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCM (Maybe HaskellPragma)
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma))
-> TCM (Maybe HaskellPragma)
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (Maybe HaskellPragma)
forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q
  env <- askGHCEnv
  let is GHCEnv -> Maybe QName
p = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
p GHCEnv
env
  typeCheckedMainDef <- checkTypeOfMain def
  let mainDecl = Maybe Decl -> [Decl]
forall a. Maybe a -> [a]
maybeToList (Maybe Decl -> [Decl]) -> Maybe Decl -> [Decl]
forall a b. (a -> b) -> a -> b
$ CheckedMainFunctionDef -> Decl
checkedMainDecl (CheckedMainFunctionDef -> Decl)
-> Maybe CheckedMainFunctionDef -> Maybe Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CheckedMainFunctionDef
typeCheckedMainDef
  let retDecls b
ds = (a, b) -> m (a, b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
forall a. Monoid a => a
mempty, b
ds)
  (uncurry (,,typeCheckedMainDef)) . second ((mainDecl ++) . infodecl q) <$>
    case d of

      Defn
_ | Just (HsDefn Range
r [Char]
hs) <- Maybe HaskellPragma
pragma -> Range
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (ReaderT
   GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
 -> ReaderT
      GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl]))
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
forall a b. (a -> b) -> a -> b
$
          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.
            hsty <- QName -> HsCompileM Type
haskellType QName
q
            mapM_ (`xqual` HS.Ident "_") (namesIn ty :: Set QName)

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

            retDecls $ fbWithType hsty (fakeExp hs)

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

      -- Compiling List
      Datatype{ dataPars :: Defn -> Nat
dataPars = Nat
np } | (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvList -> do
        [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil, ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons] -- Just to get the proper error for missing NIL/CONS
        Maybe HaskellPragma
-> (HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe HaskellPragma
pragma ((HaskellPragma
  -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> (HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ \ HaskellPragma
p -> HaskellPragma
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange HaskellPragma
p (ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
PragmaCompileList
        let d :: Name
d = QName -> Name
dname QName
q
            t :: Name
t = NameKind -> QName -> Name
unqhname NameKind
TypeK QName
q
        Just nil  <- BuiltinId
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinNil
        Just cons <- getBuiltinName builtinCons
        let vars Name -> b
f Nat
n = (Nat -> b) -> [Nat] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> b
f (Name -> b) -> (Nat -> Name) -> Nat -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VariableKind -> Nat -> Name
ihname VariableKind
A) [Nat
0 .. Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
        cs <- mapM (compiledcondecl Nothing) [nil, cons]
        retDecls $ [ HS.TypeDecl t (vars HS.UnkindedVar (np - 1)) (HS.FakeType "[]")
                   , HS.FunBind [HS.Match d (vars HS.PVar np) (HS.UnGuardedRhs HS.unit_con) emptyBinds] ] ++
                   cs

      -- Compiling Maybe
      Datatype{ dataPars :: Defn -> Nat
dataPars = Nat
np } | (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvMaybe -> do
        [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing, ReaderT GHCModuleEnv (StateT HsCompileState TCM) Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust] -- Just to get the proper error for missing NOTHING/JUST
        Maybe HaskellPragma
-> (HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *) a. Monad m => Maybe a -> (a -> m ()) -> m ()
whenJust Maybe HaskellPragma
pragma ((HaskellPragma
  -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> (HaskellPragma
    -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ \ HaskellPragma
p -> HaskellPragma
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange HaskellPragma
p (ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ Warning -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning Warning
PragmaCompileMaybe
        let d :: Name
d = QName -> Name
dname QName
q
            t :: Name
t = NameKind -> QName -> Name
unqhname NameKind
TypeK QName
q
        Just nothing <- BuiltinId
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinNothing
        Just just    <- getBuiltinName builtinJust
        let vars Name -> b
f Nat
n = (Nat -> b) -> [Nat] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> b
f (Name -> b) -> (Nat -> Name) -> Nat -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VariableKind -> Nat -> Name
ihname VariableKind
A) [Nat
0 .. Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
        cs <- mapM (compiledcondecl Nothing) [nothing, just]
        retDecls $ [ HS.TypeDecl t (vars HS.UnkindedVar (np - 1)) (HS.FakeType "Maybe")
                   , HS.FunBind [HS.Match d (vars HS.PVar np) (HS.UnGuardedRhs HS.unit_con) emptyBinds] ] ++
                   cs

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

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

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

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

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

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

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

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

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

      -- 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 int <- BuiltinId
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinInterval
        int      <- xhqn TypeK int
        -- re  #3733: implement reflId
        retDecls $
          [ HS.TypeDecl (unqhname TypeK q)
              [] -- [HS.UnkindedVar (ihname A i) | i <- [0..3]]
              (HS.TyApp (HS.FakeType "(,) Bool")
                 (HS.TyFun (HS.TyCon int) mazAnyType))
          , HS.FunBind
              [HS.Match (dname q) []
                 (HS.UnGuardedRhs (HS.FakeExp "\\_ _ _ _ -> ()"))
                 emptyBinds]
          ]

      -- conid.
      Primitive{} | (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvConId -> do
        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 = Bool -> (Pat -> Pat) -> Pat -> Pat
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyWhen Bool
strict Pat -> Pat
HS.PBangPat (Pat -> Pat) -> (Name -> Pat) -> Name -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Pat
HS.PVar
        retDecls $
          [ HS.FunBind
              [HS.Match (dname q)
                 [ var (ihname A i) | i <- [0..1] ]
                 (HS.UnGuardedRhs $
                  HS.App (HS.App (HS.FakeExp "(,)")
                            (HS.Var (HS.UnQual (ihname A 0))))
                    (HS.Var (HS.UnQual (ihname A 1))))
                 emptyBinds]
          ]

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

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

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

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

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

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

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

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

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

      -- Compute the type approximation
      def <- getConstInfo q
      (argTypes0, resType) <- hsTelApproximation $ defType def
      let pars = case Definition -> Defn
theDef Definition
def of
                   Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projIndex :: Projection -> Nat
projIndex = Nat
i } } | Nat
i Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
> Nat
0 -> Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1
                   Defn
_ -> Nat
0
          argTypes  = Nat -> [Type] -> [Type]
forall a. Nat -> [a] -> [a]
drop Nat
pars [Type]
argTypes0
          argTypesS = [ArgUsage] -> [Type] -> [Type]
forall a. [ArgUsage] -> [a] -> [a]
filterUsed [ArgUsage]
used [Type]
argTypes

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

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

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

      return (useFloat,
              if dostrip
                then tyfunbind (dname q) argTypes resType ps0' b0 ++
                     tyfunbind (duname q) argTypesS resType ps b
                else tyfunbind (dname q) argTypes resType ps b)

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

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

  axiomErr :: HS.Exp
  axiomErr :: Exp
axiomErr = 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
  TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO () -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ())
-> TCMT IO ()
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) ()
forall a b. (a -> b) -> a -> b
$ QName -> [QName] -> [[Char]] -> TCMT IO ()
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 (TCMT IO Bool
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
forall a.
TCM a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM (TCMT IO Bool
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool)
-> TCMT IO Bool
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) Bool
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Bool
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
QName -> m Bool
noCheckCover QName
q) ([Decl] -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall a. a -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) a
forall (m :: * -> *) a. Monad m => a -> m a
return []) (ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall a b. (a -> b) -> a -> b
$ do
    ccs <- [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat ([[Decl]] -> [Decl])
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [[Decl]]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (QName
 -> [Char]
 -> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl])
-> [QName]
-> [[Char]]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [[Decl]]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM QName
-> [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
checkConstructorType [QName]
cs [[Char]]
hsCons
    cov <- liftTCM $ checkCover q hsTy np cs hsCons
    return $ ccs ++ cov

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

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

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

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

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

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

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

-- | Constructor coverage monad
type CC = CCT TCM

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

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

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

checkConstructorType :: QName -> HaskellCode -> HsCompileM [HS.Decl]
checkConstructorType :: QName
-> [Char]
-> ReaderT GHCModuleEnv (StateT HsCompileState TCM) [Decl]
checkConstructorType QName
q [Char]
hs = do
  ty <- QName -> HsCompileM Type
haskellType QName
q
  return [ HS.TypeSig [unqhname CheckK q] ty
         , HS.FunBind [HS.Match (unqhname CheckK q) []
                                (HS.UnGuardedRhs $ fakeExp hs) emptyBinds]
         ]

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

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

  return [ HS.TypeSig [unqhname CoverK q] $ fakeType $ unwords (ty : tvs) ++ " -> ()"
         , HS.FunBind [HS.Match (unqhname CoverK q) [HS.PVar $ HS.Ident "x"]
                                (HS.UnGuardedRhs rhs) emptyBinds]
         ]

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

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

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

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

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

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

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

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

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

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

  T.TCase Nat
sc CaseInfo
ct TTerm
def [TAlt]
alts -> do
    sc'   <- TTerm -> CC Exp
term (TTerm -> CC Exp) -> TTerm -> CC Exp
forall a b. (a -> b) -> a -> b
$ Nat -> TTerm
T.TVar Nat
sc
    alts' <- traverse (alt sc) alts
    def'  <- term def
    let defAlt = Pat -> Rhs -> Maybe Binds -> Alt
HS.Alt Pat
HS.PWildCard (Exp -> Rhs
HS.UnGuardedRhs Exp
def') Maybe Binds
emptyBinds
    return $ HS.Case (hsCoerce sc') (alts' ++ [defAlt])

  T.TLit Literal
l    -> Literal -> CC Exp
forall (m :: * -> *). Monad m => Literal -> CCT m Exp
literal Literal
l
  T.TPrim TPrim
p   -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ TPrim -> Exp
compilePrim TPrim
p
  TTerm
T.TUnit     -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Exp
HS.unit_con
  TTerm
T.TSort     -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Exp
HS.unit_con
  TTerm
T.TErased   -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ Name -> Exp
hsVarUQ (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Name
HS.Ident [Char]
mazErasedName
  T.TError TError
e  -> Exp -> CC Exp
forall a.
a
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CC Exp) -> Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ case TError
e of
    TError
T.TUnreachable -> Exp
rtmUnreachableError
    T.TMeta [Char]
s      -> [Char] -> Exp
rtmHole [Char]
s

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

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

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

    mkAlt :: HS.Pat -> CC HS.Alt
    mkAlt :: Pat
-> ReaderT
     CCEnv
     (WriterT
        UsesFloat (ReaderT GHCModuleEnv (StateT HsCompileState TCM)))
     Alt
mkAlt Pat
pat = do
        body' <- TTerm -> CC Exp
term (TTerm -> CC Exp) -> TTerm -> CC Exp
forall a b. (a -> b) -> a -> b
$ TAlt -> TTerm
T.aBody TAlt
a
        let body'' = case Exp
body' of
                       HS.Lambda{} -> Exp -> Exp
hsCoerce Exp
body'
                       Exp
_           -> Exp
body'
        return $ HS.Alt pat (HS.UnGuardedRhs body'') emptyBinds

literal :: forall m. Monad m => Literal -> CCT m HS.Exp
literal :: forall (m :: * -> *). Monad m => Literal -> CCT m Exp
literal Literal
l = case Literal
l of
  LitNat    Integer
_   -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp
typed [Char]
"Integer"
  LitWord64 Word64
_   -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ [Char] -> Exp
typed [Char]
"MAlonzo.RTE.Word64"
  LitFloat  Double
x   -> Double -> [Char] -> CCT m Exp
floatExp Double
x [Char]
"Double"
  LitQName  QName
x   -> Exp -> CCT m Exp
forall a. a -> ReaderT CCEnv (WriterT UsesFloat (HsCompileT m)) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> CCT m Exp) -> Exp -> CCT m Exp
forall a b. (a -> b) -> a -> b
$ QName -> Exp
litqname QName
x
  LitString 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
  opts <- ReaderT GHCModuleEnv (StateT HsCompileState TCM) GHCOptions
forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  def <- getConstInfo q
  let Constructor{ conPars = np, conSrcCon, conErased = erased } = theDef def
  (argTypes0, _) <- hsTelApproximation (defType def)
  let strict     = if ConHead -> Induction
conInductive ConHead
conSrcCon Induction -> Induction -> Bool
forall a. Eq a => a -> a -> Bool
== Induction
Inductive Bool -> Bool -> Bool
&&
                      GHCOptions -> Bool
optGhcStrictData GHCOptions
opts
                   then Strictness
HS.Strict
                   else Strictness
HS.Lazy
      argTypes   = [ (Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
strict, Type
t)
                   | (Type
t, Bool
False) <- [Type] -> [Bool] -> [(Type, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Nat -> [Type] -> [Type]
forall a. Nat -> [a] -> [a]
drop Nat
np [Type]
argTypes0)
                                       ([Bool] -> Maybe [Bool] -> [Bool]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Bool]
erased [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
                   ]
  return $ HS.ConDecl (unqhname ConK q) argTypes

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

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

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

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

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

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

type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)

copyRTEModules :: MonadGHCIO m => m ()
copyRTEModules :: forall (m :: * -> *). MonadGHCIO m => m ()
copyRTEModules = do
  dataDir <- IO [Char] -> m [Char]
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO [Char]
getDataDir
  let srcDir = [Char]
dataDir [Char] -> [Char] -> [Char]
</> [Char]
"MAlonzo" [Char] -> [Char] -> [Char]
</> [Char]
"src"
  dstDir <- optGhcCompileDir <$> askGhcOpts
  liftIO $ copyDirContent srcDir dstDir

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

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

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

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

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

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

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

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

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

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