git.iko.soy/Idris-dev
on master help sign in
Fix some reachability warnings with Eff
b283c0dEdwin Brady
libs/effects/Effects.idr+2−2
compare with master
unifiedsplit
@@ -93,10 +93,10 @@ updateWith [] (x :: xs) (Keep rest) = []
93rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
93rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
94 Env m xs -> Env m (updateWith ys' xs prf)
94 Env m xs -> Env m (updateWith ys' xs prf)
95rebuildEnv [] SubNil env = env
95rebuildEnv [] SubNil env = env
96+rebuildEnv (x :: xs) SubNil env = x :: xs
97+rebuildEnv [] (Keep rest) (y :: env) = []
96rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
98rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
97rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
99rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
98−rebuildEnv (x :: xs) SubNil [] = x :: xs
99−rebuildEnv [] (Keep x) (x :: xs) = []
100
100
101
101
102-- -------------------------------------------------- [ The Effect EDSL itself ]
102-- -------------------------------------------------- [ The Effect EDSL itself ]
src/Idris/Core/CaseTree.hs+24
@@ -197,6 +197,22 @@ findAllUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nu' sc) where
197 nua (SucCase _ sc) = nu' sc
197 nua (SucCase _ sc) = nu' sc
198 nua (DefaultCase sc) = nu' sc
198 nua (DefaultCase sc) = nu' sc
199
199
200+-- Return whether name is used anywhere in a case tree
201+isUsed :: SC -> Name -> Bool
202+isUsed sc n = used sc where
203+
204+ used (Case n' alts) = n == n' || or (map usedA alts)
205+ used (ProjCase t alts) = n `elem` freeNames t || or (map usedA alts)
206+ used (STerm t) = n `elem` freeNames t
207+ used _ = False
208+
209+ usedA (ConCase _ _ args sc) = used sc
210+ usedA (FnCase _ args sc) = used sc
211+ usedA (ConstCase _ sc) = used sc
212+ usedA (SucCase _ sc) = used sc
213+ usedA (DefaultCase sc) = used sc
214+
215+
200data Phase = CompileTime | RunTime
216data Phase = CompileTime | RunTime
201 deriving (Show, Eq)
217 deriving (Show, Eq)
202
218
@@ -609,6 +625,14 @@ prune proj (Case n alts) = case alts' of
609 -- | proj -> mkProj n 0 args (prune proj sc)
625 -- | proj -> mkProj n 0 args (prune proj sc)
610 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
626 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
611
627
628+ -- If none of the args are used in the sc, however, we can just replace it
629+ -- with sc
630+ as@[ConCase cn i args sc]
631+ | proj -> let sc' = prune proj sc in
632+ if any (isUsed sc') args
633+ then Case n [ConCase cn i args sc']
634+ else sc'
635+
612 [SucCase cn sc]
636 [SucCase cn sc]
613 | proj
637 | proj
614 -> projRep cn n (-1) $ prune proj sc
638 -> projRep cn n (-1) $ prune proj sc