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

Copyright(c) Galois Inc 2019-2020
LicenseBSD3
Maintainerrdockins@galois.com
Safe HaskellNone
LanguageHaskell2010

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
(TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e :: StringInfo -> Type) Source # 
Instance details

Defined in What4.Expr.StringSeq

Methods

testEquality :: 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 :: Int -> StringSeq e tp -> Int #

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

append :: (HasAbsValue e, HashableF e) => StringSeq e si -> StringSeq e si -> StringSeq 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 #