{-# 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)
  ]