logicaffeine_language/parser/

clause.rs

//! Clause-level parsing: sentences, conditionals, conjunctions, and relative clauses.
//!
//! This module handles the top-level sentence structures including:
//!
//! - **Simple sentences**: Subject-verb-object patterns
//! - **Conditionals**: "If P then Q" with DRS scope handling
//! - **Counterfactuals**: "If P were/had, Q would" (subjunctive)
//! - **Disjunctions**: "Either P or Q", "P or Q"
//! - **Conjunctions**: "P and Q"
//! - **Relative clauses**: "who/that/which" attaching to noun phrases
//! - **VP ellipsis**: "John ran and Mary did too"
//!
//! The [`ClauseParsing`] trait defines the interface implemented by [`Parser`].

use super::modal::ModalParsing;
use super::noun::NounParsing;
use super::pragmatics::PragmaticsParsing;
use super::quantifier::QuantifierParsing;
use super::question::QuestionParsing;
use super::verb::LogicVerbParsing;
use super::{EventTemplate, ParseResult, Parser};
use crate::ast::{AspectOperator, LogicExpr, NeoEventData, NounPhrase, QuantifierKind, TemporalOperator, Term, ThematicRole};
use crate::lexer::Lexer;
use crate::lexicon::Time;
use crate::drs::{BoxType, Gender, Number};
use super::ParserMode;
use crate::error::{ParseError, ParseErrorKind};
use logicaffeine_base::Symbol;
use crate::lexicon::Definiteness;
use crate::token::TokenType;

