{-# 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

{- Note [Tree]
Here we encode the following:

    mutual
      data Tree (A : Set) : Set where
        node : A -> Forest A -> Tree A

      data Forest (A : Set) : Set where
        nil  : Forest A
        cons : Tree A -> Forest A -> Forest A

    mutual
      mapTree : ∀ A B -> (A -> B) -> Tree A -> Tree B
      mapTree A B f (node x forest) = node (f x) (mapForest A B f forest)

      mapForest : ∀ A B -> (A -> B) -> Forest A -> Forest B
      mapForest A B f  nil               = nil
      mapForest A B f (cons rose forest) = cons (mapTree A B f rose) (mapForest A B f forest)

using this representation:

    {-# OPTIONS_GHC --type-in-type #-}

    {-# NO_POSITIVITY_CHECK #-}
    data IFix {A : Set} (F : (A -> Set) -> A -> Set) (x : A) : Set where
      wrap : F (IFix F) x -> IFix F x

    Fix₂ : ∀ {A B} -> ((A -> B -> Set) -> A -> B -> Set) -> A -> B -> Set
    Fix₂ F x y = IFix (λ B P -> P (F λ x y -> B λ R -> R x y)) (λ R -> R x y)

    treeTag : Set -> Set -> Set
    treeTag T F = T

    forestTag : Set -> Set -> Set
    forestTag T F = F

    AsTree : (Set -> (Set -> Set -> Set) -> Set) -> Set -> Set
    AsTree D A = D A treeTag

    AsForest : (Set -> (Set -> Set -> Set) -> Set) -> Set -> Set
    AsForest D A = D A forestTag

    TreeForest : Set -> (Set -> Set -> Set) -> Set
    TreeForest =
      Fix₂ λ Rec A tag ->
      ∀ R ->
        tag ((A -> AsForest Rec A -> R) -> R) (R -> (AsTree Rec A -> AsForest Rec A -> R) -> R)

    Tree : Set -> Set
    Tree = AsTree TreeForest

    Forest : Set -> Set
    Forest = AsForest TreeForest
-}

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])

-- |
--
-- > /\(a :: *) -> \(x : a) (fr : forest a) ->
-- >     wrapTree [a] /\(r :: *) -> \(f : a -> forest a -> r) -> f x fr
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
            ]

-- |
--
-- > /\(a :: *) ->
-- >     wrapForest [a] /\(r :: *) -> \(z : r) (f : tree a -> forest a -> r) -> z
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

-- |
--
-- > /\(a :: *) -> \(tr : tree a) (fr : forest a)
-- >     wrapForest [a] /\(r :: *) -> \(z : r) (f : tree a -> forest a -> r) -> f tr fr
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
            ]