camxes-rs 1.1.1

//! Lower the PEG-produced `jbo_prop::Texticule` / `JboProp` tree
//! into egglog program text (a sequence of `(let …)` expressions) that can
//! be fed to an `EGraph` via `parse_and_run_program`.
//!
//! Lowering strategy: each recursive call returns an egglog **expression
//! string** (an s-expression that can appear on the right-hand side of a
//! `let` binding).  We collect the full program in a `Vec<String>` of lines
//! and join them at the end.  No `let` bindings are emitted for sub-
//! expressions — everything is inlined — to keep the output compact.
//!
//! The schema (datatypes/constructors) and the rewrite rules live in the
//! `.egg` files embedded with `include_str!`.

use crate::jbo_prop::{
    DecoratedTagUnit, JboConnective, JboFragment, JboMex, JboModalOp, JboOperator, JboProp,
    JboQuantifier, JboRel, JboTag, JboTagUnit, JboTerm, SideType, Texticule,
};
use crate::jbo_syntax::{LogJboConnective, SumtiQualifier};
use crate::logic::{Connective, LojQuantifier, Prop};

// ---------------------------------------------------------------------------
// Public entry point
// ---------------------------------------------------------------------------

/// Lower a slice of `Texticule`s (the semantic output of `eval_text`) into an
/// egglog program string that, when run, asserts all facts into the e-graph.
///
/// The returned string does **not** include the schema or rules — it only
/// contains `(let …)` / `(TextTexticule …)` assertions.
pub fn lower_text(text_id: i64, texticules: &[Texticule]) -> String {
    let mut lines: Vec<String> = Vec::new();
    for (pos, tex) in texticules.iter().enumerate() {
        let expr = lower_texticule(tex, &mut lines);
        lines.push(format!(
            "(TextTexticule {} {} {})",
            text_id, pos as i64, expr
        ));
    }
    lines.join("\n")
}

// ---------------------------------------------------------------------------
// Texticule
// ---------------------------------------------------------------------------

fn lower_texticule(tex: &Texticule, _lines: &mut Vec<String>) -> String {
    match tex {
        Texticule::TexticuleProp(prop) => {
            format!("(TexticuleProp {})", lower_prop(prop))
        }
        Texticule::TexticuleFrag(frag) => match frag {
            JboFragment::JboFragTerms(terms) => {
                format!(
                    "(TexticuleFragTerms {})",
                    lower_term_list(terms)
                )
            }
            JboFragment::JboFragUnparsed(_) => {
                "(TexticuleFragTerms (TNil))".to_string()
            }
        },
        Texticule::TexticuleSide(side, inner) => {
            let inner_str = lower_texticule(inner, &mut Vec::new());
            match side {
                SideType::SideBracketed => {
                    format!("(TexticuleSideBracketed {})", inner_str)
                }
                SideType::SideDiscursive => {
                    format!("(TexticuleSideDiscursive {})", inner_str)
                }
            }
        }
    }
}

// ---------------------------------------------------------------------------
// JboProp
// ---------------------------------------------------------------------------

fn lower_prop(prop: &JboProp) -> String {
    match prop {
        Prop::Eet => "(Eet)".to_string(),
        Prop::Not(p) => format!("(PNot {})", lower_prop(p)),
        Prop::Connected(conn, p1, p2) => {
            let ctor = match conn {
                Connective::And => "PAnd",
                Connective::Or => "POr",
                Connective::Impl => "PImpl",
                Connective::Equiv => "PEquiv",
            };
            format!("({} {} {})", ctor, lower_prop(p1), lower_prop(p2))
        }
        Prop::NonLogConnected(c, p1, p2) => {
            format!(
                "(PNonLog {} {} {})",
                egglog_string(c),
                lower_prop(p1),
                lower_prop(p2)
            )
        }
        Prop::Modal(op, p) => {
            format!("(PModal {} {})", lower_modal_op(op), lower_prop(p))
        }
        Prop::Quantified(q, _restriction, _body) => {
            // Higher-order functions cannot be directly represented;
            // we represent the quantifier structure with a synthetic var index 0.
            // A fuller encoding would pre-evaluate the body at a fresh variable.
            let quant_str = lower_quantifier(q);
            format!("(PQuant {} 0 (Eet) 0)", quant_str)
        }
        Prop::Rel(rel, terms) => {
            format!("(PRel {} {})", lower_rel(rel), lower_term_list(terms))
        }
    }
}

// ---------------------------------------------------------------------------
// JboRel
// ---------------------------------------------------------------------------

