%% middot_test.pl — Tests for the 13 Middot of Rabbi Yishmael.
%%
%% Phase 3: Hermeneutical inference predicates.

:- use_module(library(plunit)).
:- use_module('../src/middot/middot').
:- use_module('../src/middot/kal_vachomer').
:- use_module('../src/middot/gezerah_shavah').
:- use_module('../src/middot/binyan_av').
:- use_module('../src/middot/klal_ufrat').
:- use_module('../src/middot/davar_yatza').
:- use_module('../src/middot/lamed_inyan').
:- use_module('../src/middot/shnei_ketuvim').
:- use_module('../src/specification/mitzvot').
:- use_module('../src/specification/torah_text').
:- use_module('../src/specification/root_meanings').

%% ============================================================
%% MASTER MODULE TESTS
%% ============================================================

:- begin_tests(middot_master).

%% All 13 middot are named
test(all_thirteen_named) :-
    findall(N, middah_name(N, _), Numbers),
    length(Numbers, 13).

%% all_middot returns a list of 13 names
test(all_middot_list) :-
    all_middot(Middot),
    length(Middot, 13).

%% Key middot names are correct
test(middah_1_is_kal_vachomer) :-
    middah_name(1, kal_vachomer).

test(middah_2_is_gezerah_shavah) :-
    middah_name(2, gezerah_shavah).

test(middah_13_is_shnei_ketuvim) :-
    middah_name(13, shnei_ketuvim).

%% apply_middah works for rule 1 (kal vachomer)
test(apply_middah_1, [nondet]) :-
    apply_middah(1, shabbat_rest, festival_rest, _Reasoning).

%% apply_middah works for rule 5 (klal ufrat)
test(apply_middah_5, [nondet]) :-
    apply_middah(5,
        general(fruit_trees),
        particular([olive, grape]),
        narrowed_to([olive, grape], from(fruit_trees))).

:- end_tests(middot_master).


%% ============================================================
%% RULE 1: KAL VACHOMER
%% ============================================================

:- begin_tests(kal_vachomer_tests).

%% Severity ordering: monetary < physical < capital < divine
test(monetary_less_than_physical) :-
    severity_ordering(monetary, physical).

test(physical_less_than_capital) :-
    severity_ordering(physical, capital).

test(capital_less_than_divine) :-
    severity_ordering(capital, divine).

%% Transitive stringency
test(monetary_less_than_capital) :-
    is_more_stringent(monetary, capital).

test(monetary_less_than_divine) :-
    is_more_stringent(monetary, divine).

%% Kal vachomer: shabbat → festival
test(shabbat_to_festival) :-
    kal_vachomer(shabbat_rest, festival_rest, _, definite).

%% Kal vachomer: monetary → physical compensation
test(monetary_to_physical) :-
    kal_vachomer(compensate_monetary, compensate_physical, _, definite).

%% Kal vachomer: domain-based derivation
test(domain_derivation, [nondet]) :-
    kal_vachomer(
        law_in(monetary, _),
        law_in(physical, _),
        derived(_, from(monetary), to(physical), kal_vachomer),
        definite
    ).

%% Unconditional mitzvah implies conditional
test(unconditional_implies_conditional, [nondet]) :-
    kal_vachomer(
        mitzvah_applies(1, always),
        mitzvah_applies(1, when(_)),
        derived(1, unconditional_implies_conditional, kal_vachomer),
        definite
    ).

%% Dayo principle: derived law equals source law
test(dayo_principle) :-
    kal_vachomer:dayo(derived(some_law, _, _, _), some_law).

:- end_tests(kal_vachomer_tests).


%% ============================================================
%% RULE 2: GEZERAH SHAVAH
%% ============================================================

:- begin_tests(gezerah_shavah_tests).

%% Known gezerah shavah: shabbat ↔ pesach (shemirah)
test(shabbat_pesach_shemirah) :-
    gezerah_shavah(shabbat_keeping, pesach_keeping, _, shin_mem_resh).

%% Known gezerah shavah: shabbat ↔ circumcision (ot)
test(shabbat_circumcision_ot) :-
    gezerah_shavah(shabbat_sign, circumcision_sign, _, aleph_vav_tav).

%% Shared keyword: two verses sharing a root link
test(shared_keyword_creation, [nondet]) :-
    shared_keyword(ref(bereishit, 1, 1), ref(bereishit, 1, 27), bet_resh_aleph).

%% Dynamic gezerah shavah from Torah text
test(dynamic_gezerah_shavah, [nondet]) :-
    gezerah_shavah(ref(bereishit, 1, 1), ref(bereishit, 1, 27), _, bet_resh_aleph).

:- end_tests(gezerah_shavah_tests).


%% ============================================================
%% RULES 3-4: BINYAN AV
%% ============================================================

:- begin_tests(binyan_av_tests).

%% Binyan av from one verse: source verse establishes domain law
%% Using Shemot 20:8 — mitzvah 154 (rest_on_shabbat), root qof_dalet_shin → holiness
test(binyan_av_one_verse, [nondet]) :-
    binyan_av_one(ref(shemot, 20, 8), applies_to_domain(_, _), _).

%% Binyan av from two verses: common root found
test(binyan_av_two_verses, [nondet]) :-
    binyan_av_two(
        ref(bereishit, 1, 1),
        ref(bereishit, 1, 27),
        general_rule(bet_resh_aleph, creation),
        bet_resh_aleph
    ).

%% Unified interface: single verse
test(binyan_av_single, [nondet]) :-
    binyan_av(single_verse(ref(shemot, 20, 8)), _, _).

