    module Agda.Compiler.Treeless.Uncase (caseToSeq) where

    import Agda.Syntax.Treeless
    import Agda.TypeChecking.Substitute
    import Agda.Compiler.Treeless.Subst
    import Agda.Compiler.Treeless.Compare

    import Agda.Utils.List

    import Agda.Utils.Impossible

    caseToSeq :: Monad m => TTerm -> m TTerm
    caseToSeq :: forall (m :: * -> *). Monad m => TTerm -> m TTerm
    caseToSeq TTerm
    t = TTerm -> m TTerm
    forall (m :: * -> *) a. Monad m => a -> m a
    return (TTerm -> m TTerm) -> TTerm -> m TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    uncase TTerm
    t

    uncase :: TTerm -> TTerm
    uncase :: TTerm -> TTerm
    uncase TTerm
    t = case TTerm
    t of
      TVar{}    -> TTerm
    t
      TPrim{}   -> TTerm
    t
      TDef{}    -> TTerm
    t
      TApp TTerm
    f Args
    es -> TTerm -> Args -> TTerm
    tApp (TTerm -> TTerm
    uncase TTerm
    f) ((TTerm -> TTerm) -> Args -> Args
    forall a b. (a -> b) -> [a] -> [b]
    map TTerm -> TTerm
    uncase Args
    es)
      TLam TTerm
    b    -> TTerm -> TTerm
    TLam (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    uncase TTerm
    b
      TLit{}    -> TTerm
    t
      TCon{}    -> TTerm
    t
      TLet TTerm
    e TTerm
    b  -> TTerm -> TTerm -> TTerm
    tLet (TTerm -> TTerm
    uncase TTerm
    e) (TTerm -> TTerm
    uncase TTerm
    b)
      TCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    doCase Int
    x CaseInfo
    t (TTerm -> TTerm
    uncase TTerm
    d) ((TAlt -> TAlt) -> [TAlt] -> [TAlt]
    forall a b. (a -> b) -> [a] -> [b]
    map TAlt -> TAlt
    uncaseAlt [TAlt]
    bs)
      TUnit{}   -> TTerm
    t
      TSort{}   -> TTerm
    t
      TErased{} -> TTerm
    t
      TError{}  -> TTerm
    t
      TCoerce TTerm
    t -> TTerm -> TTerm
    TCoerce (TTerm -> TTerm
    uncase TTerm
    t)
      where
        uncaseAlt :: TAlt -> TAlt
    uncaseAlt (TACon QName
    c Int
    a TTerm
    b) = QName -> Int -> TTerm -> TAlt
    TACon QName
    c Int
    a (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    uncase TTerm
    b
        uncaseAlt (TALit Literal
    l TTerm
    b)   = Literal -> TTerm -> TAlt
    TALit Literal
    l (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    uncase TTerm
    b
        uncaseAlt (TAGuard TTerm
    g TTerm
    b) = TTerm -> TTerm -> TAlt
    TAGuard (TTerm -> TTerm
    uncase TTerm
    g) (TTerm -> TTerm
    uncase TTerm
    b)

        doCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    doCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs
          | Just TTerm
    u <- Maybe TTerm
    mu,
            (TAlt -> Bool) -> [TAlt] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Int -> TTerm -> TAlt -> Bool
    equalTo Int
    x TTerm
    u) [TAlt]
    bs = TTerm -> TTerm
    maybeSeq TTerm
    u
          | Bool
    otherwise            = TTerm
    fallback
          where
            maybeSeq :: TTerm -> TTerm
    maybeSeq TTerm
    u | CaseInfo -> Bool
    caseLazy CaseInfo
    t = TTerm
    u
                       | Bool
    otherwise  = TTerm -> Args -> TTerm
    tApp (TPrim -> TTerm
    TPrim TPrim
    PSeq) [Int -> TTerm
    TVar Int
    x, TTerm
    u]
            fallback :: TTerm
    fallback = Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    x CaseInfo
    t TTerm
    d [TAlt]
    bs
            (Int
    fv, Maybe TTerm
    mu)
              | TTerm -> Bool
    forall a. Unreachable a => a -> Bool
    isUnreachable TTerm
    d =
                case TAlt -> [TAlt] -> TAlt
    forall a. a -> [a] -> a
    lastWithDefault TAlt
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [TAlt]
    bs of
                  TACon QName
    _ Int
    a TTerm
    b -> (Int
    a, Int -> TTerm -> Maybe TTerm
    forall a. (HasFree a, Subst a) => Int -> a -> Maybe a
    tryStrengthen Int
    a TTerm
    b)
                  TALit Literal
    l TTerm
    b   -> (Int
    0, TTerm -> Maybe TTerm
    forall a. a -> Maybe a
    Just TTerm
    b)
                  TAGuard TTerm
    _ TTerm
    b -> (Int
    0, TTerm -> Maybe TTerm
    forall a. a -> Maybe a
    Just TTerm
    b)
              | Bool
    otherwise = (Int
    0, TTerm -> Maybe TTerm
    forall a. a -> Maybe a
    Just TTerm
    d)

        equalTo :: Int -> TTerm -> TAlt -> Bool
        equalTo :: Int -> TTerm -> TAlt -> Bool
    equalTo Int
    x TTerm
    t (TACon QName
    c Int
    a TTerm
    b)
          | Just TTerm
    b' <- Int -> TTerm -> Maybe TTerm
    forall a. (HasFree a, Subst a) => Int -> a -> Maybe a
    tryStrengthen Int
    a TTerm
    b = TTerm -> TTerm -> Bool
    equalTerms (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    x TTerm
    SubstArg TTerm
    v TTerm
    t) (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    x TTerm
    SubstArg TTerm
    v TTerm
    b')
          | Bool
    otherwise                    = Bool
    False
          where v :: TTerm
    v = TTerm -> Args -> TTerm
    mkTApp (QName -> TTerm
    TCon QName
    c) (Int -> TTerm -> Args
    forall a. Int -> a -> [a]
    replicate Int
    a TTerm
    TErased)
        equalTo Int
    x TTerm
    t (TALit Literal
    l TTerm
    b)   = TTerm -> TTerm -> Bool
    equalTerms (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    x (Literal -> TTerm
    TLit Literal
    l) TTerm
    t) (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    subst Int
    x (Literal -> TTerm
    TLit Literal
    l) TTerm
    b)
        equalTo Int
    x TTerm
    t (TAGuard TTerm
    _ TTerm
    b) = TTerm -> TTerm -> Bool
    equalTerms TTerm
    t TTerm
    b

        tLet :: TTerm -> TTerm -> TTerm
    tLet TTerm
    e TTerm
    b =
          case Int -> TTerm -> Occurs
    forall a. HasFree a => Int -> a -> Occurs
    occursIn Int
    0 TTerm
    b of
            Occurs Int
    0 UnderLambda
    _ SeqArg
    _ -> Impossible -> TTerm -> TTerm
    forall a. Subst a => Impossible -> a -> a
    strengthen Impossible
    HasCallStack => Impossible
    impossible TTerm
    b
            Occurs
    _            -> TTerm -> TTerm -> TTerm
    TLet TTerm
    e TTerm
    b

        -- Primitive operations are already strict
        tApp :: TTerm -> Args -> TTerm
    tApp (TPrim TPrim
    PSeq) [TTerm
    _, b :: TTerm
    b@(TApp (TPrim TPrim
    op) Args
    _)]
          | TPrim
    op TPrim -> [TPrim] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [TPrim
    PAdd, TPrim
    PSub, TPrim
    PMul, TPrim
    PLt, TPrim
    PGeq, TPrim
    PRem, TPrim
    PQuot] Bool -> Bool -> Bool
    || TPrim -> Bool
    isPrimEq TPrim
    op = TTerm
    b
        tApp TTerm
    f Args
    es = TTerm -> Args -> TTerm
    TApp TTerm
    f Args
    es