git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/IRTS/Simplified.hs
228 lines 9.3 kB history raw
1{-|
2Module : IRTS.Simplified
3Description : Simplified expressions, where functions/constructors can only be applied to variables.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE FlexibleContexts #-}
9module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
11import Idris.Core.CaseTree
12import Idris.Core.TT
13import IRTS.Defunctionalise
15import Control.Monad.State
17data SExp = SV LVar
18 | SApp Bool Name [LVar]
19 | SLet LVar SExp SExp
20 | SUpdate LVar SExp
21 | SCon (Maybe LVar) -- location to reallocate, if available
22 Int Name [LVar]
23 | SCase CaseType LVar [SAlt]
24 | SChkCase LVar [SAlt]
25 | SProj LVar Int
26 | SConst Const
27 -- Keep DExps for describing foreign things, because they get
28 -- translated differently
29 | SForeign FDesc FDesc [(FDesc, LVar)]
30 | SOp PrimFn [LVar]
31 | SNothing -- erased value, will never be inspected
32 | SError String
33 deriving Show
35data SAlt = SConCase Int Int Name [Name] SExp
36 | SConstCase Const SExp
37 | SDefaultCase SExp
38 deriving Show
40data SDecl = SFun Name [Name] Int SExp
41 deriving Show
44ldefs :: State (DDefs, Int) DDefs
45ldefs = do (l, h) <- get
46 return l
48-- | Simplify an expression by let-binding argument expressions that
49-- are not variables
50-- The boolean parameter indicates whether the expression is at tail
51-- call position.
52simplify :: Bool -> DExp -> State (DDefs, Int) SExp
53simplify tl (DV x)
54 = do ctxt <- ldefs
55 case lookupCtxtExact x ctxt of
56 Just (DConstructor _ t 0) -> return $ SCon Nothing t x []
57 _ -> return $ SV (Glob x)
58simplify tl (DApp tc n args) = bindExprs args (SApp (tl || tc) n)
59simplify tl (DForeign ty fn args)
60 = let (fdescs, exprs) = unzip args
61 in bindExprs exprs (\vars -> SForeign ty fn (zip fdescs vars))
62simplify tl (DLet n v e) = do v' <- simplify False v
63 e' <- simplify tl e
64 return (SLet (Glob n) v' e')
65simplify tl (DUpdate n e) = do e' <- simplify False e
66 return (SUpdate (Glob n) e')
67simplify tl (DC loc i n args) = bindExprs args (SCon (Glob <$> loc) i n)
68simplify tl (DProj t i) = bindExpr t (\var -> SProj var i)
69simplify tl (DCase up e alts)
70 = do alts' <- mapM (sAlt tl) alts
71 bindExpr e (\var -> SCase up var alts')
72simplify tl (DChkCase e alts)
73 = do alts' <- mapM (sAlt tl) alts
74 bindExpr e (\var -> SChkCase var alts')
75simplify tl (DConst c) = return (SConst c)
76simplify tl (DOp p args) = bindExprs args (SOp p)
77simplify tl DNothing = return SNothing
78simplify tl (DError str) = return $ SError str
81-- | Let-bind a list of expressions to variables and construct the
82-- inner expression with the bound variables.
83-- If an expression in the list is already a variable we don’t bind it
84-- again.
85bindExprs :: [DExp] -> ([LVar] -> SExp) -> State (DDefs, Int) SExp
86bindExprs es f = bindExprs' es f [] where
87 bindExprs' [] f vars = return $ f (reverse vars)
88 bindExprs' (e:es) f vars =
89 bindExprM e (\var -> bindExprs' es f (var:vars))
91-- | Special case of 'bindExprs' for just one expression
92bindExpr :: DExp -> (LVar -> SExp) -> State (DDefs, Int) SExp
93bindExpr e f = bindExprM e (return . f)
95bindExprM :: DExp -> (LVar -> State (DDefs, Int) SExp) -> State (DDefs, Int) SExp
96bindExprM (DV x) f
97 = do ctxt <- ldefs
98 case lookupCtxtExact x ctxt of
99 Just (DConstructor _ t 0) -> bindExprM (DC Nothing t x []) f
100 _ -> f (Glob x)
101bindExprM e f =
102 do e' <- simplify False e
103 var <- freshVar
104 f' <- f var
105 return $ SLet var e' f'
106 where
107 freshVar = do (defs, i) <- get
108 put (defs, i + 1)
109 return (Glob (sMN i "R"))
112sAlt :: Bool -> DAlt -> State (DDefs, Int) SAlt
113sAlt tl (DConCase i n args e) = do e' <- simplify tl e
114 return (SConCase (-1) i n args e')
115sAlt tl (DConstCase c e) = do e' <- simplify tl e
116 return (SConstCase c e')
117sAlt tl (DDefaultCase e) = do e' <- simplify tl e
118 return (SDefaultCase e')
120simplifyDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
121simplifyDefs ctxt [] = return []
122simplifyDefs ctxt (con@(n, DConstructor _ _ _) : xs)
123 = do xs' <- simplifyDefs ctxt xs
124 return xs'
125simplifyDefs ctxt ((n, DFun n' args exp) : xs)
126 = do let sexp = evalState (simplify True exp) (ctxt, 0)
127 (exp', locs) <- runStateT (scopecheck n ctxt (zip args [0..]) sexp) (length args)
128 xs' <- simplifyDefs ctxt xs
129 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')
131lvar v = do i <- get
132 put (max i v)
134scopecheck :: Name -> DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
135scopecheck fn ctxt envTop tm = sc envTop tm where
136 failsc err = fail $ "Codegen error in " ++ show fn ++ ":" ++ err
138 sc env (SV (Glob n)) =
139 case lookup n (reverse env) of -- most recent first
140 Just i -> do lvar i; return (SV (Loc i))
141 Nothing -> case lookupCtxtExact n ctxt of
142 Just (DConstructor _ i ar) ->
143 if True -- ar == 0
144 then return (SCon Nothing i n [])
145 else failsc $ "Constructor " ++ show n ++
146 " has arity " ++ show ar
147 Just _ -> return (SV (Glob n))
148 Nothing -> failsc $ "No such variable " ++ show n
149 sc env (SApp tc f args)
150 = do args' <- mapM (scVar env) args
151 case lookupCtxtExact f ctxt of
152 Just (DConstructor n tag ar) ->
153 if True -- (ar == length args)
154 then return $ SCon Nothing tag n args'
155 else failsc $ "Constructor " ++ show f ++
156 " has arity " ++ show ar
157 Just _ -> return $ SApp tc f args'
158 Nothing -> failsc $ "No such variable " ++ show f
159 sc env (SForeign ty f args)
160 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
161 return (t, a')) args
162 return $ SForeign ty f args'
163 sc env (SCon loc tag f args)
164 = do loc' <- case loc of
165 Nothing -> return Nothing
166 Just l -> do l' <- scVar env l
167 return (Just l')
168 args' <- mapM (scVar env) args
169 case lookupCtxtExact f ctxt of
170 Just (DConstructor n tag ar) ->
171 if True -- (ar == length args)
172 then return $ SCon loc' tag n args'
173 else failsc $ "Constructor " ++ show f ++
174 " has arity " ++ show ar
175 _ -> failsc $ "No such constructor " ++ show f
176 sc env (SProj e i)
177 = do e' <- scVar env e
178 return (SProj e' i)
179 sc env (SCase up e alts)
180 = do e' <- scVar env e
181 alts' <- mapM (scalt env) alts
182 return (SCase up e' alts')
183 sc env (SChkCase e alts)
184 = do e' <- scVar env e
185 alts' <- mapM (scalt env) alts
186 return (SChkCase e' alts')
187 sc env (SLet (Glob n) v e)
188 = do let env' = env ++ [(n, length env)]
189 v' <- sc env v
190 n' <- scVar env' (Glob n)
191 e' <- sc env' e
192 return (SLet n' v' e')
193 sc env (SUpdate (Glob n) e)
194 = do -- n already in env
195 e' <- sc env e
196 n' <- scVar env (Glob n)
197 return (SUpdate n' e')
198 sc env (SOp prim args)
199 = do args' <- mapM (scVar env) args
200 return (SOp prim args')
201 sc env x = return x
203 scVar env (Glob n) =
204 case lookup n (reverse env) of -- most recent first
205 Just i -> do lvar i; return (Loc i)
206 Nothing -> case lookupCtxtExact n ctxt of
207 Just (DConstructor _ i ar) ->
208 failsc "can't pass constructor here"
209 Just _ -> return (Glob n)
210 Nothing -> failsc $ "No such variable " ++ show n ++
211 " in " ++ show tm ++ " " ++ show envTop
212 scVar _ x = return x
214 scalt env (SConCase _ i n args e)
215 = do let env' = env ++ zip args [length env..]
216 tag <- case lookupCtxtExact n ctxt of
217 Just (DConstructor _ i ar) ->
218 if True -- (length args == ar)
219 then return i
220 else failsc $ "Constructor " ++ show n ++
221 " has arity " ++ show ar
222 _ -> failsc $ "No constructor " ++ show n
223 e' <- sc env' e
224 return (SConCase (length env) tag n args e')
225 scalt env (SConstCase c e) = do e' <- sc env e
226 return (SConstCase c e')
227 scalt env (SDefaultCase e) = do e' <- sc env e
228 return (SDefaultCase e')