-- | 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.
{-# LANGUAGE CPP #-}
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

import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.Maybe
import Agda.Utils.Impossible

#include "undefined.h"

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

builtinKit :: TCM BuiltinKit
builtinKit =
  BuiltinKit <$> isB con builtinZero
             <*> isB con builtinSuc
             <*> isB con builtinIntegerPos
             <*> isB con builtinIntegerNegSuc
             <*> isB def builtinNatPlus
             <*> isB def builtinNatTimes
             <*> isB def builtinNatLess
             <*> isB def builtinNatEquals
             <*> isP pf  "primForce"
             <*> isP pf  "primWord64FromNat"
             <*> isP pf  "primWord64ToNat"
  where
    con (I.Con c _ _) = pure $ I.conName c
    con _           = Nothing
    def (I.Def d _) = pure d
    def _           = Nothing

    pf = Just . primFunName

    is  a b = maybe (const False) (==) . (a =<<) <$> b
    isB a b = is a (getBuiltin' b)
    isP a p = is a (getPrimitive' p)

translateBuiltins :: TTerm -> TCM TTerm
translateBuiltins t = do
  kit <- builtinKit
  return $ transform kit t

transform :: BuiltinKit -> TTerm -> TTerm
transform BuiltinKit{..} = tr
  where
    tr t = case t of

      TCon c | isZero c   -> tInt 0
             | isSuc c    -> TLam (tPlusK 1 (TVar 0))
             | isPos c    -> TLam (TVar 0)
             | isNegSuc c -> TLam $ tNegPlusK 1 (TVar 0)

      TDef f | isPlus f   -> TPrim PAdd
             | isTimes f  -> TPrim PMul
             | isLess f   -> TPrim PLt
             | isEqual f  -> TPrim PEqI
             | isWord64ToNat f   -> TPrim P64ToI
             | isWord64FromNat f -> 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) (_ : _ : _ : _ : e : f : es)
        | isForce q -> tr $ TLet e $ mkTApp (tOp PSeq (TVar 0) $ mkTApp (raise 1 f) [TVar 0]) es

      TApp (TCon s) [e] | isSuc s ->
        case tr e of
          TLit (LitNat r n) -> tInt (n + 1)
          e | Just (i, e) <- plusKView e -> tPlusK (i + 1) e
          e                 -> tPlusK 1 e

      TApp (TCon c) [e]
        | isPos c    -> tr e
        | isNegSuc c ->
        case tr e of
          TLit (LitNat _ n) -> tInt (-n - 1)
          e | Just (i, e) <- plusKView e -> tNegPlusK (i + 1) e
          e -> tNegPlusK 1 e

      TCase e t d bs -> TCase e (inferCaseType t bs) (tr d) $ concatMap trAlt bs
        where
          trAlt b = case b of
            TACon c 0 b | isZero c -> [TALit (LitNat noRange 0) (tr b)]
            TACon c 1 b | isSuc c  ->
              case tr b of
                -- Collapse nested n+k patterns
                TCase 0 _ d bs' -> map sucBranch bs' ++ [nPlusKAlt 1 d]
                b -> [nPlusKAlt 1 b]
              where
                sucBranch (TALit (LitNat r i) b) = TALit (LitNat r (i + 1)) $ TLet (tInt i) b
                sucBranch alt | Just (k, b) <- nPlusKView alt =
                  nPlusKAlt (k + 1) $ TLet (tOp PAdd (TVar 0) (tInt 1)) $
                    applySubst ([TVar 1, TVar 0] ++# wkS 2 idS) b
                sucBranch _ = __IMPOSSIBLE__

                nPlusKAlt k b = TAGuard (tOp PGeq (TVar e) (tInt k)) $
                                TLet (tOp PSub (TVar e) (tInt k)) b

                str err = compactS err [Nothing]

            TACon c 1 b | isPos c ->
              case tr b of
                -- collapse nested nat patterns
                TCase 0 _ d bs -> map sub bs ++ [posAlt d]
                b -> [posAlt  b]
              where
                -- subst scrutinee for the pos argument
                sub :: Subst TTerm a => a -> a
                sub = applySubst (TVar e :# IdS)

                posAlt b = TAGuard (tOp PGeq (TVar e) (tInt 0)) $ sub b

            TACon c 1 b | isNegSuc c ->
              case tr b of
                -- collapse nested nat patterns
                TCase 0 _ d bs -> map negsucBranch bs ++ [negAlt d]
                b -> [negAlt b]
              where
                body b   = TLet (tNegPlusK 1 (TVar e)) b
                negAlt b = TAGuard (tOp PLt (TVar e) (tInt 0)) $ body b

                negsucBranch (TALit (LitNat r i) b) = TALit (LitNat r (-i - 1)) $ body b
                negsucBranch alt | Just (k, b) <- nPlusKView alt =
                  TAGuard (tOp PLt (TVar e) (tInt (-k))) $
                  body $ TLet (tNegPlusK (k + 1) (TVar $ e + 1)) b
                negsucBranch _ = __IMPOSSIBLE__


            TACon c a b -> [TACon c a (tr b)]
            TALit l b   -> [TALit l (tr b)]
            TAGuard g b -> [TAGuard (tr g) (tr b)]

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

      TCoerce a -> TCoerce (tr a)

      TLam b                  -> TLam (tr b)
      TApp a bs               -> TApp (tr a) (map tr bs)
      TLet e b                -> TLet (tr e) (tr b)

    inferCaseType t (TACon c _ _ : _)
      | isZero c   = t { caseType = CTNat }
      | isSuc c    = t { caseType = CTNat }
      | isPos c    = t { caseType = CTInt }
      | isNegSuc c = t { caseType = CTInt }
    inferCaseType t _ = t

    nPlusKView (TAGuard (TApp (TPrim PGeq) [TVar 0, (TLit (LitNat _ k))])
                        (TLet (TApp (TPrim PSub) [TVar 0, (TLit (LitNat _ j))]) b))
      | k == j = Just (k, b)
    nPlusKView _ = Nothing