{-# LANGUAGE OverloadedStrings #-}

module PlutusCore.Examples.Data.List
    ( omapList
    ) where

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

import PlutusCore.StdLib.Data.Function
import PlutusCore.StdLib.Data.List

import PlutusCore.Examples.Builtins

-- | Monomorphic @map@ over built-in lists.
--
-- /\(a :: *) -> \(f : a -> a) ->
--     fix {list a} {list a} \(rec : list a -> list a) (xs : list a) ->
--         matchList {a} xs {list a} xs \(x : a) (xs' : list a) -> cons {a} (f x) (rec xs')
omapList :: MatchOption -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList :: MatchOption
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList MatchOption
optMatch = Quote
  (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a. Quote a -> a
runQuote (Quote
   (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
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
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
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 DefaultUni ()
listA = ()
-> 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
TyApp () Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni [] =>
Type tyname uni ()
list (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
a
        unwrap' :: ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
unwrap' ()
ann = ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ()
ann (Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ())
-> (Type TyName DefaultUni ()
    -> Term TyName Name DefaultUni (Either DefaultFun b) ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () ((DefaultFun -> Either DefaultFun b)
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall fun fun' tyname name (uni :: * -> *) ann.
(fun -> fun')
-> Term tyname name uni fun ann -> Term tyname name uni fun' ann
mapFun DefaultFun -> Either DefaultFun b
forall a b. a -> Either a b
Left (MatchOption -> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
matchList MatchOption
optMatch)) (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
    Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Quote
      (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> TyName
-> Kind ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) 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 TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) 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 ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName DefaultUni ()
listA, Type TyName DefaultUni ()
listA])
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) 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
rec (()
-> 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 () Type TyName DefaultUni ()
listA Type TyName DefaultUni ()
listA)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) 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
xs Type TyName DefaultUni ()
listA
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall {b}.
()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
unwrap' () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs)) Type TyName DefaultUni ()
listA) (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) 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
x (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) 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
xs' Type TyName DefaultUni ()
listA
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Quote
      (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Term
      TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (()
-> Either DefaultFun ExtensionFun
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Either DefaultFun ExtensionFun
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () (Either DefaultFun ExtensionFun
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Either DefaultFun ExtensionFun
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ DefaultFun -> Either DefaultFun ExtensionFun
forall a b. a -> Either a b
Left DefaultFun
MkCons) (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
            [ ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f) (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
            , ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec) (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs'
            ]