{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
module PlutusIR.Generators.QuickCheck.ShrinkTerms where
import PlutusPrelude
import PlutusIR.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.ShrinkTypes
import PlutusCore.Generators.QuickCheck.Substitutions
import PlutusCore.Generators.QuickCheck.Utils
import PlutusCore.Builtin
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1 (offchain_zero)
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2 (offchain_zero)
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing (identityMlResult)
import PlutusCore.Data
import PlutusCore.Default
import PlutusCore.MkPlc (mkConstantOf, mkTyBuiltinOf)
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.Subst (typeSubstClosedType)
import PlutusIR
import PlutusIR.Subst
import Data.Bifunctor
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Set.Lens (setOf)
import GHC.Stack
import Test.QuickCheck (shrink, shrinkList)
addTmBind :: Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind :: Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind (TermBind ()
_ Strictness
_ (VarDecl ()
_ Name
x Type TyName DefaultUni ()
a) Term TyName Name DefaultUni DefaultFun ()
_) = Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a
addTmBind (DatatypeBind ()
_ Datatype TyName Name DefaultUni ()
dat) = ([(Name, Type TyName DefaultUni ())]
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Datatype TyName Name DefaultUni ()
-> (Name, Type TyName DefaultUni ())
matchType Datatype TyName Name DefaultUni ()
dat (Name, Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
-> [(Name, Type TyName DefaultUni ())]
forall a. a -> [a] -> [a]
: Datatype TyName Name DefaultUni ()
-> [(Name, Type TyName DefaultUni ())]
constrTypes Datatype TyName Name DefaultUni ()
dat) Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall a. Semigroup a => a -> a -> a
<>)
addTmBind Binding TyName Name DefaultUni DefaultFun ()
_ = Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall a. a -> a
id
scopeCheckTyVars :: TypeCtx
-> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars :: TypeCtx
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars TypeCtx
tyctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) = Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy Type TyName DefaultUni ()
ty Set TyName -> Set TyName -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set TyName
inscope
where
inscope :: Set TyName
inscope = TypeCtx -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet TypeCtx
tyctx Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> [TyName] -> Set TyName
forall a. Ord a => [a] -> Set a
Set.fromList (((TyName, Kind ()) -> TyName) -> [(TyName, Kind ())] -> [TyName]
forall a b. (a -> b) -> [a] -> [b]
map (TyName, Kind ()) -> TyName
forall a b. (a, b) -> a
fst ([(TyName, Kind ())] -> [TyName])
-> [(TyName, Kind ())] -> [TyName]
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun () -> [(TyName, Kind ())]
datatypes Term TyName Name DefaultUni DefaultFun ()
tm)
findHelp :: Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp :: Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp Map Name (Type TyName DefaultUni ())
ctx =
case Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())])
-> Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$ (Type TyName DefaultUni () -> Bool)
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter Type TyName DefaultUni () -> Bool
forall {a} {uni :: * -> *}. Eq a => Type a uni () -> Bool
isHelpType Map Name (Type TyName DefaultUni ())
ctx of
[] -> Maybe Name
forall a. Maybe a
Nothing
(Name
x, Type TyName DefaultUni ()
_) : [(Name, Type TyName DefaultUni ())]
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
where
isHelpType :: Type a uni () -> Bool
isHelpType (TyForall ()
_ a
x (Type ()) (TyVar ()
_ a
x')) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x'
isHelpType Type a uni ()
_ = Bool
False
mkHelp :: Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp :: Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
_ (TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni) = SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin SomeTypeIn DefaultUni
someUni
mkHelp (Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp -> Just Name
help) Type TyName DefaultUni ()
ty = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
help) Type TyName DefaultUni ()
ty
mkHelp Map Name (Type TyName DefaultUni ())
_ Type TyName DefaultUni ()
ty = ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty
fixupTerm_ :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxOld Map Name (Type TyName DefaultUni ())
ctxOld TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew Term TyName Name DefaultUni DefaultFun ()
tm0 =
case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Term TyName Name DefaultUni DefaultFun ()
tm0 of
Left String
_ -> case Term TyName Name DefaultUni DefaultFun ()
tm0 of
LamAbs ()
_ Name
x Type TyName DefaultUni ()
_ Term TyName Name DefaultUni DefaultFun ()
tm | TyFun () Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b <- Type TyName DefaultUni ()
tyNew -> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (()
-> 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 ()
a) (()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a)
((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxOld (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctxOld)
TypeCtx
tyctxNew (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctxNew) Type TyName DefaultUni ()
b Term TyName Name DefaultUni DefaultFun ()
tm
Apply ()
_ (Apply ()
_ (TyInst ()
_ (Builtin ()
_ DefaultFun
Trace) Type TyName DefaultUni ()
_) Term TyName Name DefaultUni DefaultFun ()
s) Term TyName Name DefaultUni DefaultFun ()
tm ->
let (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
tm') = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxOld Map Name (Type TyName DefaultUni ())
ctxOld TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew Term TyName Name DefaultUni DefaultFun ()
tm
in (Type TyName DefaultUni ()
ty', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin () DefaultFun
Trace) Type TyName DefaultUni ()
ty') Term TyName Name DefaultUni DefaultFun ()
s) Term TyName Name DefaultUni DefaultFun ()
tm')
Term TyName Name DefaultUni DefaultFun ()
_ | TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni <- Type TyName DefaultUni ()
tyNew -> (Type TyName DefaultUni ()
tyNew, SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin SomeTypeIn DefaultUni
someUni)
| Bool
otherwise -> (Type TyName DefaultUni ()
tyNew, Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew)
Right Type TyName DefaultUni ()
ty -> (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm0)
fixupTerm :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
_ Map Name (Type TyName DefaultUni ())
_ TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew Term TyName Name DefaultUni DefaultFun ()
tm
| Either String () -> Bool
forall a b. Either a b -> Bool
isRight (TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Either String ()
typeCheckTermInContext TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
tyNew) = Term TyName Name DefaultUni DefaultFun ()
tm
| Bool
otherwise = Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew
minimalBuiltin :: SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin :: SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin (SomeTypeIn DefaultUni (Esc a)
uni) = case DefaultUni (Esc a) -> SingKind k
forall k (a :: k). DefaultUni (Esc a) -> SingKind k
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc a)
uni of
SingKind k
SingType -> ()
-> DefaultUni (Esc a)
-> a
-> Term TyName Name DefaultUni DefaultFun ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
TermLike term tyname name uni fun =>
ann -> uni (Esc a) -> a -> term ann
mkConstantOf () DefaultUni (Esc a)
DefaultUni (Esc a)
uni (a -> Term TyName Name DefaultUni DefaultFun ())
-> a -> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> a
forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a)
DefaultUni (Esc a)
uni
SingKind k
_ -> String -> Term TyName Name DefaultUni DefaultFun ()
forall a. HasCallStack => String -> a
error String
"Higher-kinded built-in types cannot be used here"
where
go :: DefaultUni (Esc a) -> a
go :: forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a)
DefaultUniUnit = ()
go DefaultUni (Esc a)
DefaultUniInteger = a
0
go DefaultUni (Esc a)
DefaultUniBool = a
Bool
False
go DefaultUni (Esc a)
DefaultUniString = a
""
go DefaultUni (Esc a)
DefaultUniByteString = a
""
go DefaultUni (Esc a)
DefaultUniData = Integer -> Data
I Integer
0
go (DefaultUni (Esc f)
DefaultUniProtoList `DefaultUniApply` DefaultUni (Esc a1)
_) = []
go (DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a1)
a `DefaultUniApply` DefaultUni (Esc a1)
b) = (DefaultUni (Esc a1) -> a1
forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a1)
DefaultUni (Esc a1)
a, DefaultUni (Esc a1) -> a1
forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a1)
DefaultUni (Esc a1)
b)
go (DefaultUni (Esc f)
f `DefaultUniApply` DefaultUni (Esc a1)
_ `DefaultUniApply` DefaultUni (Esc a1)
_ `DefaultUniApply` DefaultUni (Esc a1)
_) = DefaultUni (Esc f) -> a
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f
go DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element = a
Element
BLS12_381.G1.offchain_zero
go DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element = a
Element
BLS12_381.G2.offchain_zero
go DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult = a
MlResult
BLS12_381.Pairing.identityMlResult
shrinkBind :: HasCallStack
=> Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
shrinkBind :: HasCallStack =>
Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
shrinkBind Recursivity
_ TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Binding TyName Name DefaultUni DefaultFun ()
bind =
case Binding TyName Name DefaultUni DefaultFun ()
bind of
TermBind ()
_ Strictness
s (VarDecl ()
_ Name
x Type TyName DefaultUni ()
ty) Term TyName Name DefaultUni DefaultFun ()
tm -> [ ()
-> Strictness
-> VarDecl TyName Name DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind () Strictness
s (()
-> 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 ()
ty') Term TyName Name DefaultUni DefaultFun ()
tm'
| (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
tm') <- HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm)
] [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
forall a. [a] -> [a] -> [a]
++
[ ()
-> Strictness
-> VarDecl TyName Name DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind () Strictness
Strict (()
-> 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 ()
ty) Term TyName Name DefaultUni DefaultFun ()
tm | Strictness
s Strictness -> Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness
NonStrict ]
TypeBind ()
_ (TyVarDecl ()
_ TyName
a Kind ()
k) Type TyName DefaultUni ()
ty -> [ ()
-> TyVarDecl TyName ()
-> Type TyName DefaultUni ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind () (() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a Kind ()
k') Type TyName DefaultUni ()
ty'
| (Kind ()
k', Type TyName DefaultUni ()
ty') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
tyctx (Kind ()
k, Type TyName DefaultUni ()
ty) ]
DatatypeBind ()
_ Datatype TyName Name DefaultUni ()
dat -> [ ()
-> Datatype TyName Name DefaultUni ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind () Datatype TyName Name DefaultUni ()
dat' | Datatype TyName Name DefaultUni ()
dat' <- TypeCtx
-> Datatype TyName Name DefaultUni ()
-> [Datatype TyName Name DefaultUni ()]
shrinkDat TypeCtx
tyctx Datatype TyName Name DefaultUni ()
dat ]
shrinkDat :: TypeCtx
-> Datatype TyName Name DefaultUni ()
-> [Datatype TyName Name DefaultUni ()]
shrinkDat :: TypeCtx
-> Datatype TyName Name DefaultUni ()
-> [Datatype TyName Name DefaultUni ()]
shrinkDat TypeCtx
ctx (Datatype ()
_ dd :: TyVarDecl TyName ()
dd@(TyVarDecl ()
_ TyName
d Kind ()
_) [TyVarDecl TyName ()]
xs Name
m [VarDecl TyName Name DefaultUni ()]
cs) =
[ ()
-> TyVarDecl TyName ()
-> [TyVarDecl TyName ()]
-> Name
-> [VarDecl TyName Name DefaultUni ()]
-> Datatype TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype () TyVarDecl TyName ()
dd [TyVarDecl TyName ()]
xs Name
m [VarDecl TyName Name DefaultUni ()]
cs' | [VarDecl TyName Name DefaultUni ()]
cs' <- (VarDecl TyName Name DefaultUni ()
-> [VarDecl TyName Name DefaultUni ()])
-> [VarDecl TyName Name DefaultUni ()]
-> [[VarDecl TyName Name DefaultUni ()]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList VarDecl TyName Name DefaultUni ()
-> [VarDecl TyName Name DefaultUni ()]
shrinkCon [VarDecl TyName Name DefaultUni ()]
cs ]
where
ctx' :: TypeCtx
ctx' = TypeCtx
ctx TypeCtx -> TypeCtx -> TypeCtx
forall a. Semigroup a => a -> a -> a
<> [(TyName, Kind ())] -> TypeCtx
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TyName
x, Kind ()
k) | TyVarDecl ()
_ TyName
x Kind ()
k <- [TyVarDecl TyName ()]
xs ]
shrinkCon :: VarDecl TyName Name DefaultUni ()
-> [VarDecl TyName Name DefaultUni ()]
shrinkCon (VarDecl ()
_ Name
c Type TyName DefaultUni ()
ty) = [ ()
-> 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
c Type TyName DefaultUni ()
ty''
| Type TyName DefaultUni ()
ty' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
ctx' Type TyName DefaultUni ()
ty
, let ty'' :: Type TyName DefaultUni ()
ty'' = Type TyName DefaultUni ()
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {tyname} {uni :: * -> *}.
Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget (Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {tyname} {uni :: * -> *} {ann}.
Type tyname uni ann -> Type tyname uni ann
getTarget Type TyName DefaultUni ()
ty) Type TyName DefaultUni ()
ty'
, Type TyName DefaultUni ()
ty'' Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
ty
, TyName
d TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy (Type TyName DefaultUni ()
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {tyname} {uni :: * -> *}.
Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget (forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @() ()) Type TyName DefaultUni ()
ty') ]
where
getTarget :: Type tyname uni ann -> Type tyname uni ann
getTarget (TyFun ann
_ Type tyname uni ann
_ Type tyname uni ann
b) = Type tyname uni ann -> Type tyname uni ann
getTarget Type tyname uni ann
b
getTarget Type tyname uni ann
b = Type tyname uni ann
b
setTarget :: Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget Type tyname uni ()
t (TyFun ()
_ Type tyname uni ()
a Type tyname uni ()
b) = ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type tyname uni ()
a (Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget Type tyname uni ()
t Type tyname uni ()
b)
setTarget Type tyname uni ()
t Type tyname uni ()
_ = Type tyname uni ()
t
shrinkTypedTerm :: HasCallStack
=> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm :: HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm TypeCtx
tyctx0 Map Name (Type TyName DefaultUni ())
ctx0 (Type TyName DefaultUni ()
ty0, Term TyName Name DefaultUni DefaultFun ()
tm0) = [[(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[
((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> Bool)
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. (a -> Bool) -> [a] -> [a]
filter (TypeCtx
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars TypeCtx
tyctx0)
[ (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
tm')
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun () -> Bool
forall {tyname} {uni :: * -> *} {fun} {a}.
Map Name (Type TyName DefaultUni ())
-> Term tyname Name uni fun a -> Bool
isHelp Map Name (Type TyName DefaultUni ())
ctx0 Term TyName Name DefaultUni DefaultFun ()
tm0
, Type TyName DefaultUni ()
ty' <- Type TyName DefaultUni ()
ty0 Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()] -> [Type TyName DefaultUni ()]
forall a. a -> [a] -> [a]
: HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType (TypeCtx
tyctx0 TypeCtx -> TypeCtx -> TypeCtx
forall a. Semigroup a => a -> a -> a
<> [(TyName, Kind ())] -> TypeCtx
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Term TyName Name DefaultUni DefaultFun () -> [(TyName, Kind ())]
datatypes Term TyName Name DefaultUni DefaultFun ()
tm0)) Type TyName DefaultUni ()
ty0
, let tm' :: Term TyName Name DefaultUni DefaultFun ()
tm' = Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
ctx0 Type TyName DefaultUni ()
ty'
]
, HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx0 Map Name (Type TyName DefaultUni ())
ctx0 (Type TyName DefaultUni ()
ty0, Term TyName Name DefaultUni DefaultFun ()
tm0)
]
where
isHelp :: Map Name (Type TyName DefaultUni ())
-> Term tyname Name uni fun a -> Bool
isHelp Map Name (Type TyName DefaultUni ())
_ (Constant a
_ Some (ValueOf uni)
_) = Bool
True
isHelp Map Name (Type TyName DefaultUni ())
ctx (TyInst a
_ (Var a
_ Name
x) Type tyname uni a
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp Map Name (Type TyName DefaultUni ())
ctx
isHelp Map Name (Type TyName DefaultUni ())
_ (Error a
_ Type tyname uni a
_) = Bool
True
isHelp Map Name (Type TyName DefaultUni ())
_ Term tyname Name uni fun a
_ = Bool
False
addTyBind :: Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind (TypeBind a
_ (TyVarDecl a
_ k
a Kind a
k) Type k uni a
_) = k -> Kind a -> Map k (Kind a) -> Map k (Kind a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
a Kind a
k
addTyBind (DatatypeBind a
_ (Datatype a
_ (TyVarDecl a
_ k
a Kind a
k) [TyVarDecl k a]
_ name
_ [VarDecl k name uni a]
_)) = k -> Kind a -> Map k (Kind a) -> Map k (Kind a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
a Kind a
k
addTyBind Binding k name uni fun a
_ = Map k (Kind a) -> Map k (Kind a)
forall a. a -> a
id
addTyBindSubst :: Binding k name uni fun a
-> Map k (Type k uni a) -> Map k (Type k uni a)
addTyBindSubst (TypeBind a
_ (TyVarDecl a
_ k
a Kind a
_) Type k uni a
ty) = k -> Type k uni a -> Map k (Type k uni a) -> Map k (Type k uni a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
a Type k uni a
ty
addTyBindSubst Binding k name uni fun a
_ = Map k (Type k uni a) -> Map k (Type k uni a)
forall a. a -> a
id
go :: HasCallStack => _
go :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) =
((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> Bool)
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. (a -> Bool) -> [a] -> [a]
filter (TypeCtx
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars TypeCtx
tyctx) ([(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())])
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$
HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
nonstructural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
structural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm)
nonstructural :: HasCallStack => _
nonstructural :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
nonstructural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) =
case Term TyName Name DefaultUni DefaultFun ()
tm of
Let ()
_ Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL Term TyName Name DefaultUni DefaultFun ()
body -> [[(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[
[ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
body
| let tyctxInner :: TypeCtx
tyctxInner = (Binding TyName Name DefaultUni DefaultFun ()
-> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
ctxInner :: Map Name (Type TyName DefaultUni ())
ctxInner = (Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
]
,
[ (Type TyName DefaultUni ()
letTy, case [Binding TyName Name DefaultUni DefaultFun ()]
binds of
[] -> Term TyName Name DefaultUni DefaultFun ()
letTm
Binding TyName Name DefaultUni DefaultFun ()
b:[Binding TyName Name DefaultUni DefaultFun ()]
bs -> ()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
NonRec (Binding TyName Name DefaultUni DefaultFun ()
b Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:| [Binding TyName Name DefaultUni DefaultFun ()]
bs) Term TyName Name DefaultUni DefaultFun ()
letTm)
| (NonEmptyContext [Binding TyName Name DefaultUni DefaultFun ()]
binds [Binding TyName Name DefaultUni DefaultFun ()]
_, TermBind ()
_ Strictness
_ (VarDecl ()
_ Name
_ Type TyName DefaultUni ()
letTy) Term TyName Name DefaultUni DefaultFun ()
letTm) <-
NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> [(OneHoleContext
NonEmpty (Binding TyName Name DefaultUni DefaultFun ()),
Binding TyName Name DefaultUni DefaultFun ())]
forall a. NonEmpty a -> [(OneHoleContext NonEmpty a, a)]
forall (f :: * -> *) a.
Container f =>
f a -> [(OneHoleContext f a, a)]
oneHoleContexts NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
, Recursivity
rec Recursivity -> Recursivity -> Bool
forall a. Eq a => a -> a -> Bool
== Recursivity
NonRec
]
,
[ (Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec (Binding TyName Name DefaultUni DefaultFun ()
b Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:| [Binding TyName Name DefaultUni DefaultFun ()]
binds'))
((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner TypeCtx
tyctxInner' Map Name (Type TyName DefaultUni ())
ctxInner' Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
body
| (NonEmptyContext [Binding TyName Name DefaultUni DefaultFun ()]
binds0 [Binding TyName Name DefaultUni DefaultFun ()]
binds1, Binding TyName Name DefaultUni DefaultFun ()
_) <- NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> [(OneHoleContext
NonEmpty (Binding TyName Name DefaultUni DefaultFun ()),
Binding TyName Name DefaultUni DefaultFun ())]
forall a. NonEmpty a -> [(OneHoleContext NonEmpty a, a)]
forall (f :: * -> *) a.
Container f =>
f a -> [(OneHoleContext f a, a)]
oneHoleContexts NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL,
let tyctxInner :: TypeCtx
tyctxInner = (Binding TyName Name DefaultUni DefaultFun ()
-> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
ctxInner :: Map Name (Type TyName DefaultUni ())
ctxInner = (Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
binds :: [Binding TyName Name DefaultUni DefaultFun ()]
binds = [Binding TyName Name DefaultUni DefaultFun ()]
binds0 [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
forall a. [a] -> [a] -> [a]
++ [Binding TyName Name DefaultUni DefaultFun ()]
binds1
tyctxInner' :: TypeCtx
tyctxInner' = (Binding TyName Name DefaultUni DefaultFun ()
-> TypeCtx -> TypeCtx)
-> TypeCtx
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> TypeCtx
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx [Binding TyName Name DefaultUni DefaultFun ()]
binds
ctxInner' :: Map Name (Type TyName DefaultUni ())
ctxInner' = (Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx [Binding TyName Name DefaultUni DefaultFun ()]
binds
, Binding TyName Name DefaultUni DefaultFun ()
b:[Binding TyName Name DefaultUni DefaultFun ()]
binds' <- [[Binding TyName Name DefaultUni DefaultFun ()]
binds]
]
]
LamAbs ()
_ Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body ->
[ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctx) TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
b Term TyName Name DefaultUni DefaultFun ()
body
| TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
ty]
]
Apply ()
_ Term TyName Name DefaultUni DefaultFun ()
fun Term TyName Name DefaultUni DefaultFun ()
arg -> case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Term TyName Name DefaultUni DefaultFun ()
arg of
Right Type TyName DefaultUni ()
argTy ->
[
(Type TyName DefaultUni ()
ty, TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
arg)
, (Type TyName DefaultUni ()
ty, TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
fun)
,
(Type TyName DefaultUni ()
argTy, Term TyName Name DefaultUni DefaultFun ()
arg)
, (()
-> 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 ()
argTy Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
fun)
]
Left String
err -> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error (String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())])
-> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ String -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlcCondensedErrorClassic String
err
TyAbs ()
_ TyName
x Kind ()
_ Term TyName Name DefaultUni DefaultFun ()
body ->
[ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
k TypeCtx
tyctx) Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
tyInner' Term TyName Name DefaultUni DefaultFun ()
body
| TyForall ()
_ TyName
y Kind ()
k Type TyName DefaultUni ()
tyInner <- [Type TyName DefaultUni ()
ty]
, let tyInner' :: Type TyName DefaultUni ()
tyInner' = TyName
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) a.
Eq tyname =>
tyname
-> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
typeSubstClosedType TyName
y (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k) Type TyName DefaultUni ()
tyInner
]
Var{} -> []
Constant{} -> []
Builtin{} -> []
TyInst{} -> []
Error{} -> []
IWrap{} -> []
Unwrap{} -> []
PlutusIR.Constr{} -> []
Case{} -> []
structural :: HasCallStack => _
structural :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
structural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) =
case Term TyName Name DefaultUni DefaultFun ()
tm of
Let ()
_ Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds Term TyName Name DefaultUni DefaultFun ()
body ->
[ (Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substTypeParallel Map TyName (Type TyName DefaultUni ())
subst Type TyName DefaultUni ()
ty', ()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds Term TyName Name DefaultUni DefaultFun ()
body')
| (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
body') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body) ] [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
[ (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fix ((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ (Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds') ((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner TypeCtx
tyctxInner' Map Name (Type TyName DefaultUni ())
ctxInner' Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
body
| (context :: OneHoleContext
NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
context@(NonEmptyContext [Binding TyName Name DefaultUni DefaultFun ()]
before [Binding TyName Name DefaultUni DefaultFun ()]
_), Binding TyName Name DefaultUni DefaultFun ()
bind) <- NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> [(OneHoleContext
NonEmpty (Binding TyName Name DefaultUni DefaultFun ()),
Binding TyName Name DefaultUni DefaultFun ())]
forall a. NonEmpty a -> [(OneHoleContext NonEmpty a, a)]
forall (f :: * -> *) a.
Container f =>
f a -> [(OneHoleContext f a, a)]
oneHoleContexts NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds,
let ctxBind :: Map Name (Type TyName DefaultUni ())
ctxBind | Recursivity
Rec <- Recursivity
rec = Map Name (Type TyName DefaultUni ())
ctxInner
| Bool
otherwise = (Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx [Binding TyName Name DefaultUni DefaultFun ()]
before
tyctxBind :: TypeCtx
tyctxBind | Recursivity
Rec <- Recursivity
rec = TypeCtx
tyctxInner
| Bool
otherwise = (Binding TyName Name DefaultUni DefaultFun ()
-> TypeCtx -> TypeCtx)
-> TypeCtx
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> TypeCtx
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx [Binding TyName Name DefaultUni DefaultFun ()]
before,
Binding TyName Name DefaultUni DefaultFun ()
bind' <- HasCallStack =>
Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
shrinkBind Recursivity
rec TypeCtx
tyctxBind Map Name (Type TyName DefaultUni ())
ctxBind Binding TyName Name DefaultUni DefaultFun ()
bind,
let binds' :: NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds' = OneHoleContext
NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. OneHoleContext NonEmpty a -> a -> NonEmpty a
forall (f :: * -> *) a.
Container f =>
OneHoleContext f a -> a -> f a
plugHole OneHoleContext
NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
context Binding TyName Name DefaultUni DefaultFun ()
bind'
tyctxInner' :: TypeCtx
tyctxInner' = (Binding TyName Name DefaultUni DefaultFun ()
-> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds'
ctxInner' :: Map Name (Type TyName DefaultUni ())
ctxInner' = (Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds'
fix :: (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fix = (Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx)
] where subst :: Map TyName (Type TyName DefaultUni ())
subst = (Binding TyName Name DefaultUni DefaultFun ()
-> Map TyName (Type TyName DefaultUni ())
-> Map TyName (Type TyName DefaultUni ()))
-> Map TyName (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map TyName (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map TyName (Type TyName DefaultUni ())
-> Map TyName (Type TyName DefaultUni ())
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a
-> Map k (Type k uni a) -> Map k (Type k uni a)
addTyBindSubst Map TyName (Type TyName DefaultUni ())
forall a. Monoid a => a
mempty NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds
tyctxInner :: TypeCtx
tyctxInner = (Binding TyName Name DefaultUni DefaultFun ()
-> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds
ctxInner :: Map Name (Type TyName DefaultUni ())
ctxInner = (Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds
TyInst ()
_ Term TyName Name DefaultUni DefaultFun ()
fun Type TyName DefaultUni ()
argTy -> case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Term TyName Name DefaultUni DefaultFun ()
fun of
Right funTy :: Type TyName DefaultUni ()
funTy@(TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
tyInner) ->
[ (HasCallStack =>
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall k a. k -> a -> Map k a
Map.singleton TyName
x' Type TyName DefaultUni ()
argTy') Type TyName DefaultUni ()
tyInner', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
fun' Type TyName DefaultUni ()
argTy')
| (TyForall () TyName
x' Kind ()
k' Type TyName DefaultUni ()
tyInner', Term TyName Name DefaultUni DefaultFun ()
fun') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
funTy, Term TyName Name DefaultUni DefaultFun ()
fun)
, let argTy' :: Type TyName DefaultUni ()
argTy' | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k' = Type TyName DefaultUni ()
argTy
| Bool
otherwise = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k'
] [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
[ (HasCallStack =>
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall k a. k -> a -> Map k a
Map.singleton TyName
x Type TyName DefaultUni ()
argTy') Type TyName DefaultUni ()
tyInner', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
fun' Type TyName DefaultUni ()
argTy')
| (Kind ()
k', Type TyName DefaultUni ()
argTy') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
tyctx (Kind ()
k, Type TyName DefaultUni ()
argTy)
, let tyInner' :: Type TyName DefaultUni ()
tyInner' | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k' = Type TyName DefaultUni ()
tyInner
| Bool
otherwise = HasCallStack =>
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall k a. k -> a -> Map k a
Map.singleton TyName
x (Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ()))
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k) Type TyName DefaultUni ()
tyInner
fun' :: Term TyName Name DefaultUni DefaultFun ()
fun' = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
x Kind ()
k' Type TyName DefaultUni ()
tyInner') Term TyName Name DefaultUni DefaultFun ()
fun
]
Left String
err -> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error (String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())])
-> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ String -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlcCondensedErrorClassic String
err
Right Type TyName DefaultUni ()
tyWrong -> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error (String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())])
-> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ String
"Expected a 'TyForall', but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type TyName DefaultUni () -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc Type TyName DefaultUni ()
tyWrong
TyAbs ()
_ TyName
x Kind ()
_ Term TyName Name DefaultUni DefaultFun ()
body | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyName -> TypeCtx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member TyName
x TypeCtx
tyctx ->
[ (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
x Kind ()
k Type TyName DefaultUni ()
tyInner', ()
-> TyName
-> Kind ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs () TyName
x Kind ()
k Term TyName Name DefaultUni DefaultFun ()
body')
| TyForall ()
_ TyName
y Kind ()
k Type TyName DefaultUni ()
tyInner <- [Type TyName DefaultUni ()
ty]
, (Type TyName DefaultUni ()
tyInner', Term TyName Name DefaultUni DefaultFun ()
body') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
k TypeCtx
tyctx) Map Name (Type TyName DefaultUni ())
ctx (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
y TyName
x Type TyName DefaultUni ()
tyInner, Term TyName Name DefaultUni DefaultFun ()
body)
]
LamAbs ()
_ Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body ->
[ (()
-> 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 ()
a Type TyName DefaultUni ()
b', ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body')
| TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
ty],
(Type TyName DefaultUni ()
b', Term TyName Name DefaultUni DefaultFun ()
body') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctx) (Type TyName DefaultUni ()
b, Term TyName Name DefaultUni DefaultFun ()
body)
] [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
[ (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (()
-> 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 ()
a') (()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a') ((Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctx) TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a' Map Name (Type TyName DefaultUni ())
ctx) Type TyName DefaultUni ()
b Term TyName Name DefaultUni DefaultFun ()
body
| TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
ty],
Type TyName DefaultUni ()
a' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
tyctx Type TyName DefaultUni ()
a
]
Apply ()
_ Term TyName Name DefaultUni DefaultFun ()
fun Term TyName Name DefaultUni DefaultFun ()
arg -> case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Term TyName Name DefaultUni DefaultFun ()
arg of
Left String
err -> String
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error String
err
Right Type TyName DefaultUni ()
argTy ->
[ (Type TyName DefaultUni ()
ty', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
fun' Term TyName Name DefaultUni DefaultFun ()
arg')
| (TyFun ()
_ Type TyName DefaultUni ()
argTy' Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
fun') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (()
-> 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 ()
argTy Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
fun)
, let arg' :: Term TyName Name DefaultUni DefaultFun ()
arg' = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
argTy' Term TyName Name DefaultUni DefaultFun ()
arg
] [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
[ (Type TyName DefaultUni ()
ty, ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
fun' Term TyName Name DefaultUni DefaultFun ()
arg')
| (Type TyName DefaultUni ()
argTy', Term TyName Name DefaultUni DefaultFun ()
arg') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
argTy, Term TyName Name DefaultUni DefaultFun ()
arg)
, let fun' :: Term TyName Name DefaultUni DefaultFun ()
fun' = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (()
-> 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 ()
argTy' Type TyName DefaultUni ()
ty) Term TyName Name DefaultUni DefaultFun ()
fun
]
Constant ()
_ Some (ValueOf DefaultUni)
val ->
Some (ValueOf DefaultUni) -> [Some (ValueOf DefaultUni)]
forall a. Arbitrary a => a -> [a]
shrink Some (ValueOf DefaultUni)
val [Some (ValueOf DefaultUni)]
-> (Some (ValueOf DefaultUni)
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \val' :: Some (ValueOf DefaultUni)
val'@(Some (ValueOf DefaultUni (Esc a)
uni a
_)) ->
(() -> DefaultUni (Esc a) -> Type TyName DefaultUni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf () DefaultUni (Esc a)
uni, ()
-> Some (ValueOf DefaultUni)
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant () Some (ValueOf DefaultUni)
val')
Error ()
_ Type TyName DefaultUni ()
_ -> HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
tyctx Type TyName DefaultUni ()
ty [Type TyName DefaultUni ()]
-> (Type TyName DefaultUni ()
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ()))
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Type TyName DefaultUni ()
ty' -> (Type TyName DefaultUni ()
ty', ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty')
Var{} -> []
IWrap{} -> []
Unwrap{} -> []
Builtin{} -> []
Case{} -> []
TyAbs{} -> []
PlutusIR.Constr{} -> []
shrinkClosedTypedTerm :: (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())]
shrinkClosedTypedTerm :: (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
shrinkClosedTypedTerm = HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm TypeCtx
forall a. Monoid a => a
mempty Map Name (Type TyName DefaultUni ())
forall a. Monoid a => a
mempty