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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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::Implies,
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        // Handle do-support: "every X does not hold" → ¬Hold(x)
852        if self.check(&TokenType::Does) || self.check(&TokenType::Do) {
853            self.advance(); // consume "does"/"do"
854            let negative = self.match_token(&[TokenType::Not]);
855            // The verb after "does not" becomes the predicate
856            let verb_sym = self.consume_verb();
857            let predicate_expr = self.ctx.exprs.alloc(LogicExpr::Predicate {
858                name: verb_sym,
859                args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
860                world: None,
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::Implies,
875                    right: final_predicate,
876                }),
877                _ => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
878                    left: subject_pred,
879                    op: TokenType::And,
880                    right: final_predicate,
881                }),
882            };
883
884            let result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
885                kind: match quantifier_token {
886                    TokenType::All => QuantifierKind::Universal,
887                    _ => QuantifierKind::Existential,
888                },
889                variable: var_name,
890                body: body,
891                island_id: self.current_island,
892            });
893            self.in_negative_quantifier = was_in_negative_quantifier;
894            return Ok(result);
895        }
896
897        self.consume_copula()?;
898
899        let negative = self.match_token(&[TokenType::Not]);
900        let predicate_np = self.parse_noun_phrase(true)?;
901
902        let predicate_expr = self.ctx.exprs.alloc(LogicExpr::Predicate {
903            name: predicate_np.noun,
904            args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
905            world: None,
906        });
907
908        let final_predicate = if negative {
909            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
910                op: TokenType::Not,
911                operand: predicate_expr,
912            })
913        } else {
914            predicate_expr
915        };
916
917        let body = match quantifier_token {
918            TokenType::All => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
919                left: subject_pred,
920                op: TokenType::Implies,
921                right: final_predicate,
922            }),
923            TokenType::Any => {
924                if self.is_negative_context() {
925                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
926                        left: subject_pred,
927                        op: TokenType::And,
928                        right: final_predicate,
929                    })
930                } else {
931                    self.ctx.exprs.alloc(LogicExpr::BinaryOp {
932                        left: subject_pred,
933                        op: TokenType::Implies,
934                        right: final_predicate,
935                    })
936                }
937            }
938            TokenType::Some
939            | TokenType::Most
940            | TokenType::Few
941            | TokenType::Many
942            | TokenType::Cardinal(_)
943            | TokenType::AtLeast(_)
944            | TokenType::AtMost(_) => self.ctx.exprs.alloc(LogicExpr::BinaryOp {
945                left: subject_pred,
946                op: TokenType::And,
947                right: final_predicate,
948            }),
949            TokenType::No => {
950                let neg_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
951                    name: predicate_np.noun,
952                    args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
953                    world: None,
954                });
955                let neg = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
956                    op: TokenType::Not,
957                    operand: neg_pred,
958                });
959                self.ctx.exprs.alloc(LogicExpr::BinaryOp {
960                    left: subject_pred,
961                    op: TokenType::Implies,
962                    right: neg,
963                })
964            }
965            _ => {
966                return Err(ParseError {
967                    kind: ParseErrorKind::UnknownQuantifier {
968                        found: quantifier_token.clone(),
969                    },
970                    span: self.current_span(),
971                })
972            }
973        };
974
975        let kind = match quantifier_token {
976            TokenType::All | TokenType::No => QuantifierKind::Universal,
977            TokenType::Any => {
978                if self.is_negative_context() {
979                    QuantifierKind::Existential
980                } else {
981                    QuantifierKind::Universal
982                }
983            }
984            TokenType::Some => QuantifierKind::Existential,
985            TokenType::Most => QuantifierKind::Most,
986            TokenType::Few => QuantifierKind::Few,
987            TokenType::Many => QuantifierKind::Many,
988            TokenType::Cardinal(n) => QuantifierKind::Cardinal(n),
989            TokenType::AtLeast(n) => QuantifierKind::AtLeast(n),
990            TokenType::AtMost(n) => QuantifierKind::AtMost(n),
991            _ => {
992                return Err(ParseError {
993                    kind: ParseErrorKind::UnknownQuantifier {
994                        found: quantifier_token.clone(),
995                    },
996                    span: self.current_span(),
997                })
998            }
999        };
1000
1001        let mut result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1002            kind,
1003            variable: var_name,
1004            body,
1005            island_id: self.current_island,
1006        });
1007
1008        for (_noun, donkey_var, used, wide_neg) in self.donkey_bindings.iter().rev() {
1009            if *used {
1010                // Donkey anaphora: wrap with ∀ at outer scope
1011                result = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1012                    kind: QuantifierKind::Universal,
1013                    variable: *donkey_var,
1014                    body: result,
1015                    island_id: self.current_island,
1016                });
1017            } else {
1018                // Non-donkey: wrap with ∃ INSIDE the restriction
1019                result = self.wrap_donkey_in_restriction(result, *donkey_var, *wide_neg);
1020            }
1021        }
1022        self.donkey_bindings.clear();
1023
1024        self.in_negative_quantifier = was_in_negative_quantifier;
1025        Ok(result)
1026    }
1027
1028    fn parse_restriction(&mut self, var_name: Symbol) -> ParseResult<&'a LogicExpr<'a>> {
1029        let mut conditions: Vec<&'a LogicExpr<'a>> = Vec::new();
1030
1031        loop {
1032            if self.is_at_end() {
1033                break;
1034            }
1035
1036            let is_adjective = matches!(self.peek().kind, TokenType::Adjective(_));
1037            if !is_adjective {
1038                break;
1039            }
1040
1041            let next_is_content = if self.current + 1 < self.tokens.len() {
1042                matches!(
1043                    self.tokens[self.current + 1].kind,
1044                    TokenType::Noun(_) | TokenType::Adjective(_) | TokenType::ProperName(_)
1045                )
1046            } else {
1047                false
1048            };
1049
1050            if next_is_content {
1051                if let TokenType::Adjective(adj) = self.advance().kind.clone() {
1052                    conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1053                        name: adj,
1054                        args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1055                        world: None,
1056                    }));
1057                }
1058            } else {
1059                break;
1060            }
1061        }
1062
1063        let noun = self.consume_content_word()?;
1064        conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1065            name: noun,
1066            args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1067            world: None,
1068        }));
1069
1070        while self.check(&TokenType::That) || self.check(&TokenType::Who) {
1071            self.advance();
1072            let clause_pred = self.parse_relative_clause(var_name)?;
1073            conditions.push(clause_pred);
1074        }
1075
1076        self.combine_with_and(conditions)
1077    }
1078
1079    fn parse_verb_phrase_for_restriction(&mut self, var_name: Symbol) -> ParseResult<&'a LogicExpr<'a>> {
1080        let var_term = Term::Variable(var_name);
1081        let verb = self.consume_verb();
1082        let verb_str_owned = self.interner.resolve(verb).to_string();
1083
1084        // Check EARLY if verb is lexically negative (e.g., "lacks" -> "Have" with negation)
1085        // This determines whether donkey bindings need wide scope negation
1086        let (canonical_verb, is_negative) = get_canonical_verb(&verb_str_owned.to_lowercase())
1087            .map(|(lemma, neg)| (self.interner.intern(lemma), neg))
1088            .unwrap_or((verb, false));
1089
1090        // Determine if this binding needs wide scope negation wrapping
1091        let needs_wide_scope = is_negative && self.negative_scope_mode == NegativeScopeMode::Wide;
1092
1093        if Lexer::is_raising_verb(&verb_str_owned) && self.check_to() {
1094            self.advance();
1095            if self.check_verb() {
1096                let inf_verb = self.consume_verb();
1097                let inf_verb_str = self.interner.resolve(inf_verb).to_lowercase();
1098
1099                if inf_verb_str == "be" && self.check_content_word() {
1100                    let adj = self.consume_content_word()?;
1101                    let embedded = self.ctx.exprs.alloc(LogicExpr::Predicate {
1102                        name: adj,
1103                        args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1104                        world: None,
1105                    });
1106                    return Ok(self.ctx.exprs.alloc(LogicExpr::Scopal {
1107                        operator: verb,
1108                        body: embedded,
1109                    }));
1110                }
1111
1112                let embedded = self.ctx.exprs.alloc(LogicExpr::Predicate {
1113                    name: inf_verb,
1114                    args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1115                    world: None,
1116                });
1117                return Ok(self.ctx.exprs.alloc(LogicExpr::Scopal {
1118                    operator: verb,
1119                    body: embedded,
1120                }));
1121            } else if self.check(&TokenType::Is) || self.check(&TokenType::Are) {
1122                self.advance();
1123                if self.check_content_word() {
1124                    let adj = self.consume_content_word()?;
1125                    let embedded = self.ctx.exprs.alloc(LogicExpr::Predicate {
1126                        name: adj,
1127                        args: self.ctx.terms.alloc_slice([Term::Variable(var_name)]),
1128                        world: None,
1129                    });
1130                    return Ok(self.ctx.exprs.alloc(LogicExpr::Scopal {
1131                        operator: verb,
1132                        body: embedded,
1133                    }));
1134                }
1135            }
1136        }
1137
1138        let mut args = vec![var_term];
1139        let mut extra_conditions: Vec<&'a LogicExpr<'a>> = Vec::new();
1140
1141        if self.check(&TokenType::Reflexive) {
1142            self.advance();
1143            args.push(Term::Variable(var_name));
1144        } else if (self.check_content_word() || self.check_article()) && !self.check_verb() {
1145            if matches!(
1146                self.peek().kind,
1147                TokenType::Article(Definiteness::Indefinite)
1148            ) {
1149                self.advance();
1150                let noun = self.consume_content_word()?;
1151                let donkey_var = self.next_var_name();
1152
1153                if needs_wide_scope {
1154                    // === WIDE SCOPE MODE ===
1155                    // Build ¬∃y(Key(y) ∧ ∃e(Have(e) ∧ Agent(e,x) ∧ Theme(e,y))) directly
1156                    //
1157                    // We capture the binding HERE and return the complete structure.
1158                    // DO NOT push to donkey_bindings - that would leak y to outer scope.
1159
1160                    // Build: Key(y)
1161                    let restriction_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1162                        name: noun,
1163                        args: self.ctx.terms.alloc_slice([Term::Variable(donkey_var)]),
1164                        world: None,
1165                    });
1166
1167                    // Build: ∃e(Have(e) ∧ Agent(e,x) ∧ Theme(e,y)) using Neo-Davidsonian semantics
1168                    // IMPORTANT: Use build_verb_neo_event() for consistent Full-tier formatting
1169                    let inner_modifiers = self.collect_adverbs();
1170                    let verb_pred = self.build_verb_neo_event(
1171                        canonical_verb,
1172                        var_name,
1173                        Some(Term::Variable(donkey_var)),
1174                        inner_modifiers,
1175                    );
1176
1177                    // Build: Key(y) ∧ ∃e(Have(e) ∧ Agent(e,x) ∧ Theme(e,y))
1178                    let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1179                        left: restriction_pred,
1180                        op: TokenType::And,
1181                        right: verb_pred,
1182                    });
1183
1184                    // Build: ∃y(Key(y) ∧ ∃e(Have(e) ∧ ...))
1185                    let existential = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1186                        kind: QuantifierKind::Existential,
1187                        variable: donkey_var,
1188                        body,
1189                        island_id: self.current_island,
1190                    });
1191
1192                    // Build: ¬∃y(Key(y) ∧ ∃e(Have(e) ∧ ...))
1193                    let negated_existential = self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1194                        op: TokenType::Not,
1195                        operand: existential,
1196                    });
1197
1198                    // Return the complete wide-scope structure directly
1199                    return Ok(negated_existential);
1200                }
1201
1202                // === NARROW SCOPE MODE ===
1203                // Push binding for later processing (normal donkey binding flow)
1204                self.donkey_bindings.push((noun, donkey_var, false, false));
1205
1206                extra_conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1207                    name: noun,
1208                    args: self.ctx.terms.alloc_slice([Term::Variable(donkey_var)]),
1209                    world: None,
1210                }));
1211
1212                args.push(Term::Variable(donkey_var));
1213            } else {
1214                let object = self.parse_noun_phrase(false)?;
1215
1216                if self.check(&TokenType::That) || self.check(&TokenType::Who) {
1217                    self.advance();
1218                    let nested_var = self.next_var_name();
1219                    let nested_rel = self.parse_relative_clause(nested_var)?;
1220
1221                    extra_conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1222                        name: object.noun,
1223                        args: self.ctx.terms.alloc_slice([Term::Variable(nested_var)]),
1224                        world: None,
1225                    }));
1226                    extra_conditions.push(nested_rel);
1227                    args.push(Term::Variable(nested_var));
1228                } else {
1229                    args.push(Term::Constant(object.noun));
1230                }
1231            }
1232        }
1233
1234        while self.check_preposition() {
1235            self.advance();
1236            if self.check(&TokenType::Reflexive) {
1237                self.advance();
1238                args.push(Term::Variable(var_name));
1239            } else if self.check_content_word() || self.check_article() {
1240                let object = self.parse_noun_phrase(false)?;
1241
1242                if self.check(&TokenType::That) || self.check(&TokenType::Who) {
1243                    self.advance();
1244                    let nested_var = self.next_var_name();
1245                    let nested_rel = self.parse_relative_clause(nested_var)?;
1246                    extra_conditions.push(self.ctx.exprs.alloc(LogicExpr::Predicate {
1247                        name: object.noun,
1248                        args: self.ctx.terms.alloc_slice([Term::Variable(nested_var)]),
1249                        world: None,
1250                    }));
1251                    extra_conditions.push(nested_rel);
1252                    args.push(Term::Variable(nested_var));
1253                } else {
1254                    args.push(Term::Constant(object.noun));
1255                }
1256            }
1257        }
1258
1259        // Use the canonical verb determined at top of function
1260        // Extract object term from args if present (args[0] is subject, args[1] is object)
1261        let obj_term = if args.len() > 1 {
1262            Some(args.remove(1))
1263        } else {
1264            None
1265        };
1266        let final_modifiers = self.collect_adverbs();
1267        let base_pred = self.build_verb_neo_event(canonical_verb, var_name, obj_term, final_modifiers);
1268
1269        // Wrap in negation only for NARROW scope mode (de re reading)
1270        // Wide scope mode: negation handled via donkey binding flag in wrap_donkey_in_restriction
1271        // - Narrow: ∃y(Key(y) ∧ ¬Have(x,y)) - "missing ANY key"
1272        // - Wide:   ¬∃y(Key(y) ∧ Have(x,y)) - "has NO keys"
1273        let verb_pred = if is_negative && self.negative_scope_mode == NegativeScopeMode::Narrow {
1274            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1275                op: TokenType::Not,
1276                operand: base_pred,
1277            })
1278        } else {
1279            base_pred
1280        };
1281
1282        if extra_conditions.is_empty() {
1283            Ok(verb_pred)
1284        } else {
1285            extra_conditions.push(verb_pred);
1286            self.combine_with_and(extra_conditions)
1287        }
1288    }
1289
1290    fn combine_with_and(&self, mut exprs: Vec<&'a LogicExpr<'a>>) -> ParseResult<&'a LogicExpr<'a>> {
1291        if exprs.is_empty() {
1292            return Err(ParseError {
1293                kind: ParseErrorKind::EmptyRestriction,
1294                span: self.current_span(),
1295            });
1296        }
1297        if exprs.len() == 1 {
1298            return Ok(exprs.remove(0));
1299        }
1300        let mut root = exprs.remove(0);
1301        for expr in exprs {
1302            root = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1303                left: root,
1304                op: TokenType::And,
1305                right: expr,
1306            });
1307        }
1308        Ok(root)
1309    }
1310
1311    fn wrap_with_definiteness_full(
1312        &mut self,
1313        np: &NounPhrase<'a>,
1314        predicate: &'a LogicExpr<'a>,
1315    ) -> ParseResult<&'a LogicExpr<'a>> {
1316        let result = self.wrap_with_definiteness_and_adjectives_and_pps(
1317            np.definiteness,
1318            np.noun,
1319            np.adjectives,
1320            np.pps,
1321            predicate,
1322        )?;
1323
1324        // If NP has a superlative, add the superlative constraint
1325        if let Some(adj) = np.superlative {
1326            let superlative_expr = self.ctx.exprs.alloc(LogicExpr::Superlative {
1327                adjective: adj,
1328                subject: self.ctx.terms.alloc(Term::Constant(np.noun)),
1329                domain: np.noun,
1330            });
1331            Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1332                left: result,
1333                op: TokenType::And,
1334                right: superlative_expr,
1335            }))
1336        } else {
1337            Ok(result)
1338        }
1339    }
1340
1341    fn wrap_with_definiteness(
1342        &mut self,
1343        definiteness: Option<Definiteness>,
1344        noun: Symbol,
1345        predicate: &'a LogicExpr<'a>,
1346    ) -> ParseResult<&'a LogicExpr<'a>> {
1347        self.wrap_with_definiteness_and_adjectives_and_pps(definiteness, noun, &[], &[], predicate)
1348    }
1349
1350    fn wrap_with_definiteness_and_adjectives(
1351        &mut self,
1352        definiteness: Option<Definiteness>,
1353        noun: Symbol,
1354        adjectives: &[Symbol],
1355        predicate: &'a LogicExpr<'a>,
1356    ) -> ParseResult<&'a LogicExpr<'a>> {
1357        self.wrap_with_definiteness_and_adjectives_and_pps(
1358            definiteness,
1359            noun,
1360            adjectives,
1361            &[],
1362            predicate,
1363        )
1364    }
1365
1366    fn wrap_with_definiteness_and_adjectives_and_pps(
1367        &mut self,
1368        definiteness: Option<Definiteness>,
1369        noun: Symbol,
1370        adjectives: &[Symbol],
1371        pps: &[&'a LogicExpr<'a>],
1372        predicate: &'a LogicExpr<'a>,
1373    ) -> ParseResult<&'a LogicExpr<'a>> {
1374        match definiteness {
1375            Some(Definiteness::Indefinite) => {
1376                let var = self.next_var_name();
1377
1378                // Introduce referent into DRS for cross-sentence anaphora
1379                // If inside a "No" quantifier, mark as NegationScope (inaccessible)
1380                let gender = Self::infer_noun_gender(self.interner.resolve(noun));
1381                let number = if Self::is_plural_noun(self.interner.resolve(noun)) {
1382                    Number::Plural
1383                } else {
1384                    Number::Singular
1385                };
1386                if self.in_negative_quantifier {
1387                    self.drs.introduce_referent_with_source(var, noun, gender, number, ReferentSource::NegationScope);
1388                } else {
1389                    self.drs.introduce_referent(var, noun, gender, number);
1390                }
1391
1392                let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1393                    name: noun,
1394                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1395                    world: None,
1396                });
1397
1398                for adj in adjectives {
1399                    let adj_str = self.interner.resolve(*adj).to_lowercase();
1400                    let adj_pred = if is_subsective(&adj_str) {
1401                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1402                            name: *adj,
1403                            args: self.ctx.terms.alloc_slice([
1404                                Term::Variable(var),
1405                                Term::Intension(noun),
1406                            ]),
1407                            world: None,
1408                        })
1409                    } else {
1410                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1411                            name: *adj,
1412                            args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1413                            world: None,
1414                        })
1415                    };
1416                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1417                        left: restriction,
1418                        op: TokenType::And,
1419                        right: adj_pred,
1420                    });
1421                }
1422
1423                for pp in pps {
1424                    let substituted_pp = self.substitute_pp_placeholder(pp, var);
1425                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1426                        left: restriction,
1427                        op: TokenType::And,
1428                        right: substituted_pp,
1429                    });
1430                }
1431
1432                let substituted = self.substitute_constant_with_var_sym(predicate, noun, var)?;
1433                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1434                    left: restriction,
1435                    op: TokenType::And,
1436                    right: substituted,
1437                });
1438                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1439                    kind: QuantifierKind::Existential,
1440                    variable: var,
1441                    body,
1442                    island_id: self.current_island,
1443                }))
1444            }
1445            Some(Definiteness::Definite) => {
1446                let noun_str = self.interner.resolve(noun).to_string();
1447
1448                if Self::is_plural_noun(&noun_str) {
1449                    let singular = Self::singularize_noun(&noun_str);
1450                    let singular_sym = self.interner.intern(&singular);
1451                    let sigma_term = Term::Sigma(singular_sym);
1452
1453                    let substituted =
1454                        self.substitute_constant_with_sigma(predicate, noun, sigma_term)?;
1455
1456                    let verb_name = self.find_main_verb_name(predicate);
1457                    let is_collective = verb_name
1458                        .map(|v| {
1459                            let lemma = self.interner.resolve(v);
1460                            Lexer::is_collective_verb(lemma)
1461                                || (Lexer::is_mixed_verb(lemma) && self.collective_mode)
1462                        })
1463                        .unwrap_or(false);
1464
1465                    // Introduce definite plural referent to DRS for cross-sentence pronoun resolution
1466                    // E.g., "The dogs ran. They barked." - "they" refers to "dogs"
1467                    // Definite descriptions presuppose existence, so they should be globally accessible.
1468                    let gender = Gender::Unknown;  // Plural entities have unknown gender
1469                    self.drs.introduce_referent_with_source(singular_sym, singular_sym, gender, Number::Plural, ReferentSource::MainClause);
1470
1471                    if is_collective {
1472                        Ok(substituted)
1473                    } else {
1474                        Ok(self.ctx.exprs.alloc(LogicExpr::Distributive {
1475                            predicate: substituted,
1476                        }))
1477                    }
1478                } else {
1479                    let x = self.next_var_name();
1480                    let y = self.next_var_name();
1481
1482                    let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1483                        name: noun,
1484                        args: self.ctx.terms.alloc_slice([Term::Variable(x)]),
1485                        world: None,
1486                    });
1487
1488                    for adj in adjectives {
1489                        let adj_str = self.interner.resolve(*adj).to_lowercase();
1490                        let adj_pred = if is_subsective(&adj_str) {
1491                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1492                                name: *adj,
1493                                args: self.ctx.terms.alloc_slice([
1494                                    Term::Variable(x),
1495                                    Term::Intension(noun),
1496                                ]),
1497                                world: None,
1498                            })
1499                        } else {
1500                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1501                                name: *adj,
1502                                args: self.ctx.terms.alloc_slice([Term::Variable(x)]),
1503                                world: None,
1504                            })
1505                        };
1506                        restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1507                            left: restriction,
1508                            op: TokenType::And,
1509                            right: adj_pred,
1510                        });
1511                    }
1512
1513                    for pp in pps {
1514                        let substituted_pp = self.substitute_pp_placeholder(pp, x);
1515                        restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1516                            left: restriction,
1517                            op: TokenType::And,
1518                            right: substituted_pp,
1519                        });
1520                    }
1521
1522                    // Bridging anaphora: check if this noun is a part of a previously mentioned whole
1523                    // E.g., "I bought a car. The engine smoked." - engine is part of car
1524                    let has_prior_antecedent = self.drs.resolve_definite(
1525                        self.drs.current_box_index(),
1526                        noun
1527                    ).is_some();
1528
1529                    if !has_prior_antecedent {
1530                        if let Some((whole_var, _whole_name)) = self.drs.resolve_bridging(self.interner, noun) {
1531                            let part_of_sym = self.interner.intern("PartOf");
1532                            let part_of_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1533                                name: part_of_sym,
1534                                args: self.ctx.terms.alloc_slice([
1535                                    Term::Variable(x),
1536                                    Term::Constant(whole_var),
1537                                ]),
1538                                world: None,
1539                            });
1540                            restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1541                                left: restriction,
1542                                op: TokenType::And,
1543                                right: part_of_pred,
1544                            });
1545                        }
1546                    }
1547
1548                    // Introduce definite referent to DRS for cross-sentence pronoun resolution
1549                    // E.g., "The engine smoked. It broke." - "it" refers to "engine"
1550                    // Definite descriptions presuppose existence, so they should be globally
1551                    // accessible even when introduced inside conditional antecedents.
1552                    let gender = Self::infer_noun_gender(self.interner.resolve(noun));
1553                    let number = if Self::is_plural_noun(self.interner.resolve(noun)) {
1554                        Number::Plural
1555                    } else {
1556                        Number::Singular
1557                    };
1558                    self.drs.introduce_referent_with_source(x, noun, gender, number, ReferentSource::MainClause);
1559
1560                    let mut y_restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1561                        name: noun,
1562                        args: self.ctx.terms.alloc_slice([Term::Variable(y)]),
1563                        world: None,
1564                    });
1565                    for adj in adjectives {
1566                        let adj_str = self.interner.resolve(*adj).to_lowercase();
1567                        let adj_pred = if is_subsective(&adj_str) {
1568                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1569                                name: *adj,
1570                                args: self.ctx.terms.alloc_slice([
1571                                    Term::Variable(y),
1572                                    Term::Intension(noun),
1573                                ]),
1574                                world: None,
1575                            })
1576                        } else {
1577                            self.ctx.exprs.alloc(LogicExpr::Predicate {
1578                                name: *adj,
1579                                args: self.ctx.terms.alloc_slice([Term::Variable(y)]),
1580                                world: None,
1581                            })
1582                        };
1583                        y_restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1584                            left: y_restriction,
1585                            op: TokenType::And,
1586                            right: adj_pred,
1587                        });
1588                    }
1589
1590                    for pp in pps {
1591                        let substituted_pp = self.substitute_pp_placeholder(pp, y);
1592                        y_restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1593                            left: y_restriction,
1594                            op: TokenType::And,
1595                            right: substituted_pp,
1596                        });
1597                    }
1598
1599                    let identity = self.ctx.exprs.alloc(LogicExpr::Identity {
1600                        left: self.ctx.terms.alloc(Term::Variable(y)),
1601                        right: self.ctx.terms.alloc(Term::Variable(x)),
1602                    });
1603                    let uniqueness_body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1604                        left: y_restriction,
1605                        op: TokenType::Implies,
1606                        right: identity,
1607                    });
1608                    let uniqueness = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1609                        kind: QuantifierKind::Universal,
1610                        variable: y,
1611                        body: uniqueness_body,
1612                        island_id: self.current_island,
1613                    });
1614
1615                    let main_pred = self.substitute_constant_with_var_sym(predicate, noun, x)?;
1616
1617                    let inner = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1618                        left: restriction,
1619                        op: TokenType::And,
1620                        right: uniqueness,
1621                    });
1622                    let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1623                        left: inner,
1624                        op: TokenType::And,
1625                        right: main_pred,
1626                    });
1627
1628                    Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1629                        kind: QuantifierKind::Existential,
1630                        variable: x,
1631                        body,
1632                        island_id: self.current_island,
1633                    }))
1634                }
1635            }
1636            Some(Definiteness::Proximal) | Some(Definiteness::Distal) => {
1637                let var = self.next_var_name();
1638
1639                let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1640                    name: noun,
1641                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1642                    world: None,
1643                });
1644
1645                let deictic_name = if matches!(definiteness, Some(Definiteness::Proximal)) {
1646                    self.interner.intern("Proximal")
1647                } else {
1648                    self.interner.intern("Distal")
1649                };
1650                let deictic_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1651                    name: deictic_name,
1652                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1653                    world: None,
1654                });
1655                restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1656                    left: restriction,
1657                    op: TokenType::And,
1658                    right: deictic_pred,
1659                });
1660
1661                for adj in adjectives {
1662                    let adj_str = self.interner.resolve(*adj).to_lowercase();
1663                    let adj_pred = if is_subsective(&adj_str) {
1664                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1665                            name: *adj,
1666                            args: self.ctx.terms.alloc_slice([
1667                                Term::Variable(var),
1668                                Term::Intension(noun),
1669                            ]),
1670                            world: None,
1671                        })
1672                    } else {
1673                        self.ctx.exprs.alloc(LogicExpr::Predicate {
1674                            name: *adj,
1675                            args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1676                            world: None,
1677                        })
1678                    };
1679                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1680                        left: restriction,
1681                        op: TokenType::And,
1682                        right: adj_pred,
1683                    });
1684                }
1685
1686                for pp in pps {
1687                    let substituted_pp = self.substitute_pp_placeholder(pp, var);
1688                    restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1689                        left: restriction,
1690                        op: TokenType::And,
1691                        right: substituted_pp,
1692                    });
1693                }
1694
1695                let substituted = self.substitute_constant_with_var_sym(predicate, noun, var)?;
1696                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1697                    left: restriction,
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            None => Ok(predicate),
1709        }
1710    }
1711
1712    fn wrap_with_definiteness_for_object(
1713        &mut self,
1714        definiteness: Option<Definiteness>,
1715        noun: Symbol,
1716        predicate: &'a LogicExpr<'a>,
1717    ) -> ParseResult<&'a LogicExpr<'a>> {
1718        match definiteness {
1719            Some(Definiteness::Indefinite) => {
1720                let var = self.next_var_name();
1721
1722                // Introduce referent into DRS for cross-sentence anaphora
1723                // If inside a "No" quantifier, mark as NegationScope (inaccessible)
1724                let gender = Self::infer_noun_gender(self.interner.resolve(noun));
1725                let number = if Self::is_plural_noun(self.interner.resolve(noun)) {
1726                    Number::Plural
1727                } else {
1728                    Number::Singular
1729                };
1730                if self.in_negative_quantifier {
1731                    self.drs.introduce_referent_with_source(var, noun, gender, number, ReferentSource::NegationScope);
1732                } else {
1733                    self.drs.introduce_referent(var, noun, gender, number);
1734                }
1735
1736                let type_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1737                    name: noun,
1738                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1739                    world: None,
1740                });
1741                let substituted = self.substitute_constant_with_var(predicate, noun, var)?;
1742                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1743                    left: type_pred,
1744                    op: TokenType::And,
1745                    right: substituted,
1746                });
1747                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1748                    kind: QuantifierKind::Existential,
1749                    variable: var,
1750                    body,
1751                    island_id: self.current_island,
1752                }))
1753            }
1754            Some(Definiteness::Definite) => {
1755                let x = self.next_var_name();
1756                let y = self.next_var_name();
1757
1758                let type_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1759                    name: noun,
1760                    args: self.ctx.terms.alloc_slice([Term::Variable(x)]),
1761                    world: None,
1762                });
1763
1764                let identity = self.ctx.exprs.alloc(LogicExpr::Identity {
1765                    left: self.ctx.terms.alloc(Term::Variable(y)),
1766                    right: self.ctx.terms.alloc(Term::Variable(x)),
1767                });
1768                let inner_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1769                    name: noun,
1770                    args: self.ctx.terms.alloc_slice([Term::Variable(y)]),
1771                    world: None,
1772                });
1773                let uniqueness_body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1774                    left: inner_pred,
1775                    op: TokenType::Implies,
1776                    right: identity,
1777                });
1778                let uniqueness = self.ctx.exprs.alloc(LogicExpr::Quantifier {
1779                    kind: QuantifierKind::Universal,
1780                    variable: y,
1781                    body: uniqueness_body,
1782                    island_id: self.current_island,
1783                });
1784
1785                let main_pred = self.substitute_constant_with_var(predicate, noun, x)?;
1786
1787                let type_and_unique = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1788                    left: type_pred,
1789                    op: TokenType::And,
1790                    right: uniqueness,
1791                });
1792                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1793                    left: type_and_unique,
1794                    op: TokenType::And,
1795                    right: main_pred,
1796                });
1797
1798                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1799                    kind: QuantifierKind::Existential,
1800                    variable: x,
1801                    body,
1802                    island_id: self.current_island,
1803                }))
1804            }
1805            Some(Definiteness::Proximal) | Some(Definiteness::Distal) => {
1806                let var = self.next_var_name();
1807
1808                let mut restriction = self.ctx.exprs.alloc(LogicExpr::Predicate {
1809                    name: noun,
1810                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1811                    world: None,
1812                });
1813
1814                let deictic_name = if matches!(definiteness, Some(Definiteness::Proximal)) {
1815                    self.interner.intern("Proximal")
1816                } else {
1817                    self.interner.intern("Distal")
1818                };
1819                let deictic_pred = self.ctx.exprs.alloc(LogicExpr::Predicate {
1820                    name: deictic_name,
1821                    args: self.ctx.terms.alloc_slice([Term::Variable(var)]),
1822                    world: None,
1823                });
1824                restriction = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1825                    left: restriction,
1826                    op: TokenType::And,
1827                    right: deictic_pred,
1828                });
1829
1830                let substituted = self.substitute_constant_with_var(predicate, noun, var)?;
1831                let body = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1832                    left: restriction,
1833                    op: TokenType::And,
1834                    right: substituted,
1835                });
1836                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1837                    kind: QuantifierKind::Existential,
1838                    variable: var,
1839                    body,
1840                    island_id: self.current_island,
1841                }))
1842            }
1843            None => Ok(predicate),
1844        }
1845    }
1846
1847    fn substitute_pp_placeholder(&mut self, pp: &'a LogicExpr<'a>, var: Symbol) -> &'a LogicExpr<'a> {
1848        let placeholder = self.interner.intern("_PP_SELF_");
1849        match pp {
1850            LogicExpr::Predicate { name, args, .. } => {
1851                let new_args: Vec<Term<'a>> = args
1852                    .iter()
1853                    .map(|arg| match arg {
1854                        Term::Variable(v) if *v == placeholder => Term::Variable(var),
1855                        other => *other,
1856                    })
1857                    .collect();
1858                self.ctx.exprs.alloc(LogicExpr::Predicate {
1859                    name: *name,
1860                    args: self.ctx.terms.alloc_slice(new_args),
1861                    world: None,
1862                })
1863            }
1864            _ => pp,
1865        }
1866    }
1867
1868    fn substitute_constant_with_var(
1869        &self,
1870        expr: &'a LogicExpr<'a>,
1871        constant_name: Symbol,
1872        var_name: Symbol,
1873    ) -> ParseResult<&'a LogicExpr<'a>> {
1874        match expr {
1875            LogicExpr::Predicate { name, args, .. } => {
1876                let new_args: Vec<Term<'a>> = args
1877                    .iter()
1878                    .map(|arg| match arg {
1879                        Term::Constant(c) if *c == constant_name => Term::Variable(var_name),
1880                        Term::Constant(c) => Term::Constant(*c),
1881                        Term::Variable(v) => Term::Variable(*v),
1882                        Term::Function(n, a) => Term::Function(*n, *a),
1883                        Term::Group(m) => Term::Group(*m),
1884                        Term::Possessed { possessor, possessed } => Term::Possessed {
1885                            possessor: *possessor,
1886                            possessed: *possessed,
1887                        },
1888                        Term::Sigma(p) => Term::Sigma(*p),
1889                        Term::Intension(p) => Term::Intension(*p),
1890                        Term::Proposition(e) => Term::Proposition(*e),
1891                        Term::Value { kind, unit, dimension } => Term::Value {
1892                            kind: *kind,
1893                            unit: *unit,
1894                            dimension: *dimension,
1895                        },
1896                    })
1897                    .collect();
1898                Ok(self.ctx.exprs.alloc(LogicExpr::Predicate {
1899                    name: *name,
1900                    args: self.ctx.terms.alloc_slice(new_args),
1901                    world: None,
1902                }))
1903            }
1904            LogicExpr::Temporal { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
1905                operator: *operator,
1906                body: self.substitute_constant_with_var(body, constant_name, var_name)?,
1907            })),
1908            LogicExpr::Aspectual { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Aspectual {
1909                operator: *operator,
1910                body: self.substitute_constant_with_var(body, constant_name, var_name)?,
1911            })),
1912            LogicExpr::UnaryOp { op, operand } => Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
1913                op: op.clone(),
1914                operand: self.substitute_constant_with_var(operand, constant_name, var_name)?,
1915            })),
1916            LogicExpr::BinaryOp { left, op, right } => Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
1917                left: self.substitute_constant_with_var(left, constant_name, var_name)?,
1918                op: op.clone(),
1919                right: self.substitute_constant_with_var(right, constant_name, var_name)?,
1920            })),
1921            LogicExpr::Event { predicate, adverbs } => Ok(self.ctx.exprs.alloc(LogicExpr::Event {
1922                predicate: self.substitute_constant_with_var(predicate, constant_name, var_name)?,
1923                adverbs: *adverbs,
1924            })),
1925            LogicExpr::TemporalAnchor { anchor, body } => {
1926                Ok(self.ctx.exprs.alloc(LogicExpr::TemporalAnchor {
1927                    anchor: *anchor,
1928                    body: self.substitute_constant_with_var(body, constant_name, var_name)?,
1929                }))
1930            }
1931            LogicExpr::NeoEvent(data) => {
1932                // Substitute constants in thematic roles (Agent, Theme, etc.)
1933                let new_roles: Vec<(crate::ast::ThematicRole, Term<'a>)> = data
1934                    .roles
1935                    .iter()
1936                    .map(|(role, term)| {
1937                        let new_term = match term {
1938                            Term::Constant(c) if *c == constant_name => Term::Variable(var_name),
1939                            Term::Constant(c) => Term::Constant(*c),
1940                            Term::Variable(v) => Term::Variable(*v),
1941                            Term::Function(n, a) => Term::Function(*n, *a),
1942                            Term::Group(m) => Term::Group(*m),
1943                            Term::Possessed { possessor, possessed } => Term::Possessed {
1944                                possessor: *possessor,
1945                                possessed: *possessed,
1946                            },
1947                            Term::Sigma(p) => Term::Sigma(*p),
1948                            Term::Intension(p) => Term::Intension(*p),
1949                            Term::Proposition(e) => Term::Proposition(*e),
1950                            Term::Value { kind, unit, dimension } => Term::Value {
1951                                kind: *kind,
1952                                unit: *unit,
1953                                dimension: *dimension,
1954                            },
1955                        };
1956                        (*role, new_term)
1957                    })
1958                    .collect();
1959                Ok(self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(crate::ast::NeoEventData {
1960                    event_var: data.event_var,
1961                    verb: data.verb,
1962                    roles: self.ctx.roles.alloc_slice(new_roles),
1963                    modifiers: data.modifiers,
1964                    suppress_existential: data.suppress_existential,
1965                    world: None,
1966                }))))
1967            }
1968            // Recurse into nested quantifiers to substitute constants in their bodies
1969            LogicExpr::Quantifier { kind, variable, body, island_id } => {
1970                let new_body = self.substitute_constant_with_var(body, constant_name, var_name)?;
1971                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
1972                    kind: *kind,
1973                    variable: *variable,
1974                    body: new_body,
1975                    island_id: *island_id,
1976                }))
1977            }
1978            _ => Ok(expr),
1979        }
1980    }
1981
1982    fn substitute_constant_with_var_sym(
1983        &self,
1984        expr: &'a LogicExpr<'a>,
1985        constant_name: Symbol,
1986        var_name: Symbol,
1987    ) -> ParseResult<&'a LogicExpr<'a>> {
1988        self.substitute_constant_with_var(expr, constant_name, var_name)
1989    }
1990
1991    fn substitute_constant_with_sigma(
1992        &self,
1993        expr: &'a LogicExpr<'a>,
1994        constant_name: Symbol,
1995        sigma_term: Term<'a>,
1996    ) -> ParseResult<&'a LogicExpr<'a>> {
1997        match expr {
1998            LogicExpr::Predicate { name, args, .. } => {
1999                let new_args: Vec<Term<'a>> = args
2000                    .iter()
2001                    .map(|arg| match arg {
2002                        Term::Constant(c) if *c == constant_name => sigma_term.clone(),
2003                        Term::Constant(c) => Term::Constant(*c),
2004                        Term::Variable(v) => Term::Variable(*v),
2005                        Term::Function(n, a) => Term::Function(*n, *a),
2006                        Term::Group(m) => Term::Group(*m),
2007                        Term::Possessed { possessor, possessed } => Term::Possessed {
2008                            possessor: *possessor,
2009                            possessed: *possessed,
2010                        },
2011                        Term::Sigma(p) => Term::Sigma(*p),
2012                        Term::Intension(p) => Term::Intension(*p),
2013                        Term::Proposition(e) => Term::Proposition(*e),
2014                        Term::Value { kind, unit, dimension } => Term::Value {
2015                            kind: *kind,
2016                            unit: *unit,
2017                            dimension: *dimension,
2018                        },
2019                    })
2020                    .collect();
2021                Ok(self.ctx.exprs.alloc(LogicExpr::Predicate {
2022                    name: *name,
2023                    args: self.ctx.terms.alloc_slice(new_args),
2024                    world: None,
2025                }))
2026            }
2027            LogicExpr::Temporal { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
2028                operator: *operator,
2029                body: self.substitute_constant_with_sigma(body, constant_name, sigma_term)?,
2030            })),
2031            LogicExpr::Aspectual { operator, body } => Ok(self.ctx.exprs.alloc(LogicExpr::Aspectual {
2032                operator: *operator,
2033                body: self.substitute_constant_with_sigma(body, constant_name, sigma_term)?,
2034            })),
2035            LogicExpr::UnaryOp { op, operand } => Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2036                op: op.clone(),
2037                operand: self.substitute_constant_with_sigma(operand, constant_name, sigma_term)?,
2038            })),
2039            LogicExpr::BinaryOp { left, op, right } => Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2040                left: self.substitute_constant_with_sigma(
2041                    left,
2042                    constant_name,
2043                    sigma_term.clone(),
2044                )?,
2045                op: op.clone(),
2046                right: self.substitute_constant_with_sigma(right, constant_name, sigma_term)?,
2047            })),
2048            LogicExpr::Event { predicate, adverbs } => Ok(self.ctx.exprs.alloc(LogicExpr::Event {
2049                predicate: self.substitute_constant_with_sigma(
2050                    predicate,
2051                    constant_name,
2052                    sigma_term,
2053                )?,
2054                adverbs: *adverbs,
2055            })),
2056            LogicExpr::TemporalAnchor { anchor, body } => {
2057                Ok(self.ctx.exprs.alloc(LogicExpr::TemporalAnchor {
2058                    anchor: *anchor,
2059                    body: self.substitute_constant_with_sigma(body, constant_name, sigma_term)?,
2060                }))
2061            }
2062            LogicExpr::NeoEvent(data) => {
2063                let new_roles: Vec<(crate::ast::ThematicRole, Term<'a>)> = data
2064                    .roles
2065                    .iter()
2066                    .map(|(role, term)| {
2067                        let new_term = match term {
2068                            Term::Constant(c) if *c == constant_name => sigma_term.clone(),
2069                            Term::Constant(c) => Term::Constant(*c),
2070                            Term::Variable(v) => Term::Variable(*v),
2071                            Term::Function(n, a) => Term::Function(*n, *a),
2072                            Term::Group(m) => Term::Group(*m),
2073                            Term::Possessed { possessor, possessed } => Term::Possessed {
2074                                possessor: *possessor,
2075                                possessed: *possessed,
2076                            },
2077                            Term::Sigma(p) => Term::Sigma(*p),
2078                            Term::Intension(p) => Term::Intension(*p),
2079                            Term::Proposition(e) => Term::Proposition(*e),
2080                            Term::Value { kind, unit, dimension } => Term::Value {
2081                                kind: *kind,
2082                                unit: *unit,
2083                                dimension: *dimension,
2084                            },
2085                        };
2086                        (*role, new_term)
2087                    })
2088                    .collect();
2089                Ok(self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(crate::ast::NeoEventData {
2090                    event_var: data.event_var,
2091                    verb: data.verb,
2092                    roles: self.ctx.roles.alloc_slice(new_roles),
2093                    modifiers: data.modifiers,
2094                    suppress_existential: data.suppress_existential,
2095                    world: None,
2096                }))))
2097            }
2098            LogicExpr::Distributive { predicate } => Ok(self.ctx.exprs.alloc(LogicExpr::Distributive {
2099                predicate: self.substitute_constant_with_sigma(predicate, constant_name, sigma_term)?,
2100            })),
2101            _ => Ok(expr),
2102        }
2103    }
2104
2105    fn find_main_verb_name(&self, expr: &LogicExpr<'a>) -> Option<Symbol> {
2106        match expr {
2107            LogicExpr::Predicate { name, .. } => Some(*name),
2108            LogicExpr::NeoEvent(data) => Some(data.verb),
2109            LogicExpr::Temporal { body, .. } => self.find_main_verb_name(body),
2110            LogicExpr::Aspectual { body, .. } => self.find_main_verb_name(body),
2111            LogicExpr::Event { predicate, .. } => self.find_main_verb_name(predicate),
2112            LogicExpr::TemporalAnchor { body, .. } => self.find_main_verb_name(body),
2113            LogicExpr::UnaryOp { operand, .. } => self.find_main_verb_name(operand),
2114            LogicExpr::BinaryOp { left, .. } => self.find_main_verb_name(left),
2115            _ => None,
2116        }
2117    }
2118
2119    fn transform_cardinal_to_group(&mut self, expr: &'a LogicExpr<'a>) -> ParseResult<&'a LogicExpr<'a>> {
2120        match expr {
2121            LogicExpr::Quantifier { kind: QuantifierKind::Cardinal(n), variable, body, .. } => {
2122                let group_var = self.interner.intern("g");
2123                let member_var = *variable;
2124
2125                // Extract the restriction (first conjunct) and the body (rest)
2126                // The structure is: restriction ∧ body_rest
2127                let (restriction, body_rest) = match body {
2128                    LogicExpr::BinaryOp { left, op: TokenType::And, right } => (*left, *right),
2129                    _ => return Ok(expr),
2130                };
2131
2132                // Substitute the member variable with the group variable in the body
2133                let transformed_body = self.substitute_constant_with_var_sym(body_rest, member_var, group_var)?;
2134
2135                Ok(self.ctx.exprs.alloc(LogicExpr::GroupQuantifier {
2136                    group_var,
2137                    count: *n,
2138                    member_var,
2139                    restriction,
2140                    body: transformed_body,
2141                }))
2142            }
2143            // Recursively transform nested expressions
2144            LogicExpr::Temporal { operator, body } => {
2145                let transformed = self.transform_cardinal_to_group(body)?;
2146                Ok(self.ctx.exprs.alloc(LogicExpr::Temporal {
2147                    operator: *operator,
2148                    body: transformed,
2149                }))
2150            }
2151            LogicExpr::Aspectual { operator, body } => {
2152                let transformed = self.transform_cardinal_to_group(body)?;
2153                Ok(self.ctx.exprs.alloc(LogicExpr::Aspectual {
2154                    operator: *operator,
2155                    body: transformed,
2156                }))
2157            }
2158            LogicExpr::UnaryOp { op, operand } => {
2159                let transformed = self.transform_cardinal_to_group(operand)?;
2160                Ok(self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2161                    op: op.clone(),
2162                    operand: transformed,
2163                }))
2164            }
2165            LogicExpr::BinaryOp { left, op, right } => {
2166                let transformed_left = self.transform_cardinal_to_group(left)?;
2167                let transformed_right = self.transform_cardinal_to_group(right)?;
2168                Ok(self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2169                    left: transformed_left,
2170                    op: op.clone(),
2171                    right: transformed_right,
2172                }))
2173            }
2174            LogicExpr::Distributive { predicate } => {
2175                let transformed = self.transform_cardinal_to_group(predicate)?;
2176                Ok(self.ctx.exprs.alloc(LogicExpr::Distributive {
2177                    predicate: transformed,
2178                }))
2179            }
2180            LogicExpr::Quantifier { kind, variable, body, island_id } => {
2181                let transformed = self.transform_cardinal_to_group(body)?;
2182                Ok(self.ctx.exprs.alloc(LogicExpr::Quantifier {
2183                    kind: kind.clone(),
2184                    variable: *variable,
2185                    body: transformed,
2186                    island_id: *island_id,
2187                }))
2188            }
2189            _ => Ok(expr),
2190        }
2191    }
2192
2193    fn build_verb_neo_event(
2194        &mut self,
2195        verb: Symbol,
2196        subject_var: Symbol,
2197        object: Option<Term<'a>>,
2198        modifiers: Vec<Symbol>,
2199    ) -> &'a LogicExpr<'a> {
2200        let event_var = self.get_event_var();
2201
2202        // Check if verb is unaccusative (intransitive subject is Theme, not Agent)
2203        let verb_str = self.interner.resolve(verb).to_lowercase();
2204        let is_unaccusative = lookup_verb_db(&verb_str)
2205            .map(|meta| meta.features.contains(&Feature::Unaccusative))
2206            .unwrap_or(false);
2207
2208        // Determine subject role: unaccusative verbs without object use Theme
2209        let has_object = object.is_some();
2210        let subject_role = if is_unaccusative && !has_object {
2211            ThematicRole::Theme
2212        } else {
2213            ThematicRole::Agent
2214        };
2215
2216        // Build roles vector
2217        let mut roles = vec![(subject_role, Term::Variable(subject_var))];
2218        if let Some(obj_term) = object {
2219            roles.push((ThematicRole::Theme, obj_term));
2220        }
2221
2222        // Create NeoEventData with suppress_existential: false
2223        // Each quantified individual gets their own event (distributive reading)
2224        self.ctx.exprs.alloc(LogicExpr::NeoEvent(Box::new(NeoEventData {
2225            event_var,
2226            verb,
2227            roles: self.ctx.roles.alloc_slice(roles),
2228            modifiers: self.ctx.syms.alloc_slice(modifiers),
2229            suppress_existential: false,
2230            world: None,
2231        })))
2232    }
2233}
2234
2235// Helper methods for donkey binding scope handling
2236impl<'a, 'ctx, 'int> Parser<'a, 'ctx, 'int> {
2237    /// Check if an expression mentions a specific variable
2238    fn expr_mentions_var(&self, expr: &LogicExpr<'a>, var: Symbol) -> bool {
2239        match expr {
2240            LogicExpr::Predicate { args, .. } => {
2241                args.iter().any(|term| self.term_mentions_var(term, var))
2242            }
2243            LogicExpr::BinaryOp { left, right, .. } => {
2244                self.expr_mentions_var(left, var) || self.expr_mentions_var(right, var)
2245            }
2246            LogicExpr::UnaryOp { operand, .. } => self.expr_mentions_var(operand, var),
2247            LogicExpr::Quantifier { body, .. } => self.expr_mentions_var(body, var),
2248            LogicExpr::NeoEvent(data) => {
2249                data.roles.iter().any(|(_, term)| self.term_mentions_var(term, var))
2250            }
2251            LogicExpr::Temporal { body, .. } => self.expr_mentions_var(body, var),
2252            LogicExpr::Aspectual { body, .. } => self.expr_mentions_var(body, var),
2253            LogicExpr::Event { predicate, .. } => self.expr_mentions_var(predicate, var),
2254            LogicExpr::Modal { operand, .. } => self.expr_mentions_var(operand, var),
2255            LogicExpr::Scopal { body, .. } => self.expr_mentions_var(body, var),
2256            _ => false,
2257        }
2258    }
2259
2260    fn term_mentions_var(&self, term: &Term<'a>, var: Symbol) -> bool {
2261        match term {
2262            Term::Variable(v) => *v == var,
2263            Term::Function(_, args) => args.iter().any(|t| self.term_mentions_var(t, var)),
2264            _ => false,
2265        }
2266    }
2267
2268    /// Collect all conjuncts from a conjunction tree
2269    fn collect_conjuncts(&self, expr: &'a LogicExpr<'a>) -> Vec<&'a LogicExpr<'a>> {
2270        match expr {
2271            LogicExpr::BinaryOp { left, op: TokenType::And, right } => {
2272                let mut result = self.collect_conjuncts(left);
2273                result.extend(self.collect_conjuncts(right));
2274                result
2275            }
2276            _ => vec![expr],
2277        }
2278    }
2279
2280    /// Wrap unused donkey bindings inside the restriction/body of a quantifier structure.
2281    ///
2282    /// For universals (implications):
2283    ///   Transform: ∀x((P(x) ∧ Q(y)) → R(x)) with unused y
2284    ///   Into:      ∀x((P(x) ∧ ∃y(Q(y))) → R(x))
2285    ///
2286    /// For existentials (conjunctions):
2287    ///   Transform: ∃x(P(x) ∧ Q(y) ∧ R(x)) with unused y
2288    ///   Into:      ∃x(P(x) ∧ ∃y(Q(y)) ∧ R(x))
2289    ///
2290    /// If wide_scope_negation is true, wrap the existential in negation:
2291    ///   Into:      ∀x((P(x) ∧ ¬∃y(Q(y))) → R(x))
2292    fn wrap_donkey_in_restriction(
2293        &self,
2294        body: &'a LogicExpr<'a>,
2295        donkey_var: Symbol,
2296        wide_scope_negation: bool,
2297    ) -> &'a LogicExpr<'a> {
2298        // Handle Quantifier wrapping first
2299        if let LogicExpr::Quantifier { kind, variable, body: inner_body, island_id } = body {
2300            let transformed = self.wrap_donkey_in_restriction(inner_body, donkey_var, wide_scope_negation);
2301            return self.ctx.exprs.alloc(LogicExpr::Quantifier {
2302                kind: kind.clone(),
2303                variable: *variable,
2304                body: transformed,
2305                island_id: *island_id,
2306            });
2307        }
2308
2309        // Handle implication (universal quantifiers)
2310        if let LogicExpr::BinaryOp { left, op: TokenType::Implies, right } = body {
2311            return self.wrap_in_implication(*left, *right, donkey_var, wide_scope_negation);
2312        }
2313
2314        // Handle conjunction (existential quantifiers)
2315        if let LogicExpr::BinaryOp { left: _, op: TokenType::And, right: _ } = body {
2316            return self.wrap_in_conjunction(body, donkey_var, wide_scope_negation);
2317        }
2318
2319        // Not a structure we can process
2320        body
2321    }
2322
2323    /// Wrap donkey binding in an implication structure (∀x(P(x) → Q(x)))
2324    fn wrap_in_implication(
2325        &self,
2326        restriction: &'a LogicExpr<'a>,
2327        consequent: &'a LogicExpr<'a>,
2328        donkey_var: Symbol,
2329        wide_scope_negation: bool,
2330    ) -> &'a LogicExpr<'a> {
2331        // Collect all conjuncts in the restriction
2332        let conjuncts = self.collect_conjuncts(restriction);
2333
2334        // Partition into those mentioning the donkey var and those not
2335        let (with_var, without_var): (Vec<_>, Vec<_>) = conjuncts
2336            .into_iter()
2337            .partition(|c| self.expr_mentions_var(c, donkey_var));
2338
2339        if with_var.is_empty() {
2340            // Variable not found in restriction, return original implication
2341            return self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2342                left: restriction,
2343                op: TokenType::Implies,
2344                right: consequent,
2345            });
2346        }
2347
2348        // Combine the "with var" conjuncts
2349        let with_var_combined = self.combine_conjuncts(&with_var);
2350
2351        // Wrap with existential
2352        let existential = self.ctx.exprs.alloc(LogicExpr::Quantifier {
2353            kind: QuantifierKind::Existential,
2354            variable: donkey_var,
2355            body: with_var_combined,
2356            island_id: self.current_island,
2357        });
2358
2359        // For wide scope negation (de dicto reading of "lacks"), wrap ∃ in ¬
2360        let wrapped = if wide_scope_negation {
2361            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2362                op: TokenType::Not,
2363                operand: existential,
2364            })
2365        } else {
2366            existential
2367        };
2368
2369        // Combine with "without var" conjuncts
2370        let new_restriction = if without_var.is_empty() {
2371            wrapped
2372        } else {
2373            let without_combined = self.combine_conjuncts(&without_var);
2374            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2375                left: without_combined,
2376                op: TokenType::And,
2377                right: wrapped,
2378            })
2379        };
2380
2381        // Rebuild the implication
2382        self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2383            left: new_restriction,
2384            op: TokenType::Implies,
2385            right: consequent,
2386        })
2387    }
2388
2389    /// Wrap donkey binding in a conjunction structure (∃x(P(x) ∧ Q(x)))
2390    fn wrap_in_conjunction(
2391        &self,
2392        body: &'a LogicExpr<'a>,
2393        donkey_var: Symbol,
2394        wide_scope_negation: bool,
2395    ) -> &'a LogicExpr<'a> {
2396        // Collect all conjuncts
2397        let conjuncts = self.collect_conjuncts(body);
2398
2399        // Partition into those mentioning the donkey var and those not
2400        let (with_var, without_var): (Vec<_>, Vec<_>) = conjuncts
2401            .into_iter()
2402            .partition(|c| self.expr_mentions_var(c, donkey_var));
2403
2404        if with_var.is_empty() {
2405            // Variable not found, return unchanged
2406            return body;
2407        }
2408
2409        // Combine the "with var" conjuncts
2410        let with_var_combined = self.combine_conjuncts(&with_var);
2411
2412        // Wrap with existential
2413        let existential = self.ctx.exprs.alloc(LogicExpr::Quantifier {
2414            kind: QuantifierKind::Existential,
2415            variable: donkey_var,
2416            body: with_var_combined,
2417            island_id: self.current_island,
2418        });
2419
2420        // For wide scope negation (de dicto reading of "lacks"), wrap ∃ in ¬
2421        let wrapped = if wide_scope_negation {
2422            self.ctx.exprs.alloc(LogicExpr::UnaryOp {
2423                op: TokenType::Not,
2424                operand: existential,
2425            })
2426        } else {
2427            existential
2428        };
2429
2430        // Combine with "without var" conjuncts
2431        if without_var.is_empty() {
2432            wrapped
2433        } else {
2434            let without_combined = self.combine_conjuncts(&without_var);
2435            self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2436                left: without_combined,
2437                op: TokenType::And,
2438                right: wrapped,
2439            })
2440        }
2441    }
2442
2443    fn combine_conjuncts(&self, conjuncts: &[&'a LogicExpr<'a>]) -> &'a LogicExpr<'a> {
2444        if conjuncts.is_empty() {
2445            panic!("Cannot combine empty conjuncts");
2446        }
2447        if conjuncts.len() == 1 {
2448            return conjuncts[0];
2449        }
2450        let mut result = conjuncts[0];
2451        for c in &conjuncts[1..] {
2452            result = self.ctx.exprs.alloc(LogicExpr::BinaryOp {
2453                left: result,
2454                op: TokenType::And,
2455                right: *c,
2456            });
2457        }
2458        result
2459    }
2460}
logicaffeine_language/parser/quantifier.rs

logicaffeine_language/parser/
quantifier.rs
