{-# 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 :: 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
Idris ()
checkTotality
[ExportIFace]
exports <- Idris [ExportIFace]
findExports
let rootNames :: [Name]
rootNames = case Maybe Term
mtm of
Maybe Term
Nothing -> []
Just Term
t -> Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
t
Int -> String -> Idris ()
logCodeGen Int
1 String
"Running Erasure Analysis"
Int -> String -> Idris ()
iReport Int
3 String
"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
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 LDecl
md <- Term -> Idris LDecl
irMain Term
tm
Int -> String -> Idris ()
logCodeGen Int
1 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"MAIN: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ LDecl -> String
forall a. Show a => a -> String
show LDecl
md
[(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 [(Int -> String -> Name
sMN Int
0 String
"runMain", LDecl
md)]
[String]
objs <- Codegen -> Idris [String]
getObjectFiles Codegen
codegen
[String]
libs <- Codegen -> Idris [String]
getLibs Codegen
codegen
[String]
flags <- Codegen -> Idris [String]
getFlags Codegen
codegen
[String]
hdrs <- Codegen -> Idris [String]
getHdrs Codegen
codegen
[String]
impdirs <- String -> Idris [String]
rankedImportDirs String
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
let iface :: Bool
iface = case Maybe Term
mtm of
Maybe Term
Nothing -> Bool
True
Just Term
_ -> Bool
False
let defs :: [(Name, LDecl)]
defs = [(Name, LDecl)]
defsIn [(Name, LDecl)] -> [(Name, LDecl)] -> [(Name, LDecl)]
forall a. [a] -> [a] -> [a]
++ [(Name, LDecl)]
maindef
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 -> String -> Idris ()
logCodeGen Int
1 String
"Inlining"
Maybe String
dumpCases <- Idris (Maybe String)
getDumpCases
case Maybe String
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 (Int
nexttag, [(Name, LDecl)]
tagged) = Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
addTags Int
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 -> String -> Idris ()
logCodeGen Int
1 String
"Defunctionalising"
Int -> String -> Idris ()
iReport Int
3 String
"Defunctionalising"
let defuns_in :: DDefs
defuns_in = Int -> LDefs -> DDefs
defunctionalise Int
nexttag LDefs
ctxtIn
Int -> String -> Idris ()
logCodeGen Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ DDefs -> String
forall a. Show a => a -> String
show DDefs
defuns_in
Int -> String -> Idris ()
logCodeGen Int
1 String
"Inlining"
Int -> String -> Idris ()
iReport Int
3 String
"Inlining"
let defuns :: DDefs
defuns = DDefs -> DDefs
inline DDefs
defuns_in
Int -> String -> Idris ()
logCodeGen Int
5 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ DDefs -> String
forall a. Show a => a -> String
show DDefs
defuns
Int -> String -> Idris ()
logCodeGen Int
1 String
"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 String
dumpDefun <- Idris (Maybe String)
getDumpDefun
case Maybe String
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)
String
triple <- Idris String
Idris.AbsSyntax.targetTriple
String
cpu <- Idris String
Idris.AbsSyntax.targetCPU
Int -> String -> Idris ()
logCodeGen Int
1 String
"Generating Code."
Int -> String -> Idris ()
iReport Int
2 String
"Generating Code."
case TC [(Name, SDecl)]
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 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 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 IState
i <- Idris IState
getIState
case IState -> [(FC, String)]
idris_totcheckfail IState
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
Via IRFormat
_ String
"c" -> CodegenInfo -> IO ()
codegenC CodegenInfo
ir
Via IRFormat
fm String
cg -> do String
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
String
tempdir <- IO String
getTemporaryDirectory
(String
fn, Handle
h) <- String -> String -> IO (String, Handle)
openTempFile String
tempdir String
"idris-cg.json"
Handle -> CodegenInfo -> IO ()
writePortable Handle
h CodegenInfo
ir
Handle -> IO ()
hClose Handle
h
String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
fn
let cmd :: String
cmd = String
"idris-codegen-" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cg
args :: [String]
args = [String
input, String
"-o", CodegenInfo -> String
outputFile CodegenInfo
ir] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ CodegenInfo -> [String]
compilerFlags CodegenInfo
ir
ExitCode
exit <- String -> [String] -> IO ExitCode
rawSystem String
cmd (if CodegenInfo -> Bool
interfaces CodegenInfo
ir then String
"--interface" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
args else [String]
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
$
String -> IO ()
putStrLn (String
"FAILURE: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
cmd String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
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
LExp
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
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
$ [LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun [] (Int -> String -> Name
sMN Int
0 String
"runMain") [] (LExp -> LExp
LForce LExp
i)
mkDecls :: [Name] -> Idris [(Name, LDecl)]
mkDecls :: [Name] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
mkDecls [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 (\(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)
[(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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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 a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, LDecl)]
decls
getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
getDeclarations :: [Name] -> Idris [(Name, TTDecl)]
getDeclarations [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 (\(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)
[(Name, TTDecl)] -> Idris [(Name, TTDecl)]
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TTDecl)]
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 IState
i <- Idris IState
getIState
case Name -> IState -> Maybe (Int, PrimFn)
getPrim Name
n IState
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 LDecl
def <- Name -> Def -> Idris LDecl
mkLDecl Name
n Def
d
Int -> String -> Idris ()
logCodeGen Int
3 (String -> Idris ()) -> String -> Idris ()
forall a b. (a -> b) -> a -> b
$ String
"Compiled " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" =\n\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ LDecl -> String
forall a. Show a => a -> String
show LDecl
def
(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, LDecl
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
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)
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
IState
ist <- Idris IState
getIState
case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
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))
(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 LExp
msg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
msg
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
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LCrash [LExp
msg']
(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
(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
(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
(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 LExp
arg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
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
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LPar [LExp -> LExp
LLazyExp LExp
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 LExp
arg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
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
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LFork [LExp -> LExp
LLazyExp LExp
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
(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
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 a. a -> StateT IState (ExceptT Err IO) a
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 Int
0 (Name -> [String] -> Name
sNS (String -> Name
sUN String
"False") [String
"Bool",String
"Prelude"]) [] LExp
e'
,Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase Int
1 (Name -> [String] -> Name
sNS (String -> Name
sUN String
"True" ) [String
"Bool",String
"Prelude"]) [] LExp
t'
])
(P (DCon Int
t Int
arity Bool
_) Name
n Term
_, [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 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)
[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 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)
let isNewtype :: Bool
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]
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]
let padLams :: ([Name] -> LExp) -> LExp
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 Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Int
arity of
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)
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)
| 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)
| 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
-> LExp -> [Term] -> Idris LExp
buildApp (Name -> LExp
LV Name
n) [Term]
argsPruned
Ordering
LT | Bool
isNewtype
, [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
-> ([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)
(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
-> 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]
| 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)
| 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
(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
(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
(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
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
Maybe (Int, PrimFn)
_ -> Name -> IState -> [Term] -> Idris LExp
applyName Name
n IState
ist [Term]
args
(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
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
LExp
t' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
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
$ PrimFn -> [LExp] -> LExp
LOp (ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
[LExp
t', Const -> LExp
LConst (Integer -> Const
BI Integer
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
| 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 [(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)
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' :: FDesc
fname' = Term -> FDesc
toFDesc Term
fname
let ret' :: FDesc
ret' = Term -> FDesc
toFDesc Term
ret
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
$ FDesc -> FDesc -> [(FDesc, LExp)] -> LExp
LForeign FDesc
ret' FDesc
fname' [(FDesc, LExp)]
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
= do let l' :: FDesc
l' = Term -> FDesc
toFDesc Term
l
LExp
r' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm (Int -> String -> Name
sMN Int
0 String
"__foreignCall") Vars
vs [Name]
env Term
r
(FDesc, LExp) -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a. a -> StateT IState (ExceptT Err IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FDesc
l', LExp
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
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)
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 LExp
tm') [CaseAlt' Term]
alts
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
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
Shared LExp
tm' [LAlt]
alts'
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 LExp
sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
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 -> LExp -> LExp
lsubst Name
n' (LExp -> LExp
LForce (Name -> LExp
LV Name
n)) LExp
sc'
irSC Name
top Vars
vs (Case CaseType
up Name
n [CaseAlt' Term
alt]) = do
Maybe SC
replacement <- case CaseAlt' Term
alt of
ConCase Name
cn Int
a [Name]
ns 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 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)
[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 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
cn)
if Bool
detag Bool -> Bool -> Bool
&& [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
then 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 -> StateT IState (ExceptT Err IO) (Maybe SC))
-> (SC -> Maybe SC)
-> SC
-> StateT IState (ExceptT Err IO) (Maybe SC)
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
. 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. HasCallStack => [a] -> Int -> a
!! [Int] -> Int
forall a. HasCallStack => [a] -> a
head [Int]
used) Name
n SC
sc
else 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
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 Maybe SC
replacement of
Just SC
sc -> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
Maybe 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 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
$ case LAlt -> [Name]
namesBoundIn LAlt
alt' [Name] -> LExp -> [Name]
`usedIn` LAlt -> LExp
subexpr LAlt
alt' of
[] -> LAlt -> LExp
subexpr LAlt
alt'
[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
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
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 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 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 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
cn
case Maybe LikeNat
likeNat of
Just LikeNat
LikeS -> do
LAlt
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'
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 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
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
zCase, LAlt
sCase]
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
LAlt
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
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 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
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
zCase, LAlt
sCase]
| Bool
otherwise = do
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)
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
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
goneWrong
(Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ String -> Idris ()
forall a. String -> Idris a
ifail (String
"irSC: non-trivial case-match on detaggable data: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SC -> String
forall a. Show a => a -> String
show SC
sc)
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
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
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
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 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
[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 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)
let usedArgs :: [Name]
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 Maybe LikeNat
likeNat of
Just LikeNat
LikeS -> do
LExp
sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
case [Name]
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
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
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
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
LExp
rhs' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
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 (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 Integer
1)]) LExp
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