git.iko.soy/Idris-dev
on 4ade674 help sign in
Idris-dev/src/IRTS/Simplified.hs
232 lines 9.5 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 Idris.Core.CaseTree
11import Idris.Core.TT
12import Idris.Core.Typecheck
13import IRTS.Defunctionalise
15import Control.Monad.State
16import Data.Maybe
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
46ldefs :: State (DDefs, Int) DDefs
47ldefs = do (l, h) <- get
48 return l
50-- | Simplify an expression by let-binding argument expressions that
51-- are not variables
52-- The boolean parameter indicates whether the expression is at tail
53-- call position.
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) = bindExprs args (SApp (tl || tc) n)
62simplify tl (DForeign ty fn args)
63 = let (fdescs, exprs) = unzip args
64 in bindExprs exprs (\vars -> SForeign ty fn (zip fdescs vars))
65simplify tl (DLet n v e) = do v' <- simplify False v
66 e' <- simplify tl e
67 return (SLet (Glob n) v' e')
68simplify tl (DUpdate n e) = do e' <- simplify False e
69 return (SUpdate (Glob n) e')
70simplify tl (DC loc i n args) = bindExprs args (SCon loc i n)
71simplify tl (DProj t i) = bindExpr t (\var -> SProj var i)
72simplify tl (DCase up e alts)
73 = do alts' <- mapM (sAlt tl) alts
74 bindExpr e (\var -> SCase up var alts')
75simplify tl (DChkCase e alts)
76 = do alts' <- mapM (sAlt tl) alts
77 bindExpr e (\var -> SChkCase var alts')
78simplify tl (DConst c) = return (SConst c)
79simplify tl (DOp p args) = bindExprs args (SOp p)
80simplify tl DNothing = return SNothing
81simplify tl (DError str) = return $ SError str
84-- | Let-bind a list of expressions to variables and construct the
85-- inner expression with the bound variables.
86-- If an expression in the list is already a variable we don’t bind it
87-- again.
88bindExprs :: [DExp] -> ([LVar] -> SExp) -> State (DDefs, Int) SExp
89bindExprs es f = bindExprs' es f [] where
90 bindExprs' [] f vars = return $ f (reverse vars)
91 bindExprs' (e:es) f vars =
92 bindExprM e (\var -> bindExprs' es f (var:vars))
94-- | Special case of 'bindExprs' for just one expression
95bindExpr :: DExp -> (LVar -> SExp) -> State (DDefs, Int) SExp
96bindExpr e f = bindExprM e (return . f)
98bindExprM :: DExp -> (LVar -> State (DDefs, Int) SExp) -> State (DDefs, Int) SExp
99bindExprM (DV (Glob x)) f
100 = do ctxt <- ldefs
101 case lookupCtxtExact x ctxt of
102 Just (DConstructor _ t 0) -> bindExprM (DC Nothing t x []) f
103 _ -> f (Glob x)
104bindExprM (DV var) f = f var
105bindExprM e f =
106 do e' <- simplify False e
107 var <- freshVar
108 f' <- f var
109 return $ SLet var e' f'
110 where
111 freshVar = do (defs, i) <- get
112 put (defs, i + 1)
113 return (Glob (sMN i "R"))
116sAlt :: Bool -> DAlt -> State (DDefs, Int) SAlt
117sAlt tl (DConCase i n args e) = do e' <- simplify tl e
118 return (SConCase (-1) i n args e')
119sAlt tl (DConstCase c e) = do e' <- simplify tl e
120 return (SConstCase c e')
121sAlt tl (DDefaultCase e) = do e' <- simplify tl e
122 return (SDefaultCase e')
124simplifyDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
125simplifyDefs ctxt [] = return []
126simplifyDefs ctxt (con@(n, DConstructor _ _ _) : xs)
127 = do xs' <- simplifyDefs ctxt xs
128 return xs'
129simplifyDefs ctxt ((n, DFun n' args exp) : xs)
130 = do let sexp = evalState (simplify True exp) (ctxt, 0)
131 (exp', locs) <- runStateT (scopecheck n ctxt (zip args [0..]) sexp) (length args)
132 xs' <- simplifyDefs ctxt xs
133 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')
135lvar v = do i <- get
136 put (max i v)
138scopecheck :: Name -> DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
139scopecheck fn ctxt envTop tm = sc envTop tm where
140 failsc err = fail $ "Codegen error in " ++ show fn ++ ":" ++ err
142 sc env (SV (Glob n)) =
143 case lookup n (reverse env) of -- most recent first
144 Just i -> do lvar i; return (SV (Loc i))
145 Nothing -> case lookupCtxtExact n ctxt of
146 Just (DConstructor _ i ar) ->
147 if True -- ar == 0
148 then return (SCon Nothing i n [])
149 else failsc $ "Constructor " ++ show n ++
150 " has arity " ++ show ar
151 Just _ -> return (SV (Glob n))
152 Nothing -> failsc $ "No such variable " ++ show n
153 sc env (SApp tc f args)
154 = do args' <- mapM (scVar env) args
155 case lookupCtxtExact f ctxt of
156 Just (DConstructor n tag ar) ->
157 if True -- (ar == length args)
158 then return $ SCon Nothing tag n args'
159 else failsc $ "Constructor " ++ show f ++
160 " has arity " ++ show ar
161 Just _ -> return $ SApp tc f args'
162 Nothing -> failsc $ "No such variable " ++ show f
163 sc env (SForeign ty f args)
164 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
165 return (t, a')) args
166 return $ SForeign ty f args'
167 sc env (SCon loc tag f args)
168 = do loc' <- case loc of
169 Nothing -> return Nothing
170 Just l -> do l' <- scVar env l
171 return (Just l')
172 args' <- mapM (scVar env) args
173 case lookupCtxtExact f ctxt of
174 Just (DConstructor n tag ar) ->
175 if True -- (ar == length args)
176 then return $ SCon loc' tag n args'
177 else failsc $ "Constructor " ++ show f ++
178 " has arity " ++ show ar
179 _ -> failsc $ "No such constructor " ++ show f
180 sc env (SProj e i)
181 = do e' <- scVar env e
182 return (SProj e' i)
183 sc env (SCase up e alts)
184 = do e' <- scVar env e
185 alts' <- mapM (scalt env) alts
186 return (SCase up e' alts')
187 sc env (SChkCase e alts)
188 = do e' <- scVar env e
189 alts' <- mapM (scalt env) alts
190 return (SChkCase e' alts')
191 sc env (SLet (Glob n) v e)
192 = do let env' = env ++ [(n, length env)]
193 v' <- sc env v
194 n' <- scVar env' (Glob n)
195 e' <- sc env' e
196 return (SLet n' v' e')
197 sc env (SUpdate (Glob n) e)
198 = do -- n already in env
199 e' <- sc env e
200 n' <- scVar env (Glob n)
201 return (SUpdate n' e')
202 sc env (SOp prim args)
203 = do args' <- mapM (scVar env) args
204 return (SOp prim args')
205 sc env x = return x
207 scVar env (Glob n) =
208 case lookup n (reverse env) of -- most recent first
209 Just i -> do lvar i; return (Loc i)
210 Nothing -> case lookupCtxtExact n ctxt of
211 Just (DConstructor _ i ar) ->
212 failsc "can't pass constructor here"
213 Just _ -> return (Glob n)
214 Nothing -> failsc $ "No such variable " ++ show n ++
215 " in " ++ show tm ++ " " ++ show envTop
216 scVar _ x = return x
218 scalt env (SConCase _ i n args e)
219 = do let env' = env ++ zip args [length env..]
220 tag <- case lookupCtxtExact n ctxt of
221 Just (DConstructor _ i ar) ->
222 if True -- (length args == ar)
223 then return i
224 else failsc $ "Constructor " ++ show n ++
225 " has arity " ++ show ar
226 _ -> failsc $ "No constructor " ++ show n
227 e' <- sc env' e
228 return (SConCase (length env) tag n args e')
229 scalt env (SConstCase c e) = do e' <- sc env e
230 return (SConstCase c e')
231 scalt env (SDefaultCase e) = do e' <- sc env e
232 return (SDefaultCase e')