    -- | Eliminates case defaults by adding an alternative for all possible
    -- constructors. Literal cases are preserved as-is.
    module Agda.Compiler.Treeless.EliminateDefaults where

    import Control.Monad
    import qualified Data.List as List

    import Agda.Syntax.Treeless

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Substitute

    import Agda.Compiler.Treeless.Subst () --instance only

    eliminateCaseDefaults :: TTerm -> TCM TTerm
    eliminateCaseDefaults :: TTerm -> TCM TTerm
    eliminateCaseDefaults = TTerm -> TCM TTerm
    tr
      where
        tr :: TTerm -> TCM TTerm
        tr :: TTerm -> TCM TTerm
    tr = \case
          TCase Int
    sc ct :: CaseInfo
    ct@CaseInfo{caseType :: CaseInfo -> CaseType
    caseType = CTData Quantity
    _ QName
    qn} TTerm
    def [TAlt]
    alts
            | Bool -> Bool
    not (TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    isUnreachable TTerm
    def) -> do
            [QName]
    dtCons <- Defn -> [QName]
    defConstructors (Defn -> [QName]) -> (Definition -> Defn) -> Definition -> [QName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Definition -> Defn
    theDef (Definition -> [QName]) -> TCMT IO Definition -> TCMT IO [QName]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    qn
            let missingCons :: [QName]
    missingCons = [QName]
    dtCons [QName] -> [QName] -> [QName]
    forall a. Eq a => [a] -> [a] -> [a]
    List.\\ (TAlt -> QName) -> [TAlt] -> [QName]
    forall a b. (a -> b) -> [a] -> [b]
    map TAlt -> QName
    aCon [TAlt]
    alts
            TTerm
    def <- TTerm -> TCM TTerm
    tr TTerm
    def
            [TAlt]
    newAlts <- [QName] -> (QName -> TCMT IO TAlt) -> TCMT IO [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [QName]
    missingCons ((QName -> TCMT IO TAlt) -> TCMT IO [TAlt])
    -> (QName -> TCMT IO TAlt) -> TCMT IO [TAlt]
    forall a b. (a -> b) -> a -> b
    $ \QName
    con -> do
              Constructor {conArity :: Defn -> Int
    conArity = Int
    ar} <- Definition -> Defn
    theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    con
              TAlt -> TCMT IO TAlt
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TAlt -> TCMT IO TAlt) -> TAlt -> TCMT IO TAlt
    forall a b. (a -> b) -> a -> b
    $ QName -> Int -> TTerm -> TAlt
    TACon QName
    con Int
    ar (Int -> TTerm
    TVar Int
    ar)

            [TAlt]
    alts' <- ([TAlt] -> [TAlt] -> [TAlt]
    forall a. [a] -> [a] -> [a]
    ++ [TAlt]
    newAlts) ([TAlt] -> [TAlt]) -> TCMT IO [TAlt] -> TCMT IO [TAlt]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TAlt -> TCMT IO TAlt) -> [TAlt] -> TCMT IO [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (TAlt -> TCMT IO TAlt
    trAlt (TAlt -> TCMT IO TAlt) -> (TAlt -> TAlt) -> TAlt -> TCMT IO TAlt
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> TAlt -> TAlt
    forall a. Subst a => Int -> a -> a
    raise Int
    1) [TAlt]
    alts

            TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> TCM TTerm) -> TTerm -> TCM TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm
    TLet TTerm
    def (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase (Int
    sc Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) CaseInfo
    ct TTerm
    tUnreachable [TAlt]
    alts'
          TCase Int
    sc CaseInfo
    ct TTerm
    def [TAlt]
    alts -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    sc CaseInfo
    ct (TTerm -> [TAlt] -> TTerm)
    -> TCM TTerm -> TCMT IO ([TAlt] -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    def TCMT IO ([TAlt] -> TTerm) -> TCMT IO [TAlt] -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TAlt -> TCMT IO TAlt) -> [TAlt] -> TCMT IO [TAlt]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TAlt -> TCMT IO TAlt
    trAlt [TAlt]
    alts

          t :: TTerm
    t@TVar{}    -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TDef{}    -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TCon{}    -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TPrim{}   -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TLit{}    -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TUnit{}   -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TSort{}   -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TErased{} -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t
          t :: TTerm
    t@TError{}  -> TTerm -> TCM TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return TTerm
    t

          TCoerce TTerm
    a               -> TTerm -> TTerm
    TCoerce (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    a
          TLam TTerm
    b                  -> TTerm -> TTerm
    TLam (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    b
          TApp TTerm
    a Args
    bs               -> TTerm -> Args -> TTerm
    TApp (TTerm -> Args -> TTerm) -> TCM TTerm -> TCMT IO (Args -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    a TCMT IO (Args -> TTerm) -> TCMT IO Args -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> TCM TTerm) -> Args -> TCMT IO Args
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TTerm -> TCM TTerm
    tr Args
    bs
          TLet TTerm
    e TTerm
    b                -> TTerm -> TTerm -> TTerm
    TLet (TTerm -> TTerm -> TTerm) -> TCM TTerm -> TCMT IO (TTerm -> TTerm)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    e TCMT IO (TTerm -> TTerm) -> TCM TTerm -> TCM TTerm
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> TCM TTerm
    tr TTerm
    b

        trAlt :: TAlt -> TCM TAlt
        trAlt :: TAlt -> TCMT IO TAlt
    trAlt = \case
          TAGuard TTerm
    g TTerm
    b -> TTerm -> TTerm -> TAlt
    TAGuard (TTerm -> TTerm -> TAlt) -> TCM TTerm -> TCMT IO (TTerm -> TAlt)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    g TCMT IO (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> TTerm -> TCM TTerm
    tr TTerm
    b
          TACon QName
    q Int
    a TTerm
    b -> QName -> Int -> TTerm -> TAlt
    TACon QName
    q Int
    a (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    b
          TALit Literal
    l TTerm
    b   -> Literal -> TTerm -> TAlt
    TALit Literal
    l (TTerm -> TAlt) -> TCM TTerm -> TCMT IO TAlt
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM TTerm
    tr TTerm
    b