{-|
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
import Control.Monad.State
import Data.List
import qualified Data.Map as M
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 -> String -> Maybe Term -> Idris CodegenInfo
compile Codegen
codegen String
f Maybe Term
mtm = do
        Int -> String -> Idris ()
logCodeGen Int
1 String
"Compiling Output."
        Int -> String -> Idris ()
iReport Int
2 String
"Compiling Output."
        Idris ()
checkMVs  -- check for undefined metavariables
        Idris ()
checkTotality -- refuse to compile if there are totality problems
        exports <- Idris [ExportIFace]
findExports
        let rootNames = case Maybe Term
mtm of
                             Maybe Term
Nothing -> []
                             Just Term
t -> Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
t

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

        let 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)] -> [(Name, LDecl)]
inlineAll [(Name, LDecl)]
defs
        let 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

        logCodeGen 1 "Inlining"

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

        let (nexttag, tagged) = addTags 65536 (liftAll defsInlined)
        let 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

        logCodeGen 1 "Defunctionalising"
        iReport 3 "Defunctionalising"
        let defuns_in = Int -> LDefs -> DDefs
defunctionalise Int
nexttag LDefs
ctxtIn
        logCodeGen 5 $ show defuns_in
        logCodeGen 1 "Inlining"
        iReport 3 "Inlining"
        let defuns = DDefs -> DDefs
inline DDefs
defuns_in
        logCodeGen 5 $ show defuns
        logCodeGen 1 "Resolving variables for CG"

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

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

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

mkDecls :: [Name] -> Idris [(Name, LDecl)]
mkDecls :: [Name] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
mkDecls [Name]
used
    = do i <- Idris IState
getIState
         let ds = ((Name, Def) -> Bool) -> [(Name, Def)] -> [(Name, Def)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, Def
d) -> Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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)
         decls <- mapM build ds
         return decls

getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
getDeclarations :: [Name] -> Idris [(Name, TTDecl)]
getDeclarations [Name]
used
    = do i <- Idris IState
getIState
         let ds = ((Name, TTDecl) -> Bool) -> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Name
n, (Def
d,RigCount
_,Bool
_,Accessibility
_,Totality
_,MetaInformation
_)) -> Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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 b c a. (b -> c) -> (a -> b) -> a -> c
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 b c a. (b -> c) -> (a -> b) -> a -> c
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)
         return ds

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

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

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

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

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

build :: (Name, Def) -> Idris (Name, LDecl)
build :: (Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl)
build (Name
n, Def
d)
    = do i <- Idris IState
getIState
         case getPrim n i of
              Just (Int
ar, PrimFn
op) ->
                  let args :: [Name]
args = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
x -> Int -> String -> Name
sMN Int
x String
"op") [Int
0..] in
                      (Name, LDecl) -> StateT IState (ExceptT Err IO) (Name, LDecl)
forall a. a -> StateT IState (ExceptT Err IO) a
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)))))
              Maybe (Int, PrimFn)
_ -> do def <- Name -> Def -> Idris LDecl
mkLDecl Name
n Def
d
                      logCodeGen 3 $ "Compiled " ++ show n ++ " =\n\t" ++ show def
                      return (n, def)
   where getPrim :: Name -> IState -> Maybe (Int, PrimFn)
