{-|
Module      : What4.Expr.StringSeq
Description : Datastructure for sequences of appended strings
Copyright   : (c) Galois Inc, 2019-2020
License     : BSD3
Maintainer  : rdockins@galois.com

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.
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}

module What4.Expr.StringSeq
( StringSeq
, StringSeqEntry(..)
, singleton
, append
, stringSeqAbs
, toList
, traverseStringSeq
) where

import           Data.Kind
import qualified Data.Foldable as F

import qualified Data.FingerTree as FT

import           Data.Parameterized.Classes

import           What4.BaseTypes
import           What4.Interface
import           What4.Utils.AbstractDomains
import           What4.Utils.IncrHash

-- | Annotation value for string sequences.
--   First value is the XOR hash of the sequence
--   Second value is the string abstract domain.
data StringSeqNote = StringSeqNote !IncrHash !StringAbstractValue

instance Semigroup StringSeqNote where
  StringSeqNote IncrHash
xh StringAbstractValue
xabs <> :: StringSeqNote -> StringSeqNote -> StringSeqNote
<> StringSeqNote IncrHash
yh StringAbstractValue
yabs =
    IncrHash -> StringAbstractValue -> StringSeqNote
StringSeqNote (IncrHash
xh IncrHash -> IncrHash -> IncrHash
forall a. Semigroup a => a -> a -> a
<> IncrHash
yh) (StringAbstractValue -> StringAbstractValue -> StringAbstractValue
stringAbsConcat StringAbstractValue
xabs StringAbstractValue
yabs)

instance Monoid StringSeqNote where
  mempty :: StringSeqNote
mempty = IncrHash -> StringAbstractValue -> StringSeqNote
StringSeqNote IncrHash
forall a. Monoid a => a
mempty StringAbstractValue
stringAbsEmpty
  mappend :: StringSeqNote -> StringSeqNote -> StringSeqNote
mappend = StringSeqNote -> StringSeqNote -> StringSeqNote
forall a. Semigroup a => a -> a -> a
(<>)

data StringSeqEntry e si
  = StringSeqLiteral !(StringLiteral si)
  | StringSeqTerm !(e (BaseStringType si))

instance (HasAbsValue e, HashableF e) => FT.Measured StringSeqNote (StringSeqEntry e si) where
  measure :: StringSeqEntry e si -> StringSeqNote
measure (StringSeqLiteral StringLiteral si
l) = IncrHash -> StringAbstractValue -> StringSeqNote
StringSeqNote (Int -> StringLiteral si -> IncrHash
forall a. Hashable a => Int -> a -> IncrHash
toIncrHashWithSalt Int
1 StringLiteral si
l) (StringLiteral si -> StringAbstractValue
forall (si :: StringInfo). StringLiteral si -> StringAbstractValue
stringAbsSingle StringLiteral si
l)
  measure (StringSeqTerm e (BaseStringType si)
e) = IncrHash -> StringAbstractValue -> StringSeqNote
StringSeqNote (Int -> IncrHash
mkIncrHash (Int -> e (BaseStringType si) -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF Int
2 e (BaseStringType si)
e)) (e (BaseStringType si) -> AbstractValue (BaseStringType si)
forall (f :: BaseType -> Type) (tp :: BaseType).
HasAbsValue f =>
f tp -> AbstractValue tp
getAbsValue e (BaseStringType si)
e)

type StringFT e si = FT.FingerTree StringSeqNote (StringSeqEntry e si)

sft_hash :: (HashableF e, HasAbsValue e) => StringFT e si -> IncrHash
sft_hash :: StringFT e si -> IncrHash
sft_hash StringFT e si
ft =
  case StringFT e si -> StringSeqNote
forall v a. Measured v a => a -> v
FT.measure StringFT e si
ft of
    StringSeqNote IncrHash
h StringAbstractValue
_abs -> IncrHash
h

