git.iko.soy/Idris-dev
on master help sign in
Fix some reachability warnings with Eff
commitb283c0d5a3b2d7794ddf8450b12b1a8cfe08b4e6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 12 Apr 2014, 10:03 (13 years ago) parent16f7da4
2 files changed+26−2
compare with master
unifiedsplit
libs/effects/Effects.idr+2−2 src/Idris/Core/CaseTree.hs+24
libs/effects/Effects.idr+2−2
@@ -93,10 +93,10 @@ updateWith [] (x :: xs) (Keep rest) = []
9393rebuildEnv : Env m ys' -> (prf : SubList ys xs) ->
9494 Env m xs -> Env m (updateWith ys' xs prf)
9595rebuildEnv [] SubNil env = env
96+rebuildEnv (x :: xs) SubNil env = x :: xs
97+rebuildEnv [] (Keep rest) (y :: env) = []
9698rebuildEnv (x :: xs) (Keep rest) (y :: env) = x :: rebuildEnv xs rest env
9799rebuildEnv xs (Drop rest) (y :: env) = y :: rebuildEnv xs rest env
98−rebuildEnv (x :: xs) SubNil [] = x :: xs
99−rebuildEnv [] (Keep x) (x :: xs) = []
100100
101101
102102-- -------------------------------------------------- [ 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
197197 nua (SucCase _ sc) = nu' sc
198198 nua (DefaultCase sc) = nu' sc
199199
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+
200216data Phase = CompileTime | RunTime
201217 deriving (Show, Eq)
202218
@@ -609,6 +625,14 @@ prune proj (Case n alts) = case alts' of
609625 -- | proj -> mkProj n 0 args (prune proj sc)
610626 -- mkProj n i xs sc = foldr (\x -> projRep x n i) sc xs
611627
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+
612636 [SucCase cn sc]
613637 | proj
614638 -> projRep cn n (-1) $ prune proj sc