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