{-# 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 ist :: IState
ist ds :: [([Name], Term, Term)]
ds = (([Name], Term, Term) -> ([Name], Term, Term))
-> [([Name], Term, Term)] -> [([Name], Term, Term)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (ns :: [Name]
ns, lhs :: Term
lhs, rhs :: 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 ist :: IState
ist tm :: Term
tm = Term -> Term
forall n. TT n -> TT n
inl Term
tm where
inl :: TT n -> TT n
inl orig :: TT n
orig@(P _ n :: n
n _) = n -> [Any] -> TT n -> TT n
forall p p p. p -> p -> p -> p
inlApp n
n [] TT n
orig
inl orig :: TT n
orig@(App _ f :: TT n
f a :: TT n
a)
| (P _ fn :: n
fn _, args :: [TT n]
args) <- TT n -> (TT n, [TT n])
forall n. TT n -> (TT n, [TT n])
unApply TT n
orig = n -> [TT n] -> TT n -> TT n
forall p p p. p -> p -> p -> p
inlApp n
fn [TT n]
args TT n
orig
inl (Bind n :: n
n (Let rc :: RigCount
rc t :: TT n
t v :: TT n
v) sc :: TT n
sc) = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n (RigCount -> TT n -> TT n -> Binder (TT n)
forall b. RigCount -> b -> b -> Binder b
Let RigCount
rc TT n
t (TT n -> TT n
inl TT n
v)) (TT n -> TT n
inl TT n
sc)
inl (Bind n :: n
n b :: Binder (TT n)
b sc :: TT n
sc) = n -> Binder (TT n) -> TT n -> TT n
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind n
n Binder (TT n)
b (TT n -> TT n
inl TT n
sc)
inl tm :: TT n
tm = TT n
tm
inlApp :: p -> p -> p -> p
inlApp fn :: p
fn args :: p
args orig :: p
orig = p
orig