ft_eqBy :: FT.Measured v a => (a -> a -> Bool) -> FT.FingerTree v a -> FT.FingerTree v a -> Bool
ft_eqBy :: (a -> a -> Bool) -> FingerTree v a -> FingerTree v a -> Bool
ft_eqBy a -> a -> Bool
eq FingerTree v a
xs0 FingerTree v a
ys0 = ViewL (FingerTree v) a -> ViewL (FingerTree v) a -> Bool
go (FingerTree v a -> ViewL (FingerTree v) a
forall v a.
Measured v a =>
FingerTree v a -> ViewL (FingerTree v) a
FT.viewl FingerTree v a
xs0) (FingerTree v a -> ViewL (FingerTree v) a
forall v a.
Measured v a =>
FingerTree v a -> ViewL (FingerTree v) a
FT.viewl FingerTree v a
ys0)
 where
 go :: ViewL (FingerTree v) a -> ViewL (FingerTree v) a -> Bool
go ViewL (FingerTree v) a
FT.EmptyL ViewL (FingerTree v) a
FT.EmptyL = Bool
True
 go (a
x FT.:< FingerTree v a
xs) (a
y FT.:< FingerTree v a
ys) = a -> a -> Bool
eq a
x a
y Bool -> Bool -> Bool
&& ViewL (FingerTree v) a -> ViewL (FingerTree v) a -> Bool
go (FingerTree v a -> ViewL (FingerTree v) a
forall v a.
Measured v a =>
FingerTree v a -> ViewL (FingerTree v) a
FT.viewl FingerTree v a
xs) (FingerTree v a -> ViewL (FingerTree v) a
forall v a.
Measured v a =>
FingerTree v a -> ViewL (FingerTree v) a
FT.viewl FingerTree v a
ys)
 go ViewL (FingerTree v) a
_ ViewL (FingerTree v) a
_ = Bool
False

data StringSeq
  (e  :: BaseType -> Type)
  (si :: StringInfo) =
  StringSeq
  { StringSeq e si -> StringInfoRepr si
_stringSeqRepr :: StringInfoRepr si
  , StringSeq e si -> FingerTree StringSeqNote (StringSeqEntry e si)
stringSeq :: FT.FingerTree StringSeqNote (StringSeqEntry e si)
  }

instance (TestEquality e, HasAbsValue e, HashableF e) => TestEquality (StringSeq e) where
  testEquality :: StringSeq e a -> StringSeq e b -> Maybe (a :~: b)
testEquality (StringSeq StringInfoRepr a
xi FingerTree StringSeqNote (StringSeqEntry e a)
xs) (StringSeq StringInfoRepr b
yi FingerTree StringSeqNote (StringSeqEntry e b)
ys)
    | Just a :~: b
Refl <- StringInfoRepr a -> StringInfoRepr b -> Maybe (a :~: b)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StringInfoRepr a
xi StringInfoRepr b
yi
    , FingerTree StringSeqNote (StringSeqEntry e a) -> IncrHash
forall (e :: BaseType -> Type) (si :: StringInfo).
(HashableF e, HasAbsValue e) =>
StringFT e si -> IncrHash
sft_hash FingerTree StringSeqNote (StringSeqEntry e a)
xs IncrHash -> IncrHash -> Bool
forall a. Eq a => a -> a -> Bool
== FingerTree StringSeqNote (StringSeqEntry e b) -> IncrHash
forall (e :: BaseType -> Type) (si :: StringInfo).
(HashableF e, HasAbsValue e) =>
StringFT e si -> IncrHash
sft_hash FingerTree StringSeqNote (StringSeqEntry e b)
ys

    = let f :: StringSeqEntry f si -> StringSeqEntry f si -> Bool
f (StringSeqLiteral StringLiteral si
a) (StringSeqLiteral StringLiteral si
b) = StringLiteral si
a StringLiteral si -> StringLiteral si -> Bool
forall a. Eq a => a -> a -> Bool
== StringLiteral si
b
          f (StringSeqTerm f (BaseStringType si)
a) (StringSeqTerm f (BaseStringType si)
b) = Maybe (BaseStringType si :~: BaseStringType si) -> Bool
forall a. Maybe a -> Bool
isJust (f (BaseStringType si)
-> f (BaseStringType si)
-> Maybe (BaseStringType si :~: BaseStringType si)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f (BaseStringType si)
a f (BaseStringType si)
b)
          f StringSeqEntry f si