/// Trait for parsing clause-level structures.
///
/// Defines methods for parsing sentences, conditionals, conjunctions,
/// and other clause-level constructs.
pub trait ClauseParsing<'a, 'ctx, 'int> {
    /// Parses a complete sentence, handling imperatives, ellipsis, and questions.
    fn parse_sentence(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "if P then Q" conditionals with DRS scope handling.
    fn parse_conditional(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "either P or Q" exclusive disjunctions.
    fn parse_either_or(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "P or Q" disjunctions.
    fn parse_disjunction(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "P and Q" conjunctions with scope coordination.
    fn parse_conjunction(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "who/that/which" relative clauses attaching to noun phrases.
    fn parse_relative_clause(&mut self, gap_var: Symbol) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses a clause with a gap filled by borrowed verb (for VP coordination).
    fn parse_gapped_clause(&mut self, borrowed_verb: Symbol) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "if P were/had" counterfactual antecedent (subjunctive).
    fn parse_counterfactual_antecedent(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Parses "Q would" counterfactual consequent.
    fn parse_counterfactual_consequent(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
    /// Checks if current token is a wh-word (who, what, which, etc.).
    fn check_wh_word(&self) -> bool;
    /// Returns true if parsing a counterfactual context.
    fn is_counterfactual_context(&self) -> bool;
    /// Returns true if expression is a complete clause.
    fn is_complete_clause(&self, expr: &LogicExpr<'a>) -> bool;
    /// Extracts the main verb from an expression.
    fn extract_verb_from_expr(&self, expr: &LogicExpr<'a>) -> Option<Symbol>;
    /// Attempts to parse VP ellipsis ("Mary did too").
    fn try_parse_ellipsis(&mut self) -> Option<ParseResult<&'a LogicExpr<'a>>>;
    /// Checks for ellipsis auxiliary (did, does, can, etc.).
    fn check_ellipsis_auxiliary(&self) -> bool;
    /// Checks for ellipsis terminator (too, also, as well).
    fn check_ellipsis_terminator(&self) -> bool;
}

impl<'a, 'ctx, 'int> ClauseParsing<'a, 'ctx, 'int> for Parser<'a, 'ctx, 'int> {
    fn parse_sentence(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        // In imperative mode, handle Let statements by converting to LogicExpr
        // This supports declarative parser being called after process_block_headers()
        // Let x is/= value -> returns the value expression (the test just checks parsing succeeds)
        if self.mode == ParserMode::Imperative && self.check(&TokenType::Let) {
            self.advance(); // consume "Let"
            let _var = self.expect_identifier()?;
            // Accept "is", "be", "=" as assignment operators
            if self.check(&TokenType::Is) || self.check(&TokenType::Be) || self.check(&TokenType::Equals) || self.check(&TokenType::Identity) || self.check(&TokenType::Assign) {
                self.advance(); // consume the operator
            }
            // Parse the value and return it (test just checks parsing succeeds)
            return self.parse_disjunction();
        }

        // Check for ellipsis pattern: "Mary does too." / "Mary can too."
        if let Some(result) = self.try_parse_ellipsis() {
            return result;
        }

        if self.check_verb() {
            let verb_pos = self.current;
            let mut temp_pos = self.current + 1;
            while temp_pos < self.tokens.len() {
                if matches!(self.tokens[temp_pos].kind, TokenType::Exclamation) {
                    self.current = verb_pos;
                    let verb = self.consume_verb();
                    while !matches!(self.peek().kind, TokenType::Exclamation | TokenType::EOF) {
                        self.advance();
                    }
                    if self.check(&TokenType::Exclamation) {
                        self.advance();
                    }
                    let addressee = self.interner.intern("addressee");
                    let action = self.ctx.exprs.alloc(LogicExpr::Predicate {
                        name: verb,
                        args: self.ctx.terms.alloc_slice([Term::Variable(addressee)]),
                        world: None,
                    });
                    return Ok(self.ctx.exprs.alloc(LogicExpr::Imperative { action }));
                }
                if matches!(self.tokens[temp_pos].kind, TokenType::Period | TokenType::EOF) {
                    break;
                }
                temp_pos += 1;
            }
        }

        // "While X, Y" as temporal duration subordinator
        // Duration semantics: Y holds for the entire interval where X is true.
        // Lowered as implication checked globally: G(X → Y)
        if self.check(&TokenType::While) {
            self.advance(); // consume "While"
            let condition = self.parse_sentence()?;
            if self.check(&TokenType::Comma) {
                self.advance();
            }
            let consequent = self.parse_sentence()?;
            return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                left: condition,
                op: TokenType::Implies,
                right: consequent,
            }));
        }

        // "When X, Y" as temporal subordinator (before wh-question check)
        // Disambiguate: subordinator has comma-separated clauses, question does not
        if self.check(&TokenType::When) {
            let saved = self.current;
            let mut found_comma = false;
            for i in (self.current + 1)..self.tokens.len() {
                match &self.tokens[i].kind {
                    TokenType::Comma => { found_comma = true; break; }
                    TokenType::Period => break,
                    _ => {}
                }
            }
            if found_comma {
                self.advance(); // consume "When"
                let condition = self.parse_sentence()?;
                if self.check(&TokenType::Comma) {
                    self.advance();
                }
                let consequent = self.parse_sentence()?;
                return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                    left: condition,
                    op: TokenType::Implies,
                    right: consequent,
                }));
            }
            self.current = saved;
        }

        // "Whenever X, Y" → same as "When X, Y"
        if self.check_content_word() {
            let word = self.interner.resolve(self.peek().lexeme).to_string();
            if word == "Whenever" || word == "whenever" {
                self.advance(); // consume "Whenever"
                let condition = self.parse_sentence()?;
                if self.check(&TokenType::Comma) {
                    self.advance();
                }
                let consequent = self.parse_sentence()?;
                return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                    left: condition,
                    op: TokenType::Implies,
                    right: consequent,
                }));
            }
        }

        if self.check_wh_word() {
            return self.parse_wh_question();
        }

        if self.check(&TokenType::Does)
            || self.check(&TokenType::Do)
            || self.check(&TokenType::Is)
            || self.check(&TokenType::Are)
            || self.check(&TokenType::Was)
            || self.check(&TokenType::Were)
            || self.check(&TokenType::Would)
            || self.check(&TokenType::Could)
            || self.check(&TokenType::Can)
        {
            return self.parse_yes_no_question();
        }

        if self.match_token(&[TokenType::If]) {
            return self.parse_conditional();
        }

        // Handle "Either X or Y" disjunction
        // Special case: "Either NP1 or NP2 is/are PRED" should apply PRED to both
        if self.match_token(&[TokenType::Either]) {
            return self.parse_either_or();
        }

        if self.check_modal() {
            self.advance();
            return self.parse_modal();
        }

        if self.match_token(&[TokenType::Not]) {
            self.negative_depth += 1;
            let inner = self.parse_sentence()?;
            self.negative_depth -= 1;
            return Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
                op: TokenType::Not,
                operand: inner,
            }));
        }

        // "not both every request is valid and every grant is valid" → ¬(X ∧ Y)
        // Only triggers for clausal conjunction: "both" + quantifier/determiner
        // NOT for conjoined NP: "both Socrates and Plato are men"
        if self.check(&TokenType::Both) {
            // Peek at token after "both" — if it's a quantifier, this is clausal
            let next_is_clausal = if self.current + 1 < self.tokens.len() {
                matches!(self.tokens[self.current + 1].kind,
                    TokenType::All | TokenType::No | TokenType::Some | TokenType::Any
                    | TokenType::Most | TokenType::Few | TokenType::Many
                    | TokenType::Cardinal(_) | TokenType::AtLeast(_) | TokenType::AtMost(_)
                    | TokenType::Article(_)
                )
            } else {
                false
            };
            if next_is_clausal {
                self.advance(); // consume "both"
                let first = self.parse_atom()?;
                if self.check(&TokenType::And) {
                    self.advance(); // consume "and"
                }
                let second = self.parse_atom()?;
                return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                    left: first,
                    op: TokenType::And,
                    right: second,
                }));
            }
        }

        // Sentence-initial temporal operators for hardware verification:
        // "Always, P" → Temporal { Always, P }
        // "Eventually, P" → Temporal { Eventually, P }
        // "Next, P" → Temporal { Next, P }
        // "Never P" → Temporal { Always, ¬P }
        {
            let temporal_op = match &self.peek().kind {
                TokenType::Adverb(sym) | TokenType::ScopalAdverb(sym) | TokenType::TemporalAdverb(sym) => {
                    let resolved = self.interner.resolve(*sym).to_string();
                    match resolved.as_str() {
                        "Always" => Some(crate::ast::logic::TemporalOperator::Always),
                        "Eventually" => Some(crate::ast::logic::TemporalOperator::Eventually),
                        "Next" => Some(crate::ast::logic::TemporalOperator::Next),
                        _ => None,
                    }
                }
                // Handle "next" as an adjective token (common fallback)
                TokenType::Adjective(sym) => {
                    let resolved = self.interner.resolve(*sym).to_string();
                    if resolved == "Next" {
                        Some(crate::ast::logic::TemporalOperator::Next)
                    } else {
                        None
                    }
                }
                _ => None,
            };
            if let Some(op) = temporal_op {
                self.advance(); // consume the token
                // Optionally consume comma: "Always, P"
                if self.check(&TokenType::Comma) {
                    self.advance();
                }
                let body = self.parse_sentence()?;
                return Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
                    operator: op,
                    body,
                }));
            }
        }
        // "Never P" → G(¬P): Always { Not { P } }
        if self.check(&TokenType::Never) {
            self.advance(); // consume "Never"
            // Optionally consume comma
            if self.check(&TokenType::Comma) {
                self.advance();
            }
            let body = self.parse_sentence()?;
            let negated = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
                op: TokenType::Not,
                operand: body,
            });
            return Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
                operator: crate::ast::logic::TemporalOperator::Always,
                body: negated,
            }));
        }

        // "After X, Y" → X → Y (temporal sequence)
        // "Before X, Y" → Y → X
        // Handles both "After reset is deasserted, ..." (full clause)
        // and "After request, ..." (bare signal/event noun)
        if self.check_preposition_is("after") || self.check_preposition_is("After") {
            self.advance(); // consume "after"

            // Check for bare noun/signal + comma pattern: "After request, ..."
            // Also handle Performative tokens (e.g., "request" when not after determiner)
            let is_bare_noun_comma = self.current + 1 < self.tokens.len()
                && matches!(self.tokens[self.current + 1].kind, TokenType::Comma)
                && (self.check_content_word()
                    || matches!(self.peek().kind, TokenType::Performative(_)));
            let antecedent = if is_bare_noun_comma {
                let noun = match self.advance().kind.clone() {
                    TokenType::Performative(s) => s,
                    TokenType::Noun(s) | TokenType::Adjective(s) | TokenType::ProperName(s) => s,
                    TokenType::Verb { lemma, .. } => lemma,
                    _ => return Err(crate::error::ParseError {
                        kind: crate::error::ParseErrorKind::ExpectedContentWord { found: self.peek().kind.clone() },
                        span: self.current_span(),
                    }),
                };
                self.ctx.exprs.alloc(LogicExpr::Atom(noun))
            } else {
                self.parse_sentence()?
            };

            if self.check(&TokenType::Comma) {
                self.advance();
            }
            let consequent = self.parse_sentence()?;
            let consequent = self.try_wrap_bounded_delay(consequent);
            return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                left: antecedent,
                op: TokenType::Implies,
                right: consequent,
            }));
        }
        if self.check_preposition_is("before") || self.check_preposition_is("Before") {
            self.advance(); // consume "before"
            let first_clause = self.parse_sentence()?;
            if self.check(&TokenType::Comma) {
                self.advance();
            }
            let second_clause = self.parse_sentence()?;
            return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                left: second_clause,
                op: TokenType::Implies,
                right: first_clause,
            }));
        }

        self.parse_disjunction()
    }

    fn check_wh_word(&self) -> bool {
        if matches!(
            self.peek().kind,
            TokenType::Who
                | TokenType::What
                | TokenType::Where
                | TokenType::When
                | TokenType::Why
        ) {
            return true;
        }
        if self.check_preposition() && self.current + 1 < self.tokens.len() {
            matches!(
                self.tokens[self.current + 1].kind,
                TokenType::Who
                    | TokenType::What
                    | TokenType::Where
                    | TokenType::When
                    | TokenType::Why
            )
        } else {
            false
        }
    }

    fn parse_conditional(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        let is_counterfactual = self.is_counterfactual_context();

        // Enter DRS antecedent box - indefinites here get universal force
        self.drs.enter_box(BoxType::ConditionalAntecedent);
        let mut antecedent = self.parse_counterfactual_antecedent()?;

        // Handle conjunction of clauses in antecedent: "If X is Y and Z is W, ..."
        while self.check(&TokenType::And) {
            self.advance(); // consume "and"
            let second = self.parse_counterfactual_antecedent()?;
            antecedent = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                left: antecedent,
                op: TokenType::And,
                right: second,
            });
        }
        self.drs.exit_box();

        if self.check(&TokenType::Comma) {
            self.advance();
        }

        if self.check(&TokenType::Then) {
            self.advance();
        }

        // Enter DRS consequent box - can access antecedent referents
        self.drs.enter_box(BoxType::ConditionalConsequent);
        let consequent = self.parse_counterfactual_consequent()?;
        self.drs.exit_box();

        // Get DRS referents that need universal quantification
        let universal_refs = self.drs.get_universal_referents();

        // Build the conditional expression
        let conditional = if is_counterfactual {
            self.ctx.exprs.alloc(LogicExpr::Counterfactual {
                antecedent,
                consequent,
            })
        } else {
            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                left: antecedent,
                op: TokenType::If,
                right: consequent,
            })
        };

        // Wrap with universal quantifiers for DRS referents
        let mut result = conditional;
        for var in universal_refs.into_iter().rev() {
            result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
                kind: QuantifierKind::Universal,
                variable: var,
                body: result,
                island_id: self.current_island,
            });
        }

        Ok(result)
    }

    /// Parse "Either NP1 or NP2 is/are PRED" or "Either S1 or S2"
    ///
    /// Handles coordination: "Either Alice or Bob is guilty" should become
    /// guilty(Alice) ∨ guilty(Bob), not Alice ∨ guilty(Bob)
    fn parse_either_or(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        // Save position for potential backtracking
        let start_pos = self.current;

        // Try to parse as "Either NP1 or NP2 VP"
        // First, try to parse just a proper name (not a full clause)
        if let TokenType::ProperName(name1) = self.peek().kind {
            self.advance(); // consume first proper name

            if self.check(&TokenType::Or) {
                self.advance(); // consume "or"

                if let TokenType::ProperName(name2) = self.peek().kind {
                    self.advance(); // consume second proper name

                    // Check for shared predicate: "is/are ADJECTIVE"
                    let is_copula = matches!(
                        self.peek().kind,
                        TokenType::Is | TokenType::Are | TokenType::Was | TokenType::Were
                    );
                    if is_copula {
                        self.advance(); // consume copula

                        // Check for negation: "is not"
                        let is_negated = self.match_token(&[TokenType::Not]);

                        // Try to get an adjective
                        if let TokenType::Adjective(adj) = self.peek().kind {
                            self.advance(); // consume adjective

                            // Create predicate for each NP
                            let pred1 = self.ctx.exprs.alloc(LogicExpr::Predicate {
                                name: adj,
                                args: self.ctx.terms.alloc_slice(vec![
                                    Term::Constant(name1)
                                ]),
                                world: None,
                            });
                            let pred2 = self.ctx.exprs.alloc(LogicExpr::Predicate {
                                name: adj,
                                args: self.ctx.terms.alloc_slice(vec![
                                    Term::Constant(name2)
                                ]),
                                world: None,
                            });

                            // Apply negation if needed
                            let left = if is_negated {
                                self.ctx.exprs.alloc(LogicExpr::UnaryOp {
                                    op: TokenType::Not,
                                    operand: pred1,
                                })
                            } else {
                                pred1
                            };
                            let right = if is_negated {
                                self.ctx.exprs.alloc(LogicExpr::UnaryOp {
                                    op: TokenType::Not,
                                    operand: pred2,
                                })
                            } else {
                                pred2
                            };

                            return Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                                left,
                                op: TokenType::Or,
                                right,
                            }));
                        }
                    }
                }
            }

            // Backtrack if the special case didn't match
            self.current = start_pos;
        }

        // Fall back to general disjunction parsing
        // Enter disjunct box for left side - referents here are inaccessible outward
        self.drs.enter_box(BoxType::Disjunct);
        let left = self.parse_conjunction()?;
        self.drs.exit_box();

        if !self.check(&TokenType::Or) {
            return Err(ParseError {
                kind: ParseErrorKind::ExpectedKeyword { keyword: "or".to_string() },
                span: self.current_span(),
            });
        }
        self.advance(); // consume "or"

        // Enter disjunct box for right side - referents here are also inaccessible outward
        self.drs.enter_box(BoxType::Disjunct);
        let right = self.parse_conjunction()?;
        self.drs.exit_box();

        Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
            left,
            op: TokenType::Or,
            right,
        }))
    }

    fn is_counterfactual_context(&self) -> bool {
        for i in 0..5 {
            if self.current + i >= self.tokens.len() {
                break;
            }
            let token = &self.tokens[self.current + i];
            if matches!(token.kind, TokenType::Were | TokenType::Had) {
                return true;
            }
            if matches!(token.kind, TokenType::Comma | TokenType::Period) {
                break;
            }
        }
        false
    }

    fn parse_counterfactual_antecedent(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        let unknown = self.interner.intern("?");
        if self.check_content_word() || self.check_pronoun() || self.check_article() {
            // Weather verb detection: "if it rains" → ∃e(Rain(e))
            // Must check BEFORE pronoun resolution since "it" would resolve to "?"
            if self.check_pronoun() {
                let token = self.peek();
                let token_text = self.interner.resolve(token.lexeme);
                if token_text.eq_ignore_ascii_case("it") {
                    // Look ahead for weather verb: "it rains" or "it is raining"
                    if self.current + 1 < self.tokens.len() {
                        // Check for "it + verb" pattern
                        if let TokenType::Verb { lemma, time, .. } = &self.tokens[self.current + 1].kind {
                            let lemma_str = self.interner.resolve(*lemma);
                            if Lexer::is_weather_verb(lemma_str) {
                                let verb = *lemma;
                                let verb_time = *time;
                                self.advance(); // consume "it"
                                self.advance(); // consume weather verb

                                let event_var = self.get_event_var();

                                // Weather verbs are impersonal - no pronoun resolution needed
                                // Event var gets universal force from transpiler when suppress_existential=true
                                let suppress_existential = self.drs.in_conditional_antecedent();

                                let mut result: &'a LogicExpr<'a> = self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
                                    event_var,
                                    verb,
                                    roles: self.ctx.roles.alloc_slice(vec![]),
                                    modifiers: self.ctx.syms.alloc_slice(vec![]),
                                    suppress_existential,
                                    world: None,
                                })));

                                // Handle coordinated weather verbs: "rains and thunders" or "rains or thunders"
                                // SHARE the same event_var for all coordinated verbs
                                while self.check(&TokenType::And) || self.check(&TokenType::Or) {
                                    let is_disjunction = self.check(&TokenType::Or);
                                    self.advance(); // consume "and" or "or"

                                    if let TokenType::Verb { lemma: lemma2, .. } = &self.peek().kind.clone() {
                                        let lemma2_str = self.interner.resolve(*lemma2);
                                        if Lexer::is_weather_verb(lemma2_str) {
                                            let verb2 = *lemma2;
                                            self.advance(); // consume second weather verb

                                            // REUSE same event_var - no new variable, no DRS registration
                                            let neo_event2 = self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
                                                event_var,  // Same variable as first weather verb
                                                verb: verb2,
                                                roles: self.ctx.roles.alloc_slice(vec![]),
                                                modifiers: self.ctx.syms.alloc_slice(vec![]),
                                                suppress_existential,
                                                world: None,
                                            })));

                                            let op = if is_disjunction { TokenType::Or } else { TokenType::And };
                                            result = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                                                left: result,
                                                op,
                                                right: neo_event2,
                                            });
                                        } else {
                                            break; // Not a weather verb, stop coordination
                                        }
                                    } else {
                                        break;
                                    }
                                }

                                return Ok(match verb_time {
                                    Time::Past => self.ctx.exprs.alloc(LogicExpr::Temporal {
                                        operator: TemporalOperator::Past,
                                        body: result,
                                    }),
                                    Time::Future => self.ctx.exprs.alloc(LogicExpr::Temporal {
                                        operator: TemporalOperator::Future,
                                        body: result,
                                    }),
                                    _ => result,
                                });
                            }
                        }
                        // Check for "it + is/are + verb" pattern: "it is raining"
                        else if self.current + 2 < self.tokens.len() {
                            let is_copula = matches!(
                                self.tokens[self.current + 1].kind,
                                TokenType::Is | TokenType::Are | TokenType::Was | TokenType::Were
                            );
                            if is_copula {
                                if let TokenType::Verb { lemma, .. } = &self.tokens[self.current + 2].kind {
                                    let lemma_str = self.interner.resolve(*lemma);
                                    if Lexer::is_weather_verb(lemma_str) {
                                        let verb = *lemma;
                                        let verb_time = if matches!(
                                            self.tokens[self.current + 1].kind,
                                            TokenType::Was | TokenType::Were
                                        ) {
                                            Time::Past
                                        } else {
                                            Time::Present
                                        };
                                        self.advance(); // consume "it"
                                        self.advance(); // consume "is/are/was/were"
                                        self.advance(); // consume weather verb

                                        let event_var = self.get_event_var();
                                        // Weather verbs are impersonal - no pronoun resolution needed
                                        // Event var gets universal force from transpiler when suppress_existential=true
                                        let suppress_existential = self.drs.in_conditional_antecedent();

                                        let neo_event = self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
                                            event_var,
                                            verb,
                                            roles: self.ctx.roles.alloc_slice(vec![]),
                                            modifiers: self.ctx.syms.alloc_slice(vec![]),
                                            suppress_existential,
                                            world: None,
                                        })));

                                        // Progressive aspect for "is raining"
                                        let with_aspect = self.ctx.exprs.alloc(LogicExpr::Aspectual {
                                            operator: AspectOperator::Progressive,
                                            body: neo_event,
                                        });

                                        return Ok(match verb_time {
                                            Time::Past => self.ctx.exprs.alloc(LogicExpr::Temporal {
                                                operator: TemporalOperator::Past,
                                                body: with_aspect,
                                            }),
                                            _ => with_aspect,
                                        });
                                    }
                                }
                            }
                        }
                    }
                }
            }

            // Track if subject is an indefinite that needs DRS registration
            let (subject, subject_type_pred) = if self.check_pronoun() {
                let token = self.advance().clone();
                let token_text = self.interner.resolve(token.lexeme);
                // Handle first/second person pronouns as constants (deictic reference)
                let resolved = if token_text.eq_ignore_ascii_case("i") {
                    self.interner.intern("Speaker")
                } else if token_text.eq_ignore_ascii_case("you") {
                    self.interner.intern("Addressee")
                } else if let TokenType::Pronoun { gender, number, .. } = token.kind {
                    let resolved_pronoun = self.resolve_pronoun(gender, number)?;
                    match resolved_pronoun {
                        super::ResolvedPronoun::Variable(s) | super::ResolvedPronoun::Constant(s) => s,
                    }
                } else {
                    unknown
                };
                (resolved, None)
            } else {
                let np = self.parse_noun_phrase(true)?;

                // Check if this NP should introduce a DRS referent
                // Both indefinites ("a dog") and definites ("the dog") introduce referents
                // For definites without antecedent, this implements "global accommodation"
                if np.definiteness == Some(Definiteness::Indefinite)
                    || np.definiteness == Some(Definiteness::Definite)
                    || np.definiteness == Some(Definiteness::Distal) {
                    let gender = Self::infer_noun_gender(self.interner.resolve(np.noun));
                    let number = if Self::is_plural_noun(self.interner.resolve(np.noun)) {
                        Number::Plural
                    } else {
                        Number::Singular
                    };

                    // Register in DRS using noun as variable (for pronoun resolution)
                    // For DEFINITES ("the X"), use MainClause source to avoid universal force
                    // This ensures "the butler" in conditionals is treated as a constant
                    // For INDEFINITES ("a X"), use default source (gets universal force in antecedent)
                    if np.definiteness == Some(Definiteness::Definite) || np.definiteness == Some(Definiteness::Distal) {
                        self.drs.introduce_referent_with_source(np.noun, np.noun, gender, number, crate::drs::ReferentSource::MainClause);
                    } else {
                        self.drs.introduce_referent(np.noun, np.noun, gender, number);
                    }

                    // Create type predicate: Farmer(noun)
                    let type_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
                        name: np.noun,
                        args: self.ctx.terms.alloc_slice([Term::Variable(np.noun)]),
                        world: None,
                    });

                    (np.noun, Some(type_pred))
                } else {
                    // Proper name - use as constant (proper names have their own registration)
                    (np.noun, None)
                }
            };

            // Determine the subject term type
            let subject_term = if subject_type_pred.is_some() {
                Term::Variable(subject)
            } else {
                Term::Constant(subject)
            };

            // Handle presupposition triggers in antecedent: "If John stopped smoking, ..."
            // Only trigger if followed by gerund complement
            if self.check_presup_trigger() && self.is_followed_by_gerund() {
                let presup_kind = match self.advance().kind {
                    TokenType::PresupTrigger(kind) => kind,
                    TokenType::Verb { lemma, .. } => {
                        let s = self.interner.resolve(lemma).to_lowercase();
                        crate::lexicon::lookup_presup_trigger(&s)
                            .expect("Lexicon mismatch: Verb flagged as trigger but lookup failed")
                    }
                    _ => panic!("Expected presupposition trigger"),
                };
                let np = NounPhrase {
                    noun: subject,
                    definiteness: None,
                    adjectives: &[],
                    possessor: None,
                    pps: &[],
                    superlative: None,
                };
                return self.parse_presupposition(&np, presup_kind);
            }

            if self.check(&TokenType::Were) {
                self.advance();
                let predicate = if self.check_pronoun() {
                    let token = self.advance().clone();
                    if let TokenType::Pronoun { gender, number, .. } = token.kind {
                        let token_text = self.interner.resolve(token.lexeme);
                        if token_text.eq_ignore_ascii_case("i") {
                            self.interner.intern("Speaker")
                        } else if token_text.eq_ignore_ascii_case("you") {
                            self.interner.intern("Addressee")
                        } else {
                            let resolved_pronoun = self.resolve_pronoun(gender, number)?;
                            match resolved_pronoun {
                                super::ResolvedPronoun::Variable(s) | super::ResolvedPronoun::Constant(s) => s,
                            }
                        }
                    } else {
                        unknown
                    }
                } else {
                    self.consume_content_word()?
                };
                let be = self.interner.intern("Be");
                let be_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
                    name: be,
                    args: self.ctx.terms.alloc_slice([
                        subject_term,
                        Term::Constant(predicate),
                    ]),
                    world: None,
                });
                // Combine with type predicate if indefinite subject
                return Ok(if let Some(type_pred) = subject_type_pred {
                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                        left: type_pred,
                        op: TokenType::And,
                        right: be_pred,
                    })
                } else {
                    be_pred
                });
            }

            if self.check(&TokenType::Had) {
                self.advance();
                let verb = self.consume_content_word()?;
                let main_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
                    name: verb,
                    args: self.ctx.terms.alloc_slice([subject_term]),
                    world: None,
                });

                // Handle "because" causal clause in antecedent
                // Phase 35: Do NOT consume if followed by string literal (Trust justification)
                if self.check(&TokenType::Because) && !self.peek_next_is_string_literal() {
                    self.advance();
                    let cause = self.parse_atom()?;
                    let causal = self.ctx.exprs.alloc(LogicExpr::Causal {
                        effect: main_pred,
                        cause,
                    });
                    // Combine with type predicate if indefinite subject
                    return Ok(if let Some(type_pred) = subject_type_pred {
                        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                            left: type_pred,
                            op: TokenType::And,
                            right: causal,
                        })
                    } else {
                        causal
                    });
                }

                // Combine with type predicate if indefinite subject
                return Ok(if let Some(type_pred) = subject_type_pred {
                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                        left: type_pred,
                        op: TokenType::And,
                        right: main_pred,
                    })
                } else {
                    main_pred
                });
            }

            // Parse verb phrase with subject
            // Use variable term for indefinite subjects, constant for definites/proper names
            let verb_phrase = if subject_type_pred.is_some() {
                self.parse_predicate_with_subject_as_var(subject)?
            } else {
                self.parse_predicate_with_subject(subject)?
            };

            // Combine with type predicate if indefinite subject
            return Ok(if let Some(type_pred) = subject_type_pred {
                self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                    left: type_pred,
                    op: TokenType::And,
                    right: verb_phrase,
                })
            } else {
                verb_phrase
            });
        }

        self.parse_sentence()
    }

    fn parse_counterfactual_consequent(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        let unknown = self.interner.intern("?");
        if self.check_content_word() || self.check_pronoun() {
            // Check for grammatically incorrect "its" + weather adjective
            // "its" is possessive, "it's" is contraction - common typo
            if self.check_pronoun() {
                let token = self.peek();
                let token_text = self.interner.resolve(token.lexeme).to_lowercase();
                if token_text == "its" {
                    // Check if followed by weather adjective
                    if self.current + 1 < self.tokens.len() {
                        let next_token = &self.tokens[self.current + 1];
                        let next_str = self.interner.resolve(next_token.lexeme).to_lowercase();
                        if let Some(meta) = crate::lexicon::lookup_adjective_db(&next_str) {
                            if meta.features.contains(&crate::lexicon::Feature::Weather) {
                                return Err(ParseError {
                                    kind: ParseErrorKind::GrammarError(
                                        "Did you mean 'it's' (it is)? 'its' is a possessive pronoun.".to_string()
                                    ),
                                    span: self.current_span(),
                                });
                            }
                        }
                    }
                }
            }

            // Check for expletive "it" + copula + weather adjective: "it's wet" → Wet
            if self.check_pronoun() {
                let token_text = self.interner.resolve(self.peek().lexeme).to_lowercase();
                if token_text == "it" {
                    // Look ahead for copula + weather adjective
                    // Handle both "it is wet" and "it's wet" (where 's is Possessive token)
                    if self.current + 2 < self.tokens.len() {
                        let next = &self.tokens[self.current + 1].kind;
                        if matches!(next, TokenType::Is | TokenType::Was | TokenType::Possessive) {
                            // Check if followed by weather adjective
                            let adj_token = &self.tokens[self.current + 2];
                            let adj_sym = adj_token.lexeme;
                            let adj_str = self.interner.resolve(adj_sym).to_lowercase();
                            if let Some(meta) = crate::lexicon::lookup_adjective_db(&adj_str) {
                                if meta.features.contains(&crate::lexicon::Feature::Weather) {
                                    self.advance(); // consume "it"
                                    self.advance(); // consume copula
                                    self.advance(); // consume adjective token

                                    // Use the canonical lemma from lexicon (e.g., "Wet" not "wet")
                                    let adj_lemma = self.interner.intern(meta.lemma);

                                    // Get event variable from DRS (introduced in antecedent)
                                    let event_var = self.drs.get_last_event_referent(self.interner)
                                        .unwrap_or_else(|| self.interner.intern("e"));

                                    // First weather adjective predicate
                                    let mut result: &'a LogicExpr<'a> = self.ctx.exprs.alloc(LogicExpr::Predicate {
                                        name: adj_lemma,
                                        args: self.ctx.terms.alloc_slice([Term::Variable(event_var)]),
                                        world: None,
                                    });

                                    // Handle coordinated adjectives: "wet and cold"
                                    while self.check(&TokenType::And) {
                                        self.advance(); // consume "and"
                                        if self.check_content_word() {
                                            let adj2_lexeme = self.peek().lexeme;
                                            let adj2_str = self.interner.resolve(adj2_lexeme).to_lowercase();

                                            // Check if it's also a weather adjective
                                            if let Some(meta2) = crate::lexicon::lookup_adjective_db(&adj2_str) {
                                                if meta2.features.contains(&crate::lexicon::Feature::Weather) {
                                                    self.advance(); // consume adjective token
                                                    // Use the canonical lemma from lexicon (e.g., "Cold" not "cold")
                                                    let adj2_lemma = self.interner.intern(meta2.lemma);
                                                    let pred2 = self.ctx.exprs.alloc(LogicExpr::Predicate {
                                                        name: adj2_lemma,
                                                        args: self.ctx.terms.alloc_slice([Term::Variable(event_var)]),
                                                        world: None,
                                                    });
                                                    result = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                                                        left: result,
                                                        op: TokenType::And,
                                                        right: pred2,
                                                    });
                                                    continue;
                                                }
                                            }
                                        }
                                        break;
                                    }

                                    return Ok(result);
                                }
                            }
                        }
                    }
                }
            }

            let subject = if self.check_pronoun() {
                let token = self.advance().clone();
                let token_text = self.interner.resolve(token.lexeme);
                // Handle first/second person pronouns as constants (deictic reference)
                if token_text.eq_ignore_ascii_case("i") {
                    self.interner.intern("Speaker")
                } else if token_text.eq_ignore_ascii_case("you") {
                    self.interner.intern("Addressee")
                } else if let TokenType::Pronoun { gender, number, .. } = token.kind {
                    let resolved_pronoun = self.resolve_pronoun(gender, number)?;
                    match resolved_pronoun {
                        super::ResolvedPronoun::Variable(s) | super::ResolvedPronoun::Constant(s) => s,
                    }
                } else {
                    unknown
                }
            } else {
                self.parse_noun_phrase(true)?.noun
            };

            if self.check(&TokenType::Would) {
                self.advance();
                if self.check_content_word() {
                    let next_word = self.interner.resolve(self.peek().lexeme).to_lowercase();
                    if next_word == "have" {
                        self.advance();
                    }
                }
                let verb = self.consume_content_word()?;
                return Ok(self.ctx.exprs.alloc(LogicExpr::Predicate {
                    name: verb,
                    args: self.ctx.terms.alloc_slice([Term::Constant(subject)]),
                    world: None,
                }));
            }

            return self.parse_predicate_with_subject(subject);
        }

        self.parse_sentence()
    }

    fn extract_verb_from_expr(&self, expr: &LogicExpr<'a>) -> Option<Symbol> {
        match expr {
            // NeoEvent directly contains the verb
            LogicExpr::NeoEvent(data) => Some(data.verb),
            // Control structures directly contain the verb
            LogicExpr::Control { verb, .. } => Some(*verb),
            // Phase 46: For BinaryOp, try to find NeoEvent first (either side),
            // then fall back to Predicate. This handles both:
            // - Transitive: Apple(x) ∧ ∃e(Eat(e)...) - NeoEvent on right
            // - Motion PP: ∃e(Walk(e)...) ∧ To(e, Park) - NeoEvent on left
            LogicExpr::BinaryOp { left, right, .. } => {
                // First check if left contains a NeoEvent (motion PP case)
                if let Some(verb) = self.extract_neo_event_verb(left) {
                    return Some(verb);
                }
                // Then check right (transitive case with type predicate on left)
                if let Some(verb) = self.extract_neo_event_verb(right) {
                    return Some(verb);
                }
                // Fall back to any extractable verb
                self.extract_verb_from_expr(left)
                    .or_else(|| self.extract_verb_from_expr(right))
            }
            // Plain predicate - last resort (might be type predicate or PP)
            LogicExpr::Predicate { name, .. } => Some(*name),
            LogicExpr::Modal { operand, .. } => self.extract_verb_from_expr(operand),
            LogicExpr::Presupposition { assertion, .. } => self.extract_verb_from_expr(assertion),
            LogicExpr::Temporal { body, .. } => self.extract_verb_from_expr(body),
            LogicExpr::TemporalAnchor { body, .. } => self.extract_verb_from_expr(body),
            LogicExpr::Aspectual { body, .. } => self.extract_verb_from_expr(body),
            LogicExpr::Quantifier { body, .. } => self.extract_verb_from_expr(body),
            _ => None,
        }
    }

    /// Phase 46: Generalized gapping with template-guided reconstruction.
    /// Handles NPs, PPs, temporal adverbs, and preserves roles from EventTemplate.
    fn parse_gapped_clause(&mut self, borrowed_verb: Symbol) -> ParseResult<&'a LogicExpr<'a>> {
        let subject = self.parse_noun_phrase(true)?;

        if self.check(&TokenType::Comma) {
            self.advance();
        }

        let subject_term = self.noun_phrase_to_term(&subject);
        let event_var = self.get_event_var();
        let suppress_existential = self.drs.in_conditional_antecedent();

        // Get template for role guidance
        let template = self.last_event_template.clone();

        // Collect arguments (NPs, PPs, temporal adverbs) from gapped clause
        let mut np_args: Vec<Term<'a>> = Vec::new();
        let mut pp_args: Vec<(Symbol, Term<'a>)> = Vec::new();
        let mut override_adverb: Option<Symbol> = None;

        loop {
            if self.check_temporal_adverb() {
                // Temporal adverb: override template modifier
                if let TokenType::TemporalAdverb(sym) = self.advance().kind {
                    override_adverb = Some(sym);
                }
            } else if self.check_preposition() {
                // PP argument: "to the school", "on the table"
                let prep = if let TokenType::Preposition(sym) = self.advance().kind {
                    sym
                } else {
                    continue;
                };
                let np = self.parse_noun_phrase(false)?;
                pp_args.push((prep, self.noun_phrase_to_term(&np)));
            } else if self.check_content_word() || self.check_article() {
                // NP argument
                let np = self.parse_noun_phrase(false)?;
                np_args.push(self.noun_phrase_to_term(&np));
                if self.check(&TokenType::Comma) {
                    self.advance();
                }
            } else {
                break;
            }
        }

        // Build roles using template guidance
        let roles = self.build_gapped_roles(subject_term, &np_args, &pp_args, &template);

        // Handle modifiers: override if adverb provided, else inherit from template
        let modifiers = match (override_adverb, &template) {
            (Some(adv), Some(tmpl)) => {
                // Filter out temporal modifiers from template, add new one
                let mut mods: Vec<Symbol> = tmpl
                    .modifiers
                    .iter()
                    .filter(|m| !self.is_temporal_modifier(**m))
                    .cloned()
                    .collect();
                mods.push(adv);
                mods
            }
            (Some(adv), None) => vec![adv],
            (None, Some(tmpl)) => tmpl.modifiers.clone(),
            (None, None) => vec![],
        };

        Ok(self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
            event_var,
            verb: borrowed_verb,
            roles: self.ctx.roles.alloc_slice(roles),
            modifiers: self.ctx.syms.alloc_slice(modifiers),
            suppress_existential,
            world: None,
        }))))
    }

    fn is_complete_clause(&self, expr: &LogicExpr<'a>) -> bool {
        match expr {
            LogicExpr::Atom(_) => false,
            LogicExpr::Predicate { .. } => true,
            LogicExpr::Quantifier { .. } => true,
            LogicExpr::Modal { .. } => true,
            LogicExpr::Temporal { .. } => true,
            LogicExpr::Aspectual { .. } => true,
            LogicExpr::BinaryOp { .. } => true,
            LogicExpr::UnaryOp { .. } => true,
            LogicExpr::Control { .. } => true,
            LogicExpr::Presupposition { .. } => true,
            LogicExpr::Categorical(_) => true,
            LogicExpr::Relation(_) => true,
            _ => true,
        }
    }

    /// Parse disjunction (Or/Iff) - lowest precedence logical connectives.
    /// Calls parse_conjunction for operands to ensure And binds tighter.
    fn parse_disjunction(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        let mut expr = self.parse_conjunction()?;

        while self.check(&TokenType::Comma)
            || self.check(&TokenType::Or)
            || self.check(&TokenType::Iff)
        {
            if self.check(&TokenType::Comma) {
                self.advance();
            }
            if !self.match_token(&[TokenType::Or, TokenType::Iff]) {
                break;
            }
            let operator = self.previous().kind.clone();
            self.current_island += 1;

            let saved_pos = self.current;
            let standard_attempt = self.try_parse(|p| p.parse_conjunction());

            // Gapping in disjunction: only for Or, not Iff. Use original (non-expanded) trigger.
            // Expanded gapping (with Period/is_at_end) only applies in parse_conjunction.
            let use_gapping = match &standard_attempt {
                Some(right) => {
                    !self.is_complete_clause(right)
                        && (self.check(&TokenType::Comma) || self.check_content_word())
                        && operator != TokenType::Iff // Don't gap on biconditional
                }
                None => operator != TokenType::Iff, // For Iff, require successful parse
            };

            if !use_gapping {
                if let Some(right) = standard_attempt {
                    expr = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                        left: expr,
                        op: operator,
                        right,
                    });
                }
            } else {
                self.current = saved_pos;

                let borrowed_verb = self.extract_verb_from_expr(expr).ok_or(ParseError {
                    kind: ParseErrorKind::GappingResolutionFailed,
                    span: self.current_span(),
                })?;

                let right = self.parse_gapped_clause(borrowed_verb)?;

                expr = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                    left: expr,
                    op: operator,
                    right,
                });
            }
        }

        // Handle binary temporal connectives (lowest precedence temporal)
        // "P until Q" → TemporalBinary { Until, P, Q }
        // "P release Q" → TemporalBinary { Release, P, Q }
        // "P weak-until Q" → TemporalBinary { WeakUntil, P, Q }
        if self.check(&TokenType::Until) || self.check(&TokenType::Release) || self.check(&TokenType::WeakUntil) {
            let op = match self.peek().kind {
                TokenType::Release => crate::ast::logic::BinaryTemporalOp::Release,
                TokenType::WeakUntil => crate::ast::logic::BinaryTemporalOp::WeakUntil,
                _ => crate::ast::logic::BinaryTemporalOp::Until,
            };
            self.advance();
            let right = self.parse_conjunction()?;
            expr = self.ctx.exprs.alloc(LogicExpr::TemporalBinary {
                operator: op,
                left: expr,
                right,
            });
        }

        // Check for trailing "within N cycles" bounded temporal delay
        let expr = self.try_wrap_bounded_delay(expr);

        Ok(expr)
    }

    /// Parse conjunction (And) - higher precedence than Or.
    /// Calls parse_atom for operands.
    fn parse_conjunction(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
        let mut expr = self.parse_atom()?;

        // Handle causal "because" at conjunction level
        // Phase 35: Do NOT consume if followed by string literal (Trust justification)
        if self.check(&TokenType::Because) && !self.peek_next_is_string_literal() {
            self.advance();
            let cause = self.parse_atom()?;
            return Ok(self.ctx.exprs.alloc(LogicExpr::Causal {
                effect: expr,
                cause,
            }));
        }

        while self.check(&TokenType::Comma) || self.check(&TokenType::And) {
            if self.check(&TokenType::Comma) {
                self.advance();
            }
            if !self.match_token(&[TokenType::And]) {
                break;
            }
            let operator = self.previous().kind.clone();
            self.current_island += 1;

            let saved_pos = self.current;
            let standard_attempt = self.try_parse(|p| p.parse_atom());

            // Phase 46: Expanded gapping trigger to support PP gapping, temporal override,
            // and intransitive gapping (bare subject at clause boundary)
            let use_gapping = match &standard_attempt {
                Some(right) => {
                    !self.is_complete_clause(right)
                        && (self.check(&TokenType::Comma)
                            || self.check_content_word()
                            || self.check_preposition()
                            || self.check_temporal_adverb()
                            || self.check(&TokenType::Period)
                            || self.is_at_end())
                }
                None => true,
            };

            if !use_gapping {
                if let Some(right) = standard_attempt {
                    expr = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                        left: expr,
                        op: operator,
                        right,
                    });
                }
            } else {
                self.current = saved_pos;

                let borrowed_verb = self.extract_verb_from_expr(expr).ok_or(ParseError {
                    kind: ParseErrorKind::GappingResolutionFailed,
                    span: self.current_span(),
                })?;

                let right = self.parse_gapped_clause(borrowed_verb)?;

                expr = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                    left: expr,
                    op: operator,
                    right,
                });
            }
        }

        Ok(expr)
    }

    fn parse_relative_clause(&mut self, gap_var: Symbol) -> ParseResult<&'a LogicExpr<'a>> {
        if self.check_verb() {
            return self.parse_verb_phrase_for_restriction(gap_var);
        }

        // Handle "do/does (not)" in relative clauses: "who do not shave themselves"
        if self.check(&TokenType::Do) || self.check(&TokenType::Does) {
            self.advance(); // consume "do/does"

            let is_negated = self.check(&TokenType::Not);
            if is_negated {
                self.advance(); // consume "not"
            }

            if self.check_verb() {
                let verb = self.consume_verb();

                // Check for reflexive object: "shave themselves"
                let roles = if self.check(&TokenType::Reflexive) {
                    self.advance(); // consume "themselves/himself"
                    vec![
                        (ThematicRole::Agent, Term::Variable(gap_var)),
                        (ThematicRole::Theme, Term::Variable(gap_var)),
                    ]
                } else if self.check_content_word() || self.check_article() {
                    // Parse object NP
                    let obj = self.parse_noun_phrase(false)?;
                    vec![
                        (ThematicRole::Agent, Term::Variable(gap_var)),
                        (ThematicRole::Theme, Term::Constant(obj.noun)),
                    ]
                } else {
                    // Intransitive
                    vec![(ThematicRole::Agent, Term::Variable(gap_var))]
                };

                let event_var = self.get_event_var();
                let suppress_existential = self.drs.in_conditional_antecedent();
                let event = self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
                    event_var,
                    verb,
                    roles: self.ctx.roles.alloc_slice(roles),
                    modifiers: self.ctx.syms.alloc_slice(vec![]),
                    suppress_existential,
                    world: None,
                })));

                if is_negated {
                    return Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
                        op: TokenType::Not,
                        operand: event,
                    }));
                }
                return Ok(event);
            }
        }

        if self.check_content_word() || self.check_article() {
            let rel_subject = self.parse_noun_phrase_for_relative()?;

            let nested_relative = if matches!(self.peek().kind, TokenType::Article(_)) {
                let nested_var = self.next_var_name();
                Some((nested_var, self.parse_relative_clause(nested_var)?))
            } else {
                None
            };

            if self.check_verb() {
                let verb = self.consume_verb();

                let mut roles: Vec<(ThematicRole, Term<'a>)> = vec![
                    (ThematicRole::Agent, Term::Constant(rel_subject.noun)),
                    (ThematicRole::Theme, Term::Variable(gap_var)),
                ];

                while self.check_to_preposition() {
                    self.advance();
                    if self.check_content_word() || self.check_article() {
                        let recipient = self.parse_noun_phrase(false)?;
                        roles.push((ThematicRole::Recipient, Term::Constant(recipient.noun)));
                    }
                }

                let event_var = self.get_event_var();
                let suppress_existential = self.drs.in_conditional_antecedent();
                let this_event = self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
                    event_var,
                    verb,
                    roles: self.ctx.roles.alloc_slice(roles),
                    modifiers: self.ctx.syms.alloc_slice(vec![]),
                    suppress_existential,
                    world: None,
                })));

                if let Some((nested_var, nested_clause)) = nested_relative {
                    let type_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
                        name: rel_subject.noun,
                        args: self.ctx.terms.alloc_slice([Term::Variable(nested_var)]),
                        world: None,
                    });

                    let inner = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                        left: type_pred,
                        op: TokenType::And,
                        right: nested_clause,
                    });

                    let combined = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
                        left: inner,
                        op: TokenType::And,
                        right: this_event,
                    });

                    return Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
                        kind: crate::ast::QuantifierKind::Existential,
                        variable: nested_var,
                        body: combined,
                        island_id: self.current_island,
                    }));
                }

                return Ok(this_event);
            }
        }

        if self.check_verb() {
            return self.parse_verb_phrase_for_restriction(gap_var);
        }

        let unknown = self.interner.intern("?");
        Ok(self.ctx.exprs.alloc(LogicExpr::Atom(unknown)))
    }

    fn check_ellipsis_auxiliary(&self) -> bool {
        matches!(
            self.peek().kind,
            TokenType::Does | TokenType::Do |
            TokenType::Can | TokenType::Could | TokenType::Would |
            TokenType::May | TokenType::Must | TokenType::Should
        )
    }

    fn check_ellipsis_terminator(&self) -> bool {
        if self.is_at_end() || self.check(&TokenType::Period) {
            return true;
        }
        if self.check_content_word() {
            let word = self.interner.resolve(self.peek().lexeme).to_lowercase();
            return word == "too" || word == "also";
        }
        false
    }

    fn try_parse_ellipsis(&mut self) -> Option<ParseResult<&'a LogicExpr<'a>>> {
        // Need a stored template to reconstruct from
        if self.last_event_template.is_none() {
            return None;
        }

        let saved_pos = self.current;

        // Pattern: Subject + Auxiliary + (not)? + Terminator
        // Subject must be proper name or pronoun
        let subject_sym = if matches!(self.peek().kind, TokenType::ProperName(_)) {
            if let TokenType::ProperName(sym) = self.advance().kind {
                sym
            } else {
                self.current = saved_pos;
                return None;
            }
        } else if self.check_pronoun() {
            let token = self.advance().clone();
            if let TokenType::Pronoun { gender, number, .. } = token.kind {
                match self.resolve_pronoun(gender, number) {
                    Ok(resolved) => match resolved {
                        super::ResolvedPronoun::Variable(s) | super::ResolvedPronoun::Constant(s) => s,
                    },
                    Err(e) => return Some(Err(e)),
                }
            } else {
                self.current = saved_pos;
                return None;
            }
        } else {
            return None;
        };

        // Must be followed by ellipsis auxiliary
        if !self.check_ellipsis_auxiliary() {
            self.current = saved_pos;
            return None;
        }
        let aux_token = self.advance().kind.clone();

        // Check for negation
        let is_negated = self.match_token(&[TokenType::Not]);

        // Must end with terminator
        if !self.check_ellipsis_terminator() {
            self.current = saved_pos;
            return None;
        }

        // Consume "too"/"also" if present
        if self.check_content_word() {
            let word = self.interner.resolve(self.peek().lexeme).to_lowercase();
            if word == "too" || word == "also" {
                self.advance();
            }
        }

        // Reconstruct from template
        let template = self.last_event_template.clone().unwrap();
        let event_var = self.get_event_var();
        let suppress_existential = self.drs.in_conditional_antecedent();

        // Build roles with new subject as Agent
        let mut roles: Vec<(ThematicRole, Term<'a>)> = vec![
            (ThematicRole::Agent, Term::Constant(subject_sym))
        ];
        roles.extend(template.non_agent_roles.iter().cloned());

        let neo_event = self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
            event_var,
            verb: template.verb,
            roles: self.ctx.roles.alloc_slice(roles),
            modifiers: self.ctx.syms.alloc_slice(template.modifiers.clone()),
            suppress_existential,
            world: None,
        })));

        // Apply modal if auxiliary is modal
        let with_modal = match aux_token {
            TokenType::Can | TokenType::Could => {
                let vector = self.token_to_vector(&aux_token);
                self.ctx.modal(vector, neo_event)
            }
            TokenType::Would | TokenType::May | TokenType::Must | TokenType::Should => {
                let vector = self.token_to_vector(&aux_token);
                self.ctx.modal(vector, neo_event)
            }
            _ => neo_event,
        };

        // Apply negation if present
        let result = if is_negated {
            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
                op: TokenType::Not,
                operand: with_modal,
            })
        } else {
            with_modal
        };

        Some(Ok(result))
    }
}

