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