-- | @list@ and related functions.

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

module PlutusCore.StdLib.Data.ScottList
    ( listData
    , listTy
    , nil
    , cons
    , foldrList
    , foldList
    , map
    , reverse
    , enumFromTo
    , sum
    , sumr
    , product
    ) where

import Prelude hiding (enumFromTo, map, product, reverse, sum)

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

import PlutusCore.StdLib.Data.Bool
import PlutusCore.StdLib.Data.Function
import PlutusCore.StdLib.Data.Integer
import PlutusCore.StdLib.Data.Unit
import PlutusCore.StdLib.Type

import Universe

-- | @List@ as a PLC type.
--
-- > fix \(list :: * -> *) (a :: *) -> all (r :: *). r -> (a -> list a -> r) -> r
listData :: RecursiveType uni fun ()
listData :: RecursiveType uni fun ()
listData = Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ()
forall a. Quote a -> a
runQuote (Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ())
-> Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ()
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
list <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"list"
    TyName
r    <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
    let listA :: Type TyName uni ()
listA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
list) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    FromDataPieces uni () (RecursiveType uni fun ())
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveType () TyName
list [() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
        (Type TyName uni () -> Quote (RecursiveType uni fun ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (RecursiveType uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (Type TyName uni () -> Quote (RecursiveType uni fun ()))
-> Type TyName uni () -> Quote (RecursiveType uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r

listTy :: Type TyName uni ()
listTy :: Type TyName uni ()
listTy = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
listData

-- |  '[]' as a PLC term.
--
-- >  /\(a :: *) -> wrapList [a] /\(r :: *) -> \(z : r) (f : a -> list a -> r) -> z)
nil :: TermLike term TyName Name uni fun => term ()
nil :: term ()
nil = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let RecursiveType Type TyName uni ()
list forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapList = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
listData
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
    Name
z <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    let listA :: Type TyName uni ()
listA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
list (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    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
. () -> TyName -> Kind () -> term () -> term ()
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
. [Type TyName uni ()] -> term () -> term ()
forall (uni :: * -> *) fun (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapList [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a]
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> 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 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
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
z

-- |  '(:)' as a PLC term.
--
-- > /\(a :: *) -> \(x : a) (xs : list a) ->
-- >     wrapList [a] /\(r :: *) -> \(z : r) (f : a -> list a -> r) -> f x xs
cons :: TermLike term TyName Name uni fun => term ()
cons :: term ()
cons = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let RecursiveType Type TyName uni ()
list forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapList = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
listData
    TyName
a  <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    Name
x  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Name
xs <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
    TyName
r  <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
    Name
z  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
    Name
f  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    let listA :: Type TyName uni ()
listA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
list (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    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
. () -> TyName -> Kind () -> term () -> term ()
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
. () -> 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 (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (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
xs Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type TyName uni ()] -> term () -> term ()
forall (uni :: * -> *) fun (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapList [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a]
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> 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 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
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
          [ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
          , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs
          ]

-- |  @foldrList@ as a PLC term.
--
-- > /\(a :: *) (r :: *) -> \(f : a -> r -> r) (z : r) ->
-- >     fix {list a} {r} \(rec : list a -> r) (xs : list a) ->
-- >         unwrap xs {r} z \(x : a) (xs' : list a) -> f x (rec xs')
foldrList :: TermLike term TyName Name uni fun => term ()
foldrList :: term ()
foldrList = 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
r   <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
    Name
f   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
z   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
    Name
rec <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Name
xs  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
    Name
x   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Name
xs' <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs'"
    let listA :: Type TyName uni ()
listA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listTy (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    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
. () -> TyName -> Kind () -> term () -> term ()
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 (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> 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 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
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
apply () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r])
        (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
rec (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
xs Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA
        (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
apply () (() -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
unwrap () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs)) (Type TyName uni () -> term ()) -> Type TyName uni () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (term () -> term ()) -> term () -> 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
z)
        (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
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (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
xs' Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
          [ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
          , () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec) (term () -> term ()) -> term () -> 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
xs'
          ]

-- |  @map@ as a PLC term.
--
-- > /\(a :: *) (b :: *) -> \(f : a -> b) ->
-- >     foldrList {a} {list b} (\(x : a) -> cons {b} (f x)) (nil {b})
map :: TermLike term TyName Name uni fun => term ()
map :: term ()
map = 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"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    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
. () -> TyName -> Kind () -> term () -> term ()
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 (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
. () -> 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
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
        (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 () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
foldrList [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listTy (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
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
$ [   () -> 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 (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
            (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
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
cons (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b))
            (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
apply () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
            (term () -> term ()) -> term () -> 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
x
          , () -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
nil (Type TyName uni () -> term ()) -> Type TyName uni () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b
          ]

-- |  'foldl\'' as a PLC term.
--
-- > /\(a :: *) (r :: *) -> \(f : r -> a -> r) ->
-- >     fix {r} {list a -> r} \(rec : r -> list a -> r) (z : r) (xs : list a) ->
-- >         unwrap xs {r} z \(x : a) (xs' : list a) -> rec (f z x) xs'
foldList :: TermLike term TyName Name uni fun => term ()
foldList :: term ()
foldList = 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
r   <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
    Name
f   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
rec <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Name
z   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
    Name
xs  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
    Name
x   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Name
xs' <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs'"
    let listA :: Type TyName uni ()
listA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listTy (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
    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
. () -> TyName -> Kind () -> term () -> term ()
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 (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> 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 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
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
apply () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r, ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r])
        (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
rec (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (Type TyName uni () -> Type TyName uni ())
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Type TyName uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
        (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
xs Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA
        (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
apply () (() -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
unwrap () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs)) (Type TyName uni () -> term ()) -> Type TyName uni () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (term () -> term ()) -> term () -> 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
z)
        (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
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (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
xs' Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA
        (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 () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec)
        ([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f) [() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
z, () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x]
          , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs'
          ]

-- |  'reverse' as a PLC term.
--
-- > /\(a :: *) -> \(xs : list a) ->
-- >     foldList {a} {list a} (\(r : list a) (x : a) -> cons {a} x r) (nil {a})
reverse :: TermLike term TyName Name uni fun => term ()
reverse :: term ()
reverse = 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"
    Name
xs  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
    Name
x   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Name
r   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"r"
    let vA :: Type TyName uni ()
vA = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
        listA :: Type TyName uni ()
listA = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listTy Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
vA
    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
. () -> TyName -> Kind () -> term () -> term ()
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
. () -> 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
xs Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
foldList [Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
vA, Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA])
            [ () -> 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
r Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listA (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
x Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
vA (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
cons Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
vA) [() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x, () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
r]
            , () -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
nil Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
vA
            , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs
            ]

-- | 'enumFromTo' as a PLC term
--
-- > \(n m : integer) ->
-- >     fix {integer} {list (integer)}
-- >         (\(rec : integer -> list (integer)) (n' : integer) ->
-- >             ifThenElse {list (integer)}
-- >                 (lessThanEqualsInteger n' m)
-- >                 (cons {integer} n' (rec (succInteger n')))
-- >                 (nil {integer}))
-- >         n
enumFromTo
    :: ( TermLike term TyName Name uni DefaultFun
       , uni `Includes` Integer, uni `Includes` (), uni `Includes` Bool
       )
    => term ()
enumFromTo :: term ()
enumFromTo = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    Name
n   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"n"
    Name
m   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"m"
    Name
rec <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Name
n'  <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"n'"
    Name
u   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"u"
    let leqInteger :: term ()
leqInteger  = () -> DefaultFun -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
LessThanEqualsInteger
        int :: Type tyname uni ()
int = () -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
        listInt :: Type TyName uni ()
listInt = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
listTy Type TyName uni ()
forall tyname. Type tyname uni ()
int
    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
n Type TyName uni ()
forall tyname. Type tyname uni ()
int
        (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
m Type TyName uni ()
forall tyname. Type tyname uni ()
int
        (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 () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName uni ()
forall tyname. Type tyname uni ()
int, Type TyName uni ()
listInt])
        ([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [   () -> 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
rec (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall tyname. Type tyname uni ()
int Type TyName uni ()
listInt)
            (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
n' Type TyName uni ()
forall tyname. Type tyname uni ()
int
            (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 () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun, Includes uni Bool,
 Includes uni ()) =>
term ()
ifThenElse Type TyName uni ()
listInt)
            ([term ()] -> term ()) -> [term ()] -> term ()
forall a b. (a -> b) -> a -> b
$ [ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () term ()
leqInteger [ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
n' , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
m]
              , () -> 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
u Type TyName uni ()
forall (uni :: * -> *). Includes uni () => Type TyName uni ()
unit (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
cons Type TyName uni ()
forall tyname. Type tyname uni ()
int)
                    [ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
n'
                    ,    () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec)
                       (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
apply () term ()
forall (term :: * -> *) (uni :: * -> *).
(TermLike term TyName Name uni DefaultFun, Includes uni Integer) =>
term ()
succInteger
                       (term () -> term ()) -> term () -> 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
n'
                    ]
              , () -> 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
u Type TyName uni ()
forall (uni :: * -> *). Includes uni () => Type TyName uni ()
unit (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
nil Type TyName uni ()
forall tyname. Type tyname uni ()
int
              ]
          , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
n
          ]

-- |  'sum' as a PLC term.
--
-- > foldList {integer} {integer} addInteger 0
sum :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
sum :: term ()
sum = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let int :: Type tyname uni ()
int = () -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
        add :: term ()
add = () -> 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 ())
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
. () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
foldList [Type TyName uni ()
forall tyname. Type tyname uni ()
int, Type TyName uni ()
forall tyname. Type tyname uni ()
int])
        ([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term ()
add , () -> 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
0]

-- > foldrList {integer} {integer} 0 addInteger
sumr :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
sumr :: term ()
sumr = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let int :: Type tyname uni ()
int = () -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
        add :: term ()
add = () -> 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 ())
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
. () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
foldrList [Type TyName uni ()
forall tyname. Type tyname uni ()
int, Type TyName uni ()
forall tyname. Type tyname uni ()
int])
        ([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term ()
add, () -> 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
0 ]

-- |  'product' as a PLC term.
--
-- > foldList {integer} {integer} multiplyInteger 1
product :: (TermLike term TyName Name uni DefaultFun, uni `Includes` Integer) => term ()
product :: term ()
product = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let int :: Type tyname uni ()
int = () -> Type tyname uni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
        mul :: term ()
mul = () -> DefaultFun -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
MultiplyInteger
    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
. () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> term () -> [Type TyName uni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
foldList [Type TyName uni ()
forall tyname. Type tyname uni ()
int, Type TyName uni ()
forall tyname. Type tyname uni ()
int])
        ([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term ()
mul , () -> 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]