2025-08-30 23:05:11 +01:00
|
|
|
structure PersistentVector =
|
|
|
|
|
struct
|
2025-09-29 14:02:07 +01:00
|
|
|
(* Clojure-style persistent vector, for building search list.
|
|
|
|
|
* There is an "int table" too, which stores the last index
|
|
|
|
|
* at the node with the same index.
|
|
|
|
|
* We can use the size table for binary search.
|
|
|
|
|
* *)
|
2025-08-30 23:05:11 +01:00
|
|
|
datatype t =
|
2025-09-29 14:02:07 +01:00
|
|
|
BRANCH of t vector * int vector
|
|
|
|
|
| LEAF of {start: int, finish: int} vector * int vector
|
2025-08-30 23:05:11 +01:00
|
|
|
|
|
|
|
|
val maxSize = 32
|
2025-12-01 12:24:45 +00:00
|
|
|
val halfSize = 16
|
2025-08-30 23:05:11 +01:00
|
|
|
|
2025-09-29 14:49:50 +01:00
|
|
|
fun isEmpty t =
|
|
|
|
|
case t of
|
2025-09-29 14:55:20 +01:00
|
|
|
LEAF (_, sizes) => Vector.length sizes = 0
|
2026-01-15 06:13:38 +00:00
|
|
|
| BRANCH (_, sizes) => Vector.length sizes = 0
|
2025-09-29 14:49:50 +01:00
|
|
|
|
2025-09-29 14:02:07 +01:00
|
|
|
val empty = LEAF (#[], #[])
|
2025-08-30 23:05:11 +01:00
|
|
|
|
|
|
|
|
datatype append_result = APPEND of t | UPDATE of t
|
|
|
|
|
|
2025-09-29 14:29:43 +01:00
|
|
|
fun isInRange (checkIdx, t) =
|
|
|
|
|
case t of
|
|
|
|
|
BRANCH (nodes, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val searchIdx = BinSearch.equalOrMore (checkIdx, sizes)
|
|
|
|
|
in
|
|
|
|
|
if searchIdx = ~1 then
|
|
|
|
|
false
|
2025-12-02 08:53:23 +00:00
|
|
|
else if searchIdx = 0 then
|
2025-09-29 14:29:43 +01:00
|
|
|
isInRange (checkIdx, Vector.sub (nodes, searchIdx))
|
2025-12-02 08:53:23 +00:00
|
|
|
else
|
2025-12-12 10:30:21 +00:00
|
|
|
let
|
|
|
|
|
val nextCheckIdx = checkIdx - Vector.sub (sizes, searchIdx - 1)
|
|
|
|
|
in
|
|
|
|
|
isInRange (nextCheckIdx, Vector.sub (nodes, searchIdx))
|
2025-12-02 08:53:23 +00:00
|
|
|
end
|
2025-09-29 14:29:43 +01:00
|
|
|
end
|
|
|
|
|
| LEAF (values, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val searchIdx = BinSearch.equalOrMore (checkIdx, sizes)
|
|
|
|
|
in
|
|
|
|
|
if searchIdx = ~1 then
|
|
|
|
|
false
|
|
|
|
|
else
|
2025-12-12 10:30:21 +00:00
|
|
|
let
|
|
|
|
|
val {start, finish} = Vector.sub (values, searchIdx)
|
|
|
|
|
in
|
|
|
|
|
checkIdx >= start andalso checkIdx <= finish
|
2025-09-29 14:29:43 +01:00
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
|
2025-09-29 14:02:07 +01:00
|
|
|
fun getFinishIdx t =
|
|
|
|
|
case t of
|
|
|
|
|
BRANCH (_, sizes) => Vector.sub (sizes, Vector.length sizes - 1)
|
|
|
|
|
| LEAF (_, sizes) => Vector.sub (sizes, Vector.length sizes - 1)
|
|
|
|
|
|
2026-01-17 23:14:05 +00:00
|
|
|
fun getStartIdx t =
|
|
|
|
|
case t of
|
|
|
|
|
BRANCH (nodes, _) => getStartIdx (Vector.sub (nodes, 0))
|
|
|
|
|
| LEAF (items, _) =>
|
|
|
|
|
if Vector.length items = 0 then
|
|
|
|
|
0
|
|
|
|
|
else
|
|
|
|
|
#start (Vector.sub (items, 0))
|
|
|
|
|
|
2025-09-29 14:02:07 +01:00
|
|
|
fun helpAppend (start, finish, tree) =
|
2025-08-30 23:05:11 +01:00
|
|
|
case tree of
|
2025-09-29 14:02:07 +01:00
|
|
|
BRANCH (nodes, sizes) =>
|
2025-08-30 23:05:11 +01:00
|
|
|
let
|
|
|
|
|
val lastNode = Vector.sub (nodes, Vector.length nodes - 1)
|
2025-12-02 08:53:23 +00:00
|
|
|
val prevSize =
|
|
|
|
|
if Vector.length sizes > 1 then
|
|
|
|
|
Vector.sub (sizes, Vector.length sizes - 2)
|
|
|
|
|
else
|
|
|
|
|
0
|
2025-08-30 23:05:11 +01:00
|
|
|
in
|
2025-12-02 08:53:23 +00:00
|
|
|
case helpAppend (start - prevSize, finish - prevSize, lastNode) of
|
2025-08-30 23:05:11 +01:00
|
|
|
UPDATE newLast =>
|
|
|
|
|
let
|
2025-09-29 14:02:07 +01:00
|
|
|
val lastPos = Vector.length nodes - 1
|
|
|
|
|
val newNode = Vector.update (nodes, lastPos, newLast)
|
|
|
|
|
val newSizes = Vector.update (sizes, lastPos, finish)
|
|
|
|
|
val newNode = BRANCH (newNode, newSizes)
|
2025-08-30 23:05:11 +01:00
|
|
|
in
|
|
|
|
|
UPDATE newNode
|
|
|
|
|
end
|
|
|
|
|
| APPEND newVec =>
|
2025-12-02 08:53:23 +00:00
|
|
|
if Vector.length nodes = maxSize then
|
2025-12-12 10:30:21 +00:00
|
|
|
let
|
2025-12-02 08:53:23 +00:00
|
|
|
(* adjust "finish" so that it does not consider
|
|
|
|
|
* offset for "lower" vector *)
|
2025-12-12 10:30:21 +00:00
|
|
|
val finish = finish - Vector.sub (sizes, Vector.length sizes - 1)
|
2025-12-08 10:57:00 +00:00
|
|
|
val newNode = BRANCH (#[newVec], #[finish])
|
2025-12-12 10:30:21 +00:00
|
|
|
in
|
2025-12-02 08:53:23 +00:00
|
|
|
APPEND newNode
|
2025-08-30 23:05:11 +01:00
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val newNodes = Vector.concat [nodes, #[newVec]]
|
2025-09-29 14:02:07 +01:00
|
|
|
val newSizes = Vector.concat [sizes, #[finish]]
|
|
|
|
|
val newNodes = BRANCH (newNodes, newSizes)
|
2025-08-30 23:05:11 +01:00
|
|
|
in
|
|
|
|
|
UPDATE newNodes
|
|
|
|
|
end
|
|
|
|
|
end
|
2025-09-29 14:02:07 +01:00
|
|
|
| LEAF (values, sizes) =>
|
|
|
|
|
if Vector.length values + 1 > maxSize then
|
2025-12-02 08:53:23 +00:00
|
|
|
(* when we split a leaf into two vectors,
|
|
|
|
|
* we want to adjust the start and finish parameters
|
|
|
|
|
* so that they don't contain the offset relevant to the
|
|
|
|
|
* "lower" vector, which was split from *)
|
2025-12-12 10:30:21 +00:00
|
|
|
let
|
2025-12-02 08:53:23 +00:00
|
|
|
val prevFinish = Vector.sub (sizes, Vector.length sizes - 1)
|
|
|
|
|
val start = start - prevFinish
|
|
|
|
|
val finish = finish - prevFinish
|
2025-12-08 22:40:38 +00:00
|
|
|
val newNode = LEAF (#[{start = start, finish = finish}], #[finish])
|
2025-12-12 10:30:21 +00:00
|
|
|
in
|
2025-12-02 08:53:23 +00:00
|
|
|
APPEND newNode
|
2025-08-30 23:05:11 +01:00
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
let
|
2025-09-29 14:02:07 +01:00
|
|
|
val newNode = Vector.concat
|
|
|
|
|
[values, #[{start = start, finish = finish}]]
|
|
|
|
|
val newSizes = Vector.concat [sizes, #[finish]]
|
|
|
|
|
val newNode = LEAF (newNode, newSizes)
|
2025-08-30 23:05:11 +01:00
|
|
|
in
|
|
|
|
|
UPDATE newNode
|
|
|
|
|
end
|
|
|
|
|
|
2025-09-29 14:02:07 +01:00
|
|
|
fun append (start, finish, tree) =
|
2025-10-08 08:10:51 +01:00
|
|
|
case helpAppend (start, finish, tree) of
|
|
|
|
|
UPDATE t => t
|
2025-12-12 10:30:21 +00:00
|
|
|
| APPEND newNode =>
|
|
|
|
|
let
|
|
|
|
|
val maxSize = getFinishIdx tree
|
|
|
|
|
in
|
|
|
|
|
BRANCH (#[tree, newNode], #[maxSize, finish])
|
2025-10-08 08:10:51 +01:00
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun getStart tree =
|
|
|
|
|
case tree of
|
|
|
|
|
LEAF (values, _) => Vector.sub (values, 0)
|
|
|
|
|
| BRANCH (nodes, _) => getStart (Vector.sub (nodes, 0))
|
|
|
|
|
|
2026-01-15 05:25:17 +00:00
|
|
|
fun helpNextMatch (cursorIdx, tree, absOffset) =
|
2025-10-08 08:10:51 +01:00
|
|
|
case tree of
|
|
|
|
|
LEAF (values, sizes) =>
|
|
|
|
|
let
|
2025-10-08 10:27:19 +01:00
|
|
|
val idx = BinSearch.equalOrMore (cursorIdx, sizes)
|
2025-10-08 08:10:51 +01:00
|
|
|
in
|
2025-12-12 10:30:21 +00:00
|
|
|
if idx = ~1 then {start = ~1, finish = ~1}
|
2026-01-15 05:25:17 +00:00
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {start, finish} = Vector.sub (values, idx)
|
|
|
|
|
in
|
|
|
|
|
{start = start + absOffset, finish = finish + absOffset}
|
|
|
|
|
end
|
2025-10-08 08:10:51 +01:00
|
|
|
end
|
|
|
|
|
| BRANCH (nodes, sizes) =>
|
|
|
|
|
let
|
2025-10-08 10:27:19 +01:00
|
|
|
val idx = BinSearch.equalOrMore (cursorIdx, sizes)
|
2025-10-08 08:10:51 +01:00
|
|
|
in
|
2026-01-15 05:25:17 +00:00
|
|
|
if idx = ~1 then
|
|
|
|
|
{start = ~1, finish = ~1}
|
|
|
|
|
else if idx = 0 then
|
|
|
|
|
helpNextMatch (cursorIdx, Vector.sub (nodes, idx), absOffset)
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val prevSize = Vector.sub (sizes, idx - 1)
|
|
|
|
|
val cursorIdx = cursorIdx - prevSize
|
|
|
|
|
val absOffset = absOffset + prevSize
|
|
|
|
|
in
|
|
|
|
|
helpNextMatch (cursorIdx, Vector.sub (nodes, idx), absOffset)
|
|
|
|
|
end
|
2025-10-08 08:10:51 +01:00
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun loopNextMatch (prevStart, prevFinish, tree, count) =
|
|
|
|
|
if count = 0 then
|
|
|
|
|
prevStart
|
|
|
|
|
else
|
|
|
|
|
let
|
2026-01-15 05:25:17 +00:00
|
|
|
val {start, finish} = helpNextMatch (prevFinish + 1, tree, 0)
|
2025-10-08 08:10:51 +01:00
|
|
|
in
|
|
|
|
|
if start = ~1 then
|
|
|
|
|
let val {start, finish} = getStart tree
|
|
|
|
|
in loopNextMatch (start, finish, tree, count - 1)
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
loopNextMatch (start, finish, tree, count - 1)
|
|
|
|
|
end
|
|
|
|
|
|
2025-10-08 10:27:19 +01:00
|
|
|
fun nextMatch (cursorIdx, tree, count) =
|
2025-10-08 08:10:51 +01:00
|
|
|
if isEmpty tree then
|
|
|
|
|
~1
|
|
|
|
|
else
|
|
|
|
|
let
|
2026-01-15 05:25:17 +00:00
|
|
|
val {start, finish} = helpNextMatch (cursorIdx, tree, 0)
|
2025-10-08 08:10:51 +01:00
|
|
|
in
|
|
|
|
|
if start = ~1 then
|
|
|
|
|
let val {start, finish} = getStart tree
|
|
|
|
|
in loopNextMatch (start, finish, tree, count - 1)
|
2025-09-29 14:29:43 +01:00
|
|
|
end
|
2025-12-12 10:30:21 +00:00
|
|
|
else if cursorIdx >= start andalso cursorIdx <= finish then
|
|
|
|
|
loopNextMatch (start, finish, tree, count)
|
2025-10-08 08:10:51 +01:00
|
|
|
else
|
2025-12-12 10:30:21 +00:00
|
|
|
loopNextMatch (start, finish, tree, count - 1)
|
2025-10-08 08:10:51 +01:00
|
|
|
end
|
2025-10-08 08:16:20 +01:00
|
|
|
|
2026-01-15 05:39:55 +00:00
|
|
|
fun getLast (tree, absOffset) =
|
2025-10-08 08:16:20 +01:00
|
|
|
case tree of
|
2026-01-15 05:39:55 +00:00
|
|
|
LEAF (values, _) =>
|
|
|
|
|
let
|
|
|
|
|
val {start, finish} = Vector.sub (values, Vector.length values - 1)
|
|
|
|
|
in
|
|
|
|
|
{start = start + absOffset, finish = finish + absOffset}
|
|
|
|
|
end
|
|
|
|
|
| BRANCH (nodes, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val prevSize =
|
|
|
|
|
if Vector.length sizes - 2 >= 0 then
|
|
|
|
|
Vector.sub (sizes, Vector.length sizes - 2)
|
|
|
|
|
else
|
|
|
|
|
0
|
|
|
|
|
val absOffset = absOffset + prevSize
|
|
|
|
|
in
|
|
|
|
|
getLast (Vector.sub (nodes, Vector.length nodes - 1), absOffset)
|
|
|
|
|
end
|
2025-10-08 10:27:19 +01:00
|
|
|
|
2025-10-08 11:10:06 +01:00
|
|
|
(* slightly tricky.
|
|
|
|
|
* The `sizes` vector contains the last/finish position of the item
|
|
|
|
|
* at the corresponding index in the `nodes` or `values` vector
|
|
|
|
|
* However, what we when searching for the previous match
|
|
|
|
|
* is different: we want the node that has a start prior
|
|
|
|
|
* to the cursorIdx.
|
|
|
|
|
* This information cannot be retrieved with 100% accuracy
|
|
|
|
|
* using the `sizes` vector.
|
|
|
|
|
* To get what we want, we recurse downwards using the `sizes` vector.
|
|
|
|
|
* If we found the node we want, we return it.
|
|
|
|
|
* Otherwise, we return a state meaning "no node at this position"
|
|
|
|
|
* and we use the call stack to descend down the node at the previous index.
|
|
|
|
|
* There might not be a previous index because the current index is 0.
|
|
|
|
|
* In this case, either the call stack will handle it,
|
|
|
|
|
* or the caller to `helpPrevMatch` will. *)
|
2026-01-15 05:39:55 +00:00
|
|
|
fun helpPrevMatch (cursorIdx, tree, absOffset) =
|
2025-10-08 10:27:19 +01:00
|
|
|
case tree of
|
|
|
|
|
LEAF (values, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val idx = BinSearch.equalOrMore (cursorIdx, sizes)
|
|
|
|
|
in
|
2025-10-08 11:10:06 +01:00
|
|
|
if idx < 0 then
|
|
|
|
|
{start = ~1, finish = ~1}
|
|
|
|
|
else if idx = 0 then
|
|
|
|
|
let
|
2026-01-15 05:39:55 +00:00
|
|
|
val {start, finish} = Vector.sub (values, 0)
|
2025-10-08 11:10:06 +01:00
|
|
|
in
|
2026-01-15 05:39:55 +00:00
|
|
|
if start < cursorIdx then
|
|
|
|
|
{start = start + absOffset, finish = finish + absOffset}
|
|
|
|
|
else
|
|
|
|
|
{start = ~1, finish = ~1}
|
2025-10-08 11:10:06 +01:00
|
|
|
end
|
2025-10-08 10:27:19 +01:00
|
|
|
else
|
|
|
|
|
let
|
2026-01-15 05:39:55 +00:00
|
|
|
val {start, finish} = Vector.sub (values, idx)
|
2025-10-08 10:27:19 +01:00
|
|
|
in
|
2026-01-15 05:39:55 +00:00
|
|
|
if cursorIdx > start then
|
|
|
|
|
{start = start + absOffset, finish = finish + absOffset}
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {start, finish} = Vector.sub (values, idx - 1)
|
|
|
|
|
in
|
|
|
|
|
{start = start + absOffset, finish = finish + absOffset}
|
|
|
|
|
end
|
2025-10-08 10:27:19 +01:00
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
| BRANCH (nodes, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val idx = BinSearch.equalOrMore (cursorIdx, sizes)
|
|
|
|
|
in
|
2025-10-08 11:10:06 +01:00
|
|
|
if idx < 0 then
|
|
|
|
|
{start = ~1, finish = ~1}
|
|
|
|
|
else if idx = 0 then
|
2026-01-15 05:39:55 +00:00
|
|
|
helpPrevMatch (cursorIdx, Vector.sub (nodes, idx), absOffset)
|
2025-10-08 11:10:06 +01:00
|
|
|
else
|
2025-10-08 10:39:49 +01:00
|
|
|
let
|
2026-01-15 05:39:55 +00:00
|
|
|
val prevSize = Vector.sub (sizes, idx - 1)
|
2025-10-08 10:39:49 +01:00
|
|
|
val node = Vector.sub (nodes, idx)
|
2026-01-15 05:39:55 +00:00
|
|
|
val result =
|
|
|
|
|
helpPrevMatch (cursorIdx - prevSize, node, absOffset + prevSize)
|
2025-10-08 10:39:49 +01:00
|
|
|
in
|
2026-01-15 05:39:55 +00:00
|
|
|
if #start result = ~1 then
|
|
|
|
|
let
|
|
|
|
|
val prevSize =
|
|
|
|
|
if idx - 2 >= 0 then
|
|
|
|
|
Vector.sub (sizes, idx - 2)
|
|
|
|
|
else
|
|
|
|
|
0
|
|
|
|
|
val absOffset = absOffset + prevSize
|
|
|
|
|
in
|
|
|
|
|
getLast (Vector.sub (nodes, idx - 1), absOffset)
|
|
|
|
|
end
|
2025-12-12 10:30:21 +00:00
|
|
|
else result
|
2025-10-08 10:39:49 +01:00
|
|
|
end
|
2025-10-08 10:27:19 +01:00
|
|
|
end
|
|
|
|
|
|
2025-10-08 11:10:06 +01:00
|
|
|
fun loopPrevMatch (prevStart, prevFinish, tree, count) =
|
2025-10-08 10:27:19 +01:00
|
|
|
if count = 0 then
|
|
|
|
|
prevStart
|
|
|
|
|
else
|
|
|
|
|
let
|
2026-01-15 05:39:55 +00:00
|
|
|
val {start, finish} = helpPrevMatch (prevFinish - 1, tree, 0)
|
2025-10-08 10:27:19 +01:00
|
|
|
in
|
|
|
|
|
if start = ~1 then
|
2026-01-15 05:39:55 +00:00
|
|
|
let val {start, finish} = getLast (tree, 0)
|
2025-10-08 11:10:06 +01:00
|
|
|
in loopPrevMatch (start, finish, tree, count - 1)
|
2025-10-08 10:27:19 +01:00
|
|
|
end
|
|
|
|
|
else
|
2025-10-08 11:10:06 +01:00
|
|
|
loopPrevMatch (start, finish, tree, count - 1)
|
2025-10-08 10:27:19 +01:00
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun prevMatch (cursorIdx, tree, count) =
|
|
|
|
|
if isEmpty tree then
|
|
|
|
|
~1
|
|
|
|
|
else
|
|
|
|
|
let
|
2026-01-15 05:39:55 +00:00
|
|
|
val {start, finish} = helpPrevMatch (cursorIdx, tree, 0)
|
2025-10-08 10:27:19 +01:00
|
|
|
in
|
|
|
|
|
if start = ~1 then
|
2026-01-15 05:39:55 +00:00
|
|
|
let val {start, finish} = getLast (tree, 0)
|
2025-10-08 11:10:06 +01:00
|
|
|
in loopPrevMatch (start, finish, tree, count - 1)
|
2025-10-08 10:27:19 +01:00
|
|
|
end
|
|
|
|
|
else if cursorIdx >= start andalso cursorIdx <= finish then
|
2025-10-08 11:10:06 +01:00
|
|
|
loopPrevMatch (start, finish, tree, count)
|
2025-10-08 10:27:19 +01:00
|
|
|
else
|
2025-10-08 11:10:06 +01:00
|
|
|
loopPrevMatch (start, finish, tree, count - 1)
|
2025-10-08 10:27:19 +01:00
|
|
|
end
|
2026-01-15 05:51:22 +00:00
|
|
|
|
2026-01-16 21:58:59 +00:00
|
|
|
fun splitLeft (splitIdx, tree) =
|
2026-01-15 05:51:22 +00:00
|
|
|
case tree of
|
|
|
|
|
LEAF (items, sizes) =>
|
|
|
|
|
if Vector.length items = 0 then
|
|
|
|
|
(* if tree is empty, then just return tree *)
|
|
|
|
|
tree
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {start, ...} = Vector.sub (items, 0)
|
|
|
|
|
in
|
2026-01-16 21:58:59 +00:00
|
|
|
(* if all items are after splitIdx,
|
2026-01-15 05:51:22 +00:00
|
|
|
* then we want to return an empty tree,
|
|
|
|
|
* splitting everything *)
|
2026-01-16 21:58:59 +00:00
|
|
|
if splitIdx < start then
|
2026-01-15 05:51:22 +00:00
|
|
|
empty
|
2026-01-16 21:58:59 +00:00
|
|
|
else if splitIdx > Vector.sub (sizes, Vector.length sizes - 1) then
|
|
|
|
|
(* if all items are before splitIdx,
|
2026-01-15 05:51:22 +00:00
|
|
|
* then we want to return the same tree,
|
|
|
|
|
* splitting nothing *)
|
|
|
|
|
tree
|
|
|
|
|
else
|
|
|
|
|
(* we want to split from somewhere in middle, keeping left *)
|
|
|
|
|
let
|
2026-01-16 21:58:59 +00:00
|
|
|
val idx = BinSearch.equalOrMore (splitIdx, sizes)
|
2026-01-15 05:51:22 +00:00
|
|
|
val idx = SOME idx
|
|
|
|
|
|
|
|
|
|
val items = VectorSlice.slice (items, 0, idx)
|
|
|
|
|
val items = VectorSlice.vector items
|
|
|
|
|
|
|
|
|
|
val sizes = VectorSlice.slice (sizes, 0, idx)
|
|
|
|
|
val sizes = VectorSlice.vector sizes
|
|
|
|
|
in
|
|
|
|
|
LEAF (items, sizes)
|
|
|
|
|
end
|
|
|
|
|
end
|
2026-01-15 06:13:38 +00:00
|
|
|
| BRANCH (nodes, sizes) =>
|
2026-01-16 22:16:44 +00:00
|
|
|
if Vector.length nodes = 0 then
|
2026-01-15 06:13:38 +00:00
|
|
|
tree
|
2026-01-16 22:16:44 +00:00
|
|
|
else
|
|
|
|
|
if splitIdx < Vector.sub (sizes, 0) then
|
|
|
|
|
(* we want to split first node from rest *)
|
|
|
|
|
splitLeft (splitIdx, Vector.sub (nodes, 0))
|
|
|
|
|
else if splitIdx > Vector.sub (sizes, Vector.length sizes - 1) then
|
|
|
|
|
(* split point is after this subtree,
|
|
|
|
|
* so return this subtree unchanged *)
|
|
|
|
|
tree
|
|
|
|
|
else
|
|
|
|
|
(* we want to split from somewhere in middle *)
|
|
|
|
|
let
|
|
|
|
|
val idx = BinSearch.equalOrMore (splitIdx, sizes)
|
|
|
|
|
val prevSize =
|
|
|
|
|
if idx = 0 then
|
|
|
|
|
0
|
|
|
|
|
else
|
|
|
|
|
Vector.sub (sizes, idx - 1)
|
|
|
|
|
val child =
|
|
|
|
|
splitLeft (splitIdx - prevSize, Vector.sub (nodes, idx))
|
2026-01-15 06:13:38 +00:00
|
|
|
|
2026-01-16 22:16:44 +00:00
|
|
|
val sizes = VectorSlice.slice (sizes, 0, SOME idx)
|
|
|
|
|
val nodes = VectorSlice.slice (nodes, 0, SOME idx)
|
|
|
|
|
in
|
|
|
|
|
if isEmpty child then
|
|
|
|
|
let
|
|
|
|
|
val sizes = VectorSlice.vector sizes
|
|
|
|
|
val nodes = VectorSlice.vector nodes
|
|
|
|
|
in
|
|
|
|
|
BRANCH (nodes, sizes)
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val childSize = VectorSlice.full #[getFinishIdx child + prevSize]
|
|
|
|
|
val sizes =VectorSlice.concat [sizes, childSize]
|
2026-01-15 06:13:38 +00:00
|
|
|
|
2026-01-16 22:16:44 +00:00
|
|
|
val childNode = VectorSlice.full #[child]
|
|
|
|
|
val nodes = VectorSlice.concat [nodes, childNode]
|
|
|
|
|
in
|
|
|
|
|
BRANCH (nodes, sizes)
|
|
|
|
|
end
|
|
|
|
|
end
|
2026-01-15 07:16:04 +00:00
|
|
|
|
2026-01-16 21:58:59 +00:00
|
|
|
(* When we split in this function,
|
|
|
|
|
* we always want to update the sizes vector
|
|
|
|
|
* so that the relative rope-like metadata is valid *)
|
|
|
|
|
fun splitRight (splitIdx, tree) =
|
|
|
|
|
case tree of
|
|
|
|
|
BRANCH (nodes, sizes) =>
|
|
|
|
|
if splitIdx > Vector.sub (sizes, Vector.length sizes - 1) then
|
|
|
|
|
(* splitIdx is greater than largest element,
|
|
|
|
|
* so we want to remove everything;
|
|
|
|
|
* or, in other words, we want to return an empty vec *)
|
|
|
|
|
empty
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val idx = BinSearch.equalOrMore (splitIdx, sizes)
|
|
|
|
|
val prevSize =
|
|
|
|
|
if idx = 0 then
|
|
|
|
|
0
|
|
|
|
|
else
|
|
|
|
|
Vector.sub (sizes, idx - 1)
|
|
|
|
|
|
|
|
|
|
val oldChildSize = Vector.sub (sizes, idx)
|
|
|
|
|
val child = splitRight (splitIdx - prevSize, Vector.sub (nodes, idx))
|
|
|
|
|
|
|
|
|
|
val len = Vector.length nodes - (idx + 1)
|
|
|
|
|
val sizesSlice = VectorSlice.slice (sizes, idx + 1, SOME len)
|
|
|
|
|
val nodesSlice = VectorSlice.slice (nodes, idx + 1, SOME len)
|
|
|
|
|
in
|
|
|
|
|
if isEmpty child then
|
|
|
|
|
if VectorSlice.length sizesSlice = 0 then
|
|
|
|
|
(* if we descended down last node and last node became empty,
|
|
|
|
|
* then return empty vector *)
|
|
|
|
|
empty
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val nodes = VectorSlice.vector nodesSlice
|
2026-01-16 22:31:43 +00:00
|
|
|
val sizes = VectorSlice.map (fn el => el - oldChildSize) sizesSlice
|
2026-01-16 21:58:59 +00:00
|
|
|
in
|
|
|
|
|
BRANCH (nodes, sizes)
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val newChildSize = getFinishIdx child
|
|
|
|
|
val sizes = Vector.tabulate (VectorSlice.length sizesSlice + 1,
|
|
|
|
|
fn i =>
|
|
|
|
|
if i = 0 then
|
|
|
|
|
newChildSize
|
|
|
|
|
else
|
2026-01-16 22:40:38 +00:00
|
|
|
let
|
|
|
|
|
val el = VectorSlice.sub (sizesSlice, i - 1)
|
|
|
|
|
in
|
|
|
|
|
el - oldChildSize + newChildSize
|
|
|
|
|
end
|
2026-01-16 21:58:59 +00:00
|
|
|
)
|
|
|
|
|
|
|
|
|
|
val child = VectorSlice.full #[child]
|
|
|
|
|
val nodes = VectorSlice.concat [child, nodesSlice]
|
|
|
|
|
in
|
|
|
|
|
BRANCH (nodes, sizes)
|
|
|
|
|
end
|
|
|
|
|
end
|
2026-01-16 22:16:44 +00:00
|
|
|
| LEAF (items, sizes) =>
|
|
|
|
|
if Vector.length items = 0 then
|
|
|
|
|
tree
|
|
|
|
|
else
|
|
|
|
|
if splitIdx > Vector.sub (sizes, Vector.length sizes - 1) then
|
|
|
|
|
empty
|
|
|
|
|
else if splitIdx < Vector.sub (sizes, 0) then
|
|
|
|
|
tree
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val idx = BinSearch.equalOrMore (splitIdx, sizes)
|
|
|
|
|
val {start, finish} = Vector.sub (items, idx)
|
|
|
|
|
val idx =
|
|
|
|
|
if splitIdx >= start then
|
|
|
|
|
idx + 1
|
|
|
|
|
else
|
|
|
|
|
idx
|
|
|
|
|
in
|
|
|
|
|
if idx >= Vector.length items then
|
|
|
|
|
empty
|
|
|
|
|
else
|
|
|
|
|
let
|
2026-01-16 22:31:43 +00:00
|
|
|
val prevSize =
|
|
|
|
|
if idx > 0 then
|
|
|
|
|
Vector.sub (sizes, idx - 1)
|
|
|
|
|
else
|
|
|
|
|
0
|
2026-01-16 22:16:44 +00:00
|
|
|
val len = Vector.length items - idx
|
|
|
|
|
val itemsSlice = VectorSlice.slice (items, idx, SOME len)
|
|
|
|
|
val items = VectorSlice.map
|
|
|
|
|
(fn {start, finish} =>
|
2026-01-16 22:31:43 +00:00
|
|
|
{start = start - prevSize, finish = finish - prevSize}
|
2026-01-16 22:16:44 +00:00
|
|
|
)
|
|
|
|
|
itemsSlice
|
|
|
|
|
val sizes = Vector.map #finish items
|
|
|
|
|
in
|
|
|
|
|
LEAF (items, sizes)
|
|
|
|
|
end
|
|
|
|
|
end
|
2026-01-16 21:58:59 +00:00
|
|
|
|
2026-01-17 22:46:08 +00:00
|
|
|
fun decrementBy (decBy, tree) =
|
|
|
|
|
case tree of
|
|
|
|
|
BRANCH (nodes, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val child = decrementBy (decBy, Vector.sub (nodes, 0))
|
|
|
|
|
val nodes = Vector.update (nodes, 0, child)
|
|
|
|
|
val sizes = Vector.map (fn sz => sz - decBy) sizes
|
|
|
|
|
in
|
|
|
|
|
BRANCH (nodes, sizes)
|
|
|
|
|
end
|
|
|
|
|
| LEAF (items, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val items = Vector.map
|
|
|
|
|
(fn {start, finish} =>
|
|
|
|
|
{start = start - decBy, finish = finish - decBy}
|
|
|
|
|
) items
|
|
|
|
|
val sizes = Vector.map #finish items
|
|
|
|
|
in
|
|
|
|
|
LEAF (items, sizes)
|
|
|
|
|
end
|
|
|
|
|
|
2026-01-17 22:51:06 +00:00
|
|
|
fun countDepthLoop (counter, tree) =
|
|
|
|
|
case tree of
|
|
|
|
|
BRANCH (nodes, _) => countDepthLoop (counter + 1, Vector.sub (nodes, 0))
|
|
|
|
|
| LEAF (_, _) => counter + 1
|
|
|
|
|
|
|
|
|
|
fun countDepth tree = countDepthLoop (0, tree)
|
|
|
|
|
|
2026-02-05 23:54:31 +00:00
|
|
|
datatype merge_same_depth_result =
|
|
|
|
|
MERGE_SAME_DEPTH_UPDATE of t
|
|
|
|
|
| MERGE_SAME_DEPTH_FULL
|
2026-01-18 06:40:22 +00:00
|
|
|
|
|
|
|
|
fun mergeSameDepth (left, right) =
|
|
|
|
|
case (left, right) of
|
|
|
|
|
(LEAF (leftItems, leftSizes), LEAF (rightItems, rightSizes)) =>
|
|
|
|
|
if Vector.length leftItems + Vector.length rightItems <= maxSize then
|
|
|
|
|
let
|
|
|
|
|
val offset = Vector.sub (leftSizes, Vector.length leftSizes - 1)
|
|
|
|
|
val newVecLen = Vector.length leftItems + Vector.length rightItems
|
|
|
|
|
val items = Vector.tabulate (newVecLen,
|
|
|
|
|
fn i =>
|
|
|
|
|
if i < Vector.length leftItems then
|
|
|
|
|
Vector.sub (leftItems, i)
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {start, finish} =
|
|
|
|
|
Vector.sub (rightItems, i - Vector.length leftItems)
|
|
|
|
|
in
|
|
|
|
|
{start = start + offset, finish = finish + offset}
|
|
|
|
|
end
|
|
|
|
|
)
|
|
|
|
|
val sizes = Vector.map #finish items
|
|
|
|
|
in
|
2026-02-05 23:54:31 +00:00
|
|
|
MERGE_SAME_DEPTH_UPDATE (LEAF (items, sizes))
|
2026-01-18 06:40:22 +00:00
|
|
|
end
|
|
|
|
|
else
|
2026-02-05 23:54:31 +00:00
|
|
|
MERGE_SAME_DEPTH_FULL
|
2026-01-18 06:40:22 +00:00
|
|
|
| (BRANCH (leftNodes, leftSizes), BRANCH (rightNodes, rightSizes)) =>
|
|
|
|
|
if Vector.length leftNodes + Vector.length rightNodes <= maxSize then
|
|
|
|
|
let
|
|
|
|
|
val offset = Vector.sub (leftSizes, Vector.length leftSizes - 1)
|
|
|
|
|
val nodes = Vector.concat [leftNodes, rightNodes]
|
|
|
|
|
|
|
|
|
|
val sizes = Vector.tabulate (Vector.length nodes,
|
|
|
|
|
fn i =>
|
|
|
|
|
if i < Vector.length leftSizes then
|
|
|
|
|
Vector.sub (leftSizes, i)
|
|
|
|
|
else
|
|
|
|
|
Vector.sub (rightSizes, i - Vector.length leftSizes) + offset
|
|
|
|
|
)
|
|
|
|
|
in
|
2026-02-05 23:54:31 +00:00
|
|
|
MERGE_SAME_DEPTH_UPDATE (BRANCH (nodes, sizes))
|
2026-01-18 06:40:22 +00:00
|
|
|
end
|
|
|
|
|
else
|
2026-02-05 23:54:31 +00:00
|
|
|
MERGE_SAME_DEPTH_FULL
|
2026-01-18 06:40:22 +00:00
|
|
|
| _ =>
|
|
|
|
|
raise Fail "PersistentVector.mergeSameDepth: \
|
|
|
|
|
\left and right should both be BRANCH or both be LEAF \
|
|
|
|
|
\but one is BRANCH and one is LEAF"
|
|
|
|
|
|
2026-02-05 23:54:31 +00:00
|
|
|
datatype merge_diff_depth_result =
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE of t
|
|
|
|
|
| MERGE_DIFF_DEPTH_FULL
|
|
|
|
|
|
|
|
|
|
fun mergeWhenRightDepthIsGreater (left, right, targetDepth, curDepth) =
|
|
|
|
|
if curDepth = targetDepth then
|
|
|
|
|
case mergeSameDepth (left, right) of
|
|
|
|
|
MERGE_SAME_DEPTH_UPDATE tree => MERGE_DIFF_DEPTH_UPDATE tree
|
|
|
|
|
| MERGE_SAME_DEPTH_FULL => MERGE_DIFF_DEPTH_FULL
|
2026-01-18 06:52:49 +00:00
|
|
|
else
|
|
|
|
|
case right of
|
|
|
|
|
BRANCH (nodes, sizes) =>
|
2026-02-05 23:54:31 +00:00
|
|
|
(case mergeWhenRightDepthIsGreater
|
|
|
|
|
(left, Vector.sub (nodes, 0), targetDepth, curDepth + 1) of
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE child =>
|
|
|
|
|
let
|
|
|
|
|
val oldChildSize = Vector.sub (sizes, 0)
|
|
|
|
|
val newChildSize = getFinishIdx child
|
|
|
|
|
val difference = newChildSize - oldChildSize
|
2026-01-18 06:52:49 +00:00
|
|
|
|
2026-02-05 23:54:31 +00:00
|
|
|
val nodes = Vector.update (nodes, 0, child)
|
|
|
|
|
val sizes = Vector.map (fn el => el + difference) sizes
|
|
|
|
|
in
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE (BRANCH (nodes, sizes))
|
|
|
|
|
end
|
|
|
|
|
| MERGE_DIFF_DEPTH_FULL =>
|
|
|
|
|
let
|
|
|
|
|
val leftSize = getFinishIdx left
|
|
|
|
|
val sizes = Vector.tabulate (Vector.length nodes + 1,
|
|
|
|
|
fn i =>
|
|
|
|
|
if i = 0 then
|
|
|
|
|
leftSize
|
|
|
|
|
else
|
|
|
|
|
Vector.sub (sizes, i - 1) + leftSize
|
|
|
|
|
)
|
|
|
|
|
val nodes = Vector.concat [#[left], nodes]
|
|
|
|
|
in
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE (BRANCH (nodes, sizes))
|
|
|
|
|
end)
|
2026-01-18 06:52:49 +00:00
|
|
|
| LEAF _ =>
|
|
|
|
|
raise Fail "PersistentVector.mergeWhenRightDepthIsGreater: \
|
2026-02-05 23:54:31 +00:00
|
|
|
\reached LEAF before (curDepth = targetDepth)"
|
2026-01-18 06:52:49 +00:00
|
|
|
|
2026-02-05 23:54:31 +00:00
|
|
|
fun mergeWhenLeftDepthIsGreater (left, right, targetDepth, curDepth) =
|
|
|
|
|
if targetDepth = curDepth then
|
|
|
|
|
case mergeSameDepth (left, right) of
|
|
|
|
|
MERGE_SAME_DEPTH_UPDATE tree => MERGE_DIFF_DEPTH_UPDATE tree
|
|
|
|
|
| MERGE_SAME_DEPTH_FULL => MERGE_DIFF_DEPTH_FULL
|
2026-01-18 06:58:41 +00:00
|
|
|
else
|
|
|
|
|
case left of
|
|
|
|
|
BRANCH (nodes, sizes) =>
|
2026-02-05 23:54:31 +00:00
|
|
|
(case
|
|
|
|
|
mergeWhenLeftDepthIsGreater (
|
|
|
|
|
Vector.sub (nodes, Vector.length nodes - 1),
|
|
|
|
|
right,
|
|
|
|
|
targetDepth,
|
|
|
|
|
curDepth + 1) of
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE child =>
|
|
|
|
|
let
|
|
|
|
|
val lastIdx = Vector.length sizes - 1
|
|
|
|
|
val oldChildSize = Vector.sub (sizes, lastIdx)
|
|
|
|
|
val newChildSize = getFinishIdx child
|
|
|
|
|
val difference = newChildSize - oldChildSize
|
2026-01-18 06:58:41 +00:00
|
|
|
|
2026-02-05 23:54:31 +00:00
|
|
|
val nodes = Vector.update (nodes, lastIdx, child)
|
|
|
|
|
val sizes = Vector.map (fn el => el + difference) sizes
|
|
|
|
|
in
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE (BRANCH (nodes, sizes))
|
|
|
|
|
end
|
|
|
|
|
| MERGE_DIFF_DEPTH_FULL =>
|
|
|
|
|
let
|
|
|
|
|
val maxLeftSize = Vector.sub (sizes, Vector.length sizes - 1)
|
|
|
|
|
val rightSize = getFinishIdx right + maxLeftSize
|
|
|
|
|
val sizes = Vector.concat [sizes, #[rightSize]]
|
|
|
|
|
val nodes = Vector.concat [nodes, #[right]]
|
|
|
|
|
in
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE (BRANCH (nodes, sizes))
|
|
|
|
|
end)
|
2026-01-18 06:58:41 +00:00
|
|
|
| LEAF _ =>
|
|
|
|
|
raise Fail "PersistentVector.mergeWhenLeftDepthIsGreater: \
|
2026-02-05 23:54:31 +00:00
|
|
|
\reached LEAF before (curDepth = targetDepth)"
|
2026-01-18 06:58:41 +00:00
|
|
|
|
2026-01-18 06:52:49 +00:00
|
|
|
fun merge (left, right) =
|
|
|
|
|
let
|
|
|
|
|
val leftDepth = countDepth left
|
|
|
|
|
val rightDepth = countDepth right
|
|
|
|
|
in
|
|
|
|
|
if leftDepth = rightDepth then
|
2026-02-05 23:54:31 +00:00
|
|
|
case mergeSameDepth (left, right) of
|
|
|
|
|
MERGE_SAME_DEPTH_UPDATE t => t
|
|
|
|
|
| MERGE_SAME_DEPTH_FULL =>
|
|
|
|
|
let
|
|
|
|
|
val leftSize = getFinishIdx left
|
|
|
|
|
val sizes = #[leftSize, getFinishIdx right + leftSize]
|
|
|
|
|
val nodes = #[left, right]
|
|
|
|
|
in
|
|
|
|
|
BRANCH (nodes, sizes)
|
|
|
|
|
end
|
2026-01-18 06:52:49 +00:00
|
|
|
else if leftDepth < rightDepth then
|
2026-02-05 20:39:01 +00:00
|
|
|
let
|
|
|
|
|
val targetDepth = rightDepth - leftDepth
|
|
|
|
|
in
|
2026-02-05 23:54:31 +00:00
|
|
|
case mergeWhenRightDepthIsGreater
|
|
|
|
|
(left, right, targetDepth, 0) of
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE t => t
|
|
|
|
|
| MERGE_DIFF_DEPTH_FULL => empty
|
2026-02-05 20:39:01 +00:00
|
|
|
end
|
2026-01-18 06:52:49 +00:00
|
|
|
else
|
2026-02-05 20:39:01 +00:00
|
|
|
let
|
|
|
|
|
val targetDepth = leftDepth - rightDepth
|
|
|
|
|
in
|
2026-02-05 23:54:31 +00:00
|
|
|
case mergeWhenLeftDepthIsGreater
|
|
|
|
|
(left, right, targetDepth, 0) of
|
|
|
|
|
MERGE_DIFF_DEPTH_UPDATE t => t
|
|
|
|
|
| MERGE_DIFF_DEPTH_FULL => empty
|
2026-02-05 20:39:01 +00:00
|
|
|
end
|
2026-01-18 06:52:49 +00:00
|
|
|
end
|
2026-01-17 23:14:05 +00:00
|
|
|
|
2026-01-17 23:45:20 +00:00
|
|
|
fun delete (start, length, tree) =
|
2026-01-18 00:27:03 +00:00
|
|
|
if isEmpty tree then
|
|
|
|
|
empty
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val finish = start + length
|
2026-01-18 08:52:38 +00:00
|
|
|
|
2026-01-18 00:27:03 +00:00
|
|
|
val matchBeforeStart = prevMatch (start, tree, 1)
|
|
|
|
|
val matchBeforeStart =
|
|
|
|
|
if matchBeforeStart >= start then
|
|
|
|
|
~1
|
2026-01-17 23:14:05 +00:00
|
|
|
else
|
2026-01-18 00:27:03 +00:00
|
|
|
matchBeforeStart
|
2026-01-18 08:52:38 +00:00
|
|
|
|
2026-01-18 00:27:03 +00:00
|
|
|
val matchAfterFinish = nextMatch (finish, tree, 1)
|
2026-01-18 08:52:38 +00:00
|
|
|
val matchAfterFinish =
|
|
|
|
|
if matchAfterFinish < finish then
|
|
|
|
|
~1
|
|
|
|
|
else
|
|
|
|
|
matchAfterFinish
|
2026-01-18 00:27:03 +00:00
|
|
|
in
|
|
|
|
|
if matchBeforeStart = ~1 andalso matchAfterFinish = ~1 then
|
|
|
|
|
empty
|
|
|
|
|
else if matchAfterFinish = ~1 then
|
|
|
|
|
(* there is no match after 'finish', so just split left.
|
|
|
|
|
* No need to decrement or split right,
|
|
|
|
|
* because the right vector would be empty. *)
|
|
|
|
|
splitLeft (start, tree)
|
|
|
|
|
else if matchBeforeStart = ~1 then
|
|
|
|
|
(* We don't want to use left split
|
|
|
|
|
* because there are no elements
|
|
|
|
|
* before the deletion range's 'start'.
|
|
|
|
|
* So we make a right split and then decrement it. *)
|
|
|
|
|
let
|
|
|
|
|
val right = splitRight (finish, tree)
|
|
|
|
|
in
|
|
|
|
|
if isEmpty right then
|
|
|
|
|
empty
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val startIdx = getStartIdx right
|
|
|
|
|
val shouldBeStartIdx = matchAfterFinish - length
|
|
|
|
|
val difference = startIdx - shouldBeStartIdx
|
|
|
|
|
in
|
|
|
|
|
if difference = 0 then
|
|
|
|
|
right
|
|
|
|
|
else if isEmpty right then
|
|
|
|
|
empty
|
|
|
|
|
else
|
|
|
|
|
decrementBy (difference, right)
|
|
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val left = splitLeft (start, tree)
|
|
|
|
|
val right = splitRight (finish, tree)
|
|
|
|
|
in
|
|
|
|
|
if isEmpty right then
|
|
|
|
|
left
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val leftSize = getFinishIdx left
|
|
|
|
|
val rightStartRelative = getStartIdx right
|
|
|
|
|
val rightStartAbsolute = leftSize + rightStartRelative
|
2026-01-17 23:14:05 +00:00
|
|
|
|
2026-01-18 00:27:03 +00:00
|
|
|
val shouldBeStartIdx = matchAfterFinish - length
|
|
|
|
|
val difference = rightStartAbsolute - shouldBeStartIdx
|
|
|
|
|
in
|
|
|
|
|
if difference = 0 then
|
2026-01-17 23:14:05 +00:00
|
|
|
merge (left, right)
|
2026-01-18 00:27:03 +00:00
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val right = decrementBy (difference, right)
|
|
|
|
|
in
|
|
|
|
|
merge (left, right)
|
|
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
end
|
2026-01-17 23:14:05 +00:00
|
|
|
|
2026-01-18 08:52:38 +00:00
|
|
|
(* Usually, when inserting, we want the absolute metadata
|
|
|
|
|
* to be adjusted appropriately.
|
|
|
|
|
* An insertion should cause the absolute metadata to increment.
|
|
|
|
|
* However, we sometimes want to insert a match without adjusting
|
|
|
|
|
* the absolute metadata in this way.
|
|
|
|
|
* We want to do this when deleting some part of the buffer
|
|
|
|
|
* would cause a new match to be found, for example. *)
|
|
|
|
|
fun insertMatchKeepingAbsoluteInddices (start, finish, tree) =
|
|
|
|
|
let
|
|
|
|
|
val matchAfterFinish = nextMatch (finish, tree, 1)
|
|
|
|
|
in
|
|
|
|
|
if matchAfterFinish <= finish then
|
2026-02-07 00:29:58 +00:00
|
|
|
(* no match after the 'finish', so we can just append to 'tree' *)
|
2026-01-18 08:52:38 +00:00
|
|
|
append (start, finish, tree)
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val left = splitLeft (start, tree)
|
|
|
|
|
val right = splitRight (finish, tree)
|
|
|
|
|
|
2026-02-06 08:57:18 +00:00
|
|
|
val left = append (start, finish, left)
|
2026-01-18 08:52:38 +00:00
|
|
|
|
|
|
|
|
val rightStartRelative = getStartIdx right
|
|
|
|
|
val rightStartAbsolute = rightStartRelative + finish
|
|
|
|
|
val difference = rightStartAbsolute - matchAfterFinish
|
|
|
|
|
val right = decrementBy (difference, right)
|
|
|
|
|
in
|
|
|
|
|
merge (left, right)
|
|
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
|
2026-02-07 00:29:58 +00:00
|
|
|
fun extendExistingMatch (start, newFinish, tree) =
|
|
|
|
|
let
|
|
|
|
|
val matchAfterFinish = nextMatch (newFinish, tree, 1)
|
|
|
|
|
val left = splitLeft (start, tree)
|
|
|
|
|
val left = append (start, newFinish, left)
|
|
|
|
|
in
|
|
|
|
|
if matchAfterFinish <= newFinish then
|
|
|
|
|
(* no match after newFinish, so we can return 'left'
|
|
|
|
|
* which has the newFinish appended *)
|
|
|
|
|
left
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val right = splitRight (newFinish, tree)
|
|
|
|
|
|
|
|
|
|
val leftFinish = getFinishIdx left
|
|
|
|
|
val rightStartRelative = getStartIdx right
|
|
|
|
|
|
|
|
|
|
val rightStartAbsolute = rightStartRelative + leftFinish
|
|
|
|
|
val difference = rightStartAbsolute - matchAfterFinish
|
|
|
|
|
val right = decrementBy (difference, right)
|
|
|
|
|
in
|
|
|
|
|
merge (left, right)
|
|
|
|
|
end
|
|
|
|
|
end
|
|
|
|
|
|
2026-01-15 07:16:04 +00:00
|
|
|
(* functions only for testing *)
|
2026-02-05 23:54:31 +00:00
|
|
|
fun childrenHaveSameDepth (pos, nodes, expectedDepth) =
|
|
|
|
|
if pos = Vector.length nodes then
|
|
|
|
|
true
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val node = Vector.sub (nodes, pos)
|
|
|
|
|
in
|
|
|
|
|
if allLeavesAtSameDepth node then
|
|
|
|
|
let
|
|
|
|
|
val nodeDepth = countDepth node
|
|
|
|
|
in
|
|
|
|
|
if nodeDepth = expectedDepth then
|
|
|
|
|
childrenHaveSameDepth (pos + 1, nodes, expectedDepth)
|
2026-02-05 20:39:01 +00:00
|
|
|
else
|
2026-02-05 23:54:31 +00:00
|
|
|
false
|
|
|
|
|
end
|
|
|
|
|
else
|
|
|
|
|
false
|
|
|
|
|
end
|
2026-02-05 20:39:01 +00:00
|
|
|
|
2026-02-05 23:54:31 +00:00
|
|
|
and allLeavesAtSameDepth tree =
|
|
|
|
|
case tree of
|
|
|
|
|
BRANCH (nodes, _) =>
|
|
|
|
|
let
|
2026-02-05 20:39:01 +00:00
|
|
|
val expectedDepth = countDepth (Vector.sub (nodes, 0))
|
|
|
|
|
in
|
2026-02-05 23:54:31 +00:00
|
|
|
childrenHaveSameDepth (0, nodes, expectedDepth)
|
2026-02-05 20:39:01 +00:00
|
|
|
end
|
|
|
|
|
| LEAF _ => true
|
|
|
|
|
|
2026-01-15 07:16:04 +00:00
|
|
|
fun fromListLoop (lst, acc) =
|
|
|
|
|
case lst of
|
|
|
|
|
{start, finish} :: tl =>
|
|
|
|
|
let
|
|
|
|
|
val acc = append (start, finish, acc)
|
|
|
|
|
in
|
|
|
|
|
fromListLoop (tl, acc)
|
|
|
|
|
end
|
|
|
|
|
| [] => acc
|
|
|
|
|
|
|
|
|
|
fun fromList coords = fromListLoop (coords, empty)
|
|
|
|
|
|
|
|
|
|
fun toListLoop (tree, acc) =
|
|
|
|
|
case tree of
|
|
|
|
|
BRANCH (nodes, _) =>
|
|
|
|
|
let
|
|
|
|
|
fun branchLoop (pos, acc) =
|
|
|
|
|
if pos = Vector.length nodes then
|
|
|
|
|
acc
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val acc = toListLoop (Vector.sub (nodes, pos), acc)
|
|
|
|
|
in
|
|
|
|
|
branchLoop (pos + 1, acc)
|
|
|
|
|
end
|
|
|
|
|
in
|
|
|
|
|
branchLoop (0, acc)
|
|
|
|
|
end
|
|
|
|
|
| LEAF (items, _) =>
|
|
|
|
|
let
|
|
|
|
|
fun itemLoop (pos, acc, offset) =
|
|
|
|
|
if pos = Vector.length items then
|
|
|
|
|
acc
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {start, finish} = Vector.sub (items, pos)
|
|
|
|
|
val item = {start = start + offset, finish = finish + offset}
|
|
|
|
|
in
|
|
|
|
|
itemLoop (pos + 1, item :: acc, offset)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
val offset =
|
|
|
|
|
case acc of
|
|
|
|
|
{finish, ...} :: _ => finish
|
|
|
|
|
| [] => 0
|
|
|
|
|
in
|
|
|
|
|
itemLoop (0, acc, offset)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
fun toList tree =
|
|
|
|
|
let
|
|
|
|
|
val result = toListLoop (tree, [])
|
|
|
|
|
in
|
|
|
|
|
List.rev result
|
|
|
|
|
end
|
2025-08-30 23:05:11 +01:00
|
|
|
end
|