Data.SBV.Tuple

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 3rd 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 untuple:

>>> 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 tuple:

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

Orphan instances

(SymVal a, Metric a, SymVal b, Metric b) => Metric (a, b)

Associated Types

type MetricSpace (a, b)

Methods

toMetricSpace :: SBV (a, b) -> SBV (MetricSpace (a, b))

fromMetricSpace :: SBV (MetricSpace (a, b)) -> SBV (a, b)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b) -> m ()

(SymVal a, Metric a, SymVal b, Metric b, SymVal c, Metric c) => Metric (a, b, c)

Associated Types

type MetricSpace (a, b, c)

Methods

toMetricSpace :: SBV (a, b, c) -> SBV (MetricSpace (a, b, c))

fromMetricSpace :: SBV (MetricSpace (a, b, c)) -> SBV (a, b, c)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c) -> m ()

(SymVal a, Metric a, SymVal b, Metric b, SymVal c, Metric c, SymVal d, Metric d) => Metric (a, b, c, d)

Associated Types

type MetricSpace (a, b, c, d)

Methods

toMetricSpace :: SBV (a, b, c, d) -> SBV (MetricSpace (a, b, c, d))

fromMetricSpace :: SBV (MetricSpace (a, b, c, d)) -> SBV (a, b, c, d)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d) -> m ()

(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)

Associated Types

type MetricSpace (a, b, c, d, e)

Methods

toMetricSpace :: SBV (a, b, c, d, e) -> SBV (MetricSpace (a, b, c, d, e))

fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e)) -> SBV (a, b, c, d, e)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e) -> m ()

(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)

Associated Types

type MetricSpace (a, b, c, d, e, f)

Methods

toMetricSpace :: SBV (a, b, c, d, e, f) -> SBV (MetricSpace (a, b, c, d, e, f))

fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e, f)) -> SBV (a, b, c, d, e, f)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f) -> m ()

(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)

Associated Types

type MetricSpace (a, b, c, d, e, f, g)

Methods

toMetricSpace :: SBV (a, b, c, d, e, f, g) -> SBV (MetricSpace (a, b, c, d, e, f, g))

fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e, f, g)) -> SBV (a, b, c, d, e, f, g)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g) -> m ()

(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)

Associated Types

type MetricSpace (a, b, c, d, e, f, g, h)

Methods

toMetricSpace :: SBV (a, b, c, d, e, f, g, h) -> SBV (MetricSpace (a, b, c, d, e, f, g, h))

fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e, f, g, h)) -> SBV (a, b, c, d, e, f, g, h)

msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g, h) -> m ()

msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g, h) -> m ()