-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Tuple
-- Copyright : (c) Joel Burget
--                 Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Accessing symbolic tuple fields and deconstruction.
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE Rank2Types             #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Tuple (
  -- * Symbolic field access
    (^.), _1, _2, _3, _4, _5, _6, _7, _8
  -- * Tupling and untupling
  , tuple, untuple
  ) where

import GHC.TypeLits

import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic
import Data.SBV.Core.Model

-- $setup
-- >>> -- For doctest purposes only:
-- >>> :set -XTypeApplications
-- >>> import Data.SBV

-- | Field access, inspired by the lens library. This is merely reverse
-- application, but allows us to write things like @(1, 2)^._1@ which is
-- likely to be familiar to most Haskell programmers out there. Note that
-- this is precisely equivalent to @_1 (1, 2)@, but perhaps it reads a little
-- nicer.
(^.) :: a -> (a -> b) -> b
a
t ^. :: a -> (a -> b) -> b
^. a -> b
f = a -> b
f a
t
infixl 8 ^.

-- | Dynamic interface to exporting tuples, this function is not
-- exported on purpose; use it only via the field functions '_1', '_2', etc.
symbolicFieldAccess :: (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess :: Int -> SBV tup -> SBV a
symbolicFieldAccess Int
i SBV tup
tup
  | Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i Bool -> Bool -> Bool
|| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
lks
  = String -> SBV a
forall a. String -> a
bad (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"Index is out of bounds, " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is outside [1," String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
lks String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
  | SBV (SVal Kind
kval (Left CV
v)) <- SBV tup
tup
  = case CV -> CVal
cvVal CV
v of
      CTuple [CVal]
vs | Kind
kval      Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
ktup -> String -> SBV a
forall a. String -> a
bad (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"Kind/value mismatch: "      String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
kval
                | [CVal] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CVal]
vs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
lks  -> String -> SBV a
forall a. String -> a
bad (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"Value has fewer elements: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show (Kind -> CVal -> CV
CV Kind
kval ([CVal] -> CVal
CTuple [CVal]
vs))
                | Bool
True              -> a -> SBV a
forall a. SymVal a => a -> SBV a
literal (a -> SBV a) -> a -> SBV a
forall a b. (a -> b) -> a -> b
$ CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> CV -> a
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
kElem ([CVal]
vs [CVal] -> Int -> CVal
forall a. [a] -> Int -> a
!! (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))
      CVal
_                             -> String -> SBV a
forall a. String -> a
bad (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ String
"Kind/value mismatch: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
v
  | Bool
True
  = SBV a
forall a. SBV a
symAccess
  where ktup :: Kind
ktup = SBV tup -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV tup
tup

        (Int
lks, [Kind]
eks) = case Kind
ktup of
                       KTuple [Kind]
ks -> ([Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks, [Kind]
ks)
                       Kind
_         -> String -> (Int, [Kind])
forall a. String -> a
bad String
"Was expecting to receive a tuple!"

        kElem :: Kind
kElem = [Kind]
eks [Kind] -> Int -> Kind
forall a. [a] -> Int -> a
!! (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

        bad :: String -> a
        bad :: String -> a
bad String
problem = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"*** Data.SBV.field: Impossible happened"
                                      , String
"***   Accessing element: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
                                      , String
"***   Argument kind    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
ktup
                                      , String
"***   Problem          : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
problem
                                      , String
"*** Please report this as a bug!"
                                      ]

        symAccess :: SBV a
        symAccess :: SBV a
symAccess = SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
kElem (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
y
          where y :: State -> IO SV
y State
st = do SV
sv <- State -> SVal -> IO SV
svToSV State
st (SVal -> IO SV) -> SVal -> IO SV
forall a b. (a -> b) -> a -> b
$ SBV tup -> SVal
forall a. SBV a -> SVal
unSBV SBV tup
tup
                          State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
kElem (Op -> [SV] -> SBVExpr
SBVApp (Int -> Int -> Op
TupleAccess Int
i Int
lks) [SV
sv])

-- | Field labels
data Label (l :: Symbol) = Get

-- | The class 'HasField' captures the notion that a type has a certain field
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 :: Label "_1" -> SBV (a, b) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
1
instance (HasKind a, HasKind b, HasKind c                                                       , SymVal a) => HasField "_1" a (a, b, c)                where field :: Label "_1" -> SBV (a, b, c) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b, c) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
1
instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal a) => HasField "_1" a (a, b, c, d)             where field :: Label "_1" -> SBV (a, b, c, d) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b, c, d) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
1
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal a) => HasField "_1" a (a, b, c, d, e)          where field :: Label "_1" -> SBV (a, b, c, d, e) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b, c, d, e) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_1" -> SBV (a, b, c, d, e, f) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b, c, d, e, f) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_1" -> SBV (a, b, c, d, e, f, g) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_1" -> SBV (a, b, c, d, e, f, g, h) -> SBV a
field Label "_1"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV a
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
1

instance (HasKind a, HasKind b                                                                  , SymVal b) => HasField "_2" b (a, b)                   where field :: Label "_2" -> SBV (a, b) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
2
instance (HasKind a, HasKind b, HasKind c                                                       , SymVal b) => HasField "_2" b (a, b, c)                where field :: Label "_2" -> SBV (a, b, c) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b, c) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
2
instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal b) => HasField "_2" b (a, b, c, d)             where field :: Label "_2" -> SBV (a, b, c, d) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b, c, d) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
2
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal b) => HasField "_2" b (a, b, c, d, e)          where field :: Label "_2" -> SBV (a, b, c, d, e) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b, c, d, e) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_2" -> SBV (a, b, c, d, e, f) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b, c, d, e, f) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_2" -> SBV (a, b, c, d, e, f, g) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_2" -> SBV (a, b, c, d, e, f, g, h) -> SBV b
field Label "_2"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV b
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
2

