%% phase3_verify_test.pl — Phase 3 verification tests.
%%
%% Architecture §4, Step 20: Verify the system can:
%%   1. Deliberate a case through full dialectical process
%%   2. Produce majority decision with preserved dissent
%%   3. Apply middot-based reasoning
%%   4. Run diagnostic protocol
%%   5. Query 613 mitzvot by domain, condition, category

:- use_module(library(plunit)).
:- use_module('../src/reasoning/interpret').
:- use_module('../src/reasoning/challenge').
:- use_module('../src/reasoning/resolve').
:- use_module('../src/reasoning/teiku').
:- use_module('../src/specification/mitzvot').
:- use_module('../src/specification/torah_text').
:- use_module('../src/specification/relationships').
:- use_module('../src/specification/root_meanings').
:- use_module('../src/middot/middot').
:- use_module('../src/middot/kal_vachomer').
:- use_module('../src/middot/gezerah_shavah').
:- use_module('../src/middot/shnei_ketuvim').
:- use_module('../src/diagnostic/tzaraat').
:- use_module('../src/diagnostic/inspection').
:- use_module('../src/diagnostic/diagnosis').

%% ============================================================
%% STEP 20: FULL DELIBERATION CYCLE
%% ============================================================

:- begin_tests(full_deliberation).

%% A case about holiness can be interpreted
test(interpret_holiness, [nondet]) :-
    Case = case(verify_holiness, holiness, [qof_dalet_shin],
                'What does it mean to be holy?'),
    interpret(Case, interpretation(verify_holiness, _, _, _, _, _)).

%% A case about judgment produces a challenge
test(judgment_case_challenged, [nondet]) :-
    Case = case(verify_judgment, judgment, [shin_pe_tet, tzade_dalet_qof],
                'How to judge righteously?'),
    interpret(Case, Interpretation),
    challenge(Interpretation, kushya(_, _, _, _)).

%% A case can go through full resolution
test(full_resolve_cycle, [nondet]) :-
    Case = case(verify_resolve, holiness, [qof_dalet_shin],
                'What is the holiness obligation?'),
    resolve(Case, Resolution),
    (   Resolution = accepted(_)
    ;   Resolution = challenged(_, _)
    ;   Resolution = synthesized(_, _, _)
    ;   Resolution = teiku(_)
    ).

%% Teiku count is tracked
test(teiku_tracking) :-
    teiku_count(Count),
    integer(Count).

:- end_tests(full_deliberation).


%% ============================================================
%% STEP 20: 613 MITZVOT QUERYABILITY
%% ============================================================

:- begin_tests(mitzvot_queryability).

%% Query all mitzvot in a domain
test(query_by_domain, [nondet]) :-
    domain_mitzvot(judgment, Mitzvot),
    Mitzvot \= [].

%% Query mitzvot by category
test(query_positives) :-
    findall(ID, mitzvah(ID, positive, _, _), IDs),
    length(IDs, 248).

test(query_prohibitions) :-
    findall(ID, mitzvah(ID, prohibition, _, _), IDs),
    length(IDs, 365).

%% Query conditional mitzvot
test(query_conditional, [nondet]) :-
    mitzvah(_, _, _, when(_)).

%% Query unconditional mitzvot
test(query_unconditional, [nondet]) :-
    mitzvah(_, _, _, always).

%% Mitzvah source grounding
test(sources_exist) :-
    findall(ID, mitzvah_source(ID, _), IDs),
    length(IDs, Count),
    Count > 50.  %% At least 50 mitzvot have sources

%% Complementary pairs exist
test(complementary_pairs) :-
    findall(pair(A,B), complementary_mitzvot(A, B), Pairs),
    length(Pairs, Count),
    Count >= 16.  %% 8 pairs * 2 directions

%% Tension pairs exist
test(tension_pairs) :-
    findall(pair(A,B), mitzvah_conflicts_with(A, B, _), Pairs),
    length(Pairs, Count),
    Count >= 8.

:- end_tests(mitzvot_queryability).


%% ============================================================
%% STEP 20: MIDDOT APPLICATION
%% ============================================================

:- begin_tests(middot_application).

%% All 13 middot are enumerated
test(all_13_enumerated) :-
    all_middot(M),
    length(M, 13).

%% Kal vachomer produces derivation
test(kal_vachomer_derivation) :-
    kal_vachomer(shabbat_rest, festival_rest, Derived, definite),
    Derived = derived(rest_obligation, from(shabbat), to(festival), kal_vachomer).

%% Gezerah shavah finds verbal link
test(gezerah_shavah_link) :-
    gezerah_shavah(shabbat_keeping, pesach_keeping, _, shin_mem_resh).

%% Gezerah shavah from Torah text
test(dynamic_verbal_link, [nondet]) :-
    shared_keyword(ref(bereishit, 1, 1), ref(bereishit, 1, 27), bet_resh_aleph).

%% Shnei ketuvim: domain tensions known
test(domain_tensions_known) :-
    domains_in_tension(judgment, mercy),
    domains_in_tension(holiness, transgression).

%% Challenge module has middot-based strategies
test(challenge_has_kal_vachomer_strategy) :-
    challenge_strength(contradiction(kal_vachomer_tension, _, _, _), strong).

test(challenge_has_shnei_ketuvim_strategy) :-
    challenge_strength(contradiction(shnei_ketuvim_tension, _, _, _), strong).

:- end_tests(middot_application).


%% ============================================================
%% STEP 20: TZARA'AT DIAGNOSTIC
%% ============================================================

:- begin_tests(tzaraat_diagnostic).

%% Clean input passes
test(clean_input_passes) :-
    diagnose(input(declared, [visible], within_bounds, []), declared_tahor).

%% Impure input rejected
test(impure_input_rejected) :-
    diagnose(input(undeclared, [visible], within_bounds, []), confirmed_tamei).

%% Ambiguous input quarantined
test(ambiguous_input_quarantined) :-
    diagnose(input(declared, [hidden], within_bounds, []), requires_quarantine(quarantine_1)).

%% The paradox: full visibility = purity
test(full_visibility_paradox) :-
    diagnose(
        input(undeclared, [hidden], exceeds_bounds, [leaks_implementation]),
        fully_visible_tahor
    ).

%% 8 diagnosis states
test(eight_states) :-
    findall(S, diagnosis_state(S), States),
    length(States, 8).

:- end_tests(tzaraat_diagnostic).


%% ============================================================
%% STEP 20: ROOT AND VERSE QUERYABILITY
%% ============================================================

:- begin_tests(root_verse_queries).

%% All semantic domains
test(domains_exist) :-
    all_domains(Domains),
    length(Domains, Count),
    Count >= 10.

%% Roots in a domain
test(roots_in_holiness, [nondet]) :-
    roots_in_domain(holiness, Roots),
    Roots \= [].

%% Verses mentioning a root
test(verses_with_kadosh, [nondet]) :-
    verses_mentioning_root(qof_dalet_shin, Verses),
    Verses \= [].

%% Verse roots can be retrieved
test(verse_roots_retrieved) :-
    verse_roots(bereishit, 1, 1, Roots),
    member(bet_resh_aleph, Roots).

:- end_tests(root_verse_queries).