{-# LANGUAGE PatternGuards #-}
module Idris.Inliner(inlineDef, inlineTerm) where
import Idris.AbsSyntax
import Idris.Core.TT
inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]
inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]
inlineDef IState
ist [([Name], Term, Term)]
ds = (([Name], Term, Term) -> ([Name], Term, Term))
-> [([Name], Term, Term)] -> [([Name], Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ ([Name]
ns, Term
lhs, Term
rhs) -> ([Name]
ns, Term
lhs, IState -> Term -> Term
inlineTerm IState
ist Term
rhs)) [([Name], Term, Term)]
ds
inlineTerm :: IState -> Term -> Term
inlineTerm :: IState -> Term -> Term
inlineTerm IState
ist Term
tm = Term -> Term
forall {p}. TT p -> TT p
inl Term
tm where
inl :: TT p -> TT p
inl orig :: TT p
orig@(P NameType
_ p
n TT p
_) = p -> [Any] -> TT p -> TT p
forall {p} {p} {p}. p -> p -> p -> p
inlApp p
n [] TT p
orig
inl orig :: TT p
orig@(App AppStatus p
_ TT p
f TT p
a)
| (P NameType
_ p
fn TT p
_, [TT p]
args) <- TT p -> (TT p, [TT p])
forall n. TT n -> (TT n, [TT n])
unApply TT p
orig = p -> [TT p] -> TT p -> TT p
forall {p} {p} {p}. p -> p -> p -> p
inlApp p
fn [TT p]
args TT p
orig
inl (Bind p
n (Let RigCount
rc TT p
t TT p
v) TT p
sc) = p -> Binder (TT p) -> TT p -> TT p
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind p
n (RigCount -> TT p -> TT p -> Binder (TT p)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT p
t (TT p -> TT p
inl TT p
v)) (TT p -> TT p
inl TT p
sc)
inl (Bind p
n Binder (TT p)
b TT p
sc) = p -> Binder (TT p) -> TT p -> TT p
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind p
n Binder (TT p)
b (TT p -> TT p
inl TT p
sc)
inl TT p
tm = TT p
tm
inlApp :: p -> p -> p -> p
inlApp p
fn p
args p
orig = p
orig