git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Inliner.hs
36 lines 1.2 kB history raw
1{-|
2Module : Idris.Inliner
3Description : Idris' Inliner.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
10module Idris.Inliner(inlineDef, inlineTerm) where
12import Idris.AbsSyntax
13import Idris.Core.TT
15inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]
16inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds
18-- | Inlining is either top level (i.e. not in a function arg) or argument level
19--
20-- For each application in a term:
21-- * Check if the function is inlinable
22-- (Dictionaries are inlinable in an argument, not otherwise)
23-- - If so, try inlining without reducing its arguments
24-- + If successful, then continue on the result (top level)
25-- + If not, reduce the arguments (argument level) and try again
26-- - If not, inline all the arguments (top level)
27inlineTerm :: IState -> Term -> Term
28inlineTerm ist tm = inl tm where
29 inl orig@(P _ n _) = inlApp n [] orig
30 inl orig@(App _ f a)
31 | (P _ fn _, args) <- unApply orig = inlApp fn args orig
32 inl (Bind n (Let rc t v) sc) = Bind n (Let rc t (inl v)) (inl sc)
33 inl (Bind n b sc) = Bind n b (inl sc)
34 inl tm = tm
36 inlApp fn args orig = orig