module Agda.Compiler.MAlonzo.Compiler where

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

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

import GHC.Generics (Generic)

import qualified Agda.Utils.Haskell.Syntax as HS

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

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

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

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

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

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

import Paths_Agda

import Agda.Utils.Impossible

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

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

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

--- Command-line flags ---

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

instance NFData GHCFlags

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

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

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

--- Context types ---

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

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

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

instance Monad m => ReadGHCOpts (ReaderT GHCModuleEnv m) where
  askGhcOpts :: ReaderT GHCModuleEnv m GHCOptions
askGhcOpts = forall r' r (m :: * -> *) a.
(r' -> r) -> ReaderT r m a -> ReaderT r' m a
withReaderT GHCModuleEnv -> GHCEnv
ghcModEnv 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 = forall r' r (m :: * -> *) a.
(r' -> r) -> ReaderT r m a -> ReaderT r' m a
withReaderT GHCModule -> GHCModuleEnv
ghcModModuleEnv forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts

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

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

--- Top-level compilation ---

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

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

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

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

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

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

--- Module compilation ---

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

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

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

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

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

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

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

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

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

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

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

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

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

imports ::
  BuiltinThings PrimFun -> Set TopLevelModuleName -> [Definition] ->
  [HS.ImportDecl]
imports :: BuiltinThings PrimFun
-> Set TopLevelModuleName -> [Definition] -> [ImportDecl]
imports BuiltinThings PrimFun
builtinThings Set TopLevelModuleName
usedModules [Definition]
defs = [ImportDecl]
hsImps 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 forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
              (Bool
False, [ Name -> ImportSpec
HS.IVar forall a b. (a -> b) -> a -> b
$ FilePath -> Name
HS.Ident FilePath
x
                      | FilePath
x <- [FilePath
mazCoerceName, FilePath
mazErasedName, FilePath
mazAnyTypeName] forall a. [a] -> [a] -> [a]
++
                             forall a b. (a -> b) -> [a] -> [b]
map TPrim -> FilePath
treelessPrimName [TPrim]
rtePrims ])

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

  imps :: [HS.ImportDecl]
  imps :: [ImportDecl]
imps = forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> ImportDecl
decl forall a b. (a -> b) -> a -> b
$ [ModuleName] -> [ModuleName]
uniq forall a b. (a -> b) -> a -> b
$ BuiltinThings PrimFun -> [Definition] -> [ModuleName]
importsForPrim BuiltinThings PrimFun
builtinThings [Definition]
defs forall a. [a] -> [a] -> [a]
++ 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 forall a. Maybe a
Nothing

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

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

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

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

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

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

instance Monoid UsesFloat where
  mempty :: UsesFloat
mempty  = UsesFloat
NoFloat
  mappend :: UsesFloat -> UsesFloat -> UsesFloat
mappend = 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 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 forall a b. (a -> b) -> a -> b
$ forall a. LensModality a => a -> Bool
usableModality ArgInfo
info = do
  forall (m :: * -> *).
MonadDebug m =>
FilePath -> Nat -> TCM Doc -> m ()
reportSDoc FilePath
"compile.ghc.definition" Nat
10 forall a b. (a -> b) -> a -> b
$
    (TCM Doc
"Not compiling" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) forall a. Semigroup a => a -> a -> a
<> TCM Doc
"."
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty, 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
  forall (m :: * -> *).
MonadDebug m =>
FilePath -> Nat -> TCM Doc -> m ()
reportSDoc FilePath
"compile.ghc.definition" Nat
10 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
vcat
    [ (TCM Doc
"Compiling" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) forall a. Semigroup a => a -> a -> a
<> TCM Doc
":"
    , forall (m :: * -> *). Functor m => Nat -> m Doc -> m Doc
nest Nat
2 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty Defn
d
    ]
  Maybe HaskellPragma
pragma <- forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
liftTCM forall a b. (a -> b) -> a -> b
$ QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q
  GHCEnv
env <- forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let is :: (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
p = forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
p GHCEnv
env
  Maybe CheckedMainFunctionDef
typeCheckedMainDef <- Definition -> HsCompileM (Maybe CheckedMainFunctionDef)
checkTypeOfMain Definition
def
  let mainDecl :: [Decl]
mainDecl = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ CheckedMainFunctionDef -> Decl
checkedMainDecl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CheckedMainFunctionDef
typeCheckedMainDef
  let retDecls :: b -> m (a, b)
retDecls b
ds = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Monoid a => a
mempty, b
ds)
  (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (,,Maybe CheckedMainFunctionDef
typeCheckedMainDef)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (([Decl]
mainDecl forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> [Decl] -> [Decl]
infodecl QName
q) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    case Defn
d of

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

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

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

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

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

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

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

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

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

      -- itIsOne.
      Axiom{} | (GHCEnv -> Maybe QName) -> Bool
is GHCEnv -> Maybe QName
ghcEnvItIsOne -> do
        forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
retDecls 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
        forall {m :: * -> *} {a} {b}. (Monad m, Monoid a) => b -> m (a, b)
retDecls forall a b. (a -> b) -> a -> b
$
          [ [Match] -> Decl
HS.FunBind
              [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match (QName -> Name
dname QName
q) []
                 (Exp -> Rhs
HS.UnGuardedRhs (FilePath -> Exp
HS.FakeExp FilePath
"\\_ _ _ -> ()"))
                 Maybe Binds
emptyBinds]
          ]

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

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

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

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

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

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

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

      DataOrRecSig{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

      PrimitiveSort{} -> 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 forall a b. (a -> b) -> a -> b
$ QName
-> ReaderT
     GHCModuleEnv (StateT HsCompileState TCM) (UsesFloat, [Decl])
functionViaTreeless QName
q

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

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

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

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

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

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

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

      -- The definition of the non-stripped function
      ([Pat]
ps0, Exp
_) <- Exp -> ([Pat], Exp)
lamView forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> HsCompileM Exp
closedTerm_ (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
($) TTerm
T.TErased forall a b. (a -> b) -> a -> b
$ forall a. Nat -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Nat
length [ArgUsage]
used) TTerm -> TTerm
T.TLam)
      let b0 :: Exp
b0 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
HS.App (Name -> Exp
hsVarUQ forall a b. (a -> b) -> a -> b
$ QName -> Name
duname QName
q) [ Name -> Exp
hsVarUQ Name
x | (~(HS.PVar Name
x), ArgUsage
ArgUsed) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Pat]
ps0 [ArgUsage]
used ]
          ps0' :: [Pat]
ps0' = 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

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

  fbWithType :: HS.Type -> HS.Exp -> [HS.Decl]
  fbWithType :: Type -> Exp -> [Decl]
fbWithType Type
ty Exp
e =
    [Name] -> Type -> Decl
HS.TypeSig [QName -> Name
dname QName
q] Type
ty 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 forall a b. (a -> b) -> a -> b
$ FilePath -> Text
Text.pack forall a b. (a -> b) -> a -> b
$ FilePath
"postulate evaluated: " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> FilePath
prettyShow QName
q

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

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

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

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

ccContext :: Lens' CCContext CCEnv
ccContext :: Lens' [Name] CCEnv
ccContext [Name] -> f [Name]
f CCEnv
e = (\ [Name]
cxt -> CCEnv
e { _ccContext :: [Name]
_ccContext = [Name]
cxt }) 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 = 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ [Name]
xs 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Ord a => a -> a -> Bool
< Nat
0 = forall a. HasCallStack => a
__IMPOSSIBLE__
freshNames Nat
n [Name] -> CCT m a
cont = do
  ([Name]
xs, [Name]
rest) <- forall a. Nat -> [a] -> ([a], [a])
splitAt Nat
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall o (m :: * -> *) i. MonadReader o m => Lens' i o -> m i
view Lens' [Name] CCEnv
ccNameSupply
  forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (forall i o. Lens' i o -> LensMap i o
over Lens' [Name] CCEnv
ccNameSupply (forall a b. a -> b -> a
const [Name]
rest)) forall a b. (a -> b) -> a -> b
$ [Name] -> CCT m a
cont [Name]
xs

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

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

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

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

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

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

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

-- Translate case on bool to if
mkIf :: T.TTerm -> CC T.TTerm
mkIf :: TTerm -> CC TTerm
mkIf t :: TTerm
t@(TCase Nat
e CaseInfo
_ TTerm
d [TACon QName
c1 Nat
0 TTerm
b1, TACon QName
c2 Nat
0 TTerm
b2]) | forall a. Unreachable a => a -> Bool
T.isUnreachable TTerm
d = do
  GHCEnv
env <- forall (m :: * -> *) a. Monad m => HsCompileT m a -> CCT m a
liftCC forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
askGHCEnv
  let isTrue :: QName -> Bool
isTrue  QName
c = forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
ghcEnvTrue  GHCEnv
env
      isFalse :: QName -> Bool
isFalse QName
c = forall a. a -> Maybe a
Just QName
c forall a. Eq a => a -> a -> Bool
== GHCEnv -> Maybe QName
ghcEnvFalse GHCEnv
env
  if | QName -> Bool
isTrue QName
c1, QName -> Bool
isFalse QName
c2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm -> TTerm -> TTerm
T.tIfThenElse (TTerm -> TTerm
TCoerce forall a b. (a -> b) -> a -> b
$ Nat -> TTerm
TVar Nat
e) TTerm
b1 TTerm
b2
     | QName -> Bool
isTrue QName
c2, QName -> Bool
isFalse QName
c1 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm -> TTerm -> TTerm
T.tIfThenElse (TTerm -> TTerm
TCoerce forall a b. (a -> b) -> a -> b
$ Nat -> TTerm
TVar Nat
e) TTerm
b2 TTerm
b1
     | Bool
otherwise             -> forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
mkIf TTerm
t = 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 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            = forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
hasCoerce Exp -> Exp
hsCoerce
  case (TTerm
t, [TTerm]
ts) of
    (T.TPrim TPrim
T.PIf, [TTerm
c, TTerm
x, TTerm
y]) -> Exp -> Exp
coe forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do Exp -> Exp -> Exp -> Exp
HS.If forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> CC Exp
term TTerm
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> CC Exp
term TTerm
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> CC Exp
term TTerm
y

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

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

    -- Other kind of application: fall back to apps.
    (TTerm
t, [TTerm]
ts) -> TTerm -> CC Exp
noApplication TTerm
t 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 = 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 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 forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Nat -> a -> a
raise Nat
n TTerm
t TTerm -> [TTerm] -> TTerm
`T.mkTApp` forall a b. (a -> b) -> [a] -> [b]
map Nat -> TTerm
T.TVar (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{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
  T.TCoerce{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
  T.TCon{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
  T.TDef{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

compiledTypeSynonym :: QName -> String -> Nat -> HS.Decl
compiledTypeSynonym :: QName -> FilePath -> Nat -> Decl
compiledTypeSynonym QName
q FilePath
hsT Nat
arity =
  Name -> [TyVarBind] -> Type -> Decl
HS.TypeDecl (NameKind -> QName -> Name
unqhname NameKind
TypeK QName
q) (forall a b. (a -> b) -> [a] -> [b]
map Name -> TyVarBind
HS.UnkindedVar [Name]
vs)
              (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Type -> Type -> Type
HS.TyApp (FilePath -> Type
HS.FakeType FilePath
hsT) forall a b. (a -> b) -> a -> b
$ 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 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] forall a. a -> [a] -> [a]
:
  forall b a. b -> (a -> b) -> Maybe a -> b
maybe [DataOrNew -> Name -> [TyVarBind] -> [ConDecl] -> [Deriving] -> Decl
HS.DataDecl DataOrNew
kind Name
tn [] [ConDecl]
cds' []]
        (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 forall a b. (a -> b) -> a -> b
$ VariableKind -> Nat -> Name
ihname VariableKind
A Nat
i | Nat
i <- [Nat
0 .. Nat
npar 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 [(forall a. Maybe a
Nothing, Type
t)]])
      -- The strictness annotations are removed for newtype
      -- constructors.
    (Induction, [ConDecl])
_ -> (DataOrNew
HS.DataType, [ConDecl]
cds)

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

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

type MonadGHCIO m = (MonadIO m, ReadGHCOpts m)

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

writeModule :: MonadGHCIO m => HS.Module -> m ()
writeModule :: forall (m :: * -> *). MonadGHCIO m => Module -> m ()
writeModule (HS.Module ModuleName
m [ModulePragma]
ps [ImportDecl]
imp [Decl]
ds) = do
  -- Note that GHC assumes that sources use ASCII or UTF-8.
  FilePath
out <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
MonadGHCIO m =>
ModuleName -> m (FilePath, FilePath)
outFileAndDir ModuleName
m
  Bool
strict <- GHCOptions -> Bool
optGhcStrict forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  let languagePragmas :: [ModulePragma]
languagePragmas =
        forall a b. (a -> b) -> [a] -> [b]
List.map ([Name] -> ModulePragma
HS.LanguagePragma forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall el coll. Singleton el coll => el -> coll
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Name
HS.Ident) forall a b. (a -> b) -> a -> b
$
          forall a. Ord a => [a] -> [a]
List.sort forall a b. (a -> b) -> a -> b
$
            [ FilePath
"QualifiedDo" | Bool
strict ] 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.
            [ FilePath
"BangPatterns"
            , FilePath
"EmptyDataDecls"
            , FilePath
"EmptyCase"
            , FilePath
"ExistentialQuantification"
            , FilePath
"ScopedTypeVariables"
            , FilePath
"NoMonomorphismRestriction"
            , FilePath
"RankNTypes"
            , FilePath
"PatternSynonyms"
            , FilePath
"OverloadedStrings"
            ]
  let ghcOptions :: [ModulePragma]
ghcOptions =
        forall a b. (a -> b) -> [a] -> [b]
List.map FilePath -> ModulePragma
HS.OtherPragma
          [ FilePath
""  -- to separate from LANGUAGE pragmas
          , FilePath
"{-# 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.)
          ]
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
UTF8.writeFile FilePath
out forall a b. (a -> b) -> a -> b
$ (forall a. [a] -> [a] -> [a]
++ FilePath
"\n") forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> FilePath
prettyPrint forall a b. (a -> b) -> a -> b
$
    -- TODO: It might make sense to skip bang patterns for the unused
    -- arguments of the "non-stripped" functions.
    forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
strict forall a. MakeStrict a => a -> a
makeStrict forall a b. (a -> b) -> a -> b
$
    ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
HS.Module ModuleName
m (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[ModulePragma]
languagePragmas, [ModulePragma]
ghcOptions, [ModulePragma]
ps]) [ImportDecl]
imp [Decl]
ds

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

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

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

callGHC :: ReaderT GHCModule TCM ()
callGHC :: ReaderT GHCModule TCM ()
callGHC = do
  GHCOptions
opts     <- forall (m :: * -> *). ReadGHCOpts m => m GHCOptions
askGhcOpts
  CommandLineOptions
agdaOpts <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions
  FilePath
hsmod    <- forall a. Pretty a => a -> FilePath
prettyPrint forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadGHCModuleEnv m => m ModuleName
curHsMod
  TopLevelModuleName
agdaMod  <- forall (m :: * -> *). ReadGHCModuleEnv m => m TopLevelModuleName
curAgdaMod
  let outputName :: FilePath
outputName = Text -> FilePath
Text.unpack forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> a
List1.last forall a b. (a -> b) -> a -> b
$ TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
agdaMod
  (FilePath
mdir, FilePath
fp) <- forall (m :: * -> *).
(MonadGHCIO m, ReadGHCModuleEnv m) =>
m (FilePath, FilePath)
curOutFileAndDir
  let ghcopts :: [FilePath]
ghcopts = GHCOptions -> [FilePath]
optGhcFlags GHCOptions
opts

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

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

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

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

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