{-|
Module      : IRTS.Inliner
Description : Inline expressions.

License     : BSD3
Maintainer  : The Idris Community.
-}
module IRTS.Inliner where

import Idris.Core.TT
import IRTS.Defunctionalise

inline :: DDefs -> DDefs
inline :: DDefs -> DDefs
inline DDefs
xs = let sep :: [(Name, DDecl)]
sep = DDefs -> [(Name, DDecl)]
forall a. Ctxt a -> [(Name, a)]
toAlist DDefs
xs
                inls :: [(Name, DDecl)]
inls = ((Name, DDecl) -> (Name, DDecl))
-> [(Name, DDecl)] -> [(Name, DDecl)]
forall a b. (a -> b) -> [a] -> [b]
map (DDefs -> (Name, DDecl) -> (Name, DDecl)
inl DDefs
xs) [(Name, DDecl)]
sep in
                [(Name, DDecl)] -> DDefs -> DDefs
forall a. [(Name, a)] -> Ctxt a -> Ctxt a
addAlist [(Name, DDecl)]
inls DDefs
forall {k} {a}. Map k a
emptyContext

inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)
inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)
inl DDefs
ds d :: (Name, DDecl)
d@(Name
n, DFun Name
n' [Name]
args DExp
exp)
    = case DDefs -> DExp -> Maybe DExp
forall {p} {a}. p -> a -> Maybe a
evalD DDefs
ds DExp
exp of
           Just DExp
exp' -> (Name
n, Name -> [Name] -> DExp -> DDecl
DFun Name
n' [Name]
args DExp
exp')
           Maybe DExp
_ -> (Name, DDecl)
d
inl DDefs
ds (Name, DDecl)
d = (Name, DDecl)
d

evalD :: p -> a -> Maybe a
evalD p
_ a
e = a -> Maybe a
forall {a}. a -> Maybe a
ev a
e
  where
    ev :: a -> Maybe a
ev a
e = a -> Maybe a
forall {a}. a -> Maybe a
Just a
e