content: ---
  layout: post
  title: "Text Write"
  date: 2014-02-23
  comments: true
  external-url:
  author: Eric Seidel
  published: false
  categories: benchmarks, text
  demo: TextWrite.hs
  ---
  
  Last time, we showed how to reason about Unicode and a variable-width
  encoding of `Char`s when consuming a `Text` value, today we'll look at
  the same issue from the perspective of *building* a `Text`.
  
  <!-- more -->
  
  <div class="hidden">
  
  \begin{code}
  {-# LANGUAGE BangPatterns, CPP, MagicHash, Rank2Types,
      RecordWildCards, UnboxedTuples, ExistentialQuantification #-}
  {-@ LIQUID "--no-termination" @-}
  module TextWrite where
  
  import Control.Monad.ST.Unsafe (unsafeIOToST)
  import Foreign.C.Types (CSize)
  import GHC.Base hiding (unsafeChr)
  import GHC.ST
  import GHC.Word (Word16(..))
  import Data.Bits hiding (shiftL)
  import Data.Word
  
  import Language.Haskell.Liquid.Prelude
  
  --------------------------------------------------------------------------------
  --- From TextInternal
  --------------------------------------------------------------------------------
  
  {-@ shiftL :: i:Nat -> n:Nat -> {v:Nat | ((n = 1) => (v = (i * 2)))} @-}
  shiftL :: Int -> Int -> Int
  shiftL = undefined -- (I# x#) (I# i#) = I# (x# `iShiftL#` i#)
  
  {-@ measure isUnknown :: Size -> Prop
      isUnknown (Exact n) = false
      isUnknown (Max   n) = false
      isUnknown (Unknown) = true
    @-}
  {-@ measure getSize :: Size -> Int
      getSize (Exact n) = n
      getSize (Max   n) = n
    @-}
  
  {-@ invariant {v:Size | (getSize v) >= 0} @-}
  
  data Size = Exact {-# UNPACK #-} !Int -- ^ Exact size.
            | Max   {-# UNPACK #-} !Int -- ^ Upper bound on size.
            | Unknown                   -- ^ Unknown size.
              deriving (Eq, Show)
  
  {-@ upperBound :: k:Nat -> s:Size -> {v:Nat | v = ((isUnknown s) ? k : (getSize s))} @-}
  upperBound :: Int -> Size -> Int
  upperBound _ (Exact n) = n
  upperBound _ (Max   n) = n
  upperBound k _         = k
  
  data Step s a = Done
                | Skip !s
                | Yield !a !s
  
  data Stream a =
      forall s. Stream
      (s -> Step s a)             -- stepper function
      !s                          -- current state
      !Size                       -- size hint
  
  {-@ data Array = Array { aBA  :: ByteArray#
                         , aLen :: Nat 
                         } 
    @-}
  
  data Array = Array {
      aBA  :: ByteArray#
    , aLen :: !Int
    }
  
  {-@ measure alen     :: Array -> Int
      alen (Array a n) = n
    @-}
  
  {-@ aLen :: a:Array -> {v:Nat | v = (alen a)}  @-}
  
  {-@ type ArrayN  N   = {v:Array | (alen v) = N} @-}
  
  {-@ type AValidI A   = {v:Nat | v     <  (alen A)} @-}
  {-@ type AValidO A   = {v:Nat | v     <= (alen A)} @-}
  {-@ type AValidL O A = {v:Nat | (v+O) <= (alen A)} @-}
  
  {-@ data MArray s = MArray { maBA  :: MutableByteArray# s
                             , maLen :: Nat } @-}
  
  data MArray s = MArray {
      maBA  :: MutableByteArray# s
    , maLen :: !Int
    }
  
  {-@ measure malen :: MArray s -> Int
      malen (MArray a n) = n
    @-}
  
  {-@ maLen :: a:MArray s -> {v:Nat | v = (malen a)}  @-}
  
  {-@ type MArrayN s N = {v:MArray s | (malen v) = N} @-}
  
  {-@ type MAValidI MA = {v:Nat | v <  (malen MA)} @-}
  {-@ type MAValidO MA = {v:Nat | v <= (malen MA)} @-}
  
  {-@ new :: forall s. n:Nat -> ST s (MArrayN s n) @-}
  new          :: forall s. Int -> ST s (MArray s)
  new n
    | n < 0 || n .&. highBit /= 0 = error $ "new: size overflow"
    | otherwise = ST $ \s1# ->
         case newByteArray# len# s1# of
           (# s2#, marr# #) -> (# s2#, MArray marr# n #)
    where !(I# len#) = bytesInArray n
          highBit    = maxBound `xor` (maxBound `shiftR` 1)
          bytesInArray n = n `shiftL` 1
  
  {-@ unsafeWrite :: ma:MArray s -> MAValidI ma -> Word16 -> ST s () @-}
  unsafeWrite  :: MArray s -> Int -> Word16 -> ST s ()
  unsafeWrite MArray{..} i@(I# i#) (W16# e#)
    | i < 0 || i >= maLen = liquidError "out of bounds"
    | otherwise = ST $ \s1# ->
        case writeWord16Array# maBA i# e# s1# of
          s2# -> (# s2#, () #)
  
  {-@ copyM :: dest:MArray s 
            -> didx:MAValidO dest
            -> src:MArray s 
            -> sidx:MAValidO src
            -> {v:Nat | (((didx + v) <= (malen dest))
                      && ((sidx + v) <= (malen src)))}
            -> ST s ()
    @-}
  copyM        :: MArray s               -- ^ Destination
               -> Int                    -- ^ Destination offset
               -> MArray s               -- ^ Source
               -> Int                    -- ^ Source offset
               -> Int                    -- ^ Count
               -> ST s ()
  copyM dest didx src sidx count
      | count <= 0 = return ()
      | otherwise =
      liquidAssert (sidx + count <= maLen src) .
      liquidAssert (didx + count <= maLen dest) .
      unsafeIOToST $ memcpyM (maBA dest) (fromIntegral didx)
                             (maBA src) (fromIntegral sidx)
                             (fromIntegral count)
  
  {-@ memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () @-}
  memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO ()
  memcpyM = undefined
  
  {-@ unsafeFreeze :: ma:MArray s -> ST s (ArrayN (malen ma)) @-}
  unsafeFreeze :: MArray s -> ST s Array
  unsafeFreeze MArray{..} = ST $ \s# ->
                            (# s#, Array (unsafeCoerce# maBA) maLen #)
  
  {-@ unsafeIndex :: a:Array -> AValidI a -> Word16 @-}
  unsafeIndex  :: Array -> Int -> Word16
  unsafeIndex Array{..} i@(I# i#)
    | i < 0 || i >= aLen = liquidError "out of bounds"
    | otherwise = case indexWord16Array# aBA i# of
                    r# -> (W16# r#)
  
  data Text = Text Array Int Int
  {-@ data Text [tlen] = Text (arr :: Array)
                              (off :: TValidO arr)
                              (len :: TValidL off arr)
    @-}
  
  {-@ measure tarr :: Text -> Array
      tarr (Text a o l) = a
    @-}
  
  {-@ measure toff :: Text -> Int
      toff (Text a o l) = o
    @-}
  
  {-@ measure tlen :: Text -> Int
      tlen (Text a o l) = l
    @-}
  
  {-@ type TValidI T   = {v:Nat | v     <  (tlen T)} @-}
  {-@ type TValidO A   = {v:Nat | v     <= (alen A)} @-}
  {-@ type TValidL O A = {v:Nat | (v+O) <= (alen A)} @-}
  
  
  --------------------------------------------------------------------------------
  --- From TextRead
  --------------------------------------------------------------------------------
  
  {-@ measure numchars :: Array -> Int -> Int -> Int @-}
  {-@ measure tlength :: Text -> Int @-}
  {-@ invariant {v:Text | (tlength v) = (numchars (tarr v) (toff v) (tlen v))} @-}
  
  --------------------------------------------------------------------------------
  --- Helpers
  --------------------------------------------------------------------------------
  
  {-@ qualif Ord(v:int, i:int, x:Char)
          : ((((ord x) <  65536) => (v = i))
          && (((ord x) >= 65536) => (v = (i + 1))))
    @-}
  
  \end{code}
  
  </div>
  
  We mentioned previously that `text` uses stream fusion to optimize
  multiple loops over a `Text` into a single loop; as a result many of
  the top-level API functions are simple wrappers around equivalent
  functions over `Stream`s. The creation of `Text` values is then
  largely handled by a single function, `unstream`, which converts a
  `Stream` into a `Text`.
  
  \begin{code}
  unstream :: Stream Char -> Text
  unstream (Stream next0 s0 len) = runST $ do
    let mlen = upperBound 4 len
    arr0 <- new mlen
    let outer arr top = loop
         where
          loop !s !i =
              case next0 s of
                Done          -> do
                  arr' <- unsafeFreeze arr
                  return $! Text arr' 0 i
                Skip s'       -> loop s' i
                Yield x s'
                  | j >= top  -> do
                    let top' = (top + 1) `shiftL` 1
                    arr' <- new top'
                    copyM arr' 0 arr 0 top
                    outer arr' top' s i
                  | otherwise -> do
                    d <- writeChar arr i x
                    loop s' (i+d)
                  where j | ord x < 0x10000 = i
                          | otherwise       = i + 1
    outer arr0 mlen s0 0
  \end{code}
  
  Since we're focusing on memory safety here we won't go into detail
  about how `Stream`s work. Let's instead jump right into the inner
  `loop` and look at the `Yield` case. Here we need to write a char `x`
  into `arr`, so we compute the maximal index `j` to which we will
  write -- i.e. if `x >= U+10000` then `j = i + 1` -- and determine
  whether we can safely write at `j`. If the write is unsafe we have to
  allocate a larger array before continuing, otherwise we write `x` and
  increment `i` by `x`s width.
  
  Since `writeChar` has to handle writing *any* Unicode value, we need
  to assure it that there will always be room to write `x` into `arr`,
  regardless of `x`s width. Indeed, this is expressed in the type we
  give to `writeChar`.
  
  \begin{code}
  {-@ writeChar :: ma:MArray s -> i:Nat -> {v:Char | (Room v ma i)}
                -> ST s {v:Nat | (RoomN v ma i)}
    @-}
  \end{code}
  
  The predicate aliases `Room` and `RoomN` express that a character can
  fit in the array at index `i` and that there are at least `n` slots
  available starting at `i` respectively.
  
  \begin{code}
  {-@ predicate Room C MA I = (((One C) => (RoomN 1 MA I))
                            && ((Two C) => (RoomN 2 MA I)))
    @-}
  {-@ predicate RoomN N MA I = (I+N <= (malen MA)) @-}
  \end{code}
  
  The `One` and `Two` predicates express that a character will be
  encoded in one or two 16-bit words, by reasoning about its ordinal
  value.
  
  \begin{code}
  {-@ predicate One C = ((ord C) <  65536) @-}
  {-@ predicate Two C = ((ord C) >= 65536) @-}
  \end{code}
  
  As with `numchars`, we leave `ord` abstract, but inform LiquidHaskell
  that the `ord` *function* does in fact return the ordinal value of the
  character.
  
  \begin{code}
  {-@ measure ord :: Char -> Int @-}
  {-@ ord :: c:Char -> {v:Int | v = (ord c)} @-}
  \end{code}
  
  Since `writeChar` assumes that it will never be called unless there is room to
  write `c`, it is safe to just split `c` into 16-bit words and write them into
  the array.
  
  \begin{code}
  writeChar :: MArray s -> Int -> Char -> ST s Int
  writeChar marr i c
      | n < 0x10000 = do
          unsafeWrite marr i (fromIntegral n)
          return 1
      | otherwise = do
          unsafeWrite marr i lo
          unsafeWrite marr (i+1) hi
          return 2
      where n = ord c
            m = n - 0x10000
            lo = fromIntegral $ (m `shiftR` 10) + 0xD800
            hi = fromIntegral $ (m .&. 0x3FF) + 0xDC00
  \end{code}
  
  In typical design-by-contract style, we're putting the burden of proof to
  establish safety on `writeChar`s caller. Now, scroll back up to
  `unstream` and mouse over `j` to see its inferred type.
  \begin{code} You should see something like
  {v:Int | ((ord x >= 65536) => (v == i+1))
        && ((ord x <  65536) => (v == i))}
  \end{code}
  which, combined with the case-split on `j >= top`, provides the proof that
  writing `x` will be safe!
  
  Stay tuned, next time we'll look at another example of building a `Text` where
  LiquidHaskell fails to infer this crucial refinement...
  