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

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

import PlutusCore.Core
import PlutusCore.Data as Data
import PlutusCore.Default
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
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.StdLib.Data.Unit

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) ->
-- >              matchData
-- >                  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 :: MatchOption -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
ofoldrData :: MatchOption
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
ofoldrData MatchOption
optMatch = Quote
  (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a. Quote a -> a
runQuote (Quote
   (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
 -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a b. (a -> b) -> a -> b
$ do
    let r :: Type tyname DefaultUni ()
r = Type tyname DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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 = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
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 :: * -> *) tyname.
HasTypeLevel uni [] =>
Type tyname uni ()
list Type tyname DefaultUni ()
forall {tyname}. 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 tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn Type tyname uni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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 ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
-> Term TyName Name DefaultUni (Either DefaultFun b) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ()
ann (Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ()
 -> Term TyName Name DefaultUni (Either DefaultFun b) ())
-> 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 (MatchOption -> Term TyName Name DefaultUni DefaultFun ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
matchData MatchOption
optMatch)
    Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Quote
      (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
    -> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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.
HasTypeLevel 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 ()
forall {tyname}. Type tyname DefaultUni ()
listR Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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 :: * -> *) tyname.
HasTypeLevel uni [] =>
Type tyname uni ()
list (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {uni :: * -> *} {tyname}.
KnownTypeAst Void uni (ElaborateBuiltin uni (,)) =>
Type tyname uni () -> Type tyname uni ()
opair Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
r) Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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 ()
forall {tyname}. Type tyname DefaultUni ()
listR Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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.
HasTypeLevel uni Integer =>
Type tyname uni ()
integer Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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 () (forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @ByteString ()) Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> [Type TyName DefaultUni ()]
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Data =>
Type tyname uni ()
dataTy, Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
rec (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Data =>
Type tyname uni ()
dataTy Type TyName DefaultUni ()
forall {tyname}. 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
d Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall {b}.
()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
-> Term TyName Name DefaultUni (Either DefaultFun b) ()
unwrap' () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
d)) Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
r)
            [   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
i Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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 ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fConstr)
                  [ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (MatchOption
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList MatchOption
optMatch) Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Data =>
Type tyname uni ()
dataTy)
                      [()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec, ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
ds]
                  ]
            ,   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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 :: * -> *) tyname.
HasTypeLevel uni [] =>
Type tyname uni ()
list (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {uni :: * -> *} {tyname}.
KnownTypeAst Void uni (ElaborateBuiltin uni (,)) =>
Type tyname uni () -> Type tyname uni ()
opair Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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 ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (MatchOption
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList MatchOption
optMatch) (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 :: * -> *} {tyname}.
KnownTypeAst Void uni (ElaborateBuiltin uni (,)) =>
Type tyname uni () -> Type tyname uni ()
opair Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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 ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall (term :: * -> *).
TermLike
  term TyName Name DefaultUni (Either DefaultFun ExtensionFun) =>
term ()
obothPair Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel 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 ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec
                  , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
es
                  ]
            ,   ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
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 ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (MatchOption
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
omapList MatchOption
optMatch) Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni Data =>
Type tyname uni ()
dataTy)
                  [ ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec
                  , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
ds
                  ]
            , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fI
            , ()
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall ann.
ann
-> Name
-> Term TyName Name DefaultUni (Either DefaultFun ExtensionFun) ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fB
            ]

-- | Just a random 'Data' object.
exampleData :: Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
exampleData :: forall tyname.
Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
exampleData = 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
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
-> Quote
     (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
        (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Quote
      (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> (Data
    -> Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Data
-> Quote
     (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VarDecl tyname Name 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 =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs (Int
-> VarDecl tyname Name DefaultUni ()
-> [VarDecl tyname Name DefaultUni ()]
forall a. Int -> a -> [a]
replicate Int
4 (VarDecl tyname Name DefaultUni ()
 -> [VarDecl tyname Name DefaultUni ()])
-> VarDecl tyname Name DefaultUni ()
-> [VarDecl tyname Name DefaultUni ()]
forall a b. (a -> b) -> a -> b
$ ()
-> Name
-> Type tyname DefaultUni ()
-> VarDecl tyname Name DefaultUni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
x Type tyname DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit)
        (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
 -> Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> (Data
    -> Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ())
-> Data
-> Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Data
-> Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ()
        (Data
 -> Quote
      (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ()))
-> Data
-> Quote
     (Term tyname Name DefaultUni (Either DefaultFun ExtensionFun) ())
forall a b. (a -> b) -> a -> b
$ Integer -> [Data] -> Data
Data.Constr Integer
1
            [ [(Data, Data)] -> Data
Map
                [ ( ByteString -> Data
B ByteString
"abcdef"
                  , Integer -> [Data] -> Data
Data.Constr Integer
2
                      [ ByteString -> Data
B ByteString
""
                      , Integer -> Data
I Integer
0
                      ]
                  )
                ]
            , [Data] -> Data
List [[Data] -> Data
List [[Data] -> Data
List [[Data] -> Data
List [Integer -> Data
I Integer
123456]], ByteString -> Data
B ByteString
"ffffffffffffffffffffffffffffffffffffffffff"]]
            , Integer -> Data
I Integer
42
            ]