instance (HasKind a, HasKind b, HasKind c                                                       , SymVal c) => HasField "_3" c (a, b, c)                where field :: Label "_3" -> SBV (a, b, c) -> SBV c
field Label "_3"
_ = Int -> SBV (a, b, c) -> SBV c
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
3
instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal c) => HasField "_3" c (a, b, c, d)             where field :: Label "_3" -> SBV (a, b, c, d) -> SBV c
field Label "_3"
_ = Int -> SBV (a, b, c, d) -> SBV c
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
3
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal c) => HasField "_3" c (a, b, c, d, e)          where field :: Label "_3" -> SBV (a, b, c, d, e) -> SBV c
field Label "_3"
_ = Int -> SBV (a, b, c, d, e) -> SBV c
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_3" -> SBV (a, b, c, d, e, f) -> SBV c
field Label "_3"
_ = Int -> SBV (a, b, c, d, e, f) -> SBV c
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_3" -> SBV (a, b, c, d, e, f, g) -> SBV c
field Label "_3"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV c
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_3" -> SBV (a, b, c, d, e, f, g, h) -> SBV c
field Label "_3"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV c
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
3

instance (HasKind a, HasKind b, HasKind c, HasKind d                                            , SymVal d) => HasField "_4" d (a, b, c, d)             where field :: Label "_4" -> SBV (a, b, c, d) -> SBV d
field Label "_4"
_ = Int -> SBV (a, b, c, d) -> SBV d
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
4
instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal d) => HasField "_4" d (a, b, c, d, e)          where field :: Label "_4" -> SBV (a, b, c, d, e) -> SBV d
field Label "_4"
_ = Int -> SBV (a, b, c, d, e) -> SBV d
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_4" -> SBV (a, b, c, d, e, f) -> SBV d
field Label "_4"
_ = Int -> SBV (a, b, c, d, e, f) -> SBV d
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_4" -> SBV (a, b, c, d, e, f, g) -> SBV d
field Label "_4"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV d
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_4" -> SBV (a, b, c, d, e, f, g, h) -> SBV d
field Label "_4"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV d
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
4

