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