git.iko.soy/Idris-dev
on 168706f help sign in
Idris-dev/src/IRTS/Simplified.hs
181 lines 7.6 kB history raw
1module IRTS.Simplified where
3import IRTS.Lang
4import Core.TT
5import Data.Maybe
6import Control.Monad.State
8-- Simplified expressions, where functions/constructors can only be applied
9-- to variables
11data SExp = SV LVar
12 | SApp Bool Name [LVar]
13 | SLet LVar SExp SExp
14 | SCon Int Name [LVar]
15 | SCase LVar [SAlt]
16 | SConst Const
17 | SForeign FLang FType String [(FType, LVar)]
18 | SOp PrimFn [LVar]
19 deriving Show
21data SAlt = SConCase Int Int Name [Name] SExp
22 | SConstCase Const SExp
23 | SDefaultCase SExp
24 deriving Show
26data SDecl = SFun Name [Name] Int SExp
27 deriving Show
29hvar :: State (LDefs, Int) Int
30hvar = do (l, h) <- get
31 put (l, h + 1)
32 return h
34ldefs :: State (LDefs, Int) LDefs
35ldefs = do (l, h) <- get
36 return l
38simplify :: Bool -> LExp -> State (LDefs, Int) SExp
39simplify tl (LV (Loc i)) = return (SV (Loc i))
40simplify tl (LV (Glob x))
41 = do ctxt <- ldefs
42 case lookupCtxt Nothing x ctxt of
43 [LConstructor _ t 0] -> return $ SCon t x []
44 _ -> return $ SV (Glob x)
45simplify tl (LApp tc n args) = do args' <- mapM sVar args
46 mkapp (SApp (tl || tc) n) args'
47simplify tl (LForeign lang ty fn args)
48 = do args' <- mapM sVar (map snd args)
49 let fargs = zip (map fst args) args'
50 mkfapp (SForeign lang ty fn) fargs
51simplify tl (LLet n v e) = do v' <- simplify False v
52 e' <- simplify tl e
53 return (SLet (Glob n) v' e')
54simplify tl (LCon i n args) = do args' <- mapM sVar args
55 mkapp (SCon i n) args'
56simplify tl (LCase e alts) = do v <- sVar e
57 alts' <- mapM (sAlt tl) alts
58 case v of
59 (x, Nothing) -> return (SCase x alts')
60 (Glob x, Just e) ->
61 return (SLet (Glob x) e (SCase (Glob x) alts'))
62simplify tl (LConst c) = return (SConst c)
63simplify tl (LOp p args) = do args' <- mapM sVar args
64 mkapp (SOp p) args'
66sVar (LV (Glob x))
67 = do ctxt <- ldefs
68 case lookupCtxt Nothing x ctxt of
69 [LConstructor _ t 0] -> sVar (LCon t x [])
70 _ -> return (Glob x, Nothing)
71sVar (LV x) = return (x, Nothing)
72sVar e = do e' <- simplify False e
73 i <- hvar
74 return (Glob (MN i "R"), Just e')
76mkapp f args = mkapp' f args [] where
77 mkapp' f [] args = return $ f (reverse args)
78 mkapp' f ((x, Nothing) : xs) args = mkapp' f xs (x : args)
79 mkapp' f ((x, Just e) : xs) args
80 = do sc <- mkapp' f xs (x : args)
81 return (SLet x e sc)
83mkfapp f args = mkapp' f args [] where
84 mkapp' f [] args = return $ f (reverse args)
85 mkapp' f ((ty, (x, Nothing)) : xs) args = mkapp' f xs ((ty, x) : args)
86 mkapp' f ((ty, (x, Just e)) : xs) args
87 = do sc <- mkapp' f xs ((ty, x) : args)
88 return (SLet x e sc)
90sAlt tl (LConCase i n args e) = do e' <- simplify tl e
91 return (SConCase (-1) i n args e')
92sAlt tl (LConstCase c e) = do e' <- simplify tl e
93 return (SConstCase c e')
94sAlt tl (LDefaultCase e) = do e' <- simplify tl e
95 return (SDefaultCase e')
97checkDefs :: LDefs -> [(Name, LDecl)] -> TC [(Name, SDecl)]
98checkDefs ctxt [] = return []
99checkDefs ctxt (con@(n, LConstructor _ _ _) : xs)
100 = do xs' <- checkDefs ctxt xs
101 return xs'
102checkDefs ctxt ((n, LFun n' args exp) : xs)
103 = do let sexp = evalState (simplify True exp) (ctxt, 0)
104 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (-1)
105 xs' <- checkDefs ctxt xs
106 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')
108lvar v = do i <- get
109 put (max i v)
111scopecheck :: LDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
112scopecheck ctxt env tm = sc env tm where
113 sc env (SV (Glob n)) =
114 case lookup n (reverse env) of -- most recent first
115 Just i -> do lvar i; return (SV (Loc i))
116 Nothing -> case lookupCtxt Nothing n ctxt of
117 [LConstructor _ i ar] ->
118 if ar == 0 then return (SCon i n [])
119 else fail $ "Codegen error: Constructor " ++ show n ++
120 " has arity " ++ show ar
121 [_] -> return (SV (Glob n))
122 [] -> fail $ "Codegen error: No such variable " ++ show n
123 sc env (SApp tc f args)
124 = do args' <- mapM (scVar env) args
125 case lookupCtxt Nothing f ctxt of
126 [LConstructor n tag ar] ->
127 if (ar == length args)
128 then return $ SCon tag n args'
129 else fail $ "Codegen error: Constructor " ++ show f ++
130 " has arity " ++ show ar
131 [_] -> return $ SApp tc f args'
132 [] -> fail $ "Codegen error: No such variable " ++ show f
133 sc env (SCon tag f args)
134 = do args' <- mapM (scVar env) args
135 case lookupCtxt Nothing f ctxt of
136 [LConstructor n tag ar] ->
137 if (ar == length args)
138 then return $ SCon tag n args'
139 else fail $ "Codegen error: Constructor " ++ show f ++
140 " has arity " ++ show ar
141 _ -> fail $ "Codegen error: No such constructor " ++ show f
142 sc env (SCase e alts)
143 = do e' <- scVar env e
144 alts' <- mapM (scalt env) alts
145 return (SCase e' alts')
146 sc env (SLet (Glob n) v e)
147 = do let env' = env ++ [(n, length env)]
148 v' <- sc env v
149 n' <- scVar env' (Glob n)
150 e' <- sc env' e
151 return (SLet n' v' e')
152 sc env (SOp prim args)
153 = do args' <- mapM (scVar env) args
154 return (SOp prim args')
155 sc env x = return x
157 scVar env (Glob n) =
158 case lookup n (reverse env) of -- most recent first
159 Just i -> do lvar i; return (Loc i)
160 Nothing -> case lookupCtxt Nothing n ctxt of
161 [LConstructor _ i ar] ->
162 fail $ "Codegen error : can't pass constructor here"
163 [_] -> return (Glob n)
164 [] -> fail $ "Codegen error: No such variable " ++ show n
165 scVar _ x = return x
167 scalt env (SConCase _ i n args e)
168 = do let env' = env ++ zip args [length env..]
169 tag <- case lookupCtxt Nothing n ctxt of
170 [LConstructor _ i ar] ->
171 if (length args == ar) then return i
172 else fail $ "Codegen error: Constructor " ++ show n ++
173 " has arity " ++ show ar
174 _ -> fail $ "Codegen error: No constructor " ++ show n
175 e' <- sc env' e
176 return (SConCase (length env) tag n args e')
177 scalt env (SConstCase c e) = do e' <- sc env e
178 return (SConstCase c e')
179 scalt env (SDefaultCase e) = do e' <- sc env e
180 return (SDefaultCase e')