git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/IRTS/LangOpts.hs
83 lines 3.6 kB history raw
1{-|
2Module : IRTS.LangOpts
3Description : Transformations to apply to Idris' IR.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE DeriveFunctor, PatternGuards #-}
10module IRTS.LangOpts where
12import Idris.Core.TT
13import IRTS.Lang
15import Control.Monad.State hiding (lift)
17inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]
18inlineAll lds = let defs = addAlist lds emptyContext in
19 map (\ (n, def) -> (n, doInline defs def)) lds
21nextN :: State Int Name
22nextN = do i <- get
23 put (i + 1)
24 return $ sMN i "in"
26-- | Inline inside a declaration.
27--
28-- Variables are still Name at this stage. Need to preserve
29-- uniqueness of variable names in the resulting definition, so invent
30-- a new name for every variable we encounter
31doInline :: LDefs -> LDecl -> LDecl
32doInline defs d@(LConstructor _ _ _) = d
33doInline defs (LFun opts topn args exp)
34 = let res = evalState (inlineWith [topn] (map (\n -> (n, LV n)) args) exp) 0 in
35 LFun opts topn args res
36 where
37 inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp
38 inlineWith done env var@(LV n)
39 = case lookup n env of
40 Just t -> return t
41 Nothing -> return var
42 inlineWith done env (LLazyApp n es) = LLazyApp n <$> (mapM (inlineWith done env) es)
43 inlineWith done env (LForce e) = LForce <$> inlineWith done env e
44 inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e
45 -- Extend the environment for Let and Lam so that bound names aren't
46 -- expanded with any top level argument definitions they shadow
47 inlineWith done env (LLet n val sc)
48 = do n' <- nextN
49 LLet n' <$> inlineWith done env val <*>
50 inlineWith done ((n, LV n') : env) sc
51 inlineWith done env (LLam args sc)
52 = do ns' <- mapM (\n -> do n' <- nextN
53 return (n, n')) args
54 LLam (map snd ns') <$>
55 inlineWith done (map (\ (n,n') -> (n, LV n')) ns' ++ env) sc
56 inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i
57 inlineWith done env (LCon loc i n es)
58 = LCon loc i n <$> mapM (inlineWith done env) es
59 inlineWith done env (LCase ty e alts)
60 = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts
61 inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es
62 -- the interesting case!
63 inlineWith done env (LApp t (LV n) es)
64 | n `notElem` done,
65 [LFun opts _ args body] <- lookupCtxt n defs,
66 Inline `elem` opts,
67 length es == length args
68 = do es' <- mapM (inlineWith done env) es
69 inlineWith (n : done) (zip args es' ++ env) body
70 inlineWith done env (LApp t f es)
71 = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es
72 inlineWith done env (LForeign t s args)
73 = LForeign t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e
74 return (t, e')) args
75 inlineWith done env t = return t
77 inlineWithAlt done env (LConCase i n es rhs)
78 = do ns' <- mapM (\n -> do n' <- nextN
79 return (n, n')) es
80 LConCase i n (map snd ns') <$>
81 inlineWith done (map (\ (n,n') -> (n, LV n')) ns' ++ env) rhs
82 inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e
83 inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e