module PlutusCore.Generators.QuickCheck.Substitutions where
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.GenerateTypes
import PlutusCore.Generators.QuickCheck.ShrinkTypes
import PlutusCore.Generators.QuickCheck.Utils
import PlutusCore.Default
import PlutusCore.Name.Unique
import PlutusIR
import PlutusIR.Subst
import Control.Monad ((<=<))
import Data.Map.Strict (Map)
import Data.Map.Strict.Internal qualified as Map
import Data.Maybe
import Data.MultiSet (toMap)
import Data.MultiSet.Lens
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Set.Lens
import GHC.Stack
import Test.QuickCheck hiding (reason)
type TypeSub = Map TyName (Type TyName DefaultUni ())
substTypeCustomGo
:: HasCallStack
=> Bool
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustomGo :: HasCallStack =>
Bool
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustomGo Bool
nested Set TyName
fvs0 = Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs0 Set TyName
forall a. Set a
Set.empty where
go :: Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
ty = case Type TyName DefaultUni ()
ty of
TyVar ()
_ TyName
x | TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
x Set TyName
seen -> [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"substType' loop"
TyVar ()
_ TyName
x | Bool
nested -> Type TyName DefaultUni ()
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type TyName DefaultUni ()
ty (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x Set TyName
seen) TypeSub
sub) (Maybe (Type TyName DefaultUni ()) -> Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ TyName -> TypeSub -> Maybe (Type TyName DefaultUni ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
x TypeSub
sub
| Bool
otherwise -> Type TyName DefaultUni ()
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Type TyName DefaultUni ()
ty Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a. a -> a
id (Maybe (Type TyName DefaultUni ()) -> Type TyName DefaultUni ())
-> Maybe (Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ TyName -> TypeSub -> Maybe (Type TyName DefaultUni ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
x TypeSub
sub
TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b -> ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
a) (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
b)
TyApp ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b -> ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
a) (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
b)
TyLam ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
b
| TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
x Set TyName
fvs ->
()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x' Kind ()
k (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x' Set TyName
fvs) Set TyName
seen TypeSub
sub (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
x' Type TyName DefaultUni ()
b)
| Bool
otherwise ->
()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x Kind ()
k (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x Set TyName
fvs) (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.delete TyName
x Set TyName
seen) TypeSub
sub Type TyName DefaultUni ()
b
where x' :: TyName
x' = Set TyName -> TyName -> TyName
freshenTyNameWith (Set TyName
fvs Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> 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 ()
b) TyName
x
TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
b
| TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member TyName
x Set TyName
fvs ->
()
-> 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 () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x' Set TyName
fvs) Set TyName
seen TypeSub
sub (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
x' Type TyName DefaultUni ()
b)
| Bool
otherwise ->
()
-> 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 () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.insert TyName
x Set TyName
fvs) (TyName -> Set TyName -> Set TyName
forall a. Ord a => a -> Set a -> Set a
Set.delete TyName
x Set TyName
seen) TypeSub
sub Type TyName DefaultUni ()
b
where x' :: TyName
x' = Set TyName -> TyName -> TyName
freshenTyNameWith (Set TyName
fvs Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> 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 ()
b) TyName
x
TyBuiltin{} -> Type TyName DefaultUni ()
ty
TyIFix ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b -> ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyIFix () (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
a) (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub Type TyName DefaultUni ()
b)
TySOP ()
_ [[Type TyName DefaultUni ()]]
tyls -> () -> [[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () ((([Type TyName DefaultUni ()] -> [Type TyName DefaultUni ()])
-> [[Type TyName DefaultUni ()]] -> [[Type TyName DefaultUni ()]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Type TyName DefaultUni ()] -> [Type TyName DefaultUni ()])
-> [[Type TyName DefaultUni ()]] -> [[Type TyName DefaultUni ()]])
-> ((Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> [Type TyName DefaultUni ()] -> [Type TyName DefaultUni ()])
-> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> [[Type TyName DefaultUni ()]]
-> [[Type TyName DefaultUni ()]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> [Type TyName DefaultUni ()] -> [Type TyName DefaultUni ()]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap) (Set TyName
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
go Set TyName
fvs Set TyName
seen TypeSub
sub) [[Type TyName DefaultUni ()]]
tyls)
substEscape :: Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substEscape :: Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substEscape = HasCallStack =>
Bool
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
Bool
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustomGo Bool
True
substTypeCustom
:: HasCallStack
=> Bool
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustom :: HasCallStack =>
Bool
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustom Bool
nested TypeSub
sub0 Type TyName DefaultUni ()
ty0 = HasCallStack =>
Bool
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
Bool
-> Set TyName
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustomGo Bool
nested Set TyName
fvs0 TypeSub
sub0 Type TyName DefaultUni ()
ty0 where
fvs0 :: Set TyName
fvs0 = [Set TyName] -> Set TyName
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set TyName] -> Set TyName) -> [Set TyName] -> Set TyName
forall a b. (a -> b) -> a -> b
$ TypeSub -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet TypeSub
sub0 Set TyName -> [Set TyName] -> [Set TyName]
forall a. a -> [a] -> [a]
: (Type TyName DefaultUni () -> Set TyName)
-> [Type TyName DefaultUni ()] -> [Set TyName]
forall a b. (a -> b) -> [a] -> [b]
map (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) (TypeSub -> [Type TyName DefaultUni ()]
forall k a. Map k a -> [a]
Map.elems TypeSub
sub0)
substType
:: HasCallStack
=> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substType :: HasCallStack =>
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType = HasCallStack =>
Bool
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
Bool
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustom Bool
True
substTypeParallel
:: TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeParallel :: TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substTypeParallel = HasCallStack =>
Bool
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
Bool
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
substTypeCustom Bool
False
renameVar :: TyName -> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar :: TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
x TyName
y
| TyName
x TyName -> TyName -> Bool
forall a. Eq a => a -> a -> Bool
== TyName
y = Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a. a -> a
id
| Bool
otherwise = HasCallStack =>
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TypeSub -> Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> TypeSub
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ TyName -> Type TyName DefaultUni () -> TypeSub
forall k a. k -> a -> Map k a
Map.singleton TyName
x (() -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
y)
fvTypeR :: TypeSub -> Type TyName DefaultUni () -> Set TyName
fvTypeR :: TypeSub -> Type TyName DefaultUni () -> Set TyName
fvTypeR TypeSub
sub = Type TyName DefaultUni () -> Set TyName
go where
go :: Type TyName DefaultUni () -> Set TyName
go = (TyName -> Set TyName) -> Set TyName -> Set TyName
forall m a. Monoid m => (a -> m) -> Set a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\TyName
v -> Set TyName
-> (Type TyName DefaultUni () -> Set TyName)
-> Maybe (Type TyName DefaultUni ())
-> Set TyName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TyName -> Set TyName
forall a. a -> Set a
Set.singleton TyName
v) Type TyName DefaultUni () -> Set TyName
go (Maybe (Type TyName DefaultUni ()) -> Set TyName)
-> Maybe (Type TyName DefaultUni ()) -> Set TyName
forall a b. (a -> b) -> a -> b
$ TyName -> TypeSub -> Maybe (Type TyName DefaultUni ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
v TypeSub
sub) (Set TyName -> Set TyName)
-> (Type TyName DefaultUni () -> Set TyName)
-> Type TyName DefaultUni ()
-> Set TyName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
fvTypeBag :: Type TyName DefaultUni () -> Map TyName Int
fvTypeBag :: Type TyName DefaultUni () -> Map TyName Int
fvTypeBag = MultiSet TyName -> Map TyName Int
forall a. MultiSet a -> Map a Int
toMap (MultiSet TyName -> Map TyName Int)
-> (Type TyName DefaultUni () -> MultiSet TyName)
-> Type TyName DefaultUni ()
-> Map TyName Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (MultiSet TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> MultiSet TyName
forall a s. Getting (MultiSet a) s a -> s -> MultiSet a
multiSetOf Getting (MultiSet 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
genSubst :: TypeCtx -> Gen TypeSub
genSubst :: TypeCtx -> Gen TypeSub
genSubst TypeCtx
ctx0 = do
[(TyName, Kind ())]
xks <- [(TyName, Kind ())] -> Gen [(TyName, Kind ())]
forall a. [a] -> Gen [a]
sublistOf ([(TyName, Kind ())] -> Gen [(TyName, Kind ())])
-> ([(TyName, Kind ())] -> Gen [(TyName, Kind ())])
-> [(TyName, Kind ())]
-> Gen [(TyName, Kind ())]
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< [(TyName, Kind ())] -> Gen [(TyName, Kind ())]
forall a. [a] -> Gen [a]
shuffle ([(TyName, Kind ())] -> Gen [(TyName, Kind ())])
-> [(TyName, Kind ())] -> Gen [(TyName, Kind ())]
forall a b. (a -> b) -> a -> b
$ TypeCtx -> [(TyName, Kind ())]
forall k a. Map k a -> [(k, a)]
Map.toList TypeCtx
ctx0
TypeCtx
-> TypeSub -> Map TyName Int -> [(TyName, Kind ())] -> Gen TypeSub
go TypeCtx
ctx0 TypeSub
forall k a. Map k a
Map.empty Map TyName Int
forall k a. Map k a
Map.empty [(TyName, Kind ())]
xks
where
go :: TypeCtx
-> TypeSub -> Map TyName Int -> [(TyName, Kind ())] -> Gen TypeSub
go TypeCtx
_ TypeSub
sub Map TyName Int
_ [] = TypeSub -> Gen TypeSub
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeSub
sub
go TypeCtx
ctx TypeSub
sub Map TyName Int
counts ((TyName
x, Kind ()
k) : [(TyName, Kind ())]
xs) = do
let
ctx' :: TypeCtx
ctx' = TyName -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete TyName
x TypeCtx
ctx
w :: Int
w = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
1 (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ TyName -> Map TyName Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
x Map TyName Int
counts
Type TyName DefaultUni ()
ty <- (Int -> Gen (Type TyName DefaultUni ()))
-> Gen (Type TyName DefaultUni ())
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (Type TyName DefaultUni ()))
-> Gen (Type TyName DefaultUni ()))
-> (Int -> Gen (Type TyName DefaultUni ()))
-> Gen (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ \ Int
n -> Int
-> Gen (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ())
forall a. Int -> Gen a -> Gen a
resize (Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
w) (Gen (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ()))
-> Gen (Type TyName DefaultUni ())
-> Gen (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ TypeCtx -> Kind () -> Gen (Type TyName DefaultUni ())
genTypeWithCtx TypeCtx
ctx' Kind ()
k
let
moreCounts :: Map TyName Int
moreCounts = (Int -> Int) -> Map TyName Int -> Map TyName Int
forall a b. (a -> b) -> Map TyName a -> Map TyName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
w) (Map TyName Int -> Map TyName Int)
-> Map TyName Int -> Map TyName Int
forall a b. (a -> b) -> a -> b
$ Type TyName DefaultUni () -> Map TyName Int
fvTypeBag Type TyName DefaultUni ()
ty
sub' :: TypeSub
sub' = TyName -> Type TyName DefaultUni () -> TypeSub -> TypeSub
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Type TyName DefaultUni ()
ty TypeSub
sub
counts' :: Map TyName Int
counts' = (Int -> Int -> Int)
-> Map TyName Int -> Map TyName Int -> Map TyName Int
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Map TyName Int
counts Map TyName Int
moreCounts
TypeCtx
-> TypeSub -> Map TyName Int -> [(TyName, Kind ())] -> Gen TypeSub
go TypeCtx
ctx' TypeSub
sub' Map TyName Int
counts' [(TyName, Kind ())]
xs
shrinkSubst :: TypeCtx -> TypeSub -> [TypeSub]
shrinkSubst :: TypeCtx -> TypeSub -> [TypeSub]
shrinkSubst TypeCtx
ctx0 = ([(TyName, Type TyName DefaultUni ())] -> TypeSub)
-> [[(TyName, Type TyName DefaultUni ())]] -> [TypeSub]
forall a b. (a -> b) -> [a] -> [b]
map [(TyName, Type TyName DefaultUni ())] -> TypeSub
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([[(TyName, Type TyName DefaultUni ())]] -> [TypeSub])
-> (TypeSub -> [[(TyName, Type TyName DefaultUni ())]])
-> TypeSub
-> [TypeSub]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((TyName, Type TyName DefaultUni ())
-> [(TyName, Type TyName DefaultUni ())])
-> [(TyName, Type TyName DefaultUni ())]
-> [[(TyName, Type TyName DefaultUni ())]]
forall a. (a -> [a]) -> [a] -> [[a]]
forall (f :: * -> *) a. Arbitrary1 f => (a -> [a]) -> f a -> [f a]
liftShrink (TyName, Type TyName DefaultUni ())
-> [(TyName, Type TyName DefaultUni ())]
shrinkTy ([(TyName, Type TyName DefaultUni ())]
-> [[(TyName, Type TyName DefaultUni ())]])
-> (TypeSub -> [(TyName, Type TyName DefaultUni ())])
-> TypeSub
-> [[(TyName, Type TyName DefaultUni ())]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeSub -> [(TyName, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList
where
shrinkTy :: (TyName, Type TyName DefaultUni ())
-> [(TyName, Type TyName DefaultUni ())]
shrinkTy (TyName
x, Type TyName DefaultUni ()
ty) = (,) TyName
x (Type TyName DefaultUni () -> (TyName, Type TyName DefaultUni ()))
-> [Type TyName DefaultUni ()]
-> [(TyName, Type TyName DefaultUni ())]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HasCallStack =>
TypeCtx
-> Kind ()
-> Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()]
TypeCtx
-> Kind ()
-> Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()]
shrinkTypeAtKind (TypeCtx -> Type TyName DefaultUni () -> TypeCtx
forall {unique} {k} {a} {uni :: * -> *} {ann}.
(Coercible unique Int, Ord k, HasUnique k unique) =>
Map k a -> Type k uni ann -> Map k a
pruneCtx TypeCtx
ctx0 Type TyName DefaultUni ()
ty) Kind ()
k Type TyName DefaultUni ()
ty
where k :: Kind ()
k = Kind () -> Maybe (Kind ()) -> Kind ()
forall a. a -> Maybe a -> a
fromMaybe ([Char] -> Kind ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> Kind ()) -> [Char] -> Kind ()
forall a b. (a -> b) -> a -> b
$ [Char]
"internal error: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ TyName -> [Char]
forall a. Show a => a -> [Char]
show TyName
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" not found") (Maybe (Kind ()) -> Kind ()) -> Maybe (Kind ()) -> Kind ()
forall a b. (a -> b) -> a -> b
$ TyName -> TypeCtx -> Maybe (Kind ())
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup TyName
x TypeCtx
ctx0
pruneCtx :: Map k a -> Type k uni ann -> Map k a
pruneCtx Map k a
ctx Type k uni ann
ty = Map k a
ctx Map k a -> Set k -> Map k a
forall k a. Ord k => Map k a -> Set k -> Map k a
`Map.restrictKeys` Getting (Set k) (Type k uni ann) k -> Type k uni ann -> Set k
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set k) (Type k uni ann) k
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type k uni ann) k
ftvTy Type k uni ann
ty