Last time, we showed how to reason about Unicode and a variable-width
encoding of Chars when consuming a Text value, today we’ll look at
the same issue from the perspective of building a Text.
22: {-# LANGUAGE BangPatterns, CPP, MagicHash, Rank2Types, RecordWildCards, UnboxedTuples, ExistentialQuantification #-} 24: {-@ LIQUID "--no-termination" @-} 25: module TextWrite where 26: 27: import Control.Monad.ST.Unsafe (unsafeIOToST) 28: import Foreign.C.Types (CSize) 29: import GHC.Base hiding (unsafeChr) 30: import GHC.ST 31: import GHC.Word (Word16(..)) 32: import Data.Bits hiding (shiftL) 33: import Data.Word 34: 35: import Language.Haskell.Liquid.Prelude 36: 37: -------------------------------------------------------------------------------- 38: --- From TextInternal 39: -------------------------------------------------------------------------------- 40: 41: {-@ shiftL :: i:Nat -> n:Nat -> {v:Nat | ((n = 1) => (v = (i * 2)))} @-} 42: shiftL :: Int -> Int -> Int 43: x1:{v : GHC.Types.Int | (v >= 0)} -> x2:{v : GHC.Types.Int | (v >= 0)} -> {v : GHC.Types.Int | ((x2 == 1) => (v == (x1 * 2))) && (v >= 0)}shiftL = forall a. aundefined -- (I# x#) (I# i#) = I# (x# `iShiftL#` i#) 44: 45: {-@ measure isUnknown :: Size -> Prop 46: isUnknown (Exact n) = false 47: isUnknown (Max n) = false 48: isUnknown (Unknown) = true 49: @-} 50: {-@ measure getSize :: Size -> Int 51: getSize (Exact n) = n 52: getSize (Max n) = n 53: @-} 54: 55: {-@ invariant {v:Size | (getSize v) >= 0} @-} 56: 57: data Size = Exact {-# UNPACK #-} !Int -- ^ Exact size. 58: | Max {-# UNPACK #-} !Int -- ^ Upper bound on size. 59: | Unknown -- ^ Unknown size. 60: deriving (Eq, Show) 61: 62: {-@ upperBound :: k:Nat -> s:Size -> {v:Nat | v = ((isUnknown s) ? k : (getSize s))} @-} 63: upperBound :: Int -> Size -> Int 64: x1:{v : GHC.Types.Int | (v >= 0)} -> x2:TextWrite.Size -> {v : GHC.Types.Int | (v == (if ((isUnknown x2)) then x1 else (getSize x2))) && (v >= 0)}upperBound _ (Exact n) = {x2 : GHC.Types.Int | (x2 == n)}n 65: upperBound _ (Max n) = {x2 : GHC.Types.Int | (x2 == n)}n 66: upperBound k _ = {x2 : GHC.Types.Int | (x2 >= 0)}k 67: 68: data Step s a = Done 69: | Skip !s 70: | Yield !a !s 71: 72: data Stream a = 73: forall s. Stream 74: (s -> Step s a) -- stepper function 75: !s -- current state 76: !Size -- size hint 77: 78: {-@ data Array = Array { aBA :: ByteArray# 79: , aLen :: Nat 80: } 81: @-} 82: 83: data Array = Array { 84: TextWrite.Array -> GHC.Prim.ByteArray#aBA :: ByteArray# 85: , x1:TextWrite.Array -> {v : GHC.Types.Int | (v == (alen x1)) && (v >= 0)}aLen :: !Int 86: } 87: 88: {-@ measure alen :: Array -> Int 89: alen (Array a n) = n 90: @-} 91: 92: {-@ aLen :: a:Array -> {v:Nat | v = (alen a)} @-} 93: 94: {-@ type ArrayN N = {v:Array | (alen v) = N} @-} 95: 96: {-@ type AValidI A = {v:Nat | v < (alen A)} @-} 97: {-@ type AValidO A = {v:Nat | v <= (alen A)} @-} 98: {-@ type AValidL O A = {v:Nat | (v+O) <= (alen A)} @-} 99: 100: {-@ data MArray s = MArray { maBA :: MutableByteArray# s 101: , maLen :: Nat } @-} 102: 103: data MArray s = MArray { 104: forall a. (TextWrite.MArray a) -> (GHC.Prim.MutableByteArray# a)maBA :: MutableByteArray# s 105: , forall a. x1:(TextWrite.MArray a) -> {v : GHC.Types.Int | (v == (malen x1)) && (v >= 0)}maLen :: !Int 106: } 107: 108: {-@ measure malen :: MArray s -> Int 109: malen (MArray a n) = n 110: @-} 111: 112: {-@ maLen :: a:MArray s -> {v:Nat | v = (malen a)} @-} 113: 114: {-@ type MArrayN s N = {v:MArray s | (malen v) = N} @-} 115: 116: {-@ type MAValidI MA = {v:Nat | v < (malen MA)} @-} 117: {-@ type MAValidO MA = {v:Nat | v <= (malen MA)} @-} 118: 119: {-@ new :: forall s. n:Nat -> ST s (MArrayN s n) @-} 120: new :: forall s. Int -> ST s (MArray s) 121: forall a. x1:{v : GHC.Types.Int | (v >= 0)} -> (GHC.ST.ST a {v : (TextWrite.MArray a) | ((malen v) == x1)})new {v : GHC.Types.Int | (v >= 0)}n 122: | {x3 : GHC.Types.Int | (x3 == n) && (x3 >= 0)}n x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : GHC.Types.Int | (x2 == (0 : int))}0 x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (((Prop x1)) || ((Prop x2))))}|| {x3 : GHC.Types.Int | (x3 == n) && (x3 >= 0)}n GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int.&. {x2 : GHC.Types.Int | (x2 == highBit)}highBit x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 /= x2))}/= {x2 : GHC.Types.Int | (x2 == (0 : int))}0 = [GHC.Types.Char] -> {x1 : (GHC.ST.ST a {x2 : (TextWrite.MArray a) | false}) | false}error ({x10 : [GHC.Types.Char] | ((len x10) >= 0)} -> {x7 : (GHC.ST.ST a {x8 : (TextWrite.MArray a) | false}) | false}) -> {x10 : [GHC.Types.Char] | ((len x10) >= 0)} -> {x7 : (GHC.ST.ST a {x8 : (TextWrite.MArray a) | false}) | false}$ {x2 : [GHC.Types.Char] | ((len x2) >= 0)}"Data.Text.Array.new: size overflow" 123: | otherwise = ((GHC.Prim.State# a) -> ((GHC.Prim.State# a), {x7 : (TextWrite.MArray a) | ((malen x7) == n)})) -> (GHC.ST.ST a {x3 : (TextWrite.MArray a) | ((malen x3) == n)})ST (((GHC.Prim.State# a) -> ((GHC.Prim.State# a), {x17 : (TextWrite.MArray a) | ((malen x17) == n)})) -> (GHC.ST.ST a {x12 : (TextWrite.MArray a) | ((malen x12) == n)})) -> ((GHC.Prim.State# a) -> ((GHC.Prim.State# a), {x17 : (TextWrite.MArray a) | ((malen x17) == n)})) -> (GHC.ST.ST a {x12 : (TextWrite.MArray a) | ((malen x12) == n)})$ \(GHC.Prim.State# a)s1# -> 124: case GHC.Prim.Int# -> (GHC.Prim.State# a) -> ((GHC.Prim.State# a), (GHC.Prim.MutableByteArray# a))newByteArray# {x2 : GHC.Prim.Int# | (x2 == len)}len# {x2 : (GHC.Prim.State# a) | (x2 == s1)}s1# of 125: (# s2#, marr# #) -> forall a b. a -> b -> (a, b)(# {x2 : (GHC.Prim.State# a) | (x2 == s2)}s2#, x1:(GHC.Prim.MutableByteArray# a) -> x2:{x6 : GHC.Types.Int | (x6 >= 0)} -> {x4 : (TextWrite.MArray a) | ((maBA x4) == x1) && ((maLen x4) == x2) && ((malen x4) == x2)}MArray {x2 : (GHC.Prim.MutableByteArray# a) | (x2 == marr)}marr# {x3 : GHC.Types.Int | (x3 == n) && (x3 >= 0)}n #) 126: where !(I# len#) = x1:{x12 : GHC.Types.Int | (x12 == n) && (x12 == (if ((isUnknown TextWrite.Unknown)) then n else (getSize TextWrite.Unknown))) && (x12 >= 0)} -> {x8 : GHC.Types.Int | ((x1 == 1) => (x8 == (x1 * 2))) && ((x1 == 1) => (x8 == (n * 2))) && ((n == 1) => (x8 == (x1 * 2))) && ((n == 1) => (x8 == (n * 2))) && (x8 >= 0) && (x8 >= x1) && (x8 >= n)}bytesInArray {x3 : GHC.Types.Int | (x3 == n) && (x3 >= 0)}n 127: GHC.Types.InthighBit = GHC.Types.IntmaxBound GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int`xor` (GHC.Types.IntmaxBound GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int`shiftR` {x2 : GHC.Types.Int | (x2 == (1 : int))}1) 128: n:{VV : GHC.Types.Int | (VV == n) && (VV == (if ((isUnknown TextWrite.Unknown)) then n else (getSize TextWrite.Unknown))) && (VV >= 0)} -> {VV : GHC.Types.Int | ((n == 1) => (VV == (n * 2))) && ((n == 1) => (VV == (n * 2))) && ((n == 1) => (VV == (n * 2))) && ((n == 1) => (VV == (n * 2))) && (VV >= 0) && (VV >= n) && (VV >= n)}bytesInArray {VV : GHC.Types.Int | (VV == n) && (VV == (if ((isUnknown TextWrite.Unknown)) then n else (getSize TextWrite.Unknown))) && (VV >= 0)}n = {x5 : GHC.Types.Int | (x5 == n) && (x5 == n) && (x5 == (if ((isUnknown TextWrite.Unknown)) then n else (getSize TextWrite.Unknown))) && (x5 >= 0)}n x1:{x7 : GHC.Types.Int | (x7 >= 0)} -> x2:{x5 : GHC.Types.Int | (x5 >= 0)} -> {x3 : GHC.Types.Int | ((x2 == 1) => (x3 == (x1 * 2))) && (x3 >= 0)}`shiftL` {x2 : GHC.Types.Int | (x2 == (1 : int))}1 129: 130: {-@ unsafeWrite :: ma:MArray s -> MAValidI ma -> Word16 -> ST s () @-} 131: unsafeWrite :: MArray s -> Int -> Word16 -> ST s () 132: forall a. x1:(TextWrite.MArray a) -> {v : GHC.Types.Int | (v >= 0) && (v < (malen x1))} -> GHC.Word.Word16 -> (GHC.ST.ST a ())unsafeWrite MArray{..} {v : GHC.Types.Int | (v >= 0)}i@(I# i#) (W16# e#) 133: | {x5 : GHC.Types.Int | (x5 == i) && (x5 == i) && (x5 == (i : int)) && (x5 >= 0)}i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : GHC.Types.Int | (x2 == (0 : int))}0 x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (((Prop x1)) || ((Prop x2))))}|| {x5 : GHC.Types.Int | (x5 == i) && (x5 == i) && (x5 == (i : int)) && (x5 >= 0)}i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 >= x2))}>= {x2 : GHC.Types.Int | (x2 >= 0)}maLen = {x3 : [GHC.Types.Char] | false} -> (GHC.ST.ST a ())liquidError {x2 : [GHC.Types.Char] | ((len x2) >= 0)}"out of bounds" 134: | otherwise = ((GHC.Prim.State# a) -> ((GHC.Prim.State# a), ())) -> (GHC.ST.ST a ())ST (((GHC.Prim.State# a) -> ((GHC.Prim.State# a), ())) -> (GHC.ST.ST a ())) -> ((GHC.Prim.State# a) -> ((GHC.Prim.State# a), ())) -> (GHC.ST.ST a ())$ \(GHC.Prim.State# a)s1# -> 135: case (GHC.Prim.MutableByteArray# a) -> GHC.Prim.Int# -> GHC.Prim.Word# -> (GHC.Prim.State# a) -> (GHC.Prim.State# a)writeWord16Array# (GHC.Prim.MutableByteArray# a)maBA {x2 : GHC.Prim.Int# | (x2 == i)}i# {x2 : GHC.Prim.Word# | (x2 == e)}e# {x2 : (GHC.Prim.State# a) | (x2 == s1)}s1# of 136: s2# -> forall a b. a -> b -> (a, b)(# (GHC.Prim.State# a)s2#, {x2 : () | (x2 == GHC.Tuple.())}() #) 137: 138: {-@ copyM :: dest:MArray s 139: -> didx:MAValidO dest 140: -> src:MArray s 141: -> sidx:MAValidO src 142: -> {v:Nat | (((didx + v) <= (malen dest)) && ((sidx + v) <= (malen src)))} 144: -> ST s () 145: @-} 146: copyM :: MArray s -- ^ Destination 147: -> Int -- ^ Destination offset 148: -> MArray s -- ^ Source 149: -> Int -- ^ Source offset 150: -> Int -- ^ Count 151: -> ST s () 152: forall a. x1:(TextWrite.MArray a) -> x2:{v : GHC.Types.Int | (v >= 0) && (v <= (malen x1))} -> x3:(TextWrite.MArray a) -> x4:{v : GHC.Types.Int | (v >= 0) && (v <= (malen x3))} -> {v : GHC.Types.Int | (v >= 0) && ((x2 + v) <= (malen x1)) && ((x4 + v) <= (malen x3))} -> (GHC.ST.ST a ())copyM (TextWrite.MArray a)dest {v : GHC.Types.Int | (v >= 0) && (v <= (malen dest))}didx (TextWrite.MArray a)src {v : GHC.Types.Int | (v >= 0) && (v <= (malen src))}sidx {v : GHC.Types.Int | (v >= 0) && ((didx + v) <= (malen dest)) && ((sidx + v) <= (malen src))}count 153: | {x5 : GHC.Types.Int | (x5 == count) && (x5 >= 0) && ((didx + x5) <= (malen dest)) && ((sidx + x5) <= (malen src))}count x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 <= x2))}<= {x2 : GHC.Types.Int | (x2 == (0 : int))}0 = () -> (GHC.ST.ST a ())return {x2 : () | (x2 == GHC.Tuple.())}() 154: | otherwise = 155: {x6 : GHC.Types.Bool | ((Prop x6))} -> (GHC.ST.ST a ()) -> (GHC.ST.ST a ())liquidAssert ({x4 : GHC.Types.Int | (x4 == sidx) && (x4 >= 0) && (x4 <= (malen src))}sidx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+ {x5 : GHC.Types.Int | (x5 == count) && (x5 >= 0) && ((didx + x5) <= (malen dest)) && ((sidx + x5) <= (malen src))}count x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 <= x2))}<= x1:(TextWrite.MArray a) -> {x3 : GHC.Types.Int | (x3 == (malen x1)) && (x3 >= 0)}maLen {x2 : (TextWrite.MArray a) | (x2 == src)}src) ((GHC.ST.ST a ()) -> (GHC.ST.ST a ())) -> ((GHC.Types.IO ()) -> (GHC.ST.ST a ())) -> (GHC.Types.IO ()) -> exists [(GHC.ST.ST a ())].(GHC.ST.ST a ()). 156: {x6 : GHC.Types.Bool | ((Prop x6))} -> (GHC.ST.ST a ()) -> (GHC.ST.ST a ())liquidAssert ({x4 : GHC.Types.Int | (x4 == didx) && (x4 >= 0) && (x4 <= (malen dest))}didx x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+ {x5 : GHC.Types.Int | (x5 == count) && (x5 >= 0) && ((didx + x5) <= (malen dest)) && ((sidx + x5) <= (malen src))}count x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 <= x2))}<= x1:(TextWrite.MArray a) -> {x3 : GHC.Types.Int | (x3 == (malen x1)) && (x3 >= 0)}maLen {x2 : (TextWrite.MArray a) | (x2 == dest)}dest) ((GHC.ST.ST a ()) -> (GHC.ST.ST a ())) -> ((GHC.Types.IO ()) -> (GHC.ST.ST a ())) -> (GHC.Types.IO ()) -> exists [(GHC.ST.ST a ())].(GHC.ST.ST a ()). 157: (GHC.Types.IO ()) -> (GHC.ST.ST a ())unsafeIOToST ((GHC.Types.IO ()) -> (GHC.ST.ST a ())) -> (GHC.Types.IO ()) -> (GHC.ST.ST a ())$ (GHC.Prim.MutableByteArray# a) -> Foreign.C.Types.CSize -> (GHC.Prim.MutableByteArray# a) -> Foreign.C.Types.CSize -> Foreign.C.Types.CSize -> (GHC.Types.IO ())memcpyM ((TextWrite.MArray a) -> (GHC.Prim.MutableByteArray# a)maBA {x2 : (TextWrite.MArray a) | (x2 == dest)}dest) (x1:GHC.Types.Int -> {x2 : Foreign.C.Types.CSize | (x2 == x1)}fromIntegral {x4 : GHC.Types.Int | (x4 == didx) && (x4 >= 0) && (x4 <= (malen dest))}didx) 158: ((TextWrite.MArray a) -> (GHC.Prim.MutableByteArray# a)maBA {x2 : (TextWrite.MArray a) | (x2 == src)}src) (x1:GHC.Types.Int -> {x2 : Foreign.C.Types.CSize | (x2 == x1)}fromIntegral {x4 : GHC.Types.Int | (x4 == sidx) && (x4 >= 0) && (x4 <= (malen src))}sidx) 159: (x1:GHC.Types.Int -> {x2 : Foreign.C.Types.CSize | (x2 == x1)}fromIntegral {x5 : GHC.Types.Int | (x5 == count) && (x5 >= 0) && ((didx + x5) <= (malen dest)) && ((sidx + x5) <= (malen src))}count) 160: 161: {-@ memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () @-} 162: memcpyM :: MutableByteArray# s -> CSize -> MutableByteArray# s -> CSize -> CSize -> IO () 163: forall a. (GHC.Prim.MutableByteArray# a) -> Foreign.C.Types.CSize -> (GHC.Prim.MutableByteArray# a) -> Foreign.C.Types.CSize -> Foreign.C.Types.CSize -> (GHC.Types.IO ())memcpyM = forall a. aundefined 164: 165: {-@ unsafeFreeze :: ma:MArray s -> ST s (ArrayN (malen ma)) @-} 166: unsafeFreeze :: MArray s -> ST s Array 167: forall a. x1:(TextWrite.MArray a) -> (GHC.ST.ST a {v : TextWrite.Array | ((alen v) == (malen x1))})unsafeFreeze MArray{..} = ((GHC.Prim.State# a) -> ((GHC.Prim.State# a), {x5 : TextWrite.Array | false})) -> (GHC.ST.ST a {x2 : TextWrite.Array | false})ST (((GHC.Prim.State# a) -> {x11 : ((GHC.Prim.State# a), {x13 : TextWrite.Array | false}) | false}) -> (GHC.ST.ST a {x9 : TextWrite.Array | false})) -> ((GHC.Prim.State# a) -> {x11 : ((GHC.Prim.State# a), {x13 : TextWrite.Array | false}) | false}) -> (GHC.ST.ST a {x9 : TextWrite.Array | false})$ \(GHC.Prim.State# a)s# -> 168: forall a b. a -> b -> (a, b)(# {x2 : (GHC.Prim.State# a) | (x2 == s)}s#, x1:GHC.Prim.ByteArray# -> x2:{x6 : GHC.Types.Int | (x6 >= 0)} -> {x4 : TextWrite.Array | ((aBA x4) == x1) && ((aLen x4) == x2) && ((alen x4) == x2)}Array ((GHC.Prim.MutableByteArray# a) -> {x1 : GHC.Prim.ByteArray# | false}unsafeCoerce# (GHC.Prim.MutableByteArray# a)maBA) {x2 : GHC.Types.Int | (x2 >= 0)}maLen #) 169: 170: {-@ unsafeIndex :: a:Array -> AValidI a -> Word16 @-} 171: unsafeIndex :: Array -> Int -> Word16 172: x1:TextWrite.Array -> {v : GHC.Types.Int | (v >= 0) && (v < (alen x1))} -> GHC.Word.Word16unsafeIndex Array{..} {v : GHC.Types.Int | (v >= 0)}i@(I# i#) 173: | {x5 : GHC.Types.Int | (x5 == i) && (x5 == i) && (x5 == (i : int)) && (x5 >= 0)}i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : GHC.Types.Int | (x2 == (0 : int))}0 x1:GHC.Types.Bool -> x2:GHC.Types.Bool -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (((Prop x1)) || ((Prop x2))))}|| {x5 : GHC.Types.Int | (x5 == i) && (x5 == i) && (x5 == (i : int)) && (x5 >= 0)}i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 >= x2))}>= {x2 : GHC.Types.Int | (x2 >= 0)}aLen = {x2 : [GHC.Types.Char] | false} -> GHC.Word.Word16liquidError {x2 : [GHC.Types.Char] | ((len x2) >= 0)}"out of bounds" 174: | otherwise = case GHC.Prim.ByteArray# -> GHC.Prim.Int# -> GHC.Prim.Word#indexWord16Array# GHC.Prim.ByteArray#aBA {x2 : GHC.Prim.Int# | (x2 == i)}i# of 175: r# -> (GHC.Prim.Word# -> GHC.Word.Word16W16# GHC.Prim.Word#r#) 176: 177: data Text = Text Array Int Int 178: {-@ data Text [tlen] = Text (tarr :: Array) 179: (toff :: TValidO tarr) 180: (tlen :: TValidL toff tarr) 181: @-} 182: 183: {-@ type TValidI T = {v:Nat | v < (tlen T)} @-} 184: {-@ type TValidO A = {v:Nat | v <= (alen A)} @-} 185: {-@ type TValidL O A = {v:Nat | (v+O) <= (alen A)} @-} 186: 187: 188: -------------------------------------------------------------------------------- 189: --- From TextRead 190: -------------------------------------------------------------------------------- 191: 192: {-@ measure numchars :: Array -> Int -> Int -> Int @-} 193: {-@ measure tlength :: Text -> Int @-} 194: {-@ invariant {v:Text | (tlength v) = (numchars (tarr v) (toff v) (tlen v))} @-} 195: 196: -------------------------------------------------------------------------------- 197: --- Helpers 198: -------------------------------------------------------------------------------- 199: 200: {-@ qualif Ord(v:int, i:int, x:Char) 201: : ((((ord x) < 65536) => (v = i)) 202: && (((ord x) >= 65536) => (v = (i + 1)))) 203: @-} 204:
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 Streams. The creation of Text values is then
largely handled by a single function, unstream, which converts a
Stream into a Text.
217: unstream :: Stream Char -> Text 218: (TextWrite.Stream GHC.Types.Char) -> TextWrite.Textunstream (Stream next0 s0 len) = (forall s. (GHC.ST.ST s TextWrite.Text)) -> TextWrite.TextrunST ((forall s. (GHC.ST.ST s TextWrite.Text)) -> TextWrite.Text) -> (forall s. (GHC.ST.ST s TextWrite.Text)) -> TextWrite.Text$ do 219: let {x2 : GHC.Types.Int | (x2 >= 0)}mlen = x1:{x6 : GHC.Types.Int | (x6 >= 0)} -> x2:TextWrite.Size -> {x3 : GHC.Types.Int | (x3 == (if ((isUnknown x2)) then x1 else (getSize x2))) && (x3 >= 0)}upperBound {x2 : GHC.Types.Int | (x2 == (4 : int))}4 {x3 : TextWrite.Size | (x3 == len) && ((getSize x3) >= 0)}len 220: {VV : (TextWrite.MArray a) | ((malen VV) == mlen)}arr0 <- x1:{x5 : GHC.Types.Int | (x5 >= 0)} -> (GHC.ST.ST a {x3 : (TextWrite.MArray a) | ((malen x3) == x1)})new {x3 : GHC.Types.Int | (x3 == mlen) && (x3 >= 0)}mlen 221: let x1:(TextWrite.MArray a) -> x2:{VV : GHC.Types.Int | (VV == (malen x1)) && (VV >= 0) && (VV >= mlen)} -> b -> {VV : GHC.Types.Int | (VV >= 0) && (VV <= x2) && (VV <= (malen x1)) && ((mlen + VV) <= (malen x1))} -> (GHC.ST.ST a TextWrite.Text)outer (TextWrite.MArray a)arr {VV : GHC.Types.Int | (VV == (malen arr)) && (VV >= 0) && (VV >= mlen)}top = a -> {x6 : GHC.Types.Int | (x6 >= 0) && (x6 <= top) && (x6 <= (malen arr))} -> (GHC.ST.ST b TextWrite.Text)loop 222: where 223: a -> {VV : GHC.Types.Int | (VV >= 0) && (VV <= top) && (VV <= (malen arr))} -> (GHC.ST.ST b TextWrite.Text)loop !as !{VV : GHC.Types.Int | (VV >= 0) && (VV <= top) && (VV <= (malen arr))}i = 224: case a -> (TextWrite.Step a GHC.Types.Char)next0 {VV : a | (VV == s)}s of 225: Done -> do 226: {VV : TextWrite.Array | ((alen VV) == (malen arr))}arr' <- x1:(TextWrite.MArray a) -> (GHC.ST.ST a {x3 : TextWrite.Array | ((alen x3) == (malen x1))})unsafeFreeze {x2 : (TextWrite.MArray a) | (x2 == arr)}arr 227: TextWrite.Text -> (GHC.ST.ST a TextWrite.Text)return (TextWrite.Text -> (GHC.ST.ST a TextWrite.Text)) -> TextWrite.Text -> (GHC.ST.ST a TextWrite.Text)$! x1:TextWrite.Array -> x2:{x10 : GHC.Types.Int | (x10 >= 0) && (x10 <= (alen x1))} -> x3:{x7 : GHC.Types.Int | (x7 >= 0) && ((x7 + x2) <= (alen x1))} -> {x4 : TextWrite.Text | ((tarr x4) == x1) && ((tlen x4) == x3) && ((toff x4) == x2)}Text {x3 : TextWrite.Array | (x3 == arr') && ((alen x3) == (malen arr))}arr' {x2 : GHC.Types.Int | (x2 == (0 : int))}0 {x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}i 228: Skip s' -> a -> {VV : GHC.Types.Int | (VV >= 0) && (VV <= top) && (VV <= (malen arr))} -> (GHC.ST.ST b TextWrite.Text)loop {VV : a | (VV == s')}s' {x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}i 229: Yield x s' 230: | {x6 : GHC.Types.Int | (((ord x) >= 65536) => (x6 == (i + 1))) && (((ord x) < 65536) => (x6 == i)) && (x6 == j) && (x6 >= 0) && (x6 >= i)}j x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 >= x2))}>= {x5 : GHC.Types.Int | (x5 == top) && (x5 == (malen arr)) && (x5 >= 0) && (x5 >= mlen)}top -> do 231: let {x2 : GHC.Types.Int | (x2 >= 0)}top' = ({x5 : GHC.Types.Int | (x5 == top) && (x5 == (malen arr)) && (x5 >= 0) && (x5 >= mlen)}top x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+ {x2 : GHC.Types.Int | (x2 == (1 : int))}1) x1:{x7 : GHC.Types.Int | (x7 >= 0)} -> x2:{x5 : GHC.Types.Int | (x5 >= 0)} -> {x3 : GHC.Types.Int | ((x2 == 1) => (x3 == (x1 * 2))) && (x3 >= 0)}`shiftL` {x2 : GHC.Types.Int | (x2 == (1 : int))}1 232: {VV : (TextWrite.MArray a) | ((malen VV) == top') && (VV /= arr)}arr' <- x1:{x5 : GHC.Types.Int | (x5 >= 0)} -> (GHC.ST.ST a {x3 : (TextWrite.MArray a) | ((malen x3) == x1)})new {x3 : GHC.Types.Int | (x3 == top') && (x3 >= 0)}top' 233: x1:(TextWrite.MArray a) -> x2:{x13 : GHC.Types.Int | (x13 >= 0) && (x13 <= (malen x1))} -> x3:(TextWrite.MArray a) -> x4:{x9 : GHC.Types.Int | (x9 >= 0) && (x9 <= (malen x3))} -> {x6 : GHC.Types.Int | (x6 >= 0) && ((x2 + x6) <= (malen x1)) && ((x4 + x6) <= (malen x3))} -> (GHC.ST.ST a ())copyM {x4 : (TextWrite.MArray a) | (x4 == arr') && ((malen x4) == top') && (x4 /= arr)}arr' {x2 : GHC.Types.Int | (x2 == (0 : int))}0 {x2 : (TextWrite.MArray a) | (x2 == arr)}arr {x2 : GHC.Types.Int | (x2 == (0 : int))}0 {x5 : GHC.Types.Int | (x5 == top) && (x5 == (malen arr)) && (x5 >= 0) && (x5 >= mlen)}top 234: x1:(TextWrite.MArray a) -> x2:{VV : GHC.Types.Int | (VV == (malen x1)) && (VV >= 0) && (VV >= mlen)} -> b -> {VV : GHC.Types.Int | (VV >= 0) && (VV <= x2) && (VV <= (malen x1)) && ((mlen + VV) <= (malen x1))} -> (GHC.ST.ST a TextWrite.Text)outer {x4 : (TextWrite.MArray a) | (x4 == arr') && ((malen x4) == top') && (x4 /= arr)}arr' {x3 : GHC.Types.Int | (x3 == top') && (x3 >= 0)}top' {VV : a | (VV == s)}s {x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}i 235: | otherwise -> do 236: {VV : GHC.Types.Int | (VV >= 0) && (VV <= top) && (VV <= (malen arr)) && ((i + VV) <= (malen arr))}d <- x1:(TextWrite.MArray a) -> x2:{x9 : GHC.Types.Int | (x9 >= 0)} -> {x7 : GHC.Types.Char | (((ord x7) >= 65536) => ((x2 + 2) <= (malen x1))) && (((ord x7) < 65536) => ((x2 + 1) <= (malen x1)))} -> (GHC.ST.ST a {x4 : GHC.Types.Int | (x4 >= 0) && ((x2 + x4) <= (malen x1))})writeChar {x2 : (TextWrite.MArray a) | (x2 == arr)}arr {x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}i {x2 : GHC.Types.Char | (x2 == x)}x 237: a -> {VV : GHC.Types.Int | (VV >= 0) && (VV <= top) && (VV <= (malen arr))} -> (GHC.ST.ST b TextWrite.Text)loop {VV : a | (VV == s')}s' ({x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}ix1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+{x6 : GHC.Types.Int | (x6 == d) && (x6 >= 0) && (x6 <= top) && (x6 <= (malen arr)) && ((i + x6) <= (malen arr))}d) 238: where {VV : GHC.Types.Int | (((ord x) >= 65536) => (VV == (i + 1))) && (((ord x) < 65536) => (VV == i)) && (VV >= 0) && (VV >= i)}j | x1:GHC.Types.Char -> {x2 : GHC.Types.Int | (x2 == (ord x1))}ord {x2 : GHC.Types.Char | (x2 == x)}x x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : GHC.Types.Int | (x2 == (65536 : int))}0x10000 = {x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}i 239: | otherwise = {x5 : GHC.Types.Int | (x5 == i) && (x5 >= 0) && (x5 <= top) && (x5 <= (malen arr))}i x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+ {x2 : GHC.Types.Int | (x2 == (1 : int))}1 240: x1:{x22 : (TextWrite.MArray a) | ((malen x22) == mlen)} -> x2:{x20 : GHC.Types.Int | (x20 == mlen) && (x20 == (malen arr0)) && (x20 == (malen x1)) && (x20 == (if ((isUnknown TextWrite.Unknown)) then mlen else (getSize TextWrite.Unknown))) && (x20 == (if ((isUnknown len)) then mlen else (getSize len))) && (x20 >= 0)} -> {VV : b | (VV == s0)} -> {x13 : GHC.Types.Int | (x13 == 0) && (x13 >= 0) && (x13 <= x2) && (x13 <= mlen) && (x13 <= (malen arr0)) && (x13 <= (malen x1)) && ((x2 + x13) <= (malen arr0)) && ((x2 + x13) <= (malen x1)) && ((mlen + x13) <= (malen arr0)) && ((mlen + x13) <= (malen x1))} -> (GHC.ST.ST a TextWrite.Text)outer {x3 : (TextWrite.MArray a) | (x3 == arr0) && ((malen x3) == mlen)}arr0 {x3 : GHC.Types.Int | (x3 == mlen) && (x3 >= 0)}mlen {VV : a | (VV == s0)}s0 {x2 : GHC.Types.Int | (x2 == (0 : int))}0
Since we’re focusing on memory safety here we won’t go into detail
about how Streams 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 xs 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 xs width. Indeed, this is expressed in the type we
give to writeChar.
258: {-@ writeChar :: ma:MArray s -> i:Nat -> {v:Char | (Room v ma i)} 259: -> ST s {v:Nat | (RoomN v ma i)} 260: @-}
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.
268: {-@ predicate Room C MA I = (((One C) => (RoomN 1 MA I)) 269: && ((Two C) => (RoomN 2 MA I))) 270: @-} 271: {-@ predicate RoomN N MA I = (I+N <= (malen MA)) @-}
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.
279: {-@ predicate One C = ((ord C) < 65536) @-} 280: {-@ predicate Two C = ((ord C) >= 65536) @-}
As with numchars, we leave ord abstract, but inform LiquidHaskell
that the ord function does in fact return the ordinal value of the
character.
288: {-@ measure ord :: Char -> Int @-} 289: {-@ ord :: c:Char -> {v:Int | v = (ord c)} @-}
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.
297: writeChar :: MArray s -> Int -> Char -> ST s Int 298: forall a. x1:(TextWrite.MArray a) -> x2:{v : GHC.Types.Int | (v >= 0)} -> {v : GHC.Types.Char | (((ord v) >= 65536) => ((x2 + 2) <= (malen x1))) && (((ord v) < 65536) => ((x2 + 1) <= (malen x1)))} -> (GHC.ST.ST a {v : GHC.Types.Int | (v >= 0) && ((x2 + v) <= (malen x1))})writeChar (TextWrite.MArray a)marr {v : GHC.Types.Int | (v >= 0)}i {v : GHC.Types.Char | (((ord v) >= 65536) => ((i + 2) <= (malen marr))) && (((ord v) < 65536) => ((i + 1) <= (malen marr)))}c 299: | {x3 : GHC.Types.Int | (x3 == n) && (x3 == (ord c))}n x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x2 : GHC.Types.Bool | (((Prop x2)) <=> (x1 < x2))}< {x2 : GHC.Types.Int | (x2 == (65536 : int))}0x10000 = do 300: x1:(TextWrite.MArray a) -> {x6 : GHC.Types.Int | (x6 >= 0) && (x6 < (malen x1))} -> GHC.Word.Word16 -> (GHC.ST.ST a ())unsafeWrite {x2 : (TextWrite.MArray a) | (x2 == marr)}marr {x3 : GHC.Types.Int | (x3 == i) && (x3 >= 0)}i (x1:GHC.Types.Int -> {x2 : GHC.Word.Word16 | (x2 == x1)}fromIntegral {x3 : GHC.Types.Int | (x3 == n) && (x3 == (ord c))}n) 301: {x26 : GHC.Types.Int | ((m == 1) => (x26 == (hi * 2))) && ((m == 1) => (x26 == (i * 2))) && ((m == 1) => (x26 == (lo * 2))) && ((m == 1) => (x26 == (m * 2))) && ((m == 1) => (x26 == (n * 2))) && (x26 == 1) && (x26 > 0) && (x26 > m) && (x26 <= (malen marr)) && ((i + x26) <= (malen marr)) && ((m + x26) <= (malen marr))} -> (GHC.ST.ST a {x26 : GHC.Types.Int | ((m == 1) => (x26 == (hi * 2))) && ((m == 1) => (x26 == (i * 2))) && ((m == 1) => (x26 == (lo * 2))) && ((m == 1) => (x26 == (m * 2))) && ((m == 1) => (x26 == (n * 2))) && (x26 == 1) && (x26 > 0) && (x26 > m) && (x26 <= (malen marr)) && ((i + x26) <= (malen marr)) && ((m + x26) <= (malen marr))})return {x2 : GHC.Types.Int | (x2 == (1 : int))}1 302: | otherwise = do 303: x1:(TextWrite.MArray a) -> {x6 : GHC.Types.Int | (x6 >= 0) && (x6 < (malen x1))} -> GHC.Word.Word16 -> (GHC.ST.ST a ())unsafeWrite {x2 : (TextWrite.MArray a) | (x2 == marr)}marr {x3 : GHC.Types.Int | (x3 == i) && (x3 >= 0)}i {x2 : GHC.Word.Word16 | (x2 == lo)}lo 304: x1:(TextWrite.MArray a) -> {x6 : GHC.Types.Int | (x6 >= 0) && (x6 < (malen x1))} -> GHC.Word.Word16 -> (GHC.ST.ST a ())unsafeWrite {x2 : (TextWrite.MArray a) | (x2 == marr)}marr ({x3 : GHC.Types.Int | (x3 == i) && (x3 >= 0)}ix1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+{x2 : GHC.Types.Int | (x2 == (1 : int))}1) {x2 : GHC.Word.Word16 | (x2 == hi)}hi 305: {x32 : GHC.Types.Int | ((hi == 1) => (x32 == (hi * 2))) && ((i == 1) => (x32 == (i * 2))) && ((lo == 1) => (x32 == (lo * 2))) && ((m == 1) => (x32 == (m * 2))) && ((n == 1) => (x32 == (hi * 2))) && ((n == 1) => (x32 == (i * 2))) && ((n == 1) => (x32 == (lo * 2))) && ((n == 1) => (x32 == (m * 2))) && ((n == 1) => (x32 == (n * 2))) && (x32 > 0) && (x32 >= 0) && (x32 < n) && (x32 <= (malen marr)) && ((i + x32) <= (malen marr))} -> (GHC.ST.ST a {x32 : GHC.Types.Int | ((hi == 1) => (x32 == (hi * 2))) && ((i == 1) => (x32 == (i * 2))) && ((lo == 1) => (x32 == (lo * 2))) && ((m == 1) => (x32 == (m * 2))) && ((n == 1) => (x32 == (hi * 2))) && ((n == 1) => (x32 == (i * 2))) && ((n == 1) => (x32 == (lo * 2))) && ((n == 1) => (x32 == (m * 2))) && ((n == 1) => (x32 == (n * 2))) && (x32 > 0) && (x32 >= 0) && (x32 < n) && (x32 <= (malen marr)) && ((i + x32) <= (malen marr))})return {x2 : GHC.Types.Int | (x2 == (2 : int))}2 306: where {x2 : GHC.Types.Int | (x2 == (ord c))}n = x1:GHC.Types.Char -> {x2 : GHC.Types.Int | (x2 == (ord x1))}ord {x4 : GHC.Types.Char | (((ord x4) >= 65536) => ((i + 2) <= (malen marr))) && (((ord x4) < 65536) => ((i + 1) <= (malen marr))) && (x4 == c)}c 307: GHC.Types.Intm = {x3 : GHC.Types.Int | (x3 == n) && (x3 == (ord c))}n x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 - x2))}- {x2 : GHC.Types.Int | (x2 == (65536 : int))}0x10000 308: GHC.Word.Word16lo = x1:GHC.Types.Int -> {x2 : GHC.Word.Word16 | (x2 == x1)}fromIntegral (GHC.Types.Int -> GHC.Word.Word16) -> GHC.Types.Int -> GHC.Word.Word16$ GHC.Types.Int({x2 : GHC.Types.Int | (x2 == m)}m GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int`shiftR` {x2 : GHC.Types.Int | (x2 == (10 : int))}10) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+ {x2 : GHC.Types.Int | (x2 == (55296 : int))}0xD800 309: GHC.Word.Word16hi = x1:GHC.Types.Int -> {x2 : GHC.Word.Word16 | (x2 == x1)}fromIntegral (GHC.Types.Int -> GHC.Word.Word16) -> GHC.Types.Int -> GHC.Word.Word16$ GHC.Types.Int({x2 : GHC.Types.Int | (x2 == m)}m GHC.Types.Int -> GHC.Types.Int -> GHC.Types.Int.&. {x2 : GHC.Types.Int | (x2 == (1023 : int))}0x3FF) x1:GHC.Types.Int -> x2:GHC.Types.Int -> {x4 : GHC.Types.Int | (x4 == (x1 + x2))}+ {x2 : GHC.Types.Int | (x2 == (56320 : int))}0xDC00
In typical design-by-contract style, we’re putting the burden of proof to
establish safety on writeChars caller. Now, scroll back up to
unstream and mouse over j to see its inferred type.
You should see something like
316: {v:Int | ((ord x >= 65536) => (v == i+1)) 317: && ((ord x < 65536) => (v == i))}
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…