{-|
Module      : IRTS.Compiler
Description : Coordinates the compilation process.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, NamedFieldPuns, PatternGuards,
             TypeSynonymInstances #-}

module IRTS.Compiler(compile, generate) where

import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Erasure
import Idris.Error
import Idris.Options
import Idris.Output
import IRTS.CodegenC
import IRTS.CodegenCommon
import IRTS.Defunctionalise
import IRTS.DumpBC
import IRTS.Exports
import IRTS.Inliner
import IRTS.LangOpts
import IRTS.Portable
import IRTS.Simplified

import Prelude hiding (id, (.))

import Control.Category
import Control.Monad.State
import Data.List
import qualified Data.Map as M
import Data.Maybe (maybe)
import Data.Ord
import qualified Data.Set as S
import System.Directory
import System.Exit
import System.IO
import System.Process

-- |  Compile to simplified forms and return CodegenInfo
compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
compile codegen :: Codegen
codegen f :: FilePath
f mtm :: Maybe Term
mtm = do
        Int -> FilePath -> Idris ()
logCodeGen 1 "Compiling Output."
        Int -> FilePath -> Idris ()
iReport 2 "Compiling Output."
        Idris ()
checkMVs  -- check for undefined metavariables
        Idris ()
checkTotality -- refuse to compile if there are totality problems
        [ExportIFace]
exports <- Idris [ExportIFace]
findExports
        let rootNames :: [Name]
rootNames = case Maybe Term
mtm of
                             Nothing -> []
                             Just t :: Term
t -> Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
t

        Int -> FilePath -> Idris ()
logCodeGen 1 "Running Erasure Analysis"
        Int -> FilePath -> Idris ()
iReport 3 "Running Erasure Analysis"
        [Name]
reachableNames <- [Name] -> Idris [Name]
performUsageAnalysis
                              ([Name]
rootNames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [ExportIFace] -> [Name]
getExpNames [ExportIFace]
exports)
        [(Name, LDecl)]
maindef <- case Maybe Term
mtm of
                        Nothing -> [(Name, LDecl)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
                        Just tm :: Term
tm -> do LDecl
md <- Term -> Idris LDecl
irMain Term
tm
                                      Int -> FilePath -> Idris ()
logCodeGen 1 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "MAIN: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LDecl -> FilePath
forall a. Show a => a -> FilePath
show LDecl
md
                                      [(Name, LDecl)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int -> FilePath -> Name
sMN 0 "runMain", LDecl
md)]
        [FilePath]
objs <- Codegen -> Idris [FilePath]
getObjectFiles Codegen
codegen
        [FilePath]
libs <- Codegen -> Idris [FilePath]
getLibs Codegen
codegen
        [FilePath]
flags <- Codegen -> Idris [FilePath]
getFlags Codegen
codegen
        [FilePath]
hdrs <- Codegen -> Idris [FilePath]
getHdrs Codegen
codegen
        [FilePath]
impdirs <- FilePath -> Idris [FilePath]
rankedImportDirs FilePath
f
        [(Name, TTDecl)]
ttDeclarations <- [Name] -> Idris [(Name, TTDecl)]
getDeclarations [Name]
reachableNames
        [(Name, LDecl)]
defsIn <- [Name] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
mkDecls [Name]
reachableNames
        -- if no 'main term' given, generate interface files
        let iface :: Bool
iface = case Maybe Term
mtm of
                         Nothing -> Bool
True
                         Just _ -> Bool
False

        let defs :: [(Name, LDecl)]
defs = [(Name, LDecl)]
defsIn [(Name, LDecl)] -> [(Name, LDecl)] -> [(Name, LDecl)]
forall a. [a] -> [a] -> [a]
++ [(Name, LDecl)]
maindef

        -- Inlined top level LDecl made here
        let defsInlined :: [(Name, LDecl)]
defsInlined = [(Name, LDecl)] -> [(Name, LDecl)]
inlineAll [(Name, LDecl)]
defs
        let defsUniq :: [(Name, LDecl)]
defsUniq = ((Name, LDecl) -> (Name, LDecl))
-> [(Name, LDecl)] -> [(Name, LDecl)]
forall a b. (a -> b) -> [a] -> [b]
map (LDefs -> (Name, LDecl) -> (Name, LDecl)
allocUnique ([(Name, LDecl)] -> LDefs -> LDefs
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, LDecl)]
defsInlined LDefs
forall k a. Map k a
emptyContext))
                           [(Name, LDecl)]
defsInlined

        Int -> FilePath -> Idris ()
logCodeGen 1 "Inlining"

        Maybe FilePath
dumpCases <- Idris (Maybe FilePath)
getDumpCases
        case Maybe FilePath
dumpCases of
            Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just f :: FilePath
f -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeFile FilePath
f ([(Name, LDecl)] -> FilePath
showCaseTrees [(Name, LDecl)]
defsUniq)

        let (nexttag :: Int
nexttag, tagged :: [(Name, LDecl)]
tagged) = Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
addTags 65536 ([(Name, LDecl)] -> [(Name, LDecl)]
liftAll [(Name, LDecl)]
defsInlined)
        let ctxtIn :: LDefs
ctxtIn = [(Name, LDecl)] -> LDefs -> LDefs
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, LDecl)]
tagged LDefs
forall k a. Map k a
emptyContext

        Int -> FilePath -> Idris ()
logCodeGen 1 "Defunctionalising"
        Int -> FilePath -> Idris ()
iReport 3 "Defunctionalising"
        let defuns_in :: DDefs
defuns_in = Int -> LDefs -> DDefs
defunctionalise Int
nexttag LDefs
ctxtIn
        Int -> FilePath -> Idris ()
logCodeGen 5 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ DDefs -> FilePath
forall a. Show a => a -> FilePath
show DDefs
defuns_in
        Int -> FilePath -> Idris ()
logCodeGen 1 "Inlining"
        Int -> FilePath -> Idris ()
iReport 3 "Inlining"
        let defuns :: DDefs
defuns = DDefs -> DDefs
inline DDefs
defuns_in
        Int -> FilePath -> Idris ()
logCodeGen 5 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ DDefs -> FilePath
forall a. Show a => a -> FilePath
show DDefs
defuns
        Int -> FilePath -> Idris ()
logCodeGen 1 "Resolving variables for CG"

        let checked :: TC [(Name, SDecl)]
