{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Data.SBV.Tuple (
(^.), _1, _2, _3, _4, _5, _6, _7, _8
, tuple, untuple
) where
import GHC.TypeLits
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic
import Data.SBV.Core.Model
(^.) :: a -> (a -> b) -> b
t ^. f = f t
infixl 8 ^.
symbolicFieldAccess :: (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess i tup
| 1 > i || i > lks
= bad $ "Index is out of bounds, " ++ show i ++ " is outside [1," ++ show lks ++ "]"
| SBV (SVal kval (Left v)) <- tup
= case cvVal v of
CTuple vs | kval /= ktup -> bad $ "Kind/value mismatch: " ++ show kval
| length vs /= lks -> bad $ "Value has fewer elements: " ++ show (CV kval (CTuple vs))
| True -> literal $ fromCV $ CV kElem (vs !! (i-1))
_ -> bad $ "Kind/value mismatch: " ++ show v
| True
= symAccess
where ktup = kindOf tup
(lks, eks) = case ktup of
KTuple ks -> (length ks, ks)
_ -> bad "Was expecting to receive a tuple!"
kElem = eks !! (i-1)
bad :: String -> a
bad problem = error $ unlines [ "*** Data.SBV.field: Impossible happened"
, "*** Accessing element: " ++ show i
, "*** Argument kind : " ++ show ktup
, "*** Problem : " ++ problem
, "*** Please report this as a bug!"
]
symAccess :: SBV a
symAccess = SBV $ SVal kElem $ Right $ cache y
where y st = do sv <- svToSV st $ unSBV tup
newExpr st kElem (SBVApp (TupleAccess i lks) [sv])
data Label (l :: Symbol) = Get
class (SymVal elt, HasKind tup) => HasField l elt tup | l tup -> elt where
field :: Label l -> SBV tup -> SBV elt
instance (HasKind a, HasKind b , SymVal a) => HasField "_1" a (a, b) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b, HasKind c , SymVal a) => HasField "_1" a (a, b, c) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b, HasKind c, HasKind d , SymVal a) => HasField "_1" a (a, b, c, d) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e , SymVal a) => HasField "_1" a (a, b, c, d, e) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f , SymVal a) => HasField "_1" a (a, b, c, d, e, f) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal a) => HasField "_1" a (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal a) => HasField "_1" a (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 1
instance (HasKind a, HasKind b , SymVal b) => HasField "_2" b (a, b) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c , SymVal b) => HasField "_2" b (a, b, c) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c, HasKind d , SymVal b) => HasField "_2" b (a, b, c, d) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e , SymVal b) => HasField "_2" b (a, b, c, d, e) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f , SymVal b) => HasField "_2" b (a, b, c, d, e, f) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal b) => HasField "_2" b (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal b) => HasField "_2" b (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 2
instance (HasKind a, HasKind b, HasKind c , SymVal c) => HasField "_3" c (a, b, c) where field _ = symbolicFieldAccess 3
instance (HasKind a, HasKind b, HasKind c, HasKind d , SymVal c) => HasField "_3" c (a, b, c, d) where field _ = symbolicFieldAccess 3
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e , SymVal c) => HasField "_3" c (a, b, c, d, e) where field _ = symbolicFieldAccess 3
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f , SymVal c) => HasField "_3" c (a, b, c, d, e, f) where field _ = symbolicFieldAccess 3
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal c) => HasField "_3" c (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 3
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal c) => HasField "_3" c (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 3
instance (HasKind a, HasKind b, HasKind c, HasKind d , SymVal d) => HasField "_4" d (a, b, c, d) where field _ = symbolicFieldAccess 4
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e , SymVal d) => HasField "_4" d (a, b, c, d, e) where field _ = symbolicFieldAccess 4
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f , SymVal d) => HasField "_4" d (a, b, c, d, e, f) where field _ = symbolicFieldAccess 4
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal d) => HasField "_4" d (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 4
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal d) => HasField "_4" d (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 4
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e , SymVal e) => HasField "_5" e (a, b, c, d, e) where field _ = symbolicFieldAccess 5
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f , SymVal e) => HasField "_5" e (a, b, c, d, e, f) where field _ = symbolicFieldAccess 5
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal e) => HasField "_5" e (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 5
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal e) => HasField "_5" e (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 5
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f , SymVal f) => HasField "_6" f (a, b, c, d, e, f) where field _ = symbolicFieldAccess 6
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal f) => HasField "_6" f (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 6
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal f) => HasField "_6" f (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 6
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g , SymVal g) => HasField "_7" g (a, b, c, d, e, f, g) where field _ = symbolicFieldAccess 7
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal g) => HasField "_7" g (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 7
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e, HasKind f, HasKind g, HasKind h, SymVal h) => HasField "_8" h (a, b, c, d, e, f, g, h) where field _ = symbolicFieldAccess 8
_1 :: HasField "_1" b a => SBV a -> SBV b
_1 = field (Get @"_1")
_2 :: HasField "_2" b a => SBV a -> SBV b
_2 = field (Get @"_2")
_3 :: HasField "_3" b a => SBV a -> SBV b
_3 = field (Get @"_3")
_4 :: HasField "_4" b a => SBV a -> SBV b
_4 = field (Get @"_4")
_5 :: HasField "_5" b a => SBV a -> SBV b
_5 = field (Get @"_5")
_6 :: HasField "_6" b a => SBV a -> SBV b
_6 = field (Get @"_6")
_7 :: HasField "_7" b a => SBV a -> SBV b
_7 = field (Get @"_7")
_8 :: HasField "_8" b a => SBV a -> SBV b
_8 = field (Get @"_8")
class Tuple tup a | a -> tup, tup -> a where
untuple :: SBV tup -> a
tuple :: a -> SBV tup
instance (SymVal a, SymVal b) => Tuple (a, b) (SBV a, SBV b) where
untuple p = (p^._1, p^._2)
tuple p@(sa, sb)
| Just a <- unliteral sa, Just b <- unliteral sb
= literal (a, b)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
newExpr st k (SBVApp (TupleConstructor 2) [asv, bsv])
instance (SymVal a, SymVal b, SymVal c)
=> Tuple (a, b, c) (SBV a, SBV b, SBV c) where
untuple p = (p^._1, p^._2, p^._3)
tuple p@(sa, sb, sc)
| Just a <- unliteral sa, Just b <- unliteral sb, Just c <- unliteral sc
= literal (a, b, c)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
csv <- sbvToSV st sc
newExpr st k (SBVApp (TupleConstructor 3) [asv, bsv, csv])
instance (SymVal a, SymVal b, SymVal c, SymVal d)
=> Tuple (a, b, c, d) (SBV a, SBV b, SBV c, SBV d) where
untuple p = (p^._1, p^._2, p^._3, p^._4)
tuple p@(sa, sb, sc, sd)
| Just a <- unliteral sa, Just b <- unliteral sb, Just c <- unliteral sc, Just d <- unliteral sd
= literal (a, b, c, d)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
csv <- sbvToSV st sc
dsv <- sbvToSV st sd
newExpr st k (SBVApp (TupleConstructor 4) [asv, bsv, csv, dsv])
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e)
=> Tuple (a, b, c, d, e) (SBV a, SBV b, SBV c, SBV d, SBV e) where
untuple p = (p^._1, p^._2, p^._3, p^._4, p^._5)
tuple p@(sa, sb, sc, sd, se)
| Just a <- unliteral sa, Just b <- unliteral sb, Just c <- unliteral sc, Just d <- unliteral sd, Just e <- unliteral se
= literal (a, b, c, d, e)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
csv <- sbvToSV st sc
dsv <- sbvToSV st sd
esv <- sbvToSV st se
newExpr st k (SBVApp (TupleConstructor 5) [asv, bsv, csv, dsv, esv])
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f)
=> Tuple (a, b, c, d, e, f) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
untuple p = (p^._1, p^._2, p^._3, p^._4, p^._5, p^._6)
tuple p@(sa, sb, sc, sd, se, sf)
| Just a <- unliteral sa, Just b <- unliteral sb, Just c <- unliteral sc, Just d <- unliteral sd, Just e <- unliteral se, Just f <- unliteral sf
= literal (a, b, c, d, e, f)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
csv <- sbvToSV st sc
dsv <- sbvToSV st sd
esv <- sbvToSV st se
fsv <- sbvToSV st sf
newExpr st k (SBVApp (TupleConstructor 6) [asv, bsv, csv, dsv, esv, fsv])
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g)
=> Tuple (a, b, c, d, e, f, g) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
untuple p = (p^._1, p^._2, p^._3, p^._4, p^._5, p^._6, p^._7)
tuple p@(sa, sb, sc, sd, se, sf, sg)
| Just a <- unliteral sa, Just b <- unliteral sb, Just c <- unliteral sc, Just d <- unliteral sd, Just e <- unliteral se, Just f <- unliteral sf, Just g <- unliteral sg
= literal (a, b, c, d, e, f, g)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
csv <- sbvToSV st sc
dsv <- sbvToSV st sd
esv <- sbvToSV st se
fsv <- sbvToSV st sf
gsv <- sbvToSV st sg
newExpr st k (SBVApp (TupleConstructor 7) [asv, bsv, csv, dsv, esv, fsv, gsv])
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h)
=> Tuple (a, b, c, d, e, f, g, h) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) where
untuple p = (p^._1, p^._2, p^._3, p^._4, p^._5, p^._6, p^._7, p^._8)
tuple p@(sa, sb, sc, sd, se, sf, sg, sh)
| Just a <- unliteral sa, Just b <- unliteral sb, Just c <- unliteral sc, Just d <- unliteral sd, Just e <- unliteral se, Just f <- unliteral sf, Just g <- unliteral sg, Just h <- unliteral sh
= literal (a, b, c, d, e, f, g, h)
| True
= SBV $ SVal k $ Right $ cache res
where k = kindOf p
res st = do asv <- sbvToSV st sa
bsv <- sbvToSV st sb
csv <- sbvToSV st sc
dsv <- sbvToSV st sd
esv <- sbvToSV st se
fsv <- sbvToSV st sf
gsv <- sbvToSV st sg
hsv <- sbvToSV st sh
newExpr st k (SBVApp (TupleConstructor 8) [asv, bsv, csv, dsv, esv, fsv, gsv, hsv])
instance ( SymVal a, Metric a
, SymVal b, Metric b)
=> Metric (a, b) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
instance ( SymVal a, Metric a
, SymVal b, Metric b
, SymVal c, Metric c)
=> Metric (a, b, c) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMinimize (nm ++ "^._3") (p^._3)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
msMaximize (nm ++ "^._3") (p^._3)
instance ( SymVal a, Metric a
, SymVal b, Metric b
, SymVal c, Metric c
, SymVal d, Metric d)
=> Metric (a, b, c, d) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMinimize (nm ++ "^._3") (p^._3)
msMinimize (nm ++ "^._4") (p^._4)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
msMaximize (nm ++ "^._3") (p^._3)
msMaximize (nm ++ "^._4") (p^._4)
instance ( SymVal a, Metric a
, SymVal b, Metric b
, SymVal c, Metric c
, SymVal d, Metric d
, SymVal e, Metric e)
=> Metric (a, b, c, d, e) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMinimize (nm ++ "^._3") (p^._3)
msMinimize (nm ++ "^._4") (p^._4)
msMinimize (nm ++ "^._5") (p^._5)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
msMaximize (nm ++ "^._3") (p^._3)
msMaximize (nm ++ "^._4") (p^._4)
msMaximize (nm ++ "^._5") (p^._5)
instance ( SymVal a, Metric a
, SymVal b, Metric b
, SymVal c, Metric c
, SymVal d, Metric d
, SymVal e, Metric e
, SymVal f, Metric f)
=> Metric (a, b, c, d, e, f) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMinimize (nm ++ "^._3") (p^._3)
msMinimize (nm ++ "^._4") (p^._4)
msMinimize (nm ++ "^._5") (p^._5)
msMinimize (nm ++ "^._6") (p^._6)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
msMaximize (nm ++ "^._3") (p^._3)
msMaximize (nm ++ "^._4") (p^._4)
msMaximize (nm ++ "^._5") (p^._5)
msMaximize (nm ++ "^._6") (p^._6)
instance ( SymVal a, Metric a
, SymVal b, Metric b
, SymVal c, Metric c
, SymVal d, Metric d
, SymVal e, Metric e
, SymVal f, Metric f
, SymVal g, Metric g)
=> Metric (a, b, c, d, e, f, g) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMinimize (nm ++ "^._3") (p^._3)
msMinimize (nm ++ "^._4") (p^._4)
msMinimize (nm ++ "^._5") (p^._5)
msMinimize (nm ++ "^._6") (p^._6)
msMinimize (nm ++ "^._7") (p^._7)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
msMaximize (nm ++ "^._3") (p^._3)
msMaximize (nm ++ "^._4") (p^._4)
msMaximize (nm ++ "^._5") (p^._5)
msMaximize (nm ++ "^._6") (p^._6)
msMaximize (nm ++ "^._7") (p^._7)
instance ( SymVal a, Metric a
, SymVal b, Metric b
, SymVal c, Metric c
, SymVal d, Metric d
, SymVal e, Metric e
, SymVal f, Metric f
, SymVal g, Metric g
, SymVal h, Metric h)
=> Metric (a, b, c, d, e, f, g, h) where
msMinimize nm p = do msMinimize (nm ++ "^._1") (p^._1)
msMinimize (nm ++ "^._2") (p^._2)
msMinimize (nm ++ "^._3") (p^._3)
msMinimize (nm ++ "^._4") (p^._4)
msMinimize (nm ++ "^._5") (p^._5)
msMinimize (nm ++ "^._6") (p^._6)
msMinimize (nm ++ "^._7") (p^._7)
msMinimize (nm ++ "^._8") (p^._8)
msMaximize nm p = do msMaximize (nm ++ "^._1") (p^._1)
msMaximize (nm ++ "^._2") (p^._2)
msMaximize (nm ++ "^._3") (p^._3)
msMaximize (nm ++ "^._4") (p^._4)
msMaximize (nm ++ "^._5") (p^._5)
msMaximize (nm ++ "^._6") (p^._6)
msMaximize (nm ++ "^._7") (p^._7)
msMaximize (nm ++ "^._8") (p^._8)
{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}