instance (HasKind a, HasKind b, HasKind c, HasKind d, HasKind e                                 , SymVal e) => HasField "_5" e (a, b, c, d, e)          where field :: Label "_5" -> SBV (a, b, c, d, e) -> SBV e
field Label "_5"
_ = Int -> SBV (a, b, c, d, e) -> SBV e
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_5" -> SBV (a, b, c, d, e, f) -> SBV e
field Label "_5"
_ = Int -> SBV (a, b, c, d, e, f) -> SBV e
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_5" -> SBV (a, b, c, d, e, f, g) -> SBV e
field Label "_5"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV e
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_5" -> SBV (a, b, c, d, e, f, g, h) -> SBV e
field Label "_5"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV e
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_6" -> SBV (a, b, c, d, e, f) -> SBV f
field Label "_6"
_ = Int -> SBV (a, b, c, d, e, f) -> SBV f
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_6" -> SBV (a, b, c, d, e, f, g) -> SBV f
field Label "_6"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV f
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_6" -> SBV (a, b, c, d, e, f, g, h) -> SBV f
field Label "_6"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV f
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_7" -> SBV (a, b, c, d, e, f, g) -> SBV g
field Label "_7"
_ = Int -> SBV (a, b, c, d, e, f, g) -> SBV g
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_7" -> SBV (a, b, c, d, e, f, g, h) -> SBV g
field Label "_7"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV g
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
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 :: Label "_8" -> SBV (a, b, c, d, e, f, g, h) -> SBV h
field Label "_8"
_ = Int -> SBV (a, b, c, d, e, f, g, h) -> SBV h
forall a tup. (SymVal a, HasKind tup) => Int -> SBV tup -> SBV a
symbolicFieldAccess Int
8

-- | Access the 1st element of an @STupleN@, @2 <= N <= 8@. Also see '^.'.
_1 :: HasField "_1" b a => SBV a -> SBV b
_1 :: SBV a -> SBV b
_1 = Label "_1" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_1"
forall (l :: Symbol). Label l
Get @"_1")

-- | Access the 2nd element of an @STupleN@, @2 <= N <= 8@. Also see '^.'.
_2 :: HasField "_2" b a => SBV a -> SBV b
_2 :: SBV a -> SBV b
_2 = Label "_2" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_2"
forall (l :: Symbol). Label l
Get @"_2")

-- | Access the 3rd element of an @STupleN@, @3 <= N <= 8@. Also see '^.'.
_3 :: HasField "_3" b a => SBV a -> SBV b
_3 :: SBV a -> SBV b
_3 = Label "_3" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_3"
forall (l :: Symbol). Label l
Get @"_3")

-- | Access the 4th element of an @STupleN@, @4 <= N <= 8@. Also see '^.'.
_4 :: HasField "_4" b a => SBV a -> SBV b
_4 :: SBV a -> SBV b
_4 = Label "_4" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_4"
forall (l :: Symbol). Label l
Get @"_4")

-- | Access the 5th element of an @STupleN@, @5 <= N <= 8@. Also see '^.'.
_5 :: HasField "_5" b a => SBV a -> SBV b
_5 :: SBV a -> SBV b
_5 = Label "_5" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_5"
forall (l :: Symbol). Label l
Get @"_5")

-- | Access the 6th element of an @STupleN@, @6 <= N <= 8@. Also see '^.'.
_6 :: HasField "_6" b a => SBV a -> SBV b
_6 :: SBV a -> SBV b
_6 = Label "_6" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_6"
forall (l :: Symbol). Label l
Get @"_6")

-- | Access the 7th element of an @STupleN@, @7 <= N <= 8@. Also see '^.'.
_7 :: HasField "_7" b a => SBV a -> SBV b
_7 :: SBV a -> SBV b
_7 = Label "_7" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_7"
forall (l :: Symbol). Label l
Get @"_7")

-- | Access the 8th element of an @STupleN@, @8 <= N <= 8@. Also see '^.'.
_8 :: HasField "_8" b a => SBV a -> SBV b
_8 :: SBV a -> SBV b
_8 = Label "_8" -> SBV a -> SBV b
forall (l :: Symbol) elt tup.
HasField l elt tup =>
Label l -> SBV tup -> SBV elt
field (Label "_8"
forall (l :: Symbol). Label l
Get @"_8")

-- | Constructing a tuple from its parts and deconstructing back.
class Tuple tup a | a -> tup, tup -> a where
  -- | Deconstruct a tuple, getting its constituent parts apart. Forms an
  -- isomorphism pair with 'tuple':
  --
  -- >>> prove $ \p -> tuple @(Integer, Bool, (String, Char)) (untuple p) .== p
  -- Q.E.D.
  untuple :: SBV tup -> a

  -- | Constructing a tuple from its parts. Forms an isomorphism pair with 'untuple':
  --
  -- >>> prove $ \p -> untuple @(Integer, Bool, (String, Char)) (tuple p) .== p
  -- Q.E.D.
  tuple   :: a -> SBV tup

instance (SymVal a, SymVal b) => Tuple (a, b) (SBV a, SBV b) where
  untuple :: SBV (a, b) -> (SBV a, SBV b)
