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-09-29 14:49:50 +01:00
|
|
|
fun isEmpty t =
|
|
|
|
|
case t of
|
|
|
|
|
LEAF (_, sizes) = Vector.length sizes = 0
|
|
|
|
|
| _ => false
|
|
|
|
|
|
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
|
|
|
|
|
else
|
|
|
|
|
isInRange (checkIdx, Vector.sub (nodes, searchIdx))
|
|
|
|
|
end
|
|
|
|
|
| LEAF (values, sizes) =>
|
|
|
|
|
let
|
|
|
|
|
val searchIdx = BinSearch.equalOrMore (checkIdx, sizes)
|
|
|
|
|
in
|
|
|
|
|
if searchIdx = ~1 then
|
|
|
|
|
false
|
|
|
|
|
else
|
|
|
|
|
let
|
|
|
|
|
val {start, finish} = Vector.sub (values, searchIdx)
|
|
|
|
|
in
|
|
|
|
|
checkIdx >= start andalso checkIdx <= finish
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
in
|
2025-09-29 14:02:07 +01:00
|
|
|
case helpAppend (start, finish, 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 =>
|
|
|
|
|
if Vector.length nodes + 1 > maxSize then
|
2025-09-29 14:02:07 +01:00
|
|
|
let val newNode = BRANCH (#[newVec], #[finish])
|
2025-08-30 23:05:11 +01:00
|
|
|
in APPEND newNode
|
|
|
|
|
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
|
|
|
|
|
let val newNode = LEAF (#[{start = start, finish = finish}], #[finish])
|
2025-08-30 23:05:11 +01:00
|
|
|
in APPEND newNode
|
|
|
|
|
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) =
|
|
|
|
|
case helpAppend (start, finish, tree) of
|
|
|
|
|
UPDATE t => t
|
2025-09-29 14:29:43 +01:00
|
|
|
| APPEND newNode =>
|
|
|
|
|
let
|
|
|
|
|
val maxSize = getFinishIdx tree
|
|
|
|
|
in
|
|
|
|
|
BRANCH (#[tree, newNode], #[maxSize, finish])
|
|
|
|
|
end
|
2025-08-30 23:05:11 +01:00
|
|
|
end
|