{-# LANGUAGE CPP, FlexibleContexts, MultiWayIf, NamedFieldPuns, PatternGuards,
TypeSynonymInstances #-}
module IRTS.Compiler(compile, generate) where
import Idris.AbsSyntax
import Idris.ASTUtils
import Idris.Core.CaseTree
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Erasure
import Idris.Error
import Idris.Options
import Idris.Output
import IRTS.CodegenC
import IRTS.CodegenCommon
import IRTS.Defunctionalise
import IRTS.DumpBC
import IRTS.Exports
import IRTS.Inliner
import IRTS.LangOpts
import IRTS.Portable
import IRTS.Simplified
import Prelude hiding (id, (.))
import Control.Category
import Control.Monad.State
import Data.List
import qualified Data.Map as M
import Data.Maybe (maybe)
import Data.Ord
import qualified Data.Set as S
import System.Directory
import System.Exit
import System.IO
import System.Process
compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo
compile codegen :: Codegen
codegen f :: FilePath
f mtm :: Maybe Term
mtm = do
Int -> FilePath -> Idris ()
logCodeGen 1 "Compiling Output."
Int -> FilePath -> Idris ()
iReport 2 "Compiling Output."
Idris ()
checkMVs
Idris ()
checkTotality
[ExportIFace]
exports <- Idris [ExportIFace]
findExports
let rootNames :: [Name]
rootNames = case Maybe Term
mtm of
Nothing -> []
Just t :: Term
t -> Term -> [Name]
forall n. Eq n => TT n -> [n]
freeNames Term
t
Int -> FilePath -> Idris ()
logCodeGen 1 "Running Erasure Analysis"
Int -> FilePath -> Idris ()
iReport 3 "Running Erasure Analysis"
[Name]
reachableNames <- [Name] -> Idris [Name]
performUsageAnalysis
([Name]
rootNames [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [ExportIFace] -> [Name]
getExpNames [ExportIFace]
exports)
[(Name, LDecl)]
maindef <- case Maybe Term
mtm of
Nothing -> [(Name, LDecl)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
Just tm :: Term
tm -> do LDecl
md <- Term -> Idris LDecl
irMain Term
tm
Int -> FilePath -> Idris ()
logCodeGen 1 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "MAIN: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LDecl -> FilePath
forall a. Show a => a -> FilePath
show LDecl
md
[(Name, LDecl)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Int -> FilePath -> Name
sMN 0 "runMain", LDecl
md)]
[FilePath]
objs <- Codegen -> Idris [FilePath]
getObjectFiles Codegen
codegen
[FilePath]
libs <- Codegen -> Idris [FilePath]
getLibs Codegen
codegen
[FilePath]
flags <- Codegen -> Idris [FilePath]
getFlags Codegen
codegen
[FilePath]
hdrs <- Codegen -> Idris [FilePath]
getHdrs Codegen
codegen
[FilePath]
impdirs <- FilePath -> Idris [FilePath]
rankedImportDirs FilePath
f
[(Name, TTDecl)]
ttDeclarations <- [Name] -> Idris [(Name, TTDecl)]
getDeclarations [Name]
reachableNames
[(Name, LDecl)]
defsIn <- [Name] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
mkDecls [Name]
reachableNames
let iface :: Bool
iface = case Maybe Term
mtm of
Nothing -> Bool
True
Just _ -> Bool
False
let defs :: [(Name, LDecl)]
defs = [(Name, LDecl)]
defsIn [(Name, LDecl)] -> [(Name, LDecl)] -> [(Name, LDecl)]
forall a. [a] -> [a] -> [a]
++ [(Name, LDecl)]
maindef
let defsInlined :: [(Name, LDecl)]
defsInlined = [(Name, LDecl)] -> [(Name, LDecl)]
inlineAll [(Name, LDecl)]
defs
let defsUniq :: [(Name, LDecl)]
defsUniq = ((Name, LDecl) -> (Name, LDecl))
-> [(Name, LDecl)] -> [(Name, LDecl)]
forall a b. (a -> b) -> [a] -> [b]
map (LDefs -> (Name, LDecl) -> (Name, LDecl)
allocUnique ([(Name, LDecl)] -> LDefs -> LDefs
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, LDecl)]
defsInlined LDefs
forall k a. Map k a
emptyContext))
[(Name, LDecl)]
defsInlined
Int -> FilePath -> Idris ()
logCodeGen 1 "Inlining"
Maybe FilePath
dumpCases <- Idris (Maybe FilePath)
getDumpCases
case Maybe FilePath
dumpCases of
Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just f :: FilePath
f -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeFile FilePath
f ([(Name, LDecl)] -> FilePath
showCaseTrees [(Name, LDecl)]
defsUniq)
let (nexttag :: Int
nexttag, tagged :: [(Name, LDecl)]
tagged) = Int -> [(Name, LDecl)] -> (Int, [(Name, LDecl)])
addTags 65536 ([(Name, LDecl)] -> [(Name, LDecl)]
liftAll [(Name, LDecl)]
defsInlined)
let ctxtIn :: LDefs
ctxtIn = [(Name, LDecl)] -> LDefs -> LDefs
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, LDecl)]
tagged LDefs
forall k a. Map k a
emptyContext
Int -> FilePath -> Idris ()
logCodeGen 1 "Defunctionalising"
Int -> FilePath -> Idris ()
iReport 3 "Defunctionalising"
let defuns_in :: DDefs
defuns_in = Int -> LDefs -> DDefs
defunctionalise Int
nexttag LDefs
ctxtIn
Int -> FilePath -> Idris ()
logCodeGen 5 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ DDefs -> FilePath
forall a. Show a => a -> FilePath
show DDefs
defuns_in
Int -> FilePath -> Idris ()
logCodeGen 1 "Inlining"
Int -> FilePath -> Idris ()
iReport 3 "Inlining"
let defuns :: DDefs
defuns = DDefs -> DDefs
inline DDefs
defuns_in
Int -> FilePath -> Idris ()
logCodeGen 5 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ DDefs -> FilePath
forall a. Show a => a -> FilePath
show DDefs
defuns
Int -> FilePath -> Idris ()
logCodeGen 1 "Resolving variables for CG"
let checked :: TC [(Name, SDecl)]
checked = DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
simplifyDefs DDefs
defuns (DDefs -> [(Name, DDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist DDefs
defuns)
OutputType
outty <- Idris OutputType
outputTy
Maybe FilePath
dumpDefun <- Idris (Maybe FilePath)
getDumpDefun
case Maybe FilePath
dumpDefun of
Nothing -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just f :: FilePath
f -> IO () -> Idris ()
forall a. IO a -> Idris a
runIO (IO () -> Idris ()) -> IO () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> IO ()
writeFile FilePath
f (DDefs -> FilePath
dumpDefuns DDefs
defuns)
FilePath
triple <- Idris FilePath
Idris.AbsSyntax.targetTriple
FilePath
cpu <- Idris FilePath
Idris.AbsSyntax.targetCPU
Int -> FilePath -> Idris ()
logCodeGen 1 "Generating Code."
Int -> FilePath -> Idris ()
iReport 2 "Generating Code."
case TC [(Name, SDecl)]
checked of
OK c :: [(Name, SDecl)]
c -> do CodegenInfo -> Idris CodegenInfo
forall (m :: * -> *) a. Monad m => a -> m a
return (CodegenInfo -> Idris CodegenInfo)
-> CodegenInfo -> Idris CodegenInfo
forall a b. (a -> b) -> a -> b
$ FilePath
-> OutputType
-> FilePath
-> FilePath
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> [FilePath]
-> DbgLevel
-> [(Name, SDecl)]
-> [(Name, DDecl)]
-> [(Name, LDecl)]
-> Bool
-> [ExportIFace]
-> [(Name, TTDecl)]
-> CodegenInfo
CodegenInfo FilePath
f OutputType
outty FilePath
triple FilePath
cpu
[FilePath]
hdrs [FilePath]
impdirs [FilePath]
objs [FilePath]
libs [FilePath]
flags
DbgLevel
NONE [(Name, SDecl)]
c (DDefs -> [(Name, DDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist DDefs
defuns)
[(Name, LDecl)]
tagged Bool
iface [ExportIFace]
exports
[(Name, TTDecl)]
ttDeclarations
Error e :: Err
e -> Err -> Idris CodegenInfo
forall a. Err -> Idris a
ierror Err
e
where checkMVs :: Idris ()
checkMVs = do IState
i <- Idris IState
getIState
case ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
i) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs of
[] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
ms :: [Name]
ms -> do FilePath -> Idris ()
iputStrLn (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "WARNING: There are incomplete holes:\n " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
ms
FilePath -> Idris ()
iputStrLn "\nEvaluation of any of these will crash at run time."
() -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkTotality :: Idris ()
checkTotality = do IState
i <- Idris IState
getIState
case IState -> [(FC, FilePath)]
idris_totcheckfail IState
i of
[] -> () -> Idris ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
((fc :: FC
fc, msg :: FilePath
msg):fs :: [(FC, FilePath)]
fs) -> Err -> Idris ()
forall a. Err -> Idris a
ierror (Err -> Idris ()) -> (FilePath -> Err) -> FilePath -> Idris ()
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
fc (Err -> Err) -> (FilePath -> Err) -> FilePath -> Err
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. FilePath -> Err
forall t. FilePath -> Err' t
Msg (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Cannot compile:\n " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
msg
generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
generate :: Codegen -> FilePath -> CodegenInfo -> IO ()
generate codegen :: Codegen
codegen mainmod :: FilePath
mainmod ir :: CodegenInfo
ir
= case Codegen
codegen of
Via _ "c" -> CodegenInfo -> IO ()
codegenC CodegenInfo
ir
Via fm :: IRFormat
fm cg :: FilePath
cg -> do FilePath
input <- case IRFormat
fm of
IBCFormat -> FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
mainmod
JSONFormat -> do
FilePath
tempdir <- IO FilePath
getTemporaryDirectory
(fn :: FilePath
fn, h :: Handle
h) <- FilePath -> FilePath -> IO (FilePath, Handle)
openTempFile FilePath
tempdir "idris-cg.json"
Handle -> CodegenInfo -> IO ()
writePortable Handle
h CodegenInfo
ir
Handle -> IO ()
hClose Handle
h
FilePath -> IO FilePath
forall (m :: * -> *) a. Monad m => a -> m a
return FilePath
fn
let cmd :: FilePath
cmd = "idris-codegen-" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
cg
args :: [FilePath]
args = [FilePath
input, "-o", CodegenInfo -> FilePath
outputFile CodegenInfo
ir] [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ CodegenInfo -> [FilePath]
compilerFlags CodegenInfo
ir
ExitCode
exit <- FilePath -> [FilePath] -> IO ExitCode
rawSystem FilePath
cmd (if CodegenInfo -> Bool
interfaces CodegenInfo
ir then "--interface" FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
args else [FilePath]
args)
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ExitCode
exit ExitCode -> ExitCode -> Bool
forall a. Eq a => a -> a -> Bool
/= ExitCode
ExitSuccess) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
FilePath -> IO ()
putStrLn ("FAILURE: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
forall a. Show a => a -> FilePath
show FilePath
cmd FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
forall a. Show a => a -> FilePath
show [FilePath]
args)
Bytecode -> [(Name, SDecl)] -> FilePath -> IO ()
dumpBC (CodegenInfo -> [(Name, SDecl)]
simpleDecls CodegenInfo
ir) (CodegenInfo -> FilePath
outputFile CodegenInfo
ir)
irMain :: TT Name -> Idris LDecl
irMain :: Term -> Idris LDecl
irMain tm :: Term
tm = do
LExp
i <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm (Int -> FilePath -> Name
sMN 0 "runMain") Vars
forall k a. Map k a
M.empty [] Term
tm
LDecl -> Idris LDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (LDecl -> Idris LDecl) -> LDecl -> Idris LDecl
forall a b. (a -> b) -> a -> b
$ [LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun [] (Int -> FilePath -> Name
sMN 0 "runMain") [] (LExp -> LExp
LForce LExp
i)
mkDecls :: [Name] -> Idris [(Name, LDecl)]
mkDecls :: [Name] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
mkDecls used :: [Name]
used
= do IState
i <- Idris IState
getIState
let ds :: [(Name, Def)]
ds = ((Name, Def) -> Bool) -> [(Name, Def)] -> [(Name, Def)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: Name
n, d :: Def
d) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
used Bool -> Bool -> Bool
|| Def -> Bool
isCon Def
d) ([(Name, Def)] -> [(Name, Def)]) -> [(Name, Def)] -> [(Name, Def)]
forall a b. (a -> b) -> a -> b
$ Context -> [(Name, Def)]
ctxtAlist (IState -> Context
tt_ctxt IState
i)
[(Name, LDecl)]
decls <- ((Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl))
-> [(Name, Def)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl)
build [(Name, Def)]
ds
[(Name, LDecl)] -> StateT IState (ExceptT Err IO) [(Name, LDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, LDecl)]
decls
getDeclarations :: [Name] -> Idris ([(Name, TTDecl)])
getDeclarations :: [Name] -> Idris [(Name, TTDecl)]
getDeclarations used :: [Name]
used
= do IState
i <- Idris IState
getIState
let ds :: [(Name, TTDecl)]
ds = ((Name, TTDecl) -> Bool) -> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(n :: Name
n, (d :: Def
d,_,_,_,_,_)) -> Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
used Bool -> Bool -> Bool
|| Def -> Bool
isCon Def
d) ([(Name, TTDecl)] -> [(Name, TTDecl)])
-> [(Name, TTDecl)] -> [(Name, TTDecl)]
forall a b. (a -> b) -> a -> b
$ ((Ctxt TTDecl -> [(Name, TTDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist (Ctxt TTDecl -> [(Name, TTDecl)])
-> (IState -> Ctxt TTDecl) -> IState -> [(Name, TTDecl)]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Context -> Ctxt TTDecl
definitions (Context -> Ctxt TTDecl)
-> (IState -> Context) -> IState -> Ctxt TTDecl
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Context
tt_ctxt) IState
i)
[(Name, TTDecl)] -> Idris [(Name, TTDecl)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Name, TTDecl)]
ds
showCaseTrees :: [(Name, LDecl)] -> String
showCaseTrees :: [(Name, LDecl)] -> FilePath
showCaseTrees = FilePath -> [FilePath] -> FilePath
showSep "\n\n" ([FilePath] -> FilePath)
-> ([(Name, LDecl)] -> [FilePath]) -> [(Name, LDecl)] -> FilePath
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Name, LDecl) -> FilePath) -> [(Name, LDecl)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (Name, LDecl) -> FilePath
forall a. Show a => (a, LDecl) -> FilePath
showCT ([(Name, LDecl)] -> [FilePath])
-> ([(Name, LDecl)] -> [(Name, LDecl)])
-> [(Name, LDecl)]
-> [FilePath]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ((Name, LDecl) -> (Name, LDecl) -> Ordering)
-> [(Name, LDecl)] -> [(Name, LDecl)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Name, LDecl) -> FilePath)
-> (Name, LDecl) -> (Name, LDecl) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Name, LDecl) -> FilePath
defnRank)
where
showCT :: (a, LDecl) -> FilePath
showCT (n :: a
n, LFun opts :: [LOpt]
opts f :: Name
f args :: [Name]
args lexp :: LExp
lexp)
= FilePath
showOpts FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
a -> FilePath
forall a. Show a => a -> FilePath
show a
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
showSep " " ((Name -> FilePath) -> [Name] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map Name -> FilePath
forall a. Show a => a -> FilePath
show [Name]
args) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " =\n\t"
FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LExp -> FilePath
forall a. Show a => a -> FilePath
show LExp
lexp
where
showOpts :: FilePath
showOpts | LOpt
Inline LOpt -> [LOpt] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [LOpt]
opts = "%inline "
| Bool
otherwise = ""
showCT (n :: a
n, LConstructor c :: Name
c t :: Int
t a :: Int
a) = "data " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ a -> FilePath
forall a. Show a => a -> FilePath
show a
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
a
defnRank :: (Name, LDecl) -> String
defnRank :: (Name, LDecl) -> FilePath
defnRank (n :: Name
n, LFun _ _ _ _) = "1" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
defnRank (n :: Name
n, LConstructor _ _ _) = "2" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
nameRank :: Name -> String
nameRank :: Name -> FilePath
nameRank (UN s :: Text
s) = "1" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
s
nameRank (MN i :: Int
i s :: Text
s) = "2" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i
nameRank (NS n :: Name
n ns :: [Text]
ns) = "3" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Text -> FilePath) -> [Text] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> FilePath
forall a. Show a => a -> FilePath
show ([Text] -> [Text]
forall a. [a] -> [a]
reverse [Text]
ns) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
nameRank (SN sn :: SpecialName
sn) = "4" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SpecialName -> FilePath
snRank SpecialName
sn
nameRank n :: Name
n = "5" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
snRank :: SpecialName -> String
snRank :: SpecialName -> FilePath
snRank (WhereN i :: Int
i n :: Name
n n' :: Name
n') = "1" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n' FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i
snRank (ImplementationN n :: Name
n args :: [Text]
args) = "2" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Text -> FilePath) -> [Text] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Text -> FilePath
forall a. Show a => a -> FilePath
show [Text]
args
snRank (ParentN n :: Name
n s :: Text
s) = "3" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Text -> FilePath
forall a. Show a => a -> FilePath
show Text
s
snRank (MethodN n :: Name
n) = "4" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
snRank (CaseN _ n :: Name
n) = "5" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
snRank (ImplementationCtorN n :: Name
n) = "7" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n
snRank (WithN i :: Int
i n :: Name
n) = "8" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
nameRank Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i
isCon :: Def -> Bool
isCon (TyDecl _ _) = Bool
True
isCon _ = Bool
False
build :: (Name, Def) -> Idris (Name, LDecl)
build :: (Name, Def) -> StateT IState (ExceptT Err IO) (Name, LDecl)
build (n :: Name
n, d :: Def
d)
= do IState
i <- Idris IState
getIState
case Name -> IState -> Maybe (Int, PrimFn)
getPrim Name
n IState
i of
Just (ar :: Int
ar, op :: PrimFn
op) ->
let args :: [Name]
args = (Int -> Name) -> [Int] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: Int
x -> Int -> FilePath -> Name
sMN Int
x "op") [0..] in
(Name, LDecl) -> StateT IState (ExceptT Err IO) (Name, LDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, ([LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun [] Name
n (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
ar [Name]
args)
(PrimFn -> [LExp] -> LExp
LOp PrimFn
op ((Name -> LExp) -> [Name] -> [LExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> LExp
LV (Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
take Int
ar [Name]
args)))))
_ -> do LDecl
def <- Name -> Def -> Idris LDecl
mkLDecl Name
n Def
d
Int -> FilePath -> Idris ()
logCodeGen 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Compiled " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " =\n\t" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ LDecl -> FilePath
forall a. Show a => a -> FilePath
show LDecl
def
(Name, LDecl) -> StateT IState (ExceptT Err IO) (Name, LDecl)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
n, LDecl
def)
where getPrim :: Name -> IState -> Maybe (Int, PrimFn)
getPrim n :: Name
n i :: IState
i
| Just (ar :: Int
ar, op :: PrimFn
op) <- Name -> [(Name, (Int, PrimFn))] -> Maybe (Int, PrimFn)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
i)
= (Int, PrimFn) -> Maybe (Int, PrimFn)
forall a. a -> Maybe a
Just (Int
ar, PrimFn
op)
| Just ar :: Int
ar <- Name -> [(Name, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (Set (Name, Int) -> [(Name, Int)]
forall a. Set a -> [a]
S.toList (IState -> Set (Name, Int)
idris_externs IState
i))
= (Int, PrimFn) -> Maybe (Int, PrimFn)
forall a. a -> Maybe a
Just (Int
ar, Name -> PrimFn
LExternal Name
n)
getPrim n :: Name
n i :: IState
i = Maybe (Int, PrimFn)
forall a. Maybe a
Nothing
declArgs :: [Name] -> Bool -> Name -> LExp -> LDecl
declArgs args :: [Name]
args inl :: Bool
inl n :: Name
n (LLam xs :: [Name]
xs x :: LExp
x) = [Name] -> Bool -> Name -> LExp -> LDecl
declArgs ([Name]
args [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
xs) Bool
inl Name
n LExp
x
declArgs args :: [Name]
args inl :: Bool
inl n :: Name
n x :: LExp
x = [LOpt] -> Name -> [Name] -> LExp -> LDecl
LFun (if Bool
inl then [LOpt
Inline] else []) Name
n [Name]
args LExp
x
mkLDecl :: Name -> Def -> Idris LDecl
mkLDecl n :: Name
n (Function tm :: Term
tm _)
= [Name] -> Bool -> Name -> LExp -> LDecl
declArgs [] Bool
True Name
n (LExp -> LDecl) -> Idris LExp -> Idris LDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
n Vars
forall k a. Map k a
M.empty [] Term
tm
mkLDecl n :: Name
n (CaseOp ci :: CaseInfo
ci _ _ _ pats :: [([Name], Term, Term)]
pats cd :: CaseDefs
cd)
= [Name] -> Bool -> Name -> LExp -> LDecl
declArgs [] (CaseInfo -> Bool
case_inlinable CaseInfo
ci Bool -> Bool -> Bool
|| Name -> Bool
caseName Name
n) Name
n (LExp -> LDecl) -> Idris LExp -> Idris LDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> [Name] -> SC -> Idris LExp
irTree Name
n [Name]
args SC
sc
where
(args :: [Name]
args, sc :: SC
sc) = CaseDefs -> ([Name], SC)
cases_runtime CaseDefs
cd
caseName :: Name -> Bool
caseName (SN (CaseN _ _)) = Bool
True
caseName (SN (WithN _ _)) = Bool
True
caseName (NS n :: Name
n _) = Name -> Bool
caseName Name
n
caseName _ = Bool
False
mkLDecl n :: Name
n (TyDecl (DCon tag :: Int
tag arity :: Int
arity _) _) =
Name -> Int -> Int -> LDecl
LConstructor Name
n Int
tag (Int -> LDecl)
-> ([(Int, [(Name, Int)])] -> Int)
-> [(Int, [(Name, Int)])]
-> LDecl
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. [(Int, [(Name, Int)])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Int, [(Name, Int)])] -> LDecl)
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> Idris LDecl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n)
mkLDecl n :: Name
n (TyDecl (TCon t :: Int
t a :: Int
a) _) = LDecl -> Idris LDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (LDecl -> Idris LDecl) -> LDecl -> Idris LDecl
forall a b. (a -> b) -> a -> b
$ Name -> Int -> Int -> LDecl
LConstructor Name
n (-1) Int
a
mkLDecl n :: Name
n _ = LDecl -> Idris LDecl
forall (m :: * -> *) a. Monad m => a -> m a
return (LDecl -> Idris LDecl) -> LDecl -> Idris LDecl
forall a b. (a -> b) -> a -> b
$ ([Name] -> Bool -> Name -> LExp -> LDecl
declArgs [] Bool
True Name
n LExp
LNothing)
data VarInfo = VI
{ VarInfo -> Maybe Name
viMethod :: Maybe Name
}
deriving Int -> VarInfo -> FilePath -> FilePath
[VarInfo] -> FilePath -> FilePath
VarInfo -> FilePath
(Int -> VarInfo -> FilePath -> FilePath)
-> (VarInfo -> FilePath)
-> ([VarInfo] -> FilePath -> FilePath)
-> Show VarInfo
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [VarInfo] -> FilePath -> FilePath
$cshowList :: [VarInfo] -> FilePath -> FilePath
show :: VarInfo -> FilePath
$cshow :: VarInfo -> FilePath
showsPrec :: Int -> VarInfo -> FilePath -> FilePath
$cshowsPrec :: Int -> VarInfo -> FilePath -> FilePath
Show
type Vars = M.Map Name VarInfo
irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm :: Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env tm :: Term
tm@(App _ f :: Term
f a :: Term
a) = do
IState
ist <- Idris IState
getIState
case Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm of
(P _ n :: Name
n _, args :: [Term]
args)
| Name
n Name -> [Name] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name)
-> [(Name, (Maybe Name, Int, [Name], Bool, Bool))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, (Maybe Name, Int, [Name], Bool, Bool)) -> Name
forall a b. (a, b) -> a
fst (IState -> [(Name, (Maybe Name, Int, [Name], Bool, Bool))]
idris_metavars IState
ist) [Name] -> [Name] -> [Name]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Name]
primDefs
-> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FilePath -> LExp
LError (FilePath -> LExp) -> FilePath -> LExp
forall a b. (a -> b) -> a -> b
$ "ABORT: Attempt to evaluate hole " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
n
(P _ (UN m :: Text
m) _, args :: [Term]
args)
| Text
m Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "mkForeignPrim"
-> Vars -> [Name] -> [Term] -> Idris LExp
doForeign Vars
vs [Name]
env ([Term] -> [Term]
forall a. [a] -> [a]
reverse (Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
drop 4 [Term]
args))
(P _ (UN u :: Text
u) _, [_, arg :: Term
arg])
| Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "unsafePerformPrimIO"
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN u :: Text
u) _, _)
| Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "assert_unreachable"
-> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FilePath -> LExp
LError (FilePath -> LExp) -> FilePath -> LExp
forall a b. (a -> b) -> a -> b
$ "ABORT: Reached an unreachable case in " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Name -> FilePath
forall a. Show a => a -> FilePath
show Name
top
(P _ (UN u :: Text
u) _, [_, msg :: Term
msg])
| Text
u Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "idris_crash"
-> do LExp
msg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
msg
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LCrash [LExp
msg']
(P _ (UN r :: Text
r) _, [_, _, _, _, _, arg :: Term
arg])
| Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "replace"
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN r :: Text
r) _, _)
| Text
r Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "void"
-> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
(P _ (UN l :: Text
l) _, [_, arg :: Term
arg])
| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "lazy"
-> FilePath -> Idris LExp
forall a. HasCallStack => FilePath -> a
error "lazy has crept in somehow"
(P _ (UN l :: Text
l) _, [_, arg :: Term
arg])
| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "force"
-> LExp -> LExp
LForce (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN l :: Text
l) _, [_, _, arg :: Term
arg])
| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
-> LExp -> LExp
LLazyExp (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN l :: Text
l) _, [_, _, arg :: Term
arg])
| Text
l Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Force"
-> LExp -> LExp
LForce (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN a :: Text
a) _, [_, _, _, arg :: Term
arg])
| Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "assert_smaller"
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN a :: Text
a) _, [_, arg :: Term
arg])
| Text
a Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "assert_total"
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
(P _ (UN p :: Text
p) _, [_, arg :: Term
arg])
| Text
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "par"
-> do LExp
arg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LPar [LExp -> LExp
LLazyExp LExp
arg']
(P _ (UN pf :: Text
pf) _, [arg :: Term
arg])
| Text
pf Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "prim_fork"
-> do LExp
arg' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
arg
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp PrimFn
LFork [LExp -> LExp
LLazyExp LExp
arg']
(P _ (UN m :: Text
m) _, [_,size :: Term
size,t :: Term
t])
| Text
m Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "malloc"
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
(P _ (UN tm :: Text
tm) _, [_,t :: Term
t])
| Text
tm Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "trace_malloc"
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
(P _ (NS (UN be :: Text
be) [b :: Text
b,p :: Text
p]) _, [_,x :: Term
x,(App _ (App _ (App _ (P _ (UN d :: Text
d) _) _) _) t :: Term
t),
(App _ (App _ (App _ (P _ (UN d' :: Text
d') _) _) _) e :: Term
e)])
| Text
be Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "ifThenElse"
, Text
d Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
, Text
d' Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
, Text
b Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Bool"
, Text
p Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Prelude"
-> do
LExp
x' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
x
LExp
t' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
LExp
e' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
e
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
Shared LExp
x'
[Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase 0 (Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN "False") ["Bool","Prelude"]) [] LExp
e'
,Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase 1 (Name -> [FilePath] -> Name
sNS (FilePath -> Name
sUN "True" ) ["Bool","Prelude"]) [] LExp
t'
])
(P (DCon t :: Int
t arity :: Int
arity _) n :: Name
n _, args :: [Term]
args) -> do
Bool
detag <- Field IState Bool -> StateT IState (ExceptT Err IO) Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
n)
[Int]
used <- ((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n)
let isNewtype :: Bool
isNewtype = [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
used Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 Bool -> Bool -> Bool
&& Bool
detag
let argsPruned :: [Term]
argsPruned = [Term
a | (i :: Int
i,a :: Term
a) <- [Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Term]
args, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]
let padLams :: ([Name] -> LExp) -> LExp
padLams = [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
padLambdas [Int]
used ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Int
arity
case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) Int
arity of
GT -> FilePath -> Idris LExp
forall a. FilePath -> Idris a
ifail ("overapplied data constructor: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Term -> FilePath
forall a. Show a => a -> FilePath
show Term
tm FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"\nDEBUG INFO:\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"Arity: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
arity FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"Arguments: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Term] -> FilePath
forall a. Show a => a -> FilePath
show [Term]
args FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
"Pruned arguments: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Term] -> FilePath
forall a. Show a => a -> FilePath
show [Term]
argsPruned)
EQ | Bool
isNewtype
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env ([Term] -> Term
forall a. [a] -> a
head [Term]
argsPruned)
| Just LikeZ <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
n
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Const -> Term
forall n. Const -> TT n
Constant (Integer -> Const
BI 0)
| Just LikeS <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
n
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp
(NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (FilePath -> Name
sUN "prim__addBigInt") Term
forall n. TT n
Erased)
(Const -> Term
forall n. Const -> TT n
Constant (Integer -> Const
BI 1) Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
argsPruned)
| Bool
otherwise
-> LExp -> [Term] -> Idris LExp
buildApp (Name -> LExp
LV Name
n) [Term]
argsPruned
LT | Bool
isNewtype
, [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
argsPruned Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1
-> ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> LExp)
-> (LExp -> [Name] -> LExp) -> LExp -> LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (\tm :: LExp
tm [] -> LExp
tm)
(LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env ([Term] -> Term
forall a. [a] -> a
head [Term]
argsPruned)
| Bool
isNewtype
-> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp)
-> (([Name] -> LExp) -> LExp) -> ([Name] -> LExp) -> Idris LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> Idris LExp) -> ([Name] -> LExp) -> Idris LExp
forall a b. (a -> b) -> a -> b
$ \[vn :: Name
vn] -> Bool -> LExp -> [LExp] -> LExp
LApp Bool
False (Name -> LExp
LV Name
n) [Name -> LExp
LV Name
vn]
| Just LikeS <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
n
-> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$
AppStatus Name -> Term -> Term -> Term
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
forall n. AppStatus n
Complete
(NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Ref (FilePath -> Name
sUN "prim__addBigInt") Term
forall n. TT n
Erased)
(Const -> Term
forall n. Const -> TT n
Constant (Const -> Term) -> Const -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Const
BI 1)
| Bool
otherwise
-> ([Name] -> LExp) -> LExp
padLams (([Name] -> LExp) -> LExp)
-> (LExp -> [Name] -> LExp) -> LExp -> LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. LExp -> [Name] -> LExp
applyToNames (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LExp -> [Term] -> Idris LExp
buildApp (Name -> LExp
LV Name
n) [Term]
argsPruned
(P (TCon t :: Int
t a :: Int
a) n :: Name
n _, args :: [Term]
args) -> LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
(P _ n :: Name
n _, args :: [Term]
args) | (Name, Int) -> Set (Name, Int) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member (Name
n, [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args) (IState -> Set (Name, Int)
idris_externs IState
ist) -> do
PrimFn -> [LExp] -> LExp
LOp (Name -> PrimFn
LExternal Name
n) ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args
(P _ n :: Name
n _, args :: [Term]
args) -> do
case Name -> [(Name, (Int, PrimFn))] -> Maybe (Int, PrimFn)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Name
n (IState -> [(Name, (Int, PrimFn))]
idris_scprims IState
ist) of
Just (arity :: Int
arity, op :: PrimFn
op) | [Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arity
-> PrimFn -> [LExp] -> LExp
LOp PrimFn
op ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args
_ -> Name -> IState -> [Term] -> Idris LExp
applyName Name
n IState
ist [Term]
args
(V i :: Int
i, args :: [Term]
args) -> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp) -> Term -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Term -> [Term] -> Term
forall n. TT n -> [TT n] -> TT n
mkApp (NameType -> Name -> Term -> Term
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound ([Name]
env [Name] -> Int -> Name
forall a. [a] -> Int -> a
!! Int
i) Term
forall n. TT n
Erased) [Term]
args
(f :: Term
f, args :: [Term]
args)
-> Bool -> LExp -> [LExp] -> LExp
LApp Bool
False
(LExp -> [LExp] -> LExp)
-> Idris LExp -> StateT IState (ExceptT Err IO) ([LExp] -> LExp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
f
StateT IState (ExceptT Err IO) ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
args
where
buildApp :: LExp -> [Term] -> Idris LExp
buildApp :: LExp -> [Term] -> Idris LExp
buildApp e :: LExp
e [] = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
e
buildApp e :: LExp
e xs :: [Term]
xs = Bool -> LExp -> [LExp] -> LExp
LApp Bool
False LExp
e ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Idris LExp)
-> [Term] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env) [Term]
xs
applyToNames :: LExp -> [Name] -> LExp
applyToNames :: LExp -> [Name] -> LExp
applyToNames tm :: LExp
tm [] = LExp
tm
applyToNames tm :: LExp
tm ns :: [Name]
ns = Bool -> LExp -> [LExp] -> LExp
LApp Bool
False LExp
tm ([LExp] -> LExp) -> [LExp] -> LExp
forall a b. (a -> b) -> a -> b
$ (Name -> LExp) -> [Name] -> [LExp]
forall a b. (a -> b) -> [a] -> [b]
map Name -> LExp
LV [Name]
ns
padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
padLambdas :: [Int] -> Int -> Int -> ([Name] -> LExp) -> LExp
padLambdas used :: [Int]
used startIdx :: Int
startIdx endSIdx :: Int
endSIdx mkTerm :: [Name] -> LExp
mkTerm
= [Name] -> LExp -> LExp
LLam [Name]
allNames (LExp -> LExp) -> LExp -> LExp
forall a b. (a -> b) -> a -> b
$ [Name] -> LExp
mkTerm [Name]
nonerasedNames
where
allNames :: [Name]
allNames = [Int -> FilePath -> Name
sMN Int
i "sat" | Int
i <- [Int
startIdx .. Int
endSIdxInt -> Int -> Int
forall a. Num a => a -> a -> a
-1]]
nonerasedNames :: [Name]
nonerasedNames = [Int -> FilePath -> Name
sMN Int
i "sat" | Int
i <- [Int
startIdx .. Int
endSIdxInt -> Int -> Int
forall a. Num a => a -> a -> a
-1], Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]
applyName :: Name -> IState -> [Term] -> Idris LExp
applyName :: Name -> IState -> [Term] -> Idris LExp
applyName n :: Name
n ist :: IState
ist args :: [Term]
args =
Bool -> LExp -> [LExp] -> LExp
LApp Bool
False (Name -> LExp
LV Name
n) ([LExp] -> LExp)
-> StateT IState (ExceptT Err IO) [LExp] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Int, Term) -> Idris LExp)
-> [(Int, Term)] -> StateT IState (ExceptT Err IO) [LExp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env (Term -> Idris LExp)
-> ((Int, Term) -> Term) -> (Int, Term) -> Idris LExp
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. (Int, Term) -> Term
forall n. (Int, TT n) -> TT n
erase) ([Int] -> [Term] -> [(Int, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Term]
args)
where
erase :: (Int, TT n) -> TT n
erase (i :: Int
i, x :: TT n
x)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
arity Bool -> Bool -> Bool
|| Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used = TT n
x
| Bool
otherwise = TT n
forall n. TT n
Erased
arity :: Int
arity = case TTDecl -> Def
forall a b c d e f. (a, b, c, d, e, f) -> a
fst4 (TTDecl -> Def) -> Maybe TTDecl -> Maybe Def
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Ctxt TTDecl -> Maybe TTDecl
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n (Context -> Ctxt TTDecl
definitions (Context -> Ctxt TTDecl)
-> (IState -> Context) -> IState -> Ctxt TTDecl
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. IState -> Context
tt_ctxt (IState -> Ctxt TTDecl) -> IState -> Ctxt TTDecl
forall a b. (a -> b) -> a -> b
$ IState
ist) of
Just (CaseOp ci :: CaseInfo
ci ty :: Term
ty tys :: [(Term, Bool)]
tys def :: [Either Term (Term, Term)]
def tot :: [([Name], Term, Term)]
tot cdefs :: CaseDefs
cdefs) -> [(Term, Bool)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Term, Bool)]
tys
Just (TyDecl (DCon tag :: Int
tag ar :: Int
ar _) _) -> Int
ar
Just (TyDecl Ref ty :: Term
ty) -> [(Name, Term)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Name, Term)] -> Int) -> [(Name, Term)] -> Int
forall a b. (a -> b) -> a -> b
$ Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
ty
Just (Operator ty :: Term
ty ar :: Int
ar op :: [Value] -> Maybe Value
op) -> Int
ar
Just def :: Def
def -> FilePath -> Int
forall a. HasCallStack => FilePath -> a
error (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ "unknown arity: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Name, Def) -> FilePath
forall a. Show a => a -> FilePath
show (Name
n, Def
def)
Nothing -> 0
uName :: Name
uName
| Just n' :: Name
n' <- VarInfo -> Maybe Name
viMethod (VarInfo -> Maybe Name) -> Maybe VarInfo -> Maybe Name
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Name -> Vars -> Maybe VarInfo
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
n Vars
vs = Name
n'
| Bool
otherwise = Name
n
used :: [Int]
used = [Int] -> (CGInfo -> [Int]) -> Maybe CGInfo -> [Int]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> (CGInfo -> [(Int, [(Name, Int)])]) -> CGInfo -> [Int]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. CGInfo -> [(Int, [(Name, Int)])]
usedpos) (Maybe CGInfo -> [Int]) -> Maybe CGInfo -> [Int]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
uName (IState -> Ctxt CGInfo
idris_callgraph IState
ist)
fst4 :: (a, b, c, d, e, f) -> a
fst4 (x :: a
x,_,_,_,_,_) = a
x
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (P _ n :: Name
n _) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Name -> LExp
LV Name
n
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (V i :: Int
i)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0 Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Name] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name]
env = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Name -> LExp
LV ([Name]
env[Name] -> Int -> Name
forall a. [a] -> Int -> a
!!Int
i)
| Bool
otherwise = FilePath -> Idris LExp
forall a. FilePath -> Idris a
ifail (FilePath -> Idris LExp) -> FilePath -> Idris LExp
forall a b. (a -> b) -> a -> b
$ "bad de bruijn index: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
i
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Bind n :: Name
n (Lam _ _) sc :: Term
sc) = [Name] -> LExp -> LExp
LLam [Name
n'] (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
env) Term
sc
where
n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n [Name]
env
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Bind n :: Name
n (Let _ _ v :: Term
v) sc :: Term
sc)
= Name -> LExp -> LExp -> LExp
LLet Name
n (LExp -> LExp -> LExp)
-> Idris LExp -> StateT IState (ExceptT Err IO) (LExp -> LExp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
v StateT IState (ExceptT Err IO) (LExp -> LExp)
-> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs (Name
n Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: [Name]
env) Term
sc
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Bind _ _ _) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Proj t :: Term
t (-1)) = do
LExp
t' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ PrimFn -> [LExp] -> LExp
LOp (ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
[LExp
t', Const -> LExp
LConst (Integer -> Const
BI 1)]
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Proj t :: Term
t i :: Int
i) = LExp -> Int -> LExp
LProj (LExp -> Int -> LExp)
-> Idris LExp -> StateT IState (ExceptT Err IO) (Int -> LExp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [Name]
env Term
t StateT IState (ExceptT Err IO) (Int -> LExp)
-> StateT IState (ExceptT Err IO) Int -> Idris LExp
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> StateT IState (ExceptT Err IO) Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure Int
i
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Constant TheWorld) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (Constant c :: Const
c) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (Const -> LExp
LConst Const
c)
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env (TType _) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env Erased = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irTerm top :: Name
top vs :: Vars
vs env :: [Name]
env Impossible = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
data LikeNat = LikeZ | LikeS
isLikeNat :: IState -> Name -> Maybe LikeNat
isLikeNat :: IState -> Name -> Maybe LikeNat
isLikeNat ist :: IState
ist cn :: Name
cn
| Optimisation
GeneralisedNatHack Optimisation -> [Optimisation] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` IOption -> [Optimisation]
opt_optimise (IState -> IOption
idris_options IState
ist)
= Maybe LikeNat
forall a. Maybe a
Nothing
| Just cTy :: Term
cTy <- Name -> Context -> Maybe Term
lookupTyExact Name
cn (Context -> Maybe Term) -> Context -> Maybe Term
forall a b. (a -> b) -> a -> b
$ IState -> Context
tt_ctxt IState
ist
, (P TCon{} tyN :: Name
tyN _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> (Term, [Term])) -> Term -> (Term, [Term])
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall n. TT n -> TT n
getRetTy Term
cTy
, Just (z :: Name
z, s :: Name
s) <- Name -> Maybe (Name, Name)
natLikeCtors Name
tyN
= if | Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
z -> LikeNat -> Maybe LikeNat
forall a. a -> Maybe a
Just LikeNat
LikeZ
| Name
cn Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
s -> LikeNat -> Maybe LikeNat
forall a. a -> Maybe a
Just LikeNat
LikeS
| Bool
otherwise -> FilePath -> Maybe LikeNat
forall a. HasCallStack => FilePath -> a
error (FilePath -> Maybe LikeNat) -> FilePath -> Maybe LikeNat
forall a b. (a -> b) -> a -> b
$ "isLikeNat: constructor not found in its own family: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (Name, Name) -> FilePath
forall a. Show a => a -> FilePath
show (Name
cn, Name
tyN)
| Bool
otherwise = Maybe LikeNat
forall a. Maybe a
Nothing
where
natLikeCtors :: Name -> Maybe (Name, Name)
natLikeCtors :: Name -> Maybe (Name, Name)
natLikeCtors tyN :: Name
tyN = case Name -> Ctxt TypeInfo -> Maybe TypeInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
tyN (Ctxt TypeInfo -> Maybe TypeInfo)
-> Ctxt TypeInfo -> Maybe TypeInfo
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt TypeInfo
idris_datatypes IState
ist of
Just TI{con_names :: TypeInfo -> [Name]
con_names = [z :: Name
z, s :: Name
s]}
| Int
0 <- Name -> Int
getUsedCount Name
z
, Name -> Bool
looksLikeS Name
s
-> (Name, Name) -> Maybe (Name, Name)
forall a. a -> Maybe a
Just (Name
z, Name
s)
Just TI{con_names :: TypeInfo -> [Name]
con_names = [s :: Name
s, z :: Name
z]}
| Int
0 <- Name -> Int
getUsedCount Name
z
, Name -> Bool
looksLikeS Name
s
-> (Name, Name) -> Maybe (Name, Name)
forall a. a -> Maybe a
Just (Name
z, Name
s)
_ -> Maybe (Name, Name)
forall a. Maybe a
Nothing
getUsedCount :: Name -> Int
getUsedCount :: Name -> Int
getUsedCount n :: Name
n =
Int -> (CGInfo -> Int) -> Maybe CGInfo -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe 0 ([(Int, [(Name, Int)])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Int, [(Name, Int)])] -> Int)
-> (CGInfo -> [(Int, [(Name, Int)])]) -> CGInfo -> Int
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. CGInfo -> [(Int, [(Name, Int)])]
usedpos)
(Maybe CGInfo -> Int) -> Maybe CGInfo -> Int
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
n
(Ctxt CGInfo -> Maybe CGInfo) -> Ctxt CGInfo -> Maybe CGInfo
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt CGInfo
idris_callgraph IState
ist
looksLikeS :: Name -> Bool
looksLikeS :: Name -> Bool
looksLikeS cn :: Name
cn
| Just [(i :: Int
i, _)] <- (CGInfo -> [(Int, [(Name, Int)])])
-> Maybe CGInfo -> Maybe [(Int, [(Name, Int)])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CGInfo -> [(Int, [(Name, Int)])]
usedpos (Maybe CGInfo -> Maybe [(Int, [(Name, Int)])])
-> Maybe CGInfo -> Maybe [(Int, [(Name, Int)])]
forall a b. (a -> b) -> a -> b
$ Name -> Ctxt CGInfo -> Maybe CGInfo
forall a. Name -> Ctxt a -> Maybe a
lookupCtxtExact Name
cn (Ctxt CGInfo -> Maybe CGInfo) -> Ctxt CGInfo -> Maybe CGInfo
forall a b. (a -> b) -> a -> b
$ IState -> Ctxt CGInfo
idris_callgraph IState
ist
, Just cTy :: Term
cTy <- Name -> Context -> Maybe Term
lookupTyExact Name
cn (Context -> Maybe Term) -> Context -> Maybe Term
forall a b. (a -> b) -> a -> b
$ IState -> Context
tt_ctxt IState
ist
, [recTy :: Term
recTy] <- [Term
recTy | (j :: Int
j, (_n :: Name
_n, recTy :: Term
recTy)) <- [Int] -> [(Name, Term)] -> [(Int, (Name, Term))]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] (Term -> [(Name, Term)]
forall n. TT n -> [(n, TT n)]
getArgTys Term
cTy), Int
j Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i]
, (P TCon{} recTyN :: Name
recTyN _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
recTy
, (P TCon{} tyN :: Name
tyN _, _) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply (Term -> (Term, [Term])) -> Term -> (Term, [Term])
forall a b. (a -> b) -> a -> b
$ Term -> Term
forall n. TT n -> TT n
getRetTy Term
cTy
, Name
recTyN Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
tyN
= Bool
True
| Bool
otherwise = Bool
False
doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
doForeign :: Vars -> [Name] -> [Term] -> Idris LExp
doForeign vs :: Vars
vs env :: [Name]
env (ret :: Term
ret : fname :: Term
fname : world :: Term
world : args :: [Term]
args)
= do [(FDesc, LExp)]
args' <- (Term -> StateT IState (ExceptT Err IO) (FDesc, LExp))
-> [Term] -> StateT IState (ExceptT Err IO) [(FDesc, LExp)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> StateT IState (ExceptT Err IO) (FDesc, LExp)
splitArg [Term]
args
let fname' :: FDesc
fname' = Term -> FDesc
toFDesc Term
fname
let ret' :: FDesc
ret' = Term -> FDesc
toFDesc Term
ret
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FDesc -> FDesc -> [(FDesc, LExp)] -> LExp
LForeign FDesc
ret' FDesc
fname' [(FDesc, LExp)]
args'
where
splitArg :: Term -> StateT IState (ExceptT Err IO) (FDesc, LExp)
splitArg tm :: Term
tm | (_, [_,_,l :: Term
l,r :: Term
r]) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm
= do let l' :: FDesc
l' = Term -> FDesc
toFDesc Term
l
LExp
r' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm (Int -> FilePath -> Name
sMN 0 "__foreignCall") Vars
vs [Name]
env Term
r
(FDesc, LExp) -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall (m :: * -> *) a. Monad m => a -> m a
return (FDesc
l', LExp
r')
splitArg _ = FilePath -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) (FDesc, LExp))
-> FilePath -> StateT IState (ExceptT Err IO) (FDesc, LExp)
forall a b. (a -> b) -> a -> b
$ "Badly formed foreign function call: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
[Term] -> FilePath
forall a. Show a => a -> FilePath
show (Term
ret Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Term
fname Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: Term
world Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
args)
toFDesc :: Term -> FDesc
toFDesc (Constant (Str str :: FilePath
str)) = FilePath -> FDesc
FStr FilePath
str
toFDesc tm :: Term
tm
| (P _ n :: Name
n _, []) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> FDesc
FCon (Name -> Name
deNS Name
n)
| (P _ n :: Name
n _, as :: [Term]
as) <- Term -> (Term, [Term])
forall n. TT n -> (TT n, [TT n])
unApply Term
tm = Name -> [FDesc] -> FDesc
FApp (Name -> Name
deNS Name
n) ((Term -> FDesc) -> [Term] -> [FDesc]
forall a b. (a -> b) -> [a] -> [b]
map Term -> FDesc
toFDesc [Term]
as)
toFDesc _ = FDesc
FUnknown
deNS :: Name -> Name
deNS (NS n :: Name
n _) = Name
n
deNS n :: Name
n = Name
n
doForeign vs :: Vars
vs env :: [Name]
env xs :: [Term]
xs = FilePath -> Idris LExp
forall a. FilePath -> Idris a
ifail "Badly formed foreign function call"
irTree :: Name -> [Name] -> SC -> Idris LExp
irTree :: Name -> [Name] -> SC -> Idris LExp
irTree top :: Name
top args :: [Name]
args tree :: SC
tree = do
Int -> FilePath -> Idris ()
logCodeGen 3 (FilePath -> Idris ()) -> FilePath -> Idris ()
forall a b. (a -> b) -> a -> b
$ "Compiling " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
args FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SC -> FilePath
forall a. Show a => a -> FilePath
show SC
tree
[Name] -> LExp -> LExp
LLam [Name]
args (LExp -> LExp) -> Idris LExp -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
forall k a. Map k a
M.empty SC
tree
irSC :: Name -> Vars -> SC -> Idris LExp
irSC :: Name -> Vars -> SC -> Idris LExp
irSC top :: Name
top vs :: Vars
vs (STerm t :: Term
t) = Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [] Term
t
irSC top :: Name
top vs :: Vars
vs (UnmatchedCase str :: FilePath
str) = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ FilePath -> LExp
LError FilePath
str
irSC top :: Name
top vs :: Vars
vs (ProjCase tm :: Term
tm alts :: [CaseAlt' Term]
alts) = do
LExp
tm' <- Name -> Vars -> [Name] -> Term -> Idris LExp
irTerm Name
top Vars
vs [] Term
tm
[LAlt]
alts' <- (CaseAlt' Term -> StateT IState (ExceptT Err IO) LAlt)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [LAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs LExp
tm') [CaseAlt' Term]
alts
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
Shared LExp
tm' [LAlt]
alts'
irSC top :: Name
top vs :: Vars
vs (Case up :: CaseType
up n :: Name
n [ConCase (UN delay :: Text
delay) i :: Int
i [_, _, n' :: Name
n'] sc :: SC
sc])
| Text
delay Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath -> Text
txt "Delay"
= do LExp
sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ Name -> LExp -> LExp -> LExp
lsubst Name
n' (LExp -> LExp
LForce (Name -> LExp
LV Name
n)) LExp
sc'
irSC top :: Name
top vs :: Vars
vs (Case up :: CaseType
up n :: Name
n [alt :: CaseAlt' Term
alt]) = do
Maybe SC
replacement <- case CaseAlt' Term
alt of
ConCase cn :: Name
cn a :: Int
a ns :: [Name]
ns sc :: SC
sc -> do
Bool
detag <- Field IState Bool -> StateT IState (ExceptT Err IO) Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
cn)
[Int]
used <- ((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
cn)
if Bool
detag Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
used Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1
then Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC))
-> (SC -> Maybe SC)
-> SC
-> StateT IState (ExceptT Err IO) (Maybe SC)
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. SC -> Maybe SC
forall a. a -> Maybe a
Just (SC -> StateT IState (ExceptT Err IO) (Maybe SC))
-> SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall a b. (a -> b) -> a -> b
$ Name -> Name -> SC -> SC
substSC ([Name]
ns [Name] -> Int -> Name
forall a. [a] -> Int -> a
!! [Int] -> Int
forall a. [a] -> a
head [Int]
used) Name
n SC
sc
else Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SC
forall a. Maybe a
Nothing
_ -> Maybe SC -> StateT IState (ExceptT Err IO) (Maybe SC)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe SC
forall a. Maybe a
Nothing
case Maybe SC
replacement of
Just sc :: SC
sc -> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
_ -> do
LAlt
alt' <- Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n) CaseAlt' Term
alt
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ case LAlt -> [Name]
namesBoundIn LAlt
alt' [Name] -> LExp -> [Name]
`usedIn` LAlt -> LExp
subexpr LAlt
alt' of
[] -> LAlt -> LExp
subexpr LAlt
alt'
_ -> CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
alt']
where
namesBoundIn :: LAlt -> [Name]
namesBoundIn :: LAlt -> [Name]
namesBoundIn (LConCase cn :: Int
cn i :: Name
i ns :: [Name]
ns sc :: LExp
sc) = [Name]
ns
namesBoundIn (LConstCase c :: Const
c sc :: LExp
sc) = []
namesBoundIn (LDefaultCase sc :: LExp
sc) = []
subexpr :: LAlt -> LExp
subexpr :: LAlt -> LExp
subexpr (LConCase _ _ _ e :: LExp
e) = LExp
e
subexpr (LConstCase _ e :: LExp
e) = LExp
e
subexpr (LDefaultCase e :: LExp
e) = LExp
e
irSC top :: Name
top vs :: Vars
vs (Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' Term]
alts@[ConCase cn :: Name
cn a :: Int
a ns :: [Name]
ns sc :: SC
sc, DefaultCase sc' :: SC
sc']) = do
Bool
detag <- Field IState Bool -> StateT IState (ExceptT Err IO) Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
cn)
if Bool
detag
then Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs (CaseType -> Name -> [CaseAlt' Term] -> SC
forall t. CaseType -> Name -> [CaseAlt' t] -> SC' t
Case CaseType
up Name
n [Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
a [Name]
ns SC
sc])
else do
Maybe LikeNat
likeNat <- IState -> Name -> Maybe LikeNat
isLikeNat (IState -> Name -> Maybe LikeNat)
-> Idris IState
-> StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
-> StateT IState (ExceptT Err IO) Name
-> StateT IState (ExceptT Err IO) (Maybe LikeNat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> StateT IState (ExceptT Err IO) Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
cn
case Maybe LikeNat
likeNat of
Just LikeS -> do
LAlt
zCase <- Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI 0) (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc'
LAlt
sCase <- Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n) (Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cn Int
a [Name]
ns SC
sc)
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
zCase, LAlt
sCase]
_ -> CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) ([LAlt] -> LExp)
-> StateT IState (ExceptT Err IO) [LAlt] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CaseAlt' Term -> StateT IState (ExceptT Err IO) LAlt)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [LAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n)) [CaseAlt' Term]
alts
irSC top :: Name
top vs :: Vars
vs sc :: SC
sc@(Case up :: CaseType
up n :: Name
n alts :: [CaseAlt' Term]
alts) = Idris IState
getIState Idris IState -> (IState -> Idris LExp) -> Idris LExp
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IState -> Idris LExp
rhs
where
rhs :: IState -> Idris LExp
rhs ist :: IState
ist
| [ConCase cns :: Name
cns as :: Int
as nss :: [Name]
nss scs :: SC
scs, ConCase cnz :: Name
cnz az :: Int
az nsz :: [Name]
nsz scz :: SC
scz] <- [CaseAlt' Term]
alts
, Just LikeS <- IState -> Name -> Maybe LikeNat
isLikeNat IState
ist Name
cns
= do
LAlt
zCase <- Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI 0) (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
scz
LAlt
sCase <- Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n) (Name -> Int -> [Name] -> SC -> CaseAlt' Term
forall t. Name -> Int -> [Name] -> SC' t -> CaseAlt' t
ConCase Name
cns Int
as [Name]
nss SC
scs)
LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return (LExp -> Idris LExp) -> LExp -> Idris LExp
forall a b. (a -> b) -> a -> b
$ CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) [LAlt
zCase, LAlt
sCase]
| Bool
otherwise = do
Bool
goneWrong <- [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool)
-> StateT IState (ExceptT Err IO) [Bool]
-> StateT IState (ExceptT Err IO) Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CaseAlt' Term -> StateT IState (ExceptT Err IO) Bool)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM CaseAlt' Term -> StateT IState (ExceptT Err IO) Bool
forall (m :: * -> *) t. MonadState IState m => CaseAlt' t -> m Bool
isDetaggable [CaseAlt' Term]
alts
Bool -> Idris () -> Idris ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
goneWrong
(Idris () -> Idris ()) -> Idris () -> Idris ()
forall a b. (a -> b) -> a -> b
$ FilePath -> Idris ()
forall a. FilePath -> Idris a
ifail ("irSC: non-trivial case-match on detaggable data: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SC -> FilePath
forall a. Show a => a -> FilePath
show SC
sc)
CaseType -> LExp -> [LAlt] -> LExp
LCase CaseType
up (Name -> LExp
LV Name
n) ([LAlt] -> LExp)
-> StateT IState (ExceptT Err IO) [LAlt] -> Idris LExp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (CaseAlt' Term -> StateT IState (ExceptT Err IO) LAlt)
-> [CaseAlt' Term] -> StateT IState (ExceptT Err IO) [LAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt Name
top Vars
vs (Name -> LExp
LV Name
n)) [CaseAlt' Term]
alts
isDetaggable :: CaseAlt' t -> m Bool
isDetaggable (ConCase cn :: Name
cn _ _ _) = Field IState Bool -> m Bool
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field IState Bool -> m Bool) -> Field IState Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Field OptInfo Bool
opt_detaggable Field OptInfo Bool -> Field IState OptInfo -> Field IState Bool
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState OptInfo
ist_optimisation Name
cn
isDetaggable _ = Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
irSC top :: Name
top vs :: Vars
vs ImpossibleCase = LExp -> Idris LExp
forall (m :: * -> *) a. Monad m => a -> m a
return LExp
LNothing
irAlt :: Name -> Vars -> LExp -> CaseAlt -> Idris LAlt
irAlt :: Name
-> Vars
-> LExp
-> CaseAlt' Term
-> StateT IState (ExceptT Err IO) LAlt
irAlt top :: Name
top vs :: Vars
vs tm :: LExp
tm (ConCase n :: Name
n t :: Int
t args :: [Name]
args sc :: SC
sc) = do
Maybe LikeNat
likeNat <- IState -> Name -> Maybe LikeNat
isLikeNat (IState -> Name -> Maybe LikeNat)
-> Idris IState
-> StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Idris IState
getIState StateT IState (ExceptT Err IO) (Name -> Maybe LikeNat)
-> StateT IState (ExceptT Err IO) Name
-> StateT IState (ExceptT Err IO) (Maybe LikeNat)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Name -> StateT IState (ExceptT Err IO) Name
forall (f :: * -> *) a. Applicative f => a -> f a
pure Name
n
[Int]
used <- ((Int, [(Name, Int)]) -> Int) -> [(Int, [(Name, Int)])] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, [(Name, Int)]) -> Int
forall a b. (a, b) -> a
fst ([(Int, [(Name, Int)])] -> [Int])
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Field IState [(Int, [(Name, Int)])]
-> StateT IState (ExceptT Err IO) [(Int, [(Name, Int)])]
forall s (m :: * -> *) a. MonadState s m => Field s a -> m a
fgetState (Field CGInfo [(Int, [(Name, Int)])]
cg_usedpos Field CGInfo [(Int, [(Name, Int)])]
-> Field IState CGInfo -> Field IState [(Int, [(Name, Int)])]
forall k (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Name -> Field IState CGInfo
ist_callgraph Name
n)
let usedArgs :: [Name]
usedArgs = [Name
a | (i :: Int
i,a :: Name
a) <- [Int] -> [Name] -> [(Int, Name)]
forall a b. [a] -> [b] -> [(a, b)]
zip [0..] [Name]
args, Int
i Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
used]
case Maybe LikeNat
likeNat of
Just LikeS -> do
LExp
sc' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
case [Name]
usedArgs of
[pv :: Name
pv] -> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall (m :: * -> *) a. Monad m => a -> m a
return (LAlt -> StateT IState (ExceptT Err IO) LAlt)
-> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (LExp -> LAlt) -> LExp -> LAlt
forall a b. (a -> b) -> a -> b
$ Name -> LExp -> LExp -> LExp
LLet Name
pv
( PrimFn -> [LExp] -> LExp
LOp
(ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
[ LExp
tm
, Const -> LExp
LConst (Integer -> Const
BI 1)
]
)
LExp
sc'
_ -> FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) LAlt)
-> FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ "irAlt/LikeS: multiple used args: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [Name] -> FilePath
forall a. Show a => a -> FilePath
show [Name]
usedArgs
Just LikeZ -> Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase (Integer -> Const
BI 0) (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
sc
Nothing -> Int -> Name -> [Name] -> LExp -> LAlt
forall e. Int -> Name -> [Name] -> e -> LAlt' e
LConCase (-1) Name
n [Name]
usedArgs (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top (Vars
methodVars Vars -> Vars -> Vars
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` Vars
vs) SC
sc
where
methodVars :: Vars
methodVars = case Name
n of
SN (ImplementationCtorN interfaceName :: Name
interfaceName)
-> [(Name, VarInfo)] -> Vars
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Name
v, VI :: Maybe Name -> VarInfo
VI
{ viMethod :: Maybe Name
viMethod = Name -> Maybe Name
forall a. a -> Maybe a
Just (Name -> Maybe Name) -> Name -> Maybe Name
forall a b. (a -> b) -> a -> b
$ Name -> Int -> Name
mkFieldName Name
n Int
i
}) | (v :: Name
v,i :: Int
i) <- [Name] -> [Int] -> [(Name, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Name]
args [0..]]
_
-> Vars
forall k a. Map k a
M.empty
irAlt top :: Name
top vs :: Vars
vs _ (ConstCase x :: Const
x rhs :: SC
rhs)
| Const -> Bool
matchable Const
x = Const -> LExp -> LAlt
forall e. Const -> e -> LAlt' e
LConstCase Const
x (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
| Const -> Bool
matchableTy Const
x = LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
where
matchable :: Const -> Bool
matchable (I _) = Bool
True
matchable (BI _) = Bool
True
matchable (Ch _) = Bool
True
matchable (Str _) = Bool
True
matchable (B8 _) = Bool
True
matchable (B16 _) = Bool
True
matchable (B32 _) = Bool
True
matchable (B64 _) = Bool
True
matchable _ = Bool
False
matchableTy :: Const -> Bool
matchableTy (AType (ATInt ITNative)) = Bool
True
matchableTy (AType (ATInt ITBig)) = Bool
True
matchableTy (AType (ATInt ITChar)) = Bool
True
matchableTy StrType = Bool
True
matchableTy (AType (ATInt (ITFixed IT8))) = Bool
True
matchableTy (AType (ATInt (ITFixed IT16))) = Bool
True
matchableTy (AType (ATInt (ITFixed IT32))) = Bool
True
matchableTy (AType (ATInt (ITFixed IT64))) = Bool
True
matchableTy _ = Bool
False
irAlt top :: Name
top vs :: Vars
vs tm :: LExp
tm (SucCase n :: Name
n rhs :: SC
rhs) = do
LExp
rhs' <- Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs
LAlt -> StateT IState (ExceptT Err IO) LAlt
forall (m :: * -> *) a. Monad m => a -> m a
return (LAlt -> StateT IState (ExceptT Err IO) LAlt)
-> LAlt -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (Name -> LExp -> LExp -> LExp
LLet Name
n (PrimFn -> [LExp] -> LExp
LOp (ArithTy -> PrimFn
LMinus (IntTy -> ArithTy
ATInt IntTy
ITBig))
[LExp
tm,
Const -> LExp
LConst (Integer -> Const
BI 1)]) LExp
rhs')
irAlt top :: Name
top vs :: Vars
vs _ (ConstCase c :: Const
c rhs :: SC
rhs)
= FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a. FilePath -> Idris a
ifail (FilePath -> StateT IState (ExceptT Err IO) LAlt)
-> FilePath -> StateT IState (ExceptT Err IO) LAlt
forall a b. (a -> b) -> a -> b
$ "Can't match on (" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Const -> FilePath
forall a. Show a => a -> FilePath
show Const
c FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")"
irAlt top :: Name
top vs :: Vars
vs _ (DefaultCase rhs :: SC
rhs)
= LExp -> LAlt
forall e. e -> LAlt' e
LDefaultCase (LExp -> LAlt) -> Idris LExp -> StateT IState (ExceptT Err IO) LAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Name -> Vars -> SC -> Idris LExp
irSC Name
top Vars
vs SC
rhs