Copyright	(c) Joel Burget Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Data.SBV.Tuple

Contents

Symbolic field access
Tupling and untupling
Orphan instances

Description

Accessing symbolic tuple fields and deconstruction.

Synopsis

(^.) :: a -> (a -> b) -> b
_1 :: HasField "_1" b a => SBV a -> SBV b
_2 :: HasField "_2" b a => SBV a -> SBV b
_3 :: HasField "_3" b a => SBV a -> SBV b
_4 :: HasField "_4" b a => SBV a -> SBV b
_5 :: HasField "_5" b a => SBV a -> SBV b
_6 :: HasField "_6" b a => SBV a -> SBV b
_7 :: HasField "_7" b a => SBV a -> SBV b
_8 :: HasField "_8" b a => SBV a -> SBV b
tuple :: Tuple tup a => a -> SBV tup
untuple :: Tuple tup a => SBV tup -> a

Symbolic field access

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

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 Source #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tupling and untupling

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

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 Source #

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) Source #
Instance details Associated Types type MetricSpace (a, b) Source # Methods toMetricSpace :: SBV (a, b) -> SBV (MetricSpace (a, b)) Source # fromMetricSpace :: SBV (MetricSpace (a, b)) -> SBV (a, b) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b) -> m () Source #
(SymVal a, Metric a, SymVal b, Metric b, SymVal c, Metric c) => Metric (a, b, c) Source #
Instance details Associated Types type MetricSpace (a, b, c) Source # Methods toMetricSpace :: SBV (a, b, c) -> SBV (MetricSpace (a, b, c)) Source # fromMetricSpace :: SBV (MetricSpace (a, b, c)) -> SBV (a, b, c) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c) -> m () Source #
(SymVal a, Metric a, SymVal b, Metric b, SymVal c, Metric c, SymVal d, Metric d) => Metric (a, b, c, d) Source #
Instance details Associated Types type MetricSpace (a, b, c, d) Source # Methods toMetricSpace :: SBV (a, b, c, d) -> SBV (MetricSpace (a, b, c, d)) Source # fromMetricSpace :: SBV (MetricSpace (a, b, c, d)) -> SBV (a, b, c, d) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d) -> m () Source #
(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) Source #
Instance details Associated Types type MetricSpace (a, b, c, d, e) Source # Methods toMetricSpace :: SBV (a, b, c, d, e) -> SBV (MetricSpace (a, b, c, d, e)) Source # fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e)) -> SBV (a, b, c, d, e) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e) -> m () Source #
(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) Source #
Instance details Associated Types type MetricSpace (a, b, c, d, e, f) Source # Methods toMetricSpace :: SBV (a, b, c, d, e, f) -> SBV (MetricSpace (a, b, c, d, e, f)) Source # fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e, f)) -> SBV (a, b, c, d, e, f) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f) -> m () Source #
(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) Source #
Instance details Associated Types type MetricSpace (a, b, c, d, e, f, g) Source # Methods toMetricSpace :: SBV (a, b, c, d, e, f, g) -> SBV (MetricSpace (a, b, c, d, e, f, g)) Source # fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e, f, g)) -> SBV (a, b, c, d, e, f, g) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g) -> m () Source #
(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) Source #
Instance details Associated Types type MetricSpace (a, b, c, d, e, f, g, h) Source # Methods toMetricSpace :: SBV (a, b, c, d, e, f, g, h) -> SBV (MetricSpace (a, b, c, d, e, f, g, h)) Source # fromMetricSpace :: SBV (MetricSpace (a, b, c, d, e, f, g, h)) -> SBV (a, b, c, d, e, f, g, h) Source # msMinimize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g, h) -> m () Source # msMaximize :: (MonadSymbolic m, SolverContext m) => String -> SBV (a, b, c, d, e, f, g, h) -> m () Source #