Data.SBV.Tuple

Author : Joel Burget, Levent Erkok License : BSD3 Maintainer: [e-mail] Stability : experimental

Accessing symbolic tuple fields and deconstruction.

Symbolic field access

(^.) :: a -> (a -> b) -> b infixl 8

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.

_1 :: HasField "_1" b a => SBV a -> SBV b

Access the 1st element of an STupleN, 2 <= N <= 8. Also see ^..

_2 :: HasField "_2" b a => SBV a -> SBV b

Access the 2nd element of an STupleN, 2 <= N <= 8. Also see ^..

_3 :: HasField "_3" b a => SBV a -> SBV b

Access the 3nd element of an STupleN, 3 <= N <= 8. Also see ^..

_4 :: HasField "_4" b a => SBV a -> SBV b

Access the 4th element of an STupleN, 4 <= N <= 8. Also see ^..

_5 :: HasField "_5" b a => SBV a -> SBV b

Access the 5th element of an STupleN, 5 <= N <= 8. Also see ^..

_6 :: HasField "_6" b a => SBV a -> SBV b

Access the 6th element of an STupleN, 6 <= N <= 8. Also see ^..

_7 :: HasField "_7" b a => SBV a -> SBV b

Access the 7th element of an STupleN, 7 <= N <= 8. Also see ^..

_8 :: HasField "_8" b a => SBV a -> SBV b

Access the 8th element of an STupleN, 8 <= N <= 8. Also see ^..

Tupling and untupling

tuple :: Tuple tup a => a -> SBV tup

Constructing a tuple from its parts. Forms an isomorphism pair with tuple:

>>> prove $ \p -> untuple @(Integer, Bool, (String, Char)) (tuple p) .== p
Q.E.D.

untuple :: Tuple tup a => SBV tup -> a

Deconstruct a tuple, getting its constituent parts apart. Forms an isomorphism pair with untuple:

>>> prove $ \p -> tuple @(Integer, Bool, (String, Char)) (untuple p) .== p
Q.E.D.