{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module PlutusCore.Examples.Data.TreeForest
( treeData
, forestData
, treeNode
, forestNil
, forestCons
) where
import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Normalize
import PlutusCore.Quote
import PlutusCore.StdLib.Type
import Universe
infixr 5 ~~>
class HasArrow a where
(~~>) :: a -> a -> a
instance a ~ () => HasArrow (Kind a) where
~~> :: Kind a -> Kind a -> Kind a
(~~>) = a -> Kind a -> Kind a -> Kind a
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ()
instance a ~ () => HasArrow (Type tyname uni a) where
~~> :: Type tyname uni a -> Type tyname uni a -> Type tyname uni a
(~~>) = a -> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ()
star :: Kind ()
star :: Kind ()
star = () -> Kind ()
forall ann. ann -> Kind ann
Type ()
treeTag :: Type TyName uni ()
treeTag :: forall (uni :: * -> *). Type TyName uni ()
treeTag = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
TyName
t <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"t"
TyName
f <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"f"
Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (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
TyLam () TyName
t Kind ()
star
(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
TyLam () TyName
f Kind ()
star
(Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (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
t
forestTag :: Type TyName uni ()
forestTag :: forall (uni :: * -> *). Type TyName uni ()
forestTag = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
TyName
t <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"t"
TyName
f <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"f"
Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (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
TyLam () TyName
t Kind ()
star
(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
TyLam () TyName
f Kind ()
star
(Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (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
f
asTree :: Type TyName uni ()
asTree :: forall (uni :: * -> *). Type TyName uni ()
asTree = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
TyName
d <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"d"
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (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
TyLam () TyName
d (Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> (Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star) Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star)
(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
TyLam () TyName
a Kind ()
star
(Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ 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
d)
[ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
, Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
treeTag
]
asForest :: Type TyName uni ()
asForest :: forall (uni :: * -> *). Type TyName uni ()
asForest = Quote (Type TyName uni ()) -> Type TyName uni ()
forall a. Quote a -> a
runQuote (Quote (Type TyName uni ()) -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ do
TyName
d <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"d"
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
Type TyName uni () -> Quote (Type TyName uni ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Type TyName uni () -> Quote (Type TyName uni ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (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
TyLam () TyName
d (Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> (Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star) Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star)
(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
TyLam () TyName
a Kind ()
star
(Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ 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
d)
[ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
, Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
forestTag
]
treeForestData :: RecursiveType uni fun ()
treeForestData :: forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeForestData = 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
treeForest <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"treeForest"
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"
TyName
tag <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"tag"
let vA :: Type TyName uni ()
vA = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
vR :: Type TyName uni ()
vR = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
recSpine :: [Type TyName uni ()]
recSpine = [() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
treeForest, Type TyName uni ()
vA]
let tree :: Type TyName uni ()
tree = 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 ()
asTree [Type TyName uni ()]
recSpine
forest :: Type TyName uni ()
forest = 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 ()
asForest [Type TyName uni ()]
recSpine
body :: Type TyName uni ()
body
= () -> 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 ()
forall a b. (a -> b) -> a -> b
$ 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
tag)
[ (Type TyName uni ()
vA Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> Type TyName uni ()
forest Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> Type TyName uni ()
vR) Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> Type TyName uni ()
vR
, Type TyName uni ()
vR Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> (Type TyName uni ()
tree Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> Type TyName uni ()
forest Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> Type TyName uni ()
vR) Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall a. HasArrow a => a -> a -> a
~~> Type TyName uni ()
vR
]
FromDataPieces uni () (RecursiveType uni fun ())
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveType () TyName
treeForest
[() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a Kind ()
star, () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
tag (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star Kind () -> Kind () -> Kind ()
forall a. HasArrow a => a -> a -> a
~~> Kind ()
star]
Type TyName uni ()
body
treeData :: RecursiveType uni fun ()
treeData :: forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeData = 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
let RecursiveType Type TyName uni ()
treeForest forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapTreeForest = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeForestData
tree :: Type TyName uni ()
tree = ()
-> 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 ()
asTree Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
treeForest
RecursiveType uni fun () -> Quote (RecursiveType uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecursiveType uni fun () -> Quote (RecursiveType uni fun ()))
-> RecursiveType uni fun () -> Quote (RecursiveType uni fun ())
forall a b. (a -> b) -> a -> b
$ Type TyName uni ()
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ())
-> RecursiveType uni fun ()
forall (uni :: * -> *) fun ann.
Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
RecursiveType Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
tree (\[Type TyName uni ()
a] -> [Type TyName uni ()] -> term () -> term ()
forall {uni :: * -> *} {fun} (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapTreeForest [Type TyName uni ()
a, Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
treeTag])
forestData :: RecursiveType uni fun ()
forestData :: forall (uni :: * -> *) fun. RecursiveType uni fun ()
forestData = 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
let RecursiveType Type TyName uni ()
treeForest forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapTreeForest = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeForestData
forest :: Type TyName uni ()
forest = ()
-> 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 ()
asForest Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
treeForest
RecursiveType uni fun () -> Quote (RecursiveType uni fun ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecursiveType uni fun () -> Quote (RecursiveType uni fun ()))
-> RecursiveType uni fun () -> Quote (RecursiveType uni fun ())
forall a b. (a -> b) -> a -> b
$ Type TyName uni ()
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ())
-> RecursiveType uni fun ()
forall (uni :: * -> *) fun ann.
Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
RecursiveType Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
forest (\[Type TyName uni ()
a] -> [Type TyName uni ()] -> term () -> term ()
forall {uni :: * -> *} {fun} (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapTreeForest [Type TyName uni ()
a, Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
forestTag])
treeNode :: HasUniApply uni => Term TyName Name uni fun ()
treeNode :: forall (uni :: * -> *) fun.
HasUniApply uni =>
Term TyName Name uni fun ()
treeNode = 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
$ Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall tyname name (uni :: * -> *) (m :: * -> *) fun ann.
(HasUnique tyname TypeUnique, HasUnique name TermUnique,
MonadNormalizeType uni m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
normalizeTypesIn (Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
let RecursiveType Type TyName uni ()
_ forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapTree = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeData
RecursiveType Type TyName uni ()
forest forall (term :: * -> *).
TermLike term TyName Name uni Any =>
[Type TyName uni ()] -> term () -> term ()
_ = RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
forestData
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
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
Name
fr <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fr"
Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
let vA :: Type TyName uni ()
vA = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
vR :: Type TyName uni ()
vR = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
Normalized Type TyName uni ()
forestA <- Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType (Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
forest Type TyName uni ()
vA
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
. ()
-> 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 Type TyName uni ()
vA
(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
fr Type TyName uni ()
forestA
(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 ()
wrapTree [Type TyName uni ()
vA]
(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 (()
-> [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 () [Type TyName uni ()
vA, Type TyName uni ()
forestA] Type TyName uni ()
vR)
(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
fr
]
forestNil :: HasUniApply uni => Term TyName Name uni fun ()
forestNil :: forall (uni :: * -> *) fun.
HasUniApply uni =>
Term TyName Name uni fun ()
forestNil = 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
$ Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall tyname name (uni :: * -> *) (m :: * -> *) fun ann.
(HasUnique tyname TypeUnique, HasUnique name TermUnique,
MonadNormalizeType uni m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
normalizeTypesIn (Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
let RecursiveType Type TyName uni ()
tree forall (term :: * -> *).
TermLike term TyName Name uni Any =>
[Type TyName uni ()] -> term () -> term ()
_ = RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeData
RecursiveType Type TyName uni ()
forest forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapForest = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
forestData
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 vA :: Type TyName uni ()
vA = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
vR :: Type TyName uni ()
vR = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
Normalized Type TyName uni ()
treeA <- Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType (Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
tree Type TyName uni ()
vA
Normalized Type TyName uni ()
forestA <- Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType (Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
forest Type TyName uni ()
vA
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
. [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 ()
wrapForest [Type TyName uni ()
vA]
(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 Type TyName uni ()
vR
(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 () [Type TyName uni ()
treeA, Type TyName uni ()
forestA] Type TyName uni ()
vR)
(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
forestCons :: HasUniApply uni => Term TyName Name uni fun ()
forestCons :: forall (uni :: * -> *) fun.
HasUniApply uni =>
Term TyName Name uni fun ()
forestCons = 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
$ Term TyName Name uni fun () -> Quote (Term TyName Name uni fun ())
forall tyname name (uni :: * -> *) (m :: * -> *) fun ann.
(HasUnique tyname TypeUnique, HasUnique name TermUnique,
MonadNormalizeType uni m) =>
Term tyname name uni fun ann -> m (Term tyname name uni fun ann)
normalizeTypesIn (Term TyName Name uni fun ()
-> Quote (Term TyName Name uni fun ()))
-> Quote (Term TyName Name uni fun ())
-> Quote (Term TyName Name uni fun ())
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
let RecursiveType Type TyName uni ()
tree forall (term :: * -> *).
TermLike term TyName Name uni Any =>
[Type TyName uni ()] -> term () -> term ()
_ = RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
treeData
RecursiveType Type TyName uni ()
forest forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapForest = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
forestData
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
Name
tr <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"tr"
Name
fr <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fr"
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 vA :: Type TyName uni ()
vA = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
vR :: Type TyName uni ()
vR = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
Normalized Type TyName uni ()
treeA <- Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType (Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
tree Type TyName uni ()
vA
Normalized Type TyName uni ()
forestA <- Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall tyname (uni :: * -> *) (m :: * -> *) ann.
(HasUnique tyname TypeUnique, MonadNormalizeType uni m) =>
Type tyname uni ann -> m (Normalized (Type tyname uni ann))
normalizeType (Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ())))
-> Type TyName uni ()
-> QuoteT Identity (Normalized (Type TyName uni ()))
forall a b. (a -> b) -> a -> b
$ ()
-> 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 ()
forest Type TyName uni ()
vA
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
. ()
-> 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
tr Type TyName uni ()
treeA
(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
fr Type TyName uni ()
forestA
(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 ()
wrapForest [Type TyName uni ()
vA]
(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 Type TyName uni ()
vR
(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 () [Type TyName uni ()
treeA, Type TyName uni ()
forestA] Type TyName uni ()
vR)
(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
tr
, () -> Name -> Term TyName Name uni fun ()
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var () Name
fr
]