{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Core.Data.Class.ITEOp
( ITEOp (..),
)
where
import GHC.TypeNats (KnownNat, type (<=))
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.Prim.Term
( LinkedRep,
SupportedPrim (pevalITETerm),
)
import Grisette.Internal.SymPrim.SymBV
( SymIntN (SymIntN),
SymWordN (SymWordN),
)
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
class ITEOp v where
symIte :: SymBool -> v -> v -> v
#define ITEOP_SIMPLE(type) \
instance ITEOp type where \
symIte (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \
{-# INLINE symIte #-}
#define ITEOP_BV(type) \
instance (KnownNat n, 1 <= n) => ITEOp (type n) where \
symIte (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \
{-# INLINE symIte #-}
#define ITEOP_FUN(cop, op, cons) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => ITEOp (op sa sb) where \
symIte (SymBool c) (cons t) (cons f) = cons $ pevalITETerm c t f; \
{-# INLINE symIte #-}
#if 1
ITEOP_SIMPLE(SymBool)
ITEOP_SIMPLE(SymInteger)
ITEOP_BV(SymIntN)
ITEOP_BV(SymWordN)
ITEOP_FUN((=->), (=~>), SymTabularFun)
ITEOP_FUN((-->), (-~>), SymGeneralFun)
#endif