{-# LANGUAGE ImportQualifiedPost #-}

module Constrained.Examples.Either where

import Data.Set qualified as Set

import Constrained

eitherSpec :: Specification BaseFn (Either Int Int)
eitherSpec :: Specification BaseFn (Either Int Int)
eitherSpec = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Either Int Int)
e ->
  (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term BaseFn (Either Int Int)
e)
    (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0)
    (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i -> Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
0 forall a (fn :: [*] -> * -> *).
(Ord a, OrdLike fn a) =>
Term fn a -> Term fn a -> Term fn Bool
<=. Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
i)

foldTrueCases :: Specification BaseFn (Either Int Int)
foldTrueCases :: Specification BaseFn (Either Int Int)
foldTrueCases = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term BaseFn (Either Int Int)
x ->
  [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *).
BaseUniverse fn =>
Term fn Bool -> Term fn Bool
not_ forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term BaseFn (Either Int Int)
x (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (forall a. Ord a => [a] -> Set a
Set.fromList [forall a b. a -> Either a b
Left Int
10]))
  , forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
Term fn a -> (Term fn a -> p) -> Pred fn
letBind (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term BaseFn (Either Int Int)
x (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit (Int
0 :: Int))) forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Either Int Int, Int)
p ->
      forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
        (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  (Either Int Int, Int)
p)
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
_ -> Bool
True)
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term
  (Fix
     (Oneof
        (Oneof
           (Oneof MapFn (Oneof PairFn ListFn))
           (Oneof FunFn (Oneof SetFn OrdFn)))
        (Oneof
           (Oneof SumFn (Oneof BoolFn GenericsFn))
           (Oneof SizeFn (Oneof EqFn IntFn)))))
  Int
_ -> Bool
True)
  ]