git.iko.soy/Idris-dev
on bbbe563 help sign in
Idris-dev/src/IRTS/Simplified.hs
211 lines 8.9 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 | SProj LVar Int
20 | SConst Const
21 | SForeign FLang FType String [(FType, LVar)]
22 | SOp PrimFn [LVar]
23 | SNothing -- erased value, will never be inspected
24 | SError String
25 deriving Show
27data SAlt = SConCase Int Int Name [Name] SExp
28 | SConstCase Const SExp
29 | SDefaultCase SExp
30 deriving Show
32data SDecl = SFun Name [Name] Int SExp
33 deriving Show
35hvar :: State (DDefs, Int) Int
36hvar = do (l, h) <- get
37 put (l, h + 1)
38 return h
40ldefs :: State (DDefs, Int) DDefs
41ldefs = do (l, h) <- get
42 return l
44simplify :: Bool -> DExp -> State (DDefs, Int) SExp
45simplify tl (DV (Loc i)) = return (SV (Loc i))
46simplify tl (DV (Glob x))
47 = do ctxt <- ldefs
48 case lookupCtxt Nothing x ctxt of
49 [DConstructor _ t 0] -> return $ SCon t x []
50 _ -> return $ SV (Glob x)
51simplify tl (DApp tc n args) = do args' <- mapM sVar args
52 mkapp (SApp (tl || tc) n) args'
53simplify tl (DForeign lang ty fn args)
54 = do args' <- mapM sVar (map snd args)
55 let fargs = zip (map fst args) args'
56 mkfapp (SForeign lang ty fn) fargs
57simplify tl (DLet n v e) = do v' <- simplify False v
58 e' <- simplify tl e
59 return (SLet (Glob n) v' e')
60simplify tl (DUpdate n e) = do e' <- simplify False e
61 return (SUpdate (Glob n) e')
62simplify tl (DC i n args) = do args' <- mapM sVar args
63 mkapp (SCon i n) args'
64simplify tl (DProj t i) = do v <- sVar t
65 case v of
66 (x, Nothing) -> return (SProj x i)
67 (Glob x, Just e) ->
68 return (SLet (Glob x) e (SProj (Glob x) i))
69simplify tl (DCase e alts) = do v <- sVar e
70 alts' <- mapM (sAlt tl) alts
71 case v of
72 (x, Nothing) -> return (SCase x alts')
73 (Glob x, Just e) ->
74 return (SLet (Glob x) e (SCase (Glob x) alts'))
75simplify tl (DConst c) = return (SConst c)
76simplify tl (DOp p args) = do args' <- mapM sVar args
77 mkapp (SOp p) args'
78simplify tl DNothing = return SNothing
79simplify tl (DError str) = return $ SError str
81sVar (DV (Glob x))
82 = do ctxt <- ldefs
83 case lookupCtxt Nothing x ctxt of
84 [DConstructor _ t 0] -> sVar (DC t x [])
85 _ -> return (Glob x, Nothing)
86sVar (DV x) = return (x, Nothing)
87sVar e = do e' <- simplify False e
88 i <- hvar
89 return (Glob (MN i "R"), Just e')
91mkapp f args = mkapp' f args [] where
92 mkapp' f [] args = return $ f (reverse args)
93 mkapp' f ((x, Nothing) : xs) args = mkapp' f xs (x : args)
94 mkapp' f ((x, Just e) : xs) args
95 = do sc <- mkapp' f xs (x : args)
96 return (SLet x e sc)
98mkfapp f args = mkapp' f args [] where
99 mkapp' f [] args = return $ f (reverse args)
100 mkapp' f ((ty, (x, Nothing)) : xs) args = mkapp' f xs ((ty, x) : args)
101 mkapp' f ((ty, (x, Just e)) : xs) args
102 = do sc <- mkapp' f xs ((ty, x) : args)
103 return (SLet x e sc)
105sAlt tl (DConCase i n args e) = do e' <- simplify tl e
106 return (SConCase (-1) i n args e')
107sAlt tl (DConstCase c e) = do e' <- simplify tl e
108 return (SConstCase c e')
109sAlt tl (DDefaultCase e) = do e' <- simplify tl e
110 return (SDefaultCase e')
112checkDefs :: DDefs -> [(Name, DDecl)] -> TC [(Name, SDecl)]
113checkDefs ctxt [] = return []
114checkDefs ctxt (con@(n, DConstructor _ _ _) : xs)
115 = do xs' <- checkDefs ctxt xs
116 return xs'
117checkDefs ctxt ((n, DFun n' args exp) : xs)
118 = do let sexp = evalState (simplify True exp) (ctxt, 0)
119 (exp', locs) <- runStateT (scopecheck ctxt (zip args [0..]) sexp) (length args)
120 xs' <- checkDefs ctxt xs
121 return ((n, SFun n' args ((locs + 1) - length args) exp') : xs')
123lvar v = do i <- get
124 put (max i v)
126scopecheck :: DDefs -> [(Name, Int)] -> SExp -> StateT Int TC SExp
127scopecheck ctxt envTop tm = sc envTop tm where
128 sc env (SV (Glob n)) =
129 case lookup n (reverse env) of -- most recent first
130 Just i -> do lvar i; return (SV (Loc i))
131 Nothing -> case lookupCtxt Nothing n ctxt of
132 [DConstructor _ i ar] ->
133 if True -- ar == 0
134 then return (SCon i n [])
135 else fail $ "Codegen error: Constructor " ++ show n ++
136 " has arity " ++ show ar
137 [_] -> return (SV (Glob n))
138 [] -> fail $ "Codegen error: No such variable " ++ show n
139 sc env (SApp tc f args)
140 = do args' <- mapM (scVar env) args
141 case lookupCtxt Nothing f ctxt of
142 [DConstructor n tag ar] ->
143 if True -- (ar == length args)
144 then return $ SCon tag n args'
145 else fail $ "Codegen error: Constructor " ++ show f ++
146 " has arity " ++ show ar
147 [_] -> return $ SApp tc f args'
148 [] -> fail $ "Codegen error: No such variable " ++ show f
149 sc env (SForeign l ty f args)
150 = do args' <- mapM (\ (t, a) -> do a' <- scVar env a
151 return (t, a')) args
152 return $ SForeign l ty f args'
153 sc env (SCon tag f args)
154 = do args' <- mapM (scVar env) args
155 case lookupCtxt Nothing f ctxt of
156 [DConstructor n tag ar] ->
157 if True -- (ar == length args)
158 then return $ SCon tag n args'
159 else fail $ "Codegen error: Constructor " ++ show f ++
160 " has arity " ++ show ar
161 _ -> fail $ "Codegen error: No such constructor " ++ show f
162 sc env (SProj e i)
163 = do e' <- scVar env e
164 return (SProj e' i)
165 sc env (SCase e alts)
166 = do e' <- scVar env e
167 alts' <- mapM (scalt env) alts
168 return (SCase e' alts')
169 sc env (SLet (Glob n) v e)
170 = do let env' = env ++ [(n, length env)]
171 v' <- sc env v
172 n' <- scVar env' (Glob n)
173 e' <- sc env' e
174 return (SLet n' v' e')
175 sc env (SUpdate (Glob n) e)
176 = do -- n already in env
177 e' <- sc env e
178 n' <- scVar env (Glob n)
179 return (SUpdate n' e')
180 sc env (SOp prim args)
181 = do args' <- mapM (scVar env) args
182 return (SOp prim args')
183 sc env x = return x
185 scVar env (Glob n) =
186 case lookup n (reverse env) of -- most recent first
187 Just i -> do lvar i; return (Loc i)
188 Nothing -> case lookupCtxt Nothing n ctxt of
189 [DConstructor _ i ar] ->
190 fail $ "Codegen error : can't pass constructor here"
191 [_] -> return (Glob n)
192 [] -> fail $ "Codegen error: No such variable " ++ show n ++
193 " in " ++ show tm ++ " " ++ show envTop
194 scVar _ x = return x
196 scalt env (SConCase _ i n args e)
197 = do let env' = env ++ zip args [length env..]
198 tag <- case lookupCtxt Nothing n ctxt of
199 [DConstructor _ i ar] ->
200 if True -- (length args == ar)
201 then return i
202 else fail $ "Codegen error: Constructor " ++ show n ++
203 " has arity " ++ show ar
204 _ -> fail $ "Codegen error: No constructor " ++ show n
205 e' <- sc env' e
206 return (SConCase (length env) tag n args e')
207 scalt env (SConstCase c e) = do e' <- sc env e
208 return (SConstCase c e')
209 scalt env (SDefaultCase e) = do e' <- sc env e
210 return (SDefaultCase e')