%% challenge.pl — Kushya generation.
%%
%% Architecture §3.4:
%%   challenge(Interpretation, Challenge) :-
%%       mitzvah(_, _, _, _) = Contradicting,
%%       contradicts(Interpretation, Contradicting),
%%       Challenge = kushya(Contradicting, Interpretation).
%%
%% A kushya is a challenge grounded in Torah text.
%% It identifies a tension between the proposed interpretation
%% and another part of the specification.
%%
%% The challenge is a question, not a refutation.
%% It says: "But what about THIS verse/mitzvah?"
%%
%% Each kushya carries a grounding_type — Shemot 33:23:
%%   v'raita et ACHORAI u'fanai lo yera'u.
%%   "You will see My back, but My face shall not be seen."
%%
%% achorai = effects directly observable in L1 text
%%   (mitzvah_tension, shnei_ketuvim_tension, condition_tension)
%% panim = intention inferred/attributed by the system
%%   (domain_tension, kal_vachomer_tension)

:- module(challenge, [
    challenge/2,
    find_contradiction/3,
    contradicts/2,
    challenge_strength/2,
    grounding_type/2
]).

:- use_module('../specification/mitzvot').
:- use_module('../specification/torah_text').
:- use_module('../specification/relationships').
:- use_module('../specification/root_meanings').
:- use_module('../middot/kal_vachomer').
:- use_module('../middot/shnei_ketuvim').

%% ============================================================
%% CHALLENGE GENERATION
%% ============================================================

%% Generate a challenge to an interpretation.
%% A challenge consists of:
%%   kushya(Contradicting, CaseRef, Strength, GroundingType)
%%   - Contradicting: the mitzvah or verse that creates tension
%%   - CaseRef: the interpretation being challenged
%%   - Strength: strong | moderate | weak
%%   - GroundingType: achorai | panim (Shemot 33:23)
challenge(interpretation(CaseRef, Mitzvot, Verses, _Reading, _Confidence, _CouplingTrace), Challenge) :-
    find_contradiction(Mitzvot, Verses, Contradicting),
    challenge_strength(Contradicting, Strength),
    grounding_type(Contradicting, GType),
    Challenge = kushya(Contradicting, CaseRef, Strength, GType).

%% ============================================================
%% FIND CONTRADICTIONS
%% ============================================================

%% Strategy 1: Find a mitzvah that conflicts with one in the interpretation
find_contradiction(Mitzvot, _Verses, contradiction(mitzvah_tension, ID1, ID2, Desc)) :-
    member(mitzvah(ID1, _, _, _), Mitzvot),
    mitzvah_conflicts_with(ID1, ID2, Desc).

%% Strategy 2: Find a verse with a root in a conflicting domain
find_contradiction(_Mitzvot, Verses, contradiction(domain_tension, Root, Domain1, Domain2)) :-
    member(verse_ref(Book, Ch, Vs, _), Verses),
    verse(Book, Ch, Vs, VerseRoots, _),
    member(Root, VerseRoots),
    root_domain(Root, Domain1),
    root_domain(OtherRoot, Domain2),
    Domain1 \= Domain2,
    domains_in_tension(Domain1, Domain2),
    member(OtherRoot, VerseRoots).

%% Strategy 3: Find a mitzvah whose condition conflicts with the case context
find_contradiction(Mitzvot, _Verses, contradiction(condition_tension, ID, Action, Cond)) :-
    member(mitzvah(ID, _, Action, when(Cond)), Mitzvot),
    condition_creates_tension(Cond).

%% Strategy 4: Kal vachomer — if a law applies in the minor case,
%% challenge interpretations that don't account for the major case
find_contradiction(Mitzvot, _Verses, contradiction(kal_vachomer_tension, MinorDomain, MajorDomain, Law)) :-
    member(mitzvah(_, _, Law, _), Mitzvot),
    mitzvah_domain_for_action(Law, MinorDomain),
    is_more_stringent(MinorDomain, MajorDomain).

%% Strategy 5: Shnei ketuvim — two verses in the interpretation's
%% grounding contradict each other and no resolution is offered
find_contradiction(_Mitzvot, Verses, contradiction(shnei_ketuvim_tension, Ref1, Ref2, Tension)) :-
    member(verse_ref(B1, C1, Vs1, _), Verses),
    member(verse_ref(B2, C2, Vs2, _), Verses),
    Ref1 = ref(B1,C1,Vs1),
    Ref2 = ref(B2,C2,Vs2),
    Ref1 \= Ref2,
    verses_contradict(Ref1, Ref2, Tension).

%% ============================================================
%% TENSION DETECTION
%% ============================================================

%% contradicts/2 — does a source contradict an interpretation?
%% This is the core logic: given an interpretation's grounding,
%% does some other part of Torah create a tension?
contradicts(interpretation(_, Mitzvot, _, _, _, _), Source) :-
    find_contradiction(Mitzvot, [], Source).

%% Domains that are inherently in tension
domains_in_tension(judgment, mercy).
domains_in_tension(mercy, judgment).
domains_in_tension(holiness, transgression).
domains_in_tension(transgression, holiness).
domains_in_tension(death, life).
domains_in_tension(life, death).
domains_in_tension(authority, service).
domains_in_tension(service, authority).

%% Conditions that create tension (they limit universality)
condition_creates_tension(seventh_day).        % Shabbat limits action
condition_creates_tension(capital_case).        % Higher standard of evidence
condition_creates_tension(pursuit_in_progress). % Time pressure
condition_creates_tension(court_deliberation).  % Procedural constraints

%% ============================================================
%% CHALLENGE STRENGTH
%% ============================================================

%% Assess how strong a challenge is
challenge_strength(contradiction(mitzvah_tension, _, _, _), strong).
challenge_strength(contradiction(domain_tension, _, _, _), moderate).
challenge_strength(contradiction(condition_tension, _, _, _), weak).
challenge_strength(contradiction(kal_vachomer_tension, _, _, _), strong).
challenge_strength(contradiction(shnei_ketuvim_tension, _, _, _), strong).

%% ============================================================
%% GROUNDING TYPE — Shemot 33:23
%% ============================================================

%% Achorai: directly observable in L1 text.
%% The tension is stated, not inferred.
grounding_type(contradiction(mitzvah_tension, _, _, _), achorai).
grounding_type(contradiction(condition_tension, _, _, _), achorai).
grounding_type(contradiction(shnei_ketuvim_tension, _, _, _), achorai).

%% Panim: inferred by the system.
%% The tension is attributed, not directly stated in text.
grounding_type(contradiction(domain_tension, _, _, _), panim).
grounding_type(contradiction(kal_vachomer_tension, _, _, _), panim).

%% ============================================================
%% HELPERS
%% ============================================================

%% Map a mitzvah action to its domain (via relationships module)
mitzvah_domain_for_action(Action, Domain) :-
    action_domain(Action, Domain).