module UVMHS.Lib.Shrinky where

import UVMHS.Core

class Shrinky a where
  shrink ∷ a → 𝐼 a

isoShrink ∷ (a ⇄ b,Shrinky b) ⇒ a → 𝐼 a
isoShrink :: forall a b. (a ⇄ b, Shrinky b) => a -> 𝐼 a
isoShrink = b -> a
forall a b. (a ⇄ b) => b -> a
isofr (b -> a) -> (b -> 𝐼 b) -> b -> 𝐼 a
forall (t :: * -> *) b c a.
Functor t =>
(b -> c) -> (a -> t b) -> a -> t c
^∘ b -> 𝐼 b
forall a. Shrinky a => a -> 𝐼 a
shrink (b -> 𝐼 a) -> (a -> b) -> a -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
forall a b. (a ⇄ b) => a -> b
isoto

instance Shrinky () where shrink :: () -> 𝐼 ()
shrink = 𝐼 () -> () -> 𝐼 ()
forall a b. a -> b -> a
const 𝐼 ()
forall a. Null a => a
null

instance Shrinky ℕ64 where
  shrink :: ℕ64 -> 𝐼 ℕ64
shrink ℕ64
n =
    if 
    | ℕ64
n ℕ64 -> ℕ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ64
0     → 𝐼 ℕ64
forall a. Null a => a
null
    | ℕ64
n ℕ64 -> ℕ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ64
1     → ℕ64 -> 𝐼 ℕ64
forall a t. Single a t => a -> t
single ℕ64
0
    | 𝔹
otherwise → [ℕ64] -> 𝐼 ℕ64
forall a t. ToIter a t => t -> 𝐼 a
iter [ℕ64
0,ℕ64
nℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
-ℕ64
1,ℕ64
nℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
-ℕ64
2,ℕ64
nℕ64 -> ℕ64 -> ℕ64
forall a. DivMod a => a -> a -> a
⌿ℕ64
2]

instance Shrinky ℤ64 where
  shrink :: ℤ64 -> 𝐼 ℤ64
shrink ℤ64
i =
    if
    | ℤ64
i ℤ64 -> ℤ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℤ64
0     → 𝐼 ℤ64
forall a. Null a => a
null
    | ℤ64
i ℤ64 -> ℤ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℤ64
1     → ℤ64 -> 𝐼 ℤ64
forall a t. Single a t => a -> t
single ℤ64
0
    | ℤ64
i ℤ64 -> ℤ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℤ64 -> ℤ64
forall a. (Zero a, Minus a) => a -> a
neg ℤ64
1 → ℤ64 -> 𝐼 ℤ64
forall a t. Single a t => a -> t
single ℤ64
0
    | 𝔹
otherwise →
        let iP :: ℤ64
iP = ℕ -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ -> ℤ64) -> ℕ -> ℤ64
forall a b. (a -> b) -> a -> b
$ ℤ -> ℕ
zabs (ℤ -> ℕ) -> ℤ -> ℕ
forall a b. (a -> b) -> a -> b
$ ℤ64 -> ℤ
forall a. ToInt a => a -> ℤ
int ℤ64
i
            iN :: ℤ64
iN = ℤ64 -> ℤ64
forall a. (Zero a, Minus a) => a -> a
neg ℤ64
iP
        in
        [𝐼 ℤ64] -> 𝐼 ℤ64
forall a t. (Monoid a, ToIter a t) => t -> a
concat
          [ [ℤ64] -> 𝐼 ℤ64
forall a t. ToIter a t => t -> 𝐼 a
iter [ℤ64
0]
          , [ℤ64] -> 𝐼 ℤ64
forall a t. ToIter a t => t -> 𝐼 a
iter ([ℤ64] -> 𝐼 ℤ64) -> [ℤ64] -> 𝐼 ℤ64
forall a b. (a -> b) -> a -> b
$ if ℤ64
iN ℤ64 -> ℤ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≢ ℤ64
i then [ℤ64
iN] else []
          , [ℤ64] -> 𝐼 ℤ64
forall a t. ToIter a t => t -> 𝐼 a
iter [ℤ64
iPℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
1,ℤ64
iNℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
1,ℤ64
iPℤ64 -> ℤ64 -> ℤ64
forall a. Minus a => a -> a -> a
-ℤ64
2,ℤ64
iNℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ℤ64
2,ℤ64
iPℤ64 -> ℤ64 -> ℤ64
forall a. DivMod a => a -> a -> a
⌿ℤ64
2,ℤ64
iNℤ64 -> ℤ64 -> ℤ64
forall a. DivMod a => a -> a -> a
⌿ℤ64
2]
          ]

