git.iko.soy/Idris-dev
on f8a6746 help sign in
Idris-dev/src/IRTS/Simplified.hs
232 lines 9.9 kB history raw
1module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
3import IRTS.Defunctionalise
4import Idris.Core.TT
5import Idris.Core.CaseTree
6import Idris.Core.Typecheck
7import Data.Maybe
8import Control.Monad.State
10import Debug.Trace
12-- Simplified expressions, where functions/constructors can only be applied
13-- to variables
15data SExp = SV LVar
16 | SApp Bool Name [LVar]
17 | SLet LVar SExp SExp
18 | SUpdate LVar SExp
19 | SCon (Maybe LVar) -- location to reallocate, if available
20 Int Name [LVar]
21 | SCase CaseType LVar [SAlt]
22 | SChkCase LVar [SAlt]
23 | SProj LVar Int
24 | SConst Const
25 | SForeign FLang FType String [(FType, LVar)]
26 | SOp PrimFn [LVar]
27 | SNothing -- erased value, will never be inspected
28 | SError String
29 deriving Show
31data SAlt = SConCase Int Int Name [Name] SExp
32 | SConstCase Const SExp
33 | SDefaultCase SExp
34 deriving Show
36data SDecl = SFun Name [Name] Int SExp
37 deriving Show
39hvar :: State (DDefs, Int) Int
40hvar = do (l, h) <- get
41 put (l, h + 1)
42 return h
44ldefs :: State (DDefs, Int) DDefs
45ldefs = do (l, h) <- get
46 return l
48simplify :: Bool -> DExp -> State (DDefs, Int) SExp
49simplify tl (DV (Loc i)) = return (SV (Loc i))
50simplify tl (DV (Glob x))
51 = do ctxt <- ldefs
52 case lookupCtxtExact x ctxt of
53 Just (DConstructor _ t 0) -> return $ SCon Nothing t x []
54 _ -> return $ SV (Glob x)
55simplify tl (DApp tc n args) = do args' <- mapM sVar args
56 mkapp (SApp (tl || tc) n) args'
57simplify tl (DForeign lang ty fn args)
58 = do args' <- mapM sVar (map snd args)
59 let fargs = zip (map fst args) args'
60 mkfapp (SForeign lang ty fn) fargs
61simplify tl (DLet n v e) = do v' <- simplify False v
62 e' <- simplify tl e
63 return (SLet (Glob n) v' e')
64simplify tl (DUpdate n e) = do e' <- simplify False e
65 return (SUpdate (Glob n) e')
66simplify tl (DC loc i n args) = do args' <- mapM sVar args
67 mkapp (SCon loc i n) args'
68simplify tl (DProj t i) = do v <- sVar t
69 case v of
70 (x, Nothing) -> return (SProj x i)
71 (Glob x, Just e) ->
72 return (SLet (Glob x) e (SProj (Glob x) i))
73simplify tl (DCase up e alts) = do v <- sVar e
74 alts' <- mapM (sAlt tl) alts
75 case v of
76 (x, Nothing) -> return (SCase up x alts')
77 (Glob x, Just e) ->
78 return (SLet (Glob x) e (SCase up (Glob x) alts'))
79simplify tl (DChkCase e alts)
80 = do v <- sVar e
81 alts' <- mapM (sAlt tl) alts
82 case v of
83 (x, Nothing) -> return (SChkCase x alts')
84 (Glob x, Just e) ->
85 return (SLet (Glob x) e (SChkCase (Glob x) alts'))
86simplify tl (DConst c) = return (SConst c)
87simplify tl (DOp p args) = do args' <- mapM sVar args
88 mkapp (SOp p) args'
89simplify tl DNothing = return SNothing
90simplify tl (DError str) = return $ SError str
92sVar (DV (Glob x))
93 = do ctxt <- ldefs
94 case lookupCtxtExact x ctxt of
95 Just (DConstructor _ t 0) -> sVar (DC Nothing t x [])
96 _ -> return (Glob x, Nothing)
97sVar (DV x) = return (x, Nothing)
98sVar e = do e' <- simplify False e
99 i <- hvar
100 return (Glob (sMN i "R"), Just e')
102mkapp f args = mkapp' f args [] where
103 mkapp' f [] args = return $ f (reverse args)
104 mkapp' f ((x, Nothing) : xs) args = mkapp' f xs (x : args)
105 mkapp' f ((x, Just e) : xs) args
106 = do sc <- mkapp' f xs (x : args)
107 return (SLet x e sc)
109mkfapp f args = mkapp' f args [] where
110 mkapp' f [] args = return $ f (reverse args)
111 mkapp' f ((ty, (x, Nothing)) : xs) args = mkapp' f xs ((ty, x) : args)
112 mkapp' f ((ty, (x, Just e)) : xs) args
113 = do sc <- mkapp' f xs ((ty, x) : args)
114 return (SLet x e sc)
116sAlt tl (DConCase i n args e) = do e' <- simplify tl e
117 return (SConCase (-1) i n args e')
118sAlt tl (DConstCase c e) = do e' <- simplify tl e
119 return (SConstCase c e')
120sAlt tl (DDefaultCase e) = do e' <- simplify tl e
121 return (SDefaultCase e')
123simplifyDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
124simplifyDefs ctxt [] = return []
125simplifyDefs ctxt (con@(n, DConstructor _ _ _) : xs)
126 = do xs' <- simplifyDefs ctxt xs
127 return xs'
128simplifyDefs ctxt ((n, DFun n' args exp) : xs)
129 = do let sexp = evalState (simplify True exp) (ctxt, 0)
130 (exp', locs) <- runStateT (scopecheck n ctxt (zip args [0..]) sexp) (length args)
131 xs' <- simplifyDefs ctxt xs
132 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')
134lvar v = do i <- get
135 put (max i v)
137scopecheck :: Name -> DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
138scopecheck fn ctxt envTop tm = sc envTop tm where
139 failsc err = fail $ "Codegen error in " ++ show fn ++ ":" ++ err
141 sc env (SV (Glob n)) =
142 case lookup n (reverse env) of -- most recent first
143 Just i -> do lvar i; return (SV (Loc i))
144 Nothing -> case lookupCtxtExact n ctxt of
145 Just (DConstructor _ i ar) ->
146 if True -- ar == 0
147 then return (SCon Nothing i n [])
148 else failsc $ "Constructor " ++ show n ++
149 " has arity " ++ show ar
150 Just _ -> return (SV (Glob n))
151 Nothing -> failsc $ "No such variable " ++ show n
152 sc env (SApp tc f args)
153 = do args' <- mapM (scVar env) args
154 case lookupCtxtExact f ctxt of
155 Just (DConstructor n tag ar) ->
156 if True -- (ar == length args)
157 then return $ SCon Nothing tag n args'
158 else failsc $ "Constructor " ++ show f ++
159 " has arity " ++ show ar
160 Just _ -> return $ SApp tc f args'
161 Nothing -> failsc $ "No such variable " ++ show f
162 sc env (SForeign l ty f args)
163 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
164 return (t, a')) args
165 return $ SForeign l ty f args'
166 sc env (SCon loc tag f args)
167 = do loc' <- case loc of
168 Nothing -> return Nothing
169 Just l -> do l' <- scVar env l
170 return (Just l')
171 args' <- mapM (scVar env) args
172 case lookupCtxtExact f ctxt of
173 Just (DConstructor n tag ar) ->
174 if True -- (ar == length args)
175 then return $ SCon loc' tag n args'
176 else failsc $ "Constructor " ++ show f ++
177 " has arity " ++ show ar
178 _ -> failsc $ "No such constructor " ++ show f
179 sc env (SProj e i)
180 = do e' <- scVar env e
181 return (SProj e' i)
182 sc env (SCase up e alts)
183 = do e' <- scVar env e
184 alts' <- mapM (scalt env) alts
185 return (SCase up e' alts')
186 sc env (SChkCase e alts)
187 = do e' <- scVar env e
188 alts' <- mapM (scalt env) alts
189 return (SChkCase e' alts')
190 sc env (SLet (Glob n) v e)
191 = do let env' = env ++ [(n, length env)]
192 v' <- sc env v
193 n' <- scVar env' (Glob n)
194 e' <- sc env' e
195 return (SLet n' v' e')
196 sc env (SUpdate (Glob n) e)
197 = do -- n already in env
198 e' <- sc env e
199 n' <- scVar env (Glob n)
200 return (SUpdate n' e')
201 sc env (SOp prim args)
202 = do args' <- mapM (scVar env) args
203 return (SOp prim args')
204 sc env x = return x
206 scVar env (Glob n) =
207 case lookup n (reverse env) of -- most recent first
208 Just i -> do lvar i; return (Loc i)
209 Nothing -> case lookupCtxtExact n ctxt of
210 Just (DConstructor _ i ar) ->
211 failsc $ "can't pass constructor here"
212 Just _ -> return (Glob n)
213 Nothing -> failsc $ "No such variable " ++ show n ++
214 " in " ++ show tm ++ " " ++ show envTop
215 scVar _ x = return x
217 scalt env (SConCase _ i n args e)
218 = do let env' = env ++ zip args [length env..]
219 tag <- case lookupCtxtExact n ctxt of
220 Just (DConstructor _ i ar) ->
221 if True -- (length args == ar)
222 then return i
223 else failsc $ "Constructor " ++ show n ++
224 " has arity " ++ show ar
225 _ -> failsc $ "No constructor " ++ show n
226 e' <- sc env' e
227 return (SConCase (length env) tag n args e')
228 scalt env (SConstCase c e) = do e' <- sc env e
229 return (SConstCase c e')
230 scalt env (SDefaultCase e) = do e' <- sc env e
231 return (SDefaultCase e')