    -- | Translates the Agda builtin nat datatype to arbitrary-precision integers.
    --
    -- Philipp, 20150921:
    -- At the moment, this optimization is the reason that there is a
    -- TAPlus alternative. For Haskell, this can easily be translated to guards. However, in
    -- the long term it would be easier for the backends if these things were translated
    -- directly to a less-than primitive and if-then-else expressions or similar. This would
    -- require us to add some internal Bool-datatype as compiler-internal type and
    -- a primitive less-than function, which will be much easier once Treeless
    -- is used for whole modules.
    --
    -- Ulf, 2015-09-21: No, actually we need the n+k patterns, or at least guards.
    -- Representing them with if-then-else would make it a lot harder to do
    -- optimisations that analyse case tree, like impossible case elimination.
    --
    -- Ulf, 2015-10-30: Guards are actually a better primitive. Fixed that.
    module Agda.Compiler.Treeless.Builtin (translateBuiltins) where

    import qualified Agda.Syntax.Internal as I
    import Agda.Syntax.Position
    import Agda.Syntax.Treeless
    import Agda.Syntax.Literal

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

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

    data BuiltinKit = BuiltinKit
      { BuiltinKit -> QName -> Bool
    isZero   :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isSuc    :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isPos    :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isNegSuc :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isPlus   :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isTimes  :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isLess   :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isEqual  :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isForce  :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isWord64FromNat :: QName -> Bool
      , BuiltinKit -> QName -> Bool
    isWord64ToNat   :: QName -> Bool
      }

    builtinKit :: TCM BuiltinKit
    builtinKit :: TCM BuiltinKit
    builtinKit =
      (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> (QName -> Bool)
    -> BuiltinKit
    BuiltinKit ((QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> (QName -> Bool)
     -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    con String
    builtinZero
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    con String
    builtinSuc
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    con String
    builtinIntegerPos
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    con String
    builtinIntegerNegSuc
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    def String
    builtinNatPlus
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    def String
    builtinNatTimes
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> (QName -> Bool)
          -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    def String
    builtinNatLess
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> (QName -> Bool)
       -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT
         IO
         ((QName -> Bool)
          -> (QName -> Bool) -> (QName -> Bool) -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe QName
    def String
    builtinNatEquals
                 TCMT
      IO
      ((QName -> Bool)
       -> (QName -> Bool) -> (QName -> Bool) -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT IO ((QName -> Bool) -> (QName -> Bool) -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (PrimFun -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (PrimFun -> Maybe b) -> String -> f (b -> Bool)
    isP PrimFun -> Maybe QName
    pf  String
    "primForce"
                 TCMT IO ((QName -> Bool) -> (QName -> Bool) -> BuiltinKit)
    -> TCMT IO (QName -> Bool)
    -> TCMT IO ((QName -> Bool) -> BuiltinKit)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (PrimFun -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (PrimFun -> Maybe b) -> String -> f (b -> Bool)
    isP PrimFun -> Maybe QName
    pf  String
    "primWord64FromNat"
                 TCMT IO ((QName -> Bool) -> BuiltinKit)
    -> TCMT IO (QName -> Bool) -> TCM BuiltinKit
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (PrimFun -> Maybe QName) -> String -> TCMT IO (QName -> Bool)
    forall {f :: * -> *} {b}.
    (Eq b, HasBuiltins f) =>
    (PrimFun -> Maybe b) -> String -> f (b -> Bool)
    isP PrimFun -> Maybe QName
    pf  String
    "primWord64ToNat"
      where
        con :: Term -> Maybe QName
    con (I.Con ConHead
    c ConInfo
    _ Elims
    _) = QName -> Maybe QName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (QName -> Maybe QName) -> QName -> Maybe QName
    forall a b. (a -> b) -> a -> b
    $ ConHead -> QName
    I.conName ConHead
    c
        con Term
    _           = Maybe QName
    forall a. Maybe a
    Nothing
        def :: Term -> Maybe QName
    def (I.Def QName
    d Elims
    _) = QName -> Maybe QName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure QName
    d
        def Term
    _           = Maybe QName
    forall a. Maybe a
    Nothing

        pf :: PrimFun -> Maybe QName
    pf = QName -> Maybe QName
    forall a. a -> Maybe a
    Just (QName -> Maybe QName)
    -> (PrimFun -> QName) -> PrimFun -> Maybe QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimFun -> QName
    primFunName

        is :: (a -> Maybe b) -> f (Maybe a) -> f (b -> Bool)
    is  a -> Maybe b
    a f (Maybe a)
    b = (b -> Bool) -> (b -> b -> Bool) -> Maybe b -> b -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe (Bool -> b -> Bool
    forall a b. a -> b -> a
    const Bool
    False) b -> b -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Maybe b -> b -> Bool)
    -> (Maybe a -> Maybe b) -> Maybe a -> b -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> Maybe b
    a (a -> Maybe b) -> Maybe a -> Maybe b
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<) (Maybe a -> b -> Bool) -> f (Maybe a) -> f (b -> Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> f (Maybe a)
    b
        isB :: (Term -> Maybe b) -> String -> f (b -> Bool)
    isB Term -> Maybe b
    a String
    b = (Term -> Maybe b) -> f (Maybe Term) -> f (b -> Bool)
    forall {f :: * -> *} {b} {a}.
    (Functor f, Eq b) =>
    (a -> Maybe b) -> f (Maybe a) -> f (b -> Bool)
    is Term -> Maybe b
    a (String -> f (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
    getBuiltin' String
    b)
        isP :: (PrimFun -> Maybe b) -> String -> f (b -> Bool)
    isP PrimFun -> Maybe b
    a String
    p = (PrimFun -> Maybe b) -> f (Maybe PrimFun) -> f (b -> Bool)
    forall {f :: * -> *} {b} {a}.
    (Functor f, Eq b) =>
    (a -> Maybe b) -> f (Maybe a) -> f (b -> Bool)
    is PrimFun -> Maybe b
    a (String -> f (Maybe PrimFun)
    forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
    getPrimitive' String
    p)

    translateBuiltins :: TTerm -> TCM TTerm
    translateBuiltins :: TTerm -> TCM TTerm
    translateBuiltins TTerm
    t = do
      BuiltinKit
    kit <- TCM BuiltinKit
    builtinKit
      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

    transform :: BuiltinKit -> TTerm -> TTerm
    transform :: BuiltinKit -> TTerm -> TTerm
    transform BuiltinKit{QName -> Bool
    isWord64ToNat :: QName -> Bool
    isWord64FromNat :: QName -> Bool
    isForce :: QName -> Bool
    isEqual :: QName -> Bool
    isLess :: QName -> Bool
    isTimes :: QName -> Bool
    isPlus :: QName -> Bool
    isNegSuc :: QName -> Bool
    isPos :: QName -> Bool
    isSuc :: QName -> Bool
    isZero :: QName -> Bool
    isWord64ToNat :: BuiltinKit -> QName -> Bool
    isWord64FromNat :: BuiltinKit -> QName -> Bool
    isForce :: BuiltinKit -> QName -> Bool
    isEqual :: BuiltinKit -> QName -> Bool
    isLess :: BuiltinKit -> QName -> Bool
    isTimes :: BuiltinKit -> QName -> Bool
    isPlus :: BuiltinKit -> QName -> Bool
    isNegSuc :: BuiltinKit -> QName -> Bool
    isPos :: BuiltinKit -> QName -> Bool
    isSuc :: BuiltinKit -> QName -> Bool
    isZero :: BuiltinKit -> QName -> Bool
    ..} = TTerm -> TTerm
    tr
      where
        tr :: TTerm -> TTerm
    tr = \case

          TCon QName
    c | QName -> Bool
    isZero QName
    c   -> Integer -> TTerm
    tInt Integer
    0
                 | QName -> Bool
    isSuc QName
    c    -> TTerm -> TTerm
    TLam (Integer -> TTerm -> TTerm
    tPlusK Integer
    1 (Int -> TTerm
    TVar Int
    0))
                 | QName -> Bool
    isPos QName
    c    -> TTerm -> TTerm
    TLam (Int -> TTerm
    TVar Int
    0)
                 | QName -> Bool
    isNegSuc QName
    c -> TTerm -> TTerm
    TLam (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Integer -> TTerm -> TTerm
    tNegPlusK Integer
    1 (Int -> TTerm
    TVar Int
    0)

          TDef QName
    f | QName -> Bool
    isPlus QName
    f   -> TPrim -> TTerm
    TPrim TPrim
    PAdd
                 | QName -> Bool
    isTimes QName
    f  -> TPrim -> TTerm
    TPrim TPrim
    PMul
                 | QName -> Bool
    isLess QName
    f   -> TPrim -> TTerm
    TPrim TPrim
    PLt
                 | QName -> Bool
    isEqual QName
    f  -> TPrim -> TTerm
    TPrim TPrim
    PEqI
                 | QName -> Bool
    isWord64ToNat QName
    f   -> TPrim -> TTerm
    TPrim TPrim
    P64ToI
                 | QName -> Bool
    isWord64FromNat QName
    f -> TPrim -> TTerm
    TPrim TPrim
    PITo64
            -- Note: Don't do this for builtinNatMinus! PSub is integer minus and
            --       builtin minus is monus. The simplifier will do it if it can see
            --       that it won't underflow.

          TApp (TDef QName
    q) (TTerm
    _ : TTerm
    _ : TTerm
    _ : TTerm
    _ : TTerm
    e : TTerm
    f : [TTerm]
    es)
            | QName -> Bool
    isForce QName
    q -> TTerm -> TTerm
    tr (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm
    TLet TTerm
    e (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> [TTerm] -> TTerm
    mkTApp (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PSeq (Int -> TTerm
    TVar Int
    0) (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> [TTerm] -> TTerm
    mkTApp (Int -> TTerm -> TTerm
    forall a. Subst a => Int -> a -> a
    raise Int
    1 TTerm
    f) [Int -> TTerm
    TVar Int
    0]) [TTerm]
    es

          TApp (TCon QName
    s) [TTerm
    e] | QName -> Bool
    isSuc QName
    s ->
            case TTerm -> TTerm
    tr TTerm
    e of
              TLit (LitNat Integer
    n) -> Integer -> TTerm
    tInt (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1)
              TTerm
    e | Just (Integer
    i, TTerm
    e) <- TTerm -> Maybe (Integer, TTerm)
    plusKView TTerm
    e -> Integer -> TTerm -> TTerm
    tPlusK (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) TTerm
    e
              TTerm
    e                 -> Integer -> TTerm -> TTerm
    tPlusK Integer
    1 TTerm
    e

          TApp (TCon QName
    c) [TTerm
    e]
            | QName -> Bool
    isPos QName
    c    -> TTerm -> TTerm
    tr TTerm
    e
            | QName -> Bool
    isNegSuc QName
    c ->
            case TTerm -> TTerm
    tr TTerm
    e of
              TLit (LitNat Integer
    n) -> Integer -> TTerm
    tInt (-Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)
              TTerm
    e | Just (Integer
    i, TTerm
    e) <- TTerm -> Maybe (Integer, TTerm)
    plusKView TTerm
    e -> Integer -> TTerm -> TTerm
    tNegPlusK (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) TTerm
    e
              TTerm
    e -> Integer -> TTerm -> TTerm
    tNegPlusK Integer
    1 TTerm
    e

          TCase Int
    e CaseInfo
    t TTerm
    d [TAlt]
    bs -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
    TCase Int
    e (CaseInfo -> [TAlt] -> CaseInfo
    inferCaseType CaseInfo
    t [TAlt]
    bs) (TTerm -> TTerm
    tr TTerm
    d) ([TAlt] -> TTerm) -> [TAlt] -> TTerm
    forall a b. (a -> b) -> a -> b
    $ (TAlt -> [TAlt]) -> [TAlt] -> [TAlt]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap TAlt -> [TAlt]
    trAlt [TAlt]
    bs
            where
              trAlt :: TAlt -> [TAlt]
    trAlt = \case
                TACon QName
    c Int
    0 TTerm
    b | QName -> Bool
    isZero QName
    c -> [Literal -> TTerm -> TAlt
    TALit (Integer -> Literal
    LitNat Integer
    0) (TTerm -> TTerm
    tr TTerm
    b)]
                TACon QName
    c Int
    1 TTerm
    b | QName -> Bool
    isSuc QName
    c  ->
                  case TTerm -> TTerm
    tr TTerm
    b of
                    -- Collapse nested n+k patterns
                    TCase Int
    0 CaseInfo
    _ TTerm
    d [TAlt]
    bs' -> (TAlt -> TAlt) -> [TAlt] -> [TAlt]
    forall a b. (a -> b) -> [a] -> [b]
    map TAlt -> TAlt
    sucBranch [TAlt]
    bs' [TAlt] -> [TAlt] -> [TAlt]
    forall a. [a] -> [a] -> [a]
    ++ [Integer -> TTerm -> TAlt
    nPlusKAlt Integer
    1 TTerm
    d]
                    TTerm
    b -> [Integer -> TTerm -> TAlt
    nPlusKAlt Integer
    1 TTerm
    b]
                  where
                    sucBranch :: TAlt -> TAlt
    sucBranch (TALit (LitNat Integer
    i) TTerm
    b) = Literal -> TTerm -> TAlt
    TALit (Integer -> Literal
    LitNat (Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1)) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm
    TLet (Integer -> TTerm
    tInt Integer
    i) TTerm
    b
                    sucBranch TAlt
    alt | Just (Integer
    k, TTerm
    b) <- TAlt -> Maybe (Integer, TTerm)
    nPlusKView TAlt
    alt =
                      Integer -> TTerm -> TAlt
    nPlusKAlt (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm
    TLet (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PAdd (Int -> TTerm
    TVar Int
    0) (Integer -> TTerm
    tInt Integer
    1)) (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $
                        Substitution' (SubstArg TTerm) -> TTerm -> TTerm
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst ([Int -> TTerm
    TVar Int
    1, Int -> TTerm
    TVar Int
    0] [TTerm] -> Substitution' TTerm -> Substitution' TTerm
    forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
    ++# Int -> Substitution' TTerm -> Substitution' TTerm
    forall a. Int -> Substitution' a -> Substitution' a
    wkS Int
    2 Substitution' TTerm
    forall a. Substitution' a
    idS) TTerm
    b
                    sucBranch TAlt
    _ = TAlt
    forall a. HasCallStack => a
    __IMPOSSIBLE__

                    nPlusKAlt :: Integer -> TTerm -> TAlt
    nPlusKAlt Integer
    k TTerm
    b = TTerm -> TTerm -> TAlt
    TAGuard (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PGeq (Int -> TTerm
    TVar Int
    e) (Integer -> TTerm
    tInt Integer
    k)) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $
                                    TTerm -> TTerm -> TTerm
    TLet (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PSub (Int -> TTerm
    TVar Int
    e) (Integer -> TTerm
    tInt Integer
    k)) TTerm
    b
                TACon QName
    c Int
    1 TTerm
    b | QName -> Bool
    isPos QName
    c ->
                  case TTerm -> TTerm
    tr TTerm
    b of
                    -- collapse nested nat patterns
                    TCase Int
    0 CaseInfo
    _ TTerm
    d [TAlt]
    bs -> (TAlt -> TAlt) -> [TAlt] -> [TAlt]
    forall a b. (a -> b) -> [a] -> [b]
    map TAlt -> TAlt
    forall a. SubstWith TTerm a => a -> a
    sub [TAlt]
    bs [TAlt] -> [TAlt] -> [TAlt]
    forall a. [a] -> [a] -> [a]
    ++ [TTerm -> TAlt
    posAlt TTerm
    d]
                    TTerm
    b -> [TTerm -> TAlt
    posAlt  TTerm
    b]
                  where
                    -- subst scrutinee for the pos argument
                    sub :: SubstWith TTerm a => a -> a
                    sub :: forall a. SubstWith TTerm a => a -> a
    sub = Substitution' (SubstArg a) -> a -> a
    forall a. Subst a => Substitution' (SubstArg a) -> a -> a
    applySubst (Int -> TTerm
    TVar Int
    e TTerm -> Substitution' TTerm -> Substitution' TTerm
    forall a. a -> Substitution' a -> Substitution' a
    :# Substitution' TTerm
    forall a. Substitution' a
    IdS)

                    posAlt :: TTerm -> TAlt
    posAlt TTerm
    b = TTerm -> TTerm -> TAlt
    TAGuard (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PGeq (Int -> TTerm
    TVar Int
    e) (Integer -> TTerm
    tInt Integer
    0)) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    forall a. SubstWith TTerm a => a -> a
    sub TTerm
    b

                TACon QName
    c Int
    1 TTerm
    b | QName -> Bool
    isNegSuc QName
    c ->
                  case TTerm -> TTerm
    tr TTerm
    b of
                    -- collapse nested nat patterns
                    TCase Int
    0 CaseInfo
    _ TTerm
    d [TAlt]
    bs -> (TAlt -> TAlt) -> [TAlt] -> [TAlt]
    forall a b. (a -> b) -> [a] -> [b]
    map TAlt -> TAlt
    negsucBranch [TAlt]
    bs [TAlt] -> [TAlt] -> [TAlt]
    forall a. [a] -> [a] -> [a]
    ++ [TTerm -> TAlt
    negAlt TTerm
    d]
                    TTerm
    b -> [TTerm -> TAlt
    negAlt TTerm
    b]
                  where
                    body :: TTerm -> TTerm
    body TTerm
    b   = TTerm -> TTerm -> TTerm
    TLet (Integer -> TTerm -> TTerm
    tNegPlusK Integer
    1 (Int -> TTerm
    TVar Int
    e)) TTerm
    b
                    negAlt :: TTerm -> TAlt
    negAlt TTerm
    b = TTerm -> TTerm -> TAlt
    TAGuard (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PLt (Int -> TTerm
    TVar Int
    e) (Integer -> TTerm
    tInt Integer
    0)) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    body TTerm
    b

                    negsucBranch :: TAlt -> TAlt
    negsucBranch (TALit (LitNat Integer
    i) TTerm
    b) = Literal -> TTerm -> TAlt
    TALit (Integer -> Literal
    LitNat (-Integer
    i Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    1)) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm
    body TTerm
    b
                    negsucBranch TAlt
    alt | Just (Integer
    k, TTerm
    b) <- TAlt -> Maybe (Integer, TTerm)
    nPlusKView TAlt
    alt =
                      TTerm -> TTerm -> TAlt
    TAGuard (TPrim -> TTerm -> TTerm -> TTerm
    tOp TPrim
    PLt (Int -> TTerm
    TVar Int
    e) (Integer -> TTerm
    tInt (-Integer
    k))) (TTerm -> TAlt) -> TTerm -> TAlt
    forall a b. (a -> b) -> a -> b
    $
                      TTerm -> TTerm
    body (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> TTerm -> TTerm
    TLet (Integer -> TTerm -> TTerm
    tNegPlusK (Integer
    k Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    + Integer
    1) (Int -> TTerm
    TVar (Int -> TTerm) -> Int -> TTerm
    forall a b. (a -> b) -> a -> b
    $ Int
    e Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)) TTerm
    b
                    negsucBranch TAlt
    _ = TAlt
    forall a. HasCallStack => a
    __IMPOSSIBLE__

                TACon QName
    c Int
    a TTerm
    b -> [QName -> Int -> TTerm -> TAlt
    TACon QName
    c Int
    a (TTerm -> TTerm
    tr TTerm
    b)]
                TALit Literal
    l TTerm
    b   -> [Literal -> TTerm -> TAlt
    TALit Literal
    l (TTerm -> TTerm
    tr TTerm
    b)]
                TAGuard TTerm
    g TTerm
    b -> [TTerm -> TTerm -> TAlt
    TAGuard (TTerm -> TTerm
    tr TTerm
    g) (TTerm -> TTerm
    tr TTerm
    b)]

          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 [TTerm]
    bs               -> TTerm -> [TTerm] -> TTerm
    TApp (TTerm -> TTerm
    tr TTerm
    a) ((TTerm -> TTerm) -> [TTerm] -> [TTerm]
    forall a b. (a -> b) -> [a] -> [b]
    map TTerm -> TTerm
    tr [TTerm]
    bs)
          TLet TTerm
    e TTerm
    b                -> TTerm -> TTerm -> TTerm
    TLet (TTerm -> TTerm
    tr TTerm
    e) (TTerm -> TTerm
    tr TTerm
    b)

        inferCaseType :: CaseInfo -> [TAlt] -> CaseInfo
    inferCaseType CaseInfo
    t (TACon QName
    c Int
    _ TTerm
    _ : [TAlt]
    _)
          | QName -> Bool
    isZero QName
    c   = CaseInfo
    t { caseType :: CaseType
    caseType = CaseType
    CTNat }
          | QName -> Bool
    isSuc QName
    c    = CaseInfo
    t { caseType :: CaseType
    caseType = CaseType
    CTNat }
          | QName -> Bool
    isPos QName
    c    = CaseInfo
    t { caseType :: CaseType
    caseType = CaseType
    CTInt }
          | QName -> Bool
    isNegSuc QName
    c = CaseInfo
    t { caseType :: CaseType
    caseType = CaseType
    CTInt }
        inferCaseType CaseInfo
    t [TAlt]
    _ = CaseInfo
    t

        nPlusKView :: TAlt -> Maybe (Integer, TTerm)
    nPlusKView (TAGuard (TApp (TPrim TPrim
    PGeq) [TVar Int
    0, (TLit (LitNat Integer
    k))])
                            (TLet (TApp (TPrim TPrim
    PSub) [TVar Int
    0, (TLit (LitNat Integer
    j))]) TTerm
    b))
          | Integer
    k Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j = (Integer, TTerm) -> Maybe (Integer, TTerm)
    forall a. a -> Maybe a
    Just (Integer
    k, TTerm
    b)
        nPlusKView TAlt
    _ = Maybe (Integer, TTerm)
    forall a. Maybe a
    Nothing