instance (Shrinky a,Shrinky b) ⇒ Shrinky (a,b) where
  shrink :: (a, b) -> 𝐼 (a, b)
shrink (a
x,b
y) = [𝐼 (a, b)] -> 𝐼 (a, b)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ do a
x' ← a -> 𝐼 a
forall a. Shrinky a => a -> 𝐼 a
shrink a
x ; (a, b) -> 𝐼 (a, b)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (a
x',b
y )
    , do b
y' ← b -> 𝐼 b
forall a. Shrinky a => a -> 𝐼 a
shrink b
y ; (a, b) -> 𝐼 (a, b)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (a
x ,b
y')
    ]

instance (Shrinky a,Shrinky b,Shrinky c) ⇒ Shrinky (a,b,c) where
  shrink :: (a, b, c) -> 𝐼 (a, b, c)
shrink (a
x,b
y,c
z) = do
    (a
x',(b
y',c
z')) ← (a, (b, c)) -> 𝐼 (a, (b, c))
forall a. Shrinky a => a -> 𝐼 a
shrink (a
x,(b
y,c
z))
    (a, b, c) -> 𝐼 (a, b, c)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (a
x',b
y',c
z')

instance (Shrinky a) ⇒ Shrinky (𝑂 a) where
  shrink :: 𝑂 a -> 𝐼 (𝑂 a)
shrink = \case
    𝑂 a
None → 𝐼 (𝑂 a)
forall a. Null a => a
null
    Some a
a → [𝐼 (𝑂 a)] -> 𝐼 (𝑂 a)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ 𝑂 a -> 𝐼 (𝑂 a)
forall a t. Single a t => a -> t
single 𝑂 a
forall a. 𝑂 a
None
      , a -> 𝑂 a
forall a. a -> 𝑂 a
Some (a -> 𝑂 a) -> 𝐼 a -> 𝐼 (𝑂 a)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ a -> 𝐼 a
forall a. Shrinky a => a -> 𝐼 a
shrink a
a
      ]

instance (Shrinky a,Shrinky b) ⇒ Shrinky (a ∧ b) where
  shrink :: (a ∧ b) -> 𝐼 (a ∧ b)
shrink (a
x :* b
y) = do
    (a
x',b
y') ← (a, b) -> 𝐼 (a, b)
forall a. Shrinky a => a -> 𝐼 a
shrink (a
x,b
y) 
    (a ∧ b) -> 𝐼 (a ∧ b)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∧ b) -> 𝐼 (a ∧ b)) -> (a ∧ b) -> 𝐼 (a ∧ b)
forall a b. (a -> b) -> a -> b
$ a
x' a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
y'

instance (Shrinky a,Shrinky b) ⇒ Shrinky (a ∨ b) where
  shrink :: (a ∨ b) -> 𝐼 (a ∨ b)
shrink = \case
    Inl a
