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

Copyright | (c) Galois Inc 2019-2020
License | BSD3
Maintainer | rdockins@galois.com
Safe Haskell | None
Language | Haskell2010

What4.Expr.StringSeq

Description

A simple datatype for collecting sequences of strings that are to be concatenated together.

We intend to maintain several invariants. First, that no sequence is empty; the empty string literal should instead be the unique representative of empty strings. Second, that string sequences do not contain adjacent literals. In other words, adjacent string literals are coalesced.

# Documentation

data StringSeq (e :: BaseType -> Type) (si :: StringInfo) Source #

#### Instances

Instances details

(TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e :: StringInfo -> Type) Source # |
Instance details Defined in What4.Expr.StringSeq Methods testEquality :: forall (a :: StringInfo) (b :: StringInfo). StringSeq e a -> StringSeq e b -> Maybe (a :~: b) Source #
(HasAbsValue e, HashableF e) => HashableF (StringSeq e :: StringInfo -> Type) Source # |
Instance details Defined in What4.Expr.StringSeq Methods hashWithSaltF :: forall (tp :: StringInfo). Int -> StringSeq e tp -> Int Source # hashF :: forall (tp :: StringInfo). StringSeq e tp -> Int Source #
(TestEquality e, HasAbsValue e, HashableF e) => Eq (StringSeq e si) Source # |
Instance details Defined in What4.Expr.StringSeq Methods (==) :: StringSeq e si -> StringSeq e si -> Bool Source # (/=) :: StringSeq e si -> StringSeq e si -> Bool Source #
(HasAbsValue e, HashableF e, TestEquality e) => Hashable (StringSeq e si) Source # |
Instance details Defined in What4.Expr.StringSeq Methods hashWithSalt :: Int -> StringSeq e si -> Int Source # hash :: StringSeq e si -> Int Source #

data StringSeqEntry (e :: BaseType -> Type) (si :: StringInfo) Source #

Constructors

StringSeqLiteral !(StringLiteral si) |
StringSeqTerm !(e (BaseStringType si)) |

singleton :: forall e (si :: StringInfo). (HasAbsValue e, HashableF e, IsExpr e) => StringInfoRepr si -> e (BaseStringType si) -> StringSeq e si Source #

append :: forall (e :: BaseType -> Type) (si :: StringInfo). (HasAbsValue e, HashableF e) => StringSeq e si -> StringSeq e si -> StringSeq e si Source #

stringSeqAbs :: forall (e :: BaseType -> Type) (si :: StringInfo). (HasAbsValue e, HashableF e) => StringSeq e si -> StringAbstractValue Source #

toList :: forall (e :: BaseType -> Type) (si :: StringInfo). StringSeq e si -> [StringSeqEntry e si] Source #

traverseStringSeq :: forall f m e (si :: StringInfo). (HasAbsValue f, HashableF f, Applicative m) => (forall (x :: BaseType). e x -> m (f x)) -> StringSeq e si -> m (StringSeq f si) Source #