import type { Message } from "@slackwsh/contracts";

/**
 * Spec-level helpers for §5.2. The harness and the TLA+ model both treat
 * these formulas as the source of truth — not whatever a particular SQL
 * query or UI cache happens to compute today.
 *
 * Machine-checked by:
 *   - `invariants.test.ts` / `properties.test.ts` (fast-check)
 *   - `harness.seed.test.ts` (seeded fault injection)
 *   - `spec/Sync.tla` (I4 / I5 / I5b / I7)
 */

export interface PersistedMention {
  messageId: number;
  /** `user` | `here` | `channel` | `everyone` | `group` */
  targetType: string;
  targetId: number | null;
}

export function isChannelViewMessage(message: Message): boolean {
  return message.parentId == null || message.isBroadcast;
}

export function channelView(messages: readonly Message[]): Message[] {
  return messages.filter(isChannelViewMessage).slice().sort((a, b) => a.seq - b.seq);
}

/** I1: identical seq order, ignoring delivery/wall-clock. */
export function seqOrder(messages: readonly Message[]): number[] {
  return messages.map((m) => m.seq);
}

export function assertTotalOrder(messages: readonly Message[]): void {
  const seqs = seqOrder(messages);
  for (let i = 1; i < seqs.length; i++) {
    if (seqs[i]! < seqs[i - 1]!) {
      throw new Error(`I1 violated: seq order ${seqs.join(",")}`);
    }
  }
}

/**
 * I4. Acks use GREATEST; mark-unread is the explicit-decrease exception
 * and uses LEAST. Both are monotonic in their own direction.
 */
export function clampReadSeq(current: number, incoming: number, explicitDecrease: boolean): number {
  return explicitDecrease ? Math.min(current, incoming) : Math.max(current, incoming);
}

/** I5. */
export function channelUnreadCount(
  messages: readonly Message[],
  lastReadSeq: number,
  selfId: number,
): number {
  return messages.filter(
    (m) =>
      m.seq > lastReadSeq &&
      Number(m.authorId) !== selfId &&
      m.deletedAt == null &&
      isChannelViewMessage(m),
  ).length;
}

/** I5b. */
export function threadUnreadCount(
  messages: readonly Message[],
  rootId: number,
  lastReadReplySeq: number,
  selfId: number,
): number {
  return messages.filter(
    (m) =>
      Number(m.parentId) === rootId &&
      m.seq > lastReadReplySeq &&
      Number(m.authorId) !== selfId &&
      m.deletedAt == null,
  ).length;
}

/**
 * I6. Mention badges are counted from persisted `message_mentions` rows,
 * never from re-parsing `message.text`. Broad mentions (`here`/`channel`/
 * `everyone`) target every channel member except the author.
 */
export function mentionBadgeFromRows(
  messages: readonly Message[],
  mentions: readonly PersistedMention[],
  selfId: number,
  lastReadSeq: number,
  memberIds: readonly number[],
): number {
  const byId = new Map(messages.map((m) => [Number(m.id), m]));
  const counted = new Set<number>();
  for (const row of mentions) {
    const message = byId.get(row.messageId);
    if (!message || message.deletedAt != null) continue;
    if (message.seq <= lastReadSeq) continue;
    if (Number(message.authorId) === selfId) continue;
    let hitsSelf = false;
    if (row.targetType === "user") hitsSelf = row.targetId === selfId;
    else if (row.targetType === "here" || row.targetType === "channel" || row.targetType === "everyone") {
      hitsSelf = memberIds.includes(selfId);
    }
    if (hitsSelf) counted.add(row.messageId);
  }
  return counted.size;
}

/** I8: a lower-or-equal revision must not replace a higher one. */
export function shouldApplyRevision(existingRevision: number, incomingRevision: number): boolean {
  return incomingRevision >= existingRevision;
}

export function reactionsConverged(
  a: ReadonlyArray<{ emoji: string; count: number }> | undefined,
  b: ReadonlyArray<{ emoji: string; count: number }> | undefined,
): boolean {
  const norm = (rows: ReadonlyArray<{ emoji: string; count: number }> | undefined) =>
    [...(rows ?? [])]
      .filter((r) => r.count > 0)
      .sort((x, y) => x.emoji.localeCompare(y.emoji))
      .map((r) => `${r.emoji}:${r.count}`)
      .join(",");
  return norm(a) === norm(b);
}