fn lower_rel(rel: &JboRel) -> String {
    match rel {
        JboRel::Brivla(s) => format!("(Brivla {})", egglog_string(s)),
        JboRel::Equal => "(Equal)".to_string(),
        JboRel::Among(t) => format!("(Among {})", lower_term(t)),
        JboRel::Tanru(r1, r2) => format!("(Tanru {} {})", lower_rel(r1), lower_rel(r2)),
        JboRel::AppliedRel(r, terms) => {
            // Encode as a Tanru(r, …) approximation — AppliedRel is not in
            // the schema as a separate constructor (it's a niche internal form).
            // Represent as the underlying relation + PRel with the extra terms.
            let _ = terms;
            lower_rel(r)
        }
        JboRel::TanruConnective(_conn, r1, r2) => {
            format!("(Tanru {} {})", lower_rel(r1), lower_rel(r2))
        }
        JboRel::PermutedRel(n, r) => {
            format!("(PermutedRel {} {})", n, lower_rel(r))
        }
        JboRel::RVar(n) => format!("(RVar {})", n),
        JboRel::BoundRVar(n) => format!("(BoundRVar {})", n),
        JboRel::RAss(n) => format!("(RAss {})", n),
        JboRel::UnboundBribasti(_) => "(RVar -1)".to_string(),
        JboRel::Moi(t, s) => {
            format!("(Tanru (Brivla {}) (Among {}))", egglog_string(s), lower_term(t))
        }
        JboRel::OperatorRel(op) => {
            let _ = op;
            "(Brivla \"<op>\")".to_string()
        }
        JboRel::ScalarNegatedRel(s, r) => {
            format!("(ScalarNegRel {} {})", egglog_string(s), lower_rel(r))
        }
        JboRel::VPredRel(_) => "(Brivla \"<vpred>\")".to_string(),
        JboRel::AbsPred(abs, _) => {
            format!("(Brivla {})", egglog_string(&format!("<abspred:{}>", abs)))
        }
        JboRel::AbsProp(abs, prop) => {
            format!("(AbsPropRel {} {})", egglog_string(abs), lower_prop(prop))
        }
        JboRel::TagRel(tag) => format!("(TagRel {})", lower_tag(tag)),
        JboRel::ModalRel(op, r) => {
            format!("(ModalRel {} {})", lower_modal_op(op), lower_rel(r))
        }
    }
}

// ---------------------------------------------------------------------------
// JboTerm
// ---------------------------------------------------------------------------

fn lower_term(term: &JboTerm) -> String {
    match term {
        JboTerm::BoundVar(n) => format!("(BoundVar {})", n),
        JboTerm::Var(n) => format!("(Var {})", n),
        JboTerm::Named(s) => format!("(Named {})", egglog_string(s)),
        JboTerm::NonAnaph(s) => format!("(NonAnaph {})", egglog_string(s)),
        JboTerm::Unfilled => "(Unfilled)".to_string(),
        JboTerm::Valsi(s) => format!("(Valsi {})", egglog_string(s)),
        JboTerm::PredNamed(_) => "(Named \"<pred-named>\")".to_string(),
        JboTerm::Constant(n, args) => {
            // Encode as a Named with a synthetic label + inline args
            let _ = args;
            format!("(Named {})", egglog_string(&format!("<const:{}>", n)))
        }
        JboTerm::UnboundSumbasti(_) => "(Var -1)".to_string(),
        JboTerm::Value(_) => "(Var -2)".to_string(),
        JboTerm::QualifiedTerm(q, t) => {
            let q_str = match q {
                SumtiQualifier::LAhE(s) => s.clone(),
                SumtiQualifier::NAhE_BO(s) => s.clone(),
            };
            format!("(QualifiedTerm {} {})", egglog_string(&q_str), lower_term(t))
        }
        JboTerm::TheMex(_) => "(Var -3)".to_string(),
        JboTerm::JoikedTerms(j, t1, t2) => {
            format!(
                "(JoikedTerms {} {} {})",
                egglog_string(j),
                lower_term(t1),
                lower_term(t2)
            )
        }
        JboTerm::JboQuote(text) => {
            let list = lower_texticule_list(text);
            format!("(JboQuoteT {})", list)
        }
        JboTerm::JboErrorQuote(words) => {
            format!("(Valsi {})", egglog_string(&words.join(" ")))
        }
        JboTerm::JboNonJboQuote(s) => format!("(Valsi {})", egglog_string(s)),
        JboTerm::TermWithSides(t, _sides) => lower_term(t),
    }
}

fn lower_term_list(terms: &[JboTerm]) -> String {
    terms.iter().rev().fold("(TNil)".to_string(), |acc, t| {
        format!("(TCons {} {})", lower_term(t), acc)
    })
}

fn lower_texticule_list(texs: &[Texticule]) -> String {
    texs.iter().rev().fold("(XNil)".to_string(), |acc, t| {
        format!("(XCons {} {})", lower_texticule(t, &mut Vec::new()), acc)
    })
}

