-- Support for Strings for SMT 

{-# LANGUAGE OverloadedStrings   #-}

module Language.Haskell.Liquid.String where

import qualified Data.ByteString as BS
import qualified Data.String     as ST

{-@ embed SMTString as Str @-}

data SMTString = S BS.ByteString 
  deriving (SMTString -> SMTString -> Bool
(SMTString -> SMTString -> Bool)
-> (SMTString -> SMTString -> Bool) -> Eq SMTString
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTString -> SMTString -> Bool
$c/= :: SMTString -> SMTString -> Bool
== :: SMTString -> SMTString -> Bool
$c== :: SMTString -> SMTString -> Bool
Eq, Int -> SMTString -> ShowS
[SMTString] -> ShowS
SMTString -> String
(Int -> SMTString -> ShowS)
-> (SMTString -> String)
-> ([SMTString] -> ShowS)
-> Show SMTString
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTString] -> ShowS
$cshowList :: [SMTString] -> ShowS
show :: SMTString -> String
$cshow :: SMTString -> String
showsPrec :: Int -> SMTString -> ShowS
$cshowsPrec :: Int -> SMTString -> ShowS
Show)

{-@ invariant {s:SMTString | 0 <= stringLen s } @-}

{-@ measure stringEmp    :: SMTString @-}
{-@ measure stringLen    :: SMTString -> Int @-}
{-@ measure subString    :: SMTString -> Int -> Int -> SMTString @-}
{-@ measure concatString :: SMTString -> SMTString -> SMTString @-}
{-@ measure fromString   :: String -> SMTString @-}
{-@ measure takeString   :: Int -> SMTString -> SMTString @-}
{-@ measure dropString   :: Int -> SMTString -> SMTString @-}

----------------------------------

{-@ assume concatString :: x:SMTString -> y:SMTString 
                 -> {v:SMTString | v == concatString x y && stringLen v == stringLen x + stringLen y } @-}
concatString :: SMTString -> SMTString -> SMTString
concatString :: SMTString -> SMTString -> SMTString
concatString (S ByteString
s1) (S ByteString
s2) = ByteString -> SMTString
S (ByteString
s1 ByteString -> ByteString -> ByteString
`BS.append` ByteString
s2)

{-@ assume stringEmp :: {v:SMTString | v == stringEmp  && stringLen v == 0 } @-}
stringEmp :: SMTString
stringEmp :: SMTString
stringEmp = ByteString -> SMTString
S (ByteString
BS.empty)

stringLen :: SMTString -> Int  
{-@ assume stringLen :: x:SMTString -> {v:Nat | v == stringLen x} @-}
stringLen :: SMTString -> Int
stringLen (S ByteString
s) = ByteString -> Int
BS.length ByteString
s 


{-@ assume subString  :: s:SMTString -> offset:Int -> ln:Int -> {v:SMTString | v == subString s offset ln } @-}
subString :: SMTString -> Int -> Int -> SMTString 
subString :: SMTString -> Int -> Int -> SMTString
subString (S ByteString
s) Int
o Int
l = ByteString -> SMTString
S (Int -> ByteString -> ByteString
BS.take Int
l (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Int -> ByteString -> ByteString
BS.drop Int
o ByteString
s) 


{-@ assume takeString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == i && v == takeString i xs } @-} 
takeString :: Int -> SMTString -> SMTString
takeString :: Int -> SMTString -> SMTString
takeString Int
i (S ByteString
s) = ByteString -> SMTString
S (Int -> ByteString -> ByteString
BS.take Int
i ByteString
s)

{-@ assume dropString :: i:Nat -> xs:{SMTString | i <= stringLen xs } -> {v:SMTString | stringLen v == stringLen xs - i && v == dropString i xs } @-} 
dropString :: Int -> SMTString -> SMTString
dropString :: Int -> SMTString -> SMTString
dropString Int
i (S ByteString
s) = ByteString -> SMTString
S (Int -> ByteString -> ByteString
BS.drop Int
i ByteString
s)


{-@ assume fromString :: i:String -> {o:SMTString | i == o && o == fromString i} @-}
fromString :: String -> SMTString
fromString :: String -> SMTString
fromString = ByteString -> SMTString
S (ByteString -> SMTString)
-> (String -> ByteString) -> String -> SMTString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
forall a. IsString a => String -> a
ST.fromString 


{-@ assume isNullString :: i:SMTString -> {b:Bool | b <=> stringLen i == 0 } @-} 
isNullString :: SMTString -> Bool 
isNullString :: SMTString -> Bool
isNullString (S ByteString
s) = ByteString -> Int
BS.length ByteString
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0