logicaffeine_language/parser/
quantifier.rs

1//! Quantifier parsing and scope management.
2//!
3//! This module handles determiners with quantificational force:
4//!
5//! - **Universal**: every, all, each → `∀x`
6//! - **Existential**: a, an, some → `∃x`
7//! - **Negative**: no, neither → `¬∃x` or `∀x(... → ¬...)`
8//! - **Proportional**: most, few, many → generalized quantifiers
9//! - **Definite**: the → uniqueness presupposition (ιx)
10//!
11//! # Quantifier Scope
12//!
13//! Quantifiers are assigned to scope islands during parsing. The `island_id` field
14//! tracks which island a quantifier belongs to, preventing illicit scope inversions
15//! (e.g., extracting from relative clauses).
16//!
17//! # Donkey Anaphora
18//!
19//! Indefinites in conditional antecedents or relative clauses receive universal
20//! force when bound by a pronoun in the main clause:
21//!
22//! "If a farmer owns a donkey, he beats it" → `∀x∀y((Farmer(x) ∧ Donkey(y) ∧ Owns(x,y)) → Beats(x,y))`
23
24use super::clause::ClauseParsing;
25use super::modal::ModalParsing;
26use super::noun::NounParsing;
27use super::{NegativeScopeMode, ParseResult, Parser};
28use crate::ast::{LogicExpr, NeoEventData, NounPhrase, QuantifierKind, Term, ThematicRole};
29use crate::drs::{Gender, Number};
30use crate::drs::ReferentSource;
31use crate::error::{ParseError, ParseErrorKind};
32use logicaffeine_base::Symbol;
33use crate::lexer::Lexer;
34use crate::lexicon::{get_canonical_verb, is_subsective, lookup_verb_db, Definiteness, Feature, Time};
35use crate::token::{PresupKind, TokenType};
36
37/// Trait for parsing quantified expressions and managing scope.
38///
39/// Provides methods for parsing quantifiers (every, some, no, most),
40/// their restrictions, and wrapping expressions with appropriate scope.
41pub trait QuantifierParsing<'a, 'ctx, 'int> {
42    /// Parses a quantified expression from a quantifier determiner.
43    fn parse_quantified(&mut self) -> ParseResult<&'a LogicExpr<'a>>;
44    /// Parses the restrictor clause for a quantifier.
45    fn parse_restriction(&mut self, var_name: Symbol) -> ParseResult<&'a LogicExpr<'a>>;
46    /// Parses a verb phrase as the nuclear scope of a quantifier.
47    fn parse_verb_phrase_for_restriction(&mut self, var_name: Symbol) -> ParseResult<&'a LogicExpr<'a>>;
48    /// Combines multiple expressions with conjunction.
49    fn combine_with_and(&self, exprs: Vec<&'a LogicExpr<'a>>) -> ParseResult<&'a LogicExpr<'a>>;
50    fn wrap_with_definiteness_full(
51        &mut self,
52        np: &NounPhrase<'a>,
53        predicate: &'a LogicExpr<'a>,
54    ) -> ParseResult<&'a LogicExpr<'a>>;
55    fn wrap_with_definiteness(
56        &mut self,
57        definiteness: Option<Definiteness>,
58        noun: Symbol,
59        predicate: &'a LogicExpr<'a>,
60    ) -> ParseResult<&'a LogicExpr<'a>>;
61    fn wrap_with_definiteness_and_adjectives(
62        &mut self,
63        definiteness: Option<Definiteness>,
64        noun: Symbol,
65        adjectives: &[Symbol],
66        predicate: &'a LogicExpr<'a>,
67    ) -> ParseResult<&'a LogicExpr<'a>>;
68    fn wrap_with_definiteness_and_adjectives_and_pps(
69        &mut self,
70        definiteness: Option<Definiteness>,
71        noun: Symbol,
72        adjectives: &[Symbol],
73        pps: &[&'a LogicExpr<'a>],
74        predicate: &'a LogicExpr<'a>,
75    ) -> ParseResult<&'a LogicExpr<'a>>;
76    fn wrap_with_definiteness_for_object(
77        &mut self,
78        definiteness: Option<Definiteness>,
79        noun: Symbol,
80        predicate: &'a LogicExpr<'a>,
81    ) -> ParseResult<&'a LogicExpr<'a>>;
82    fn substitute_pp_placeholder(&mut self, pp: &'a LogicExpr<'a>, var: Symbol) -> &'a LogicExpr<'a>;
83    fn substitute_constant_with_var(
84        &self,
85        expr: &'a LogicExpr<'a>,
86        constant_name: Symbol,
87        var_name: Symbol,
88    ) -> ParseResult<&'a LogicExpr<'a>>;
89    fn substitute_constant_with_var_sym(
90        &self,
91        expr: &'a LogicExpr<'a>,
92        constant_name: Symbol,
93        var_name: Symbol,
94    ) -> ParseResult<&'a LogicExpr<'a>>;
95    fn substitute_constant_with_sigma(
96        &self,
97        expr: &'a LogicExpr<'a>,
98        constant_name: Symbol,
99        sigma_term: Term<'a>,
100    ) -> ParseResult<&'a LogicExpr<'a>>;
101    fn find_main_verb_name(&self, expr: &LogicExpr<'a>) -> Option<Symbol>;
102    fn transform_cardinal_to_group(&mut self, expr: &'a LogicExpr<'a>) -> ParseResult<&'a LogicExpr<'a>>;
103    fn build_verb_neo_event(
104        &mut self,
105        verb: Symbol,
106        subject_var: Symbol,
107        object: Option<Term<'a>>,
108        modifiers: Vec<Symbol>,
109    ) -> &'a LogicExpr<'a>;
110}
111
112impl<'a, 'ctx, 'int> QuantifierParsing<'a, 'ctx, 'int> for Parser<'a, 'ctx, 'int> {
113    fn parse_quantified(&mut self) -> ParseResult<&'a LogicExpr<'a>> {
114        let quantifier_token = self.previous().kind.clone();
115        let var_name = self.next_var_name();
116
117        // Track if we're inside a "No" quantifier - referents introduced here
118        // are inaccessible for cross-sentence anaphora
119        let was_in_negative_quantifier = self.in_negative_quantifier;
120        if matches!(quantifier_token, TokenType::No) {
121            self.in_negative_quantifier = true;
122        }
123
124        let subject_pred = self.parse_restriction(var_name)?;
125
126        if self.check_modal() {
127            use crate::ast::ModalFlavor;
128
129            self.advance();
130            let vector = self.token_to_vector(&self.previous().kind.clone());
131            let verb = self.consume_content_word()?;
132
133            // Parse object if present (e.g., "can enter the room" -> room is object)
134            let obj_term = if self.check_content_word() || self.check_article() {
135                let obj_np = self.parse_noun_phrase(false)?;
136                Some(self.noun_phrase_to_term(&obj_np))
137            } else {
138                None
139            };
140
141            // Collect any trailing adverbs
142            let modifiers = self.collect_adverbs();
143            let verb_pred = self.build_verb_neo_event(verb, var_name, obj_term, modifiers);
144
145            // Determine quantifier kind first (shared by both branches)
146            let kind = match quantifier_token {
147                TokenType::All | TokenType::No => QuantifierKind::Universal,
148                TokenType::Any => {
149                    if self.is_negative_context() {
150                        QuantifierKind::Existential
151                    } else {
152                        QuantifierKind::Universal
153                    }
154                }
155                TokenType::Some => QuantifierKind::Existential,
156                TokenType::Most => QuantifierKind::Most,
157                TokenType::Few => QuantifierKind::Few,
158                TokenType::Many => QuantifierKind::Many,
159                TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
160                TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
161                TokenType::AtMost(n) => QuantifierKind::AtMost(n),
162                _ => {
163                    return Err(ParseError {
164                        kind: ParseErrorKind::UnknownQuantifier {
165                            found: quantifier_token.clone(),
166                        },
167                        span: self.current_span(),
168                    })
169                }
170            };
171
172            // Branch on modal flavor for scope handling
173            if vector.flavor == ModalFlavor::Root {
174                // === NARROW SCOPE (De Re) ===
175                // Root modals (can, must, should) attach to the predicate inside the quantifier
176                // "Some birds can fly" → ∃x(Bird(x) ∧ ◇Fly(x))
177
178                // Wrap the verb predicate in the modal
179                let modal_verb = self.ctx.exprs.alloc(LogicExpr::Modal {
180                    vector,
181                    operand: verb_pred,
182                });
183
184                let body = match quantifier_token {
185                    TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
186                        left: subject_pred,
187                        op: TokenType::If,
188                        right: modal_verb,
189                    }),
190                    TokenType::Any => {
191                        if self.is_negative_context() {
192                            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
193                                left: subject_pred,
194                                op: TokenType::And,
195                                right: modal_verb,
196                            })
197                        } else {
198                            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
199                                left: subject_pred,
200                                op: TokenType::If,
201                                right: modal_verb,
202                            })
203                        }
204                    }
205                    TokenType::Some
206                    | TokenType::Most
207                    | TokenType::Few
208                    | TokenType::Many
209                    | TokenType::Cardinal(_)
210                    | TokenType::AtLeast(_)
211                    | TokenType::AtMost(_) => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
212                        left: subject_pred,
213                        op: TokenType::And,
214                        right: modal_verb,
215                    }),
216                    TokenType::No => {
217                        let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
218                            op: TokenType::Not,
219                            operand: modal_verb,
220                        });
221                        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
222                            left: subject_pred,
223                            op: TokenType::If,
224                            right: neg,
225                        })
226                    }
227                    _ => {
228                        return Err(ParseError {
229                            kind: ParseErrorKind::UnknownQuantifier {
230                                found: quantifier_token.clone(),
231                            },
232                            span: self.current_span(),
233                        })
234                    }
235                };
236
237                // Build quantifier (modal is inside)
238                let mut result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
239                    kind,
240                    variable: var_name,
241                    body,
242                    island_id: self.current_island,
243                });
244
245                // Process donkey bindings for indefinites in restrictions (e.g., "who lacks a key")
246                for (_noun, donkey_var, used, wide_neg) in self.donkey_bindings.iter().rev() {
247                    if *used {
248                        // Donkey anaphora: wrap with ∀ at outer scope
249                        result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
250                            kind: QuantifierKind::Universal,
251                            variable: *donkey_var,
252                            body: result,
253                            island_id: self.current_island,
254                        });
255                    } else {
256                        // Non-donkey: wrap with ∃ INSIDE the restriction
257                        result = self.wrap_donkey_in_restriction(result, *donkey_var, *wide_neg);
258                    }
259                }
260                self.donkey_bindings.clear();
261
262                self.in_negative_quantifier = was_in_negative_quantifier;
263                return Ok(result);
264
265            } else {
266                // === WIDE SCOPE (De Dicto) ===
267                // Epistemic modals (might, may) wrap the entire quantifier
268                // "Some unicorns might exist" → ◇∃x(Unicorn(x) ∧ Exist(x))
269
270                let body = match quantifier_token {
271                    TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
272                        left: subject_pred,
273                        op: TokenType::If,
274                        right: verb_pred,
275                    }),
276                    TokenType::Any => {
277                        if self.is_negative_context() {
278                            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
279                                left: subject_pred,
280                                op: TokenType::And,
281                                right: verb_pred,
282                            })
283                        } else {
284                            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
285                                left: subject_pred,
286                                op: TokenType::If,
287                                right: verb_pred,
288                            })
289                        }
290                    }
291                    TokenType::Some
292                    | TokenType::Most
293                    | TokenType::Few
294                    | TokenType::Many
295                    | TokenType::Cardinal(_)
296                    | TokenType::AtLeast(_)
297                    | TokenType::AtMost(_) => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
298                        left: subject_pred,
299                        op: TokenType::And,
300                        right: verb_pred,
301                    }),
302                    TokenType::No => {
303                        let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
304                            op: TokenType::Not,
305                            operand: verb_pred,
306                        });
307                        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
308                            left: subject_pred,
309                            op: TokenType::If,
310                            right: neg,
311                        })
312                    }
313                    _ => {
314                        return Err(ParseError {
315                            kind: ParseErrorKind::UnknownQuantifier {
316                                found: quantifier_token.clone(),
317                            },
318                            span: self.current_span(),
319                        })
320                    }
321                };
322
323                let mut result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
324                    kind,
325                    variable: var_name,
326                    body,
327                    island_id: self.current_island,
328                });
329
330                // Process donkey bindings for indefinites in restrictions (e.g., "who lacks a key")
331                for (_noun, donkey_var, used, wide_neg) in self.donkey_bindings.iter().rev() {
332                    if *used {
333                        // Donkey anaphora: wrap with ∀ at outer scope
334                        result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
335                            kind: QuantifierKind::Universal,
336                            variable: *donkey_var,
337                            body: result,
338                            island_id: self.current_island,
339                        });
340                    } else {
341                        // Non-donkey: wrap with ∃ INSIDE the restriction
342                        result = self.wrap_donkey_in_restriction(result, *donkey_var, *wide_neg);
343                    }
344                }
345                self.donkey_bindings.clear();
346
347                // Wrap the entire quantifier in the modal
348                self.in_negative_quantifier = was_in_negative_quantifier;
349                return Ok(self.ctx.exprs.alloc(LogicExpr::Modal {
350                    vector,
351                    operand: result,
352                }));
353            }
354        }
355
356        if self.check_auxiliary() {
357            let aux_token = self.advance();
358            let aux_time = if let TokenType::Auxiliary(time) = aux_token.kind.clone() {
359                time
360            } else {
361                Time::None
362            };
363            self.pending_time = Some(aux_time);
364
365            let is_negated = self.match_token(&[TokenType::Not]);
366            if is_negated {
367                self.negative_depth += 1;
368            }
369
370            if self.check_verb() {
371                let verb = self.consume_verb();
372
373                // Convert aux_time to modifier
374                let modifiers = match aux_time {
375                    Time::Past => vec![self.interner.intern("Past")],
376                    Time::Future => vec![self.interner.intern("Future")],
377                    _ => vec![],
378                };
379
380                let verb_pred = self.build_verb_neo_event(verb, var_name, None, modifiers);
381
382                let maybe_negated = if is_negated {
383                    self.negative_depth -= 1;
384                    self.ctx.exprs.alloc(LogicExpr::UnaryOp {
385                        op: TokenType::Not,
386                        operand: verb_pred,
387                    })
388                } else {
389                    verb_pred
390                };
391
392                let body = match quantifier_token {
393                    TokenType::All | TokenType::Any => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
394                        left: subject_pred,
395                        op: TokenType::If,
396                        right: maybe_negated,
397                    }),
398                    _ => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
399                        left: subject_pred,
400                        op: TokenType::And,
401                        right: maybe_negated,
402                    }),
403                };
404
405                let kind = match quantifier_token {
406                    TokenType::All | TokenType::No => QuantifierKind::Universal,
407                    TokenType::Some => QuantifierKind::Existential,
408                    TokenType::Most => QuantifierKind::Most,
409                    TokenType::Few => QuantifierKind::Few,
410                    TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
411                    TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
412                    TokenType::AtMost(n) => QuantifierKind::AtMost(n),
413                    _ => QuantifierKind::Universal,
414                };
415
416                self.in_negative_quantifier = was_in_negative_quantifier;
417                return Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
418                    kind,
419                    variable: var_name,
420                    body,
421                    island_id: self.current_island,
422                }));
423            }
424        }
425
426        // Only trigger presupposition if followed by gerund complement
427        if self.check_presup_trigger() && self.is_followed_by_gerund() {
428            let presup_kind = match self.advance().kind {
429                TokenType::PresupTrigger(kind) => kind,
430                TokenType::Verb { lemma, .. } => {
431                    let s = self.interner.resolve(lemma).to_lowercase();
432                    crate::lexicon::lookup_presup_trigger(&s)
433                        .expect("Lexicon mismatch: Verb flagged as trigger but lookup failed")
434                }
435                _ => panic!("Expected presupposition trigger"),
436            };
437
438            let complement = if self.check_verb() {
439                let verb = self.consume_verb();
440                let modifiers = self.collect_adverbs();
441                self.build_verb_neo_event(verb, var_name, None, modifiers)
442            } else {
443                let unknown = self.interner.intern("?");
444                self.ctx.exprs.alloc(LogicExpr::Atom(unknown))
445            };
446
447            let verb_pred = match presup_kind {
448                PresupKind::Stop => self.ctx.exprs.alloc(LogicExpr::UnaryOp {
449                    op: TokenType::Not,
450                    operand: complement,
451                }),
452                PresupKind::Start | PresupKind::Continue => complement,
453                PresupKind::Regret | PresupKind::Realize | PresupKind::Know => complement,
454            };
455
456            let body = match quantifier_token {
457                TokenType::All | TokenType::Any => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
458                    left: subject_pred,
459                    op: TokenType::If,
460                    right: verb_pred,
461                }),
462                _ => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
463                    left: subject_pred,
464                    op: TokenType::And,
465                    right: verb_pred,
466                }),
467            };
468
469            let kind = match quantifier_token {
470                TokenType::All | TokenType::No => QuantifierKind::Universal,
471                TokenType::Some => QuantifierKind::Existential,
472                TokenType::Most => QuantifierKind::Most,
473                TokenType::Few => QuantifierKind::Few,
474                TokenType::Many => QuantifierKind::Many,
475                TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
476                TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
477                TokenType::AtMost(n) => QuantifierKind::AtMost(n),
478                _ => QuantifierKind::Universal,
479            };
480
481            self.in_negative_quantifier = was_in_negative_quantifier;
482            return Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
483                kind,
484                variable: var_name,
485                body,
486                island_id: self.current_island,
487            }));
488        }
489
490        if self.check_verb() {
491            let verb = self.consume_verb();
492            let mut args = vec![Term::Variable(var_name)];
493
494            if self.check_pronoun() {
495                let token = self.peek().clone();
496                if let TokenType::Pronoun { gender, .. } = token.kind {
497                    self.advance();
498                    if let Some(donkey_var) = self.resolve_donkey_pronoun(gender) {
499                        args.push(Term::Variable(donkey_var));
500                    } else {
501                        let resolved = self.resolve_pronoun(gender, Number::Singular)?;
502                        let term = match resolved {
503                            super::ResolvedPronoun::Variable(s) => Term::Variable(s),
504                            super::ResolvedPronoun::Constant(s) => Term::Constant(s),
505                        };
506                        args.push(term);
507                    }
508                }
509            } else if self.check_npi_object() {
510                let npi_token = self.advance().kind.clone();
511                let obj_var = self.next_var_name();
512
513                let restriction_name = match npi_token {
514                    TokenType::Anything => "Thing",
515                    TokenType::Anyone => "Person",
516                    _ => "Thing",
517                };
518
519                let restriction_sym = self.interner.intern(restriction_name);
520                let obj_restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
521                    name: restriction_sym,
522                    args: self.ctx.terms.alloc_slice([Term::Variable(obj_var)]),
523                    world: None,
524                });
525
526                let npi_modifiers = self.collect_adverbs();
527                let verb_with_obj = self.build_verb_neo_event(
528                    verb,
529                    var_name,
530                    Some(Term::Variable(obj_var)),
531                    npi_modifiers,
532                );
533
534                let npi_body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
535                    left: obj_restriction,
536                    op: TokenType::And,
537                    right: verb_with_obj,
538                });
539
540                let npi_quantified = self.ctx.exprs.alloc(LogicExpr::Quantifier {
541                    kind: QuantifierKind::Existential,
542                    variable: obj_var,
543                    body: npi_body,
544                    island_id: self.current_island,
545                });
546
547                let negated_npi = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
548                    op: TokenType::Not,
549                    operand: npi_quantified,
550                });
551
552                let body = match quantifier_token {
553                    TokenType::All | TokenType::No => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
554                        left: subject_pred,
555                        op: TokenType::If,
556                        right: negated_npi,
557                    }),
558                    _ => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
559                        left: subject_pred,
560                        op: TokenType::And,
561                        right: negated_npi,
562                    }),
563                };
564
565                let kind = match quantifier_token {
566                    TokenType::All | TokenType::No => QuantifierKind::Universal,
567                    TokenType::Some => QuantifierKind::Existential,
568                    TokenType::Most => QuantifierKind::Most,
569                    TokenType::Few => QuantifierKind::Few,
570                    TokenType::Many => QuantifierKind::Many,
571                    TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
572                    TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
573                    TokenType::AtMost(n) => QuantifierKind::AtMost(n),
574                    _ => QuantifierKind::Universal,
575                };
576
577                self.in_negative_quantifier = was_in_negative_quantifier;
578                return Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
579                    kind,
580                    variable: var_name,
581                    body,
582                    island_id: self.current_island,
583                }));
584            } else if self.check_quantifier() || self.check_article() {
585                let obj_quantifier = if self.check_quantifier() {
586                    Some(self.advance().kind.clone())
587                } else {
588                    let art = self.advance().kind.clone();
589                    if let TokenType::Article(def) = art {
590                        if def == Definiteness::Indefinite {
591                            Some(TokenType::Some)
592                        } else {
593                            None
594                        }
595                    } else {
596                        None
597                    }
598                };
599
600                let object = self.parse_noun_phrase(false)?;
601
602                if let Some(obj_q) = obj_quantifier {
603                    let obj_var = self.next_var_name();
604
605                    // Introduce object referent in DRS for cross-sentence anaphora (telescoping)
606                    // BUT: If inside "No X" quantifier, mark with NegationScope to block accessibility
607                    let obj_gender = Self::infer_noun_gender(self.interner.resolve(object.noun));
608                    let obj_number = if Self::is_plural_noun(self.interner.resolve(object.noun)) {
609                        Number::Plural
610                    } else {
611                        Number::Singular
612                    };
613                    if self.in_negative_quantifier {
614                        self.drs.introduce_referent_with_source(obj_var, object.noun, obj_gender, obj_number, ReferentSource::NegationScope);
615                    } else {
616                        self.drs.introduce_referent(obj_var, object.noun, obj_gender, obj_number);
617                    }
618
619                    let obj_restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
620                        name: object.noun,
621                        args: self.ctx.terms.alloc_slice([Term::Variable(obj_var)]),
622                        world: None,
623                    });
624
625                    let obj_modifiers = self.collect_adverbs();
626                    let verb_with_obj = self.build_verb_neo_event(
627                        verb,
628                        var_name,
629                        Some(Term::Variable(obj_var)),
630                        obj_modifiers,
631                    );
632
633                    let obj_kind = match obj_q {
634                        TokenType::All => QuantifierKind::Universal,
635                        TokenType::Some => QuantifierKind::Existential,
636                        TokenType::No => QuantifierKind::Universal,
637                        TokenType::Most => QuantifierKind::Most,
638                        TokenType::Few => QuantifierKind::Few,
639                        TokenType::Many => QuantifierKind::Many,
640                        TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
641                        TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
642                        TokenType::AtMost(n) => QuantifierKind::AtMost(n),
643                        _ => QuantifierKind::Existential,
644                    };
645
646                    let obj_body = match obj_q {
647                        TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
648                            left: obj_restriction,
649                            op: TokenType::If,
650                            right: verb_with_obj,
651                        }),
652                        TokenType::No => {
653                            let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
654                                op: TokenType::Not,
655                                operand: verb_with_obj,
656                            });
657                            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
658                                left: obj_restriction,
659                                op: TokenType::If,
660                                right: neg,
661                            })
662                        }
663                        _ => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
664                            left: obj_restriction,
665                            op: TokenType::And,
666                            right: verb_with_obj,
667                        }),
668                    };
669
670                    let obj_quantified = self.ctx.exprs.alloc(LogicExpr::Quantifier {
671                        kind: obj_kind,
672                        variable: obj_var,
673                        body: obj_body,
674                        island_id: self.current_island,
675                    });
676
677                    let subj_kind = match quantifier_token {
678                        TokenType::All | TokenType::No => QuantifierKind::Universal,
679                        TokenType::Any => {
680                            if self.is_negative_context() {
681                                QuantifierKind::Existential
682                            } else {
683                                QuantifierKind::Universal
684                            }
685                        }
686                        TokenType::Some => QuantifierKind::Existential,
687                        TokenType::Most => QuantifierKind::Most,
688                        TokenType::Few => QuantifierKind::Few,
689                        TokenType::Many => QuantifierKind::Many,
690                        TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
691                        TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
692                        TokenType::AtMost(n) => QuantifierKind::AtMost(n),
693                        _ => QuantifierKind::Universal,
694                    };
695
696                    let subj_body = match quantifier_token {
697                        TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
698                            left: subject_pred,
699                            op: TokenType::If,
700                            right: obj_quantified,
701                        }),
702                        TokenType::No => {
703                            let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
704                                op: TokenType::Not,
705                                operand: obj_quantified,
706                            });
707                            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
708                                left: subject_pred,
709                                op: TokenType::If,
710                                right: neg,
711                            })
712                        }
713                        _ => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
714                            left: subject_pred,
715                            op: TokenType::And,
716                            right: obj_quantified,
717                        }),
718                    };
719
720                    self.in_negative_quantifier = was_in_negative_quantifier;
721                    return Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
722                        kind: subj_kind,
723                        variable: var_name,
724                        body: subj_body,
725                        island_id: self.current_island,
726                    }));
727                } else {
728                    args.push(Term::Constant(object.noun));
729                }
730            } else if self.check_content_word() {
731                let object = self.parse_noun_phrase(false)?;
732                args.push(Term::Constant(object.noun));
733            }
734
735            // Extract object term from args if present (args[0] is subject, args[1] is object)
736            let obj_term = if args.len() > 1 {
737                Some(args.remove(1))
738            } else {
739                None
740            };
741            // Collect any trailing adverbs (e.g., "bark loudly")
742            let modifiers = self.collect_adverbs();
743            let verb_pred = self.build_verb_neo_event(verb, var_name, obj_term, modifiers);
744
745            let body = match quantifier_token {
746                TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
747                    left: subject_pred,
748                    op: TokenType::If,
749                    right: verb_pred,
750                }),
751                TokenType::Any => {
752                    if self.is_negative_context() {
753                        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
754                            left: subject_pred,
755                            op: TokenType::And,
756                            right: verb_pred,
757                        })
758                    } else {
759                        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
760                            left: subject_pred,
761                            op: TokenType::If,
762                            right: verb_pred,
763                        })
764                    }
765                }
766                TokenType::Some
767                | TokenType::Most
768                | TokenType::Few
769                | TokenType::Many
770                | TokenType::Cardinal(_)
771                | TokenType::AtLeast(_)
772                | TokenType::AtMost(_) => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
773                    left: subject_pred,
774                    op: TokenType::And,
775                    right: verb_pred,
776                }),
777                TokenType::No => {
778                    let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
779                        op: TokenType::Not,
780                        operand: verb_pred,
781                    });
782                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
783                        left: subject_pred,
784                        op: TokenType::If,
785                        right: neg,
786                    })
787                }
788                _ => {
789                    return Err(ParseError {
790                        kind: ParseErrorKind::UnknownQuantifier {
791                            found: quantifier_token.clone(),
792                        },
793                        span: self.current_span(),
794                    })
795                }
796            };
797
798            let kind = match quantifier_token {
799                TokenType::All | TokenType::No => QuantifierKind::Universal,
800                TokenType::Any => {
801                    if self.is_negative_context() {
802                        QuantifierKind::Existential
803                    } else {
804                        QuantifierKind::Universal
805                    }
806                }
807                TokenType::Some => QuantifierKind::Existential,
808                TokenType::Most => QuantifierKind::Most,
809                TokenType::Few => QuantifierKind::Few,
810                TokenType::Many => QuantifierKind::Many,
811                TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
812                TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
813                TokenType::AtMost(n) => QuantifierKind::AtMost(n),
814                _ => {
815                    return Err(ParseError {
816                        kind: ParseErrorKind::UnknownQuantifier {
817                            found: quantifier_token.clone(),
818                        },
819                        span: self.current_span(),
820                    })
821                }
822            };
823
824            let mut result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
825                kind,
826                variable: var_name,
827                body,
828                island_id: self.current_island,
829            });
830
831            for (_noun, donkey_var, used, wide_neg) in self.donkey_bindings.iter().rev() {
832                if *used {
833                    // Donkey anaphora: wrap with ∀ at outer scope
834                    result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
835                        kind: QuantifierKind::Universal,
836                        variable: *donkey_var,
837                        body: result,
838                        island_id: self.current_island,
839                    });
840                } else {
841                    // Non-donkey: wrap with ∃ INSIDE the restriction
842                    result = self.wrap_donkey_in_restriction(result, *donkey_var, *wide_neg);
843                }
844            }
845            self.donkey_bindings.clear();
846
847            self.in_negative_quantifier = was_in_negative_quantifier;
848            return Ok(result);
849        }
850
851        self.consume_copula()?;
852
853        let negative = self.match_token(&[TokenType::Not]);
854        let predicate_np = self.parse_noun_phrase(true)?;
855
856        let predicate_expr = self.ctx.exprs.alloc(LogicExpr::Predicate {
857            name: predicate_np.noun,
858            args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
859            world: None,
860        });
861
862        let final_predicate = if negative {
863            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
864                op: TokenType::Not,
865                operand: predicate_expr,
866            })
867        } else {
868            predicate_expr
869        };
870
871        let body = match quantifier_token {
872            TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
873                left: subject_pred,
874                op: TokenType::If,
875                right: final_predicate,
876            }),
877            TokenType::Any => {
878                if self.is_negative_context() {
879                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
880                        left: subject_pred,
881                        op: TokenType::And,
882                        right: final_predicate,
883                    })
884                } else {
885                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
886                        left: subject_pred,
887                        op: TokenType::If,
888                        right: final_predicate,
889                    })
890                }
891            }
892            TokenType::Some
893            | TokenType::Most
894            | TokenType::Few
895            | TokenType::Many
896            | TokenType::Cardinal(_)
897            | TokenType::AtLeast(_)
898            | TokenType::AtMost(_) => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
899                left: subject_pred,
900                op: TokenType::And,
901                right: final_predicate,
902            }),
903            TokenType::No => {
904                let neg_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
905                    name: predicate_np.noun,
906                    args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
907                    world: None,
908                });
909                let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
910                    op: TokenType::Not,
911                    operand: neg_pred,
912                });
913                self.ctx.exprs.alloc(LogicExpr::BinaryOp {
914                    left: subject_pred,
915                    op: TokenType::If,
916                    right: neg,
917                })
918            }
919            _ => {
920                return Err(ParseError {
921                    kind: ParseErrorKind::UnknownQuantifier {
922                        found: quantifier_token.clone(),
923                    },
924                    span: self.current_span(),
925                })
926            }
927        };
928
929        let kind = match quantifier_token {
930            TokenType::All | TokenType::No => QuantifierKind::Universal,
931            TokenType::Any => {
932                if self.is_negative_context() {
933                    QuantifierKind::Existential
934                } else {
935                    QuantifierKind::Universal
936                }
937            }
938            TokenType::Some => QuantifierKind::Existential,
939            TokenType::Most => QuantifierKind::Most,
940            TokenType::Few => QuantifierKind::Few,
941            TokenType::Many => QuantifierKind::Many,
942            TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
943            TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
944            TokenType::AtMost(n) => QuantifierKind::AtMost(n),
945            _ => {
946                return Err(ParseError {
947                    kind: ParseErrorKind::UnknownQuantifier {
948                        found: quantifier_token.clone(),
949                    },
950                    span: self.current_span(),
951                })
952            }
953        };
954
955        let mut result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
956            kind,
957            variable: var_name,
958            body,
959            island_id: self.current_island,
960        });
961
962        for (_noun, donkey_var, used, wide_neg) in self.donkey_bindings.iter().rev() {
963            if *used {
964                // Donkey anaphora: wrap with ∀ at outer scope
965                result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
966                    kind: QuantifierKind::Universal,
967                    variable: *donkey_var,
968                    body: result,
969                    island_id: self.current_island,
970                });
971            } else {
972                // Non-donkey: wrap with ∃ INSIDE the restriction
973                result = self.wrap_donkey_in_restriction(result, *donkey_var, *wide_neg);
974            }
975        }
976        self.donkey_bindings.clear();
977
978        self.in_negative_quantifier = was_in_negative_quantifier;
979        Ok(result)
980    }
981
982    fn parse_restriction(&mut self, var_name: Symbol) -> ParseResult<&'a LogicExpr<'a>> {
983        let mut conditions: Vec<&'a LogicExpr<'a>> = Vec::new();
984
985        loop {
986            if self.is_at_end() {
987                break;
988            }
989
990            let is_adjective = matches!(self.peek().kind, TokenType::Adjective(_));
991            if !is_adjective {
992                break;
993            }
994
995            let next_is_content = if self.current + 1 < self.tokens.len() {
996                matches!(
997                    self.tokens[self.current + 1].kind,
998                    TokenType::Noun(_) | TokenType::Adjective(_) | TokenType::ProperName(_)
999                )
1000            } else {
1001                false
1002            };
1003
1004            if next_is_content {
1005                if let TokenType::Adjective(adj) = self.advance().kind.clone() {
1006                    conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1007                        name: adj,
1008                        args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1009                        world: None,
1010                    }));
1011                }
1012            } else {
1013                break;
1014            }
1015        }
1016
1017        let noun = self.consume_content_word()?;
1018        conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1019            name: noun,
1020            args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1021            world: None,
1022        }));
1023
1024        while self.check(&TokenType::That) || self.check(&TokenType::Who) {
1025            self.advance();
1026            let clause_pred = self.parse_relative_clause(var_name)?;
1027            conditions.push(clause_pred);
1028        }
1029
1030        self.combine_with_and(conditions)
1031    }
1032
1033    fn parse_verb_phrase_for_restriction(&mut self, var_name: Symbol) -> ParseResult<&'a LogicExpr<'a>> {
1034        let var_term = Term::Variable(var_name);
1035        let verb = self.consume_verb();
1036        let verb_str_owned = self.interner.resolve(verb).to_string();
1037
1038        // Check EARLY if verb is lexically negative (e.g., "lacks" -> "Have" with negation)
1039        // This determines whether donkey bindings need wide scope negation
1040        let (canonical_verb, is_negative) = get_canonical_verb(&verb_str_owned.to_lowercase())
1041            .map(|(lemma, neg)| (self.interner.intern(lemma), neg))
1042            .unwrap_or((verb, false));
1043
1044        // Determine if this binding needs wide scope negation wrapping
1045        let needs_wide_scope = is_negative && self.negative_scope_mode == NegativeScopeMode::Wide;
1046
1047        if Lexer::is_raising_verb(&verb_str_owned) && self.check_to() {
1048            self.advance();
1049            if self.check_verb() {
1050                let inf_verb = self.consume_verb();
1051                let inf_verb_str = self.interner.resolve(inf_verb).to_lowercase();
1052
1053                if inf_verb_str == "be" && self.check_content_word() {
1054                    let adj = self.consume_content_word()?;
1055                    let embedded = self.ctx.exprs.alloc(LogicExpr::Predicate {
1056                        name: adj,
1057                        args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1058                        world: None,
1059                    });
1060                    return Ok(self.ctx.exprs.alloc(LogicExpr::Scopal {
1061                        operator: verb,
1062                        body: embedded,
1063                    }));
1064                }
1065
1066                let embedded = self.ctx.exprs.alloc(LogicExpr::Predicate {
1067                    name: inf_verb,
1068                    args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1069                    world: None,
1070                });
1071                return Ok(self.ctx.exprs.alloc(LogicExpr::Scopal {
1072                    operator: verb,
1073                    body: embedded,
1074                }));
1075            } else if self.check(&TokenType::Is) || self.check(&TokenType::Are) {
1076                self.advance();
1077                if self.check_content_word() {
1078                    let adj = self.consume_content_word()?;
1079                    let embedded = self.ctx.exprs.alloc(LogicExpr::Predicate {
1080                        name: adj,
1081                        args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1082                        world: None,
1083                    });
1084                    return Ok(self.ctx.exprs.alloc(LogicExpr::Scopal {
1085                        operator: verb,
1086                        body: embedded,
1087                    }));
1088                }
1089            }
1090        }
1091
1092        let mut args = vec![var_term];
1093        let mut extra_conditions: Vec<&'a LogicExpr<'a>> = Vec::new();
1094
1095        if self.check(&TokenType::Reflexive) {
1096            self.advance();
1097            args.push(Term::Variable(var_name));
1098        } else if (self.check_content_word() || self.check_article()) && !self.check_verb() {
1099            if matches!(
1100                self.peek().kind,
1101                TokenType::Article(Definiteness::Indefinite)
1102            ) {
1103                self.advance();
1104                let noun = self.consume_content_word()?;
1105                let donkey_var = self.next_var_name();
1106
1107                if needs_wide_scope {
1108                    // === WIDE SCOPE MODE ===
1109                    // Build ¬∃y(Key(y) ∧ ∃e(Have(e) ∧ Agent(e,x) ∧ Theme(e,y))) directly
1110                    //
1111                    // We capture the binding HERE and return the complete structure.
1112                    // DO NOT push to donkey_bindings - that would leak y to outer scope.
1113
1114                    // Build: Key(y)
1115                    let restriction_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1116                        name: noun,
1117                        args: self.ctx.terms.alloc_slice([Term::Variable(donkey_var)]),
1118                        world: None,
1119                    });
1120
1121                    // Build: ∃e(Have(e) ∧ Agent(e,x) ∧ Theme(e,y)) using Neo-Davidsonian semantics
1122                    // IMPORTANT: Use build_verb_neo_event() for consistent Full-tier formatting
1123                    let inner_modifiers = self.collect_adverbs();
1124                    let verb_pred = self.build_verb_neo_event(
1125                        canonical_verb,
1126                        var_name,
1127                        Some(Term::Variable(donkey_var)),
1128                        inner_modifiers,
1129                    );
1130
1131                    // Build: Key(y) ∧ ∃e(Have(e) ∧ Agent(e,x) ∧ Theme(e,y))
1132                    let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1133                        left: restriction_pred,
1134                        op: TokenType::And,
1135                        right: verb_pred,
1136                    });
1137
1138                    // Build: ∃y(Key(y) ∧ ∃e(Have(e) ∧ ...))
1139                    let existential = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1140                        kind: QuantifierKind::Existential,
1141                        variable: donkey_var,
1142                        body,
1143                        island_id: self.current_island,
1144                    });
1145
1146                    // Build: ¬∃y(Key(y) ∧ ∃e(Have(e) ∧ ...))
1147                    let negated_existential = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1148                        op: TokenType::Not,
1149                        operand: existential,
1150                    });
1151
1152                    // Return the complete wide-scope structure directly
1153                    return Ok(negated_existential);
1154                }
1155
1156                // === NARROW SCOPE MODE ===
1157                // Push binding for later processing (normal donkey binding flow)
1158                self.donkey_bindings.push((noun, donkey_var, false, false));
1159
1160                extra_conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1161                    name: noun,
1162                    args: self.ctx.terms.alloc_slice([Term::Variable(donkey_var)]),
1163                    world: None,
1164                }));
1165
1166                args.push(Term::Variable(donkey_var));
1167            } else {
1168                let object = self.parse_noun_phrase(false)?;
1169
1170                if self.check(&TokenType::That) || self.check(&TokenType::Who) {
1171                    self.advance();
1172                    let nested_var = self.next_var_name();
1173                    let nested_rel = self.parse_relative_clause(nested_var)?;
1174
1175                    extra_conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1176                        name: object.noun,
1177                        args: self.ctx.terms.alloc_slice([Term::Variable(nested_var)]),
1178                        world: None,
1179                    }));
1180                    extra_conditions.push(nested_rel);
1181                    args.push(Term::Variable(nested_var));
1182                } else {
1183                    args.push(Term::Constant(object.noun));
1184                }
1185            }
1186        }
1187
1188        while self.check_preposition() {
1189            self.advance();
1190            if self.check(&TokenType::Reflexive) {
1191                self.advance();
1192                args.push(Term::Variable(var_name));
1193            } else if self.check_content_word() || self.check_article() {
1194                let object = self.parse_noun_phrase(false)?;
1195
1196                if self.check(&TokenType::That) || self.check(&TokenType::Who) {
1197                    self.advance();
1198                    let nested_var = self.next_var_name();
1199                    let nested_rel = self.parse_relative_clause(nested_var)?;
1200                    extra_conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1201                        name: object.noun,
1202                        args: self.ctx.terms.alloc_slice([Term::Variable(nested_var)]),
1203                        world: None,
1204                    }));
1205                    extra_conditions.push(nested_rel);
1206                    args.push(Term::Variable(nested_var));
1207                } else {
1208                    args.push(Term::Constant(object.noun));
1209                }
1210            }
1211        }
1212
1213        // Use the canonical verb determined at top of function
1214        // Extract object term from args if present (args[0] is subject, args[1] is object)
1215        let obj_term = if args.len() > 1 {
1216            Some(args.remove(1))
1217        } else {
1218            None
1219        };
1220        let final_modifiers = self.collect_adverbs();
1221        let base_pred = self.build_verb_neo_event(canonical_verb, var_name, obj_term, final_modifiers);
1222
1223        // Wrap in negation only for NARROW scope mode (de re reading)
1224        // Wide scope mode: negation handled via donkey binding flag in wrap_donkey_in_restriction
1225        // - Narrow: ∃y(Key(y) ∧ ¬Have(x,y)) - "missing ANY key"
1226        // - Wide:   ¬∃y(Key(y) ∧ Have(x,y)) - "has NO keys"
1227        let verb_pred = if is_negative && self.negative_scope_mode == NegativeScopeMode::Narrow {
1228            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1229                op: TokenType::Not,
1230                operand: base_pred,
1231            })
1232        } else {
1233            base_pred
1234        };
1235
1236        if extra_conditions.is_empty() {
1237            Ok(verb_pred)
1238        } else {
1239            extra_conditions.push(verb_pred);
1240            self.combine_with_and(extra_conditions)
1241        }
1242    }
1243
1244    fn combine_with_and(&self, mut exprs: Vec<&'a LogicExpr<'a>>) -> ParseResult<&'a LogicExpr<'a>> {
1245        if exprs.is_empty() {
1246            return Err(ParseError {
1247                kind: ParseErrorKind::EmptyRestriction,
1248                span: self.current_span(),
1249            });
1250        }
1251        if exprs.len() == 1 {
1252            return Ok(exprs.remove(0));
1253        }
1254        let mut root = exprs.remove(0);
1255        for expr in exprs {
1256            root = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1257                left: root,
1258                op: TokenType::And,
1259                right: expr,
1260            });
1261        }
1262        Ok(root)
1263    }
1264
1265    fn wrap_with_definiteness_full(
1266        &mut self,
1267        np: &NounPhrase<'a>,
1268        predicate: &'a LogicExpr<'a>,
1269    ) -> ParseResult<&'a LogicExpr<'a>> {
1270        let result = self.wrap_with_definiteness_and_adjectives_and_pps(
1271            np.definiteness,
1272            np.noun,
1273            np.adjectives,
1274            np.pps,
1275            predicate,
1276        )?;
1277
1278        // If NP has a superlative, add the superlative constraint
1279        if let Some(adj) = np.superlative {
1280            let superlative_expr = self.ctx.exprs.alloc(LogicExpr::Superlative {
1281                adjective: adj,
1282                subject: self.ctx.terms.alloc(Term::Constant(np.noun)),
1283                domain: np.noun,
1284            });
1285            Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1286                left: result,
1287                op: TokenType::And,
1288                right: superlative_expr,
1289            }))
1290        } else {
1291            Ok(result)
1292        }
1293    }
1294
1295    fn wrap_with_definiteness(
1296        &mut self,
1297        definiteness: Option<Definiteness>,
1298        noun: Symbol,
1299        predicate: &'a LogicExpr<'a>,
1300    ) -> ParseResult<&'a LogicExpr<'a>> {
1301        self.wrap_with_definiteness_and_adjectives_and_pps(definiteness, noun, &[], &[], predicate)
1302    }
1303
1304    fn wrap_with_definiteness_and_adjectives(
1305        &mut self,
1306        definiteness: Option<Definiteness>,
1307        noun: Symbol,
1308        adjectives: &[Symbol],
1309        predicate: &'a LogicExpr<'a>,
1310    ) -> ParseResult<&'a LogicExpr<'a>> {
1311        self.wrap_with_definiteness_and_adjectives_and_pps(
1312            definiteness,
1313            noun,
1314            adjectives,
1315            &[],
1316            predicate,
1317        )
1318    }
1319
1320    fn wrap_with_definiteness_and_adjectives_and_pps(
1321        &mut self,
1322        definiteness: Option<Definiteness>,
1323        noun: Symbol,
1324        adjectives: &[Symbol],
1325        pps: &[&'a LogicExpr<'a>],
1326        predicate: &'a LogicExpr<'a>,
1327    ) -> ParseResult<&'a LogicExpr<'a>> {
1328        match definiteness {
1329            Some(Definiteness::Indefinite) => {
1330                let var = self.next_var_name();
1331
1332                // Introduce referent into DRS for cross-sentence anaphora
1333                // If inside a "No" quantifier, mark as NegationScope (inaccessible)
1334                let gender = Self::infer_noun_gender(self.interner.resolve(noun));
1335                let number = if Self::is_plural_noun(self.interner.resolve(noun)) {
1336                    Number::Plural
1337                } else {
1338                    Number::Singular
1339                };
1340                if self.in_negative_quantifier {
1341                    self.drs.introduce_referent_with_source(var, noun, gender, number, ReferentSource::NegationScope);
1342                } else {
1343                    self.drs.introduce_referent(var, noun, gender, number);
1344                }
1345
1346                let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1347                    name: noun,
1348                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1349                    world: None,
1350                });
1351
1352                for adj in adjectives {
1353                    let adj_str = self.interner.resolve(*adj).to_lowercase();
1354                    let adj_pred = if is_subsective(&adj_str) {
1355                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1356                            name: *adj,
1357                            args: self.ctx.terms.alloc_slice([
1358                                Term::Variable(var),
1359                                Term::Intension(noun),
1360                            ]),
1361                            world: None,
1362                        })
1363                    } else {
1364                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1365                            name: *adj,
1366                            args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1367                            world: None,
1368                        })
1369                    };
1370                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1371                        left: restriction,
1372                        op: TokenType::And,
1373                        right: adj_pred,
1374                    });
1375                }
1376
1377                for pp in pps {
1378                    let substituted_pp = self.substitute_pp_placeholder(pp, var);
1379                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1380                        left: restriction,
1381                        op: TokenType::And,
1382                        right: substituted_pp,
1383                    });
1384                }
1385
1386                let substituted = self.substitute_constant_with_var_sym(predicate, noun, var)?;
1387                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1388                    left: restriction,
1389                    op: TokenType::And,
1390                    right: substituted,
1391                });
1392                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1393                    kind: QuantifierKind::Existential,
1394                    variable: var,
1395                    body,
1396                    island_id: self.current_island,
1397                }))
1398            }
1399            Some(Definiteness::Definite) => {
1400                let noun_str = self.interner.resolve(noun).to_string();
1401
1402                if Self::is_plural_noun(&noun_str) {
1403                    let singular = Self::singularize_noun(&noun_str);
1404                    let singular_sym = self.interner.intern(&singular);
1405                    let sigma_term = Term::Sigma(singular_sym);
1406
1407                    let substituted =
1408                        self.substitute_constant_with_sigma(predicate, noun, sigma_term)?;
1409
1410                    let verb_name = self.find_main_verb_name(predicate);
1411                    let is_collective = verb_name
1412                        .map(|v| {
1413                            let lemma = self.interner.resolve(v);
1414                            Lexer::is_collective_verb(lemma)
1415                                || (Lexer::is_mixed_verb(lemma) && self.collective_mode)
1416                        })
1417                        .unwrap_or(false);
1418
1419                    // Introduce definite plural referent to DRS for cross-sentence pronoun resolution
1420                    // E.g., "The dogs ran. They barked." - "they" refers to "dogs"
1421                    // Definite descriptions presuppose existence, so they should be globally accessible.
1422                    let gender = Gender::Unknown;  // Plural entities have unknown gender
1423                    self.drs.introduce_referent_with_source(singular_sym, singular_sym, gender, Number::Plural, ReferentSource::MainClause);
1424
1425                    if is_collective {
1426                        Ok(substituted)
1427                    } else {
1428                        Ok(self.ctx.exprs.alloc(LogicExpr::Distributive {
1429                            predicate: substituted,
1430                        }))
1431                    }
1432                } else {
1433                    let x = self.next_var_name();
1434                    let y = self.next_var_name();
1435
1436                    let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1437                        name: noun,
1438                        args: self.ctx.terms.alloc_slice([Term::Variable(x)]),
1439                        world: None,
1440                    });
1441
1442                    for adj in adjectives {
1443                        let adj_str = self.interner.resolve(*adj).to_lowercase();
1444                        let adj_pred = if is_subsective(&adj_str) {
1445                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1446                                name: *adj,
1447                                args: self.ctx.terms.alloc_slice([
1448                                    Term::Variable(x),
1449                                    Term::Intension(noun),
1450                                ]),
1451                                world: None,
1452                            })
1453                        } else {
1454                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1455                                name: *adj,
1456                                args: self.ctx.terms.alloc_slice([Term::Variable(x)]),
1457                                world: None,
1458                            })
1459                        };
1460                        restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1461                            left: restriction,
1462                            op: TokenType::And,
1463                            right: adj_pred,
1464                        });
1465                    }
1466
1467                    for pp in pps {
1468                        let substituted_pp = self.substitute_pp_placeholder(pp, x);
1469                        restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1470                            left: restriction,
1471                            op: TokenType::And,
1472                            right: substituted_pp,
1473                        });
1474                    }
1475
1476                    // Bridging anaphora: check if this noun is a part of a previously mentioned whole
1477                    // E.g., "I bought a car. The engine smoked." - engine is part of car
1478                    let has_prior_antecedent = self.drs.resolve_definite(
1479                        self.drs.current_box_index(),
1480                        noun
1481                    ).is_some();
1482
1483                    if !has_prior_antecedent {
1484                        if let Some((whole_var, _whole_name)) = self.drs.resolve_bridging(self.interner, noun) {
1485                            let part_of_sym = self.interner.intern("PartOf");
1486                            let part_of_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1487                                name: part_of_sym,
1488                                args: self.ctx.terms.alloc_slice([
1489                                    Term::Variable(x),
1490                                    Term::Constant(whole_var),
1491                                ]),
1492                                world: None,
1493                            });
1494                            restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1495                                left: restriction,
1496                                op: TokenType::And,
1497                                right: part_of_pred,
1498                            });
1499                        }
1500                    }
1501
1502                    // Introduce definite referent to DRS for cross-sentence pronoun resolution
1503                    // E.g., "The engine smoked. It broke." - "it" refers to "engine"
1504                    // Definite descriptions presuppose existence, so they should be globally
1505                    // accessible even when introduced inside conditional antecedents.
1506                    let gender = Self::infer_noun_gender(self.interner.resolve(noun));
1507                    let number = if Self::is_plural_noun(self.interner.resolve(noun)) {
1508                        Number::Plural
1509                    } else {
1510                        Number::Singular
1511                    };
1512                    self.drs.introduce_referent_with_source(x, noun, gender, number, ReferentSource::MainClause);
1513
1514                    let mut y_restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1515                        name: noun,
1516                        args: self.ctx.terms.alloc_slice([Term::Variable(y)]),
1517                        world: None,
1518                    });
1519                    for adj in adjectives {
1520                        let adj_str = self.interner.resolve(*adj).to_lowercase();
1521                        let adj_pred = if is_subsective(&adj_str) {
1522                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1523                                name: *adj,
1524                                args: self.ctx.terms.alloc_slice([
1525                                    Term::Variable(y),
1526                                    Term::Intension(noun),
1527                                ]),
1528                                world: None,
1529                            })
1530                        } else {
1531                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1532                                name: *adj,
1533                                args: self.ctx.terms.alloc_slice([Term::Variable(y)]),
1534                                world: None,
1535                            })
1536                        };
1537                        y_restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1538                            left: y_restriction,
1539                            op: TokenType::And,
1540                            right: adj_pred,
1541                        });
1542                    }
1543
1544                    for pp in pps {
1545                        let substituted_pp = self.substitute_pp_placeholder(pp, y);
1546                        y_restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1547                            left: y_restriction,
1548                            op: TokenType::And,
1549                            right: substituted_pp,
1550                        });
1551                    }
1552
1553                    let identity = self.ctx.exprs.alloc(LogicExpr::Identity {
1554                        left: self.ctx.terms.alloc(Term::Variable(y)),
1555                        right: self.ctx.terms.alloc(Term::Variable(x)),
1556                    });
1557                    let uniqueness_body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1558                        left: y_restriction,
1559                        op: TokenType::If,
1560                        right: identity,
1561                    });
1562                    let uniqueness = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1563                        kind: QuantifierKind::Universal,
1564                        variable: y,
1565                        body: uniqueness_body,
1566                        island_id: self.current_island,
1567                    });
1568
1569                    let main_pred = self.substitute_constant_with_var_sym(predicate, noun, x)?;
1570
1571                    let inner = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1572                        left: restriction,
1573                        op: TokenType::And,
1574                        right: uniqueness,
1575                    });
1576                    let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1577                        left: inner,
1578                        op: TokenType::And,
1579                        right: main_pred,
1580                    });
1581
1582                    Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1583                        kind: QuantifierKind::Existential,
1584                        variable: x,
1585                        body,
1586                        island_id: self.current_island,
1587                    }))
1588                }
1589            }
1590            Some(Definiteness::Proximal) | Some(Definiteness::Distal) => {
1591                let var = self.next_var_name();
1592
1593                let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1594                    name: noun,
1595                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1596                    world: None,
1597                });
1598
1599                let deictic_name = if matches!(definiteness, Some(Definiteness::Proximal)) {
1600                    self.interner.intern("Proximal")
1601                } else {
1602                    self.interner.intern("Distal")
1603                };
1604                let deictic_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1605                    name: deictic_name,
1606                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1607                    world: None,
1608                });
1609                restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1610                    left: restriction,
1611                    op: TokenType::And,
1612                    right: deictic_pred,
1613                });
1614
1615                for adj in adjectives {
1616                    let adj_str = self.interner.resolve(*adj).to_lowercase();
1617                    let adj_pred = if is_subsective(&adj_str) {
1618                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1619                            name: *adj,
1620                            args: self.ctx.terms.alloc_slice([
1621                                Term::Variable(var),
1622                                Term::Intension(noun),
1623                            ]),
1624                            world: None,
1625                        })
1626                    } else {
1627                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1628                            name: *adj,
1629                            args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1630                            world: None,
1631                        })
1632                    };
1633                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1634                        left: restriction,
1635                        op: TokenType::And,
1636                        right: adj_pred,
1637                    });
1638                }
1639
1640                for pp in pps {
1641                    let substituted_pp = self.substitute_pp_placeholder(pp, var);
1642                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1643                        left: restriction,
1644                        op: TokenType::And,
1645                        right: substituted_pp,
1646                    });
1647                }
1648
1649                let substituted = self.substitute_constant_with_var_sym(predicate, noun, var)?;
1650                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1651                    left: restriction,
1652                    op: TokenType::And,
1653                    right: substituted,
1654                });
1655                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1656                    kind: QuantifierKind::Existential,
1657                    variable: var,
1658                    body,
1659                    island_id: self.current_island,
1660                }))
1661            }
1662            None => Ok(predicate),
1663        }
1664    }
1665
1666    fn wrap_with_definiteness_for_object(
1667        &mut self,
1668        definiteness: Option<Definiteness>,
1669        noun: Symbol,
1670        predicate: &'a LogicExpr<'a>,
1671    ) -> ParseResult<&'a LogicExpr<'a>> {
1672        match definiteness {
1673            Some(Definiteness::Indefinite) => {
1674                let var = self.next_var_name();
1675
1676                // Introduce referent into DRS for cross-sentence anaphora
1677                // If inside a "No" quantifier, mark as NegationScope (inaccessible)
1678                let gender = Self::infer_noun_gender(self.interner.resolve(noun));
1679                let number = if Self::is_plural_noun(self.interner.resolve(noun)) {
1680                    Number::Plural
1681                } else {
1682                    Number::Singular
1683                };
1684                if self.in_negative_quantifier {
1685                    self.drs.introduce_referent_with_source(var, noun, gender, number, ReferentSource::NegationScope);
1686                } else {
1687                    self.drs.introduce_referent(var, noun, gender, number);
1688                }
1689
1690                let type_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1691                    name: noun,
1692                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1693                    world: None,
1694                });
1695                let substituted = self.substitute_constant_with_var(predicate, noun, var)?;
1696                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1697                    left: type_pred,
1698                    op: TokenType::And,
1699                    right: substituted,
1700                });
1701                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1702                    kind: QuantifierKind::Existential,
1703                    variable: var,
1704                    body,
1705                    island_id: self.current_island,
1706                }))
1707            }
1708            Some(Definiteness::Definite) => {
1709                let x = self.next_var_name();
1710                let y = self.next_var_name();
1711
1712                let type_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1713                    name: noun,
1714                    args: self.ctx.terms.alloc_slice([Term::Variable(x)]),
1715                    world: None,
1716                });
1717
1718                let identity = self.ctx.exprs.alloc(LogicExpr::Identity {
1719                    left: self.ctx.terms.alloc(Term::Variable(y)),
1720                    right: self.ctx.terms.alloc(Term::Variable(x)),
1721                });
1722                let inner_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1723                    name: noun,
1724                    args: self.ctx.terms.alloc_slice([Term::Variable(y)]),
1725                    world: None,
1726                });
1727                let uniqueness_body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1728                    left: inner_pred,
1729                    op: TokenType::If,
1730                    right: identity,
1731                });
1732                let uniqueness = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1733                    kind: QuantifierKind::Universal,
1734                    variable: y,
1735                    body: uniqueness_body,
1736                    island_id: self.current_island,
1737                });
1738
1739                let main_pred = self.substitute_constant_with_var(predicate, noun, x)?;
1740
1741                let type_and_unique = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1742                    left: type_pred,
1743                    op: TokenType::And,
1744                    right: uniqueness,
1745                });
1746                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1747                    left: type_and_unique,
1748                    op: TokenType::And,
1749                    right: main_pred,
1750                });
1751
1752                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1753                    kind: QuantifierKind::Existential,
1754                    variable: x,
1755                    body,
1756                    island_id: self.current_island,
1757                }))
1758            }
1759            Some(Definiteness::Proximal) | Some(Definiteness::Distal) => {
1760                let var = self.next_var_name();
1761
1762                let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1763                    name: noun,
1764                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1765                    world: None,
1766                });
1767
1768                let deictic_name = if matches!(definiteness, Some(Definiteness::Proximal)) {
1769                    self.interner.intern("Proximal")
1770                } else {
1771                    self.interner.intern("Distal")
1772                };
1773                let deictic_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1774                    name: deictic_name,
1775                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1776                    world: None,
1777                });
1778                restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1779                    left: restriction,
1780                    op: TokenType::And,
1781                    right: deictic_pred,
1782                });
1783
1784                let substituted = self.substitute_constant_with_var(predicate, noun, var)?;
1785                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1786                    left: restriction,
1787                    op: TokenType::And,
1788                    right: substituted,
1789                });
1790                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1791                    kind: QuantifierKind::Existential,
1792                    variable: var,
1793                    body,
1794                    island_id: self.current_island,
1795                }))
1796            }
1797            None => Ok(predicate),
1798        }
1799    }
1800
1801    fn substitute_pp_placeholder(&mut self, pp: &'a LogicExpr<'a>, var: Symbol) -> &'a LogicExpr<'a> {
1802        let placeholder = self.interner.intern("_PP_SELF_");
1803        match pp {
1804            LogicExpr::Predicate { name, args, .. } => {
1805                let new_args: Vec<Term<'a>> = args
1806                    .iter()
1807                    .map(|arg| match arg {
1808                        Term::Variable(v) if *v == placeholder => Term::Variable(var),
1809                        other => *other,
1810                    })
1811                    .collect();
1812                self.ctx.exprs.alloc(LogicExpr::Predicate {
1813                    name: *name,
1814                    args: self.ctx.terms.alloc_slice(new_args),
1815                    world: None,
1816                })
1817            }
1818            _ => pp,
1819        }
1820    }
1821
1822    fn substitute_constant_with_var(
1823        &self,
1824        expr: &'a LogicExpr<'a>,
1825        constant_name: Symbol,
1826        var_name: Symbol,
1827    ) -> ParseResult<&'a LogicExpr<'a>> {
1828        match expr {
1829            LogicExpr::Predicate { name, args, .. } => {
1830                let new_args: Vec<Term<'a>> = args
1831                    .iter()
1832                    .map(|arg| match arg {
1833                        Term::Constant(c) if *c == constant_name => Term::Variable(var_name),
1834                        Term::Constant(c) => Term::Constant(*c),
1835                        Term::Variable(v) => Term::Variable(*v),
1836                        Term::Function(n, a) => Term::Function(*n, *a),
1837                        Term::Group(m) => Term::Group(*m),
1838                        Term::Possessed { possessor, possessed } => Term::Possessed {
1839                            possessor: *possessor,
1840                            possessed: *possessed,
1841                        },
1842                        Term::Sigma(p) => Term::Sigma(*p),
1843                        Term::Intension(p) => Term::Intension(*p),
1844                        Term::Proposition(e) => Term::Proposition(*e),
1845                        Term::Value { kind, unit, dimension } => Term::Value {
1846                            kind: *kind,
1847                            unit: *unit,
1848                            dimension: *dimension,
1849                        },
1850                    })
1851                    .collect();
1852                Ok(self.ctx.exprs.alloc(LogicExpr::Predicate {
1853                    name: *name,
1854                    args: self.ctx.terms.alloc_slice(new_args),
1855                    world: None,
1856                }))
1857            }
1858            LogicExpr::Temporal { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
1859                operator: *operator,
1860                body: self.substitute_constant_with_var(body, constant_name, var_name)?,
1861            })),
1862            LogicExpr::Aspectual { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Aspectual {
1863                operator: *operator,
1864                body: self.substitute_constant_with_var(body, constant_name, var_name)?,
1865            })),
1866            LogicExpr::UnaryOp { op, operand } => Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1867                op: op.clone(),
1868                operand: self.substitute_constant_with_var(operand, constant_name, var_name)?,
1869            })),
1870            LogicExpr::BinaryOp { left, op, right } => Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1871                left: self.substitute_constant_with_var(left, constant_name, var_name)?,
1872                op: op.clone(),
1873                right: self.substitute_constant_with_var(right, constant_name, var_name)?,
1874            })),
1875            LogicExpr::Event { predicate, adverbs } => Ok(self.ctx.exprs.alloc(LogicExpr::Event {
1876                predicate: self.substitute_constant_with_var(predicate, constant_name, var_name)?,
1877                adverbs: *adverbs,
1878            })),
1879            LogicExpr::TemporalAnchor { anchor, body } => {
1880                Ok(self.ctx.exprs.alloc(LogicExpr::TemporalAnchor {
1881                    anchor: *anchor,
1882                    body: self.substitute_constant_with_var(body, constant_name, var_name)?,
1883                }))
1884            }
1885            LogicExpr::NeoEvent(data) => {
1886                // Substitute constants in thematic roles (Agent, Theme, etc.)
1887                let new_roles: Vec<(crate::ast::ThematicRole, Term<'a>)> = data
1888                    .roles
1889                    .iter()
1890                    .map(|(role, term)| {
1891                        let new_term = match term {
1892                            Term::Constant(c) if *c == constant_name => Term::Variable(var_name),
1893                            Term::Constant(c) => Term::Constant(*c),
1894                            Term::Variable(v) => Term::Variable(*v),
1895                            Term::Function(n, a) => Term::Function(*n, *a),
1896                            Term::Group(m) => Term::Group(*m),
1897                            Term::Possessed { possessor, possessed } => Term::Possessed {
1898                                possessor: *possessor,
1899                                possessed: *possessed,
1900                            },
1901                            Term::Sigma(p) => Term::Sigma(*p),
1902                            Term::Intension(p) => Term::Intension(*p),
1903                            Term::Proposition(e) => Term::Proposition(*e),
1904                            Term::Value { kind, unit, dimension } => Term::Value {
1905                                kind: *kind,
1906                                unit: *unit,
1907                                dimension: *dimension,
1908                            },
1909                        };
1910                        (*role, new_term)
1911                    })
1912                    .collect();
1913                Ok(self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(crate::ast::NeoEventData {
1914                    event_var: data.event_var,
1915                    verb: data.verb,
1916                    roles: self.ctx.roles.alloc_slice(new_roles),
1917                    modifiers: data.modifiers,
1918                    suppress_existential: data.suppress_existential,
1919                    world: None,
1920                }))))
1921            }
1922            // Recurse into nested quantifiers to substitute constants in their bodies
1923            LogicExpr::Quantifier { kind, variable, body, island_id } => {
1924                let new_body = self.substitute_constant_with_var(body, constant_name, var_name)?;
1925                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1926                    kind: *kind,
1927                    variable: *variable,
1928                    body: new_body,
1929                    island_id: *island_id,
1930                }))
1931            }
1932            _ => Ok(expr),
1933        }
1934    }
1935
1936    fn substitute_constant_with_var_sym(
1937        &self,
1938        expr: &'a LogicExpr<'a>,
1939        constant_name: Symbol,
1940        var_name: Symbol,
1941    ) -> ParseResult<&'a LogicExpr<'a>> {
1942        self.substitute_constant_with_var(expr, constant_name, var_name)
1943    }
1944
1945    fn substitute_constant_with_sigma(
1946        &self,
1947        expr: &'a LogicExpr<'a>,
1948        constant_name: Symbol,
1949        sigma_term: Term<'a>,
1950    ) -> ParseResult<&'a LogicExpr<'a>> {
1951        match expr {
1952            LogicExpr::Predicate { name, args, .. } => {
1953                let new_args: Vec<Term<'a>> = args
1954                    .iter()
1955                    .map(|arg| match arg {
1956                        Term::Constant(c) if *c == constant_name => sigma_term.clone(),
1957                        Term::Constant(c) => Term::Constant(*c),
1958                        Term::Variable(v) => Term::Variable(*v),
1959                        Term::Function(n, a) => Term::Function(*n, *a),
1960                        Term::Group(m) => Term::Group(*m),
1961                        Term::Possessed { possessor, possessed } => Term::Possessed {
1962                            possessor: *possessor,
1963                            possessed: *possessed,
1964                        },
1965                        Term::Sigma(p) => Term::Sigma(*p),
1966                        Term::Intension(p) => Term::Intension(*p),
1967                        Term::Proposition(e) => Term::Proposition(*e),
1968                        Term::Value { kind, unit, dimension } => Term::Value {
1969                            kind: *kind,
1970                            unit: *unit,
1971                            dimension: *dimension,
1972                        },
1973                    })
1974                    .collect();
1975                Ok(self.ctx.exprs.alloc(LogicExpr::Predicate {
1976                    name: *name,
1977                    args: self.ctx.terms.alloc_slice(new_args),
1978                    world: None,
1979                }))
1980            }
1981            LogicExpr::Temporal { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
1982                operator: *operator,
1983                body: self.substitute_constant_with_sigma(body, constant_name, sigma_term)?,
1984            })),
1985            LogicExpr::Aspectual { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Aspectual {
1986                operator: *operator,
1987                body: self.substitute_constant_with_sigma(body, constant_name, sigma_term)?,
1988            })),
1989            LogicExpr::UnaryOp { op, operand } => Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1990                op: op.clone(),
1991                operand: self.substitute_constant_with_sigma(operand, constant_name, sigma_term)?,
1992            })),
1993            LogicExpr::BinaryOp { left, op, right } => Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1994                left: self.substitute_constant_with_sigma(
1995                    left,
1996                    constant_name,
1997                    sigma_term.clone(),
1998                )?,
1999                op: op.clone(),
2000                right: self.substitute_constant_with_sigma(right, constant_name, sigma_term)?,
2001            })),
2002            LogicExpr::Event { predicate, adverbs } => Ok(self.ctx.exprs.alloc(LogicExpr::Event {
2003                predicate: self.substitute_constant_with_sigma(
2004                    predicate,
2005                    constant_name,
2006                    sigma_term,
2007                )?,
2008                adverbs: *adverbs,
2009            })),
2010            LogicExpr::TemporalAnchor { anchor, body } => {
2011                Ok(self.ctx.exprs.alloc(LogicExpr::TemporalAnchor {
2012                    anchor: *anchor,
2013                    body: self.substitute_constant_with_sigma(body, constant_name, sigma_term)?,
2014                }))
2015            }
2016            LogicExpr::NeoEvent(data) => {
2017                let new_roles: Vec<(crate::ast::ThematicRole, Term<'a>)> = data
2018                    .roles
2019                    .iter()
2020                    .map(|(role, term)| {
2021                        let new_term = match term {
2022                            Term::Constant(c) if *c == constant_name => sigma_term.clone(),
2023                            Term::Constant(c) => Term::Constant(*c),
2024                            Term::Variable(v) => Term::Variable(*v),
2025                            Term::Function(n, a) => Term::Function(*n, *a),
2026                            Term::Group(m) => Term::Group(*m),
2027                            Term::Possessed { possessor, possessed } => Term::Possessed {
2028                                possessor: *possessor,
2029                                possessed: *possessed,
2030                            },
2031                            Term::Sigma(p) => Term::Sigma(*p),
2032                            Term::Intension(p) => Term::Intension(*p),
2033                            Term::Proposition(e) => Term::Proposition(*e),
2034                            Term::Value { kind, unit, dimension } => Term::Value {
2035                                kind: *kind,
2036                                unit: *unit,
2037                                dimension: *dimension,
2038                            },
2039                        };
2040                        (*role, new_term)
2041                    })
2042                    .collect();
2043                Ok(self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(crate::ast::NeoEventData {
2044                    event_var: data.event_var,
2045                    verb: data.verb,
2046                    roles: self.ctx.roles.alloc_slice(new_roles),
2047                    modifiers: data.modifiers,
2048                    suppress_existential: data.suppress_existential,
2049                    world: None,
2050                }))))
2051            }
2052            LogicExpr::Distributive { predicate } => Ok(self.ctx.exprs.alloc(LogicExpr::Distributive {
2053                predicate: self.substitute_constant_with_sigma(predicate, constant_name, sigma_term)?,
2054            })),
2055            _ => Ok(expr),
2056        }
2057    }
2058
2059    fn find_main_verb_name(&self, expr: &LogicExpr<'a>) -> Option<Symbol> {
2060        match expr {
2061            LogicExpr::Predicate { name, .. } => Some(*name),
2062            LogicExpr::NeoEvent(data) => Some(data.verb),
2063            LogicExpr::Temporal { body, .. } => self.find_main_verb_name(body),
2064            LogicExpr::Aspectual { body, .. } => self.find_main_verb_name(body),
2065            LogicExpr::Event { predicate, .. } => self.find_main_verb_name(predicate),
2066            LogicExpr::TemporalAnchor { body, .. } => self.find_main_verb_name(body),
2067            LogicExpr::UnaryOp { operand, .. } => self.find_main_verb_name(operand),
2068            LogicExpr::BinaryOp { left, .. } => self.find_main_verb_name(left),
2069            _ => None,
2070        }
2071    }
2072
2073    fn transform_cardinal_to_group(&mut self, expr: &'a LogicExpr<'a>) -> ParseResult<&'a LogicExpr<'a>> {
2074        match expr {
2075            LogicExpr::Quantifier { kind: QuantifierKind::Cardinal(n), variable, body, .. } => {
2076                let group_var = self.interner.intern("g");
2077                let member_var = *variable;
2078
2079                // Extract the restriction (first conjunct) and the body (rest)
2080                // The structure is: restriction ∧ body_rest
2081                let (restriction, body_rest) = match body {
2082                    LogicExpr::BinaryOp { left, op: TokenType::And, right } => (*left, *right),
2083                    _ => return Ok(expr),
2084                };
2085
2086                // Substitute the member variable with the group variable in the body
2087                let transformed_body = self.substitute_constant_with_var_sym(body_rest, member_var, group_var)?;
2088
2089                Ok(self.ctx.exprs.alloc(LogicExpr::GroupQuantifier {
2090                    group_var,
2091                    count: *n,
2092                    member_var,
2093                    restriction,
2094                    body: transformed_body,
2095                }))
2096            }
2097            // Recursively transform nested expressions
2098            LogicExpr::Temporal { operator, body } => {
2099                let transformed = self.transform_cardinal_to_group(body)?;
2100                Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
2101                    operator: *operator,
2102                    body: transformed,
2103                }))
2104            }
2105            LogicExpr::Aspectual { operator, body } => {
2106                let transformed = self.transform_cardinal_to_group(body)?;
2107                Ok(self.ctx.exprs.alloc(LogicExpr::Aspectual {
2108                    operator: *operator,
2109                    body: transformed,
2110                }))
2111            }
2112            LogicExpr::UnaryOp { op, operand } => {
2113                let transformed = self.transform_cardinal_to_group(operand)?;
2114                Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2115                    op: op.clone(),
2116                    operand: transformed,
2117                }))
2118            }
2119            LogicExpr::BinaryOp { left, op, right } => {
2120                let transformed_left = self.transform_cardinal_to_group(left)?;
2121                let transformed_right = self.transform_cardinal_to_group(right)?;
2122                Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2123                    left: transformed_left,
2124                    op: op.clone(),
2125                    right: transformed_right,
2126                }))
2127            }
2128            LogicExpr::Distributive { predicate } => {
2129                let transformed = self.transform_cardinal_to_group(predicate)?;
2130                Ok(self.ctx.exprs.alloc(LogicExpr::Distributive {
2131                    predicate: transformed,
2132                }))
2133            }
2134            LogicExpr::Quantifier { kind, variable, body, island_id } => {
2135                let transformed = self.transform_cardinal_to_group(body)?;
2136                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
2137                    kind: kind.clone(),
2138                    variable: *variable,
2139                    body: transformed,
2140                    island_id: *island_id,
2141                }))
2142            }
2143            _ => Ok(expr),
2144        }
2145    }
2146
2147    fn build_verb_neo_event(
2148        &mut self,
2149        verb: Symbol,
2150        subject_var: Symbol,
2151        object: Option<Term<'a>>,
2152        modifiers: Vec<Symbol>,
2153    ) -> &'a LogicExpr<'a> {
2154        let event_var = self.get_event_var();
2155
2156        // Check if verb is unaccusative (intransitive subject is Theme, not Agent)
2157        let verb_str = self.interner.resolve(verb).to_lowercase();
2158        let is_unaccusative = lookup_verb_db(&verb_str)
2159            .map(|meta| meta.features.contains(&Feature::Unaccusative))
2160            .unwrap_or(false);
2161
2162        // Determine subject role: unaccusative verbs without object use Theme
2163        let has_object = object.is_some();
2164        let subject_role = if is_unaccusative && !has_object {
2165            ThematicRole::Theme
2166        } else {
2167            ThematicRole::Agent
2168        };
2169
2170        // Build roles vector
2171        let mut roles = vec![(subject_role, Term::Variable(subject_var))];
2172        if let Some(obj_term) = object {
2173            roles.push((ThematicRole::Theme, obj_term));
2174        }
2175
2176        // Create NeoEventData with suppress_existential: false
2177        // Each quantified individual gets their own event (distributive reading)
2178        self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
2179            event_var,
2180            verb,
2181            roles: self.ctx.roles.alloc_slice(roles),
2182            modifiers: self.ctx.syms.alloc_slice(modifiers),
2183            suppress_existential: false,
2184            world: None,
2185        })))
2186    }
2187}
2188
2189// Helper methods for donkey binding scope handling
2190impl<'a, 'ctx, 'int> Parser<'a, 'ctx, 'int> {
2191    /// Check if an expression mentions a specific variable
2192    fn expr_mentions_var(&self, expr: &LogicExpr<'a>, var: Symbol) -> bool {
2193        match expr {
2194            LogicExpr::Predicate { args, .. } => {
2195                args.iter().any(|term| self.term_mentions_var(term, var))
2196            }
2197            LogicExpr::BinaryOp { left, right, .. } => {
2198                self.expr_mentions_var(left, var) || self.expr_mentions_var(right, var)
2199            }
2200            LogicExpr::UnaryOp { operand, .. } => self.expr_mentions_var(operand, var),
2201            LogicExpr::Quantifier { body, .. } => self.expr_mentions_var(body, var),
2202            LogicExpr::NeoEvent(data) => {
2203                data.roles.iter().any(|(_, term)| self.term_mentions_var(term, var))
2204            }
2205            LogicExpr::Temporal { body, .. } => self.expr_mentions_var(body, var),
2206            LogicExpr::Aspectual { body, .. } => self.expr_mentions_var(body, var),
2207            LogicExpr::Event { predicate, .. } => self.expr_mentions_var(predicate, var),
2208            LogicExpr::Modal { operand, .. } => self.expr_mentions_var(operand, var),
2209            LogicExpr::Scopal { body, .. } => self.expr_mentions_var(body, var),
2210            _ => false,
2211        }
2212    }
2213
2214    fn term_mentions_var(&self, term: &Term<'a>, var: Symbol) -> bool {
2215        match term {
2216            Term::Variable(v) => *v == var,
2217            Term::Function(_, args) => args.iter().any(|t| self.term_mentions_var(t, var)),
2218            _ => false,
2219        }
2220    }
2221
2222    /// Collect all conjuncts from a conjunction tree
2223    fn collect_conjuncts(&self, expr: &'a LogicExpr<'a>) -> Vec<&'a LogicExpr<'a>> {
2224        match expr {
2225            LogicExpr::BinaryOp { left, op: TokenType::And, right } => {
2226                let mut result = self.collect_conjuncts(left);
2227                result.extend(self.collect_conjuncts(right));
2228                result
2229            }
2230            _ => vec![expr],
2231        }
2232    }
2233
2234    /// Wrap unused donkey bindings inside the restriction/body of a quantifier structure.
2235    ///
2236    /// For universals (implications):
2237    ///   Transform: ∀x((P(x) ∧ Q(y)) → R(x)) with unused y
2238    ///   Into:      ∀x((P(x) ∧ ∃y(Q(y))) → R(x))
2239    ///
2240    /// For existentials (conjunctions):
2241    ///   Transform: ∃x(P(x) ∧ Q(y) ∧ R(x)) with unused y
2242    ///   Into:      ∃x(P(x) ∧ ∃y(Q(y)) ∧ R(x))
2243    ///
2244    /// If wide_scope_negation is true, wrap the existential in negation:
2245    ///   Into:      ∀x((P(x) ∧ ¬∃y(Q(y))) → R(x))
2246    fn wrap_donkey_in_restriction(
2247        &self,
2248        body: &'a LogicExpr<'a>,
2249        donkey_var: Symbol,
2250        wide_scope_negation: bool,
2251    ) -> &'a LogicExpr<'a> {
2252        // Handle Quantifier wrapping first
2253        if let LogicExpr::Quantifier { kind, variable, body: inner_body, island_id } = body {
2254            let transformed = self.wrap_donkey_in_restriction(inner_body, donkey_var, wide_scope_negation);
2255            return self.ctx.exprs.alloc(LogicExpr::Quantifier {
2256                kind: kind.clone(),
2257                variable: *variable,
2258                body: transformed,
2259                island_id: *island_id,
2260            });
2261        }
2262
2263        // Handle implication (universal quantifiers)
2264        if let LogicExpr::BinaryOp { left, op: TokenType::If, right } = body {
2265            return self.wrap_in_implication(*left, *right, donkey_var, wide_scope_negation);
2266        }
2267
2268        // Handle conjunction (existential quantifiers)
2269        if let LogicExpr::BinaryOp { left: _, op: TokenType::And, right: _ } = body {
2270            return self.wrap_in_conjunction(body, donkey_var, wide_scope_negation);
2271        }
2272
2273        // Not a structure we can process
2274        body
2275    }
2276
2277    /// Wrap donkey binding in an implication structure (∀x(P(x) → Q(x)))
2278    fn wrap_in_implication(
2279        &self,
2280        restriction: &'a LogicExpr<'a>,
2281        consequent: &'a LogicExpr<'a>,
2282        donkey_var: Symbol,
2283        wide_scope_negation: bool,
2284    ) -> &'a LogicExpr<'a> {
2285        // Collect all conjuncts in the restriction
2286        let conjuncts = self.collect_conjuncts(restriction);
2287
2288        // Partition into those mentioning the donkey var and those not
2289        let (with_var, without_var): (Vec<_>, Vec<_>) = conjuncts
2290            .into_iter()
2291            .partition(|c| self.expr_mentions_var(c, donkey_var));
2292
2293        if with_var.is_empty() {
2294            // Variable not found in restriction, return original implication
2295            return self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2296                left: restriction,
2297                op: TokenType::If,
2298                right: consequent,
2299            });
2300        }
2301
2302        // Combine the "with var" conjuncts
2303        let with_var_combined = self.combine_conjuncts(&with_var);
2304
2305        // Wrap with existential
2306        let existential = self.ctx.exprs.alloc(LogicExpr::Quantifier {
2307            kind: QuantifierKind::Existential,
2308            variable: donkey_var,
2309            body: with_var_combined,
2310            island_id: self.current_island,
2311        });
2312
2313        // For wide scope negation (de dicto reading of "lacks"), wrap ∃ in ¬
2314        let wrapped = if wide_scope_negation {
2315            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2316                op: TokenType::Not,
2317                operand: existential,
2318            })
2319        } else {
2320            existential
2321        };
2322
2323        // Combine with "without var" conjuncts
2324        let new_restriction = if without_var.is_empty() {
2325            wrapped
2326        } else {
2327            let without_combined = self.combine_conjuncts(&without_var);
2328            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2329                left: without_combined,
2330                op: TokenType::And,
2331                right: wrapped,
2332            })
2333        };
2334
2335        // Rebuild the implication
2336        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2337            left: new_restriction,
2338            op: TokenType::If,
2339            right: consequent,
2340        })
2341    }
2342
2343    /// Wrap donkey binding in a conjunction structure (∃x(P(x) ∧ Q(x)))
2344    fn wrap_in_conjunction(
2345        &self,
2346        body: &'a LogicExpr<'a>,
2347        donkey_var: Symbol,
2348        wide_scope_negation: bool,
2349    ) -> &'a LogicExpr<'a> {
2350        // Collect all conjuncts
2351        let conjuncts = self.collect_conjuncts(body);
2352
2353        // Partition into those mentioning the donkey var and those not
2354        let (with_var, without_var): (Vec<_>, Vec<_>) = conjuncts
2355            .into_iter()
2356            .partition(|c| self.expr_mentions_var(c, donkey_var));
2357
2358        if with_var.is_empty() {
2359            // Variable not found, return unchanged
2360            return body;
2361        }
2362
2363        // Combine the "with var" conjuncts
2364        let with_var_combined = self.combine_conjuncts(&with_var);
2365
2366        // Wrap with existential
2367        let existential = self.ctx.exprs.alloc(LogicExpr::Quantifier {
2368            kind: QuantifierKind::Existential,
2369            variable: donkey_var,
2370            body: with_var_combined,
2371            island_id: self.current_island,
2372        });
2373
2374        // For wide scope negation (de dicto reading of "lacks"), wrap ∃ in ¬
2375        let wrapped = if wide_scope_negation {
2376            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2377                op: TokenType::Not,
2378                operand: existential,
2379            })
2380        } else {
2381            existential
2382        };
2383
2384        // Combine with "without var" conjuncts
2385        if without_var.is_empty() {
2386            wrapped
2387        } else {
2388            let without_combined = self.combine_conjuncts(&without_var);
2389            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2390                left: without_combined,
2391                op: TokenType::And,
2392                right: wrapped,
2393            })
2394        }
2395    }
2396
2397    fn combine_conjuncts(&self, conjuncts: &[&'a LogicExpr<'a>]) -> &'a LogicExpr<'a> {
2398        if conjuncts.is_empty() {
2399            panic!("Cannot combine empty conjuncts");
2400        }
2401        if conjuncts.len() == 1 {
2402            return conjuncts[0];
2403        }
2404        let mut result = conjuncts[0];
2405        for c in &conjuncts[1..] {
2406            result = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2407                left: result,
2408                op: TokenType::And,
2409                right: *c,
2410            });
2411        }
2412        result
2413    }
2414}
logicaffeine_language/parser/quantifier.rs

logicaffeine_language/parser/
quantifier.rs