// ---------------------------------------------------------------------------
// JboQuantifier
// ---------------------------------------------------------------------------

fn lower_quantifier(q: &JboQuantifier) -> String {
    match q {
        JboQuantifier::MexQuantifier(m) => format!("(MexQuant {})", lower_mex(m)),
        JboQuantifier::LojQuantifier(lq) => match lq {
            LojQuantifier::Exists => "(Exists)".to_string(),
            LojQuantifier::Forall => "(Forall)".to_string(),
            LojQuantifier::Exactly(n) => format!("(Exactly {})", n),
        },
        JboQuantifier::QuestionQuantifier => "(QuestionQ)".to_string(),
        JboQuantifier::RelQuantifier(inner) => {
            format!("(RelQuant {})", lower_quantifier(inner))
        }
    }
}

// ---------------------------------------------------------------------------
// JboModalOp
// ---------------------------------------------------------------------------

fn lower_modal_op(op: &JboModalOp) -> String {
    match op {
        JboModalOp::NonVeridical => "(NonVeridical)".to_string(),
        JboModalOp::QTruthModal => "(QTruthModal)".to_string(),
        JboModalOp::WithEventAs(t) => format!("(WithEventAs {})", lower_term(t)),
        JboModalOp::Tagged(tag, Some(t)) => {
            format!("(Tagged {} {})", lower_tag(tag), lower_term(t))
        }
        JboModalOp::Tagged(tag, None) => {
            format!("(TaggedNoTerm {})", lower_tag(tag))
        }
    }
}

// ---------------------------------------------------------------------------
// JboTag / DecoratedTagUnit / JboTagUnit / JboConnective
// ---------------------------------------------------------------------------

fn lower_tag(tag: &JboTag) -> String {
    match tag {
        JboTag::DecoratedTagUnits(units) => {
            let list = units.iter().rev().fold("(DTNil)".to_string(), |acc, u| {
                format!("(DTCons {} {})", lower_dec_tag_unit(u), acc)
            });
            format!("(DecoratedTagUnits {})", list)
        }
        JboTag::ConnectedTag(conn, t1, t2) => {
            format!(
                "(ConnectedTag {} {} {})",
                lower_jbo_conn(conn),
                lower_tag(t1),
                lower_tag(t2)
            )
        }
    }
}

fn lower_dec_tag_unit(dtu: &DecoratedTagUnit) -> String {
    let nahe = dtu.nahe.as_deref().unwrap_or("");
    let se = dtu.se.unwrap_or(0);
    let nai = if dtu.nai { 1i64 } else { 0i64 };
    format!(
        "(DecTagUnitMk {} {} {} {})",
        egglog_string(nahe),
        se,
        nai,
        lower_tag_unit(&dtu.tag_unit)
    )
}

fn lower_tag_unit(tu: &JboTagUnit) -> String {
    match tu {
        JboTagUnit::TenseCmavo(s) => format!("(TenseCmavo {})", egglog_string(s)),
        JboTagUnit::CAhA(s) => format!("(CAhA {})", egglog_string(s)),
        JboTagUnit::BAI(s) => format!("(BAI {})", egglog_string(s)),
        JboTagUnit::FAhA(mohi, s) => {
            let m = match mohi {
                Some(true) => 1i64,
                _ => 0i64,
            };
            format!("(FAhA {} {})", m, egglog_string(s))
        }
        JboTagUnit::TAhE_ZAhO(is_space, s) => {
            format!("(TAhE_ZAhO {} {})", *is_space as i64, egglog_string(s))
        }
        JboTagUnit::ROI(s, is_space, mex) => {
            format!(
                "(ROI {} {} {})",
                egglog_string(s),
                *is_space as i64,
                lower_mex(mex)
            )
        }
        JboTagUnit::FIhO(_) => format!("(FIhO_tag {})", egglog_string("<fiho>")),
        JboTagUnit::KI => "(KI)".to_string(),
        JboTagUnit::CUhE(s) => format!("(CUhE {})", egglog_string(s)),
    }
}

fn lower_jbo_conn(conn: &JboConnective) -> String {
    match conn {
        JboConnective::JboConnLog(Some(tag), ljc) => {
            format!(
                "(JboConnLog {} {})",
                lower_tag(tag),
                lower_log_conn(ljc)
            )
        }
        JboConnective::JboConnLog(None, ljc) => {
            format!("(JboConnLogNoTag {})", lower_log_conn(ljc))
        }
        JboConnective::JboConnJoik(Some(tag), joik) => {
            format!(
                "(JboConnJoik {} {})",
                lower_tag(tag),
                egglog_string(joik)
            )
        }
        JboConnective::JboConnJoik(None, joik) => {
            format!("(JboConnJoikNoTag {})", egglog_string(joik))
        }
    }
}

