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

Copyright (c) Joel BurgetLevent Erkok BSD3 erkokl@gmail.com experimental None Haskell2010

Data.SBV.Tuple

Description

Accessing symbolic tuple fields and deconstruction.

Synopsis

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

>>> 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 untuple: >>> 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 Typestype MetricSpace (a, b) :: Type Source # MethodstoMetricSpace :: 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 Typestype MetricSpace (a, b, c) :: Type Source # MethodstoMetricSpace :: 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 Typestype MetricSpace (a, b, c, d) :: Type Source # MethodstoMetricSpace :: 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 Typestype MetricSpace (a, b, c, d, e) :: Type Source # MethodstoMetricSpace :: 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 Typestype MetricSpace (a, b, c, d, e, f) :: Type Source # MethodstoMetricSpace :: 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 Typestype MetricSpace (a, b, c, d, e, f, g) :: Type Source # MethodstoMetricSpace :: 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 Typestype MetricSpace (a, b, c, d, e, f, g, h) :: Type Source # MethodstoMetricSpace :: 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 #