@@ -395,21 +395,44 @@ instance ToIR SC where
395 alt' <- mkIRAlt tm' alt
395 alt' <- mkIRAlt tm' alt
396 return $ LCase tm' [alt']
396 return $ LCase tm' [alt']
398+ -- There are two transformations in this case:
400+ -- 1. Newtype-case elimination:
402+ -- wrap({e1}) -> P({e1}) ==> P({e0})
404+ -- This is important because newtyped constructors are compiled away entirely
405+ -- and we need to do that everywhere.
407+ -- 2. Unused-case elimination:
409+ -- C(x,y) -> P[... x,y not used ...] ==> P
398 -- This is important for runtime because sometimes we case on irrelevant data:
411 -- This is important for runtime because sometimes we case on irrelevant data:
401− -- SingleConstructor x y => ... x, y never used ...
403− -- In the example above, {foo} will most probably have been erased
413+ -- In the example above, {e0} will most probably have been erased
404− -- so this vain projection would make the resulting program segfault.
414+ -- so this vain projection would make the resulting program segfault
415+ -- because the code generator still emits a PROJECT(...) STG instruction.
406 -- Hence, we check whether the variables are used at all
417 -- Hence, we check whether the variables are used at all
407 -- and erase the casesplit if they are not.
418 -- and erase the casesplit if they are not.
408 ir' (Case n [alt]) = do
419 ir' (Case n [alt]) = do
420+ replacement <- case alt of
421+ ConCase cn a ns sc -> do
422+ detag <- maybe False detaggable . lookupCtxtExact cn . idris_optimisation <$> getIState
423+ used <- maybe [] (map fst . usedpos) . lookupCtxtExact cn . idris_callgraph <$> getIState
424+ if detag && length used == 1
425+ then return . Just $ substSC (ns !! head used) n sc
409− alt' <- mkIRAlt (LV (Glob n)) alt
432+ alt' <- mkIRAlt (LV (Glob n)) alt
410− return $ case namesBoundIn alt' `usedIn` subexpr alt' of
433+ return $ case namesBoundIn alt' `usedIn` subexpr alt' of
411− [] -> subexpr alt' -- strip the unused top-most case
434+ [] -> subexpr alt' -- strip the unused top-most case
412− _ -> LCase (LV (Glob n)) [alt']
435+ _ -> LCase (LV (Glob n)) [alt']
414 namesBoundIn :: LAlt -> [Name]
437 namesBoundIn :: LAlt -> [Name]
415 namesBoundIn (LConCase cn i ns sc) = ns
438 namesBoundIn (LConCase cn i ns sc) = ns
@@ -421,6 +444,22 @@ instance ToIR SC where
421 subexpr (LConstCase _ e) = e
444 subexpr (LConstCase _ e) = e
422 subexpr (LDefaultCase e) = e
445 subexpr (LDefaultCase e) = e
447+ substSC :: Name -> Name -> SC -> SC
448+ substSC n repl (Case n' alts)
449+ | n == n' = Case repl (map (substAlt n repl) alts)
450+ | otherwise = Case n' (map (substAlt n repl) alts)
451+ substSC n repl (STerm t) = STerm $ subst n (P Bound repl Erased) t
452+ substSC n repl sc = error $ "unsupported in substSC: " ++ show sc
454+ substAlt :: Name -> Name -> CaseAlt -> CaseAlt
455+ substAlt n repl (ConCase cn a ns sc) = ConCase cn a ns (substSC n repl sc)
456+ substAlt n repl (FnCase fn ns sc) = FnCase fn ns (substSC n repl sc)
457+ substAlt n repl (ConstCase c sc) = ConstCase c (substSC n repl sc)
458+ substAlt n repl (SucCase n' sc)
459+ | n == n' = SucCase n (substSC n repl sc)
460+ | otherwise = SucCase n' (substSC n repl sc)
461+ substAlt n repl (DefaultCase sc) = DefaultCase (substSC n repl sc)
424 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
463 ir' (Case n alts) = do alts' <- mapM (mkIRAlt (LV (Glob n))) alts
425 return $ LCase (LV (Glob n)) alts'
464 return $ LCase (LV (Glob n)) alts'
426 ir' ImpossibleCase = return LNothing
465 ir' ImpossibleCase = return LNothing