// Phase 46: Helper methods for generalized gapping (not part of trait)
impl<'a, 'ctx, 'int> Parser<'a, 'ctx, 'int> {
    /// Helper to extract verb specifically from NeoEvent structures
    fn extract_neo_event_verb(&self, expr: &LogicExpr<'a>) -> Option<Symbol> {
        match expr {
            LogicExpr::NeoEvent(data) => Some(data.verb),
            LogicExpr::Quantifier { body, .. } => self.extract_neo_event_verb(body),
            LogicExpr::BinaryOp { left, right, .. } => {
                self.extract_neo_event_verb(left)
                    .or_else(|| self.extract_neo_event_verb(right))
            }
            LogicExpr::Temporal { body, .. } => self.extract_neo_event_verb(body),
            LogicExpr::Aspectual { body, .. } => self.extract_neo_event_verb(body),
            _ => None,
        }
    }

    /// Build roles for gapped clause using template guidance.
    /// NP args map to Theme/Recipient roles, PP args map by preposition type.
    fn build_gapped_roles(
        &self,
        subject_term: Term<'a>,
        np_args: &[Term<'a>],
        pp_args: &[(Symbol, Term<'a>)],
        template: &Option<EventTemplate<'a>>,
    ) -> Vec<(ThematicRole, Term<'a>)> {
        let mut roles = vec![(ThematicRole::Agent, subject_term)];

        match template {
            Some(tmpl) => {
                let template_roles = &tmpl.non_agent_roles;

                // Separate template roles into NP-type and PP-type
                let np_template_roles: Vec<_> = template_roles
                    .iter()
                    .filter(|(r, _)| {
                        matches!(
                            r,
                            ThematicRole::Theme | ThematicRole::Recipient | ThematicRole::Patient
                        )
                    })
                    .collect();

                let pp_template_roles: Vec<_> = template_roles
                    .iter()
                    .filter(|(r, _)| {
                        matches!(
                            r,
                            ThematicRole::Goal
                                | ThematicRole::Source
                                | ThematicRole::Location
                                | ThematicRole::Instrument
                        )
                    })
                    .collect();

                // Handle NPs by matching to template NP roles
                match (np_template_roles.len(), np_args.len()) {
                    (0, 0) => {} // Intransitive - no NP roles
                    (_, 0) => {
                        // Use all template NP roles unchanged
                        for (role, term) in &np_template_roles {
                            roles.push((*role, term.clone()));
                        }
                    }
                    (n, 1) if n > 0 => {
                        // 1 NP arg: replace LAST NP role (usually Theme), keep others
                        for (role, term) in np_template_roles.iter().take(n - 1) {
                            roles.push((*role, term.clone()));
                        }
                        if let Some((last_role, _)) = np_template_roles.last() {
                            roles.push((*last_role, np_args[0].clone()));
                        }
                    }
                    (n, m) if m == n => {
                        // Same count: replace all NP roles in order
                        for ((role, _), arg) in np_template_roles.iter().zip(np_args.iter()) {
                            roles.push((*role, arg.clone()));
                        }
                    }
                    (_, _) => {
                        // Fallback: assign Theme to each NP
                        for (i, arg) in np_args.iter().enumerate() {
                            let role = np_template_roles
                                .get(i)
                                .map(|(r, _)| *r)
                                .unwrap_or(ThematicRole::Theme);
                            roles.push((role, arg.clone()));
                        }
                    }
                }

                // Handle PPs: use parsed PPs if provided, else use template
                if pp_args.is_empty() {
                    // Use template PP roles unchanged
                    for (role, term) in &pp_template_roles {
                        roles.push((*role, term.clone()));
                    }
                } else {
                    // Use parsed PPs, map preposition to role
                    for (prep, term) in pp_args {
                        let role = self.preposition_to_role(*prep);
                        roles.push((role, term.clone()));
                    }
                }
            }
            None => {
                // No template: backward-compat hardcoded Agent + Theme
                for arg in np_args {
                    roles.push((ThematicRole::Theme, arg.clone()));
                }
                for (prep, term) in pp_args {
                    let role = self.preposition_to_role(*prep);
                    roles.push((role, term.clone()));
                }
            }
        }
        roles
    }

    /// Map preposition to thematic role
    fn preposition_to_role(&self, prep: Symbol) -> ThematicRole {
        let prep_str = self.interner.resolve(prep).to_lowercase();
        match prep_str.as_str() {
            "to" | "toward" | "towards" => ThematicRole::Goal,
            "from" => ThematicRole::Source,
            "in" | "on" | "at" => ThematicRole::Location,
            "with" | "by" => ThematicRole::Instrument,
            _ => ThematicRole::Location, // Default fallback
        }
    }

    /// Check if modifier is temporal (for override filtering)
    fn is_temporal_modifier(&self, sym: Symbol) -> bool {
        let s = self.interner.resolve(sym).to_lowercase();
        matches!(
            s.as_str(),
            "yesterday" | "today" | "tomorrow" | "now" | "then" | "past" | "future"
        )
    }
}