x → a -> a ∨ b
forall a b. a -> a ∨ b
Inl (a -> a ∨ b) -> 𝐼 a -> 𝐼 (a ∨ b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ a -> 𝐼 a
forall a. Shrinky a => a -> 𝐼 a
shrink a
x
    Inr b
y → b -> a ∨ b
forall a b. b -> a ∨ b
Inr (b -> a ∨ b) -> 𝐼 b -> 𝐼 (a ∨ b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ b -> 𝐼 b
forall a. Shrinky a => a -> 𝐼 a
shrink b
y

instance (Shrinky a) ⇒ Shrinky (𝐿 a) where
  shrink :: 𝐿 a -> 𝐼 (𝐿 a)
shrink = \case
    𝐿 a
Nil → 𝐼 (𝐿 a)
forall a. Null a => a
null
    a
x :& 𝐿 a
xs → [𝐼 (𝐿 a)] -> 𝐼 (𝐿 a)
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ 𝐿 a -> 𝐼 (𝐿 a)
forall a t. Single a t => a -> t
single 𝐿 a
xs
      , do (a
x',𝐿 a
xs') ← (a, 𝐿 a) -> 𝐼 (a, 𝐿 a)
forall a. Shrinky a => a -> 𝐼 a
shrink (a
x,𝐿 a
xs) ; 𝐿 a -> 𝐼 (𝐿 a)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 a -> 𝐼 (𝐿 a)) -> 𝐿 a -> 𝐼 (𝐿 a)
forall a b. (a -> b) -> a -> b
$ a
x' a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 a
xs'
      ]

instance (Shrinky a) ⇒ Shrinky (𝐼 a) where shrink :: 𝐼 a -> 𝐼 (𝐼 a)
shrink = (𝐿 a -> 𝐼 a) -> 𝐼 (𝐿 a) -> 𝐼 (𝐼 a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝐿 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter (𝐼 (𝐿 a) -> 𝐼 (𝐼 a)) -> (𝐿 a -> 𝐼 (𝐿 a)) -> 𝐿 a -> 𝐼 (𝐼 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 a -> 𝐼 (𝐿 a)
forall a. Shrinky a => a -> 𝐼 a
shrink (𝐿 a -> 𝐼 (𝐼 a)) -> (𝐼 a -> 𝐿 a) -> 𝐼 a -> 𝐼 (𝐼 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 a -> 𝐿 a
forall a t. ToIter a t => t -> 𝐿 a
list
instance (Shrinky a) ⇒ Shrinky (𝕍 a) where shrink :: 𝕍 a -> 𝐼 (𝕍 a)
shrink = (𝐿 a -> 𝕍 a) -> 𝐼 (𝐿 a) -> 𝐼 (𝕍 a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝐿 a -> 𝕍 a
forall a t. ToIter a t => t -> 𝕍 a
vec (𝐼 (𝐿 a) -> 𝐼 (𝕍 a)) -> (𝐿 a -> 𝐼 (𝐿 a)) -> 𝐿 a -> 𝐼 (𝕍 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 a -> 𝐼 (𝐿 a)
forall a. Shrinky a => a -> 𝐼 a
shrink (𝐿 a -> 𝐼 (𝕍 a)) -> (𝕍 a -> 𝐿 a) -> 𝕍 a -> 𝐼 (𝕍 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕍 a -> 𝐿 a
forall a t. ToIter a t => t -> 𝐿 a
list

shrinkAssoc ∷ (Shrinky v) ⇒ 𝐿 (k ∧ v) → 𝐼 (𝐿 (k ∧ v))
shrinkAssoc :: forall v k. Shrinky v => 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
shrinkAssoc = \case
  𝐿 (k ∧ v)
Nil → 𝐼 (𝐿 (k ∧ v))
forall a. Null a => a
null
  (k
k :* v
v) :& 𝐿 (k ∧ v)
kvs → [𝐼 (𝐿 (k ∧ v))] -> 𝐼 (𝐿 (k ∧ v))
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall a t. Single a t => a -> t
single 𝐿 (k ∧ v)
kvs
    , do v
v'   ← v -> 𝐼 v
forall a. Shrinky a => a -> 𝐼 a
shrink      v
v   ; 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))) -> 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall a b. (a -> b) -> a -> b
$ (k
k k -> v -> k ∧ v
forall a b. a -> b -> a ∧ b
:* v
v') (k ∧ v) -> 𝐿 (k ∧ v) -> 𝐿 (k ∧ v)
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 (k ∧ v)
kvs
    , do 𝐿 (k ∧ v)
kvs' ← 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall v k. Shrinky v => 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
shrinkAssoc 𝐿 (k ∧ v)
kvs ; 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))) -> 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall a b. (a -> b) -> a -> b
$ (k
k k -> v -> k ∧ v
forall a b. a -> b -> a ∧ b
:* v
v ) (k ∧ v) -> 𝐿 (k ∧ v) -> 𝐿 (k ∧ v)
forall a. a -> 𝐿 a -> 𝐿 a
:& 𝐿 (k ∧ v)
kvs'
    ]

instance (Ord k,Shrinky v) ⇒ Shrinky (k ⇰ v) where
  shrink :: (k ⇰ v) -> 𝐼 (k ⇰ v)
shrink = (𝐿 (k ∧ v) -> k ⇰ v) -> 𝐼 (𝐿 (k ∧ v)) -> 𝐼 (k ⇰ v)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝐿 (k ∧ v) -> k ⇰ v
forall (d :: * -> *) t a k s.
(Dict k s d, ToIter (k ∧ a) t) =>
t -> d a
assoc (𝐼 (𝐿 (k ∧ v)) -> 𝐼 (k ⇰ v))
-> (𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))) -> 𝐿 (k ∧ v) -> 𝐼 (k ⇰ v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
forall v k. Shrinky v => 𝐿 (k ∧ v) -> 𝐼 (𝐿 (k ∧ v))
shrinkAssoc (𝐿 (k ∧ v) -> 𝐼 (k ⇰ v))
-> ((k ⇰ v) -> 𝐿 (k ∧ v)) -> (k ⇰ v) -> 𝐼 (k ⇰ v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (k ⇰ v) -> 𝐿 (k ∧ v)
forall a t. ToIter a t => t -> 𝐿 a
list


shrunkR ∷ (Shrinky a) ⇒ (a → 𝔹) → ℕ64 → a → 𝑆 a → ℕ64 ∧ a
shrunkR :: forall a. Shrinky a => (a -> 𝔹) -> ℕ64 -> a -> 𝑆 a -> ℕ64 ∧ a
shrunkR a -> 𝔹
p =
  let outerLoop :: ℕ64 -> a -> 𝑆 a -> ℕ64 ∧ a
outerLoop ℕ64
n a
x₀ =
        let loop :: 𝑆 a -> ℕ64 ∧ a
loop 𝑆 a
xs = case 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
forall a. 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
un𝑆 𝑆 a
xs () of
              𝑂 (a ∧ 𝑆 a)
None → ℕ64
n ℕ64 -> a -> ℕ64 ∧ a
forall a b. a -> b -> a ∧ b
:* a
x₀
              Some (a
x  :* 𝑆 a
xs') →
                if a -> 𝔹
p a
x 
                then ℕ64 -> a -> 𝑆 a -> ℕ64 ∧ a
outerLoop (ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
1) a
x (𝑆 a -> ℕ64 ∧ a) -> 𝑆 a -> ℕ64 ∧ a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream (𝐼 a -> 𝑆 a) -> 𝐼 a -> 𝑆 a
forall a b. (a -> b) -> a -> b
$ a -> 𝐼 a
forall a. Shrinky a => a -> 𝐼 a
shrink a
x
                else 𝑆 a -> ℕ64 ∧ a
loop 𝑆 a
xs'
        in 𝑆 a -> ℕ64 ∧ a
loop
  in ℕ64 -> a -> 𝑆 a -> ℕ64 ∧ a
outerLoop

shrunk ∷ (Shrinky a) ⇒ (a → 𝔹) → a → ℕ64 ∧ a
shrunk :: forall a. Shrinky a => (a -> 𝔹) -> a -> ℕ64 ∧ a
shrunk a -> 𝔹
p a
x = (a -> 𝔹) -> ℕ64 -> a -> 𝑆 a -> ℕ64 ∧ a
forall a. Shrinky a => (a -> 𝔹) -> ℕ64 -> a -> 𝑆 a -> ℕ64 ∧ a
shrunkR a -> 𝔹
p ℕ64
0 a
x (𝑆 a -> ℕ64 ∧ a) -> 𝑆 a -> ℕ64 ∧ a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream (𝐼 a -> 𝑆 a) -> 𝐼 a -> 𝑆 a
forall a b. (a -> b) -> a -> b
$ a -> 𝐼 a
forall a. Shrinky a => a -> 𝐼 a
shrink a
x