-- | Built-in @pair@ and related functions.

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

module PlutusCore.StdLib.Data.Pair
    ( pair
    , fstPair
    , sndPair
    , uncurry
    ) where

import Prelude hiding (fst, snd, uncurry)

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

-- | @(,)@ as a built-in PLC type.
pair :: uni `HasTypeLevel` (,) => Type tyname uni ()
pair :: forall (uni :: * -> *) tyname.
HasTypeLevel uni (,) =>
Type tyname uni ()
pair = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @(,) ()

-- | @fst@ as a PLC term.
--
-- > /\(a :: *) (b :: *) -> \(p : pair a b) -> fst {a} {b} p
fstPair :: TermLike term tyname name DefaultUni DefaultFun => term ()
fstPair :: forall (term :: * -> *) tyname name.
TermLike term tyname name DefaultUni DefaultFun =>
term ()
fstPair = () -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
FstPair

-- | @snd@ as a PLC term.
--
-- > /\(a :: *) (b :: *) -> \(p : pair a b) -> snd {a} {b} p
sndPair :: TermLike term tyname name DefaultUni DefaultFun => term ()
sndPair :: forall (term :: * -> *) tyname name.
TermLike term tyname name DefaultUni DefaultFun =>
term ()
sndPair = () -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
SndPair

-- | @uncurry@ as a PLC term.
--
-- > /\(a :: *) (b :: *) (c :: *) -> \(f : a -> b -> c) (p : pair a b) ->
-- >     f (fst {a} {b} p) (snd {a} {b} p)
uncurry :: TermLike term TyName Name DefaultUni DefaultFun => term ()
uncurry :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
term ()
uncurry = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    TyName
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    TyName
c <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"c"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
p <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"p"
    term () -> Quote (term ())
forall a. a -> QuoteT Identity a
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
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
c (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term ann
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
f (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
c)
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term ann
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
p (Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni (,) =>
Type tyname uni ()
pair [() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b])
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
            [ () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
forall (term :: * -> *) tyname name.
TermLike term tyname name DefaultUni DefaultFun =>
term ()
fstPair [() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b]) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
p
            , () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
forall (term :: * -> *) tyname name.
TermLike term tyname name DefaultUni DefaultFun =>
term ()
sndPair [() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b]) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
p
            ]