what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Utils.StringLiteral

Description

Synopsis

- data StringLiteral (si :: StringInfo) :: Type where
  - UnicodeLiteral :: !Text -> StringLiteral Unicode
  - Char8Literal :: !ByteString -> StringLiteral Char8
  - Char16Literal :: !Word16String -> StringLiteral Char16
- stringLiteralInfo :: StringLiteral si -> StringInfoRepr si
- fromUnicodeLit :: StringLiteral Unicode -> Text
- fromChar8Lit :: StringLiteral Char8 -> ByteString
- fromChar16Lit :: StringLiteral Char16 -> Word16String
- stringLitEmpty :: StringInfoRepr si -> StringLiteral si
- stringLitLength :: StringLiteral si -> Integer
- stringLitNull :: StringLiteral si -> Bool
- stringLitBounds :: StringLiteral si -> Maybe (Int, Int)
- stringLitContains :: StringLiteral si -> StringLiteral si -> Bool
- stringLitIsPrefixOf :: StringLiteral si -> StringLiteral si -> Bool
- stringLitIsSuffixOf :: StringLiteral si -> StringLiteral si -> Bool
- stringLitSubstring :: StringLiteral si -> Integer -> Integer -> StringLiteral si
- stringLitIndexOf :: StringLiteral si -> StringLiteral si -> Integer -> Integer

# Documentation

data StringLiteral (si :: StringInfo) :: Type where Source #

Constructors

UnicodeLiteral :: !Text -> StringLiteral Unicode |
Char8Literal :: !ByteString -> StringLiteral Char8 |
Char16Literal :: !Word16String -> StringLiteral Char16 |

#### Instances

Instances details

TestEquality StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods testEquality :: forall (a :: k) (b :: k). StringLiteral a -> StringLiteral b -> Maybe (a :~: b) Source #
HashableF StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods hashWithSaltF :: forall (tp :: k). Int -> StringLiteral tp -> Int Source # hashF :: forall (tp :: k). StringLiteral tp -> Int Source #
OrdF StringLiteral Source # |

Instance details

Defined in What4.Utils.StringLiteral

Methods

compareF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> OrderingF x y Source #

leqF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool Source #

ltF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool Source #

geqF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool Source #

gtF :: forall (x :: k) (y :: k). StringLiteral x -> StringLiteral y -> Bool Source #

ShowF StringLiteral Source # |
Instance details Defined in What4.Utils.StringLiteral Methods withShow :: forall p q (tp :: k) a. p StringLiteral -> q tp -> (Show (StringLiteral tp) => a) -> a Source # showF :: forall (tp :: k). StringLiteral tp -> String Source # showsPrecF :: forall (tp :: k). Int -> StringLiteral tp -> String -> String Source #
IsString (StringLiteral Unicode) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods fromString :: String -> StringLiteral Unicode Source #
Semigroup (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods (<>) :: StringLiteral si -> StringLiteral si -> StringLiteral si Source # sconcat :: NonEmpty (StringLiteral si) -> StringLiteral si Source # stimes :: Integral b => b -> StringLiteral si -> StringLiteral si Source #
Show (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods showsPrec :: Int -> StringLiteral si -> ShowS Source # show :: StringLiteral si -> String Source # showList :: [StringLiteral si] -> ShowS Source #
Eq (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods (==) :: StringLiteral si -> StringLiteral si -> Bool Source # (/=) :: StringLiteral si -> StringLiteral si -> Bool Source #
Ord (StringLiteral si) Source # |

Instance details

Defined in What4.Utils.StringLiteral

Methods

compare :: StringLiteral si -> StringLiteral si -> Ordering Source #

(<) :: StringLiteral si -> StringLiteral si -> Bool Source #

(<=) :: StringLiteral si -> StringLiteral si -> Bool Source #

(>) :: StringLiteral si -> StringLiteral si -> Bool Source #

(>=) :: StringLiteral si -> StringLiteral si -> Bool Source #

max :: StringLiteral si -> StringLiteral si -> StringLiteral si Source #

min :: StringLiteral si -> StringLiteral si -> StringLiteral si Source #

Hashable (StringLiteral si) Source # |
Instance details Defined in What4.Utils.StringLiteral Methods hashWithSalt :: Int -> StringLiteral si -> Int Source # hash :: StringLiteral si -> Int Source #

stringLiteralInfo :: StringLiteral si -> StringInfoRepr si Source #

fromUnicodeLit :: StringLiteral Unicode -> Text Source #

fromChar8Lit :: StringLiteral Char8 -> ByteString Source #

fromChar16Lit :: StringLiteral Char16 -> Word16String Source #

stringLitEmpty :: StringInfoRepr si -> StringLiteral si Source #

stringLitLength :: StringLiteral si -> Integer Source #

stringLitNull :: StringLiteral si -> Bool Source #

stringLitBounds :: StringLiteral si -> Maybe (Int, Int) Source #

stringLitContains :: StringLiteral si -> StringLiteral si -> Bool Source #

stringLitIsPrefixOf :: StringLiteral si -> StringLiteral si -> Bool Source #

stringLitIsSuffixOf :: StringLiteral si -> StringLiteral si -> Bool Source #

stringLitSubstring :: StringLiteral si -> Integer -> Integer -> StringLiteral si Source #

stringLitIndexOf :: StringLiteral si -> StringLiteral si -> Integer -> Integer Source #

Index of first occurrence of second string in first one starting at the position specified by the third argument. `stringLitIndexOf s t k`, with `0 <= k <= |s|` is the position of the first occurrence of `t` in `s` at or after position `k`, if any. Otherwise, it is `-1`. Note that the result is `k` whenever `k` is within the range `[0, |s|]` and `t` is empty.