Crate nibli_render 

Shared human-readable rendering for Nibli.

ONE place that turns the engine’s internal representations into English for the two surfaces humans read to verify the engine:

• render_logic_buffer — the Transparency Triad back-translation: compiles a LogicBuffer (the FOL IR) into structure-exposing English.
• humanize_fact / render_proof / render_proof_text — readable proof traces, sharing the same fact humanizer and term rendering.

Rendering is pure: it reads LogicBuffer/ProofTrace and never mutates a verdict or a proof’s tree shape. Unknown predicates fall back to a generic relation(args) / gloss-based frame — never invented English.

Structs

DomainGloss

A domain-term overlay for one curated example. The tables are tiny (a handful of entries each), so a linear scan is fine.

RenderedNode

A rendered proof node: everything the text and component renderers need, computed once. Children are rendered recursively.

Enums

Register

Controls how structure-exposing the rendered English is.

Statics

DRUG_INTERACTIONS_OVERLAY

Drug-interaction case study (drug-interactions.nibli, book Ch 20).

GDPR_OVERLAY

GDPR compliance case study (gdpr.nibli, book Ch 19).

UTOPIA_OVERLAY

Utopia constitutional provocation (utopia.nibli).

Functions

collapse_proof

Collapse a verbose proof trace into a macro-logical DAG (a RenderedNode tree). Render-only; the trace is unchanged.

collapse_proof_with

As collapse_proof, rendering under a domain-gloss overlay (None = the dictionary-fallback default).

css_class

CSS class for color-coding in the UI proof tree.

fact_to_english

Translate one humanized/raw fact string to an English clause via the place frames. None when it cannot be rendered (caller falls back to functional).

humanize_fact

Humanize a single flat fact-display string into readable notation.

icon

Unicode icon for a proof rule type.

label

Human-readable label describing the proof step (UI component form).

render_collapsed_text

The collapsed macro-logical-DAG proof of a whole trace as indented text (the REPL / server / book view): the closed-world NAF caveat (when the verdict rests on it), then the collapsed tree. With include_detail = false the role-level clusters are omitted (the clean macro view). One call every text surface shares — nibli-host, nibli-server, nibli-wasm.

render_collapsed_text_with

As render_collapsed_text, rendering under a domain-gloss overlay (None = the dictionary-fallback default).

render_logic_buffer

Render a compiled LogicBuffer as readable English.

render_logic_tree

Render a compiled LogicBuffer as an indented, one-node-per-line structural tree with functional term notation — the [Logic] half of :debug.

render_node_text

Render any RenderedNode tree as indented text (the building block of render_collapsed_text). With include_detail = false, proof-role-detail clusters are skipped (the clean macro view); with true, they render too.

render_proof

Build the structured rendered proof tree from a wire proof trace.

render_proof_text

Render the proof tree as indented text (REPL/CLI), with the NAF note header.

render_proof_text_indented

As render_proof_text, with a base indentation (nibli-host indents by one).

summarize_proof

Build a one-block plain-English “why” explanation of the trace, or None if there is nothing summarizable (callers then print nothing extra).

summarize_proof_with

As summarize_proof, but renders under a domain-gloss overlay (curated examples read in real domain terms; None = the dictionary-fallback default).

trace_display

Compact textual rendering used in CLI proof traces (… -> TRUE).