_ StringSeqEntry f si
_ = Bool
False

       in if (StringSeqEntry e a -> StringSeqEntry e a -> Bool)
-> FingerTree StringSeqNote (StringSeqEntry e a)
-> FingerTree StringSeqNote (StringSeqEntry e a)
-> Bool
forall v a.
Measured v a =>
(a -> a -> Bool) -> FingerTree v a -> FingerTree v a -> Bool
ft_eqBy StringSeqEntry e a -> StringSeqEntry e a -> Bool
forall (f :: BaseType -> Type) (si :: StringInfo).
TestEquality f =>
StringSeqEntry f si -> StringSeqEntry f si -> Bool
f FingerTree StringSeqNote (StringSeqEntry e a)
xs FingerTree StringSeqNote (StringSeqEntry e a)
FingerTree StringSeqNote (StringSeqEntry e b)
ys then (a :~: a) -> Maybe (a :~: a)
forall a. a -> Maybe a
Just a :~: a
forall k (a :: k). a :~: a
Refl else Maybe (a :~: b)
forall a. Maybe a
Nothing

  testEquality StringSeq e a
_ StringSeq e b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing

instance (TestEquality e, HasAbsValue e, HashableF e) => Eq (StringSeq e si) where
  StringSeq e si
x == :: StringSeq e si -> StringSeq e si -> Bool
== StringSeq e si
y = Maybe (si :~: si) -> Bool
forall a. Maybe a -> Bool
isJust (StringSeq e si -> StringSeq e si -> Maybe (si :~: si)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality StringSeq e si
x StringSeq e si
y)

instance (HasAbsValue e, HashableF e) => HashableF (StringSeq e) where
  hashWithSaltF :: Int -> StringSeq e tp -> Int
hashWithSaltF Int
s (StringSeq StringInfoRepr tp
_si FingerTree StringSeqNote (StringSeqEntry e tp)
xs) = Int -> IncrHash -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s (FingerTree StringSeqNote (StringSeqEntry e tp) -> IncrHash
forall (e :: BaseType -> Type) (si :: StringInfo).
(HashableF e, HasAbsValue e) =>
StringFT e si -> IncrHash
sft_hash FingerTree StringSeqNote (StringSeqEntry e tp)
xs)

instance (HasAbsValue e, HashableF e) => Hashable (StringSeq e si) where
  hashWithSalt :: Int -> StringSeq e si -> Int
hashWithSalt = Int -> StringSeq e si -> Int
forall k (f :: k -> Type) (tp :: k).
HashableF f =>
Int -> f tp -> Int
hashWithSaltF

singleton :: (HasAbsValue e, HashableF e, IsExpr e) => StringInfoRepr si -> e (BaseStringType si) -> StringSeq e si
singleton :: StringInfoRepr si -> e (BaseStringType si) -> StringSeq e si
singleton StringInfoRepr si
si e (BaseStringType si)
x
  | Just StringLiteral si
l <- e (BaseStringType si) -> Maybe (StringLiteral si)
forall (e :: BaseType -> Type) (si :: StringInfo).
IsExpr e =>
e (BaseStringType si) -> Maybe (StringLiteral si)
asString e (BaseStringType si)
x = StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
StringSeq StringInfoRepr si
si (StringSeqEntry e si
-> FingerTree StringSeqNote (StringSeqEntry e si)
forall v a. Measured v a => a -> FingerTree v a
FT.singleton (StringLiteral si -> StringSeqEntry e si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringLiteral si -> StringSeqEntry e si
StringSeqLiteral StringLiteral si
l))
  | Bool
otherwise            = StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
StringSeq StringInfoRepr si
si (StringSeqEntry e si
-> FingerTree StringSeqNote (StringSeqEntry e si)
forall v a. Measured v a => a -> FingerTree v a
FT.singleton (e (BaseStringType si) -> StringSeqEntry e si
forall (e :: BaseType -> Type) (si :: StringInfo).
e (BaseStringType si) -> StringSeqEntry e si
StringSeqTerm e (BaseStringType si)
x))

