nibli-render 0.1.0

//! Term-level rendering primitives shared by the fact humanizer, the IR
//! back-translation, and the proof renderer. ONE definition of role-predicate
//! detection, event-Skolem detection, and Skolem humanization lives here.

/// Detect a Neo-Davidsonian role predicate name (`goes_x2`) and return its
/// collapsed, ARGUMENT-NAMED form for the proof narrative: the curated place
/// label where the alias carries one (`goes_x2` → `goes.destination`), else the
/// positional `x<N>` fallback (`dog_x1` → `dog.dog`, since a class predicate's
/// subject place has no argument name). Returns `None` for non-role names.
pub(crate) fn collapse_role_name(name: &str) -> Option<String> {
    let base = role_base(name)?;
    let idx = role_index(name)?;
    let place = nibli_lexicon::relation_places(base)
        .and_then(|p| p.get(idx - 1).copied())
        .map(str::to_owned)
        .unwrap_or_else(|| format!("x{idx}"));
    Some(format!("{base}.{place}"))
}

/// Base relation of a role predicate (`gerku_x1` -> `Some("dog")`).
pub(crate) fn role_base(name: &str) -> Option<&str> {
    let u = name.rfind('_')?;
    let suffix = &name[u + 1..];
    let rest = suffix.strip_prefix('x')?;
    if !rest.is_empty() && rest.bytes().all(|b| b.is_ascii_digit()) {
        Some(&name[..u])
    } else {
        None
    }
}

/// 1-based place index of a role predicate (`gerku_x1` -> `Some(1)`).
pub(crate) fn role_index(name: &str) -> Option<usize> {
    let u = name.rfind('_')?;
    let rest = name[u + 1..].strip_prefix('x')?;
    rest.parse::<usize>().ok()
}

/// Is this rendered term string a bare event Skolem (`sk_N`)? Event variables
/// are internal plumbing and are hidden from role-predicate argument lists.
pub(crate) fn is_event_skolem(s: &str) -> bool {
    s.strip_prefix("sk_")
        .is_some_and(|r| !r.is_empty() && r.bytes().all(|b| b.is_ascii_digit()))
}

/// Like [`is_event_skolem`], but also accepts a DEPENDENT event Skolem
/// (`sk_N(args)`). A universal rule's conclusion event depends on the quantified
/// individual, so its role predicates carry `sk_N(rex)` in arg0 — when
/// regrouping role predicates back to a surface fact, the arg0 event is the
/// group key regardless of dependency. (Distinct from [`is_event_skolem`], which
/// is correctly strict where a `sk_N(arg)` is an exposed witness, not plumbing.)
pub(crate) fn is_event_skolem_arg(s: &str) -> bool {
    s.strip_prefix("sk_")
        .and_then(|r| r.bytes().next())
        .is_some_and(|b| b.is_ascii_digit())
}

/// Humanize a Skolem token for display: `sk_N` -> `#N`, `sk_N(arg)` -> `#N(arg)`.
/// A non-Skolem constant passes through, but routes through the active domain
/// overlay first (`varfarin` -> "warfarin") — `None` overlay = verbatim.
pub(crate) fn humanize_skolem(s: &str) -> String {
    if let Some(rest) = s.strip_prefix("sk_") {
        // Bare `sk_N`.
        if !rest.is_empty() && rest.bytes().all(|b| b.is_ascii_digit()) {
            return format!("#{rest}");
        }
        // `sk_N(arg)` — keep the argument tail verbatim.
        if let Some(paren) = rest.find('(') {
            let num = &rest[..paren];
            if !num.is_empty() && num.bytes().all(|b| b.is_ascii_digit()) {
                return format!("#{num}{}", &rest[paren..]);
            }
        }
    }
    if let Some(name) = crate::overlay::active().and_then(|o| o.name(s)) {
        return name.to_string();
    }
    s.to_string()
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn role_detection() {
        assert_eq!(collapse_role_name("dog_x1").as_deref(), Some("dog.dog"));
        assert_eq!(role_base("dog_x2"), Some("dog"));
        assert_eq!(role_index("dog_x2"), Some(2));
        assert_eq!(collapse_role_name("dog"), None);
        assert_eq!(collapse_role_name("se_katna"), None); // not _xN
        assert_eq!(role_base("animal"), None);
    }

    #[test]
    fn role_names_use_argument_labels() {
        // A labeled place renders the curated argument name…
        assert_eq!(
            collapse_role_name("goes_x2").as_deref(),
            Some("goes.destination")
        );
        assert_eq!(collapse_role_name("goes_x1").as_deref(), Some("goes.goer"));
        // …and since the committed corpus EVERY place is named, so the old
        // `dog.dog` positional fallback no longer occurs for corpus relations
        // (dog's places are ["dog", "breed"]). The x<N> fallback survives only
        // for relations unknown to the corpus.
        assert_eq!(collapse_role_name("dog_x1").as_deref(), Some("dog.dog"));
        assert_eq!(
            collapse_role_name("mystery_x1").as_deref(),
            Some("mystery.x1")
        );
    }

    #[test]
    fn event_skolem_detection() {
        assert!(is_event_skolem("sk_0"));
        assert!(is_event_skolem("sk_12"));
        assert!(!is_event_skolem("sk_1(adam)")); // witness Skolem, not an event var
        assert!(!is_event_skolem("adam"));
        assert!(!is_event_skolem("sk_"));
    }

    #[test]
    fn skolem_humanization() {
        assert_eq!(humanize_skolem("sk_2"), "#2");
        assert_eq!(humanize_skolem("sk_1(adam)"), "#1(adam)");
        assert_eq!(humanize_skolem("adam"), "adam");
    }

    #[test]
    fn overlay_name_override_then_restores() {
        use crate::corpus_overlay::DRUG_INTERACTIONS_OVERLAY;
        use crate::overlay::with_overlay;
        // Fallback: the raw cmevla passes through verbatim.
        assert_eq!(humanize_skolem("varfarin"), "varfarin");
        with_overlay(Some(&DRUG_INTERACTIONS_OVERLAY), || {
            assert_eq!(humanize_skolem("varfarin"), "warfarin");
            assert_eq!(humanize_skolem("siptucin"), "CYP2C9");
            // Non-name tokens still pass through; Skolems still humanize.
            assert_eq!(humanize_skolem("zo'e"), "zo'e");
            assert_eq!(humanize_skolem("sk_2"), "#2");
        });
        assert_eq!(humanize_skolem("varfarin"), "varfarin");
    }
}