untuple SBV (a, b)
p = (SBV (a, b)
pSBV (a, b) -> (SBV (a, b) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b)
pSBV (a, b) -> (SBV (a, b) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)

  tuple :: (SBV a, SBV b) -> SBV (a, b)
tuple p :: (SBV a, SBV b)
p@(SBV a
sa, SBV b
sb)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb
    = (a, b) -> SBV (a, b)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b)
    | Bool
True
    = SVal -> SBV (a, b)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b)) -> SVal -> SBV (a, b)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
2) [SV
asv, SV
bsv])

instance (SymVal a, SymVal b, SymVal c)
      => Tuple (a, b, c) (SBV a, SBV b, SBV c) where
  untuple :: SBV (a, b, c) -> (SBV a, SBV b, SBV c)
untuple SBV (a, b, c)
p = (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)

  tuple :: (SBV a, SBV b, SBV c) -> SBV (a, b, c)
tuple p :: (SBV a, SBV b, SBV c)
p@(SBV a
sa, SBV b
sb, SBV c
sc)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc
    = (a, b, c) -> SBV (a, b, c)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c)
    | Bool
True
    = SVal -> SBV (a, b, c)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b, c)) -> SVal -> SBV (a, b, c)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b, SBV c) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
3) [SV
asv, SV
bsv, SV
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 :: SBV (a, b, c, d) -> (SBV a, SBV b, SBV c, SBV d)
untuple SBV (a, b, c, d)
p = (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)

  tuple :: (SBV a, SBV b, SBV c, SBV d) -> SBV (a, b, c, d)
tuple p :: (SBV a, SBV b, SBV c, SBV d)
p@(SBV a
sa, SBV b
sb, SBV c
sc, SBV d
sd)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- SBV d -> Maybe d
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd
    = (a, b, c, d) -> SBV (a, b, c, d)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d)
    | Bool
True
    = SVal -> SBV (a, b, c, d)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b, c, d)) -> SVal -> SBV (a, b, c, d)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b, SBV c, SBV d) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c, SBV d)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- State -> SBV d -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
4) [SV
asv, SV
bsv, SV
csv, SV
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 :: SBV (a, b, c, d, e) -> (SBV a, SBV b, SBV c, SBV d, SBV e)
untuple SBV (a, b, c, d, e)
p = (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)

  tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> SBV (a, b, c, d, e)
tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e)
p@(SBV a
sa, SBV b
sb, SBV c
sc, SBV d
sd, SBV e
se)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- SBV d -> Maybe d
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- SBV e -> Maybe e
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se
    = (a, b, c, d, e) -> SBV (a, b, c, d, e)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e)
    | Bool
True
    = SVal -> SBV (a, b, c, d, e)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b, c, d, e)) -> SVal -> SBV (a, b, c, d, e)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b, SBV c, SBV d, SBV e) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c, SBV d, SBV e)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- State -> SBV d -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- State -> SBV e -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
5) [SV
asv, SV
bsv, SV
csv, SV
dsv, SV
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 :: SBV (a, b, c, d, e, f)
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
untuple SBV (a, b, c, d, e, f)
p = (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5, SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)

  tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
-> SBV (a, b, c, d, e, f)
tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
p@(SBV a
sa, SBV b
sb, SBV c
sc, SBV d
sd, SBV e
se, SBV f
sf)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- SBV d -> Maybe d
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- SBV e -> Maybe e
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se, Just f
f <- SBV f -> Maybe f
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV f
sf
    = (a, b, c, d, e, f) -> SBV (a, b, c, d, e, f)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e, f
f)
    | Bool
True
    = SVal -> SBV (a, b, c, d, e, f)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b, c, d, e, f)) -> SVal -> SBV (a, b, c, d, e, f)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- State -> SBV d -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- State -> SBV e -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      SV
fsv <- State -> SBV f -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV f
sf
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
6) [SV
asv, SV
bsv, SV
csv, SV
dsv, SV
esv, SV
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 :: SBV (a, b, c, d, e, f, g)
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
untuple SBV (a, b, c, d, e, f, g)
p = (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5, SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6, SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV g) -> SBV g
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV g
forall b a. HasField "_7" b a => SBV a -> SBV b
_7)

  tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
-> SBV (a, b, c, d, e, f, g)
tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
p@(SBV a
sa, SBV b
sb, SBV c
sc, SBV d
sd, SBV e
se, SBV f
sf, SBV g
sg)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- SBV d -> Maybe d
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- SBV e -> Maybe e
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se, Just f
f <- SBV f -> Maybe f
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV f
sf, Just g
g <- SBV g -> Maybe g
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV g
sg
    = (a, b, c, d, e, f, g) -> SBV (a, b, c, d, e, f, g)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e, f
