sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

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 #