{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module PlutusCore.StdLib.Data.List
( list
, MatchOption (..)
, matchList
, foldrList
, foldList
, sum
, sumr
, product
) where
import Prelude hiding (enumFromTo, map, product, reverse, sum)
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Quote
import PlutusCore.StdLib.Data.Function
import PlutusCore.StdLib.Data.MatchOption
import PlutusCore.StdLib.Data.Unit
list :: uni `HasTypeLevel` [] => Type tyname uni ()
list :: forall (uni :: * -> *) tyname.
HasTypeLevel uni [] =>
Type tyname uni ()
list = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @[] ()
matchList :: TermLike term TyName Name DefaultUni DefaultFun => MatchOption -> term ()
matchList :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
matchList MatchOption
optMatch = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
Name
xs <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
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"
Name
u <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"u"
let listA :: Type TyName DefaultUni ()
listA = ()
-> 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
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
funAtXs :: fun -> term ()
funAtXs fun
fun = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall ann. ann -> term ann -> Type TyName uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> fun -> term ()
forall ann. ann -> fun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () fun
fun) (Type TyName uni () -> term ()) -> Type TyName uni () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
xs Type TyName DefaultUni ()
listA
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
z (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
f (()
-> 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 () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> 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 ()
listA (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ case MatchOption
optMatch of
MatchOption
UseCase ->
term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
(term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn (() -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
CaseList)
[ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
, () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
])
[ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
z
, () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f
, () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs
]
MatchOption
UseChoose ->
term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn
(term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn (() -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
ChooseList)
[ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
, ()
-> 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 () =>
Type tyname uni ()
unit (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
])
[ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs
, () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
u Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
z
, () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
u Type TyName DefaultUni ()
forall (uni :: * -> *) tyname.
HasTypeLevel uni () =>
Type tyname uni ()
unit
(term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
[DefaultFun -> term ()
forall {term :: * -> *} {uni :: * -> *} {fun}.
TermLike term TyName Name uni fun =>
fun -> term ()
funAtXs DefaultFun
HeadList, DefaultFun -> term ()
forall {term :: * -> *} {uni :: * -> *} {fun}.
TermLike term TyName Name uni fun =>
fun -> term ()
funAtXs DefaultFun
TailList]
, term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
(TermLike term tyname name uni fun, HasTermLevel uni ()) =>
term ()
unitval
]
foldrList :: TermLike term TyName Name DefaultUni DefaultFun => MatchOption -> term ()
foldrList :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
foldrList MatchOption
optMatch = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
Name
z <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
Name
rec <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
Name
xs <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
Name
xs' <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs'"
let listA :: Type TyName DefaultUni ()
listA = ()
-> 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
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
unwrap' :: () -> term () -> term ()
unwrap' ()
ann = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ()
ann (term () -> term () -> term ())
-> (Type TyName DefaultUni () -> term ())
-> Type TyName DefaultUni ()
-> term ()
-> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> Type TyName DefaultUni () -> term ()
forall ann.
ann -> term ann -> Type TyName DefaultUni ann -> term 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 ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
matchList MatchOption
optMatch) (Type TyName DefaultUni () -> term () -> term ())
-> Type TyName DefaultUni () -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
f (()
-> 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 () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> 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 () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
z (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [Type TyName DefaultUni ()
listA, () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r])
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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 ()
listA (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
xs Type TyName DefaultUni ()
listA
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName DefaultUni () -> term ()
forall ann.
ann -> term ann -> Type TyName DefaultUni ann -> term 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 () -> term ()
forall {term :: * -> *}.
TermLike term TyName Name DefaultUni DefaultFun =>
() -> term () -> term ()
unwrap' () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs)) (Type TyName DefaultUni () -> term ())
-> Type TyName DefaultUni () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
z)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
x (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
xs' Type TyName DefaultUni ()
listA
(term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
[ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
, () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs'
]
foldList :: TermLike term TyName Name DefaultUni DefaultFun => MatchOption -> term ()
foldList :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
foldList MatchOption
optMatch = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"r"
Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
Name
rec <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
Name
z <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"z"
Name
xs <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs"
Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
Name
xs' <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"xs'"
let listA :: Type TyName DefaultUni ()
listA = ()
-> 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
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
unwrap' :: () -> term () -> term ()
unwrap' ()
ann = () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ()
ann (term () -> term () -> term ())
-> (Type TyName DefaultUni () -> term ())
-> Type TyName DefaultUni ()
-> term ()
-> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> Type TyName DefaultUni () -> term ()
forall ann.
ann -> term ann -> Type TyName DefaultUni ann -> term 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 ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
matchList MatchOption
optMatch) (Type TyName DefaultUni () -> term () -> term ())
-> Type TyName DefaultUni () -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(term () -> Quote (term ()))
-> ([term ()] -> term ()) -> [term ()] -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall ann. ann -> TyName -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
f (()
-> 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 () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> 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 () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix [() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r, ()
-> 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 ()
listA (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r])
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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 () (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> 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 ()
listA (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
z (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
xs Type TyName DefaultUni ()
listA
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> term () -> term ()
forall ann. ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName DefaultUni () -> term ()
forall ann.
ann -> term ann -> Type TyName DefaultUni ann -> term 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 () -> term ()
forall {term :: * -> *}.
TermLike term TyName Name DefaultUni DefaultFun =>
() -> term () -> term ()
unwrap' () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs)) (Type TyName DefaultUni () -> term ())
-> Type TyName DefaultUni () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
z)
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
x (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName DefaultUni () -> term () -> term ()
forall ann.
ann -> Name -> Type TyName DefaultUni ann -> term ann -> term 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
xs' Type TyName DefaultUni ()
listA
(term () -> term ())
-> ([term ()] -> term ()) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
rec)
([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f) [() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
z, () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x]
, () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
xs'
]
sum :: TermLike term TyName Name DefaultUni DefaultFun => MatchOption -> term ()
sum :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
sum MatchOption
optMatch = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
let int :: Type tyname DefaultUni ()
int = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
add :: term ()
add = () -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
AddInteger
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(term () -> Quote (term ()))
-> ([term ()] -> term ()) -> [term ()] -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn (MatchOption -> term ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
foldList MatchOption
optMatch) [Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int, Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int])
([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term ()
add , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0]
sumr :: TermLike term TyName Name DefaultUni DefaultFun => MatchOption -> term ()
sumr :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
sumr MatchOption
optMatch = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
let int :: Type tyname DefaultUni ()
int = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
add :: term ()
add = () -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
AddInteger
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(term () -> Quote (term ()))
-> ([term ()] -> term ()) -> [term ()] -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn (MatchOption -> term ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
foldrList MatchOption
optMatch) [Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int, Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int])
([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term ()
add, forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
0 ]
product :: TermLike term TyName Name DefaultUni DefaultFun => MatchOption -> term ()
product :: forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
product MatchOption
optMatch = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
let int :: Type tyname DefaultUni ()
int = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @Integer ()
mul :: term ()
mul = () -> DefaultFun -> term ()
forall ann. ann -> DefaultFun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin () DefaultFun
MultiplyInteger
term () -> Quote (term ())
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(term () -> Quote (term ()))
-> ([term ()] -> term ()) -> [term ()] -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (term () -> [Type TyName DefaultUni ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn (MatchOption -> term ()
forall (term :: * -> *).
TermLike term TyName Name DefaultUni DefaultFun =>
MatchOption -> term ()
foldList MatchOption
optMatch) [Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int, Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
int])
([term ()] -> Quote (term ())) -> [term ()] -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ [ term ()
mul , forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant @Integer () Integer
1]