f, g
g)
    | Bool
True
    = SVal -> SBV (a, b, c, d, e, f, g)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b, c, d, e, f, g))
-> SVal -> SBV (a, b, c, d, e, f, g)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- State -> SBV d -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- State -> SBV e -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      SV
fsv <- State -> SBV f -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV f
sf
                      SV
gsv <- State -> SBV g -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV g
sg
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
7) [SV
asv, SV
bsv, SV
csv, SV
dsv, SV
esv, SV
fsv, SV
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 :: SBV (a, b, c, d, e, f, g, h)
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
untuple SBV (a, b, c, d, e, f, g, h)
p = (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV g) -> SBV g
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV g
forall b a. HasField "_7" b a => SBV a -> SBV b
_7, SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV h) -> SBV h
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV h
forall b a. HasField "_8" b a => SBV a -> SBV b
_8)

  tuple :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
-> SBV (a, b, c, d, e, f, g, h)
tuple p :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
p@(SBV a
sa, SBV b
sb, SBV c
sc, SBV d
sd, SBV e
se, SBV f
sf, SBV g
sg, SBV h
sh)
    | Just a
a <- SBV a -> Maybe a
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV a
sa, Just b
b <- SBV b -> Maybe b
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV b
sb, Just c
c <- SBV c -> Maybe c
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV c
sc, Just d
d <- SBV d -> Maybe d
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV d
sd, Just e
e <- SBV e -> Maybe e
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV e
se, Just f
f <- SBV f -> Maybe f
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV f
sf, Just g
g <- SBV g -> Maybe g
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV g
sg, Just h
h <- SBV h -> Maybe h
forall a. SymVal a => SBV a -> Maybe a
unliteral SBV h
sh
    = (a, b, c, d, e, f, g, h) -> SBV (a, b, c, d, e, f, g, h)
forall a. SymVal a => a -> SBV a
literal (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h)
    | Bool
True
    = SVal -> SBV (a, b, c, d, e, f, g, h)
forall a. SVal -> SBV a
SBV (SVal -> SBV (a, b, c, d, e, f, g, h))
-> SVal -> SBV (a, b, c, d, e, f, g, h)
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
res
    where k :: Kind
k      = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> Kind
forall a. HasKind a => a -> Kind
kindOf (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h)
p
          res :: State -> IO SV
res State
st = do SV
asv <- State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV a
sa
                      SV
bsv <- State -> SBV b -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV b
sb
                      SV
csv <- State -> SBV c -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV c
sc
                      SV
dsv <- State -> SBV d -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV d
sd
                      SV
esv <- State -> SBV e -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV e
se
                      SV
fsv <- State -> SBV f -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV f
sf
                      SV
gsv <- State -> SBV g -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV g
sg
                      SV
hsv <- State -> SBV h -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBV h
sh
                      State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (Int -> Op
TupleConstructor Int
8) [SV
asv, SV
bsv, SV
csv, SV
dsv, SV
esv, SV
fsv, SV
gsv, SV
hsv])

-- Optimization for tuples

-- 2-tuple
instance ( SymVal a, Metric a
         , SymVal b, Metric b)
         => Metric (a, b) where
   msMinimize :: String -> SBV (a, b) -> m ()
msMinimize String
nm SBV (a, b)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b)
pSBV (a, b) -> (SBV (a, b) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b)
pSBV (a, b) -> (SBV (a, b) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
   msMaximize :: String -> SBV (a, b) -> m ()
msMaximize String
nm SBV (a, b)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b)
pSBV (a, b) -> (SBV (a, b) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b)
pSBV (a, b) -> (SBV (a, b) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)

-- 3-tuple
instance ( SymVal a, Metric a
         , SymVal b, Metric b
         , SymVal c, Metric c)
         => Metric (a, b, c) where
   msMinimize :: String -> SBV (a, b, c) -> m ()
msMinimize String
nm SBV (a, b, c)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
   msMaximize :: String -> SBV (a, b, c) -> m ()
msMaximize String
nm SBV (a, b, c)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c)
pSBV (a, b, c) -> (SBV (a, b, c) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)

