module Agda.Compiler.MAlonzo.Compiler where

import Control.Monad.Reader hiding (mapM_, forM_, mapM, forM, sequence)

import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import qualified Data.Set as Set

import Numeric.IEEE

import qualified Agda.Utils.Haskell.Syntax as HS

import System.Directory (createDirectoryIfMissing)
import System.FilePath hiding (normalise)

import Agda.Compiler.CallCompiler
import Agda.Compiler.Common
import Agda.Compiler.MAlonzo.Coerce
import Agda.Compiler.MAlonzo.Misc
import Agda.Compiler.MAlonzo.Pretty
import Agda.Compiler.MAlonzo.Primitives
import Agda.Compiler.MAlonzo.HaskellTypes
import Agda.Compiler.MAlonzo.Pragmas
import Agda.Compiler.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 Agda.Syntax.Fixity
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Internal as I
import Agda.Syntax.Internal.Names (namesIn)
import qualified Agda.Syntax.Treeless as T
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive (getBuiltinName)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Warnings

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

import Paths_Agda

import Agda.Utils.Impossible

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

ghcBackend :: Backend
ghcBackend :: Backend
ghcBackend = Backend' GHCOptions GHCOptions GHCModuleEnv IsMain [Decl]
-> Backend
forall opts env menv mod def.
Backend' opts env menv mod def -> Backend
Backend Backend' GHCOptions GHCOptions GHCModuleEnv IsMain [Decl]
ghcBackend'

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

--- Options ---

data GHCOptions = GHCOptions
  { GHCOptions -> Bool
optGhcCompile :: Bool
  , GHCOptions -> Bool
optGhcCallGhc :: Bool
  , GHCOptions -> [String]
optGhcFlags   :: [String]
  }

defaultGHCOptions :: GHCOptions
defaultGHCOptions :: GHCOptions
defaultGHCOptions = GHCOptions :: Bool -> Bool -> [String] -> GHCOptions
GHCOptions
  { optGhcCompile :: Bool
optGhcCompile = Bool
False
  , optGhcCallGhc :: Bool
optGhcCallGhc = Bool
True
  , optGhcFlags :: [String]
optGhcFlags   = []
  }