getPrim Name
n IState
i
             | Just (Int
ar, 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 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 Name
n IState
i = Maybe (Int, PrimFn)
forall a. Maybe a
Nothing

declArgs :: [Name] -> Bool -> Name -> LExp -> LDecl
declArgs [Name]
args Bool
inl Name
n (LLam [Name]
xs 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 [Name]
args Bool
inl Name
n 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 Name
n (Function Term
tm Term
_)
    = [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 Name
n (CaseOp CaseInfo
ci Term
_ [(Term, Bool)]
_ [Either Term (Term, Term)]
_ [([Name], Term, Term)]
pats 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
    ([Name]
args, SC
sc) = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd

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

mkLDecl Name
n (TyDecl (DCon Int
tag Int
arity Bool
_) Term
_) =
    Name -> Int -> Int -> LDecl
LConstructor Name
n Int
tag (Int -> LDecl)
-> ([(Int, [(Name, Int)])] -> Int)
-> [(Int, [(Name, Int)])]
-> LDecl
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 a. [a] -> 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 b c a. Field b c -> Field a b -> Field a c
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 Name
n (TyDecl (TCon Int
t Int
a) Term
_) = LDecl -> Idris LDecl
forall a. a -> StateT IState (ExceptT Err IO) a
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 (-Int
1) Int
a
mkLDecl Name
n Def
_ = LDecl -> Idris LDecl
forall a. a -> StateT IState (ExceptT Err IO) a
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 -> String -> String
[VarInfo] -> String -> String
VarInfo -> String
(Int -> VarInfo -> String -> String)
-> (VarInfo -> String)
-> ([VarInfo] -> String -> String)
-> Show VarInfo
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> VarInfo -> String -> String
showsPrec :: Int -> VarInfo -> String -> String
$cshow :: VarInfo -> String
show :: VarInfo -> String
$cshowList :: [VarInfo] -> String -> String
showList :: [VarInfo] -> String -> String
Show

type Vars = M.Map Name VarInfo

irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env tm :: Term
tm@(App AppStatus Name
_ Term
f Term
a) = do
  ist <- Idris IState
getIState
  case unApply tm of
    (P NameType
_ Name
n Term
_, [Term]
args)
        | Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> 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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ String -> LExp
LError (String -> LExp) -> String -> LExp
forall a b. (a -> b) -> a -> b
$ String
"ABORT: Attempt to evaluate hole " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
    (P NameType
_ (UN Text
m) Term
_, [Term]
args)
        | Text
m Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 Int
4 [Term]
args)) -- drop implicits

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

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

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

    -- TMP HACK - until we get inlining.
    (P NameType
_ (UN Text
r) Term
_, [Term
_, Term
_, Term
_, Term
_, Term
_, Term
arg])
        | Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 NameType
_ (UN Text
r) Term
_, [Term]
_)
        | Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"void"
        -> LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing

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

    (P NameType
_ (UN Text
l) Term
_, [Term
_, Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 NameType
_ (UN Text
l) Term
_, [Term
_, Term
_, Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 NameType
_ (UN Text
l) Term
_, [Term
_, Term
_, Term
arg])
        | Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 NameType
_ (UN Text
a) Term
_, [Term
_, Term
_, Term
_, Term
arg])
        | Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"assert_smaller"
        -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg

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

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

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

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

    (P NameType
_ (UN Text
tm) Term
_, [Term
_,Term
t])
        | Text
tm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"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 NameType
_ (NS (UN Text
be) [Text
b,Text
p]) Term
_, [Term
_,Term
x,(App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ (UN Text
d) Term
_) Term
_) Term
_) Term
t),
                                    (App AppStatus Name
_ (App AppStatus Name
_ (App AppStatus Name
_ (P NameType
_ (UN Text
d') Term
_) Term
_) Term
_) Term
e)])
        | Text
be Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"ifThenElse"
        , Text
d  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay"
        , Text
d' Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay"
        , Text
b  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Bool"
        , Text
p  Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Prelude"
        -> do
            x' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
