{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TupleSections #-}
module PlutusCore.StdLib.Type
( RecursiveType (..)
, makeRecursiveType
) where
import PlutusPrelude
import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.Quote
data RecursiveType uni fun ann = RecursiveType
{ forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType :: Type TyName uni ann
, forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann
-> forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann
_recursiveWrap :: forall term . TermLike term TyName Name uni fun
=> [Type TyName uni ann] -> term ann -> term ann
}
data IndicesLengthsMismatchException = IndicesLengthsMismatchException
{ IndicesLengthsMismatchException -> Int
_indicesLengthsMismatchExceptionExpected :: Int
, IndicesLengthsMismatchException -> Int
_indicesLengthsMismatchExceptionActual :: Int
, IndicesLengthsMismatchException -> TyName
_indicesLengthsMismatchExceptionTyName :: TyName
} deriving anyclass (Show IndicesLengthsMismatchException
Typeable IndicesLengthsMismatchException
(Typeable IndicesLengthsMismatchException,
Show IndicesLengthsMismatchException) =>
(IndicesLengthsMismatchException -> SomeException)
-> (SomeException -> Maybe IndicesLengthsMismatchException)
-> (IndicesLengthsMismatchException -> String)
-> Exception IndicesLengthsMismatchException
SomeException -> Maybe IndicesLengthsMismatchException
IndicesLengthsMismatchException -> String
IndicesLengthsMismatchException -> SomeException
forall e.
(Typeable e, Show e) =>
(e -> SomeException)
-> (SomeException -> Maybe e) -> (e -> String) -> Exception e
$ctoException :: IndicesLengthsMismatchException -> SomeException
toException :: IndicesLengthsMismatchException -> SomeException
$cfromException :: SomeException -> Maybe IndicesLengthsMismatchException
fromException :: SomeException -> Maybe IndicesLengthsMismatchException
$cdisplayException :: IndicesLengthsMismatchException -> String
displayException :: IndicesLengthsMismatchException -> String
Exception)
instance Show IndicesLengthsMismatchException where
show :: IndicesLengthsMismatchException -> String
show (IndicesLengthsMismatchException Int
expected Int
actual TyName
tyName) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ String
"Wrong number of elements\n"
, String
"expected: ", Int -> String
forall a. Show a => a -> String
show Int
expected, String
" , actual: ", Int -> String
forall a. Show a => a -> String
show Int
actual, String
"\n"
, String
"while constructing a ", TyName -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc TyName
tyName
]
argKindsToDataKindN :: ann -> [Kind ann] -> Kind ann
argKindsToDataKindN :: forall ann. ann -> [Kind ann] -> Kind ann
argKindsToDataKindN ann
ann [Kind ann]
argKinds = ann -> [Kind ann] -> Kind ann -> Kind ann
forall ann. ann -> [Kind ann] -> Kind ann -> Kind ann
mkIterKindArrow ann
ann [Kind ann]
argKinds (Kind ann -> Kind ann) -> Kind ann -> Kind ann
forall a b. (a -> b) -> a -> b
$ ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann
dataKindToSpineKind :: ann -> Kind ann -> Kind ann
dataKindToSpineKind :: forall ann. ann -> Kind ann -> Kind ann
dataKindToSpineKind ann
ann Kind ann
dataKind = ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann Kind ann
dataKind (Kind ann -> Kind ann) -> Kind ann -> Kind ann
forall a b. (a -> b) -> a -> b
$ ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann
spineKindToRecKind :: ann -> Kind ann -> Kind ann
spineKindToRecKind :: forall ann. ann -> Kind ann -> Kind ann
spineKindToRecKind ann
ann Kind ann
spineKind = ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann Kind ann
spineKind (Kind ann -> Kind ann) -> Kind ann -> Kind ann
forall a b. (a -> b) -> a -> b
$ ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann
getToSpine :: ann -> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
getToSpine :: forall ann (uni :: * -> *).
ann -> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
getToSpine ann
ann = do
TyName
dat <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"dat"
([TyDecl TyName uni ann] -> Type TyName uni ann)
-> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (([TyDecl TyName uni ann] -> Type TyName uni ann)
-> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann))
-> ([TyDecl TyName uni ann] -> Type TyName uni ann)
-> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ \[TyDecl TyName uni ann]
args ->
ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
dat (ann -> [Kind ann] -> Kind ann
forall ann. ann -> [Kind ann] -> Kind ann
argKindsToDataKindN ann
ann ([Kind ann] -> Kind ann) -> [Kind ann] -> Kind ann
forall a b. (a -> b) -> a -> b
$ (TyDecl TyName uni ann -> Kind ann)
-> [TyDecl TyName uni ann] -> [Kind ann]
forall a b. (a -> b) -> [a] -> [b]
map TyDecl TyName uni ann -> Kind ann
forall tyname (uni :: * -> *) ann.
TyDecl tyname uni ann -> Kind ann
_tyDeclKind [TyDecl TyName uni ann]
args)
(Type TyName uni ann -> Type TyName uni ann)
-> ([(ann, Type TyName uni ann)] -> Type TyName uni ann)
-> [(ann, Type TyName uni ann)]
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type TyName uni ann
-> [(ann, Type TyName uni ann)] -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyApp (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
dat)
([(ann, Type TyName uni ann)] -> Type TyName uni ann)
-> [(ann, Type TyName uni ann)] -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ (TyDecl TyName uni ann -> (ann, Type TyName uni ann))
-> [TyDecl TyName uni ann] -> [(ann, Type TyName uni ann)]
forall a b. (a -> b) -> [a] -> [b]
map ((ann
ann,) (Type TyName uni ann -> (ann, Type TyName uni ann))
-> (TyDecl TyName uni ann -> Type TyName uni ann)
-> TyDecl TyName uni ann
-> (ann, Type TyName uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyDecl TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
TyDecl tyname uni ann -> Type tyname uni ann
_tyDeclType) [TyDecl TyName uni ann]
args
getSpine :: ann -> [TyDecl TyName uni ann] -> Quote (Type TyName uni ann)
getSpine :: forall ann (uni :: * -> *).
ann -> [TyDecl TyName uni ann] -> Quote (Type TyName uni ann)
getSpine ann
ann [TyDecl TyName uni ann]
args = (([TyDecl TyName uni ann] -> Type TyName uni ann)
-> [TyDecl TyName uni ann] -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ [TyDecl TyName uni ann]
args) (([TyDecl TyName uni ann] -> Type TyName uni ann)
-> Type TyName uni ann)
-> QuoteT Identity ([TyDecl TyName uni ann] -> Type TyName uni ann)
-> QuoteT Identity (Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ann
-> QuoteT Identity ([TyDecl TyName uni ann] -> Type TyName uni ann)
forall ann (uni :: * -> *).
ann -> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
getToSpine ann
ann
getWithSpine
:: ann
-> [TyVarDecl TyName ann]
-> Quote ((Type TyName uni ann -> Type TyName uni ann) -> Type TyName uni ann)
getWithSpine :: forall ann (uni :: * -> *).
ann
-> [TyVarDecl TyName ann]
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
getWithSpine ann
ann [TyVarDecl TyName ann]
argVars = do
Type TyName uni ann
spine <- ann -> [TyDecl TyName uni ann] -> Quote (Type TyName uni ann)
forall ann (uni :: * -> *).
ann -> [TyDecl TyName uni ann] -> Quote (Type TyName uni ann)
getSpine ann
ann ([TyDecl TyName uni ann] -> Quote (Type TyName uni ann))
-> [TyDecl TyName uni ann] -> Quote (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ (TyVarDecl TyName ann -> TyDecl TyName uni ann)
-> [TyVarDecl TyName ann] -> [TyDecl TyName uni ann]
forall a b. (a -> b) -> [a] -> [b]
map TyVarDecl TyName ann -> TyDecl TyName uni ann
forall tyname ann (uni :: * -> *).
TyVarDecl tyname ann -> TyDecl tyname uni ann
tyDeclVar [TyVarDecl TyName ann]
argVars
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann))
-> ((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ \Type TyName uni ann -> Type TyName uni ann
k -> [TyVarDecl TyName ann]
-> Type TyName uni ann -> Type TyName uni ann
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam [TyVarDecl TyName ann]
argVars (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann -> Type TyName uni ann
k Type TyName uni ann
spine
type FromDataPieces uni ann a
= ann
-> TyName
-> [TyVarDecl TyName ann]
-> Type TyName uni ann
-> Quote a
packPatternFunctorBodyN :: FromDataPieces uni ann (Type TyName uni ann)
packPatternFunctorBodyN :: forall (uni :: * -> *) ann.
FromDataPieces uni ann (Type TyName uni ann)
packPatternFunctorBodyN ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN = do
let dataKind :: Kind ann
dataKind = ann -> [Kind ann] -> Kind ann
forall ann. ann -> [Kind ann] -> Kind ann
argKindsToDataKindN ann
ann ([Kind ann] -> Kind ann) -> [Kind ann] -> Kind ann
forall a b. (a -> b) -> a -> b
$ (TyVarDecl TyName ann -> Kind ann)
-> [TyVarDecl TyName ann] -> [Kind ann]
forall a b. (a -> b) -> [a] -> [b]
map TyVarDecl TyName ann -> Kind ann
forall tyname ann. TyVarDecl tyname ann -> Kind ann
_tyVarDeclKind [TyVarDecl TyName ann]
argVars
spineKind :: Kind ann
spineKind = ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann
dataKindToSpineKind ann
ann Kind ann
dataKind
recKind :: Kind ann
recKind = ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann
spineKindToRecKind ann
ann Kind ann
spineKind
vDat :: TyVarDecl TyName ann
vDat = ann -> TyName -> Kind ann -> TyVarDecl TyName ann
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl ann
ann TyName
dataName Kind ann
dataKind
patN :: Type TyName uni ann
patN = [TyVarDecl TyName ann]
-> Type TyName uni ann -> Type TyName uni ann
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam (TyVarDecl TyName ann
vDat TyVarDecl TyName ann
-> [TyVarDecl TyName ann] -> [TyVarDecl TyName ann]
forall a. a -> [a] -> [a]
: [TyVarDecl TyName ann]
argVars) Type TyName uni ann
patBodyN
(Type TyName uni ann -> Type TyName uni ann) -> Type TyName uni ann
withSpine <- ann
-> [TyVarDecl TyName ann]
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
forall ann (uni :: * -> *).
ann
-> [TyVarDecl TyName ann]
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
getWithSpine ann
ann [TyVarDecl TyName ann]
argVars
TyName
rec <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"rec"
TyName
spine <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"spine"
Type TyName uni ann -> Quote (Type TyName uni ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
(Type TyName uni ann -> Quote (Type TyName uni ann))
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Quote (Type TyName uni ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
rec Kind ann
recKind
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
spine Kind ann
spineKind
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
spine)
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann Type TyName uni ann
patN
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type TyName uni ann -> Type TyName uni ann) -> Type TyName uni ann
withSpine
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
-> (Type TyName uni ann
-> Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann
(Type TyName uni ann -> Quote (Type TyName uni ann))
-> Type TyName uni ann -> Quote (Type TyName uni ann)
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
rec
getPackedType :: FromDataPieces uni ann (Type TyName uni ann)
getPackedType :: forall (uni :: * -> *) ann.
FromDataPieces uni ann (Type TyName uni ann)
getPackedType ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN = do
(Type TyName uni ann -> Type TyName uni ann) -> Type TyName uni ann
withSpine <- ann
-> [TyVarDecl TyName ann]
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
forall ann (uni :: * -> *).
ann
-> [TyVarDecl TyName ann]
-> Quote
((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
getWithSpine ann
ann [TyVarDecl TyName ann]
argVars
(Type TyName uni ann -> Type TyName uni ann) -> Type TyName uni ann
withSpine ((Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann)
-> (Type TyName uni ann
-> Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann (Type TyName uni ann -> Type TyName uni ann)
-> Quote (Type TyName uni ann) -> Quote (Type TyName uni ann)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FromDataPieces uni ann (Type TyName uni ann)
forall (uni :: * -> *) ann.
FromDataPieces uni ann (Type TyName uni ann)
packPatternFunctorBodyN ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN
newtype PolyWrap uni fun ann = PolyWrap
(forall term. TermLike term TyName Name uni fun => [Type TyName uni ann] -> term ann -> term ann)
getPackedWrap :: FromDataPieces uni ann (PolyWrap uni fun ann)
getPackedWrap :: forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (PolyWrap uni fun ann)
getPackedWrap ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN = do
Type TyName uni ann
pat1 <- FromDataPieces uni ann (Type TyName uni ann)
forall (uni :: * -> *) ann.
FromDataPieces uni ann (Type TyName uni ann)
packPatternFunctorBodyN ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN
[TyDecl TyName uni ann] -> Type TyName uni ann
toSpine <- ann -> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
forall ann (uni :: * -> *).
ann -> Quote ([TyDecl TyName uni ann] -> Type TyName uni ann)
getToSpine ann
ann
let instVar :: TyVarDecl tyname ann
-> Type tyname uni ann -> TyDecl tyname uni ann
instVar TyVarDecl tyname ann
v Type tyname uni ann
ty = ann -> Type tyname uni ann -> Kind ann -> TyDecl tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> Type tyname uni ann -> Kind ann -> TyDecl tyname uni ann
TyDecl ann
ann Type tyname uni ann
ty (Kind ann -> TyDecl tyname uni ann)
-> Kind ann -> TyDecl tyname uni ann
forall a b. (a -> b) -> a -> b
$ TyVarDecl tyname ann -> Kind ann
forall tyname ann. TyVarDecl tyname ann -> Kind ann
_tyVarDeclKind TyVarDecl tyname ann
v
PolyWrap uni fun ann -> Quote (PolyWrap uni fun ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (PolyWrap uni fun ann -> Quote (PolyWrap uni fun ann))
-> PolyWrap uni fun ann -> Quote (PolyWrap uni fun ann)
forall a b. (a -> b) -> a -> b
$ (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> PolyWrap uni fun ann
forall (uni :: * -> *) fun ann.
(forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> PolyWrap uni fun ann
PolyWrap ((forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> PolyWrap uni fun ann)
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> PolyWrap uni fun ann
forall a b. (a -> b) -> a -> b
$ \[Type TyName uni ann]
args ->
let argVarsLen :: Int
argVarsLen = [TyVarDecl TyName ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TyVarDecl TyName ann]
argVars
argsLen :: Int
argsLen = [Type TyName uni ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type TyName uni ann]
args
in if Int
argVarsLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
argsLen
then ann
-> Type TyName uni ann
-> Type TyName uni ann
-> term ann
-> term ann
forall ann.
ann
-> Type TyName uni ann
-> Type TyName uni ann
-> term ann
-> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> term ann
-> term ann
iWrap ann
ann Type TyName uni ann
pat1 (Type TyName uni ann -> term ann -> term ann)
-> ([TyDecl TyName uni ann] -> Type TyName uni ann)
-> [TyDecl TyName uni ann]
-> term ann
-> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [TyDecl TyName uni ann] -> Type TyName uni ann
toSpine ([TyDecl TyName uni ann] -> term ann -> term ann)
-> [TyDecl TyName uni ann] -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ (TyVarDecl TyName ann
-> Type TyName uni ann -> TyDecl TyName uni ann)
-> [TyVarDecl TyName ann]
-> [Type TyName uni ann]
-> [TyDecl TyName uni ann]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TyVarDecl TyName ann
-> Type TyName uni ann -> TyDecl TyName uni ann
forall {tyname} {tyname} {uni :: * -> *}.
TyVarDecl tyname ann
-> Type tyname uni ann -> TyDecl tyname uni ann
instVar [TyVarDecl TyName ann]
argVars [Type TyName uni ann]
args
else IndicesLengthsMismatchException -> term ann -> term ann
forall a e. Exception e => e -> a
throw (IndicesLengthsMismatchException -> term ann -> term ann)
-> (TyName -> IndicesLengthsMismatchException)
-> TyName
-> term ann
-> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> TyName -> IndicesLengthsMismatchException
IndicesLengthsMismatchException Int
argVarsLen Int
argsLen (TyName -> term ann -> term ann) -> TyName -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ TyName
dataName
makeRecursiveType0
:: ann
-> TyName
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
makeRecursiveType0 :: forall ann (uni :: * -> *) fun.
ann
-> TyName
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
makeRecursiveType0 ann
ann TyName
dataName Type TyName uni ann
patBody0 = do
TyName
rec <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"rec"
TyName
f <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"f"
let argKind :: Kind ann
argKind = ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (Kind ann -> Kind ann) -> Kind ann -> Kind ann
forall a b. (a -> b) -> a -> b
$ ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann
recKind :: Kind ann
recKind = ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann Kind ann
argKind (Kind ann -> Kind ann) -> Kind ann -> Kind ann
forall a b. (a -> b) -> a -> b
$ ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann
pat1 :: Type TyName uni ann
pat1
= ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
rec Kind ann
recKind
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
f Kind ann
argKind
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
f)
(Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
rec)
(Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
f
arg :: Type TyName uni ann
arg = ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
dataName (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) Type TyName uni ann
patBody0
recType :: Type TyName uni ann
recType = ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann Type TyName uni ann
forall {uni :: * -> *}. Type TyName uni ann
pat1 Type TyName uni ann
arg
wrap :: [a] -> term ann -> term ann
wrap [a]
args = case [a]
args of
[] -> ann
-> Type TyName uni ann
-> Type TyName uni ann
-> term ann
-> term ann
forall ann.
ann
-> Type TyName uni ann
-> Type TyName uni ann
-> term ann
-> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> term ann
-> term ann
iWrap ann
ann Type TyName uni ann
forall {uni :: * -> *}. Type TyName uni ann
pat1 Type TyName uni ann
arg
[a]
_ -> IndicesLengthsMismatchException -> term ann -> term ann
forall a e. Exception e => e -> a
throw (IndicesLengthsMismatchException -> term ann -> term ann)
-> (TyName -> IndicesLengthsMismatchException)
-> TyName
-> term ann
-> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> TyName -> IndicesLengthsMismatchException
IndicesLengthsMismatchException Int
0 ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
args) (TyName -> term ann -> term ann) -> TyName -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ TyName
dataName
RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann))
-> RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann)
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
forall (uni :: * -> *) fun ann.
Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
RecursiveType Type TyName uni ann
recType [Type TyName uni ann] -> term ann -> term ann
forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann
forall {term :: * -> *} {name} {fun} {a}.
TermLike term TyName name uni fun =>
[a] -> term ann -> term ann
wrap
makeRecursiveType1
:: ann
-> TyName
-> TyVarDecl TyName ann
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
makeRecursiveType1 :: forall ann (uni :: * -> *) fun.
ann
-> TyName
-> TyVarDecl TyName ann
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
makeRecursiveType1 ann
ann TyName
dataName TyVarDecl TyName ann
argVar Type TyName uni ann
patBody1 = do
let varName :: TyName
varName = TyVarDecl TyName ann -> TyName
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName TyVarDecl TyName ann
argVar
varKind :: Kind ann
varKind = TyVarDecl TyName ann -> Kind ann
forall tyname ann. TyVarDecl tyname ann -> Kind ann
_tyVarDeclKind TyVarDecl TyName ann
argVar
TyName
varName' <- TyName -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => TyName -> m TyName
freshenTyName TyName
varName
let
recKind :: Kind ann
recKind = ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann Kind ann
varKind (Kind ann -> Kind ann) -> Kind ann -> Kind ann
forall a b. (a -> b) -> a -> b
$ ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann
pat1 :: Type TyName uni ann
pat1 = ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
dataName Kind ann
recKind (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
varName Kind ann
varKind Type TyName uni ann
patBody1
recType :: Type TyName uni ann
recType = ann
-> TyName -> Kind ann -> Type TyName uni ann -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann TyName
varName' Kind ann
varKind (Type TyName uni ann -> Type TyName uni ann)
-> (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann
-> Type TyName uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann
-> Type TyName uni ann
-> Type TyName uni ann
-> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix ann
ann Type TyName uni ann
pat1 (Type TyName uni ann -> Type TyName uni ann)
-> Type TyName uni ann -> Type TyName uni ann
forall a b. (a -> b) -> a -> b
$ ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
varName'
wrap :: [Type TyName uni ann] -> term ann -> term ann
wrap [Type TyName uni ann]
args = case [Type TyName uni ann]
args of
[Type TyName uni ann
arg] -> ann
-> Type TyName uni ann
-> Type TyName uni ann
-> term ann
-> term ann
forall ann.
ann
-> Type TyName uni ann
-> Type TyName uni ann
-> term ann
-> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> term ann
-> term ann
iWrap ann
ann Type TyName uni ann
pat1 Type TyName uni ann
arg
[Type TyName uni ann]
_ -> IndicesLengthsMismatchException -> term ann -> term ann
forall a e. Exception e => e -> a
throw (IndicesLengthsMismatchException -> term ann -> term ann)
-> (TyName -> IndicesLengthsMismatchException)
-> TyName
-> term ann
-> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> TyName -> IndicesLengthsMismatchException
IndicesLengthsMismatchException Int
1 ([Type TyName uni ann] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type TyName uni ann]
args) (TyName -> term ann -> term ann) -> TyName -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ TyName
dataName
RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann))
-> RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann)
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
forall (uni :: * -> *) fun ann.
Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
RecursiveType Type TyName uni ann
recType [Type TyName uni ann] -> term ann -> term ann
forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann
forall {term :: * -> *} {name} {fun}.
TermLike term TyName name uni fun =>
[Type TyName uni ann] -> term ann -> term ann
wrap
makeRecursiveTypeN :: FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveTypeN :: forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveTypeN ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN = do
Type TyName uni ann
recType <- FromDataPieces uni ann (Type TyName uni ann)
forall (uni :: * -> *) ann.
FromDataPieces uni ann (Type TyName uni ann)
getPackedType ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN
PolyWrap forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann
wrap <- FromDataPieces uni ann (PolyWrap uni fun ann)
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (PolyWrap uni fun ann)
getPackedWrap ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars Type TyName uni ann
patBodyN
RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann)
forall a. a -> QuoteT Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann))
-> RecursiveType uni fun ann -> Quote (RecursiveType uni fun ann)
forall a b. (a -> b) -> a -> b
$ Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
forall (uni :: * -> *) fun ann.
Type TyName uni ann
-> (forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann)
-> RecursiveType uni fun ann
RecursiveType Type TyName uni ann
recType [Type TyName uni ann] -> term ann -> term ann
forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> term ann
wrap
makeRecursiveType :: FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveType :: forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveType ann
ann TyName
dataName [] = ann
-> TyName
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
forall ann (uni :: * -> *) fun.
ann
-> TyName
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
makeRecursiveType0 ann
ann TyName
dataName
makeRecursiveType ann
ann TyName
dataName [TyVarDecl TyName ann
argVar] = ann
-> TyName
-> TyVarDecl TyName ann
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
forall ann (uni :: * -> *) fun.
ann
-> TyName
-> TyVarDecl TyName ann
-> Type TyName uni ann
-> Quote (RecursiveType uni fun ann)
makeRecursiveType1 ann
ann TyName
dataName TyVarDecl TyName ann
argVar
makeRecursiveType ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars = FromDataPieces uni ann (RecursiveType uni fun ann)
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveTypeN ann
ann TyName
dataName [TyVarDecl TyName ann]
argVars