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           = "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 ['c']  ["compile", "ghc"] (Flag GHCOptions -> ArgDescr (Flag GHCOptions)
forall a. a -> ArgDescr a
NoArg Flag GHCOptions
forall (f :: * -> *). Applicative f => GHCOptions -> f GHCOptions
enable)
                    "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 []     ["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)
                    "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 []     ["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 "GHC-FLAG")
                    "give the flag GHC-FLAG to GHC"
    ]
  where
    enable :: GHCOptions -> f GHCOptions
enable      o :: 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 o :: 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 f :: String
f   o :: 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 ghcOpts :: 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
$ "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 opts :: GHCOptions
opts isMain :: IsMain
isMain mods :: 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 _ isMain :: IsMain
isMain m :: ModuleName
m ifile :: 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 "compile.ghc" 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]
++ " : 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 "compile.ghc" 1 (String -> TCM GHCModuleEnv) -> String -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
m, String
ifile, String
out] "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 _ _ isMain :: IsMain
isMain _ defs :: [[Decl]]
defs = do
  ModuleName
m      <- TCM ModuleName
curHsMod
  [ImportDecl]
imps   <- TCM [ImportDecl]
imports
  -- Get content of FOREIGN pragmas.
  (headerPragmas :: [String]
headerPragmas, hsImps :: [String]
hsImps, code :: [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 _ env :: GHCModuleEnv
env isMain :: IsMain
isMain def :: 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 q :: 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
  _ -> 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 m :: 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 _env :: GHCModuleEnv
_env _isMain :: 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 "compile.ghc.definition" 10 (TCM Doc -> TCM GHCModuleEnv) -> TCM Doc -> TCM GHCModuleEnv
forall a b. (a -> b) -> a -> b
$
    ("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
<> "."
  [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return []
definition env :: GHCModuleEnv
env isMain :: 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 "compile.ghc.definition" 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
    [ ("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
<> ":"
    , VerboseLevel -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => VerboseLevel -> m Doc -> m Doc
nest 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

      _ | Just (HsDefn r :: Range
r hs :: 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
                "\"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 "_") | 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 "d" QName
q
        Just true :: QName
true  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinTrue
        Just false :: 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 "Bool" 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
$ \ p :: 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 "Ignoring GHC pragma for builtin lists; they always compile to Haskell lists."
        let d :: Name
d = String -> QName -> Name
unqhname "d" QName
q
            t :: Name
t = String -> QName -> Name
unqhname "T" QName
q
        Just nil :: QName
nil  <- String -> TCM (Maybe QName)
getBuiltinName String
builtinNil
        Just cons :: QName
cons <- String -> TCM (Maybe QName)
getBuiltinName String
builtinCons
        let vars :: (Name -> b) -> VerboseLevel -> [b]
vars f :: Name -> b
f n :: 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 "a") [0 .. VerboseLevel
n VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 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
- 1)) (String -> Type
HS.FakeType "[]")
                 , [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
      _ | 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 sharp :: 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 "d" QName
q
            err :: String
err = "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 "MAlonzo.RTE.Infinity" 2
                 , [Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match Name
d [Name -> Pat
HS.PVar (String -> VerboseLevel -> Name
ihname "a" 0)]
                     (Exp -> Rhs
HS.UnGuardedRhs (String -> Exp
HS.FakeExp ("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 r :: Range
r ty :: 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 r :: Range
r ty :: String
ty hsCons :: [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 "compile.ghc.definition" 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
$
          [ "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 r :: Range
r ty :: String
ty hsCons :: [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
          _ -> 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 mhe :: Maybe HaskellPragma
mhe fun :: 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 r :: Range
r name :: 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
              "\"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)
      _ -> [Decl] -> TCM [Decl]
forall (m :: * -> *) a. Monad m => a -> m a
return [Decl]
ccls

  functionViaTreeless :: QName -> TCM [HS.Decl]
  functionViaTreeless :: QName -> TCM [Decl]
functionViaTreeless q :: 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
$ \ treeless :: 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
    (argTypes0 :: [Type]
argTypes0, resType :: 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
> 0 -> VerboseLevel
i VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1
                 _ -> 0
        argTypes :: [Type]
argTypes  = VerboseLevel -> [Type] -> [Type]
forall a. VerboseLevel -> [a] -> [a]
drop VerboseLevel
pars [Type]
argTypes0
        argTypesS :: [Type]
argTypesS = [ Type
t | (t :: Type
t, 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 (ps :: [Pat]
ps, b :: Exp
b) = Exp -> ([Pat], Exp)
lamView Exp
e
        lamView :: Exp -> ([Pat], Exp)
lamView e :: Exp
e =
          case Exp
e of
            HS.Lambda ps :: [Pat]
ps b :: Exp
b -> ([Pat]
ps, Exp
b)
            b :: Exp
b              -> ([], Exp
b)

        tydecl :: Name -> t Type -> Type -> Decl
tydecl  f :: Name
f ts :: t Type
ts t :: 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 f :: Name
f ps :: [Pat]
ps b :: 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 f :: Name
f ts :: [Type]
ts t :: Type
t ps :: [Pat]
ps b :: 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
    (ps0 :: [Pat]
ps0, _) <- 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 x :: Name
x), 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 [m0 :: Match
m0, HS.Match dn :: Name
dn ps :: [Pat]
ps rhs :: Rhs
rhs emptyBinds :: Maybe Binds
emptyBinds] : fbs :: [Decl]
fbs@(_:_)) =
          [[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 fbs :: [Decl]
fbs = [Decl]
fbs

  fbWithType :: HS.Type -> HS.Exp -> [HS.Decl]
  fbWithType :: Type -> Exp -> [Decl]
fbWithType ty :: Type
ty e :: Exp
e =
    [ [Name] -> Type -> Decl
HS.TypeSig [String -> QName -> Name
unqhname "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 e :: Exp
e  = [[Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match (String -> QName -> Name
unqhname "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
$ "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 q :: QName
q np :: VerboseLevel
np cs :: [QName]
cs hsTy :: String
hsTy hsCons :: [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 f :: [Name] -> f [Name]
f e :: CCEnv
e =  (\ ns' :: [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 f :: [Name] -> f [Name]
f e :: CCEnv
e = (\ cxt :: [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 "v") [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 i :: VerboseLevel
i xs :: [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 n :: VerboseLevel
n _ | VerboseLevel
n VerboseLevel -> VerboseLevel -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = CC a
forall a. HasCallStack => a
__IMPOSSIBLE__
freshNames n :: VerboseLevel
n cont :: [Name] -> CC a
cont = do
  (xs :: [Name]
xs, rest :: [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 n :: VerboseLevel
n cont :: [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
$ \xs :: [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 q :: QName
q hs :: 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 "check" QName
q] Type
ty
         , [Match] -> Decl
HS.FunBind [Name -> [Pat] -> Rhs -> Maybe Binds -> Match
HS.Match (String -> QName -> Name
unqhname "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 q :: QName
q ty :: String
ty n :: VerboseLevel
n cs :: [QName]
cs hsCons :: [String]
hsCons = do
  let tvs :: [String]
tvs = [ "a" String -> String -> String
forall a. [a] -> [a] -> [a]
++ VerboseLevel -> String
forall a. Show a => a -> String
show VerboseLevel
i | VerboseLevel
i <- [1..VerboseLevel
n] ]
      makeClause :: QName -> String -> TCMT IO Alt
makeClause c :: QName
c hsc :: 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 "x") [Alt]
cs

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

closedTerm :: T.TTerm -> TCM HS.Exp
closedTerm :: TTerm -> TCMT IO Exp
closedTerm v :: 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 e :: VerboseLevel
e _ d :: TTerm
d [TACon c1 :: QName
c1 0 b1 :: TTerm
b1, TACon c2 :: QName
c2 0 b2 :: 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  c :: 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 c :: 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 t :: 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 tm0 :: 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
>>= \ tm0 :: TTerm
tm0 -> do
  let ((hasCoerce :: Bool
hasCoerce, t :: TTerm
t), ts :: [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 T.PIf, [c :: TTerm
c, x :: TTerm
x, y :: 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 f :: QName
f, ts :: [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 "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 | (t :: TTerm
t, 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 "d" QName
f  -- use original (non-stripped) function
          Exp -> Exp
coe Exp
f Exp -> [TTerm] -> CC Exp
`apps` [TTerm]
ts

    (T.TCon c :: QName
c, ts :: [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.
        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 | (t :: TTerm
t, 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.
        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
>= 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.
    (t :: TTerm
t, ts :: [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
>>= \ t' :: 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 (\ h :: Exp
h a :: 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 n :: VerboseLevel
n t :: 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 i :: 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 t :: TTerm
t    -> VerboseLevel -> ([Name] -> CC Exp) -> CC Exp
forall a. VerboseLevel -> ([Name] -> CC a) -> CC a
intros 1 (([Name] -> CC Exp) -> CC Exp) -> ([Name] -> CC Exp) -> CC Exp
forall a b. (a -> b) -> a -> b
$ \ [x :: 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 t1 :: TTerm
t1 t2 :: 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 1 (([Name] -> CC Exp) -> CC Exp) -> ([Name] -> CC Exp) -> CC Exp
forall a b. (a -> b) -> a -> b
$ \[x :: 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 sc :: VerboseLevel
sc ct :: CaseInfo
ct def :: TTerm
def alts :: [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 l :: 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 p :: 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
  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
  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
  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 e :: 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
    T.TUnreachable -> Exp
rtmUnreachableError

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

compilePrim :: T.TPrim -> HS.Exp
compilePrim :: TPrim -> Exp
compilePrim s :: 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 sc :: VerboseLevel
sc a :: 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
$ \ xs :: [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 "[]"
             | 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 ":"
             | 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 | (x :: Name
x, False) <- [Name] -> [Bool] -> [(Name, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
xs [Bool]
erased ])
    T.TAGuard g :: TTerm
g b :: 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 _ q :: 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 _ s :: String
s , aBody :: TAlt -> TTerm
T.aBody = TTerm
b } -> String -> Exp -> TTerm -> ReaderT CCEnv TCM Alt
mkGuarded "(==)" (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 eq :: String
eq lit :: Exp
lit b :: TTerm
b = do
      Exp
b  <- TTerm -> CC Exp
term TTerm
b
      let varName :: Name
varName = String -> Name
HS.Ident "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
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 l :: Literal
l = case Literal
l of
  LitNat    _ _   -> String -> Exp
typed "Integer"
  LitWord64 _ _   -> String -> Exp
typed "MAlonzo.RTE.Word64"
  LitFloat  _ x :: Double
x   -> Double -> String -> Exp
floatExp Double
x "Double"
  LitQName  _ x :: QName
x   -> QName -> Exp
litqname QName
x
  LitString _ s :: String
s   -> String -> Exp
litString String
s
  _               -> 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 x :: Double
x s :: String
s
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeZero Double
x = String -> Exp
rte "negativeZero"
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNegativeInf  Double
x = String -> Exp
rte "negativeInfinity"
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isInfinite Double
x     = String -> Exp
rte "positiveInfinity"
      | Double -> Bool
forall a. IEEE a => a -> Bool
isNegativeNaN Double
x  = String -> Exp
rte "negativeNaN"
      | Double -> Bool
forall a. RealFloat a => a -> Bool
isNaN Double
x          = String -> Exp
rte "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 x :: 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
< 0.0
    isNegativeNaN :: a -> Bool
isNegativeNaN x :: 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 (0.0 a -> a -> a
forall a. Fractional a => a -> a -> a
/ 0.0))

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

litString :: String -> HS.Exp
litString :: String -> Exp
litString s :: String
s =
  QName -> Exp
HS.Var (ModuleName -> Name -> QName
HS.Qual (String -> ModuleName
HS.ModuleName "Data.Text") (String -> Name
HS.Ident "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 x :: QName
x =
  String -> Exp
rteCon "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 "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 name :: 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 n :: Word64
n m :: 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 NonAssoc   = String -> Exp
rteCon "NonAssoc"
    litAssoc LeftAssoc  = String -> Exp
rteCon "LeftAssoc"
    litAssoc RightAssoc = String -> Exp
rteCon "RightAssoc"

    litPrec :: FixityLevel -> Exp
litPrec Unrelated   = String -> Exp
rteCon "Unrelated"
    litPrec (Related l :: Double
l) = String -> Exp
rteCon "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 x :: 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 "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 n :: Word64
n m :: 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 q :: QName
q _ind :: 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
  (argTypes0 :: [Type]
argTypes0, _) <- 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.
                   | (t :: Type
t, 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 "C" QName
q) [(Maybe Strictness, Type)]
argTypes

compiledcondecl :: QName -> TCM HS.Decl
compiledcondecl :: QName -> TCMT IO Decl
compiledcondecl q :: 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 "a") [0 .. VerboseLevel
ar VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 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 "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 q :: QName
q hsT :: String
hsT arity :: VerboseLevel
arity =
  Name -> [TyVarBind] -> Type -> Decl
HS.TypeDecl (String -> QName -> Name
unqhname "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 "a" VerboseLevel
i | VerboseLevel
i <- [0 .. VerboseLevel
arity VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 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 q :: QName
q ind :: Induction
ind npar :: VerboseLevel
npar cds :: [ConDecl]
cds cl :: 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
  (tn :: Name
tn, vn :: Name
vn) = (String -> QName -> Name
unqhname "T" QName
q, String -> QName -> Name
unqhname "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 "a" VerboseLevel
i | VerboseLevel
i <- [0 .. VerboseLevel
npar VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- 1]]

  -- Inductive data types consisting of a single constructor with a
  -- single argument are translated into newtypes.
  (kind :: DataOrNew
kind, cds' :: [ConDecl]
cds') = case (Induction
ind, [ConDecl]
cds) of
    (Inductive, [HS.ConDecl c :: Name
c [(_, t :: 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.
    _ -> (DataOrNew
HS.DataType, [ConDecl]
cds)

infodecl :: QName -> [HS.Decl] -> [HS.Decl]
infodecl :: QName -> [Decl] -> [Decl]
infodecl _ [] = []
infodecl q :: QName
q ds :: [Decl]
ds =
  Name -> String -> Decl
fakeD (String -> QName -> Name
unqhname "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
</> "MAlonzo" 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 m :: ModuleName
m ps :: [ModulePragma]
ps imp :: [ImportDecl]
imp ds :: [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]
++ "\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
$
        [ "EmptyDataDecls"
        , "EmptyCase"
        , "ExistentialQuantification"
        , "ScopedTypeVariables"
        , "NoMonomorphismRestriction"
        , "RankNTypes"
        , "PatternSynonyms"
        ]


outFile' :: Pretty a => a -> TCM (FilePath, FilePath)
outFile' :: a -> TCM (String, String)
outFile' m :: a
m = do
  String
mdir <- TCMT IO String
compileDir
  let (fdir :: String
fdir, fn :: 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 "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 c :: 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
$ \ c' :: Char
c' -> if Char
c' Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '.' then Char
c else Char
c'

outFile :: HS.ModuleName -> TCM FilePath
outFile :: ModuleName -> TCMT IO String
outFile m :: 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 opts :: GHCOptions
opts modIsMain :: IsMain
modIsMain mods :: 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__
        ms :: [Name]
ms -> [Name] -> Name
forall a. [a] -> a
last [Name]
ms
  (mdir :: String
mdir, fp :: 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 "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]
forall a. [a] -> [a] -> [a]
++
                             String -> [TCM Doc]
forall (m :: * -> *). Monad m => String -> [m Doc]
pwords "Use --no-main to suppress this warning.")

  let overridableArgs :: [String]
overridableArgs =
        [ "-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 ["-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]
++
        [ "-Werror"]
      otherArgs :: [String]
otherArgs       =
        [ "-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 ["-main-is", String
hsmod] else []) [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
        [ String
fp
        , "--make"
        , "-fwarn-incomplete-patterns"
        , "-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 "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