/* Exact, nonmodal declaration inspection shared by paper and review companions. */
(async () => {
  "use strict";
  const payload = document.getElementById("companion-inventory-data");
  if (!payload) return;
  const inventory = document.getElementById("human-review-inventory");
  inventory.setAttribute("aria-busy", "true");
  const encoding = payload.dataset.encoding || "json";
  let serialized = payload.textContent;
  if (encoding === "gzip-base64") {
    if (typeof DecompressionStream === "undefined") {
      throw new Error("This browser cannot decompress the declaration details. Use a browser supporting DecompressionStream; the complete main-text inventory remains available.");
    }
    if (serialized.length % 4 !== 0 || !/^[A-Za-z0-9+/]*={0,2}$/.test(serialized)) {
      throw new Error("Invalid base64 companion inventory.");
    }
    const bytes = Uint8Array.from(atob(serialized), character => character.charCodeAt(0));
    const stream = new Blob([bytes]).stream().pipeThrough(new DecompressionStream("gzip"));
    serialized = new TextDecoder("utf-8", { fatal: true }).decode(await new Response(stream).arrayBuffer());
  } else if (encoding !== "json") throw new Error("Unsupported companion inventory encoding.");
  const data = JSON.parse(serialized);
  if (data.schemaVersion !== 1) throw new Error("Unsupported companion inventory schema.");
  const project = new Map(data.nodes.map(node => [node.name, node]));
  const external = new Map(data.externalNodes.map(node => [node.name, node]));
  if (project.size !== data.nodes.length || external.size !== data.externalNodes.length ||
      [...project.keys()].some(name => external.has(name))) {
    throw new Error("Duplicate companion inventory declarations.");
  }
  const panel = document.getElementById("companion-details-panel");
  const content = document.getElementById("companion-details-content");
  const title = document.getElementById("companion-details-title");
  const close = document.getElementById("companion-details-close");
  const explicit = document.getElementById("companion-details-explicit");
  let selected = null, opener = null;
  const make = (tag, value, className) => {
    const element = document.createElement(tag);
    if (value !== undefined) element.textContent = value;
    if (className) element.className = className;
    return element;
  };
  const read = (object, field) => object[
    explicit.checked ? "explicit" + field[0].toUpperCase() + field.slice(1) : field
  ] ?? object[field] ?? "";
  const pre = value => make("pre", value, "companion-exact-expression");
  const block = (parent, heading, value) => {
    const section = make("section", undefined, "companion-specification-block");
    section.append(make("h3", heading), pre(value)); parent.append(section); return section;
  };
  const kind = node => node.kind === "axiom" ? "axiom / trust boundary" :
    node.isClass ? "class" : node.isStructure ? "structure" :
    node.isInstance ? "instance" : node.proofValued || node.kind === "theorem" ? "checked statement" : node.kind;
  const nativeCompilerAxiom = node => node.kind === "axiom" &&
    /\._native\.native_decide\.ax_\d+(?:_\d+)*$/.test(node.name) &&
    ((node.sourceRole === "source-map" && /\.SourceMap$/.test(node.module || "")) ||
     (node.sourceRole === "coverage-interpretation" && /\.Coverage$/.test(node.module || "")));
  function declarationLink(name, label) {
    const button = make("button", label || name, "companion-dependency-link");
    button.type = "button";
    button.dataset.companionTarget = name;
    if (project.has(name) || external.has(name)) {
      button.dataset.companionBoundary = String(external.has(name));
      button.addEventListener("click", () => inspect(name));
    } else {
      // A missing dependency must remain visible, never masquerade as complete.
      button.disabled = true;
      button.title = "This declaration has no extracted specification in the inventory.";
      button.append(make("span", " — specification unavailable"));
    }
    return button;
  }
  function references(parent, names, heading = "Meaning dependencies") {
    if (!names?.length) return;
    const section = make("section", undefined, "companion-specification-block");
    section.append(make("h3", heading));
    const list = make("ul", undefined, "companion-dependency-list");
    for (const name of names) {
      const item = make("li"); item.append(declarationLink(name)); list.append(item);
    }
    section.append(list); parent.append(section);
  }
  function binders(parent, entries, heading) {
    const section = make("section", undefined, "companion-specification-block");
    section.append(make("h3", heading));
    const list = make("ol", undefined, "companion-binder-list");
    for (const [index, entry] of entries.entries()) {
      const item = make("li");
      const role = entry.defined ? "local definition" : entry.hypothesis || entry.propositionValued ?
        "hypothesis" : "parameter";
      item.dataset.companionBinder = String(index);
      item.append(make("h4", entry.name || "Unnamed binder " + (index + 1)),
        make("p", (entry.binding || "explicit") + " " + role, "companion-specification-meta"),
        pre(read(entry, "type")));
      if (entry.value !== undefined) block(item, "Local value", read(entry, "value"));
      references(item, entry.references?.declarations, "Declarations in this binder");
      list.append(item);
    }
    if (!entries.length) section.append(make("p", "No parameters or hypotheses in this telescope."));
    else section.append(list);
    parent.append(section);
  }
  function telescope(parent, statement, heading) {
    binders(parent, statement.binders || [], heading);
    block(parent, "Conclusion under these binders", read(statement, "conclusion"));
  }
  function documentation(node) {
    const text = node.documentation || node.docString;
    if (text) content.append(make("p", text, "companion-specification-documentation"));
  }
  function structureSpecification(node) {
    if (node.parents?.length) {
      const section = make("section", undefined, "companion-specification-block");
      section.append(make("h3", "Every direct parent, in inheritance order"));
      for (const [index, parent] of node.parents.entries()) {
        const item = make("div", undefined, "companion-field-entry");
        item.append(make("h4", "Parent " + (index + 1)),
          make("p", parent.embedded ? "Embedded subobject" : "Reconstructed from shared fields",
            "companion-specification-meta"), declarationLink(parent.structure), declarationLink(parent.projection),
          pre(read(parent, "type")));
        section.append(item);
      }
      content.append(section);
    }
    if (node.fields?.length) {
      const section = make("section", undefined, "companion-specification-block");
      section.append(make("h3", "All stored fields and restrictions, in constructor order"));
      for (const [index, field] of node.fields.entries()) {
        const item = make("div", undefined, "companion-field-entry");
        item.dataset.companionField = field.name;
        item.append(make("h4", "Field " + (index + 1)), declarationLink(field.name),
          make("p", (field.binding || "explicit") +
            (field.context?.hypothesis ? " proposition-valued restriction" : " data or predicate field") +
            (field.subobject ? " · inherited subobject " + field.subobject : ""), "companion-specification-meta"));
        if (field.context) block(item, "Type under the preceding constructor binders", read(field.context, "type"));
        block(item, "Full public projection type", read(field, "type"));
        section.append(item);
      }
      content.append(section);
    }
  }
  function render(name) {
    const boundary = external.has(name), node = project.get(name) || external.get(name);
    if (!node) throw new Error("Missing companion declaration: " + name);
    const axiom = node.kind === "axiom", snippet = node.sourceSnippet;
    title.textContent = node.name;
    panel.dataset.companionSelected = name;
    panel.dataset.companionBoundary = String(boundary);
    content.replaceChildren();
    content.append(make("p", (boundary ? "External " : "Project ") + (kind(node) || "declaration") +
      (axiom ? " · no Lean proof body" : "") +
      (nativeCompilerAxiom(node) ? " · native_decide compiler trust" : ""),
    "companion-specification-meta companion-primary-meta"));
    if (snippet) {
      const section = block(content, snippet.label || "Lean declaration source", snippet.code);
      section.classList.add("companion-source-code");
      section.querySelector("pre").classList.add("companion-source-snippet");
      section.append(make("p", snippet.path + ":" + snippet.startLine + "–" + snippet.endLine,
        "companion-specification-meta companion-source-location"));
    }
    block(content, "Exact elaborated type", read(node, "type"));
    if (boundary) { documentation(node); return; }
    if (node.body !== undefined && !node.proofValued && !axiom) {
      block(content, data.definitionProofTermsElided ?
        "Definition body (proof terms omitted)" : "Definition body", read(node, "body"));
    }
    structureSpecification(node);
    if (node.statement) telescope(content, node.statement, "All statement parameters and hypotheses");
    if (node.localStatementContext) {
      binders(content, node.localStatementContext.entries || [], "Full local context, including local definitions");
      block(content, "Conclusion in the full local context", read(node.localStatementContext, "conclusion"));
    }
    if (node.constructorTelescope) {
      if (node.constructorInductive) references(content, [node.constructorInductive], "Constructed inductive type");
      telescope(content, node.constructorTelescope, "Complete constructor parameters and fields");
    }
    if (node.structureContext) {
      const context = node.structureContext;
      binders(content, context.parameters || [], "Structure parameters in constructor order");
      if (context.constructor) references(content, [context.constructor], "Constructor");
      block(content, "Constructed structure", read(context, "result"));
    }
    for (const rule of node.recursorRules || []) {
      const section = block(content, "Recursor rule", read(rule, "rhs"));
      section.insertBefore(declarationLink(rule.constructor), section.lastChild);
    }
    if (node.appliedPredicates?.entries?.length) {
      const section = make("section", undefined, "companion-specification-block");
      section.append(make("h3", "One-step predicate characterizations"));
      for (const entry of node.appliedPredicates.entries) {
        const item = block(section, "Statement part " + entry.part, read(entry, "expression"));
        item.insertBefore(declarationLink(entry.definition), item.lastChild);
      }
      content.append(section);
    }
    references(content, node.dependencies, "All direct meaning dependencies");
    documentation(node);
  }
  function inspect(name, trigger) {
    if (trigger) {
      opener?.setAttribute("aria-expanded", "false");
      opener = trigger; opener.setAttribute("aria-expanded", "true");
    }
    selected = name;
    render(name);
    panel.hidden = false;
    document.body.classList.add("companion-panel-open");
    content.scrollTop = 0;
    close.focus({ preventScroll: true });
  }
  function dismiss() {
    if (panel.hidden) return;
    panel.hidden = true;
    document.body.classList.remove("companion-panel-open");
    opener?.setAttribute("aria-expanded", "false");
    opener?.focus({ preventScroll: true });
  }
  document.getElementById("human-review-inventory").addEventListener("click", event => {
    const trigger = event.target.closest("button[data-companion-declaration]");
    if (trigger) inspect(trigger.dataset.companionDeclaration, trigger);
  });
  close.addEventListener("click", dismiss);
  document.addEventListener("keydown", event => {
    if (event.key === "Escape" && !panel.hidden) { event.preventDefault(); dismiss(); }
  });
  explicit.addEventListener("change", () => { if (selected) render(selected); });
  if (typeof ResizeObserver !== "undefined") new ResizeObserver(() => {
    if (!panel.hidden) document.documentElement.style.setProperty("--companion-panel-height", panel.offsetHeight + "px");
  }).observe(panel);
  // Consumers wait for the ready flag; compression changes transport only.
  globalThis.PhysicsLogicCompanionInventory = Object.freeze({ data });
  inventory.removeAttribute("aria-busy");
  document.documentElement.dataset.companionInventoryReady = "true";
})().catch(error => {
  const inventory = document.getElementById("human-review-inventory");
  if (inventory) {
    inventory.removeAttribute("aria-busy");
    const notice = document.createElement("p");
    notice.className = "companion-inventory-status";
    notice.setAttribute("role", "alert");
    notice.textContent = "Declaration details could not be opened. " + error.message;
    inventory.append(notice);
  }
  console.error(error);
});