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