/*
 * test_logic.cpp — LOGICAL body grammar, spec §6.2.1 (ANTHEOS-LOGICAL-V1-PARSER-IMPL)
 *
 * Covers every production the spec lists, every input it says to reject, the
 * round-trip, and BOTH evaluator styles — which is the point of the last two:
 * §6.2.1 makes atom semantics consumer-defined, so the grammar has to hold
 * under two readings that disagree about what the atoms mean.
 *
 * Copyright (c) 2025-2026 Are Bjørby <are.bjorby@langsyn.org>
 * SPDX-License-Identifier: MIT
 */

#include "test_common.hpp"
#include "antheos.hpp"

#include <string>

using namespace antheos;
using namespace antheos::logic;

namespace {

bool parses(std::string_view b) { return parse_logical(b).has_value(); }

/* Parse and re-emit. The spec's canonical forms must survive unchanged. */
std::string round_trip(std::string_view b) {
    auto e = parse_logical(b);
    if (!e) return "<reject>";
    return emit_logical(*e);
}

/* ── Accepted productions (§6.2.1 V1 Grammar) ── */

void test_logic_every_atom_parses() {
    /* The eleven, and only the eleven. */
    const char* atoms = "IODHUBWQMGT";
    for (const char* c = atoms; *c; ++c) {
        std::string body(1, *c);
        ASSERT_TRUE(parses(body));
        ASSERT_TRUE(round_trip(body) == body);
    }
}

void test_logic_negation() {
    ASSERT_TRUE(parses("!H"));
    ASSERT_TRUE(parses("!!H"));
    ASSERT_TRUE(round_trip("!H") == "!H");
    ASSERT_TRUE(round_trip("!!H") == "!!H");
}

void test_logic_conjunction_and_disjunction() {
    ASSERT_TRUE(round_trip("H&Q") == "H&Q");
    ASSERT_TRUE(round_trip("H&Q&D") == "H&Q&D");
    ASSERT_TRUE(round_trip("H|Q") == "H|Q");
    ASSERT_TRUE(round_trip("H|Q|D") == "H|Q|D");
}

void test_logic_precedence_is_structural() {
    /* `!` > `&` > `|`. The round-trip proves the SHAPE, not just acceptance:
     * `H|Q&D` must come back without parens, which it only can if it parsed as
     * H | (Q&D). Had it parsed as (H|Q)&D the emitter would have to add them. */
    ASSERT_TRUE(round_trip("!H&!Q") == "!H&!Q");
    ASSERT_TRUE(round_trip("H|Q&D") == "H|Q&D");
    /* And the other grouping keeps the parens that make it that grouping. */
    ASSERT_TRUE(round_trip("(H|Q)&D") == "(H|Q)&D");
}

void test_logic_parens() {
    ASSERT_TRUE(round_trip("(H|Q)&D") == "(H|Q)&D");
    ASSERT_TRUE(round_trip("!(H&Q)") == "!(H&Q)");
    ASSERT_TRUE(round_trip("!(H|Q)&!T") == "!(H|Q)&!T");
    /* Redundant parens are dropped — the emitter's job is the CANONICAL form,
     * so this one deliberately does not round-trip to its input. */
    ASSERT_TRUE(round_trip("(H)") == "H");
    ASSERT_TRUE(round_trip("(H&Q)&D") == "H&Q&D");
}

void test_logic_left_associativity_survives_emission() {
    /* `A&B&C` is (A&B)&C, so the right-nested form is a DIFFERENT tree and has
     * to keep its parens or it would read back as the left-nested one. */
    ASSERT_TRUE(round_trip("H&(Q&D)") == "H&(Q&D)");
    ASSERT_TRUE(round_trip("H|(Q|D)") == "H|(Q|D)");
}

/* ── Rejected inputs (§6.2.1 V1 Rejected Inputs) ── */

void test_logic_rejects_empty_with_teaching() {
    std::string why;
    ASSERT_TRUE(!parse_logical("", &why).has_value());
    /* The spec asks for a teaching error here specifically. */
    ASSERT_TRUE(!why.empty());
    ASSERT_TRUE(why.find("empty") != std::string::npos);
}

void test_logic_rejects_non_atoms() {
    ASSERT_TRUE(!parses("F"));      /* the one the spec calls out: no F-flag */
    ASSERT_TRUE(!parses("Z"));
    ASSERT_TRUE(!parses("h"));      /* lowercase is not the atom */
    ASSERT_TRUE(!parses("Hello"));  /* multi-character atoms are V2 */
}

void test_logic_rejects_non_v1_operators() {
    ASSERT_TRUE(!parses("H^Q"));
    ASSERT_TRUE(!parses("H>Q"));
    ASSERT_TRUE(!parses("H=Q"));
}

void test_logic_rejects_malformed_structure() {
    ASSERT_TRUE(!parses("(H"));     /* unmatched paren */
    ASSERT_TRUE(!parses("H)"));
    ASSERT_TRUE(!parses("H&"));     /* operator without right operand */
    ASSERT_TRUE(!parses("&H"));
    ASSERT_TRUE(!parses("!"));
    ASSERT_TRUE(!parses("()"));
}

void test_logic_rejects_whitespace() {
    /* V1 is strict; whitespace tolerance is reserved for V2. */
    ASSERT_TRUE(!parses("H Q"));
    ASSERT_TRUE(!parses("H & Q"));
    ASSERT_TRUE(!parses(" H"));
    ASSERT_TRUE(!parses("H "));
}

/* ── Consumer semantics (§6.2.1: atom meaning is NOT grammar-defined) ── */

void test_logic_scaleback_flag_exclusion_semantic() {
    /* Scaleback's reading: an atom is TRUE when the peer can handle that flag.
     * This peer handles everything except H and Q, so `!H&!Q` — "I cannot do
     * hex and cannot do quadword" — is the expression that holds for it. */
    auto handles = [](char a) { return a != 'H' && a != 'Q'; };

    auto e1 = parse_logical("!H&!Q");
    ASSERT_TRUE(e1.has_value());
    if (!e1) return;
    ASSERT_TRUE(evaluate_logical(*e1, handles) == true);

    auto e2 = parse_logical("!D&!T");   /* both ARE handled, so both negations fail */
    ASSERT_TRUE(e2.has_value());
    if (!e2) return;
    ASSERT_TRUE(evaluate_logical(*e2, handles) == false);

    /* De Morgan, from the spec's own example table: !(H&Q) and !H|!Q agree. */
    auto dm1 = parse_logical("!(H&Q)");
    auto dm2 = parse_logical("!H|!Q");
    ASSERT_TRUE(dm1.has_value() && dm2.has_value());
    if (!dm1 || !dm2) return;
    ASSERT_TRUE(evaluate_logical(*dm1, handles) == evaluate_logical(*dm2, handles));
}

void test_logic_literal_semantic_over_the_same_grammar() {
    /* A different consumer, opposite reading: T alone is true, everything else
     * false. Same parser, same trees — which is the separation §6.2.1 requires,
     * and the reason this is a second test rather than a second parser. */
    auto literal = [](char a) { return a == 'T'; };

    auto t = parse_logical("T");
    ASSERT_TRUE(t.has_value());
    if (!t) return;
    ASSERT_TRUE(evaluate_logical(*t, literal) == true);

    auto h = parse_logical("H");
    ASSERT_TRUE(h.has_value());
    if (!h) return;
    ASSERT_TRUE(evaluate_logical(*h, literal) == false);

    /* `F` would be the natural companion to `T` under this reading, and the
     * GRAMMAR refuses it — the separation cuts both ways. */
    ASSERT_TRUE(!parses("F"));

    /* The same body evaluates differently under the two readings, which is the
     * whole claim: `!H` is true for the literal consumer and false for a
     * Scaleback peer that handles H. */
    auto nh = parse_logical("!H");
    ASSERT_TRUE(nh.has_value());
    if (!nh) return;
    auto handles_all = [](char) { return true; };
    ASSERT_TRUE(evaluate_logical(*nh, literal) == true);
    ASSERT_TRUE(evaluate_logical(*nh, handles_all) == false);
}

void test_logic_evaluator_short_circuits() {
    /* `&` must not ask about the right operand once the left is false — a
     * consumer's evaluator may be expensive, or may not know every atom. */
    int asked = 0;
    auto counting = [&asked](char a) { asked++; return a == 'T'; };
    auto e = parse_logical("H&Q");
    ASSERT_TRUE(e.has_value());
    if (!e) return;
    ASSERT_TRUE(evaluate_logical(*e, counting) == false);
    ASSERT_EQ(asked, 1);
}

}  // namespace

void test_logic_run(int& out_run, int& out_passed) {
    std::printf("\n[logic]\n");

    TEST(test_logic_every_atom_parses);
    TEST(test_logic_negation);
    TEST(test_logic_conjunction_and_disjunction);
    TEST(test_logic_precedence_is_structural);
    TEST(test_logic_parens);
    TEST(test_logic_left_associativity_survives_emission);
    TEST(test_logic_rejects_empty_with_teaching);
    TEST(test_logic_rejects_non_atoms);
    TEST(test_logic_rejects_non_v1_operators);
    TEST(test_logic_rejects_malformed_structure);
    TEST(test_logic_rejects_whitespace);
    TEST(test_logic_scaleback_flag_exclusion_semantic);
    TEST(test_logic_literal_semantic_over_the_same_grammar);
    TEST(test_logic_evaluator_short_circuits);

    out_run    = tests_run;
    out_passed = tests_passed;
}