checked = DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
simplifyDefs DDefs
defuns (DDefs -> [(Name, DDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist DDefs
defuns)
        OutputType
outty <- Idris OutputType
outputTy
        Maybe FilePath
dumpDefun <- Idris (Maybe FilePath)
getDumpDefun
        case Maybe FilePath
dumpDefun of
            Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just f :: FilePath
f -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeFile FilePath
f (DDefs -> FilePath
dumpDefuns DDefs
defuns)
        FilePath
triple <- Idris FilePath
Idris.AbsSyntax.targetTriple
        FilePath
cpu <- Idris FilePath
Idris.AbsSyntax.targetCPU
        Int -> FilePath -> Idris ()
logCodeGen 1 "Generating Code."
        Int -> FilePath -> Idris ()
iReport 2 "Generating Code."
        case TC [(Name, SDecl)]
checked of
            OK c :: [(Name, SDecl)]
c -> do CodegenInfo -> Idris CodegenInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (CodegenInfo -> Idris CodegenInfo)
-> CodegenInfo -> Idris CodegenInfo
forall a b. (a -> b) -> a -> b
$ FilePath
-> OutputType
-> FilePath
-> FilePath
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> DbgLevel
-> [(Name, SDecl)]
-> [(Name, DDecl)]
-> [(Name, LDecl)]
-> Bool
-> [ExportIFace]
-> [(Name, TTDecl)]
-> CodegenInfo
CodegenInfo FilePath
f OutputType
outty FilePath
triple FilePath
cpu
                                            [FilePath]
hdrs [FilePath]
impdirs [FilePath]
objs [FilePath]
libs [FilePath]
flags
                                            DbgLevel
NONE [(Name, SDecl)]
c (DDefs -> [(Name, DDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist DDefs
defuns)
                                            [(Name, LDecl)]
tagged Bool
iface [ExportIFace]
exports
                                            [(Name, TTDecl)]
ttDeclarations
            Error e :: Err
e -> Err -> Idris CodegenInfo
forall a. Err -> Idris a
ierror Err
e
  where checkMVs :: Idris ()
checkMVs = do IState
i <- Idris IState
getIState
                      case ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs of
                            [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                            ms :: [Name]
ms -> do FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "WARNING: There are incomplete holes:\n " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
ms
                                     FilePath -> Idris ()
iputStrLn "\nEvaluation of any of these will crash at run time."
                                     () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        checkTotality :: Idris ()
checkTotality = do IState
i <- Idris IState
getIState
                           case IState -> [(FC, FilePath)]
idris_totcheckfail IState
i of
                             [] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                             ((fc :: FC
fc, msg :: FilePath
msg):fs :: [(FC, FilePath)]
fs) -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (FilePath -> Err) -> FilePath -> Idris ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err) -> (FilePath -> Err) -> FilePath -> Err
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Cannot compile:\n  " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
msg

generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
generate codegen :: Codegen
codegen mainmod :: FilePath
mainmod ir :: CodegenInfo
ir
  = case Codegen
codegen of
       -- Built-in code generators (FIXME: lift these out!)
       Via _ "c" -> CodegenInfo -> IO ()
codegenC CodegenInfo
ir
       -- Any external code generator
       Via fm :: IRFormat
fm cg :: FilePath
cg -> do FilePath
input <- case IRFormat
fm of
                                    IBCFormat -> FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
mainmod
                                    JSONFormat -> do
                                        FilePath
tempdir <- IO FilePath
getTemporaryDirectory
                                        (fn :: FilePath
fn, h :: Handle
h) <- FilePath -> FilePath -> IO (FilePath, Handle)
openTempFile FilePath
tempdir "idris-cg.json"
                                        Handle -> CodegenInfo -> IO ()
writePortable Handle
h CodegenInfo
ir
                                        Handle -> IO ()
hClose Handle
h
                                        FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
fn
                       let cmd :: FilePath
cmd = "idris-codegen-" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
cg
                           args :: [FilePath]
args = [FilePath
input, "-o", CodegenInfo -> FilePath
outputFile CodegenInfo
ir] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ CodegenInfo -> [FilePath]
compilerFlags CodegenInfo
ir
                       ExitCode
exit <- FilePath -> [FilePath] -> IO ExitCode
rawSystem FilePath
cmd (if CodegenInfo -> Bool
interfaces CodegenInfo
ir then "--interface" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
args else [FilePath]
args)
                       Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ExitCode
exit ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
/= ExitCode
ExitSuccess) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                            FilePath -> IO ()
putStrLn ("FAILURE: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
cmd FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. Show a => a -> FilePath
show [FilePath]
args)
       Bytecode -> [(Name, SDecl)] -> FilePath -> IO ()
dumpBC (CodegenInfo -> [(Name, SDecl)]
simpleDecls CodegenInfo
ir) (CodegenInfo -> FilePath
outputFile CodegenInfo
ir)

irMain :: TT Name -> Idris LDecl
irMain :: Term -> Idris LDecl
irMain tm :: Term
tm = do
    LExp
i <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm (Int -> FilePath -> Name
sMN 0 "runMain") Vars
forall k a. Map k a
M.empty [] Term
tm
    LDecl -> Idris LDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (LDecl -> Idris LDecl) -> LDecl -> Idris LDecl
forall a b. (a -> b) -> a -> b
$ [LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun [] (Int -> FilePath -> Name
sMN 0 "runMain") [] (LExp -> LExp
LForce LExp
i)

mkDecls :: [Name] -> Idris [(Name, LDecl)]
mkDecls :: [Name] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
mkDecls used :: [Name]
used
    = do IState
i <- Idris IState
getIState
         let ds :: [(Name, Def)]
ds = ((Name, Def) -> Bool) -> [(Name, Def)] -> [(Name, Def)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: Name
n, d :: Def
d) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
used Bool -> Bool -> Bool
|| Def -> Bool
isCon Def
d) ([(Name, Def)] -> [(Name, Def)]) -> [(Name, Def)] -> [(Name, Def)]
forall a b. (a -> b) -> a -> b
$ Context -> [(Name, Def)]
ctxtAlist (IState -> Context
tt_ctxt IState
i)
         [(Name, LDecl)]
decls <- ((Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl))
-> [(Name, Def)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl)
build [(Name, Def)]
ds
         [(Name, LDecl)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, LDecl)]
decls

getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
getDeclarations :: [Name] -> Idris [(Name, TTDecl)]
getDeclarations used :: [Name]
used
    = do IState
i <- Idris IState
getIState
         let ds :: [(Name, TTDecl)]
ds = ((Name, TTDecl) -> Bool) -> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: Name
n, (d :: Def
d,_,_,_,_,_)) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
used Bool -> Bool -> Bool
|| Def -> Bool
isCon Def
d) ([(Name, TTDecl)] -> [(Name, TTDecl)])
-> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a b. (a -> b) -> a -> b
$ ((Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist (Ctxt TTDecl -> [(Name, TTDecl)])
-> (IState -> Ctxt TTDecl) -> IState -> [(Name, TTDecl)]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Context -> Ctxt TTDecl
definitions (Context -> Ctxt TTDecl)
-> (IState -> Context) -> IState -> Ctxt TTDecl
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Context
tt_ctxt) IState
i)
         [(Name, TTDecl)] -> Idris [(Name, TTDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TTDecl)]
ds

showCaseTrees :: [(Name, LDecl)] -> String
showCaseTrees :: [(Name, LDecl)] -> FilePath
showCaseTrees = FilePath -> [FilePath] -> FilePath
showSep "\n\n" ([FilePath] -> FilePath)
-> ([(Name, LDecl)] -> [FilePath]) -> [(Name, LDecl)] -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Name, LDecl) -> FilePath) -> [(Name, LDecl)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Name, LDecl) -> FilePath
forall a. Show a => (a, LDecl) -> FilePath
showCT ([(Name, LDecl)] -> [FilePath])
-> ([(Name, LDecl)] -> [(Name, LDecl)])
-> [(Name, LDecl)]
-> [FilePath]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Name, LDecl) -> (Name, LDecl) -> Ordering)
-> [(Name, LDecl)] -> [(Name, LDecl)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Name, LDecl) -> FilePath)
-> (Name, LDecl) -> (Name, LDecl) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Name, LDecl) -> FilePath
defnRank)
  where
    showCT :: (a, LDecl) -> FilePath
showCT (n :: a
n, LFun opts :: [LOpt]
opts f :: Name
f args :: [Name]
args lexp :: LExp
lexp)
       = FilePath
showOpts FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
         a -> FilePath
forall a. Show a => a -> FilePath
show a
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep " " ((Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show [Name]
args) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " =\n\t"
            FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LExp -> FilePath
forall a. Show a => a -> FilePath
show LExp
lexp
      where
        showOpts :: FilePath
showOpts | LOpt
Inline LOpt -> [LOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [LOpt]
opts = "%inline "
                 | Bool
otherwise = ""
    showCT (n :: a
n, LConstructor c :: Name
c t :: Int
t a :: Int
a) = "data " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
a

    defnRank :: (Name, LDecl) -> String
    defnRank :: (Name, LDecl) -> FilePath
defnRank (n :: Name
n, LFun _ _ _ _)       = "1" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
    defnRank (n :: Name
n, LConstructor _ _ _) = "2" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n

    nameRank :: Name -> String
    nameRank :: Name -> FilePath
nameRank (UN s :: Text
s)   = "1" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
s
    nameRank (MN i :: Int
i s :: Text
s) = "2" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i
    nameRank (NS n :: Name
n ns :: [Text]
ns) = "3" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Text -> FilePath) -> [Text] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> FilePath
forall a. Show a => a -> FilePath
show ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
ns) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
    nameRank (SN sn :: SpecialName
sn) = "4" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SpecialName -> FilePath
snRank SpecialName
sn
    nameRank n :: Name
