@@ -4,8 +4,10 @@ module IRTS.Lang where
44
55import Control.Monad.State hiding (lift)
66import Control.Applicative hiding (Const)
7+
78import Idris.Core.TT
89import Idris.Core.CaseTree
10+
911import Data.List
1012import Debug.Trace
1113
@@ -200,98 +202,65 @@ lift env (LOp f args) = do args' <- mapM (lift env) args
200202lift env (LError str) = return $ LError str
201203lift env LNothing = return $ LNothing
202204
203−allocUnique :: LDecl -> LDecl
204−allocUnique x = x
205−
206−inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]
207−inlineAll lds = let defs = addAlist lds emptyContext in
208− map (\ (n, def) -> (n, doInline defs def)) lds
209−
210−nextN :: State Int Name
211−nextN = do i <- get
212− put (i + 1)
213− return $ sMN i "in"
214−
215−-- Inline inside a declaration. Variables are still Name at this stage.
216−-- Need to preserve uniqueness of variable names in the resulting definition,
217−-- so invent a new name for every variable we encounter
218−doInline :: LDefs -> LDecl -> LDecl
219−doInline defs d@(LConstructor _ _ _) = d
220−doInline defs (LFun opts topn args exp)
221− = let res = evalState (inlineWith [topn] (map (\n -> (n, LV (Glob n))) args) exp) 0 in
222− LFun opts topn args res
205+allocUnique :: LDefs -> (Name, LDecl) -> (Name, LDecl)
206+allocUnique defs p@(n, LConstructor _ _ _) = p
207+allocUnique defs (n, LFun opts fn args e)
208+ = let e' = evalState (findUp e) [] in
209+ (n, LFun opts fn args e')
223210 where
224− inlineWith :: [Name] -> [(Name, LExp)] -> LExp -> State Int LExp
225− inlineWith done env var@(LV (Glob n))
226− = case lookup n env of
227− Just t -> return t
228− Nothing -> return var
229− inlineWith done env (LLazyApp n es) = LLazyApp n <$> (mapM (inlineWith done env) es)
230− inlineWith done env (LForce e) = LForce <$> inlineWith done env e
231− inlineWith done env (LLazyExp e) = LLazyExp <$> inlineWith done env e
232− -- Extend the environment for Let and Lam so that bound names aren't
233− -- expanded with any top level argument definitions they shadow
234− inlineWith done env (LLet n val sc)
235− = do n' <- nextN
236− LLet n' <$> inlineWith done env val <*>
237− inlineWith done ((n, LV (Glob n')) : env) sc
238− inlineWith done env (LLam args sc)
239− = do ns' <- mapM (\n -> do n' <- nextN
240− return (n, n')) args
241− LLam (map snd ns') <$>
242− inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) sc
243− inlineWith done env (LProj exp i) = LProj <$> inlineWith done env exp <*> return i
244− inlineWith done env (LCon loc i n es)
245− = LCon loc i n <$> mapM (inlineWith done env) es
246− inlineWith done env (LCase ty e alts)
247− = LCase ty <$> inlineWith done env e <*> mapM (inlineWithAlt done env) alts
248− inlineWith done env (LOp f es) = LOp f <$> mapM (inlineWith done env) es
249− -- the interesting case!
250− inlineWith done env (LApp t (LV (Glob n)) es)
251− | n `notElem` done,
252− [LFun opts _ args body] <- lookupCtxt n defs,
253− Inline `elem` opts,
254− length es == length args
255− = do es' <- mapM (inlineWith done env) es
256− inlineWith (n : done) (zip args es' ++ env) body
257− inlineWith done env (LApp t f es)
258− = LApp t <$> inlineWith done env f <*> mapM (inlineWith done env) es
259− inlineWith done env (LForeign l t s args)
260− = LForeign l t s <$> mapM (\(t, e) -> do e' <- inlineWith done env e
261− return (t, e')) args
262− inlineWith done env t = return t
263−
264− inlineWithAlt done env (LConCase i n es rhs)
265− = do ns' <- mapM (\n -> do n' <- nextN
266− return (n, n')) es
267− LConCase i n (map snd ns') <$>
268− inlineWith done (map (\ (n,n') -> (n, LV (Glob n'))) ns' ++ env) rhs
269− inlineWithAlt done env (LConstCase c e) = LConstCase c <$> inlineWith done env e
270− inlineWithAlt done env (LDefaultCase e) = LDefaultCase <$> inlineWith done env e
271−
272−-- substLExp :: [(Name, LExp)] -> LExp -> LExp
273−-- substLExp env (LV (Glob n)) | Just t <- lookup n env = t
274−-- substLExp env (LApp t f as) = LApp t (substLExp env f) (map (substLExp env) as)
275−-- substLExp env (LLazyApp n as) = LLazyApp n (map (substLExp env) as)
276−-- substLExp env (LLazyExp e) = LLazyExp (substLExp env e)
277−-- substLExp env (LForce e) = LForce (substLExp env e)
278−-- substLExp env (LLet n v sc) = LLet n (substLExp env v)
279−-- (substLExp ((n, LV (Glob n)) : env) sc)
280−-- substLExp env (LLam args sc)
281−-- = LLam args (substLExp (map (\n -> (n, LV (Glob n))) args ++ env) sc)
282−-- substLExp env (LProj e i) = LProj (substLExp env e) i
283−-- substLExp env (LCon up i n es) = LCon up i n (map (substLExp env) es)
284−-- substLExp env (LCase ty e alts) = LCase ty (substLExp env e) (map substC alts)
285−-- where
286−-- substC (LConCase i n args e)
287−-- = LConCase i n args
288−-- (substLExp (map (\n -> (n, LV (Glob n))) args ++ env) e)
289−-- substC (LConstCase i e) = LConstCase i (substLExp env e)
290−-- substC (LDefaultCase e) = LDefaultCase (substLExp env e)
291−-- substLExp env (LForeign l t s args)
292−-- = LForeign l t s (map (\ (ty, e) -> (ty, substLExp env e)) args)
293−-- substLExp env (LOp fn es) = LOp fn (map (substLExp env) es)
294−-- substLExp env t = t
211+ -- Keep track of 'updatable' names in the state, i.e. names whose heap
212+ -- entry may be reused, along with the arity which was there
213+ findUp :: LExp -> State [(Name, Int)] LExp
214+ findUp (LApp t (LV (Glob n)) as)
215+ | Just (LConstructor _ i ar) <- lookupCtxtExact n defs,
216+ ar == length as
217+ = findUp (LCon Nothing i n as)
218+ findUp (LV (Glob n))
219+ | Just (LConstructor _ i 0) <- lookupCtxtExact n defs
220+ = findUp (LCon Nothing i n [])
221+ findUp (LApp t f as) = LApp t <$> findUp f <*> mapM findUp as
222+ findUp (LLazyApp n as) = LLazyApp n <$> mapM findUp as
223+ findUp (LLazyExp e) = LLazyExp <$> findUp e
224+ findUp (LForce e) = LForce <$> findUp e
225+ -- use assumption that names are unique!
226+ findUp (LLet n val sc) = LLet n <$> findUp val <*> findUp sc
227+ findUp (LLam ns sc) = LLam ns <$> findUp sc
228+ findUp (LProj e i) = LProj <$> findUp e <*> return i
229+ findUp (LCon (Just l) i n es) = LCon (Just l) i n <$> mapM findUp es
230+ findUp (LCon Nothing i n es)
231+ = do avail <- get
232+ v <- findVar [] avail (length es)
233+ LCon v i n <$> mapM findUp es
234+ findUp (LForeign l t s es)
235+ = LForeign l t s <$> mapM (\ (t, e) -> do e' <- findUp e
236+ return (t, e')) es
237+ findUp (LOp o es) = LOp o <$> mapM findUp es
238+ findUp (LCase Updatable e@(LV (Glob n)) as)
239+ = LCase Updatable e <$> mapM (doUpAlt n) as
240+ findUp (LCase t e as)
241+ = LCase t <$> findUp e <*> mapM findUpAlt as
242+ findUp t = return t
243+
244+ findUpAlt (LConCase i t args rhs) = do avail <- get
245+ rhs' <- findUp rhs
246+ put avail
247+ return $ LConCase i t args rhs'
248+ findUpAlt (LConstCase i rhs) = LConstCase i <$> findUp rhs
249+ findUpAlt (LDefaultCase rhs) = LDefaultCase <$> findUp rhs
250+
251+ doUpAlt n (LConCase i t args rhs)
252+ = do avail <- get
253+ put ((n, length args) : avail)
254+ rhs' <- findUp rhs
255+ put avail
256+ return $ LConCase i t args rhs'
257+ doUpAlt n (LConstCase i rhs) = LConstCase i <$> findUp rhs
258+ doUpAlt n (LDefaultCase rhs) = LDefaultCase <$> findUp rhs
259+
260+ findVar _ [] i = return Nothing
261+ findVar acc ((n, l) : ns) i | l == i = do put (reverse acc ++ ns)
262+ return (Just (Glob n))
263+ findVar acc (n : ns) i = findVar (n : acc) ns i
295264
296265
297266-- Return variables in list which are used in the expression