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

module PlutusCore.Examples.Data.Data
    ( ofoldrData
    ) where

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

import PlutusCore.StdLib.Data.Data
import PlutusCore.StdLib.Data.Function
import PlutusCore.StdLib.Data.Integer
import PlutusCore.StdLib.Data.List
import PlutusCore.StdLib.Data.Pair

import PlutusCore.Examples.Builtins
import PlutusCore.Examples.Data.List
import PlutusCore.Examples.Data.Pair

import Data.ByteString (ByteString)

-- | Right-folding over 'Data' inside PLC currently hardcoded to only ever return @Data@ as a
-- result, 'cause we need to be able to map built-in lists and pairs in the definition of the
-- right fold for 'Data' and we can only do that monomorphically
-- (see Note [Representable built-in functions over polymorphic built-in types]),
-- which forces us to always return a 'Data'.
-- Alternatively we could convert built-in lists and pairs to their non-built-in
-- Scott/Church-encoded forms, map polymorphically and convert back at the call site, but we really
-- only use this definition as a test, so it's fine to make it overly specific for the sake of
-- keeping the actual test trivial.
--
-- > metaTypeLet r = data in
-- >     \(fConstr : integer -> list r -> r)
-- >      (fMap : list (pair r r) -> r)
-- >      (fList : list r -> r)
-- >      (fI : integer -> r)
-- >      (fB : bytestring -> r) ->
-- >          fix {data} {r} \(rec : data -> r) (d : data) ->
-- >              caseData
-- >                  d
-- >                  {r}
-- >                  (\(i : integer) (ds : list data) -> fConstr i (omapList {data} rec ds)
-- >                  (\(es : list (pair data data)) ->
-- >                      fMap (omapList {pair data data} (obothPair {data} rec) es))
-- >                  (\(ds : list data) -> fList (omapList {data} rec ds))
-- >                  fI
-- >                  fB
ofoldrData :: Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
ofoldrData :: Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
ofoldrData = Quote
  (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a. Quote a -> a
runQuote (Quote
   (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ do
    let r :: Type TyName DefaultUni ()
r = Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy
    Name
fConstr <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fConstr"
    Name
fMap    <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fMap"
    Name
fList   <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fList"
    Name
fI      <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fI"
    Name
fB      <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fB"
    Name
rec     <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Name
d       <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"d"
    Name
i       <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"i"
    Name
ds      <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"ds"
    Name
es      <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"es"
    let listData :: Type tyname DefaultUni ()
listData = () -> Type tyname DefaultUni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @[Data] ()
        listR :: Type TyName DefaultUni ()
listR = ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni [] => Type TyName uni ()
list Type TyName DefaultUni ()
r
        opair :: Type TyName uni () -> Type TyName uni ()
opair Type TyName uni ()
a = ()
-> 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
mkIterTyApp () Type TyName uni ()
forall (uni :: * -> *). Contains uni (,) => Type TyName uni ()
pair [Type TyName uni ()
a, Type TyName uni ()
a]
        unwrap' :: ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
unwrap' ()
ann = ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ()
ann (Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ())
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall a b. (a -> b) -> a -> b
$ (DefaultFun -> Either DefaultFun b)
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
forall fun fun' tyname name (uni :: * -> *) ann.
(fun -> fun')
-> Term tyname name uni fun ann -> Term tyname name uni fun' ann
mapFun DefaultFun -> Either DefaultFun b
forall a b. a -> Either a b
Left Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
term ()
caseData
    Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Quote
      (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fConstr (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
Includes uni Integer =>
Type tyname uni ()
integer (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
listR Type TyName DefaultUni ()
r)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fMap (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni [] => Type TyName uni ()
list (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall (uni :: * -> *).
Contains uni (,) =>
Type TyName uni () -> Type TyName uni ()
opair Type TyName DefaultUni ()
r) Type TyName DefaultUni ()
r)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fList (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
listR Type TyName DefaultUni ()
r)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fI (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
Includes uni Integer =>
Type tyname uni ()
integer Type TyName DefaultUni ()
r)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fB (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> Type TyName DefaultUni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
Contains uni a =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @ByteString ()) Type TyName DefaultUni ()
r)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst () Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy, Type TyName DefaultUni ()
r])
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
rec (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy Type TyName DefaultUni ()
r)
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
d Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Quote
      (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Term
      TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b.
()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
unwrap' () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
d)) Type TyName DefaultUni ()
r)
            [   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
i Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
Includes uni Integer =>
Type tyname uni ()
integer
              (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
ds Type TyName DefaultUni ()
forall tyname. Type tyname DefaultUni ()
listData
              (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Term
      TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fConstr)
                  [ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
i
                  , ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Term
      TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy) [()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec, ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
ds]
                  ]
            ,   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
es (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni [] => Type TyName uni ()
list (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall (uni :: * -> *).
Contains uni (,) =>
Type TyName uni () -> Type TyName uni ()
opair Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy)
              (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fMap)
              (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Term
      TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall (uni :: * -> *).
Contains uni (,) =>
Type TyName uni () -> Type TyName uni ()
opair Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy)
                  [ ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *).
TermLike
  term TyName Name DefaultUni (Either DefaultFun ExtensionFun) =>
term ()
obothPair Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy) (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec
                  , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
es
                  ]
            ,   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
ds Type TyName DefaultUni ()
forall tyname. Type tyname DefaultUni ()
listData
              (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fList)
              (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Term
      TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList Type TyName DefaultUni ()
forall (uni :: * -> *). Contains uni Data => Type TyName uni ()
dataTy)
                  [ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec
                  , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
ds
                  ]
            , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fI
            , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fB
            ]