    -- | Converts case matches on literals to if cascades with equality comparisons.
    module Agda.Compiler.Treeless.EliminateLiteralPatterns where

    import Data.Maybe

    import Agda.Syntax.Treeless
    import Agda.Syntax.Literal

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Primitive

    import Agda.Utils.Impossible

    eliminateLiteralPatterns :: TTerm -> TCM TTerm
    eliminateLiteralPatterns :: TTerm -> TCM TTerm
    eliminateLiteralPatterns TTerm
    t = do
      BuiltinKit
    kit <- Maybe QName -> Maybe QName -> BuiltinKit
    BuiltinKit (Maybe QName -> Maybe QName -> BuiltinKit)
    -> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName -> BuiltinKit)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> String -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    String -> m (Maybe QName)
    getBuiltinName String
    builtinNat TCMT IO (Maybe QName -> BuiltinKit)
    -> TCMT IO (Maybe QName) -> TCMT IO BuiltinKit
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> TCMT IO (Maybe QName)
    forall (m :: * -> *).
    (HasBuiltins m, MonadReduce m) =>
    String -> m (Maybe QName)
    getBuiltinName String
    builtinInteger
      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
    $ BuiltinKit -> TTerm -> TTerm
    transform BuiltinKit
    kit TTerm
    t

    data BuiltinKit = BuiltinKit
      { BuiltinKit -> Maybe QName
    nat :: Maybe QName
      , BuiltinKit -> Maybe QName
    int :: Maybe QName
      }

    transform :: BuiltinKit -> TTerm -> TTerm
    transform :: BuiltinKit -> TTerm -> TTerm
    transform BuiltinKit
    kit = TTerm -> TTerm
    tr
      where
        tr :: TTerm -> TTerm
        tr :: TTerm -> TTerm
    tr = \case
          TCase Int
    sc CaseInfo
    t TTerm
    def [TAlt]
    alts | CaseInfo -> CaseType
    caseType CaseInfo
    t CaseType -> [CaseType] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [CaseType
    CTChar, CaseType
    CTString, CaseType
    CTQName, CaseType
    CTNat, CaseType
    CTInt, CaseType
    CTFloat] ->
            (TAlt -> TTerm -> TTerm) -> TTerm -> [TAlt] -> TTerm
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TAlt -> TTerm -> TTerm
    litAlt (TTerm -> TTerm
    tr TTerm
    def) [TAlt]
    alts
            where
              litAlt :: TAlt -> TTerm -> TTerm
              litAlt :: TAlt -> TTerm -> TTerm
    litAlt (TALit Literal
    l TTerm
    body) TTerm
    cont =
                TTerm -> TTerm -> TTerm -> TTerm
    tIfThenElse
                  (TPrim -> TTerm -> TTerm -> TTerm
    tOp (Literal -> TPrim
    eqFromLit Literal
    l) (Literal -> TTerm
    TLit Literal
    l) (Int -> TTerm
    TVar Int
    sc))
                  (TTerm -> TTerm
    tr TTerm
    body)
                  TTerm
    cont
              litAlt TAlt
    _ TTerm
    _ = TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          TCase Int
    sc t :: CaseInfo
    t@CaseInfo{caseType :: CaseInfo -> CaseType
    caseType = CTData Quantity
    _ QName
    dt} TTerm
    def [TAlt]
    alts ->
            Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    sc CaseInfo
    t (TTerm -> TTerm
    tr TTerm
    def) ((TAlt -> TAlt) -> [TAlt] -> [TAlt]
    forall a b. (a -> b) -> [a] -> [b]
    map TAlt -> TAlt
    trAlt [TAlt]
    alts)
            where
              trAlt :: TAlt -> TAlt
    trAlt = \case
                TAGuard TTerm
    g TTerm
    b -> TTerm -> TTerm -> TAlt
    TAGuard (TTerm -> TTerm
    tr TTerm
    g) (TTerm -> TTerm
    tr TTerm
    b)
                TACon QName
    q Int
    a TTerm
    b -> QName -> Int -> TTerm -> TAlt
    TACon QName
    q Int
    a (TTerm -> TTerm
    tr TTerm
    b)
                TALit Literal
    l TTerm
    b   -> Literal -> TTerm -> TAlt
    TALit Literal
    l (TTerm -> TTerm
    tr TTerm
    b)
          TCase Int
    _ CaseInfo
    _ TTerm
    _ [TAlt]
    _ -> TTerm
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          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)

        -- TODO:: Defined but not used
        isCaseOn :: CaseType -> [BuiltinKit -> Maybe QName] -> Bool
    isCaseOn (CTData Quantity
    _ QName
    dt) [BuiltinKit -> Maybe QName]
    xs = QName
    dt QName -> [QName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ((BuiltinKit -> Maybe QName) -> Maybe QName)
    -> [BuiltinKit -> Maybe QName] -> [QName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe ((BuiltinKit -> Maybe QName) -> BuiltinKit -> Maybe QName
    forall a b. (a -> b) -> a -> b
    $ BuiltinKit
    kit) [BuiltinKit -> Maybe QName]
    xs
        isCaseOn CaseType
    _ [BuiltinKit -> Maybe QName]
    _ = Bool
    False

        eqFromLit :: Literal -> TPrim
        eqFromLit :: Literal -> TPrim
    eqFromLit = \case
          LitNat Integer
    _     -> TPrim
    PEqI
          LitFloat Double
    _   -> TPrim
    PEqF
          LitString Text
    _  -> TPrim
    PEqS
          LitChar Char
    _    -> TPrim
    PEqC
          LitQName QName
    _   -> TPrim
    PEqQ
          Literal
    _ -> TPrim
    forall a. HasCallStack => a
    __IMPOSSIBLE__