append :: (HasAbsValue e, HashableF e) => StringSeq e si -> StringSeq e si -> StringSeq e si
append :: StringSeq e si -> StringSeq e si -> StringSeq e si
append (StringSeq StringInfoRepr si
si FingerTree StringSeqNote (StringSeqEntry e si)
xs) (StringSeq StringInfoRepr si
_ FingerTree StringSeqNote (StringSeqEntry e si)
ys) =
  case (FingerTree StringSeqNote (StringSeqEntry e si)
-> ViewR (FingerTree StringSeqNote) (StringSeqEntry e si)
forall v a.
Measured v a =>
FingerTree v a -> ViewR (FingerTree v) a
FT.viewr FingerTree StringSeqNote (StringSeqEntry e si)
xs, FingerTree StringSeqNote (StringSeqEntry e si)
-> ViewL (FingerTree StringSeqNote) (StringSeqEntry e si)
forall v a.
Measured v a =>
FingerTree v a -> ViewL (FingerTree v) a
FT.viewl FingerTree StringSeqNote (StringSeqEntry e si)
ys) of
    (FingerTree StringSeqNote (StringSeqEntry e si)
xs' FT.:> StringSeqLiteral StringLiteral si
xlit, StringSeqLiteral StringLiteral si
ylit FT.:< FingerTree StringSeqNote (StringSeqEntry e si)
ys')
      -> StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
StringSeq StringInfoRepr si
si (FingerTree StringSeqNote (StringSeqEntry e si)
xs' FingerTree StringSeqNote (StringSeqEntry e si)
-> FingerTree StringSeqNote (StringSeqEntry e si)
-> FingerTree StringSeqNote (StringSeqEntry e si)
forall a. Semigroup a => a -> a -> a
<> (StringLiteral si -> StringSeqEntry e si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringLiteral si -> StringSeqEntry e si
StringSeqLiteral (StringLiteral si
xlit StringLiteral si -> StringLiteral si -> StringLiteral si
forall a. Semigroup a => a -> a -> a
<> StringLiteral si
ylit) StringSeqEntry e si
-> FingerTree StringSeqNote (StringSeqEntry e si)
-> FingerTree StringSeqNote (StringSeqEntry e si)
forall v a. Measured v a => a -> FingerTree v a -> FingerTree v a
FT.<| FingerTree StringSeqNote (StringSeqEntry e si)
ys'))

    (ViewR (FingerTree StringSeqNote) (StringSeqEntry e si),
 ViewL (FingerTree StringSeqNote) (StringSeqEntry e si))
_ -> StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
StringSeq StringInfoRepr si
si (FingerTree StringSeqNote (StringSeqEntry e si)
xs FingerTree StringSeqNote (StringSeqEntry e si)
-> FingerTree StringSeqNote (StringSeqEntry e si)
-> FingerTree StringSeqNote (StringSeqEntry e si)
forall a. Semigroup a => a -> a -> a
<> FingerTree StringSeqNote (StringSeqEntry e si)
ys)

stringSeqAbs :: (HasAbsValue e, HashableF e) => StringSeq e si -> StringAbstractValue
stringSeqAbs :: StringSeq e si -> StringAbstractValue
stringSeqAbs (StringSeq StringInfoRepr si
_ FingerTree StringSeqNote (StringSeqEntry e si)
xs) =
  case FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeqNote
forall v a. Measured v a => a -> v
FT.measure FingerTree StringSeqNote (StringSeqEntry e si)
xs of
    StringSeqNote IncrHash
_ StringAbstractValue
a -> StringAbstractValue
a

toList :: StringSeq e si -> [StringSeqEntry e si]
toList :: StringSeq e si -> [StringSeqEntry e si]
toList = FingerTree StringSeqNote (StringSeqEntry e si)
-> [StringSeqEntry e si]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
F.toList (FingerTree StringSeqNote (StringSeqEntry e si)
 -> [StringSeqEntry e si])
-> (StringSeq e si
    -> FingerTree StringSeqNote (StringSeqEntry e si))
-> StringSeq e si
-> [StringSeqEntry e si]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StringSeq e si -> FingerTree StringSeqNote (StringSeqEntry e si)
forall (e :: BaseType -> Type) (si :: StringInfo).
StringSeq e si -> FingerTree StringSeqNote (StringSeqEntry e si)
stringSeq

traverseStringSeq :: (HasAbsValue f, HashableF f, Applicative m) =>
  (forall x. e x -> m (f x)) ->
  StringSeq e si -> m (StringSeq f si)
traverseStringSeq :: (forall (x :: BaseType). e x -> m (f x))
-> StringSeq e si -> m (StringSeq f si)
traverseStringSeq forall (x :: BaseType). e x -> m (f x)
f (StringSeq StringInfoRepr si
si FingerTree StringSeqNote (StringSeqEntry e si)
xs) =
  StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry f si) -> StringSeq f si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringInfoRepr si
-> FingerTree StringSeqNote (StringSeqEntry e si) -> StringSeq e si
StringSeq StringInfoRepr si
si (FingerTree StringSeqNote (StringSeqEntry f si) -> StringSeq f si)
-> m (FingerTree StringSeqNote (StringSeqEntry f si))
-> m (StringSeq f si)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (m (FingerTree StringSeqNote (StringSeqEntry f si))
 -> StringSeqEntry e si
 -> m (FingerTree StringSeqNote (StringSeqEntry f si)))
-> m (FingerTree StringSeqNote (StringSeqEntry f si))
-> FingerTree StringSeqNote (StringSeqEntry e si)
-> m (FingerTree StringSeqNote (StringSeqEntry f si))
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' (\m (FingerTree StringSeqNote (StringSeqEntry f si))
m StringSeqEntry e si
x -> FingerTree StringSeqNote (StringSeqEntry f si)
-> StringSeqEntry f si
-> FingerTree StringSeqNote (StringSeqEntry f si)
forall v a. Measured v a => FingerTree v a -> a -> FingerTree v a
(FT.|>) (FingerTree StringSeqNote (StringSeqEntry f si)
 -> StringSeqEntry f si
 -> FingerTree StringSeqNote (StringSeqEntry f si))
-> m (FingerTree StringSeqNote (StringSeqEntry f si))
-> m (StringSeqEntry f si
      -> FingerTree StringSeqNote (StringSeqEntry f si))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> m (FingerTree StringSeqNote (StringSeqEntry f si))
m m (StringSeqEntry f si
   -> FingerTree StringSeqNote (StringSeqEntry f si))
-> m (StringSeqEntry f si)
-> m (FingerTree StringSeqNote (StringSeqEntry f si))
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> StringSeqEntry e si -> m (StringSeqEntry f si)
g StringSeqEntry e si
x) (FingerTree StringSeqNote (StringSeqEntry f si)
-> m (FingerTree StringSeqNote (StringSeqEntry f si))
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure FingerTree StringSeqNote (StringSeqEntry f si)
forall v a. Measured v a => FingerTree v a
FT.empty) FingerTree StringSeqNote (StringSeqEntry e si)
xs
 where
 g :: StringSeqEntry e si -> m (StringSeqEntry f si)
g (StringSeqLiteral StringLiteral si
l) = StringSeqEntry f si -> m (StringSeqEntry f si)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (StringLiteral si -> StringSeqEntry f si
forall (e :: BaseType -> Type) (si :: StringInfo).
StringLiteral si -> StringSeqEntry e si
StringSeqLiteral StringLiteral si
l)
 g (StringSeqTerm e (BaseStringType si)
x) = f (BaseStringType si) -> StringSeqEntry f si
forall (e :: BaseType -> Type) (si :: StringInfo).
e (BaseStringType si) -> StringSeqEntry e si
StringSeqTerm (f (BaseStringType si) -> StringSeqEntry f si)
-> m (f (BaseStringType si)) -> m (StringSeqEntry f si)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> e (BaseStringType si) -> m (f (BaseStringType si))
forall (x :: BaseType). e x -> m (f x)
f e (BaseStringType si)
x