-- | 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.Abstract.Name (QName)
import Agda.Syntax.Position
import Agda.Syntax.Treeless
import Agda.Syntax.Literal

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

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  "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  "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  "primWord64ToNat"
  where
    con :: Term -> Maybe QName
con (I.Con c :: ConHead
c _ _) = 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 _           = Maybe QName
forall a. Maybe a
Nothing
    def :: Term -> Maybe QName
def (I.Def d :: QName
d _) = QName -> Maybe QName
forall (f :: * -> *) a. Applicative f => a -> f a
pure QName
d
    def _           = 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 :: a -> Maybe b
a b :: 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 a :: Term -> Maybe b
a b :: 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 a :: PrimFun -> Maybe b
a p :: 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 t :: 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{..} = TTerm -> TTerm
tr
  where
    tr :: TTerm -> TTerm
tr t :: TTerm
t = case TTerm
t of

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

      TDef f :: 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 q :: QName
q) (_ : _ : _ : _ : e :: TTerm
e : f :: TTerm
f : es :: [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 0) (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
mkTApp (Int -> TTerm -> TTerm
forall t a. Subst t a => Int -> a -> a
raise 1 TTerm
f) [Int -> TTerm
TVar 0]) [TTerm]
es

      TApp (TCon s :: QName
s) [e :: TTerm
e] | QName -> Bool
isSuc QName
s ->
        case TTerm -> TTerm
tr TTerm
e of
          TLit (LitNat r :: Range
r n :: Integer
n) -> Integer -> TTerm
tInt (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
          e :: TTerm
e | Just (i :: Integer
i, e :: 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
+ 1) TTerm
e
          e :: TTerm
e                 -> Integer -> TTerm -> TTerm
tPlusK 1 TTerm
e

      TApp (TCon c :: QName
c) [e :: 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 _ n :: Integer
n) -> Integer -> TTerm
tInt (-Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)
          e :: TTerm
e | Just (i :: Integer
i, e :: 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
+ 1) TTerm
e
          e :: TTerm
e -> Integer -> TTerm -> TTerm
tNegPlusK 1 TTerm
e

      TCase e :: Int
e t :: CaseInfo
t d :: TTerm
d bs :: [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 b :: TAlt
b = case TAlt
b of
            TACon c :: QName
c 0 b :: TTerm
b | QName -> Bool
isZero QName
c -> [Literal -> TTerm -> TAlt
TALit (Range -> Integer -> Literal
LitNat Range
forall a. Range' a
noRange 0) (TTerm -> TTerm
tr TTerm
b)]
            TACon c :: QName
c 1 b :: TTerm
b | QName -> Bool
isSuc QName
c  ->
              case TTerm -> TTerm
tr TTerm
b of
                -- Collapse nested n+k patterns
                TCase 0 _ d :: TTerm
d bs' :: [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 1 TTerm
d]
                b :: TTerm
b -> [Integer -> TTerm -> TAlt
nPlusKAlt 1 TTerm
b]
              where
                sucBranch :: TAlt -> TAlt
sucBranch (TALit (LitNat r :: Range
r i :: Integer
i) b :: TTerm
b) = Literal -> TTerm -> TAlt
TALit (Range -> Integer -> Literal
LitNat Range
r (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)) (TTerm -> TAlt) -> TTerm -> TAlt
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm -> TTerm
TLet (Integer -> TTerm
tInt Integer
i) TTerm
b
                sucBranch alt :: TAlt
alt | Just (k :: Integer
k, b :: 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
+ 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 0) (Integer -> TTerm
tInt 1)) (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$
                    Substitution' TTerm -> TTerm -> TTerm
forall t a. Subst t a => Substitution' t -> a -> a
applySubst ([Int -> TTerm
TVar 1, Int -> TTerm
TVar 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 2 Substitution' TTerm
forall a. Substitution' a
idS) TTerm
b
                sucBranch _ = TAlt
forall a. HasCallStack => a
__IMPOSSIBLE__

                nPlusKAlt :: Integer -> TTerm -> TAlt
nPlusKAlt k :: Integer
k b :: 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

                str :: Empty -> Substitution' a
str err :: Empty
err = Empty -> [Maybe a] -> Substitution' a
forall a. DeBruijn a => Empty -> [Maybe a] -> Substitution' a
compactS Empty
err [Maybe a
forall a. Maybe a
Nothing]

            TACon c :: QName
c 1 b :: TTerm
b | QName -> Bool
isPos QName
c ->
              case TTerm -> TTerm
tr TTerm
b of
                -- collapse nested nat patterns
                TCase 0 _ d :: TTerm
d bs :: [TAlt]
bs -> (TAlt -> TAlt) -> [TAlt] -> [TAlt]
forall a b. (a -> b) -> [a] -> [b]
map TAlt -> TAlt
forall a. Subst TTerm a => a -> a
sub [TAlt]
bs [TAlt] -> [TAlt] -> [TAlt]
forall a. [a] -> [a] -> [a]
++ [TTerm -> TAlt
posAlt TTerm
d]
                b :: TTerm
b -> [TTerm -> TAlt
posAlt  TTerm
b]
              where
                -- subst scrutinee for the pos argument
                sub :: Subst TTerm a => a -> a
                sub :: a -> a
sub = Substitution' TTerm -> a -> a
forall t a. Subst t a => Substitution' t -> 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 b :: TTerm
b = TTerm -> TTerm -> TAlt
TAGuard (TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PGeq (Int -> TTerm
TVar Int
e) (Integer -> TTerm
tInt 0)) (TTerm -> TAlt) -> TTerm -> TAlt
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm
forall a. Subst TTerm a => a -> a
sub TTerm
b

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

                negsucBranch :: TAlt -> TAlt
negsucBranch (TALit (LitNat r :: Range
r i :: Integer
i) b :: TTerm
b) = Literal -> TTerm -> TAlt
TALit (Range -> Integer -> Literal
LitNat Range
r (-Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- 1)) (TTerm -> TAlt) -> TTerm -> TAlt
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm
body TTerm
b
                negsucBranch alt :: TAlt
alt | Just (k :: Integer
k, b :: 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
+ 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
+ 1)) TTerm
b
                negsucBranch _ = TAlt
forall a. HasCallStack => a
__IMPOSSIBLE__


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

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

      TCoerce a :: TTerm
a -> TTerm -> TTerm
TCoerce (TTerm -> TTerm
tr TTerm
a)

      TLam b :: TTerm
b                  -> TTerm -> TTerm
TLam (TTerm -> TTerm
tr TTerm
b)
      TApp a :: TTerm
a bs :: [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 e :: TTerm
e b :: TTerm
b                -> TTerm -> TTerm -> TTerm
TLet (TTerm -> TTerm
tr TTerm
e) (TTerm -> TTerm
tr TTerm
b)

    inferCaseType :: CaseInfo -> [TAlt] -> CaseInfo
inferCaseType t :: CaseInfo
t (TACon c :: QName
c _ _ : _)
      | 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 t :: CaseInfo
t _ = CaseInfo
t

    nPlusKView :: TAlt -> Maybe (Integer, TTerm)
nPlusKView (TAGuard (TApp (TPrim PGeq) [TVar 0, (TLit (LitNat _ k :: Integer
k))])
                        (TLet (TApp (TPrim PSub) [TVar 0, (TLit (LitNat _ j :: Integer
j))]) b :: 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 _ = Maybe (Integer, TTerm)
forall a. Maybe a
Nothing