File size: 9,745 Bytes
ffc07fb | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 | ! Layer 3 — Sovereign IDE Text Buffer (Rope + Undo Tree)
! O(log n) insert/delete, persistent undo tree
! Maps to: errant QTT tags, sovereign-array Lean 4 proofs
MODULE sovereign_text_buffer
USE iso_c_binding
USE sovereign_runtime, ONLY: runtime_panic, arena_alloc
IMPLICIT NONE
PRIVATE
! ── Rope node kinds ────────────────────────────────────────────────────────
INTEGER, PARAMETER :: NODE_LEAF = 0
INTEGER, PARAMETER :: NODE_BRANCH = 1
INTEGER, PARAMETER :: MAX_NODES = 1048576 ! 1M nodes per buffer
INTEGER, PARAMETER :: LEAF_MAX = 1024 ! max chars in a leaf
! ── Rope node ─────────────────────────────────────────────────────────────
! QTT tag from errant: provenance token for LSP change tracking
TYPE :: rope_node_t
INTEGER :: kind = NODE_LEAF
INTEGER :: length = 0
INTEGER :: lines = 0 ! newline count in subtree
INTEGER :: left = 0 ! index into node pool (0 = nil)
INTEGER :: right = 0
INTEGER :: qtt_tag = 0 ! errant provenance tag
CHARACTER(LEN=LEAF_MAX) :: text = '' ! only valid for LEAF
END TYPE rope_node_t
! ── Undo tree node ────────────────────────────────────────────────────────
INTEGER, PARAMETER :: MAX_UNDO = 65536
TYPE :: undo_node_t
INTEGER :: parent = 0 ! 0 = root
INTEGER :: rope_root = 0 ! index of rope root at this snapshot
INTEGER :: timestamp = 0
INTEGER :: cursor_pos = 0
END TYPE undo_node_t
! ── Buffer state ──────────────────────────────────────────────────────────
TYPE :: text_buffer_t
TYPE(rope_node_t) :: nodes(MAX_NODES)
INTEGER :: node_count = 0
INTEGER :: root = 0
TYPE(undo_node_t) :: undo(MAX_UNDO)
INTEGER :: undo_count = 0
INTEGER :: undo_head = 0
END TYPE text_buffer_t
PUBLIC :: buffer_init
PUBLIC :: buffer_insert
PUBLIC :: buffer_delete
PUBLIC :: buffer_slice
PUBLIC :: buffer_length
PUBLIC :: buffer_line_count
PUBLIC :: buffer_offset_to_line_col
PUBLIC :: buffer_undo
PUBLIC :: buffer_redo
CONTAINS
! ---------------------------------------------------------------------------
SUBROUTINE buffer_init(buf, initial_text)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
CHARACTER(LEN=*), INTENT(IN), OPTIONAL :: initial_text
buf%node_count = 0
buf%undo_count = 0
buf%undo_head = 0
IF (PRESENT(initial_text)) THEN
buf%root = make_leaf(buf, initial_text)
ELSE
buf%root = make_leaf(buf, '')
END IF
END SUBROUTINE buffer_init
! ---------------------------------------------------------------------------
! Insert text at byte offset; O(log n)
SUBROUTINE buffer_insert(buf, offset, text)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
INTEGER, INTENT(IN) :: offset
CHARACTER(LEN=*), INTENT(IN) :: text
INTEGER :: left_root, right_root, text_node
! Split at offset, concat with new leaf, concat remainder
CALL rope_split(buf, buf%root, offset, left_root, right_root)
text_node = make_leaf(buf, text)
buf%root = rope_concat(buf, rope_concat(buf, left_root, text_node), right_root)
CALL push_undo(buf, offset + LEN_TRIM(text))
END SUBROUTINE buffer_insert
! ---------------------------------------------------------------------------
! Delete [offset, offset+length); O(log n)
SUBROUTINE buffer_delete(buf, offset, length)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
INTEGER, INTENT(IN) :: offset, length
INTEGER :: l, m, r
CALL rope_split(buf, buf%root, offset, l, m)
CALL rope_split(buf, m, length, m, r)
buf%root = rope_concat(buf, l, r) ! discard m (deleted region)
CALL push_undo(buf, offset)
END SUBROUTINE buffer_delete
! ---------------------------------------------------------------------------
FUNCTION buffer_length(buf) RESULT(n)
TYPE(text_buffer_t), INTENT(IN) :: buf
INTEGER :: n
IF (buf%root == 0) THEN; n = 0; RETURN; END IF
n = buf%nodes(buf%root)%length
END FUNCTION buffer_length
! ---------------------------------------------------------------------------
FUNCTION buffer_line_count(buf) RESULT(n)
TYPE(text_buffer_t), INTENT(IN) :: buf
INTEGER :: n
IF (buf%root == 0) THEN; n = 1; RETURN; END IF
n = buf%nodes(buf%root)%lines + 1
END FUNCTION buffer_line_count
! ---------------------------------------------------------------------------
SUBROUTINE buffer_slice(buf, offset, length, out_text)
TYPE(text_buffer_t), INTENT(IN) :: buf
INTEGER, INTENT(IN) :: offset, length
CHARACTER(LEN=*), INTENT(OUT) :: out_text
out_text = ''
! TODO: rope traversal collecting chars in [offset, offset+length)
END SUBROUTINE buffer_slice
! ---------------------------------------------------------------------------
SUBROUTINE buffer_offset_to_line_col(buf, offset, line, col)
TYPE(text_buffer_t), INTENT(IN) :: buf
INTEGER, INTENT(IN) :: offset
INTEGER, INTENT(OUT) :: line, col
line = 1; col = 1
! TODO: O(log n) line index traversal
END SUBROUTINE buffer_offset_to_line_col
! ---------------------------------------------------------------------------
SUBROUTINE buffer_undo(buf)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
IF (buf%undo_head <= 1) RETURN
buf%undo_head = buf%undo_head - 1
buf%root = buf%undo(buf%undo_head)%rope_root
END SUBROUTINE buffer_undo
SUBROUTINE buffer_redo(buf)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
IF (buf%undo_head >= buf%undo_count) RETURN
buf%undo_head = buf%undo_head + 1
buf%root = buf%undo(buf%undo_head)%rope_root
END SUBROUTINE buffer_redo
! ── Internal helpers ──────────────────────────────────────────────────────
FUNCTION make_leaf(buf, text) RESULT(idx)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
CHARACTER(LEN=*), INTENT(IN) :: text
INTEGER :: idx
IF (buf%node_count >= MAX_NODES) &
CALL runtime_panic('text_buffer: node pool exhausted')
buf%node_count = buf%node_count + 1
idx = buf%node_count
buf%nodes(idx)%kind = NODE_LEAF
buf%nodes(idx)%text = text(1:MIN(LEN_TRIM(text), LEAF_MAX))
buf%nodes(idx)%length = LEN_TRIM(text)
buf%nodes(idx)%lines = COUNT_NEWLINES(text)
END FUNCTION make_leaf
FUNCTION rope_concat(buf, l, r) RESULT(idx)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
INTEGER, INTENT(IN) :: l, r
INTEGER :: idx
IF (l == 0) THEN; idx = r; RETURN; END IF
IF (r == 0) THEN; idx = l; RETURN; END IF
buf%node_count = buf%node_count + 1
idx = buf%node_count
buf%nodes(idx)%kind = NODE_BRANCH
buf%nodes(idx)%left = l
buf%nodes(idx)%right = r
buf%nodes(idx)%length = buf%nodes(l)%length + buf%nodes(r)%length
buf%nodes(idx)%lines = buf%nodes(l)%lines + buf%nodes(r)%lines
END FUNCTION rope_concat
RECURSIVE SUBROUTINE rope_split(buf, root, offset, left_out, right_out)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
INTEGER, INTENT(IN) :: root, offset
INTEGER, INTENT(OUT) :: left_out, right_out
INTEGER :: left_len, ll, lr, rl, rr
IF (root == 0 .OR. offset <= 0) THEN
left_out = 0; right_out = root; RETURN
END IF
IF (offset >= buf%nodes(root)%length) THEN
left_out = root; right_out = 0; RETURN
END IF
IF (buf%nodes(root)%kind == NODE_LEAF) THEN
! Split the leaf text
left_out = make_leaf(buf, buf%nodes(root)%text(1:offset))
right_out = make_leaf(buf, buf%nodes(root)%text(offset+1:buf%nodes(root)%length))
RETURN
END IF
left_len = buf%nodes(buf%nodes(root)%left)%length
IF (offset <= left_len) THEN
CALL rope_split(buf, buf%nodes(root)%left, offset, ll, lr)
left_out = ll
right_out = rope_concat(buf, lr, buf%nodes(root)%right)
ELSE
CALL rope_split(buf, buf%nodes(root)%right, offset - left_len, rl, rr)
left_out = rope_concat(buf, buf%nodes(root)%left, rl)
right_out = rr
END IF
END SUBROUTINE rope_split
SUBROUTINE push_undo(buf, cursor_pos)
TYPE(text_buffer_t), INTENT(INOUT) :: buf
INTEGER, INTENT(IN) :: cursor_pos
IF (buf%undo_count >= MAX_UNDO) RETURN ! TODO: compact old history
buf%undo_count = buf%undo_count + 1
buf%undo_head = buf%undo_count
buf%undo(buf%undo_count)%rope_root = buf%root
buf%undo(buf%undo_count)%cursor_pos = cursor_pos
buf%undo(buf%undo_count)%timestamp = buf%undo_count
END SUBROUTINE push_undo
PURE FUNCTION COUNT_NEWLINES(s) RESULT(n)
CHARACTER(LEN=*), INTENT(IN) :: s
INTEGER :: n, i
n = 0
DO i = 1, LEN_TRIM(s)
IF (s(i:i) == CHAR(10)) n = n + 1
END DO
END FUNCTION COUNT_NEWLINES
END MODULE sovereign_text_buffer
|