x
            t' <- irTerm top vs env t
            e' <- irTerm top vs env e
            return (LCase Shared x'
                             [LConCase 0 (sNS (sUN "False") ["Bool","Prelude"]) [] e'
                             ,LConCase 1 (sNS (sUN "True" ) ["Bool","Prelude"]) [] t'
                             ])

    -- data constructor
    (P (DCon Int
t Int
arity Bool
_) Name
n Term
_, [Term]
args) -> do
        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 b c a. Field b c -> Field a b -> Field a c
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)
        used  <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)

        let isNewtype = [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
used Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Bool
detag
        let argsPruned = [Term
a | (Int
i,Term
a) <- [Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Term]
args, Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> 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 = [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
padLambdas [Int]
used ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Int
arity

        case compare (length args) arity of

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

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

                -- compile Nat-likes as bigints
                | Just LikeNat
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 Integer
0)

                -- compile Nat-likes as bigints
                | Just LikeNat
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 (String -> Name
sUN String
"prim__addBigInt") Term
forall n. TT n
Erased)
                    (Const -> Term
forall n. Const -> TT n
Constant (Integer -> Const
BI Integer
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
            Ordering
LT  | Bool
isNewtype               -- newtype
                , [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
argsPruned Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1  -- and we already have the value
                -> ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> LExp)
-> (LExp -> [Name] -> LExp) -> LExp -> LExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (\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. HasCallStack => [a] -> a
head [Term]
argsPruned)

                | Bool
isNewtype  -- newtype but the value is not among args yet
                -> LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp)
-> (([Name] -> LExp) -> LExp) -> ([Name] -> LExp) -> Idris LExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
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
$ \[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 LikeNat
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 (String -> Name
sUN String
"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 Integer
1)

                -- not a newtype, just apply to a constructor
                | Bool
otherwise
                -> ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> LExp)
-> (LExp -> [Name] -> LExp) -> LExp -> LExp
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 Int
t Int
a) Name
n Term
_, [Term]
args) -> LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing

    -- an external name applied to arguments
    (P NameType
_ Name
n Term
_, [Term]
args) | (Name, Int) -> Set (Name, Int) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Name
n, [Term] -> Int
forall a. [a] -> 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args

    -- a name applied to arguments
    (P NameType
_ Name
n Term
_, [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 (Int
arity, PrimFn
op) | [Term] -> Int
forall a. [a] -> 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args

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

    -- turn de bruijn vars into regular named references and try again
    (V Int
i, [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. HasCallStack => [a] -> Int -> a
!! Int
i) Term
forall n. TT n
Erased) [Term]
args

    (Term
f, [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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 LExp
e [] = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
e
    buildApp LExp
e [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 LExp
tm [] = LExp
tm
    applyToNames LExp
tm [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 [Int]
used Int
startIdx Int
endSIdx [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 -> String -> Name
sMN Int
i String
"sat" | Int
i <- [Int
startIdx .. Int
endSIdxInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
        nonerasedNames :: [Name]
nonerasedNames = [Int -> String -> Name
sMN Int
i String
"sat" | Int
i <- [Int
startIdx .. Int
endSIdxInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1], Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> 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 Name
n IState
ist [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 b c a. (b -> c) -> (a -> b) -> a -> c
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 [Int
0..] [Term]
args)
      where
        erase :: (Int, TT n) -> TT n
erase (Int
i, 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 a. Eq a => a -> [a] -> 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 b c a. (b -> c) -> (a -> b) -> a -> c
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 CaseInfo
ci Term
ty [(Term, Bool)]
tys [Either Term (Term, Term)]
def [([Name], Term, Term)]
tot CaseDefs
cdefs) -> [(Term, Bool)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, Bool)]
tys
            Just (TyDecl (DCon Int
tag Int
ar Bool
_) Term
_)       -> Int
ar
            Just (TyDecl NameType
Ref Term
ty)                  -> [(Name, Term)] -> Int
forall a. [a] -> 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 Term
ty Int
ar [Value] -> Maybe Value
op)              -> Int
ar
            Just Def
def -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ String
"unknown arity: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, Def) -> String
forall a. Show a => a -> String
show (Name
n, Def
def)
            Maybe Def
Nothing  -> Int
0  -- no definition, probably local name => can't erase anything

        -- name for purposes of usage info lookup
        uName :: Name
uName
            | Just 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 b c a. (b -> c) -> (a -> b) -> a -> c
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 (a
x,b
_,c
_,d
_,e
_,f
_) = a
x

irTerm Name
top Vars
vs [Name]
env (P NameType
_ Name
n Term
_) = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
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 Name
top Vars
vs [Name]
env (V Int
i)
    | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Name] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
env = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
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. HasCallStack => [a] -> Int -> a
!!Int
i)
    | Bool
otherwise = String -> Idris LExp
forall a. String -> Idris a
ifail (String -> Idris LExp) -> String -> Idris LExp
forall a b. (a -> b) -> a -> b
$ String
"bad de bruijn index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

irTerm Name
top Vars
vs [Name]
env (Bind Name
n (Lam RigCount
_ Term
_) 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 Name
top Vars
vs [Name]
env (Bind Name
n (Let RigCount
_ Term
_ Term
v) 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
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 Name
top Vars
vs [Name]
env (Bind Name
_ Binder Term
_ Term
_) = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
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 Name
top Vars
vs [Name]
env (Proj Term
t (-1)) = do
    t' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
    return $ LOp (LMinus (ATInt ITBig))
                 [t', LConst (BI 1)]

irTerm Name
top Vars
vs [Name]
env (Proj Term
t 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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> StateT IState (ExceptT Err IO) Int
forall a. a -> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
irTerm Name
top Vars
vs [Name]
env (Constant Const
TheWorld) = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm Name
top Vars
vs [Name]
env (Constant Const
c)        = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> LExp
LConst Const
c)
irTerm Name
top Vars
vs [Name]
env (TType UExp
_)           = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm Name
top Vars
vs [Name]
env Term
Erased              = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm Name
top Vars
vs [Name]
env Term
Impossible          = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
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 IState
ist 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 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{} Name
tyN Term
_, [Term]
_) <- 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 (Name
z, 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 -> String -> Maybe LikeNat
forall a. HasCallStack => String -> a
error (String -> Maybe LikeNat) -> String -> Maybe LikeNat
forall a b. (a -> b) -> a -> b
$ String
"isLikeNat: constructor not found in its own family: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Name, Name) -> String
forall a. Show a => a -> String
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 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 = [Name
z, 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 = [Name
s, 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 TypeInfo
_ -> Maybe (Name, Name)
forall a. Maybe a
Nothing

    getUsedCount :: Name -> Int
    getUsedCount :: Name -> Int
getUsedCount Name
n =
        Int -> (CGInfo -> Int) -> Maybe CGInfo -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 ([(Int, [(Name, Int)])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Int, [(Name, Int)])] -> Int)
-> (CGInfo -> [(Int, [(Name, Int)])]) -> CGInfo -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
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 Name
cn
        | Just [(Int
i, [(Name, Int)]
_)] <- (CGInfo -> [(Int, [(Name, Int)])])
-> Maybe CGInfo -> Maybe [(Int, [(Name, Int)])]
forall a b. (a -> b) -> Maybe a -> Maybe b
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 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
        , [Term
recTy] <- [Term
recTy | (Int
j, (Name
_n, Term
recTy)) <- [Int] -> [(Name, Term)] -> [(Int, (Name, Term))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
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{} Name
recTyN Term
_, [Term]
_) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
recTy
        , (P TCon{} Name
tyN Term
_, [Term]
_) <- 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 Vars
vs [Name]
env (Term
ret : Term
fname : Term
world : [Term]
args)
     = do 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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term -> StateT IState (ExceptT Err IO) (FDesc, LExp)
splitArg [Term]
args
          let fname' = Term -> FDesc
toFDesc Term
fname
          let ret' = Term -> FDesc
toFDesc Term
ret
          return $ LForeign ret' fname' args'
  where
    splitArg :: Term -> StateT IState (ExceptT Err IO) (FDesc, LExp)
splitArg Term
tm | (Term
_, [Term
_,Term
_,Term
l,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
             r' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm (Int -> String -> Name
sMN Int
0 String
"__foreignCall") Vars
vs [Name]
env Term
r
             return (l', r')
    splitArg Term
_ = String -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a. String -> Idris a
ifail (String -> StateT IState (ExceptT Err IO) (FDesc, LExp))
-> String -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a b. (a -> b) -> a -> b
$ String
"Badly formed foreign function call: " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         [Term] -> String
forall a. Show a => a -> String
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 String
str)) = String -> FDesc
FStr String
str
    toFDesc Term
tm
       | (P NameType
_ Name
n Term
_, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
       | (P NameType
_ Name
n Term
_, [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 Term
_ = FDesc
FUnknown

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

irTree :: Name -> [Name] -> SC -> Idris LExp
irTree :: Name -> [Name] -> SC -> Idris LExp
irTree Name
top [Name]
args SC
tree = do
    Int -> String -> Idris ()
logCodeGen Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Compiling " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Name] -> String
forall a. Show a => a -> String
show [Name]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
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 Name
top Vars
vs (STerm Term
t) = Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [] Term
t
irSC Name
top Vars
vs (UnmatchedCase String
str) = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ String -> LExp
LError String
str

irSC Name
top Vars
vs (ProjCase Term
tm [CaseAlt' Term]
alts) = do
    tm'   <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [] Term
tm
    alts' <- mapM (irAlt top vs tm') alts
    return $ LCase Shared tm' alts'

-- Transform matching on Delay to applications of Force.
irSC Name
top Vars
vs (Case CaseType
up Name
n [ConCase (UN Text
delay) Int
i [Name
_, Name
_, Name
n'] SC
sc])
    | Text
delay Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Text
txt String
"Delay"
    = do sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc -- mkForce n' n sc
         return $ lsubst n' (LForce (LV n)) 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 Name
top Vars
vs (Case CaseType
up Name
n [CaseAlt' Term
alt]) = do
    replacement <- case CaseAlt' Term
alt of
        ConCase Name
cn Int
a [Name]
ns SC
sc -> do
            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 b c a. Field b c -> Field a b -> Field a c
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)
            used  <- map fst <$> fgetState (cg_usedpos . ist_callgraph cn)
            if detag && length used == 1
                then return . Just $ substSC (ns !! head used) n sc
                else return Nothing
        CaseAlt' Term
_ -> Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SC
forall a. Maybe a
Nothing

    case replacement of
        Just SC
sc -> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
        Maybe SC
_ -> do
            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
            return $ case namesBoundIn alt' `usedIn` subexpr alt' of
                [] -> LAlt -> LExp
subexpr LAlt
alt'  -- strip the unused top-most case
                [Name]
_  -> CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
alt']
  where
    namesBoundIn :: LAlt -> [Name]
    namesBoundIn :: LAlt -> [Name]
namesBoundIn (LConCase Int
cn Name
i [Name]
ns LExp
sc) = [Name]
ns
    namesBoundIn (LConstCase Const
c LExp
sc)     = []
    namesBoundIn (LDefaultCase LExp
sc)     = []

    subexpr :: LAlt -> LExp
    subexpr :: LAlt -> LExp
subexpr (LConCase Int
_ Name
_ [Name]
_ LExp
e) = LExp
e
    subexpr (LConstCase Const
_   LExp
e) = LExp
e
    subexpr (LDefaultCase   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 Name
top Vars
vs (Case CaseType
up Name
n alts :: [CaseAlt' Term]
alts@[ConCase Name
cn Int
a [Name]
ns SC
sc, DefaultCase SC
sc']) = do
    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 b c a. Field b c -> Field a b -> Field a c
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 detag
        then irSC top vs (Case up n [ConCase cn a ns sc])
        else do
            likeNat <- isLikeNat <$> getIState <*> pure cn
            case 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 LikeNat
LikeS -> do
                    zCase <- Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI Integer
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'
                    sCase <- irAlt top vs (LV n) (ConCase cn a ns sc)
                    return $ LCase up (LV n) [zCase, sCase]

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

        | Bool
otherwise = do
            -- check that neither alternative needs the newtype optimisation,
            -- see comment above
            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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM CaseAlt' Term -> StateT IState (ExceptT Err IO) Bool
forall {m :: * -> *} {t}.
MonadState IState m =>
CaseAlt' t -> m Bool
isDetaggable [CaseAlt' Term]
alts
            when goneWrong
                $ ifail ("irSC: non-trivial case-match on detaggable data: " ++ show sc)

            -- everything okay
            LCase up (LV n) <$> mapM (irAlt top vs (LV n)) alts

    isDetaggable :: CaseAlt' t -> m Bool
isDetaggable (ConCase Name
cn Int
_ [Name]
_ SC' t
_) = 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 b c a. Field b c -> Field a b -> Field a c
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  CaseAlt' t
_                 = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

irSC Name
top Vars
vs SC
ImpossibleCase = LExp -> Idris LExp
forall a. a -> StateT IState (ExceptT Err IO) a
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 Name
top Vars
vs LExp
tm (ConCase Name
n Int
t [Name]
args SC
sc) = do
    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 a b.
StateT IState (ExceptT Err IO) (a -> b)
-> StateT IState (ExceptT Err IO) a
-> StateT IState (ExceptT Err IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> StateT IState (ExceptT Err IO) Name
forall a. a -> StateT IState (ExceptT Err IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n
    used <- map fst <$> fgetState (cg_usedpos . ist_callgraph n)
    let usedArgs = [Name
a | (Int
i,Name
a) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Name]
args, Int
i Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]

    case likeNat of
        -- like S
        Just LikeNat
LikeS -> do
            sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
            case usedArgs of
                [Name
pv] -> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall a. a -> StateT IState (ExceptT Err IO) a
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 Integer
1)
                            ]
                        )
                        LExp
sc'

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

        -- like Z
        Just LikeNat
LikeZ -> Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI Integer
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
        Maybe LikeNat
Nothing -> Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase (-Int
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 Name
interfaceName)
            -> [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, 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
                }) | (Name
v,Int
i) <- [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [Int
0..]]
        Name
_
            -> Vars
forall {k} {a}. Map k a
M.empty -- not an implementation constructor

irAlt Name
top Vars
vs LExp
_ (ConstCase Const
x 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 Int
_) = Bool
True
    matchable (BI Integer
_) = Bool
True
    matchable (Ch Char
_) = Bool
True
    matchable (Str String
_) = Bool
True
    matchable (B8 Word8
_) = Bool
True
    matchable (B16 Word16
_) = Bool
True
    matchable (B32 Word32
_) = Bool
True
    matchable (B64 Word64
_) = Bool
True
    matchable Const
_ = Bool
False

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

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

    matchableTy Const
_ = Bool
False

irAlt Name
top Vars
vs LExp
tm (SucCase Name
n SC
rhs) = do
    rhs' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
    return $ LDefaultCase (LLet n (LOp (LMinus (ATInt ITBig))
                                            [tm,
                                            LConst (BI 1)]) rhs')

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

irAlt Name
top Vars
vs LExp
_ (DefaultCase 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