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

Copyright(c) Joel Burget
Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.Tuple

Contents

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 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) :: Type 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) :: Type 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) :: Type 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) :: Type 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) :: Type 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) :: Type 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) :: Type 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 #