//! Tests for the logical language: terms, atoms, literals, formulas,
//! negation, and the `formula!` macro (Definition 3.2, M&P 2014).

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;

// --- Variable/constant convention ---

#[test]
fn uppercase_identifier_is_variable() {
    let f = formula!(bird(X));
    match &f {
        Formula::Lit(Literal::Pos(atom)) => {
            assert_eq!(atom.terms.len(), 1);
            assert_eq!(atom.terms[0], Term::Var("X".to_string()));
        }
        other => panic!("expected Lit(Pos(...)), got {other:?}"),
    }
}

#[test]
fn lowercase_identifier_is_constant() {
    let f = formula!(bird(tweety));
    match &f {
        Formula::Lit(Literal::Pos(atom)) => {
            assert_eq!(atom.terms.len(), 1);
            assert_eq!(atom.terms[0], Term::Const("tweety".to_string()));
        }
        other => panic!("expected Lit(Pos(...)), got {other:?}"),
    }
}

#[test]
fn mixed_variables_and_constants() {
    let f = formula!(likes(X, tweety));
    match &f {
        Formula::Lit(Literal::Pos(atom)) => {
            assert_eq!(atom.terms.len(), 2);
            assert_eq!(atom.terms[0], Term::Var("X".to_string()));
            assert_eq!(atom.terms[1], Term::Const("tweety".to_string()));
        }
        other => panic!("expected Lit(Pos(...)), got {other:?}"),
    }
}

// --- Literal::negate() round-trip ---

#[test]
fn pos_negate_yields_neg() {
    let atom = Atom {
        predicate: "p".to_string(),
        terms: vec![],
    };
    let pos = Literal::Pos(atom.clone());
    let neg = pos.negate();
    assert_eq!(neg, Literal::Neg(atom));
}

#[test]
fn neg_negate_yields_pos() {
    let atom = Atom {
        predicate: "p".to_string(),
        terms: vec![],
    };
    let neg = Literal::Neg(atom.clone());
    let pos = neg.negate();
    assert_eq!(pos, Literal::Pos(atom));
}

#[test]
fn double_negate_is_identity() {
    let atom = Atom {
        predicate: "q".to_string(),
        terms: vec![Term::Const("a".to_string())],
    };
    let original = Literal::Pos(atom);
    assert_eq!(original.negate().negate(), original);
}

// --- Formula::classical_negation() ---

#[test]
fn classical_negation_of_pos_literal_yields_neg() {
    let f = formula!(p);
    let neg = f.classical_negation();
    assert_eq!(neg, formula!(!p));
}

#[test]
fn classical_negation_of_neg_literal_yields_pos() {
    let f = formula!(!p);
    let neg = f.classical_negation();
    assert_eq!(neg, formula!(p));
}

#[test]
fn classical_negation_of_and_wraps_in_not() {
    let f = Formula::And(vec![formula!(p), formula!(q)]);
    let neg = f.classical_negation();
    match neg {
        Formula::Not(inner) => assert_eq!(*inner, Formula::And(vec![formula!(p), formula!(q)])),
        other => panic!("expected Not(And(...)), got {other:?}"),
    }
}

#[test]
fn classical_negation_of_implies_wraps_in_not() {
    let f = formula!((p) -> (q));
    let neg = f.classical_negation();
    match neg {
        Formula::Not(inner) => assert_eq!(*inner, formula!((p) -> (q))),
        other => panic!("expected Not(Implies(...)), got {other:?}"),
    }
}

// --- formula! macro compound forms ---

#[test]
fn conjunction_macro() {
    let f = formula!((p) & (q));
    match &f {
        Formula::And(fs) => {
            assert_eq!(fs.len(), 2);
            assert_eq!(fs[0], formula!(p));
            assert_eq!(fs[1], formula!(q));
        }
        other => panic!("expected And(...), got {other:?}"),
    }
}

#[test]
fn disjunction_macro() {
    let f = formula!((p) | (q));
    match &f {
        Formula::Or(fs) => {
            assert_eq!(fs.len(), 2);
            assert_eq!(fs[0], formula!(p));
            assert_eq!(fs[1], formula!(q));
        }
        other => panic!("expected Or(...), got {other:?}"),
    }
}

#[test]
fn implication_macro() {
    let f = formula!(p -> q);
    match &f {
        Formula::Implies(a, b) => {
            assert_eq!(**a, formula!(p));
            assert_eq!(**b, formula!(q));
        }
        other => panic!("expected Implies(...), got {other:?}"),
    }
}

// --- formula! macro propositional and predicate atoms ---

#[test]
fn propositional_atom_has_no_terms() {
    let f = formula!(p);
    match &f {
        Formula::Lit(Literal::Pos(atom)) => {
            assert_eq!(atom.predicate, "p");
            assert!(atom.terms.is_empty());
        }
        other => panic!("expected Lit(Pos(p)), got {other:?}"),
    }
}

#[test]
fn negated_propositional_atom() {
    let f = formula!(!p);
    match &f {
        Formula::Lit(Literal::Neg(atom)) => {
            assert_eq!(atom.predicate, "p");
            assert!(atom.terms.is_empty());
        }
        other => panic!("expected Lit(Neg(p)), got {other:?}"),
    }
}

#[test]
fn negated_atom_with_terms() {
    let f = formula!(!flies(tweety));
    match &f {
        Formula::Lit(Literal::Neg(atom)) => {
            assert_eq!(atom.predicate, "flies");
            assert_eq!(atom.terms, vec![Term::Const("tweety".to_string())]);
        }
        other => panic!("expected Lit(Neg(flies(tweety))), got {other:?}"),
    }
}