fn lower_log_conn(ljc: &LogJboConnective) -> String {
    format!(
        "(LogConnMk {} {} {})",
        ljc.b1 as i64,
        egglog_string(&ljc.c.to_string()),
        ljc.b2 as i64
    )
}

// ---------------------------------------------------------------------------
// JboMex / JboOperator
// ---------------------------------------------------------------------------

fn lower_mex(mex: &JboMex) -> String {
    match mex {
        JboMex::MexInt(n) => format!("(MexInt {})", n),
        JboMex::MexSumti(t) => format!("(MexSumti {})", lower_term(t)),
        JboMex::MexArray(ms) => {
            let list = ms.iter().rev().fold("(MLNil)".to_string(), |acc, m| {
                format!("(MLCons {} {})", lower_mex(m), acc)
            });
            format!("(MexArray {})", list)
        }
        JboMex::Operation(op, ms) => {
            let list = ms.iter().rev().fold("(MLNil)".to_string(), |acc, m| {
                format!("(MLCons {} {})", lower_mex(m), acc)
            });
            format!("(MexOp {} {})", lower_operator(op), list)
        }
        JboMex::ConnectedMex(_, _, m1, m2) => {
            // Flatten connected mex into an array approximation
            let list = format!(
                "(MLCons {} (MLCons {} (MLNil)))",
                lower_mex(m1),
                lower_mex(m2)
            );
            format!("(MexArray {})", list)
        }
        JboMex::QualifiedMex(_, m) => lower_mex(m),
        JboMex::MexNumeralString(_) => "(MexInt 0)".to_string(),
        JboMex::MexLerfuString(_) => "(MexInt 0)".to_string(),
        JboMex::MexSelbri(_) => "(MexInt -1)".to_string(),
    }
}

fn lower_operator(op: &JboOperator) -> String {
    match op {
        JboOperator::OpVUhU(s) => format!("(OpVUhU {})", egglog_string(s)),
        JboOperator::OpPermuted(n, inner) => {
            format!("(OpPermuted {} {})", n, lower_operator(inner))
        }
        JboOperator::OpScalarNegated(s, inner) => {
            format!("(OpScalarNeg {} {})", egglog_string(s), lower_operator(inner))
        }
        JboOperator::OpMex(m) => format!("(OpMex {})", lower_mex(m)),
        JboOperator::OpSelbri(_) => "(OpVUhU \"<selbri-op>\")".to_string(),
        JboOperator::ConnectedOperator(_, _, o1, o2) => {
            // Flatten to first operand (simplification)
            let _ = o2;
            lower_operator(o1)
        }
    }
}

// ---------------------------------------------------------------------------
// Helpers
// ---------------------------------------------------------------------------

/// Escape a Rust string for embedding in an egglog string literal.
pub fn egglog_string(s: &str) -> String {
    let mut out = String::with_capacity(s.len() + 2);
    out.push('"');
    for c in s.chars() {
        match c {
            '"' => out.push_str("\\\""),
            '\\' => out.push_str("\\\\"),
            '\n' => out.push_str("\\n"),
            '\t' => out.push_str("\\t"),
            _ => out.push(c),
        }
    }
    out.push('"');
    out
}

// ---------------------------------------------------------------------------
// Tests
// ---------------------------------------------------------------------------

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

    #[test]
    fn test_egglog_string_escaping() {
        assert_eq!(egglog_string("hello"), "\"hello\"");
        assert_eq!(egglog_string("a\"b"), "\"a\\\"b\"");
        assert_eq!(egglog_string("a\\b"), "\"a\\\\b\"");
    }

    #[test]
    fn test_lower_prop_eet() {
        let prop: JboProp = Prop::Eet;
        assert_eq!(lower_prop(&prop), "(Eet)");
    }

    #[test]
    fn test_lower_prop_not_eet() {
        let prop: JboProp = Prop::Not(Box::new(Prop::Eet));
        assert_eq!(lower_prop(&prop), "(PNot (Eet))");
    }

    #[test]
    fn test_lower_rel_brivla() {
        let rel = JboRel::Brivla("klama".to_string());
        assert_eq!(lower_rel(&rel), "(Brivla \"klama\")");
    }

    #[test]
    fn test_lower_term_list_empty() {
        assert_eq!(lower_term_list(&[]), "(TNil)");
    }

    #[test]
    fn test_lower_term_list_one() {
        let terms = vec![JboTerm::BoundVar(1)];
        assert_eq!(lower_term_list(&terms), "(TCons (BoundVar 1) (TNil))");
    }
}