{-# LANGUAGE ImportQualifiedPost #-} module Constrained.Examples.Either where import Constrained.API import Data.Set qualified as Set eitherSpec :: Specification (Either Int Int) eitherSpec :: Specification (Either Int Int) eitherSpec = (Term (Either Int Int) -> Pred) -> Specification (Either Int Int) forall a p. (IsPred p, HasSpec a) => (Term a -> p) -> Specification a constrained ((Term (Either Int Int) -> Pred) -> Specification (Either Int Int)) -> (Term (Either Int Int) -> Pred) -> Specification (Either Int Int) forall a b. (a -> b) -> a -> b $ \Term (Either Int Int) e -> (Term (Either Int Int) -> FunTy (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int)))) Pred forall a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term a -> FunTy (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred caseOn Term (Either Int Int) e) (FunTy (MapList Term (Args Int)) (Term Bool) -> Weighted (BinderD Deps) Int forall p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) => FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a branch (FunTy (MapList Term (Args Int)) (Term Bool) -> Weighted (BinderD Deps) Int) -> FunTy (MapList Term (Args Int)) (Term Bool) -> Weighted (BinderD Deps) Int forall a b. (a -> b) -> a -> b $ \Term Int i -> Term Int i Term Int -> Term Int -> Term Bool forall a. OrdLike a => Term a -> Term a -> Term Bool <=. Term Int 0) (FunTy (MapList Term (Args Int)) (Term Bool) -> Weighted (BinderD Deps) Int forall p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) => FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a branch (FunTy (MapList Term (Args Int)) (Term Bool) -> Weighted (BinderD Deps) Int) -> FunTy (MapList Term (Args Int)) (Term Bool) -> Weighted (BinderD Deps) Int forall a b. (a -> b) -> a -> b $ \Term Int i -> Term Int 0 Term Int -> Term Int -> Term Bool forall a. OrdLike a => Term a -> Term a -> Term Bool <=. Term Int i) foldTrueCases :: Specification (Either Int Int) foldTrueCases :: Specification (Either Int Int) foldTrueCases = (Term (Either Int Int) -> [Pred]) -> Specification (Either Int Int) forall a p. (IsPred p, HasSpec a) => (Term a -> p) -> Specification a constrained ((Term (Either Int Int) -> [Pred]) -> Specification (Either Int Int)) -> (Term (Either Int Int) -> [Pred]) -> Specification (Either Int Int) forall a b. (a -> b) -> a -> b $ \Term (Either Int Int) x -> [ Term Bool -> Pred forall p. IsPred p => p -> Pred assert (Term Bool -> Pred) -> Term Bool -> Pred forall a b. (a -> b) -> a -> b $ Term Bool -> Term Bool not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool forall a b. (a -> b) -> a -> b $ Term (Either Int Int) -> Term (Set (Either Int Int)) -> Term Bool forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool member_ Term (Either Int Int) x (Set (Either Int Int) -> Term (Set (Either Int Int)) forall a. HasSpec a => a -> Term a lit ([Either Int Int] -> Set (Either Int Int) forall a. Ord a => [a] -> Set a Set.fromList [Int -> Either Int Int forall a b. a -> Either a b Left Int 10])) , Term (Either Int Int, Int) -> (Term (Either Int Int, Int) -> Pred) -> Pred forall a p. (HasSpec a, IsPred p) => Term a -> (Term a -> p) -> Pred letBind (Term (Either Int Int) -> Term Int -> Term (Either Int Int, Int) forall a b. (HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) => Term a -> Term b -> Term (a, b) pair_ Term (Either Int Int) x (Int -> Term Int forall a. HasSpec a => a -> Term a lit (Int 0 :: Int))) ((Term (Either Int Int, Int) -> Pred) -> Pred) -> (Term (Either Int Int, Int) -> Pred) -> Pred forall a b. (a -> b) -> a -> b $ \Term (Either Int Int, Int) p -> Term (Either Int Int) -> FunTy (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep (Either Int Int)))) Pred forall a. (GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)), TypeList (Cases (SimpleRep a))) => Term a -> FunTy (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred caseOn (Term (Either Int Int, Int) -> Term (Either Int Int) forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term x fst_ Term (Either Int Int, Int) p) (FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int forall p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) => FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a branch (FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int) -> FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int forall a b. (a -> b) -> a -> b $ \Term Int _ -> Bool True) (FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int forall p a. (HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) => FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a branch (FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int) -> FunTy (MapList Term (Args Int)) Bool -> Weighted (BinderD Deps) Int forall a b. (a -> b) -> a -> b $ \Term Int _ -> Bool True) ]