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

data StringSeqEntry e si Source #

Constructors

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

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

append :: (HasAbsValue e, HashableF e) => StringSeq e si -> StringSeq e si -> StringSeq e si Source #

stringSeqAbs :: (HasAbsValue e, HashableF e) => StringSeq e si -> StringAbstractValue Source #

toList :: StringSeq e si -> [StringSeqEntry e si] Source #

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