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