Use an immutable list as private storage and cache its length. This makes the data refinement transparent without depending on library-specific dynamic array costs:The representation invariant is , with
class DocImpl extends Doc {
private var chars: List[Char] = Nil
private var length: Int = 0
def size: Int = length
def insert(x: Char, pos: Int): Unit = {
require(0 <= pos && pos <= length)
val parts = chars.splitAt(pos)
chars = parts._1 ::: (x :: parts._2)
length += 1
}
def delete(pos: Int): Char = {
require(0 <= pos && pos < length)
val parts = chars.splitAt(pos)
val old = parts._2.head
chars = parts._1 ::: parts._2.tail
length -= 1
old
}
def read(pos: Int): Char = {
require(0 <= pos && pos < length)
chars(pos)
}
}chars representing the abstract document sequence. splitAt(pos) isolates exactly the prefix before the selected array index-style position. Insertion retains that prefix and the old suffix, placing the new character between them. Deletion returns the old suffix head and retains its tail. Updating the cached length by one preserves the representation invariant. read and size preserve the abstract state.The preconditions permit insertion at the end, including position zero in an empty document, but forbid reading or deleting at the end. Articles by others on the same topic
There are currently no matching articles.