git.iko.soy/Idris-dev
on 22bcbd3 help sign in
Idris-dev/src/IRTS/Simplified.hs
231 lines 9.4 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-}
8{-# LANGUAGE FlexibleContexts #-}
9module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
11import Idris.Core.CaseTree
12import Idris.Core.TT
13import Idris.Core.Typecheck
14import IRTS.Defunctionalise
16import Control.Monad.State
17import Data.Maybe
18import Debug.Trace
20data SExp = SV LVar
21 | SApp Bool Name [LVar]
22 | SLet LVar SExp SExp
23 | SUpdate LVar SExp
24 | SCon (Maybe LVar) -- location to reallocate, if available
25 Int Name [LVar]
26 | SCase CaseType LVar [SAlt]
27 | SChkCase LVar [SAlt]
28 | SProj LVar Int
29 | SConst Const
30 -- Keep DExps for describing foreign things, because they get
31 -- translated differently
32 | SForeign FDesc FDesc [(FDesc, LVar)]
33 | SOp PrimFn [LVar]
34 | SNothing -- erased value, will never be inspected
35 | SError String
36 deriving Show
38data SAlt = SConCase Int Int Name [Name] SExp
39 | SConstCase Const SExp
40 | SDefaultCase SExp
41 deriving Show
43data SDecl = SFun Name [Name] Int SExp
44 deriving Show
47ldefs :: State (DDefs, Int) DDefs
48ldefs = do (l, h) <- get
49 return l
51-- | Simplify an expression by let-binding argument expressions that
52-- are not variables
53-- The boolean parameter indicates whether the expression is at tail
54-- call position.
55simplify :: Bool -> DExp -> State (DDefs, Int) SExp
56simplify tl (DV 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 (Glob <$> 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 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 e f =
105 do e' <- simplify False e
106 var <- freshVar
107 f' <- f var
108 return $ SLet var e' f'
109 where
110 freshVar = do (defs, i) <- get
111 put (defs, i + 1)
112 return (Glob (sMN i "R"))
115sAlt :: Bool -> DAlt -> State (DDefs, Int) SAlt
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 ty f args)
163 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
164 return (t, a')) args
165 return $ SForeign 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')