{-|
Module      : Idris.Inliner
Description : Idris' Inliner.

License     : BSD3
Maintainer  : The Idris Community.
-}
{-# 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

-- | Inlining is either top level (i.e. not in a function arg) or argument level
--
-- For each application in a term:
--    * Check if the function is inlinable
--        (Dictionaries are inlinable in an argument, not otherwise)
--      - If so, try inlining without reducing its arguments
--        + If successful, then continue on the result (top level)
--        + If not, reduce the arguments (argument level) and try again
--      - If not, inline all the arguments (top level)
inlineTerm :: IState -> Term -> Term
inlineTerm :: IState -> Term -> Term
inlineTerm IState
ist 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 NameType
_ n
n TT 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 AppStatus n
_ TT n
f TT n
a)
      | (P NameType
_ n
fn TT n
_, [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 (Let RigCount
rc TT n
t TT n
v) 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 Binder (TT n)
b 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 TT n
tm = TT n
tm

  inlApp :: p -> p -> p -> p
inlApp p
fn p
args p
orig = p
orig