List.ds

-- | Conversions between Text and Lists.
module Data.Text.List
export 
{       textOfCharList;
        charListOfText;
}
import Data.Numeric.Word
import Data.Text.Base
import Data.Text.Char
import Data.List
where


-- | Convert a list of characters to a Text object.
textOfCharList (xx: List Char): Text
 = TextVec
 $ extend RegionText using r with { Alloc r; Read r; Write r }
   in  vectorOfCharList [r] xx


-- | O(n). Convert a text object to a list of characters.
charListOfText (tx: Text): List Char
 = case tx of
        TextVec vec -> charListOfTextVec vec
        _           -> charListOfTextVec (vectorOfText [RegionText] tx)


-- | Unpack a list of characters from a vector.
charListOfTextVec
        (vec: Vector# r Word8)
        : S (Read r) (List Char)
 = go 0
 where  
        go (ix: Nat): S (Read r) (List Char)
         | ix >= (vectorLength# vec - 1)
         = Nil

         | otherwise               
         = do   txChar = promote# (vectorRead# vec ix)
                Cons txChar (go (ix + 1))


-- | Pack a list of characters into a mutable vector.
vectorOfCharList
        [r: Region]
        (xx: List Char)
        : S (Alloc r + Write r) (Vector# r Word8)
 = do
        len     = length xx
        vec     = vectorAlloc# [r] (len + 1)

        fill (ix: Nat) (xx: List Char): S (Write r) Unit
         = case xx of
                Nil     -> ()
                Cons x xs
                 -> do  vectorWrite# vec ix (truncate# x)
                        fill (ix + 1) xs

                 | otherwise
                 -> do  fill (ix + 1) xs
        fill 0 xx

        vectorWrite# vec len 0w8
        vec