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