git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/IRTS/Inliner.hs
22 lines 451 B history raw
1module IRTS.Inliner where
3import Idris.Core.TT
5import IRTS.Defunctionalise
7inline :: DDefs -> DDefs
8inline xs = let sep = toAlist xs
9 inls = map (inl xs) sep in
10 addAlist inls emptyContext
12inl :: DDefs -> (Name, DDecl) -> (Name, DDecl)
13inl ds d@(n, DFun n' args exp)
14 = case evalD ds exp of
15 Just exp' -> (n, DFun n' args exp')
16 _ -> d
17inl ds d = d
19evalD _ e = ev e
20 where
21 ev e = Just e