git.iko.soy/Idris-dev
on 0c8a486 help sign in
Idris-dev/src/IRTS/Inliner.hs
28 lines 586 B history raw
1{-|
2Module : IRTS.Inliner
3Description : Inline expressions.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8module IRTS.Inliner where
10import Idris.Core.TT
12import IRTS.Defunctionalise
14inline :: DDefs -> DDefs
15inline xs = let sep = toAlist xs
16 inls = map (inl xs) sep in
17 addAlist inls emptyContext
19inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)
20inl ds d@(n, DFun n' args exp)
21 = case evalD ds exp of
22 Just exp' -> (n, DFun n' args exp')
23 _ -> d
24inl ds d = d
26evalD _ e = ev e
27 where
28 ev e = Just e