-- | 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