-- | @unit@ and related functions.

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

module PlutusCore.StdLib.Data.Unit
    ( unit
    , unitval
    , sequ
    ) where

import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name
import PlutusCore.Quote

import Universe

-- | '()' as a PLC type.
unit :: uni `Includes` () => Type TyName uni ()
unit :: Type TyName uni ()
unit = () -> Type TyName uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @() ()

-- | '()' as a PLC term.
unitval :: (TermLike term TyName Name uni fun, uni `Includes` ()) => term ()
unitval :: term ()
unitval = () -> () -> term ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, Includes uni a) =>
ann -> a -> term ann
mkConstant () ()

-- | 'seq' specified to '()' as a PLC term.
sequ :: (TermLike term TyName Name uni fun, uni `Includes` ()) => term ()
sequ :: term ()
sequ = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
    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
x Type TyName uni ()
forall (uni :: * -> *). Includes uni () => Type TyName uni ()
unit
        (term () -> term ()) -> (term () -> term ()) -> term () -> 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
y Type TyName uni ()
forall (uni :: * -> *). Includes uni () => Type TyName uni ()
unit
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ term ()
forall (term :: * -> *) (uni :: * -> *) fun.
(TermLike term TyName Name uni fun, Includes uni ()) =>
term ()
unitval