n = "5" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n

    snRank :: SpecialName -> String
    snRank :: SpecialName -> FilePath
snRank (WhereN i :: Int
i n :: Name
n n' :: Name
n') = "1" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i
    snRank (ImplementationN n :: Name
n args :: [Text]
args) = "2" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Text -> FilePath) -> [Text] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> FilePath
forall a. Show a => a -> FilePath
show [Text]
args
    snRank (ParentN n :: Name
n s :: Text
s) = "3" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
s
    snRank (MethodN n :: Name
n) = "4" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
    snRank (CaseN _ n :: Name
n) = "5" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
    snRank (ImplementationCtorN n :: Name
n) = "7" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
    snRank (WithN i :: Int
i n :: Name
n) = "8" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i

isCon :: Def -> Bool
isCon (TyDecl _ _) = Bool
True
isCon _ = Bool
False

build :: (Name, Def) -> Idris (Name, LDecl)
build :: (Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl)
build (n :: Name
n, d :: Def
d)
    = do IState
i <- Idris IState
getIState
         case Name -> IState -> Maybe (Int, PrimFn)
getPrim Name
n IState
i of
              Just (ar :: Int
ar, op :: PrimFn
op) ->
                  let args :: [Name]
args = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Int
x -> Int -> FilePath -> Name
sMN Int
x "op") [0..] in
                      (Name, LDecl) -> StateT IState (ExceptT Err IO) (Name, LDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, ([LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun [] Name
n (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
ar [Name]
args)
                                         (PrimFn -> [LExp] -> LExp
LOp PrimFn
op ((Name -> LExp) -> [Name] -> [LExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> LExp
LV (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
ar [Name]
args)))))
              _ -> do LDecl
def <- Name -> Def -> Idris LDecl
mkLDecl Name
n Def
d
                      Int -> FilePath -> Idris ()
logCodeGen 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Compiled " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " =\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LDecl -> FilePath
forall a. Show a => a -> FilePath
show LDecl
def
                      (Name, LDecl) -> StateT IState (ExceptT Err IO) (Name, LDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, LDecl
def)
   where getPrim :: Name -> IState -> Maybe (Int, PrimFn)
getPrim n :: Name
n i :: IState
i
             | Just (ar :: Int
ar, op :: PrimFn
op) <- Name -> [(Name, (Int, PrimFn))] -> Maybe (Int, PrimFn)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i)
                  = (Int, PrimFn) -> Maybe (Int, PrimFn)
forall a. a -> Maybe a
Just (Int
ar, PrimFn
op)
             | Just ar :: Int
ar <- Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (Set (Name, Int) -> [(Name, Int)]
forall a. Set a -> [a]
S.toList (IState -> Set (Name, Int)
idris_externs IState
i))
                  = (Int, PrimFn) -> Maybe (Int, PrimFn)
forall a. a -> Maybe a
Just (Int
ar, Name -> PrimFn
LExternal Name
n)
         getPrim n :: Name
n i :: IState
i = Maybe (Int, PrimFn)
forall a. Maybe a
Nothing

declArgs :: [Name] -> Bool -> Name -> LExp -> LDecl
declArgs args :: [Name]
args inl :: Bool
inl n :: Name
n (LLam xs :: [Name]
xs x :: LExp
x) = [Name] -> Bool -> Name -> LExp -> LDecl
declArgs ([Name]
args [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
xs) Bool
inl Name
n LExp
x
declArgs args :: [Name]
args inl :: Bool
inl n :: Name
n x :: LExp
x = [LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun (if Bool
inl then [LOpt
Inline] else []) Name
n [Name]
args LExp
x

mkLDecl :: Name -> Def -> Idris LDecl
mkLDecl n :: Name
n (Function tm :: Term
tm _)
    = [Name] -> Bool -> Name -> LExp -> LDecl
declArgs [] Bool
True Name
n (LExp -> LDecl) -> Idris LExp -> Idris LDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
n Vars
forall k a. Map k a
M.empty [] Term
tm

mkLDecl n :: Name
n (CaseOp ci :: CaseInfo
ci _ _ _ pats :: [([Name], Term, Term)]
pats cd :: CaseDefs
cd)
    = [Name] -> Bool -> Name -> LExp -> LDecl
declArgs [] (CaseInfo -> Bool
case_inlinable CaseInfo
ci Bool -> Bool -> Bool
|| Name -> Bool
caseName Name
n) Name
n (LExp -> LDecl) -> Idris LExp -> Idris LDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Name] -> SC -> Idris LExp
irTree Name
n [Name]
args SC
sc
  where
    (args :: [Name]
args, sc :: SC
sc) = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd

    -- Always attempt to inline functions arising from 'case' expressions
    caseName :: Name -> Bool
caseName (SN (CaseN _ _)) = Bool
True
    caseName (SN (WithN _ _)) = Bool
True
    caseName (NS n :: Name
n _) = Name -> Bool
caseName Name
n
    caseName _ = Bool
False

mkLDecl n :: Name
n (TyDecl (DCon tag :: Int
tag arity :: Int
arity _) _) =
    Name -> Int -> Int -> LDecl
LConstructor Name
n Int
tag (Int -> LDecl)
-> ([(Int, [(Name, Int)])] -> Int)
-> [(Int, [(Name, Int)])]
-> LDecl
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [(Int, [(Name, Int)])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Int, [(Name, Int)])] -> LDecl)
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> Idris LDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n)

mkLDecl n :: Name
n (TyDecl (TCon t :: Int
t a :: Int
a) _) = LDecl -> Idris LDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (LDecl -> Idris LDecl) -> LDecl -> Idris LDecl
forall a b. (a -> b) -> a -> b
$ Name -> Int -> Int -> LDecl
LConstructor Name
n (-1) Int
a
mkLDecl n :: Name
n _ = LDecl -> Idris LDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (LDecl -> Idris LDecl) -> LDecl -> Idris LDecl
forall a b. (a -> b) -> a -> b
$ ([Name] -> Bool -> Name -> LExp -> LDecl
declArgs [] Bool
True Name
n LExp
LNothing) -- postulate, never run

data VarInfo = VI
    { VarInfo -> Maybe Name
viMethod :: Maybe Name
    }
    deriving Int -> VarInfo -> FilePath -> FilePath
[VarInfo] -> FilePath -> FilePath
VarInfo -> FilePath
(Int -> VarInfo -> FilePath -> FilePath)
-> (VarInfo -> FilePath)
-> ([VarInfo] -> FilePath -> FilePath)
-> Show VarInfo
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [VarInfo] -> FilePath -> FilePath
$cshowList :: [VarInfo] -> FilePath -> FilePath
show :: VarInfo -> FilePath
$cshow :: VarInfo -> FilePath
showsPrec :: Int -> VarInfo -> FilePath -> FilePath
$cshowsPrec :: Int -> VarInfo -> FilePath -> FilePath
Show

type Vars = M.Map Name VarInfo

irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env tm :: Term
tm@(App _ f :: Term
f a :: Term
a) = do
  IState
ist <- Idris IState
getIState
  case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm of
    (P _ n :: Name
n _, args :: [Term]
args)
        | Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs
        -> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FilePath -> LExp