ghcCommandLineFlags :: [OptDescr (Flag GHCOptions)]
ghcCommandLineFlags :: [OptDescr (Flag GHCOptions)]
ghcCommandLineFlags =
    [ String
-> [String]
-> ArgDescr (Flag GHCOptions)
-> String
-> OptDescr (Flag GHCOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [Char
'c']  [String
"compile", String
"ghc"] (Flag GHCOptions -> ArgDescr (Flag GHCOptions)
forall a. a -> ArgDescr a
NoArg Flag GHCOptions
forall (f :: * -> *). Applicative f => GHCOptions -> f GHCOptions
enable)
                    String
"compile program using the GHC backend"
    , String
-> [String]
-> ArgDescr (Flag GHCOptions)
-> String
-> OptDescr (Flag GHCOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"ghc-dont-call-ghc"] (Flag GHCOptions -> ArgDescr (Flag GHCOptions)
forall a. a -> ArgDescr a
NoArg Flag GHCOptions
forall (f :: * -> *). Applicative f => GHCOptions -> f GHCOptions
dontCallGHC)
                    String
"don't call GHC, just write the GHC Haskell files."
    , String
-> [String]
-> ArgDescr (Flag GHCOptions)
-> String
-> OptDescr (Flag GHCOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option []     [String
"ghc-flag"] ((String -> Flag GHCOptions) -> String -> ArgDescr (Flag GHCOptions)
forall a. (String -> a) -> String -> ArgDescr a
ReqArg String -> Flag GHCOptions
forall (f :: * -> *).
Applicative f =>
String -> GHCOptions -> f GHCOptions
ghcFlag String
"GHC-FLAG")
                    String
"give the flag GHC-FLAG to GHC"
    ]
  where
    enable :: GHCOptions -> f GHCOptions
enable      GHCOptions
o = GHCOptions -> f GHCOptions
forall (f :: * -> *) a. Applicative f => a -> f a
pure GHCOptions
o{ optGhcCompile :: Bool
optGhcCompile = Bool
True }
    dontCallGHC :: GHCOptions -> f GHCOptions
dontCallGHC GHCOptions
o = GHCOptions -> f GHCOptions
forall (f :: * -> *) a. Applicative f => a -> f a
pure GHCOptions
o{ optGhcCallGhc :: Bool
optGhcCallGhc = Bool
False }
    ghcFlag :: String -> GHCOptions -> f GHCOptions
ghcFlag String
f   GHCOptions
o = GHCOptions -> f GHCOptions
forall (f :: * -> *) a. Applicative f => a -> f a
pure GHCOptions
o{ optGhcFlags :: [String]
optGhcFlags   = GHCOptions -> [String]
optGhcFlags GHCOptions
o [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
f] }

--- Top-level compilation ---

ghcPreCompile :: GHCOptions -> TCM GHCOptions
ghcPreCompile :: GHCOptions -> TCM GHCOptions
ghcPreCompile GHCOptions
ghcOpts = do
  Bool
allowUnsolved <- PragmaOptions -> Bool
optAllowUnsolved (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  Bool -> TCM GHCModuleEnv -> TCM GHCModuleEnv
forall (f :: * -> *).
Applicative f =>
Bool -> f GHCModuleEnv -> f GHCModuleEnv
when Bool
allowUnsolved (TCM GHCModuleEnv -> TCM GHCModuleEnv)
-> TCM GHCModuleEnv -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ String -> TCM GHCModuleEnv
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCM GHCModuleEnv) -> String -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ String
"Unsolved meta variables are not allowed when compiling."
  GHCOptions -> TCM GHCOptions
forall (m :: * -> *) a. Monad m => a -> m a
return GHCOptions
ghcOpts

ghcPostCompile :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM ()
ghcPostCompile :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM GHCModuleEnv
ghcPostCompile GHCOptions
opts IsMain
isMain Map ModuleName IsMain
mods = TCM GHCModuleEnv
copyRTEModules TCM GHCModuleEnv -> TCM GHCModuleEnv -> TCM GHCModuleEnv
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM GHCModuleEnv
callGHC GHCOptions
opts IsMain
isMain Map ModuleName IsMain
mods

--- Module compilation ---

-- | This environment is no longer used for anything.

type GHCModuleEnv = ()

ghcPreModule
  :: GHCOptions
  -> IsMain      -- ^ Are we looking at the main module?
  -> ModuleName
  -> FilePath    -- ^ Path to the @.agdai@ file.
  -> TCM (Recompile GHCModuleEnv IsMain)
                 -- ^ Could we confirm the existence of a main function?
ghcPreModule :: GHCOptions
-> IsMain
-> ModuleName
-> String
-> TCM (Recompile GHCModuleEnv IsMain)
ghcPreModule GHCOptions
_ IsMain
isMain ModuleName
m String
ifile = TCM Bool
-> TCM (Recompile GHCModuleEnv IsMain)
-> TCM (Recompile GHCModuleEnv IsMain)
-> TCM (Recompile GHCModuleEnv IsMain)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCM Bool
uptodate TCM (Recompile GHCModuleEnv IsMain)
forall menv. TCMT IO (Recompile menv IsMain)
noComp TCM (Recompile GHCModuleEnv IsMain)
forall mod. TCMT IO (Recompile GHCModuleEnv mod)
yesComp
  where
    uptodate :: TCM Bool
uptodate = IO Bool -> TCM Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> TCM Bool) -> TCMT IO (IO Bool) -> TCM Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> String -> IO Bool
isNewerThan (String -> String -> IO Bool)
-> TCMT IO String -> TCMT IO (String -> IO Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO String
outFile_ TCMT IO (String -> IO Bool) -> TCMT IO String -> TCMT IO (IO Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> TCMT IO String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
ifile

    noComp :: TCMT IO (Recompile menv IsMain)
noComp = do
      String -> VerboseLevel -> String -> TCM GHCModuleEnv
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m GHCModuleEnv
reportSLn String
"compile.ghc" VerboseLevel
2 (String -> TCM GHCModuleEnv)
-> (ModuleName -> String) -> ModuleName -> TCM GHCModuleEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : no compilation is needed.") (String -> String)
-> (ModuleName -> String) -> ModuleName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> String
forall a. Show a => a -> String
show (QName -> String) -> (ModuleName -> QName) -> ModuleName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> QName
A.mnameToConcrete (ModuleName -> TCM GHCModuleEnv)
-> TCMT IO ModuleName -> TCM GHCModuleEnv
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
curMName
      IsMain -> Recompile menv IsMain
forall menv mod. mod -> Recompile menv mod
Skip (IsMain -> Recompile menv IsMain)
-> (Interface -> IsMain) -> Interface -> Recompile menv IsMain
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IsMain -> Interface -> IsMain
hasMainFunction IsMain
isMain (Interface -> Recompile menv IsMain)
-> TCMT IO Interface -> TCMT IO (Recompile menv IsMain)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Interface
curIF

    yesComp :: TCMT IO (Recompile GHCModuleEnv mod)
yesComp = do
      String
m   <- QName -> String
forall a. Show a => a -> String
show (QName -> String) -> (ModuleName -> QName) -> ModuleName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> QName
A.mnameToConcrete (ModuleName -> String) -> TCMT IO ModuleName -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO ModuleName
curMName
      String
out <- TCMT IO String
outFile_
      String -> VerboseLevel -> String -> TCM GHCModuleEnv
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m GHCModuleEnv
reportSLn String
"compile.ghc" VerboseLevel
1 (String -> TCM GHCModuleEnv) -> String -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
m, String
ifile, String
out] String
"Compiling <<0>> in <<1>> to <<2>>"
      Lens' (Set ModuleName) TCState
stImportedModules Lens' (Set ModuleName) TCState
-> Set ModuleName -> TCM GHCModuleEnv
forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m GHCModuleEnv
`setTCLens` Set ModuleName
forall a. Set a
Set.empty  -- we use stImportedModules to accumulate the required Haskell imports
      Recompile GHCModuleEnv mod -> TCMT IO (Recompile GHCModuleEnv mod)
forall (m :: * -> *) a. Monad m => a -> m a
return (GHCModuleEnv -> Recompile GHCModuleEnv mod
forall menv mod. menv -> Recompile menv mod
Recompile ())

ghcPostModule
  :: GHCOptions
  -> GHCModuleEnv
  -> IsMain        -- ^ Are we looking at the main module?
  -> ModuleName
  -> [[HS.Decl]]   -- ^ Compiled module content.
  -> TCM IsMain    -- ^ Could we confirm the existence of a main function?
ghcPostModule :: GHCOptions
-> GHCModuleEnv -> IsMain -> ModuleName -> [[Decl]] -> TCM IsMain
ghcPostModule GHCOptions
_ GHCModuleEnv
_ IsMain
isMain ModuleName
_ [[Decl]]
defs = do
  ModuleName
m      <- TCM ModuleName
curHsMod
  [ImportDecl]
imps   <- TCM [ImportDecl]
imports
  -- Get content of FOREIGN pragmas.
  ([String]
headerPragmas, [String]
hsImps, [String]
code) <- TCM ([String], [String], [String])
foreignHaskell
  Module -> TCM GHCModuleEnv
writeModule (Module -> TCM GHCModuleEnv) -> Module -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
HS.Module ModuleName
m
    ((String -> ModulePragma) -> [String] -> [ModulePragma]
forall a b. (a -> b) -> [a] -> [b]
map String -> ModulePragma
HS.OtherPragma [String]
headerPragmas)
    [ImportDecl]
imps
    ((String -> Decl) -> [String] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map String -> Decl
fakeDecl ([String]
hsImps [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
code) [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Decl]]
defs)
  IsMain -> Interface -> IsMain
hasMainFunction IsMain
isMain (Interface -> IsMain) -> TCMT IO Interface -> TCM IsMain
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Interface
curIF

ghcCompileDef :: GHCOptions -> GHCModuleEnv -> IsMain -> Definition -> TCM [HS.Decl]
ghcCompileDef :: GHCOptions -> GHCModuleEnv -> IsMain -> Definition -> TCM [Decl]
ghcCompileDef GHCOptions
_ GHCModuleEnv
env IsMain
isMain Definition
def = GHCModuleEnv -> IsMain -> Definition -> TCM [Decl]
definition GHCModuleEnv
env IsMain
isMain Definition
def

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

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

--------------------------------------------------
-- imported modules
--   I use stImportedModules in a non-standard way,
--   accumulating in it what are acutally used in Misc.xqual
--------------------------------------------------

imports :: TCM [HS.ImportDecl]
imports :: TCM [ImportDecl]
imports = ([ImportDecl]
hsImps [ImportDecl] -> [ImportDecl] -> [ImportDecl]
forall a. [a] -> [a] -> [a]
++) ([ImportDecl] -> [ImportDecl])
-> TCM [ImportDecl] -> TCM [ImportDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM [ImportDecl]
imps where
  hsImps :: [HS.ImportDecl]
  hsImps :: [ImportDecl]
hsImps = [ImportDecl
unqualRTE, ModuleName -> ImportDecl
decl ModuleName
mazRTE]

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

  rtePrims :: [TPrim]
rtePrims = [TPrim
T.PAdd, TPrim
T.PSub, TPrim
T.PMul, TPrim
T.PQuot, TPrim
T.PRem, TPrim
T.PGeq, TPrim
T.PLt, TPrim
T.PEqI, TPrim
T.PEqF,
              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]

  imps :: TCM [HS.ImportDecl]
  imps :: TCM [ImportDecl]
imps = (ModuleName -> ImportDecl) -> [ModuleName] -> [ImportDecl]
forall a b. (a -> b) -> [a] -> [b]
List.map ModuleName -> ImportDecl
decl ([ModuleName] -> [ImportDecl])
-> ([ModuleName] -> [ModuleName]) -> [ModuleName] -> [ImportDecl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ModuleName] -> [ModuleName]
uniq ([ModuleName] -> [ImportDecl])
-> TCMT IO [ModuleName] -> TCM [ImportDecl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
           ([ModuleName] -> [ModuleName] -> [ModuleName]
forall a. [a] -> [a] -> [a]
(++) ([ModuleName] -> [ModuleName] -> [ModuleName])
-> TCMT IO [ModuleName] -> TCMT IO ([ModuleName] -> [ModuleName])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [ModuleName]
importsForPrim TCMT IO ([ModuleName] -> [ModuleName])
-> TCMT IO [ModuleName] -> TCMT IO [ModuleName]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((ModuleName -> ModuleName) -> [ModuleName] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
List.map ModuleName -> ModuleName
mazMod ([ModuleName] -> [ModuleName])
-> TCMT IO [ModuleName] -> TCMT IO [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO [ModuleName]
mnames))

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

  mnames :: TCM [ModuleName]
  mnames :: TCMT IO [ModuleName]
mnames = Set ModuleName -> [ModuleName]
forall a. Set a -> [a]
Set.elems (Set ModuleName -> [ModuleName])
-> TCMT IO (Set ModuleName) -> TCMT IO [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Lens' (Set ModuleName) TCState -> TCMT IO (Set ModuleName)
forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (Set ModuleName) TCState
stImportedModules

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

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

definition :: GHCModuleEnv -> IsMain -> Definition -> TCM [HS.Decl]
-- ignore irrelevant definitions
{- Andreas, 2012-10-02: Invariant no longer holds
definition kit (Defn NonStrict _ _  _ _ _ _ _ _) = __IMPOSSIBLE__
-}
definition :: GHCModuleEnv -> IsMain -> Definition -> TCM [Decl]
definition GHCModuleEnv
_env IsMain
_isMain Defn{defArgInfo :: Definition -> ArgInfo
defArgInfo = ArgInfo
info, defName :: Definition -> QName
defName = QName
q} | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Bool
forall a. LensModality a => a -> Bool
usableModality ArgInfo
info = do
  String -> VerboseLevel -> TCM Doc -> TCM GHCModuleEnv
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m GHCModuleEnv
reportSDoc String
"compile.ghc.definition" VerboseLevel
10 (TCM Doc -> TCM GHCModuleEnv) -> TCM Doc -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$
    (TCM Doc
"Not compiling" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
"."
  [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return []
definition GHCModuleEnv
env IsMain
isMain def :: Definition
def@Defn{defName :: Definition -> QName
defName = QName
q, defType :: Definition -> Type
defType = Type
ty, theDef :: Definition -> Defn
theDef = Defn
d} = do
  String -> VerboseLevel -> TCM Doc -> TCM GHCModuleEnv
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m GHCModuleEnv
reportSDoc String
"compile.ghc.definition" VerboseLevel
10 (TCM Doc -> TCM GHCModuleEnv) -> TCM Doc -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
vcat
    [ (TCM Doc
"Compiling" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q) TCM Doc -> TCM Doc -> TCM Doc
forall a. Semigroup a => a -> a -> a
<> TCM Doc
":"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest VerboseLevel
2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (Defn -> String
forall a. Show a => a -> String
show Defn
d)
    ]
  Maybe HaskellPragma
pragma <- QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
q
  Maybe QName
mbool  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinBool
  Maybe QName
mlist  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinList
  Maybe QName
minf   <- String -> TCM (Maybe QName)
getBuiltinName String
builtinInf
  Maybe QName
mflat  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinFlat
  IsMain -> QName -> Definition -> TCM [Decl] -> TCM [Decl]
checkTypeOfMain IsMain
isMain QName
q Definition
def (TCM [Decl] -> TCM [Decl]) -> TCM [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ do
    QName -> [Decl] -> [Decl]
infodecl QName
q ([Decl] -> [Decl]) -> TCM [Decl] -> TCM [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Defn
d of

      Defn
_ | Just (HsDefn Range
r String
hs) <- Maybe HaskellPragma
pragma -> Range -> TCM [Decl] -> TCM [Decl]
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM [Decl] -> TCM [Decl]) -> TCM [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$
          if QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mflat
          then String -> TCM [Decl]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError
                String
"\"COMPILE GHC\" pragmas are not allowed for the FLAT builtin."
          else do
            -- Make sure we have imports for all names mentioned in the type.
            Type
hsty <- QName -> TCM Type
haskellType QName
q
            Type
ty   <- Type -> TCMT IO Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
ty
            [TCMT IO QName] -> TCM GHCModuleEnv
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m GHCModuleEnv
sequence_ [ QName -> Name -> TCMT IO QName
xqual QName
x (String -> Name
HS.Ident String
"_") | QName
x <- Set QName -> [QName]
forall a. Set a -> [a]
Set.toList (Type -> Set QName
forall a. NamesIn a => a -> Set QName
namesIn Type
ty) ]

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

            [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl] -> TCM [Decl]) -> [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ Type -> Exp -> [Decl]
fbWithType Type
hsty (String -> Exp
fakeExp String
hs)

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

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

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

      DataOrRecSig{} -> TCM [Decl]
forall a. HasCallStack => a
__IMPOSSIBLE__

      Axiom{} -> do
        VerboseLevel
ar <- Type -> TCM VerboseLevel
typeArity Type
ty
        [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl] -> TCM [Decl]) -> [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ [ QName -> String -> VerboseLevel -> Decl
compiledTypeSynonym QName
q String
ty VerboseLevel
ar | Just (HsType Range
r String
ty) <- [Maybe HaskellPragma
pragma] ] [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++
                 Exp -> [Decl]
fb Exp
axiomErr
      Primitive{ primName :: Defn -> String
primName = String
s } -> Exp -> [Decl]
fb (Exp -> [Decl]) -> TCMT IO Exp -> TCM [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Exp
primBody String
s

      Function{} -> Maybe HaskellPragma -> TCM [Decl] -> TCM [Decl]
function Maybe HaskellPragma
pragma (TCM [Decl] -> TCM [Decl]) -> TCM [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Decl]
functionViaTreeless QName
q

      Datatype{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
np, dataIxs :: Defn -> VerboseLevel
dataIxs = VerboseLevel
ni, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl, dataCons :: Defn -> [QName]
dataCons = [QName]
cs }
        | Just hsdata :: HaskellPragma
hsdata@(HsData Range
r String
ty [String]
hsCons) <- Maybe HaskellPragma
pragma -> Range -> TCM [Decl] -> TCM [Decl]
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM [Decl] -> TCM [Decl]) -> TCM [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ do
        String -> VerboseLevel -> TCM Doc -> TCM GHCModuleEnv
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m GHCModuleEnv
reportSDoc String
"compile.ghc.definition" VerboseLevel
40 (TCM Doc -> TCM GHCModuleEnv) -> TCM Doc -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
hsep ([TCM Doc] -> TCM Doc) -> [TCM Doc] -> TCM Doc
forall a b. (a -> b) -> a -> b
$
          [ TCM Doc
"Compiling data type with COMPILE pragma ...", HaskellPragma -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty HaskellPragma
hsdata ]
        QName -> TCM GHCModuleEnv
computeErasedConstructorArgs QName
q
        [Decl]
ccscov <- QName
-> VerboseLevel -> [QName] -> String -> [String] -> TCM [Decl]
constructorCoverageCode QName
q (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
ni) [QName]
cs String
ty [String]
hsCons
        [Decl]
cds <- (QName -> TCMT IO Decl) -> [QName] -> TCM [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO Decl
compiledcondecl [QName]
cs
        let result :: [Decl]
result = [[Decl]] -> [Decl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Decl]] -> [Decl]) -> [[Decl]] -> [Decl]
forall a b. (a -> b) -> a -> b
$
              [ QName
-> Induction -> VerboseLevel -> [ConDecl] -> Maybe Clause -> [Decl]
tvaldecl QName
q Induction
Inductive (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
ni) [] (Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
forall a. HasCallStack => a
__IMPOSSIBLE__)
              , [ QName -> String -> VerboseLevel -> Decl
compiledTypeSynonym QName
q String
ty VerboseLevel
np ]
              , [Decl]
cds
              , [Decl]
ccscov
              ]
        [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return [Decl]
result
      Datatype{ dataPars :: Defn -> VerboseLevel
dataPars = VerboseLevel
np, dataIxs :: Defn -> VerboseLevel
dataIxs = VerboseLevel
ni, dataClause :: Defn -> Maybe Clause
dataClause = Maybe Clause
cl,
                dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> do
        QName -> TCM GHCModuleEnv
computeErasedConstructorArgs QName
q
        [ConDecl]
cds <- (QName -> TCMT IO ConDecl) -> [QName] -> TCMT IO [ConDecl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((QName -> Induction -> TCMT IO ConDecl)
-> Induction -> QName -> TCMT IO ConDecl
forall a b c. (a -> b -> c) -> b -> a -> c
flip QName -> Induction -> TCMT IO ConDecl
condecl Induction
Inductive) [QName]
cs
        [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl] -> TCM [Decl]) -> [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ QName
-> Induction -> VerboseLevel -> [ConDecl] -> Maybe Clause -> [Decl]
tvaldecl QName
q Induction
Inductive (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
ni) [ConDecl]
cds Maybe Clause
cl
      Constructor{} -> [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      GeneralizableVar{} -> [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return []
      Record{ recPars :: Defn -> VerboseLevel
recPars = VerboseLevel
np, recClause :: Defn -> Maybe Clause
recClause = Maybe Clause
cl, recConHead :: Defn -> ConHead
recConHead = ConHead
con,
              recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind } ->
        let -- Non-recursive record types are treated as being
            -- inductive.
            inductionKind :: Induction
inductionKind = Induction -> Maybe Induction -> Induction
forall a. a -> Maybe a -> a
fromMaybe Induction
Inductive Maybe Induction
ind
        in case Maybe HaskellPragma
pragma of
          Just (HsData Range
r String
ty [String]
hsCons) -> Range -> TCM [Decl] -> TCM [Decl]
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM [Decl] -> TCM [Decl]) -> TCM [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ do
            let cs :: [QName]
cs = [ConHead -> QName
conName ConHead
con]
            QName -> TCM GHCModuleEnv
computeErasedConstructorArgs QName
q
            [Decl]
ccscov <- QName
-> VerboseLevel -> [QName] -> String -> [String] -> TCM [Decl]
constructorCoverageCode QName
q VerboseLevel
np [QName]
cs String
ty [String]
hsCons
            [Decl]
cds <- (QName -> TCMT IO Decl) -> [QName] -> TCM [Decl]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QName -> TCMT IO Decl
compiledcondecl [QName]
cs
            [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl] -> TCM [Decl]) -> [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$
              QName
-> Induction -> VerboseLevel -> [ConDecl] -> Maybe Clause -> [Decl]
tvaldecl QName
q Induction
inductionKind VerboseLevel
np [] (Clause -> Maybe Clause
forall a. a -> Maybe a
Just Clause
forall a. HasCallStack => a
__IMPOSSIBLE__) [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++
              [QName -> String -> VerboseLevel -> Decl
compiledTypeSynonym QName
q String
ty VerboseLevel
np] [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Decl]
cds [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ [Decl]
ccscov
          Maybe HaskellPragma
_ -> do
            QName -> TCM GHCModuleEnv
computeErasedConstructorArgs QName
q
            ConDecl
cd <- QName -> Induction -> TCMT IO ConDecl
condecl (ConHead -> QName
conName ConHead
con) Induction
inductionKind
            [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Decl] -> TCM [Decl]) -> [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ QName
-> Induction -> VerboseLevel -> [ConDecl] -> Maybe Clause -> [Decl]
tvaldecl QName
q Induction
inductionKind (Type -> VerboseLevel
I.arity Type
ty) [ConDecl
cd] Maybe Clause
cl
      AbstractDefn{} -> TCM [Decl]
forall a. HasCallStack => a
__IMPOSSIBLE__
  where
  function :: Maybe HaskellPragma -> TCM [HS.Decl] -> TCM [HS.Decl]
  function :: Maybe HaskellPragma -> TCM [Decl] -> TCM [Decl]
function Maybe HaskellPragma
mhe TCM [Decl]
fun = do
    [Decl]
ccls  <- [Decl] -> [Decl]
mkwhere ([Decl] -> [Decl]) -> TCM [Decl] -> TCM [Decl]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM [Decl]
fun
    Maybe QName
mflat <- String -> TCM (Maybe QName)
getBuiltinName String
builtinFlat
    case Maybe HaskellPragma
mhe of
      Just (HsExport Range
r String
name) -> Range -> TCM [Decl] -> TCM [Decl]
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM [Decl] -> TCM [Decl]) -> TCM [Decl] -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$
        if QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mflat
        then String -> TCM [Decl]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError
              String
"\"COMPILE GHC as\" pragmas are not allowed for the FLAT builtin."
        else do
          Type
t <- Range -> TCM Type -> TCM Type
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ QName -> TCM Type
haskellType QName
q
          let tsig :: HS.Decl
              tsig :: Decl
tsig = [Name] -> Type -> Decl
HS.TypeSig [String -> Name
HS.Ident String
name] Type
t

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

  functionViaTreeless :: QName -> TCM [HS.Decl]
  functionViaTreeless :: QName -> TCM [Decl]
functionViaTreeless QName
q = TCMT IO (Maybe TTerm)
-> TCM [Decl] -> (TTerm -> TCM [Decl]) -> TCM [Decl]
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (EvaluationStrategy -> QName -> TCMT IO (Maybe TTerm)
toTreeless EvaluationStrategy
LazyEvaluation QName
q) ([Decl] -> TCM [Decl]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) ((TTerm -> TCM [Decl]) -> TCM [Decl])
-> (TTerm -> TCM [Decl]) -> TCM [Decl]
forall a b. (a -> b) -> a -> b
$ \ TTerm
treeless -> do

    [Bool]
used <- QName -> TCM [Bool]
getCompiledArgUse QName
q
    let dostrip :: Bool
dostrip = (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bool -> Bool
not [Bool]
used

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

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

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

    -- The definition of the non-stripped function
    ([Pat]
ps0, Exp
_) <- Exp -> ([Pat], Exp)
lamView (Exp -> ([Pat], Exp)) -> TCMT IO Exp -> TCMT IO ([Pat], Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO Exp
closedTerm (((TTerm -> TTerm) -> TTerm -> TTerm)
-> TTerm -> [TTerm -> TTerm] -> TTerm
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
($) TTerm
T.TErased ([TTerm -> TTerm] -> TTerm) -> [TTerm -> TTerm] -> TTerm
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> (TTerm -> TTerm) -> [TTerm -> TTerm]
forall a. VerboseLevel -> a -> [a]
replicate ([Bool] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Bool]
used) TTerm -> TTerm
T.TLam)
    let b0 :: Exp
b0 = (Exp -> Exp -> Exp) -> Exp -> [Exp] -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> Exp -> Exp
HS.App (Name -> Exp
hsVarUQ (Name -> Exp) -> Name -> Exp
forall a b. (a -> b) -> a -> b
$ QName -> Name
duname QName
q) [ Name -> Exp
hsVarUQ Name
x | (~(HS.PVar Name
x), Bool
True) <- [Pat] -> [Bool] -> [(Pat, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Pat]
ps0 [Bool]
used ]

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

  mkwhere :: [HS.Decl] -> [HS.Decl]
  mkwhere :: [Decl] -> [Decl]
mkwhere (HS.FunBind [Match
m0, HS.Match Name
dn [Pat]
ps Rhs
rhs Maybe Binds
emptyBinds] : fbs :: [Decl]
fbs@(Decl
_:[Decl]
_)) =
          [[Match] -> Decl
HS.FunBind [Match
m0, Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match Name
dn [Pat]
ps Rhs
rhs Maybe Binds
bindsAux]]
    where
    bindsAux :: Maybe HS.Binds
    bindsAux :: Maybe Binds
bindsAux = Binds -> Maybe Binds
forall a. a -> Maybe a
Just (Binds -> Maybe Binds) -> Binds -> Maybe Binds
forall a b. (a -> b) -> a -> b
$ [Decl] -> Binds
HS.BDecls [Decl]
fbs

  mkwhere [Decl]
fbs = [Decl]
fbs

  fbWithType :: HS.Type -> HS.Exp -> [HS.Decl]
  fbWithType :: Type -> Exp -> [Decl]
fbWithType Type
ty Exp
e =
    [ [Name] -> Type -> Decl
HS.TypeSig [String -> QName -> Name
unqhname String
"d" QName
q] Type
ty ] [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ Exp -> [Decl]
fb Exp
e

  fb :: HS.Exp -> [HS.Decl]
  fb :: Exp -> [Decl]
fb Exp
e  = [[Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match (String -> QName -> Name
unqhname String
"d" QName
q) []
                                (Exp -> Rhs
HS.UnGuardedRhs (Exp -> Rhs) -> Exp -> Rhs
forall a b. (a -> b) -> a -> b
$ Exp
e) Maybe Binds
emptyBinds]]

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

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

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

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

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

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

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

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

type CC = ReaderT CCEnv TCM

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

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

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

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

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

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

closedTerm :: T.TTerm -> TCM HS.Exp
closedTerm :: TTerm -> TCMT IO Exp
closedTerm TTerm
v = do
  TTerm
v <- TTerm -> TCM TTerm
addCoercions TTerm
v
  TTerm -> CC Exp
term TTerm
v CC Exp -> CCEnv -> TCMT IO Exp
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
`runReaderT` CCEnv
initCCEnv

-- Translate case on bool to if
mkIf :: T.TTerm -> CC T.TTerm
mkIf :: TTerm -> CC TTerm
mkIf t :: TTerm
t@(TCase VerboseLevel
e CaseInfo
_ TTerm
d [TACon QName
c1 VerboseLevel
0 TTerm
b1, TACon QName
c2 VerboseLevel
0 TTerm
b2]) | TTerm -> Bool
forall a. Unreachable a => a -> Bool
T.isUnreachable TTerm
d = do
  Maybe QName
mTrue  <- TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName))
-> TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ String -> TCM (Maybe QName)
getBuiltinName String
builtinTrue
  Maybe QName
mFalse <- TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName))
-> TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ String -> TCM (Maybe QName)
getBuiltinName String
builtinFalse
  let isTrue :: QName -> Bool
isTrue  QName
c = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mTrue
      isFalse :: QName -> Bool
isFalse QName
c = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mFalse
  if | QName -> Bool
isTrue QName
c1, QName -> Bool
isFalse QName
c2 -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> CC TTerm) -> TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm -> TTerm -> TTerm
T.tIfThenElse (TTerm -> TTerm
TCoerce (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TTerm
TVar VerboseLevel
e) TTerm
b1 TTerm
b2
     | QName -> Bool
isTrue QName
c2, QName -> Bool
isFalse QName
c1 -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> CC TTerm) -> TTerm -> CC TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm -> TTerm -> TTerm
T.tIfThenElse (TTerm -> TTerm
TCoerce (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TTerm
TVar VerboseLevel
e) TTerm
b2 TTerm
b1
     | Bool
otherwise             -> TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
mkIf TTerm
t = TTerm -> CC TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t

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

    (T.TDef QName
f, [TTerm]
ts) -> do
      [Bool]
used <- TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [Bool] -> ReaderT CCEnv TCM [Bool])
-> TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Bool]
getCompiledArgUse QName
f
      -- #2248: no unused argument pruning for COMPILE'd functions
      Bool
isCompiled <- TCM Bool -> ReaderT CCEnv TCM Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Bool -> ReaderT CCEnv TCM Bool)
-> TCM Bool -> ReaderT CCEnv TCM Bool
forall a b. (a -> b) -> a -> b
$ Maybe HaskellPragma -> Bool
forall a. Maybe a -> Bool
isJust (Maybe HaskellPragma -> Bool)
-> TCM (Maybe HaskellPragma) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM (Maybe HaskellPragma)
getHaskellPragma QName
f
      let given :: VerboseLevel
given   = [TTerm] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [TTerm]
ts
          needed :: VerboseLevel
needed  = [Bool] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Bool]
used
          missing :: [Bool]
missing = VerboseLevel -> [Bool] -> [Bool]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
given [Bool]
used
          notUsed :: Bool -> Bool
notUsed = Bool -> Bool
not
      if Bool -> Bool
not Bool
isCompiled Bool -> Bool -> Bool
&& (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bool -> Bool
not [Bool]
used
        then if (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Bool -> Bool
notUsed [Bool]
missing then TTerm -> CC Exp
term (VerboseLevel -> TTerm -> TTerm
etaExpand (VerboseLevel
needed VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
given) TTerm
tm0) else do
          Exp
f <- TCMT IO Exp -> CC Exp
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Exp -> CC Exp) -> TCMT IO Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ QName -> Exp
HS.Var (QName -> Exp) -> TCMT IO QName -> TCMT IO Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> QName -> TCMT IO QName
xhqn String
"du" 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` [ TTerm
t | (TTerm
t, Bool
True) <- [TTerm] -> [Bool] -> [(TTerm, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TTerm]
ts ([Bool] -> [(TTerm, Bool)]) -> [Bool] -> [(TTerm, Bool)]
forall a b. (a -> b) -> a -> b
$ [Bool]
used [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
True ]
        else do
          Exp
f <- TCMT IO Exp -> CC Exp
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Exp -> CC Exp) -> TCMT IO Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ QName -> Exp
HS.Var (QName -> Exp) -> TCMT IO QName -> TCMT IO Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> QName -> TCMT IO QName
xhqn String
"d" 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  <- TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [Bool] -> ReaderT CCEnv TCM [Bool])
-> TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Bool]
getErasedConArgs QName
c
      let missing :: [Bool]
missing = VerboseLevel -> [Bool] -> [Bool]
forall a. VerboseLevel -> [a] -> [a]
drop ([TTerm] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [TTerm]
ts) [Bool]
erased
          notErased :: Bool -> Bool
notErased = Bool -> Bool
not
      case (Bool -> Bool) -> [Bool] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Bool -> Bool
notErased [Bool]
missing of
        -- If the constructor is fully applied or all missing arguments are retained,
        -- we can drop the erased arguments here, doing a complete job of dropping erased arguments.
        Bool
True  -> do
          Exp
f <- TCMT IO Exp -> CC Exp
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Exp -> CC Exp) -> TCMT IO Exp -> CC Exp
forall a b. (a -> b) -> a -> b
$ QName -> Exp
HS.Con (QName -> Exp) -> TCMT IO QName -> TCMT IO Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO QName
conhqn QName
c
          Exp -> Exp
hsCoerce Exp
f Exp -> [TTerm] -> CC Exp
`apps` [ TTerm
t | (TTerm
t, Bool
False) <- [TTerm] -> [Bool] -> [(TTerm, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TTerm]
ts [Bool]
erased ]
        -- Otherwise, we translate the eta-expanded constructor application.
        Bool
False -> do
          let n :: VerboseLevel
n = [Bool] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Bool]
missing
          Bool
-> ReaderT CCEnv TCM GHCModuleEnv -> ReaderT CCEnv TCM GHCModuleEnv
forall (f :: * -> *).
Applicative f =>
Bool -> f GHCModuleEnv -> f GHCModuleEnv
unless (VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
>= VerboseLevel
1) ReaderT CCEnv TCM GHCModuleEnv
forall a. HasCallStack => a
__IMPOSSIBLE__  -- We will add at least on TLam, not getting a busy loop here.
          TTerm -> CC Exp
term (TTerm -> CC Exp) -> TTerm -> CC Exp
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> TTerm -> TTerm
etaExpand ([Bool] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length [Bool]
missing) TTerm
tm0

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

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

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

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

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

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

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

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

alt :: Int -> T.TAlt -> CC HS.Alt
alt :: VerboseLevel -> TAlt -> ReaderT CCEnv TCM Alt
alt VerboseLevel
sc TAlt
a = do
  case TAlt
a of
    T.TACon {aCon :: TAlt -> QName
T.aCon = QName
c} -> do
      VerboseLevel
-> ([Name] -> ReaderT CCEnv TCM Alt) -> ReaderT CCEnv TCM Alt
forall a. VerboseLevel -> ([Name] -> CC a) -> CC a
intros (TAlt -> VerboseLevel
T.aArity TAlt
a) (([Name] -> ReaderT CCEnv TCM Alt) -> ReaderT CCEnv TCM Alt)
-> ([Name] -> ReaderT CCEnv TCM Alt) -> ReaderT CCEnv TCM Alt
forall a b. (a -> b) -> a -> b
$ \ [Name]
xs -> do
        [Bool]
erased <- TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [Bool] -> ReaderT CCEnv TCM [Bool])
-> TCM [Bool] -> ReaderT CCEnv TCM [Bool]
forall a b. (a -> b) -> a -> b
$ QName -> TCM [Bool]
getErasedConArgs QName
c
        Maybe QName
nil  <- TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName))
-> TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ String -> TCM (Maybe QName)
getBuiltinName String
builtinNil
        Maybe QName
cons <- TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName))
-> TCM (Maybe QName) -> ReaderT CCEnv TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ String -> TCM (Maybe QName)
getBuiltinName String
builtinCons
        QName
hConNm <-
          if | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
nil  -> QName -> ReaderT CCEnv TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> ReaderT CCEnv TCM QName)
-> QName -> ReaderT CCEnv TCM QName
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> Name
HS.Ident String
"[]"
             | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
cons -> QName -> ReaderT CCEnv TCM QName
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> ReaderT CCEnv TCM QName)
-> QName -> ReaderT CCEnv TCM QName
forall a b. (a -> b) -> a -> b
$ Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> Name
HS.Symbol String
":"
             | Bool
otherwise      -> TCMT IO QName -> ReaderT CCEnv TCM QName
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO QName -> ReaderT CCEnv TCM QName)
-> TCMT IO QName -> ReaderT CCEnv TCM QName
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO QName
conhqn QName
c
        Pat -> ReaderT CCEnv TCM Alt
mkAlt (QName -> [Pat] -> Pat
HS.PApp QName
hConNm ([Pat] -> Pat) -> [Pat] -> Pat
forall a b. (a -> b) -> a -> b
$ (Name -> Pat) -> [Name] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Pat
HS.PVar [ Name
x | (Name
x, Bool
False) <- [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Bool]
erased ])
    T.TAGuard TTerm
g TTerm
b -> do
      Exp
g <- TTerm -> CC Exp
term TTerm
g
      Exp
b <- TTerm -> CC Exp
term TTerm
b
      Alt -> ReaderT CCEnv TCM Alt
forall (m :: * -> *) a. Monad m => a -> m a
return (Alt -> ReaderT CCEnv TCM Alt) -> Alt -> ReaderT CCEnv TCM Alt
forall a b. (a -> b) -> a -> b
$ Pat -> Rhs -> Maybe Binds -> Alt
HS.Alt Pat
HS.PWildCard
                      ([GuardedRhs] -> Rhs
HS.GuardedRhss [[Stmt] -> Exp -> GuardedRhs
HS.GuardedRhs [Exp -> Stmt
HS.Qualifier Exp
g] Exp
b])
                      Maybe Binds
emptyBinds
    T.TALit { aLit :: TAlt -> Literal
T.aLit = LitQName Range
_ QName
q } -> Pat -> ReaderT CCEnv TCM Alt
mkAlt (QName -> Pat
litqnamepat QName
q)
    T.TALit { aLit :: TAlt -> Literal
T.aLit = l :: Literal
l@LitFloat{},   aBody :: TAlt -> TTerm
T.aBody = TTerm
b } -> String -> Exp -> TTerm -> ReaderT CCEnv TCM Alt
mkGuarded (TPrim -> String
treelessPrimName TPrim
T.PEqF) (Literal -> Exp
literal Literal
l) TTerm
b
    T.TALit { aLit :: TAlt -> Literal
T.aLit = LitString Range
_ String
s , aBody :: TAlt -> TTerm
T.aBody = TTerm
b } -> String -> Exp -> TTerm -> ReaderT CCEnv TCM Alt
mkGuarded String
"(==)" (String -> Exp
litString String
s) TTerm
b
    T.TALit {} -> Pat -> ReaderT CCEnv TCM Alt
mkAlt (Literal -> Pat
HS.PLit (Literal -> Pat) -> Literal -> Pat
forall a b. (a -> b) -> a -> b
$ Literal -> Literal
hslit (Literal -> Literal) -> Literal -> Literal
forall a b. (a -> b) -> a -> b
$ TAlt -> Literal
T.aLit TAlt
a)
  where
    mkGuarded :: String -> Exp -> TTerm -> ReaderT CCEnv TCM Alt
mkGuarded String
eq Exp
lit TTerm
b = do
      Exp
b  <- TTerm -> CC Exp
term TTerm
b
      let varName :: Name
varName = String -> Name
HS.Ident String
"l" -- only used locally in the guard
          pv :: Pat
pv = Name -> Pat
HS.PVar Name
varName
          v :: Exp
v  = Name -> Exp
hsVarUQ Name
varName
          guard :: Exp
guard =
            QName -> Exp
HS.Var (Name -> QName
HS.UnQual (String -> Name
HS.Ident String
eq)) Exp -> Exp -> Exp
`HS.App`
              Exp
v Exp -> Exp -> Exp
`HS.App` Exp
lit
      Alt -> ReaderT CCEnv TCM Alt
forall (m :: * -> *) a. Monad m => a -> m a
return (Alt -> ReaderT CCEnv TCM Alt) -> Alt -> ReaderT CCEnv TCM Alt
forall a b. (a -> b) -> a -> b
$ Pat -> Rhs -> Maybe Binds -> Alt
HS.Alt Pat
pv
                      ([GuardedRhs] -> Rhs
HS.GuardedRhss [[Stmt] -> Exp -> GuardedRhs
HS.GuardedRhs [Exp -> Stmt
HS.Qualifier Exp
guard] Exp
b])
                      Maybe Binds
emptyBinds

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

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

    -- ASR (2016-09-14): See Issue #2169.
    -- Ulf, 2016-09-28: and #2218.
    floatExp :: Double -> String -> HS.Exp
    floatExp :: Double -> String -> Exp
floatExp Double
x String
s
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
x = String -> Exp
rte String
"negativeZero"
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeInf  Double
x = String -> Exp
rte String
"negativeInfinity"
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
x     = String -> Exp
rte String
"positiveInfinity"
      | Double -> Bool
forall a. IEEE a => a -> Bool
isNegativeNaN Double
x  = String -> Exp
rte String
"negativeNaN"
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x          = String -> Exp
rte String
"positiveNaN"
      | Bool
otherwise        = String -> Exp
typed String
s

    rte :: String -> Exp
rte = QName -> Exp
HS.Var (QName -> Exp) -> (String -> QName) -> String -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ModuleName -> Name -> QName
HS.Qual ModuleName
mazRTE (Name -> QName) -> (String -> Name) -> String -> QName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
HS.Ident

    isNegativeInf :: a -> Bool
isNegativeInf a
x = a -> Bool
forall a. RealFloat a => a -> Bool
isInfinite a
x Bool -> Bool -> Bool
&& a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0.0
    isNegativeNaN :: a -> Bool
isNegativeNaN a
x = a -> Bool
forall a. RealFloat a => a -> Bool
isNaN a
x Bool -> Bool -> Bool
&& Bool -> Bool
not (a -> a -> Bool
forall a. IEEE a => a -> a -> Bool
identicalIEEE a
x (a
0.0 a -> a -> a
forall a. Fractional a => a -> a -> a
/ a
0.0))

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

litString :: String -> HS.Exp
litString :: String -> Exp
litString String
s =
  QName -> Exp
HS.Var (ModuleName -> Name -> QName
HS.Qual (String -> ModuleName
HS.ModuleName String
"Data.Text") (String -> Name
HS.Ident String
"pack")) Exp -> Exp -> Exp
`HS.App`
    (Literal -> Exp
HS.Lit (Literal -> Exp) -> Literal -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Literal
HS.String String
s)

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

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

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

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

condecl :: QName -> Induction -> TCM HS.ConDecl
condecl :: QName -> Induction -> TCMT IO ConDecl
condecl QName
q Induction
_ind = do
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  let Constructor{ conPars :: Defn -> VerboseLevel
conPars = VerboseLevel
np, conErased :: Defn -> Maybe [Bool]
conErased = Maybe [Bool]
erased } = Definition -> Defn
theDef Definition
def
  ([Type]
argTypes0, Type
_) <- Type -> TCM ([Type], Type)
hsTelApproximation (Definition -> Type
defType Definition
def)
  let argTypes :: [(Maybe Strictness, Type)]
argTypes   = [ (Strictness -> Maybe Strictness
forall a. a -> Maybe a
Just Strictness
HS.Lazy, Type
t)
                     -- Currently all constructors are lazy.
                   | (Type
t, Bool
False) <- [Type] -> [Bool] -> [(Type, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip (VerboseLevel -> [Type] -> [Type]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
np [Type]
argTypes0)
                                       ([Bool] -> Maybe [Bool] -> [Bool]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Bool]
erased [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ Bool -> [Bool]
forall a. a -> [a]
repeat Bool
False)
                   ]
  ConDecl -> TCMT IO ConDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (ConDecl -> TCMT IO ConDecl) -> ConDecl -> TCMT IO ConDecl
forall a b. (a -> b) -> a -> b
$ Name -> [(Maybe Strictness, Type)] -> ConDecl
HS.ConDecl (String -> QName -> Name
unqhname String
"C" QName
q) [(Maybe Strictness, Type)]
argTypes

compiledcondecl :: QName -> TCM HS.Decl
compiledcondecl :: QName -> TCMT IO Decl
compiledcondecl QName
q = do
  VerboseLevel
ar <- QName -> TCM VerboseLevel
erasedArity QName
q
  String
hsCon <- String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe String -> String)
-> TCMT IO (Maybe String) -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe String)
getHaskellConstructor QName
q
  let patVars :: [Pat]
patVars = (VerboseLevel -> Pat) -> [VerboseLevel] -> [Pat]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Pat
HS.PVar (Name -> Pat) -> (VerboseLevel -> Name) -> VerboseLevel -> Pat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> VerboseLevel -> Name
ihname String
"a") [VerboseLevel
0 .. VerboseLevel
ar VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
1]
  Decl -> TCMT IO Decl
forall (m :: * -> *) a. Monad m => a -> m a
return (Decl -> TCMT IO Decl) -> Decl -> TCMT IO Decl
forall a b. (a -> b) -> a -> b
$ Pat -> Pat -> Decl
HS.PatSyn (QName -> [Pat] -> Pat
HS.PApp (Name -> QName
HS.UnQual (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
$ String -> QName -> Name
unqhname String
"C" QName
q) [Pat]
patVars) (QName -> [Pat] -> Pat
HS.PApp (String -> QName
hsName String
hsCon) [Pat]
patVars)

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

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

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

infodecl :: QName -> [HS.Decl] -> [HS.Decl]
infodecl :: QName -> [Decl] -> [Decl]
infodecl QName
_ [] = []
infodecl QName
q [Decl]
ds =
  Name -> String -> Decl
fakeD (String -> QName -> Name
unqhname String
"name" QName
q) (String -> String
haskellStringLiteral (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q) Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl]
ds

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

copyRTEModules :: TCM ()
copyRTEModules :: TCM GHCModuleEnv
copyRTEModules = do
  String
dataDir <- IO String -> TCMT IO String
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IO String
getDataDir
  let srcDir :: String
srcDir = String
dataDir String -> String -> String
</> String
"MAlonzo" String -> String -> String
</> String
"src"
  (IO GHCModuleEnv -> TCM GHCModuleEnv
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO GHCModuleEnv -> TCM GHCModuleEnv)
-> (String -> IO GHCModuleEnv) -> String -> TCM GHCModuleEnv
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> IO GHCModuleEnv
copyDirContent String
srcDir) (String -> TCM GHCModuleEnv) -> TCMT IO String -> TCM GHCModuleEnv
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO String
compileDir

writeModule :: HS.Module -> TCM ()
writeModule :: Module -> TCM GHCModuleEnv
writeModule (HS.Module ModuleName
m [ModulePragma]
ps [ImportDecl]
imp [Decl]
ds) = do
  -- Note that GHC assumes that sources use ASCII or UTF-8.
  String
out <- ModuleName -> TCMT IO String
outFile ModuleName
m
  IO GHCModuleEnv -> TCM GHCModuleEnv
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO GHCModuleEnv -> TCM GHCModuleEnv)
-> IO GHCModuleEnv -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ String -> String -> IO GHCModuleEnv
UTF8.writeFile String
out (String -> IO GHCModuleEnv) -> String -> IO GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n") (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Module -> String
forall a. Pretty a => a -> String
prettyPrint (Module -> String) -> Module -> String
forall a b. (a -> b) -> a -> b
$
    ModuleName -> [ModulePragma] -> [ImportDecl] -> [Decl] -> Module
HS.Module ModuleName
m (ModulePragma
p ModulePragma -> [ModulePragma] -> [ModulePragma]
forall a. a -> [a] -> [a]
: [ModulePragma]
ps) [ImportDecl]
imp [Decl]
ds
  where
  p :: ModulePragma
p = [Name] -> ModulePragma
HS.LanguagePragma ([Name] -> ModulePragma) -> [Name] -> ModulePragma
forall a b. (a -> b) -> a -> b
$ (String -> Name) -> [String] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> Name
HS.Ident ([String] -> [Name]) -> [String] -> [Name]
forall a b. (a -> b) -> a -> b
$
        [ String
"EmptyDataDecls"
        , String
"EmptyCase"
        , String
"ExistentialQuantification"
        , String
"ScopedTypeVariables"
        , String
"NoMonomorphismRestriction"
        , String
"RankNTypes"
        , String
"PatternSynonyms"
        ]


outFile' :: Pretty a => a -> TCM (FilePath, FilePath)
outFile' :: a -> TCM (String, String)
outFile' a
m = do
  String
mdir <- TCMT IO String
compileDir
  let (String
fdir, String
fn) = String -> (String, String)
splitFileName (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ Char -> String -> String
repldot Char
pathSeparator (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$
                   a -> String
forall a. Pretty a => a -> String
prettyPrint a
m
  let dir :: String
dir = String
mdir String -> String -> String
</> String
fdir
      fp :: String
fp  = String
dir String -> String -> String
</> String -> String -> String
replaceExtension String
fn String
"hs"
  IO GHCModuleEnv -> TCM GHCModuleEnv
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO GHCModuleEnv -> TCM GHCModuleEnv)
-> IO GHCModuleEnv -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO GHCModuleEnv
createDirectoryIfMissing Bool
True String
dir
  (String, String) -> TCM (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
mdir, String
fp)
  where
  repldot :: Char -> String -> String
repldot Char
c = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
List.map ((Char -> Char) -> String -> String)
-> (Char -> Char) -> String -> String
forall a b. (a -> b) -> a -> b
$ \ Char
c' -> if Char
c' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'.' then Char
c else Char
c'

outFile :: HS.ModuleName -> TCM FilePath
outFile :: ModuleName -> TCMT IO String
outFile ModuleName
m = (String, String) -> String
forall a b. (a, b) -> b
snd ((String, String) -> String)
-> TCM (String, String) -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleName -> TCM (String, String)
forall a. Pretty a => a -> TCM (String, String)
outFile' ModuleName
m

outFile_ :: TCM FilePath
outFile_ :: TCMT IO String
outFile_ = ModuleName -> TCMT IO String
outFile (ModuleName -> TCMT IO String) -> TCM ModuleName -> TCMT IO String
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM ModuleName
curHsMod

callGHC :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM ()
callGHC :: GHCOptions -> IsMain -> Map ModuleName IsMain -> TCM GHCModuleEnv
callGHC GHCOptions
opts IsMain
modIsMain Map ModuleName IsMain
mods = do
  String
mdir    <- TCMT IO String
compileDir
  String
hsmod   <- ModuleName -> String
forall a. Pretty a => a -> String
prettyPrint (ModuleName -> String) -> TCM ModuleName -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM ModuleName
curHsMod
  ModuleName
agdaMod <- TCMT IO ModuleName
curMName
  let outputName :: Name
outputName = case ModuleName -> [Name]
mnameToList ModuleName
agdaMod of
        [] -> Name
forall a. HasCallStack => a
__IMPOSSIBLE__
        [Name]
ms -> [Name] -> Name
forall a. [a] -> a
last [Name]
ms
  (String
mdir, String
fp) <- ModuleName -> TCM (String, String)
forall a. Pretty a => a -> TCM (String, String)
outFile' (ModuleName -> TCM (String, String))
-> TCM ModuleName -> TCM (String, String)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM ModuleName
curHsMod
  let ghcopts :: [String]
ghcopts = GHCOptions -> [String]
optGhcFlags GHCOptions
opts

  let modIsReallyMain :: IsMain
modIsReallyMain = IsMain -> Maybe IsMain -> IsMain
forall a. a -> Maybe a -> a
fromMaybe IsMain
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe IsMain -> IsMain) -> Maybe IsMain -> IsMain
forall a b. (a -> b) -> a -> b
$ ModuleName -> Map ModuleName IsMain -> Maybe IsMain
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup ModuleName
agdaMod Map ModuleName IsMain
mods
      isMain :: IsMain
isMain = IsMain -> IsMain -> IsMain
forall a. Monoid a => a -> a -> a
mappend IsMain
modIsMain IsMain
modIsReallyMain  -- both need to be IsMain

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

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

  String
compiler <- TCMT IO String -> TCMT IO (Maybe String) -> TCMT IO String
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (String -> TCMT IO String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"ghc") (CommandLineOptions -> Maybe String
optWithCompiler (CommandLineOptions -> Maybe String)
-> TCMT IO CommandLineOptions -> TCMT IO (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO CommandLineOptions
forall (m :: * -> *). HasOptions m => m CommandLineOptions
commandLineOptions)

  -- 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
  Bool -> String -> [String] -> TCM GHCModuleEnv
callCompiler Bool
doCall String
compiler [String]
args