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