LError (FilePath -> LExp) -> FilePath -> LExp
forall a b. (a -> b) -> a -> b
$ "ABORT: Attempt to evaluate hole " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
    (P _ (UN m :: Text
m) _, args :: [Term]
args)
        | Text
m Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "mkForeignPrim"
        -> Vars -> [Name] -> [Term] -> Idris LExp
doForeign Vars
vs [Name]
env ([Term] -> [Term]
forall a. [a] -> [a]
reverse (Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
drop 4 [Term]
args)) -- drop implicits

    (P _ (UN u :: Text
u) _, [_, arg :: Term
arg])
        | Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "unsafePerformPrimIO"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    (P _ (UN u :: Text
u) _, _)
        | Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "assert_unreachable"
        -> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FilePath -> LExp
LError (FilePath -> LExp) -> FilePath -> LExp
forall a b. (a -> b) -> a -> b
$ "ABORT: Reached an unreachable case in " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
top

    (P _ (UN u :: Text
u) _, [_, msg :: Term
msg])
        | Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "idris_crash"
        -> do LExp
msg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
msg
              LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LCrash [LExp
msg']

    -- TMP HACK - until we get inlining.
    (P _ (UN r :: Text
r) _, [_, _, _, _, _, arg :: Term
arg])
        | Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "replace"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    -- 'void' doesn't have any pattern clauses and only gets called on
    -- erased things in higher order contexts (also a TMP HACK...)
    (P _ (UN r :: Text
r) _, _)
        | Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "void"
        -> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing

    -- Laziness, the old way
    (P _ (UN l :: Text
l) _, [_, arg :: Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "lazy"
        -> FilePath -> Idris LExp
forall a. HasCallStack => FilePath -> a
error "lazy has crept in somehow"

    (P _ (UN l :: Text
l) _, [_, arg :: Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "force"
        -> LExp -> LExp
LForce (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    -- Laziness, the new way
    (P _ (UN l :: Text
l) _, [_, _, arg :: Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
        -> LExp -> LExp
LLazyExp (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    (P _ (UN l :: Text
l) _, [_, _, arg :: Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Force"
        -> LExp -> LExp
LForce (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    (P _ (UN a :: Text
a) _, [_, _, _, arg :: Term
arg])
        | Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "assert_smaller"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    (P _ (UN a :: Text
a) _, [_, arg :: Term
arg])
        | Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "assert_total"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

    (P _ (UN p :: Text
p) _, [_, arg :: Term
arg])
        | Text
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "par"
        -> do LExp
arg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
              LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LPar [LExp -> LExp
LLazyExp LExp
arg']

    (P _ (UN pf :: Text
pf) _, [arg :: Term
arg])
        | Text
pf Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "prim_fork"
        -> do LExp
arg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
              LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LFork [LExp -> LExp
LLazyExp LExp
arg']

    (P _ (UN m :: Text
m) _, [_,size :: Term
size,t :: Term
t])
        | Text
m Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "malloc"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t

    (P _ (UN tm :: Text
tm) _, [_,t :: Term
t])
        | Text
tm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "trace_malloc"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t -- TODO

    -- This case is here until we get more general inlining. It's just
    -- a really common case, and the laziness hurts...
    (P _ (NS (UN be :: Text
be) [b :: Text
b,p :: Text
p]) _, [_,x :: Term
x,(App _ (App _ (App _ (P _ (UN d :: Text
d) _) _) _) t :: Term
t),
                                    (App _ (App _ (App _ (P _ (UN d' :: Text
d') _) _) _) e :: Term
e)])
        | Text
be Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "ifThenElse"
        , Text
d  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
        , Text
d' Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
        , Text
b  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Bool"
        , Text
p  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Prelude"
        -> do
            LExp
x' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
x
            LExp
t' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
            LExp
e' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
e
            LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
Shared LExp
x'
                             [Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase 0 (Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN "False") ["Bool","Prelude"]) [] LExp
e'
                             ,Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase 1 (Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN "True" ) ["Bool","Prelude"]) [] LExp
t'
                             ])

    -- data constructor
    (P (DCon t :: Int
t arity :: Int
arity _) n :: Name
n _, args :: [Term]
args) -> do
        Bool
detag <- Field IState Bool -> StateT IState (ExceptT Err IO) Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n)
        [Int]
used  <- ((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n)

        let isNewtype :: Bool
isNewtype = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
used Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
&& Bool
detag
        let argsPruned :: [Term]
argsPruned = [Term
a | (i :: Int
i,a :: Term
a) <- [Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Term]
args, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]

        -- The following code removes fields from data constructors
        -- and performs the newtype optimisation.
        --
        -- The general rule here is:
        -- Everything we get as input is not touched by erasure,
        -- so it conforms to the official arities and types
        -- and we can reason about it like it's plain TT.
        --
        -- It's only the data that leaves this point that's erased
        -- and possibly no longer typed as the original TT version.
        --
        -- Especially, underapplied constructors must yield functions
        -- even if all the remaining arguments are erased
        -- (the resulting function *will* be applied, to NULLs).
        --
        -- This will probably need rethinking when we get erasure from functions.

        -- "padLams" will wrap our term in LLam-bdas and give us
        -- the "list of future unerased args" coming from these lambdas.
        --
        -- We can do whatever we like with the list of unerased args,
        -- hence it takes a lambda: \unerased_argname_list -> resulting_LExp.
        let padLams :: ([Name] -> LExp) -> LExp
padLams = [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
padLambdas [Int]
used ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Int
arity

        case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Int
arity of

            -- overapplied
            GT  -> FilePath -> Idris LExp
forall a. FilePath -> Idris a
ifail ("overapplied data constructor: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Term -> FilePath
forall a. Show a => a -> FilePath
show Term
tm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                          "\nDEBUG INFO:\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                          "Arity: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
arity FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                          "Arguments: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Term] -> FilePath
forall a. Show a => a -> FilePath
show [Term]
args FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                          "Pruned arguments: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Term] -> FilePath
forall a. Show a => a -> FilePath
show [Term]
argsPruned)

            -- exactly saturated
            EQ  | Bool
isNewtype
                -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env ([Term] -> Term
forall a. [a] -> a
head [Term]
argsPruned)

                -- compile Nat-likes as bigints
                | Just LikeZ <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
n
                -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Const -> Term
forall n. Const -> TT n
Constant (Integer -> Const
BI 0)

                -- compile Nat-likes as bigints
                | Just LikeS <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
n
                -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp
                    (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (FilePath -> Name
sUN "prim__addBigInt") Term
forall n. TT n
Erased)
                    (Const -> Term
forall n. Const -> TT n
Constant (Integer -> Const
BI 1) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
argsPruned)

                | Bool
otherwise  -- not newtype, plain data ctor
                -> LExp -> [Term] -> Idris LExp
buildApp (Name -> LExp
LV Name
n) [Term]
argsPruned

            -- not saturated, underapplied
            LT  | Bool
isNewtype               -- newtype
                , [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
argsPruned Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1  -- and we already have the value
                -> ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> LExp)
-> (LExp -> [Name] -> LExp) -> LExp -> LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (\tm :: LExp
tm [] -> LExp
tm)  -- the [] asserts there are no unerased args
                    (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env ([Term] -> Term
forall a. [a] -> a
head [Term]
argsPruned)

                | Bool
isNewtype  -- newtype but the value is not among args yet
                -> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp)
-> (([Name] -> LExp) -> LExp) -> ([Name] -> LExp) -> Idris LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> Idris LExp) -> ([Name] -> LExp) -> Idris LExp
forall a b. (a -> b) -> a -> b
$ \[vn :: Name
vn] -> Bool -> LExp -> [LExp] -> LExp
LApp Bool
False (Name -> LExp
LV Name
n) [Name -> LExp
LV Name
vn]

                -- compile Nat-likes as bigints
                -- it seems that prim applications needn't be saturated
                | Just LikeS <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
n
                -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$
                    AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete
                        (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (FilePath -> Name
sUN "prim__addBigInt") Term
forall n. TT n
Erased)
                        (Const -> Term
forall n. Const -> TT n
Constant (Const -> Term) -> Const -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Const
BI 1)

                -- not a newtype, just apply to a constructor
                | Bool
otherwise
                -> ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> LExp)
-> (LExp -> [Name] -> LExp) -> LExp -> LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. LExp -> [Name] -> LExp
applyToNames (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LExp -> [Term] -> Idris LExp
buildApp (Name -> LExp
LV Name
n) [Term]
argsPruned

    -- type constructor
    (P (TCon t :: Int
t a :: Int
a) n :: Name
n _, args :: [Term]
args) -> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing

    -- an external name applied to arguments
    (P _ n :: Name
n _, args :: [Term]
args) | (Name, Int) -> Set (Name, Int) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Name
n, [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) (IState -> Set (Name, Int)
idris_externs IState
ist) -> do
        PrimFn -> [LExp] -> LExp
LOp (Name -> PrimFn
LExternal Name
n) ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args

    -- a name applied to arguments
    (P _ n :: Name
n _, args :: [Term]
args) -> do
        case Name -> [(Name, (Int, PrimFn))] -> Maybe (Int, PrimFn)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
ist) of
            -- if it's a primitive that is already saturated,
            -- compile to the corresponding op here already to save work
            Just (arity :: Int
arity, op :: PrimFn
op) | [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arity
                -> PrimFn -> [LExp] -> LExp
LOp PrimFn
op ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args

            -- otherwise, just apply the name
            _   -> Name -> IState -> [Term] -> Idris LExp
applyName Name
n IState
ist [Term]
args

    -- turn de bruijn vars into regular named references and try again
    (V i :: Int
i, args :: [Term]
args) -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound ([Name]
env [Name] -> Int -> Name
forall a. [a] -> Int -> a
!! Int
i) Term
forall n. TT n
Erased) [Term]
args

    (f :: Term
f, args :: [Term]
args)
        -> Bool -> LExp -> [LExp] -> LExp
LApp Bool
False
            (LExp -> [LExp] -> LExp)
-> Idris LExp -> StateT IState (ExceptT Err IO) ([LExp] -> LExp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
f
            StateT IState (ExceptT Err IO) ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args

  where
    buildApp :: LExp -> [Term] -> Idris LExp
    buildApp :: LExp -> [Term] -> Idris LExp
buildApp e :: LExp
e [] = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
e
    buildApp e :: LExp
e xs :: [Term]
xs = Bool -> LExp -> [LExp] -> LExp
LApp Bool
False LExp
e ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
xs

    applyToNames :: LExp -> [Name] -> LExp
    applyToNames :: LExp -> [Name] -> LExp
applyToNames tm :: LExp
tm [] = LExp
tm
    applyToNames tm :: LExp
tm ns :: [Name]
ns = Bool -> LExp -> [LExp] -> LExp
LApp Bool
False LExp
tm ([LExp] -> LExp) -> [LExp] -> LExp
forall a b. (a -> b) -> a -> b
$ (Name -> LExp) -> [Name] -> [LExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> LExp
LV [Name]
ns

    padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
    padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
padLambdas used :: [Int]
used startIdx :: Int
startIdx endSIdx :: Int
endSIdx mkTerm :: [Name] -> LExp
mkTerm
        = [Name] -> LExp -> LExp
LLam [Name]
allNames (LExp -> LExp) -> LExp -> LExp
forall a b. (a -> b) -> a -> b
$ [Name] -> LExp
mkTerm [Name]
nonerasedNames
      where
        allNames :: [Name]
allNames       = [Int -> FilePath -> Name
sMN Int
i "sat" | Int
i <- [Int
startIdx .. Int
endSIdxInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]]
        nonerasedNames :: [Name]
nonerasedNames = [Int -> FilePath -> Name
sMN Int
i "sat" | Int
i <- [Int
startIdx .. Int
endSIdxInt -> Int -> Int
forall a. Num a => a -> a -> a
-1], Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]

    applyName :: Name -> IState -> [Term] -> Idris LExp
    applyName :: Name -> IState -> [Term] -> Idris LExp
applyName n :: Name
n ist :: IState
ist args :: [Term]
args =
        Bool -> LExp -> [LExp] -> LExp
LApp Bool
False (Name -> LExp
LV Name
n) ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, Term) -> Idris LExp)
-> [(Int, Term)] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp)
-> ((Int, Term) -> Term) -> (Int, Term) -> Idris LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Int, Term) -> Term
forall n. (Int, TT n) -> TT n
erase) ([Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Term]
args)
      where
        erase :: (Int, TT n) -> TT n
erase (i :: Int
i, x :: TT n
x)
            | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
arity Bool -> Bool -> Bool
|| Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used = TT n
x
            | Bool
otherwise = TT n
forall n. TT n
Erased

        arity :: Int
arity = case TTDecl -> Def
forall a b c d e f. (a, b, c, d, e, f) -> a
fst4 (TTDecl -> Def) -> Maybe TTDecl -> Maybe Def
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions (Context -> Ctxt TTDecl)
-> (IState -> Context) -> IState -> Ctxt TTDecl
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Context
tt_ctxt (IState -> Ctxt TTDecl) -> IState -> Ctxt TTDecl
forall a b. (a -> b) -> a -> b
$ IState
ist) of
            Just (CaseOp ci :: CaseInfo
ci ty :: Term
ty tys :: [(Term, Bool)]
tys def :: [Either Term (Term, Term)]
def tot :: [([Name], Term, Term)]
tot cdefs :: CaseDefs
cdefs) -> [(Term, Bool)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, Bool)]
tys
            Just (TyDecl (DCon tag :: Int
tag ar :: Int
ar _) _)       -> Int
ar
            Just (TyDecl Ref ty :: Term
ty)                  -> [(Name, Term)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, Term)] -> Int) -> [(Name, Term)] -> Int
forall a b. (a -> b) -> a -> b
$ Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
ty
            Just (Operator ty :: Term
ty ar :: Int
ar op :: [Value] -> Maybe Value
op)              -> Int
ar
            Just def :: Def
def -> FilePath -> Int
forall a. HasCallStack => FilePath -> a
error (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ "unknown arity: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Name, Def) -> FilePath
forall a. Show a => a -> FilePath
show (Name
n, Def
def)
            Nothing  -> 0  -- no definition, probably local name => can't erase anything

        -- name for purposes of usage info lookup
        uName :: Name
uName
            | Just n' :: Name
n' <- VarInfo -> Maybe Name
viMethod (VarInfo -> Maybe Name) -> Maybe VarInfo -> Maybe Name
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs = Name
n'
            | Bool
otherwise = Name
n

        used :: [Int]
used = [Int] -> (CGInfo -> [Int]) -> Maybe CGInfo -> [Int]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> (CGInfo -> [(Int, [(Name, Int)])]) -> CGInfo -> [Int]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. CGInfo -> [(Int, [(Name, Int)])]
usedpos) (Maybe CGInfo -> [Int]) -> Maybe CGInfo -> [Int]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
uName (IState -> Ctxt CGInfo
idris_callgraph IState
ist)
        fst4 :: (a, b, c, d, e, f) -> a
fst4 (x :: a
x,_,_,_,_,_) = a
x

irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (P _ n :: Name
n _) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Name -> LExp
LV Name
n
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (V i :: Int
i)
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
env = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Name -> LExp
LV ([Name]
env[Name] -> Int -> Name
forall a. [a] -> Int -> a
!!Int
i)
    | Bool
otherwise = FilePath -> Idris LExp
forall a. FilePath -> Idris a
ifail (FilePath -> Idris LExp) -> FilePath -> Idris LExp
forall a b. (a -> b) -> a -> b
$ "bad de bruijn index: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i

irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Bind n :: Name
n (Lam _ _) sc :: Term
sc) = [Name] -> LExp -> LExp
LLam [Name
n'] (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) Term
sc
  where
    n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n [Name]
env

irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Bind n :: Name
n (Let _ _ v :: Term
v) sc :: Term
sc)
    = Name -> LExp -> LExp -> LExp
LLet Name
n (LExp -> LExp -> LExp)
-> Idris LExp -> StateT IState (ExceptT Err IO) (LExp -> LExp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
v StateT IState (ExceptT Err IO) (LExp -> LExp)
-> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc

irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Bind _ _ _) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ LExp
LNothing

irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Proj t :: Term
t (-1)) = do
    LExp
t' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
    LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp (ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
                 [LExp
t', Const -> LExp
LConst (Integer -> Const
BI 1)]

irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Proj t :: Term
t i :: Int
i)   = LExp -> Int -> LExp
LProj (LExp -> Int -> LExp)
-> Idris LExp -> StateT IState (ExceptT Err IO) (Int -> LExp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t StateT IState (ExceptT Err IO) (Int -> LExp)
-> StateT IState (ExceptT Err IO) Int -> Idris LExp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> StateT IState (ExceptT Err IO) Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Constant TheWorld) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Constant c :: Const
c)        = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> LExp
LConst Const
c)
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (TType _)           = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env Erased              = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env Impossible          = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing

data LikeNat = LikeZ | LikeS

isLikeNat :: IState -> Name -> Maybe LikeNat
isLikeNat :: IState -> Name -> Maybe LikeNat
isLikeNat ist :: IState
ist cn :: Name
cn
    -- Nat itself is special-cased in Idris/DataOpts.hs,
    -- which will have already happened at this point.

    -- If the optimisation is disabled then nothing looks like Nat.
    | Optimisation
GeneralisedNatHack Optimisation -> [Optimisation] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` IOption -> [Optimisation]
opt_optimise (IState -> IOption
idris_options IState
ist)
    = Maybe LikeNat
forall a. Maybe a
Nothing

    | Just cTy :: Term
cTy <- Name -> Context -> Maybe Term
lookupTyExact Name
cn (Context -> Maybe Term) -> Context -> Maybe Term
forall a b. (a -> b) -> a -> b
$ IState -> Context
tt_ctxt IState
ist
    , (P TCon{} tyN :: Name
tyN _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> (Term, [Term])) -> Term -> (Term, [Term])
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall n. TT n -> TT n
getRetTy Term
cTy
    , Just (z :: Name
z, s :: Name
s) <- Name -> Maybe (Name, Name)
natLikeCtors Name
tyN
    = if | Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
z -> LikeNat -> Maybe LikeNat
forall a. a -> Maybe a
Just LikeNat
LikeZ
         | Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s -> LikeNat -> Maybe LikeNat
forall a. a -> Maybe a
Just LikeNat
LikeS
         | Bool
otherwise -> FilePath -> Maybe LikeNat
forall a. HasCallStack => FilePath -> a
error (FilePath -> Maybe LikeNat) -> FilePath -> Maybe LikeNat
forall a b. (a -> b) -> a -> b
$ "isLikeNat: constructor not found in its own family: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Name, Name) -> FilePath
forall a. Show a => a -> FilePath
show (Name
cn, Name
tyN)

    | Bool
otherwise = Maybe LikeNat
forall a. Maybe a
Nothing
  where
    natLikeCtors :: Name -> Maybe (Name, Name)
    natLikeCtors :: Name -> Maybe (Name, Name)
natLikeCtors tyN :: Name
tyN = case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tyN (Ctxt TypeInfo -> Maybe TypeInfo)
-> Ctxt TypeInfo -> Maybe TypeInfo
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt TypeInfo
idris_datatypes IState
ist of
        Just TI{con_names :: TypeInfo -> [Name]
con_names = [z :: Name
z, s :: Name
s]}
            | Int
0 <- Name -> Int
getUsedCount Name
z
            , Name -> Bool
looksLikeS Name
s
            -> (Name, Name) -> Maybe (Name, Name)
forall a. a -> Maybe a
Just (Name
z, Name
s)

        Just TI{con_names :: TypeInfo -> [Name]
con_names = [s :: Name
s, z :: Name
z]}
            | Int
0 <- Name -> Int
getUsedCount Name
z
            , Name -> Bool
looksLikeS Name
s
            -> (Name, Name) -> Maybe (Name, Name)
forall a. a -> Maybe a
Just (Name
z, Name
s)

        _ -> Maybe (Name, Name)
forall a. Maybe a
Nothing

    getUsedCount :: Name -> Int
    getUsedCount :: Name -> Int
getUsedCount n :: Name
n =
        Int -> (CGInfo -> Int) -> Maybe CGInfo -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe 0 ([(Int, [(Name, Int)])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Int, [(Name, Int)])] -> Int)
-> (CGInfo -> [(Int, [(Name, Int)])]) -> CGInfo -> Int
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. CGInfo -> [(Int, [(Name, Int)])]
usedpos)
        (Maybe CGInfo -> Int) -> Maybe CGInfo -> Int
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n
        (Ctxt CGInfo -> Maybe CGInfo) -> Ctxt CGInfo -> Maybe CGInfo
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt CGInfo
idris_callgraph IState
ist

    looksLikeS :: Name -> Bool
    looksLikeS :: Name -> Bool
looksLikeS cn :: Name
cn
        | Just [(i :: Int
i, _)] <- (CGInfo -> [(Int, [(Name, Int)])])
-> Maybe CGInfo -> Maybe [(Int, [(Name, Int)])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CGInfo -> [(Int, [(Name, Int)])]
usedpos (Maybe CGInfo -> Maybe [(Int, [(Name, Int)])])
-> Maybe CGInfo -> Maybe [(Int, [(Name, Int)])]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn (Ctxt CGInfo -> Maybe CGInfo) -> Ctxt CGInfo -> Maybe CGInfo
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt CGInfo
idris_callgraph IState
ist
        , Just cTy :: Term
cTy <- Name -> Context -> Maybe Term
lookupTyExact Name
cn (Context -> Maybe Term) -> Context -> Maybe Term
forall a b. (a -> b) -> a -> b
$ IState -> Context
tt_ctxt IState
ist
        , [recTy :: Term
recTy] <- [Term
recTy | (j :: Int
j, (_n :: Name
_n, recTy :: Term
recTy)) <- [Int] -> [(Name, Term)] -> [(Int, (Name, Term))]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
cTy), Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i]
        , (P TCon{} recTyN :: Name
recTyN _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
recTy
        , (P TCon{} tyN :: Name
tyN _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> (Term, [Term])) -> Term -> (Term, [Term])
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall n. TT n -> TT n
getRetTy Term
cTy
        , Name
recTyN Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tyN
        = Bool
True

        | Bool
otherwise = Bool
False

doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
doForeign vs :: Vars
vs env :: [Name]
env (ret :: Term
ret : fname :: Term
fname : world :: Term
world : args :: [Term]
args)
     = do [(FDesc, LExp)]
args' <- (Term -> StateT IState (ExceptT Err IO) (FDesc, LExp))
-> [Term] -> StateT IState (ExceptT Err IO) [(FDesc, LExp)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> StateT IState (ExceptT Err IO) (FDesc, LExp)
splitArg [Term]
args
          let fname' :: FDesc
fname' = Term -> FDesc
toFDesc Term
fname
          let ret' :: FDesc
ret' = Term -> FDesc
toFDesc Term
ret
          LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FDesc -> FDesc -> [(FDesc, LExp)] -> LExp
LForeign FDesc
ret' FDesc
fname' [(FDesc, LExp)]
args'
  where
    splitArg :: Term -> StateT IState (ExceptT Err IO) (FDesc, LExp)
splitArg tm :: Term
tm | (_, [_,_,l :: Term
l,r :: Term
r]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm -- pair, two implicits
        = do let l' :: FDesc
l' = Term -> FDesc
toFDesc Term
l
             LExp
r' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm (Int -> FilePath -> Name
sMN 0 "__foreignCall") Vars
vs [Name]
env Term
r
             (FDesc, LExp) -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (FDesc
l', LExp
r')
    splitArg _ = FilePath -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) (FDesc, LExp))
-> FilePath -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a b. (a -> b) -> a -> b
$ "Badly formed foreign function call: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                         [Term] -> FilePath
forall a. Show a => a -> FilePath
show (Term
ret Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Term
fname Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Term
world Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args)


    toFDesc :: Term -> FDesc
toFDesc (Constant (Str str :: FilePath
str)) = FilePath -> FDesc
FStr FilePath
str
    toFDesc tm :: Term
tm
       | (P _ n :: Name
n _, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
       | (P _ n :: Name
n _, as :: [Term]
as) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> [FDesc] -> FDesc
FApp (Name -> Name
deNS Name
n) ((Term -> FDesc) -> [Term] -> [FDesc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> FDesc
toFDesc [Term]
as)
    toFDesc _ = FDesc
FUnknown

    deNS :: Name -> Name
deNS (NS n :: Name
n _) = Name
n
    deNS n :: Name
n = Name
n
doForeign vs :: Vars
vs env :: [Name]
env xs :: [Term]
xs = FilePath -> Idris LExp
forall a. FilePath -> Idris a
ifail "Badly formed foreign function call"

irTree :: Name -> [Name] -> SC -> Idris LExp
irTree :: Name -> [Name] -> SC -> Idris LExp
irTree top :: Name
top args :: [Name]
args tree :: SC
tree = do
    Int -> FilePath -> Idris ()
logCodeGen 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Compiling " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
args FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SC -> FilePath
forall a. Show a => a -> FilePath
show SC
tree
    [Name] -> LExp -> LExp
LLam [Name]
args (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
forall k a. Map k a
M.empty SC
tree

irSC :: Name -> Vars -> SC -> Idris LExp
irSC :: Name -> Vars -> SC -> Idris LExp
irSC top :: Name
top vs :: Vars
vs (STerm t :: Term
t) = Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [] Term
t
irSC top :: Name
top vs :: Vars
vs (UnmatchedCase str :: FilePath
str) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FilePath -> LExp
LError FilePath
str

irSC top :: Name
top vs :: Vars
vs (ProjCase tm :: Term
tm alts :: [CaseAlt' Term]
alts) = do
    LExp
tm'   <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [] Term
tm
    [LAlt]
alts' <- (CaseAlt' Term -> StateT IState (ExceptT Err IO) LAlt)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [LAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs LExp
tm') [CaseAlt' Term]
alts
    LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
Shared LExp
tm' [LAlt]
alts'

-- Transform matching on Delay to applications of Force.
irSC top :: Name
top vs :: Vars
vs (Case up :: CaseType
up n :: Name
n [ConCase (UN delay :: Text
delay) i :: Int
i [_, _, n' :: Name
n'] sc :: SC
sc])
    | Text
delay Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
    = do LExp
sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc -- mkForce n' n sc
         LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Name -> LExp -> LExp -> LExp
lsubst Name
n' (LExp -> LExp
LForce (Name -> LExp
LV Name
n)) LExp
sc'

-- There are two transformations in this case:
--
--  1. Newtype-case elimination:
--      case {e0} of
--          wrap({e1}) -> P({e1})   ==>   P({e0})
--
-- This is important because newtyped constructors are compiled away entirely
-- and we need to do that everywhere.
--
--  2. Unused-case elimination (only valid for singleton branches):
--      case {e0} of                                ==>     P
--          C(x,y) -> P[... x,y not used ...]
--
-- This is important for runtime because sometimes we case on irrelevant data:
--
-- In the example above, {e0} will most probably have been erased
-- so this vain projection would make the resulting program segfault
-- because the code generator still emits a PROJECT(...) G-machine instruction.
--
-- Hence, we check whether the variables are used at all
-- and erase the casesplit if they are not.
--
irSC top :: Name
top vs :: Vars
vs (Case up :: CaseType
up n :: Name
n [alt :: CaseAlt' Term
alt]) = do
    Maybe SC
replacement <- case CaseAlt' Term
alt of
        ConCase cn :: Name
cn a :: Int
a ns :: [Name]
ns sc :: SC
sc -> do
            Bool
detag <- Field IState Bool -> StateT IState (ExceptT Err IO) Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
cn)
            [Int]
used  <- ((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
cn)
            if Bool
detag Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
used Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1
                then Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC))
-> (SC -> Maybe SC)
-> SC
-> StateT IState (ExceptT Err IO) (Maybe SC)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. SC -> Maybe SC
forall a. a -> Maybe a
Just (SC -> StateT IState (ExceptT Err IO) (Maybe SC))
-> SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall a b. (a -> b) -> a -> b
$ Name -> Name -> SC -> SC
substSC ([Name]
ns [Name] -> Int -> Name
forall a. [a] -> Int -> a
!! [Int] -> Int
forall a. [a] -> a
head [Int]
used) Name
n SC
sc
                else Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SC
forall a. Maybe a
Nothing
        _ -> Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SC
forall a. Maybe a
Nothing

    case Maybe SC
replacement of
        Just sc :: SC
sc -> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
        _ -> do
            LAlt
alt' <- Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n) CaseAlt' Term
alt
            LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ case LAlt -> [Name]
namesBoundIn LAlt
alt' [Name] -> LExp -> [Name]
`usedIn` LAlt -> LExp
subexpr LAlt
alt' of
                [] -> LAlt -> LExp
subexpr LAlt
alt'  -- strip the unused top-most case
                _  -> CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
alt']
  where
    namesBoundIn :: LAlt -> [Name]
    namesBoundIn :: LAlt -> [Name]
namesBoundIn (LConCase cn :: Int
cn i :: Name
i ns :: [Name]
ns sc :: LExp
sc) = [Name]
ns
    namesBoundIn (LConstCase c :: Const
c sc :: LExp
sc)     = []
    namesBoundIn (LDefaultCase sc :: LExp
sc)     = []

    subexpr :: LAlt -> LExp
    subexpr :: LAlt -> LExp
subexpr (LConCase _ _ _ e :: LExp
e) = LExp
e
    subexpr (LConstCase _   e :: LExp
e) = LExp
e
    subexpr (LDefaultCase   e :: LExp
e) = LExp
e

-- FIXME: When we have a non-singleton case-tree of the form
--
--     case {e0} of
--         C(x) => ...
--         ...  => ...
--
-- and C is detaggable (the only constructor of the family), we can be sure
-- that the first branch will be always taken -- so we add special handling
-- to remove the dead default branch.
--
-- If we don't do so and C is newtype-optimisable, we will miss this newtype
-- transformation and the resulting code will probably segfault.
--
-- This work-around is not entirely optimal; the best approach would be
-- to ensure that such case trees don't arise in the first place.
--
irSC top :: Name
top vs :: Vars
vs (Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' Term]
alts@[ConCase cn :: Name
cn a :: Int
a ns :: [Name]
ns sc :: SC
sc, DefaultCase sc' :: SC
sc']) = do
    Bool
detag <- Field IState Bool -> StateT IState (ExceptT Err IO) Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
cn)
    if Bool
detag
        then Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs (CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
a [Name]
ns SC
sc])
        else do
            Maybe LikeNat
likeNat <- IState -> Name -> Maybe LikeNat
isLikeNat (IState -> Name -> Maybe LikeNat)
-> Idris IState
-> StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
-> StateT IState (ExceptT Err IO) Name
-> StateT IState (ExceptT Err IO) (Maybe LikeNat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> StateT IState (ExceptT Err IO) Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
cn
            case Maybe LikeNat
likeNat of
                -- the annoying case: LikeS is translated into a default case
                -- so we need to change the original DefaultCase to Z-case
                -- and reorder it before this one
                Just LikeS -> do
                    LAlt
zCase <- Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI 0) (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc'
                    LAlt
sCase <- Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n) (Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
a [Name]
ns SC
sc)
                    LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
zCase, LAlt
sCase]

                -- the usual case
                _ -> CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) ([LAlt] -> LExp)
-> StateT IState (ExceptT Err IO) [LAlt] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CaseAlt' Term -> StateT IState (ExceptT Err IO) LAlt)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [LAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n)) [CaseAlt' Term]
alts

irSC top :: Name
top vs :: Vars
vs sc :: SC
sc@(Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' Term]
alts) = Idris IState
getIState Idris IState -> (IState -> Idris LExp) -> Idris LExp
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IState -> Idris LExp
rhs
  where
    rhs :: IState -> Idris LExp
rhs ist :: IState
ist
        | [ConCase cns :: Name
cns as :: Int
as nss :: [Name]
nss scs :: SC
scs, ConCase cnz :: Name
cnz az :: Int
az nsz :: [Name]
nsz scz :: SC
scz] <- [CaseAlt' Term]
alts
        , Just LikeS <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
cns
        = do
            -- reorder to make the Z case come first
            LAlt
zCase <- Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI 0) (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
scz
            LAlt
sCase <- Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n) (Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cns Int
as [Name]
nss SC
scs)
            LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
zCase, LAlt
sCase]

        | Bool
otherwise = do
            -- check that neither alternative needs the newtype optimisation,
            -- see comment above
            Bool
goneWrong <- [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool)
-> StateT IState (ExceptT Err IO) [Bool]
-> StateT IState (ExceptT Err IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CaseAlt' Term -> StateT IState (ExceptT Err IO) Bool)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt' Term -> StateT IState (ExceptT Err IO) Bool
forall (m :: * -> *) t. MonadState IState m => CaseAlt' t -> m Bool
isDetaggable [CaseAlt' Term]
alts
            Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
goneWrong
                (Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Idris ()
forall a. FilePath -> Idris a
ifail ("irSC: non-trivial case-match on detaggable data: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SC -> FilePath
forall a. Show a => a -> FilePath
show SC
sc)

            -- everything okay
            CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) ([LAlt] -> LExp)
-> StateT IState (ExceptT Err IO) [LAlt] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CaseAlt' Term -> StateT IState (ExceptT Err IO) LAlt)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [LAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n)) [CaseAlt' Term]
alts

    isDetaggable :: CaseAlt' t -> m Bool
isDetaggable (ConCase cn :: Name
cn _ _ _) = Field IState Bool -> m Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field IState Bool -> m Bool) -> Field IState Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
cn
    isDetaggable  _                 = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

irSC top :: Name
top vs :: Vars
vs ImpossibleCase = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing

irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt

-- this leaves out all unused arguments of the constructor
irAlt :: Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt top :: Name
top vs :: Vars
vs tm :: LExp
tm (ConCase n :: Name
n t :: Int
t args :: [Name]
args sc :: SC
sc) = do
    Maybe LikeNat
likeNat <- IState -> Name -> Maybe LikeNat
isLikeNat (IState -> Name -> Maybe LikeNat)
-> Idris IState
-> StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
-> StateT IState (ExceptT Err IO) Name
-> StateT IState (ExceptT Err IO) (Maybe LikeNat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> StateT IState (ExceptT Err IO) Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n
    [Int]
used <- ((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n)
    let usedArgs :: [Name]
usedArgs = [Name
a | (i :: Int
i,a :: Name
a) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Name]
args, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]

    case Maybe LikeNat
likeNat of
        -- like S
        Just LikeS -> do
            LExp
sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
            case [Name]
usedArgs of
                [pv :: Name
pv] -> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall (m :: * -> *) a. Monad m => a -> m a
return (LAlt -> StateT IState (ExceptT Err IO) LAlt)
-> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (LExp -> LAlt) -> LExp -> LAlt
forall a b. (a -> b) -> a -> b
$ Name -> LExp -> LExp -> LExp
LLet Name
pv
                        ( PrimFn -> [LExp] -> LExp
LOp
                            (ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
                            [ LExp
tm
                            , Const -> LExp
LConst (Integer -> Const
BI 1)
                            ]
                        )
                        LExp
sc'

                _ -> FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) LAlt)
-> FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ "irAlt/LikeS: multiple used args: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
usedArgs

        -- like Z
        Just LikeZ -> Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI 0) (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc

        -- not like Nat
        Nothing -> Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase (-1) Name
n [Name]
usedArgs (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top (Vars
methodVars Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) SC
sc
  where
    methodVars :: Vars
methodVars = case Name
n of
        SN (ImplementationCtorN interfaceName :: Name
interfaceName)
            -> [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI :: Maybe Name -> VarInfo
VI
                { viMethod :: Maybe Name
viMethod = Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkFieldName Name
n Int
i
                }) | (v :: Name
v,i :: Int
i) <- [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [0..]]
        _
            -> Vars
forall k a. Map k a
M.empty -- not an implementation constructor

irAlt top :: Name
top vs :: Vars
vs _ (ConstCase x :: Const
x rhs :: SC
rhs)
    | Const -> Bool
matchable   Const
x = Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase Const
x (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
    | Const -> Bool
matchableTy Const
x = LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
  where
    matchable :: Const -> Bool
matchable (I _) = Bool
True
    matchable (BI _) = Bool
True
    matchable (Ch _) = Bool
True
    matchable (Str _) = Bool
True
    matchable (B8 _) = Bool
True
    matchable (B16 _) = Bool
True
    matchable (B32 _) = Bool
True
    matchable (B64 _) = Bool
True
    matchable _ = Bool
False

    matchableTy :: Const -> Bool
matchableTy (AType (ATInt ITNative)) = Bool
True
    matchableTy (AType (ATInt ITBig)) = Bool
True
    matchableTy (AType (ATInt ITChar)) = Bool
True
    matchableTy StrType = Bool
True

    matchableTy (AType (ATInt (ITFixed IT8)))  = Bool
True
    matchableTy (AType (ATInt (ITFixed IT16))) = Bool
True
    matchableTy (AType (ATInt (ITFixed IT32))) = Bool
True
    matchableTy (AType (ATInt (ITFixed IT64))) = Bool
True

    matchableTy _ = Bool
False

irAlt top :: Name
top vs :: Vars
vs tm :: LExp
tm (SucCase n :: Name
n rhs :: SC
rhs) = do
    LExp
rhs' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
    LAlt -> StateT IState (ExceptT Err IO) LAlt
forall (m :: * -> *) a. Monad m => a -> m a
return (LAlt -> StateT IState (ExceptT Err IO) LAlt)
-> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (Name -> LExp -> LExp -> LExp
LLet Name
n (PrimFn -> [LExp] -> LExp
LOp (ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
                                            [LExp
tm,
                                            Const -> LExp
LConst (Integer -> Const
BI 1)]) LExp
rhs')

irAlt top :: Name
top vs :: Vars
vs _ (ConstCase c :: Const
c rhs :: SC
rhs)
    = FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) LAlt)
-> FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ "Can't match on (" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Const -> FilePath
forall a. Show a => a -> FilePath
show Const
c FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")"

irAlt top :: Name
top vs :: Vars
vs _ (DefaultCase rhs :: SC
rhs)
    = LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs