    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Translates guard alternatives to if-then-else cascades.
    --
    -- The builtin translation must be run before this transformation.
    module Agda.Compiler.Treeless.GuardsToPrims ( convertGuards ) where

    import qualified Data.List as List

    import Agda.Syntax.Treeless

    import Agda.Utils.Impossible

    convertGuards :: TTerm -> TTerm
    convertGuards :: TTerm -> TTerm
    convertGuards = TTerm -> TTerm
    tr
      where
        tr :: TTerm -> TTerm
    tr = \case
          TCase Int
    sc CaseInfo
    t TTerm
    def [TAlt]
    alts ->
            if [TAlt] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [TAlt]
    otherAlts
              then
                TTerm
    def'
              else
                Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    sc CaseInfo
    t TTerm
    def' ((TAlt -> TAlt) -> [TAlt] -> [TAlt]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap TAlt -> TAlt
    trAlt [TAlt]
    otherAlts)
            where
              ([TAlt]
    plusAlts, [TAlt]
    otherAlts) = [TAlt] -> ([TAlt], [TAlt])
    splitAlts [TAlt]
    alts

              guardedAlt :: TAlt -> TTerm -> TTerm
              guardedAlt :: TAlt -> TTerm -> TTerm
    guardedAlt (TAGuard TTerm
    g TTerm
    body) TTerm
    cont = TTerm -> TTerm -> TTerm -> TTerm
    tIfThenElse (TTerm -> TTerm
    tr TTerm
    g) (TTerm -> TTerm
    tr TTerm
    body) (TTerm -> TTerm
    tr TTerm
    cont)
              guardedAlt TAlt
    _ TTerm
    _ = TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__

              def' :: TTerm
    def' = (TAlt -> TTerm -> TTerm) -> TTerm -> [TAlt] -> TTerm
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TAlt -> TTerm -> TTerm
    guardedAlt (TTerm -> TTerm
    tr TTerm
    def) [TAlt]
    plusAlts

              trAlt :: TAlt -> TAlt
    trAlt (TAGuard{}) = TAlt
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              trAlt TAlt
    a = TAlt
    a { aBody = tr (aBody a) }

          t :: TTerm
    t@TVar{}    -> TTerm
    t
          t :: TTerm
    t@TDef{}    -> TTerm
    t
          t :: TTerm
    t@TCon{}    -> TTerm
    t
          t :: TTerm
    t@TPrim{}   -> TTerm
    t
          t :: TTerm
    t@TLit{}    -> TTerm
    t
          t :: TTerm
    t@TUnit{}   -> TTerm
    t
          t :: TTerm
    t@TSort{}   -> TTerm
    t
          t :: TTerm
    t@TErased{} -> TTerm
    t
          t :: TTerm
    t@TError{}  -> TTerm
    t

          TCoerce TTerm
    a               -> TTerm -> TTerm
    TCoerce (TTerm -> TTerm
    tr TTerm
    a)
          TLam TTerm
    b                  -> TTerm -> TTerm
    TLam (TTerm -> TTerm
    tr TTerm
    b)
          TApp TTerm
    a Args
    bs               -> TTerm -> Args -> TTerm
    TApp (TTerm -> TTerm
    tr TTerm
    a) ((TTerm -> TTerm) -> Args -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map TTerm -> TTerm
    tr Args
    bs)
          TLet TTerm
    e TTerm
    b                -> TTerm -> TTerm -> TTerm
    TLet (TTerm -> TTerm
    tr TTerm
    e) (TTerm -> TTerm
    tr TTerm
    b)

    -- | Split alts into TAGuard alts and other alts.
    splitAlts :: [TAlt] -> ([TAlt], [TAlt])
    splitAlts :: [TAlt] -> ([TAlt], [TAlt])
    splitAlts = (TAlt -> Bool) -> [TAlt] -> ([TAlt], [TAlt])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition TAlt -> Bool
    isGuardAlt
      where isGuardAlt :: TAlt -> Bool
    isGuardAlt (TAGuard TTerm
    _ TTerm
    _) = Bool
    True
            isGuardAlt TAlt
    _ = Bool
    False