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