git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/IRTS/Defunctionalise.hs
325 lines 14 kB history raw
1{-|
2Module : IRTS.Defunctionalise
3Description : Defunctionalise Idris' IR.
5License : BSD3
6Maintainer : The Idris Community.
8To defunctionalise:
101. Create a data constructor for each function
112. Create a data constructor for each underapplication of a function
123. Convert underapplications to their corresponding constructors
134. Create an EVAL function which calls the appropriate function for data constructors
14 created as part of step 1
155. Create an APPLY function which adds an argument to each underapplication (or calls
16 APPLY again for an exact application)
176. Wrap overapplications in chains of APPLY
187. Wrap unknown applications (i.e. applications of local variables) in chains of APPLY
198. Add explicit EVAL to case, primitives, and foreign calls
21-}
22{-# LANGUAGE FlexibleContexts, PatternGuards #-}
23module IRTS.Defunctionalise(module IRTS.Defunctionalise
24 , module IRTS.Lang
25 ) where
27import Idris.Core.CaseTree
28import Idris.Core.TT
29import IRTS.Lang
31import Control.Monad
32import Control.Monad.State
33import Data.List
34import Data.Maybe
36data DExp = DV Name
37 | DApp Bool Name [DExp] -- True = tail call
38 | DLet Name DExp DExp -- name just for pretty printing
39 | DUpdate Name DExp -- eval expression, then update var with it
40 | DProj DExp Int
41 | DC (Maybe Name) Int Name [DExp]
42 | DCase CaseType DExp [DAlt]
43 | DChkCase DExp [DAlt] -- a case where the type is unknown (for EVAL/APPLY)
44 | DConst Const
45 | DForeign FDesc FDesc [(FDesc, DExp)]
46 | DOp PrimFn [DExp]
47 | DNothing -- erased value, can be compiled to anything since it'll never
48 -- be inspected
49 | DError String
50 deriving Eq
52data DAlt = DConCase Int Name [Name] DExp
53 | DConstCase Const DExp
54 | DDefaultCase DExp
55 deriving (Show, Eq)
57data DDecl = DFun Name [Name] DExp -- name, arg names, definition
58 | DConstructor Name Int Int -- constructor name, tag, arity
59 deriving (Show, Eq)
61type DDefs = Ctxt DDecl
63defunctionalise :: Int -> LDefs -> DDefs
64defunctionalise nexttag defs
65 = let all = toAlist defs
66 -- sort newcons so that EVAL and APPLY cons get sequential tags
67 (allD, (enames, anames)) = runState (mapM (addApps defs) all) ([], [])
68 anames' = sort (nub anames)
69 enames' = nub enames
70 newecons = sortBy conord $ concatMap (toCons enames') (getFn all)
71 newacons = sortBy conord $ concatMap (toConsA anames') (getFn all)
72 eval = mkEval newecons
73 app = mkApply newacons
74 app2 = mkApply2 newacons
75 condecls = declare nexttag (newecons ++ newacons) in
76 addAlist (eval : app : app2 : condecls ++ allD) emptyContext
77 where conord (n, _, _) (n', _, _) = compare n n'
79getFn :: [(Name, LDecl)] -> [(Name, Int)]
80getFn xs = mapMaybe fnData xs
81 where fnData (n, LFun _ _ args _) = Just (n, length args)
82 fnData _ = Nothing
84addApps :: LDefs -> (Name, LDecl) -> State ([Name], [(Name, Int)]) (Name, DDecl)
85addApps defs o@(n, LConstructor _ t a)
86 = return (n, DConstructor n t a)
87addApps defs (n, LFun _ _ args e)
88 = do e' <- aa args e
89 return (n, DFun n args e')
90 where
91 aa :: [Name] -> LExp -> State ([Name], [(Name, Int)]) DExp
92 aa env (LV n) | n `elem` env = return $ DV n
93 | otherwise = aa env (LApp False (LV n) [])
94 aa env (LApp tc (LV n) args)
95 = do args' <- mapM (aa env) args
96 case lookupCtxtExact n defs of
97 Just (LConstructor _ i ar) -> return $ DApp tc n args'
98 Just (LFun _ _ as _) -> let arity = length as in
99 fixApply tc n args' arity
100 Nothing -> return $ chainAPPLY (DV n) args'
101 aa env (LLazyApp n args)
102 = do args' <- mapM (aa env) args
103 case lookupCtxtExact n defs of
104 Just (LConstructor _ i ar) -> return $ DApp False n args'
105 Just (LFun _ _ as _) -> let arity = length as in
106 fixLazyApply n args' arity
107 Nothing -> return $ chainAPPLY (DV n) args'
108 aa env (LForce (LLazyApp n args)) = aa env (LApp False (LV n) args)
109 aa env (LForce e) = liftM eEVAL (aa env e)
110 aa env (LLet n v sc) = liftM2 (DLet n) (aa env v) (aa (n : env) sc)
111 aa env (LCon loc i n args) = liftM (DC loc i n) (mapM (aa env) args)
112 aa env (LProj t@(LV n) i)
113 | n `elem` env = do t' <- aa env t
114 return $ DProj (DUpdate n t') i
115 aa env (LProj t i) = do t' <- aa env t
116 return $ DProj t' i
117 aa env (LCase up e alts) = do e' <- aa env e
118 alts' <- mapM (aaAlt env) alts
119 return $ DCase up e' alts'
120 aa env (LConst c) = return $ DConst c
121 aa env (LForeign t n args)
122 = do args' <- mapM (aaF env) args
123 return $ DForeign t n args'
124 aa env (LOp LFork args) = liftM (DOp LFork) (mapM (aa env) args)
125 aa env (LOp f args) = do args' <- mapM (aa env) args
126 return $ DOp f args'
127 aa env LNothing = return DNothing
128 aa env (LError e) = return $ DError e
130 aaF env (t, e) = do e' <- aa env e
131 return (t, e')
133 aaAlt env (LConCase i n args e)
134 = liftM (DConCase i n args) (aa (args ++ env) e)
135 aaAlt env (LConstCase c e) = liftM (DConstCase c) (aa env e)
136 aaAlt env (LDefaultCase e) = liftM DDefaultCase (aa env e)
138 fixApply tc n args ar
139 | length args == ar
140 = return $ DApp tc n args
141 | length args < ar
142 = do (ens, ans) <- get
143 let alln = map (\x -> (n, x)) [length args .. ar]
144 put (ens, alln ++ ans)
145 return $ DApp tc (mkUnderCon n (ar - length args)) args
146 | length args > ar
147 = return $ chainAPPLY (DApp tc n (take ar args)) (drop ar args)
149 fixLazyApply n args ar
150 | length args == ar
151 = do (ens, ans) <- get
152 put (n : ens, ans)
153 return $ DApp False (mkFnCon n) args
154 | length args < ar
155 = do (ens, ans) <- get
156 let alln = map (\x -> (n, x)) [length args .. ar]
157 put (ens, alln ++ ans)
158 return $ DApp False (mkUnderCon n (ar - length args)) args
159 | length args > ar
160 = return $ chainAPPLY (DApp False n (take ar args)) (drop ar args)
162 chainAPPLY f [] = f
163-- chainAPPLY f (a : b : as)
164-- = chainAPPLY (DApp False (sMN 0 "APPLY2") [f, a, b]) as
165 chainAPPLY f (a : as) = chainAPPLY (DApp False (sMN 0 "APPLY") [f, a]) as
167eEVAL x = DApp False (sMN 0 "EVAL") [x]
169data EvalApply a = EvalCase (Name -> a)
170 | ApplyCase a
171 | Apply2Case a
173-- For a function name, generate a list of
174-- data constuctors, and whether to handle them in EVAL or APPLY
176toCons :: [Name] -> (Name, Int) -> [(Name, Int, EvalApply DAlt)]
177toCons ns (n, i)
178 | n `elem` ns
179 = (mkFnCon n, i,
180 EvalCase (\tlarg ->
181 (DConCase (-1) (mkFnCon n) (take i (genArgs 0))
182 (dupdate tlarg
183 (DApp False n (map DV (take i (genArgs 0))))))))
184 : [] -- mkApplyCase n 0 i
185 | otherwise = []
186 where dupdate tlarg x = DUpdate tlarg x
188toConsA :: [(Name, Int)] -> (Name, Int) -> [(Name, Int, EvalApply DAlt)]
189toConsA ns (n, i)
190 | Just ar <- lookup n ns
191-- = (mkFnCon n, i,
192-- EvalCase (\tlarg ->
193-- (DConCase (-1) (mkFnCon n) (take i (genArgs 0))
194-- (dupdate tlarg
195-- (DApp False n (map DV (take i (genArgs 0))))))))
196 = mkApplyCase n ar i
197 | otherwise = []
199mkApplyCase fname n ar | n == ar = []
200mkApplyCase fname n ar
201 = let nm = mkUnderCon fname (ar - n) in
202 (nm, n, ApplyCase (DConCase (-1) nm (take n (genArgs 0))
203 (DApp False (mkUnderCon fname (ar - (n + 1)))
204 (map DV (take n (genArgs 0) ++
205 [sMN 0 "arg"])))))
206 :
207 if (ar - (n + 2) >=0 )
208 then (nm, n, Apply2Case (DConCase (-1) nm (take n (genArgs 0))
209 (DApp False (mkUnderCon fname (ar - (n + 2)))
210 (map DV (take n (genArgs 0) ++
211 [sMN 0 "arg0", sMN 0 "arg1"])))))
212 :
213 mkApplyCase fname (n + 1) ar
214 else mkApplyCase fname (n + 1) ar
216mkEval :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
217mkEval xs = (sMN 0 "EVAL", DFun (sMN 0 "EVAL") [sMN 0 "arg"]
218 (mkBigCase (sMN 0 "EVAL") 256 (DV (sMN 0 "arg"))
219 (mapMaybe evalCase xs ++
220 [DDefaultCase (DV (sMN 0 "arg"))])))
221 where
222 evalCase (n, t, EvalCase x) = Just (x (sMN 0 "arg"))
223 evalCase _ = Nothing
225mkApply :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
226mkApply xs = (sMN 0 "APPLY", DFun (sMN 0 "APPLY") [sMN 0 "fn", sMN 0 "arg"]
227 (case mapMaybe applyCase xs of
228 [] -> DNothing
229 cases ->
230 mkBigCase (sMN 0 "APPLY") 256
231 (DV (sMN 0 "fn"))
232 (cases ++
233 [DDefaultCase DNothing])))
234 where
235 applyCase (n, t, ApplyCase x) = Just x
236 applyCase _ = Nothing
238mkApply2 :: [(Name, Int, EvalApply DAlt)] -> (Name, DDecl)
239mkApply2 xs = (sMN 0 "APPLY2", DFun (sMN 0 "APPLY2") [sMN 0 "fn", sMN 0 "arg0", sMN 0 "arg1"]
240 (case mapMaybe applyCase xs of
241 [] -> DNothing
242 cases ->
243 mkBigCase (sMN 0 "APPLY") 256
244 (DV (sMN 0 "fn"))
245 (cases ++
246 [DDefaultCase
247 (DApp False (sMN 0 "APPLY")
248 [DApp False (sMN 0 "APPLY")
249 [DV (sMN 0 "fn"),
250 DV (sMN 0 "arg0")],
251 DV (sMN 0 "arg1")])
252 ])))
253 where
254 applyCase (n, t, Apply2Case x) = Just x
255 applyCase _ = Nothing
258declare :: Int -> [(Name, Int, EvalApply DAlt)] -> [(Name, DDecl)]
259declare t xs = dec' t xs [] where
260 dec' t [] acc = reverse acc
261 dec' t ((n, ar, _) : xs) acc = dec' (t + 1) xs ((n, DConstructor n t ar) : acc)
264genArgs i = sMN i "P_c" : genArgs (i + 1)
266mkFnCon n = sMN 0 ("P_" ++ show n)
267mkUnderCon n 0 = n
268mkUnderCon n missing = sMN missing ("U_" ++ show n)
270instance Show DExp where
271 show e = show' [] e where
272 show' env (DV n) = show n
273 show' env (DApp _ e args) = show e ++ "(" ++
274 showSep ", " (map (show' env) args) ++")"
275 show' env (DLet n v e) = "let " ++ show n ++ " = " ++ show' env v ++ " in " ++
276 show' (env ++ [show n]) e
277 show' env (DUpdate n e) = "!update " ++ show n ++ "(" ++ show' env e ++ ")"
278 show' env (DC loc i n args) = atloc loc ++ "CON " ++ show n ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
279 where atloc Nothing = ""
280 atloc (Just l) = "@" ++ show (LV l) ++ ":"
281 show' env (DProj t i) = show t ++ "!" ++ show i
282 show' env (DCase up e alts) = "case" ++ update ++ show' env e ++ " of {\n\t" ++
283 showSep "\n\t| " (map (showAlt env) alts)
284 where update = case up of
285 Shared -> " "
286 Updatable -> "! "
287 show' env (DChkCase e alts) = "case' " ++ show' env e ++ " of {\n\t" ++
288 showSep "\n\t| " (map (showAlt env) alts)
289 show' env (DConst c) = show c
290 show' env (DForeign ty n args)
291 = "foreign " ++ show n ++ "(" ++ showSep ", " (map (show' env) (map snd args)) ++ ")"
292 show' env (DOp f args) = show f ++ "(" ++ showSep ", " (map (show' env) args) ++ ")"
293 show' env (DError str) = "error " ++ show str
294 show' env DNothing = "____"
296 showAlt env (DConCase _ n args e)
297 = show n ++ "(" ++ showSep ", " (map show args) ++ ") => "
298 ++ show' env e
299 showAlt env (DConstCase c e) = show c ++ " => " ++ show' env e
300 showAlt env (DDefaultCase e) = "_ => " ++ show' env e
302-- | Divide up a large case expression so that each has a maximum of
303-- 'max' branches
304mkBigCase cn max arg branches
305 | length branches <= max = DChkCase arg branches
306 | otherwise = DChkCase arg branches
308groupsOf :: Int -> [DAlt] -> [[DAlt]]
309groupsOf x [] = []
310groupsOf x xs = let (batch, rest) = span (tagLT (x + tagHead xs)) xs in
311 batch : groupsOf x rest
312 where tagHead (DConstCase (I i) _ : _) = i
313 tagHead (DConCase t _ _ _ : _) = t
314 tagHead (DDefaultCase _ : _) = -1 -- must be the end
316 tagLT i (DConstCase (I j) _) = i < j
317 tagLT i (DConCase j _ _ _) = i < j
318 tagLT i (DDefaultCase _) = False
320dumpDefuns :: DDefs -> String
321dumpDefuns ds = showSep "\n" $ map showDef (toAlist ds)
322 where showDef (x, DFun fn args exp)
323 = show fn ++ "(" ++ showSep ", " (map show args) ++ ") = \n\t" ++
324 show exp ++ "\n"
325 showDef (x, DConstructor n t a) = "Constructor " ++ show n ++ " " ++ show t