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