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