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