a272918 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Small improvements to inlining in LangOpts

This is mostly to fix evaluation of case tree and forced expressions.

commita272918ed3ca2f7322fa30b0b1590d16190dee7c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 19 Jun 2018, 16:44 (8 years ago) parent88a9f38

2 files changed+63−18

compare with master

unifiedsplit

src/IRTS/Lang.hs+25 src/IRTS/LangOpts.hs+38−18

src/IRTS/Lang.hs+25

@@ -455,3 +455,28 @@ instance Show LExp where

455455

456456 showAlt env ind (LConstCase c e) = show c ++ " => " ++ show' env ind e

457457 showAlt env ind (LDefaultCase e) = "_ => " ++ show' env ind e

458+

459+occName :: Name -> LExp -> Int

460+occName n (LV x) = if n == x then 1 else 0

461+occName n (LApp t e es) = occName n e + sum (map (occName n) es)

462+occName n (LLazyApp x es)

463+ = if n == x then 1 + sum (map (occName n) es)

464+ else sum (map (occName n) es)

465+occName n (LForce e) = occName n e

466+occName n (LLet x v sc)

467+ = if n == x then occName n v

468+ else occName n v + occName n sc

469+occName n (LLam ns sc)

470+ = if n `elem` ns then 0 else occName n sc

471+occName n (LProj e i) = occName n e

472+occName n (LCon _ _ _ es) = sum (map (occName n) es)

473+occName n (LCase t e alts) = occName n e + maximum (map occAlt alts)

474+ where

475+ occAlt (LConCase _ _ ns e)

476+ = if n `elem` ns then 0 else occName n e

477+ occAlt (LConstCase _ e) = occName n e

478+ occAlt (LDefaultCase e) = occName n e

479+occName n (LForeign _ _ es) = sum (map (occName n . snd) es)

480+occName n (LOp _ es) = sum (map (occName n) es)

481+occName n _ = 0

482+

src/IRTS/LangOpts.hs+38−18

@@ -33,16 +33,23 @@ nextN = do i <- get

3333-- uniqueness of variable names in the resulting definition, so invent

3434-- a new name for every variable we encounter

3535doInline :: LDefs -> LDecl -> LDecl

36−doInline defs d@(LConstructor _ _ _) = d

37−doInline defs (LFun opts topn args exp)

36+doInline = doInline' 1

37+

38+doInline' :: Int -> LDefs -> LDecl -> LDecl

39+doInline' 0 defs d = d

40+doInline' i defs d@(LConstructor _ _ _) = d

41+doInline' i defs (LFun opts topn args exp)

3842 = let inl = evalState (eval [] initEnv [topn] defs exp)

3943 (length args)

4044 -- do some case floating, which might arise as a result

4145 -- then, eta contract

4246 res = eta $ caseFloats 10 inl in

4347 case res of

44− LLam args' body -> LFun opts topn (map snd initNames ++ args') body

45− _ -> LFun opts topn (map snd initNames) res

48+ LLam args' body ->

49+ doInline' (i - 1) defs $

50+ LFun opts topn (map snd initNames ++ args') body

51+ _ -> doInline' (i - 1) defs $

52+ LFun opts topn (map snd initNames) res

4653 where

4754 caseFloats 0 tm = tm

4855 caseFloats n tm

@@ -72,8 +79,8 @@ eval stk env rec defs (LLazyApp n es)

7279eval stk env rec defs (LForce e)

7380 = do e' <- eval [] env rec defs e

7481 case e' of

75− LLazyExp forced -> return $ unload stk forced

76− LLazyApp n es -> return $ unload stk (LApp False (LV n) es)

82+ LLazyExp forced -> eval stk env rec defs forced

83+ LLazyApp n es -> eval stk env rec defs (LApp False (LV n) es)

7784 _ -> return (unload stk (LForce e'))

7885eval stk env rec defs (LLazyExp e)

7986 = unload stk <$> LLazyExp <$> eval [] env rec defs e

@@ -92,6 +99,7 @@ eval (world : stk) env rec defs (LApp t (LV n) [_, _, _, act, (LLam [arg] k)])

9299 = do act' <- eval [] env rec defs (LApp False act [world])

93100 argn <- nextN

94101 k' <- eval stk ((arg, LV argn) : env) rec defs (LApp False k [world])

102+ -- Needs to be a LLet to make sure the action gets evaluated

95103 return $ LLet argn act' k'

96104

97105eval stk env rec defs (LApp t f es)

@@ -106,15 +114,27 @@ eval stk env rec defs (LProj exp i)

106114eval stk env rec defs (LCon loc i n es)

107115 = unload stk <$> (LCon loc i n <$> mapM (eval [] env rec defs) es)

108116eval stk env rec defs (LCase ty e alts)

109− = do alts' <- mapM (evalAlt stk env rec defs) alts

110− e' <- eval [] env rec defs e

111− -- If they're all lambdas, bind the lambda at the top

112− let prefix = getLams (map getRHS alts')

113− case prefix of

114− [] -> return $ conOpt $ LCase ty e' (replaceInAlts e' alts')

115− args -> do alts_red <- mapM (dropArgs args) alts'

116− return $ LLam args

117− (conOpt (LCase ty e' (replaceInAlts e' alts_red)))

117+ = do e' <- eval [] env rec defs e

118+ case evalAlts e' alts of

119+ Just (env', tm) -> eval stk env' rec defs tm

120+ Nothing ->

121+ do alts' <- mapM (evalAlt stk env rec defs) alts

122+ -- If they're all lambdas, bind the lambda at the top

123+ let prefix = getLams (map getRHS alts')

124+ case prefix of

125+ [] -> return $ LCase ty e' (replaceInAlts e' alts')

126+ args -> do alts_red <- mapM (dropArgs args) alts'

127+ return $ LLam args

128+ (LCase ty e' (replaceInAlts e' alts_red))

129+ where

130+ evalAlts e' [] = Nothing

131+ evalAlts (LCon _ t n args) (LConCase i n' es rhs : as)

132+ | n == n' = Just (zip es args ++ env, rhs)

133+ evalAlts (LConst c) (LConstCase c' rhs : as)

134+ | c == c' = Just (env, rhs)

135+ evalAlts (LCon _ _ _ _) (LDefaultCase rhs : as) = Just (env, rhs)

136+ evalAlts (LConst _) (LDefaultCase rhs : as) = Just (env, rhs)

137+ evalAlts tm (_ : as) = evalAlts tm as

118138eval stk env rec defs (LOp f es)

119139 = unload stk <$> LOp f <$> mapM (eval [] env rec defs) es

120140eval stk env rec defs (LForeign t s args)

@@ -129,9 +149,9 @@ eval stk env rec defs (LLam args sc)

129149 [] -> eval stk' env' rec defs sc

130150 as -> do ns' <- mapM (\n -> do n' <- nextN

131151 return (n, n')) args'

132− unload stk' <$> LLam (map snd ns') <$>

133− eval [] (map (\ (n, n') -> (n, LV n')) ns' ++ env')

134− rec defs sc

152+ LLam (map snd ns') <$>

153+ eval stk' (map (\ (n, n') -> (n, LV n')) ns' ++ env')

154+ rec defs sc

135155eval stk env rec defs var@(LV n)

136156 = case lookup n env of

137157 Just t