%% Unified interface: two verses
test(binyan_av_two_unified, [nondet]) :-
    binyan_av(
        two_verses(ref(bereishit, 1, 1), ref(bereishit, 1, 27)),
        _,
        _
    ).

%% Common principle extraction
test(common_principle_from_list, [nondet]) :-
    common_principle(
        [ref(bereishit, 1, 1), ref(bereishit, 1, 27)],
        bet_resh_aleph,
        _
    ).

:- end_tests(binyan_av_tests).


%% ============================================================
%% RULES 5-8: KLAL UFRAT
%% ============================================================

:- begin_tests(klal_ufrat_tests).

%% Rule 5: General then particular narrows
test(klal_ufrat_narrows) :-
    klal_ufrat(
        general(fruit_trees),
        particular([olive, grape]),
        narrowed_to([olive, grape], from(fruit_trees))
    ).

%% Rule 6: Particular then general expands
test(prat_uklal_expands) :-
    prat_uklal(
        particular([sheep, cattle]),
        general(all_livestock),
        expanded_to(all_livestock, including([sheep, cattle]))
    ).

%% Rule 7: General-particular-general yields similar
test(klal_ufrat_uklal_similar) :-
    klal_ufrat_uklal(
        general(all_damage),
        particular([ox_damage, pit_damage, fire_damage]),
        general(all_damage),
        similar_to([ox_damage, pit_damage, fire_damage],
                   within(all_damage, negligence_based_damage))
    ).

%% Generic klal ufrat
test(generic_klal_ufrat) :-
    klal_ufrat(
        general(any_category),
        particular(specific_thing),
        narrowed_to(specific_thing, from(any_category))
    ).

%% Scope results
test(scope_narrowed) :-
    scope_result(klal_then_prat, narrowed).

test(scope_expanded) :-
    scope_result(prat_then_klal, expanded).

test(scope_similar) :-
    scope_result(klal_prat_klal, similar).

:- end_tests(klal_ufrat_tests).


%% ============================================================
%% RULES 9-11: DAVAR YATZA
%% ============================================================

:- begin_tests(davar_yatza_tests).

%% Rule 9: Exception teaches about the general
test(exception_teaches_general) :-
    davar_yatza_llamed(
        exception(chatat, blood_sprinkling_north),
        general(all_offerings),
        teaches(blood_sprinkling_north, applies_to_all(all_offerings))
    ).

%% Generic rule 9
test(generic_exception_teaches) :-
    davar_yatza_llamed(
        exception(item, some_law),
        general(category),
        teaches(some_law, applies_to_all(category))
    ).

%% Rule 10: Same type reduces severity
test(same_type_reduces) :-
    davar_yatza_toan_echad(
        exception(item, shared_law),
        general(category, shared_law),
        reduces(shared_law, for(category), because(item))
    ).

%% Rule 11: Different type creates dual application
test(different_type_dual_rules) :-
    davar_yatza_toan_acher(
        exception(metzora, outside_camp_procedure),
        general(tumah, standard_purification),
        dual_rules(metzora, follows(standard_purification), and(outside_camp_procedure))
    ).

:- end_tests(davar_yatza_tests).


%% ============================================================
%% RULE 12: LAMED INYAN
%% ============================================================

:- begin_tests(lamed_inyan_tests).

%% "Lo tignov" in context of capital crimes = kidnapping
test(lo_tignov_kidnapping) :-
    lamed_me_inyano(
        ref(shemot, 20, 15),
        context(capital_crimes_sequence),
        meaning(lo_tignov, refers_to(kidnapping), not(ordinary_theft))
    ).

%% Context from surrounding verses (requires prev and next verse to exist)
test(context_from_surrounding, [nondet]) :-
    lamed_me_inyano(
        ref(shemot, 20, 14),
        context(ref(shemot, 20, 13), ref(shemot, 20, 15)),
        meaning_from(context, ref(shemot, 20, 14))
    ).

%% Lamed misofo: conclusion clarifies ambiguous topic
test(conclusion_clarifies) :-
    lamed_misofo(
        ambiguous(topic),
        concludes_with(clarification),
        meaning(topic, clarified_by(clarification))
    ).

%% Unified context_determines_meaning
test(context_determines_surrounding, [nondet]) :-
    context_determines_meaning(
        ref(shemot, 20, 15),
        surrounding,
        meaning(lo_tignov, refers_to(kidnapping), not(ordinary_theft))
    ).

:- end_tests(lamed_inyan_tests).


%% ============================================================
%% RULE 13: SHNEI KETUVIM
%% ============================================================

:- begin_tests(shnei_ketuvim_tests).

%% Domains in tension
test(judgment_mercy_tension) :-
    domains_in_tension(judgment, mercy).

test(mercy_judgment_tension) :-
    domains_in_tension(mercy, judgment).

test(holiness_transgression_tension) :-
    domains_in_tension(holiness, transgression).

%% Two verses with roots in opposing domains contradict
test(verses_contradict_detection, [nondet]) :-
    verses_contradict(V1, V2, domain_conflict(_, _)),
    V1 \= V2.

%% Resolving verse shares roots with both
test(resolving_verse_found, [nondet]) :-
    resolving_verse(V1, V2, V3),
    V1 \= V3,
    V2 \= V3.

%% Shnei ketuvim unified interface — harmonized case
test(shnei_ketuvim_harmonized, [nondet]) :-
    shnei_ketuvim(
        contradicting(V1, V2),
        harmonized_reading(V1, V2, _V3),
        reasoning(V1, contradicts(V2), resolved_by(_)),
        _
    ).

:- end_tests(shnei_ketuvim_tests).