layer-3-text-buffer/text_buffer.f90

! 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