{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
module PlutusCore.Examples.Data.InterList
( interListData
, interNil
, interCons
, foldrInterList
) where
import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Quote
import PlutusCore.StdLib.Data.Function
import PlutusCore.StdLib.Data.Unit
import PlutusCore.StdLib.Type
interListData :: RecursiveType uni fun ()
interListData :: forall (uni :: * -> *) fun. RecursiveType uni fun ()
interListData = 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
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
TyName
interlist <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"interlist"
TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
let interlistBA :: Type TyName uni ()
interlistBA = Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
interlist) [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, () -> 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
interlist [() -> 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 (), () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
b (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 ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlistBA] (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
interNil :: Term TyName Name uni fun ()
interNil :: forall (uni :: * -> *) fun. Term TyName Name uni fun ()
interNil = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
let RecursiveType Type TyName uni ()
interlist forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapInterList = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
interListData
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
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 interlistBA :: Type TyName uni ()
interlistBA = Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlist [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a]
Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type TyName uni ()]
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall {uni :: * -> *} {fun} (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapInterList [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b]
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
f (()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlistBA] (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 TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
z
interCons :: Term TyName Name uni fun ()
interCons :: forall (uni :: * -> *) fun. Term TyName Name uni fun ()
interCons = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
let RecursiveType Type TyName uni ()
interlist forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapInterList = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
interListData
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
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
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 interlistBA :: Type TyName uni ()
interlistBA = Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlist [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a]
Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
y (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
xs Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlistBA
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type TyName uni ()]
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall {uni :: * -> *} {fun} (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapInterList [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b]
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
f (()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlistBA] (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 TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
f)
[ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
x
, () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
y
, () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
xs
]
foldrInterList :: uni `HasTypeAndTermLevel` () => Term TyName Name uni fun ()
foldrInterList :: forall (uni :: * -> *) fun.
HasTypeAndTermLevel uni () =>
Term TyName Name uni fun ()
foldrInterList = Quote (Term TyName Name uni fun ()) -> Term TyName Name uni fun ()
forall a. Quote a -> a
runQuote (Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ do
let interlist :: Type TyName uni ()
interlist = 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 ()
interListData
TyName
a0 <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a0"
TyName
b0 <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b0"
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
u <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"u"
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
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
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
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
y' <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y'"
let interlistOf :: TyName -> TyName -> Type TyName uni ()
interlistOf TyName
a' TyName
b' = Type TyName uni () -> [Type TyName uni ()] -> Type TyName uni ()
forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
interlist [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a', () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b']
fTy :: TyName -> TyName -> Type TyName uni ()
fTy TyName
a' TyName
b' = ()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a', () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b', () -> 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
fixTyArg2 :: Type TyName uni ()
fixTyArg2
= () -> 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
a (() -> 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
. () -> 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
b (() -> 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 -> TyName -> Type TyName uni ()
forall {uni :: * -> *}. TyName -> TyName -> Type TyName uni ()
fTy TyName
a TyName
b)
(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 -> TyName -> Type TyName uni ()
forall {uni :: * -> *}. TyName -> TyName -> Type TyName uni ()
interlistOf TyName
a TyName
b)
(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
instedFix :: Term TyName Name uni fun ()
instedFix = Term TyName Name uni fun ()
-> [Type TyName uni ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name uni fun ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName uni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit, Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fixTyArg2]
unwrappedXs :: Term TyName Name uni fun ()
unwrappedXs = ()
-> Term TyName Name uni fun ()
-> Type TyName uni ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst () (() -> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap () (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
xs)) (Type TyName uni () -> Term TyName Name uni fun ())
-> Type TyName uni () -> Term TyName Name 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
instedRec :: Term TyName Name uni fun ()
instedRec = Term TyName Name uni fun ()
-> [Type TyName uni ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn (()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply () (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
rec) Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval) [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a]
Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a0 (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
b0 (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
f (TyName -> TyName -> Type TyName uni ()
forall {uni :: * -> *}. TyName -> TyName -> Type TyName uni ()
fTy TyName
a0 TyName
b0)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
z (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> [Type TyName uni ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn
( Term TyName Name uni fun ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name uni fun ()
instedFix
[ ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun 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 :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fixTyArg2)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
u Type TyName uni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> TyName
-> Kind ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
f' (TyName -> TyName -> Type TyName uni ()
forall {uni :: * -> *}. TyName -> TyName -> Type TyName uni ()
fTy TyName
a TyName
b)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
xs (TyName -> TyName -> Type TyName uni ()
forall {uni :: * -> *}. TyName -> TyName -> Type TyName uni ()
interlistOf TyName
a TyName
b)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name uni fun ()
forall (uni :: * -> *) fun. Term TyName Name uni fun ()
unwrappedXs
[ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
z
, ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
y (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
xs' (TyName -> TyName -> Type TyName uni ()
forall {uni :: * -> *}. TyName -> TyName -> Type TyName uni ()
interlistOf TyName
b TyName
a)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
f')
[ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
x
, () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
y
, Term TyName Name uni fun ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn Term TyName Name uni fun ()
forall {fun}. Term TyName Name uni fun ()
instedRec
[ ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
y' (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> (Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName uni ()
-> Term TyName Name uni fun ()
-> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs () Name
x' (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
(Term TyName Name uni fun () -> Term TyName Name uni fun ())
-> Term TyName Name uni fun () -> Term TyName Name uni fun ()
forall a b. (a -> b) -> a -> b
$ Term TyName Name uni fun ()
-> [Term TyName Name uni fun ()] -> Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
f')
[ () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
x'
, () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
y'
]
, () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
xs'
]
]
]
, Term TyName Name uni fun ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval
]
)
[ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a0
, () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b0
]