-- 4-tuple
instance ( SymVal a, Metric a
         , SymVal b, Metric b
         , SymVal c, Metric c
         , SymVal d, Metric d)
         => Metric (a, b, c, d) where
   msMinimize :: String -> SBV (a, b, c, d) -> m ()
msMinimize String
nm SBV (a, b, c, d)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
   msMaximize :: String -> SBV (a, b, c, d) -> m ()
msMaximize String
nm SBV (a, b, c, d)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d)
pSBV (a, b, c, d) -> (SBV (a, b, c, d) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)

-- 5-tuple
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 :: String -> SBV (a, b, c, d, e) -> m ()
msMinimize String
nm SBV (a, b, c, d, e)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
   msMaximize :: String -> SBV (a, b, c, d, e) -> m ()
msMaximize String
nm SBV (a, b, c, d, e)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e)
pSBV (a, b, c, d, e) -> (SBV (a, b, c, d, e) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)

-- 6-tuple
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 :: String -> SBV (a, b, c, d, e, f) -> m ()
msMinimize String
nm SBV (a, b, c, d, e, f)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        String -> SBV f -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
   msMaximize :: String -> SBV (a, b, c, d, e, f) -> m ()
msMaximize String
nm SBV (a, b, c, d, e, f)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        String -> SBV f -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f)
pSBV (a, b, c, d, e, f)
-> (SBV (a, b, c, d, e, f) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)

-- 7-tuple
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 :: String -> SBV (a, b, c, d, e, f, g) -> m ()
msMinimize String
nm SBV (a, b, c, d, e, f, g)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        String -> SBV f -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        String -> SBV g -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV g) -> SBV g
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV g
forall b a. HasField "_7" b a => SBV a -> SBV b
_7)
   msMaximize :: String -> SBV (a, b, c, d, e, f, g) -> m ()
msMaximize String
nm SBV (a, b, c, d, e, f, g)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        String -> SBV f -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        String -> SBV g -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g)
pSBV (a, b, c, d, e, f, g)
-> (SBV (a, b, c, d, e, f, g) -> SBV g) -> SBV g
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g) -> SBV g
forall b a. HasField "_7" b a => SBV a -> SBV b
_7)

-- 8-tuple
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 :: String -> SBV (a, b, c, d, e, f, g, h) -> m ()
msMinimize String
nm SBV (a, b, c, d, e, f, g, h)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        String -> SBV f -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        String -> SBV g -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV g) -> SBV g
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV g
forall b a. HasField "_7" b a => SBV a -> SBV b
_7)
                        String -> SBV h -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMinimize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._8") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV h) -> SBV h
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV h
forall b a. HasField "_8" b a => SBV a -> SBV b
_8)
   msMaximize :: String -> SBV (a, b, c, d, e, f, g, h) -> m ()
msMaximize String
nm SBV (a, b, c, d, e, f, g, h)
p = do String -> SBV a -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._1") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV a) -> SBV a
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV a
forall b a. HasField "_1" b a => SBV a -> SBV b
_1)
                        String -> SBV b -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._2") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV b) -> SBV b
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV b
forall b a. HasField "_2" b a => SBV a -> SBV b
_2)
                        String -> SBV c -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._3") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV c) -> SBV c
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV c
forall b a. HasField "_3" b a => SBV a -> SBV b
_3)
                        String -> SBV d -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._4") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV d) -> SBV d
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV d
forall b a. HasField "_4" b a => SBV a -> SBV b
_4)
                        String -> SBV e -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._5") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV e) -> SBV e
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV e
forall b a. HasField "_5" b a => SBV a -> SBV b
_5)
                        String -> SBV f -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._6") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV f) -> SBV f
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV f
forall b a. HasField "_6" b a => SBV a -> SBV b
_6)
                        String -> SBV g -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._7") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV g) -> SBV g
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV g
forall b a. HasField "_7" b a => SBV a -> SBV b
_7)
                        String -> SBV h -> m ()
forall a (m :: * -> *).
(Metric a, MonadSymbolic m, SolverContext m) =>
String -> SBV a -> m ()
msMaximize (String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"^._8") (SBV (a, b, c, d, e, f, g, h)
pSBV (a, b, c, d, e, f, g, h)
-> (SBV (a, b, c, d, e, f, g, h) -> SBV h) -> SBV h
forall a b. a -> (a -> b) -> b
^.SBV (a, b, c, d, e, f, g, h) -> SBV h
forall b a. HasField "_8" b a => SBV a -> SBV b
_8)

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}