-- | Functions related to @integer@.

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE TypeOperators     #-}

module PlutusCore.StdLib.Data.Integer
    ( integer
    , succInteger
    ) where

import PlutusCore.Core
import PlutusCore.Default.Builtins
import PlutusCore.MkPlc
import PlutusCore.Name
import PlutusCore.Quote

import Universe

integer :: uni `Includes` Integer => Type tyname uni ()
integer :: Type tyname uni ()
integer = () -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()

-- |  @succ :: Integer -> Integer@ as a PLC term.
--
-- > \(i : integer) -> addInteger i 1
succInteger :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
succInteger :: term ()
succInteger = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    Name
i  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"i"
    term () -> Quote (term ())
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> ([term ()] -> term ()) -> [term ()] -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
i Type TyName uni ()
forall (uni :: * -> *) tyname.
Includes uni Integer =>
Type tyname uni ()
integer
        (term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> DefaultFun -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
AddInteger)
        ([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
i
          , () -> Integer -> term ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, Includes uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1
          ]