logicaffeine_language/ast/
logic.rs

1//! Logic expression AST types for first-order logic with modal and event extensions.
2//!
3//! This module defines the core logical expression types including:
4//!
5//! - **[`LogicExpr`]**: The main expression enum with all logical constructs
6//! - **[`Term`]**: Terms (constants, variables, function applications)
7//! - **[`NounPhrase`]**: Parsed noun phrase structure
8//! - **Semantic types**: Montague-style type markers
9//! - **Event roles**: Neo-Davidsonian thematic roles (Agent, Theme, Goal, etc.)
10//! - **Modal vectors**: Kripke semantics parameters (domain, flavor, force)
11//! - **Temporal operators**: Past, future, perfect, progressive
12//!
13//! All types use arena allocation with the `'a` lifetime parameter.
14
15use logicaffeine_base::Arena;
16use logicaffeine_base::Symbol;
17use crate::lexicon::Definiteness;
18use crate::token::TokenType;
19
20// ═══════════════════════════════════════════════════════════════════
21// Semantic Types (Montague Grammar)
22// ═══════════════════════════════════════════════════════════════════
23
24/// Montague semantic types for compositional interpretation.
25///
26/// These types classify expressions according to their denotation in
27/// a model-theoretic semantics, following Montague's "Universal Grammar".
28#[derive(Debug, Clone, Copy, PartialEq, Eq)]
29pub enum LogicalType {
30    /// Type `e`: Individuals (entities) like "John" or "the ball".
31    Entity,
32    /// Type `t`: Truth values (propositions) like "John runs".
33    TruthValue,
34    /// Type `<e,t>`: Properties (one-place predicates) like "is a unicorn".
35    Property,
36    /// Type `<<e,t>,t>`: Generalized quantifiers like "every man" or "a woman".
37    Quantifier,
38}
39
40// ═══════════════════════════════════════════════════════════════════
41// Degree Semantics (Prover-Ready Number System)
42// ═══════════════════════════════════════════════════════════════════
43
44/// Physical dimension for degree semantics and unit tracking.
45///
46/// Used with [`NumberKind`] to enable dimensional analysis and prevent
47/// nonsensical comparisons (e.g., adding meters to seconds).
48#[derive(Debug, Clone, Copy, PartialEq, Eq)]
49pub enum Dimension {
50    /// Spatial extent (meters, feet, inches).
51    Length,
52    /// Temporal duration (seconds, minutes, hours).
53    Time,
54    /// Mass (kilograms, pounds).
55    Weight,
56    /// Thermal measure (Celsius, Fahrenheit, Kelvin).
57    Temperature,
58    /// Count of discrete items.
59    Cardinality,
60}
61
62/// Numeric literal representation for degree semantics.
63///
64/// Supports exact integers, floating-point reals, and symbolic constants
65/// (e.g., π, e) for prover integration.
66#[derive(Debug, Clone, Copy, PartialEq)]
67pub enum NumberKind {
68    /// Floating-point real number (e.g., 3.14, 0.5).
69    Real(f64),
70    /// Exact integer (e.g., 42, -1, 0).
71    Integer(i64),
72    /// Symbolic constant (e.g., π, e, ∞).
73    Symbolic(Symbol),
74}
75
76// ═══════════════════════════════════════════════════════════════════
77// First-Order Logic Types (FOL Upgrade)
78// ═══════════════════════════════════════════════════════════════════
79
80/// First-order logic term representing entities or values.
81///
82/// Terms denote individuals, groups, or computed values in the domain
83/// of discourse. They serve as arguments to predicates.
84#[derive(Debug, Clone, Copy)]
85pub enum Term<'a> {
86    /// Named individual constant (e.g., `john`, `paris`).
87    Constant(Symbol),
88    /// Bound or free variable (e.g., `x`, `y`).
89    Variable(Symbol),
90    /// Function application: `f(t1, t2, ...)` (e.g., `mother(john)`).
91    Function(Symbol, &'a [Term<'a>]),
92    /// Plural group for collective readings (e.g., `john ⊕ mary`).
93    Group(&'a [Term<'a>]),
94    /// Possessive construction: `john's book` → `Poss(john, book)`.
95    Possessed { possessor: &'a Term<'a>, possessed: Symbol },
96    /// Definite description σ-term: `σx.P(x)` ("the unique x such that P").
97    Sigma(Symbol),
98    /// Intensional term (Montague up-arrow `^P`) for de dicto readings.
99    Intension(Symbol),
100    /// Sentential complement (embedded clause as propositional argument).
101    Proposition(&'a LogicExpr<'a>),
102    /// Numeric value with optional unit and dimension.
103    Value {
104        kind: NumberKind,
105        unit: Option<Symbol>,
106        dimension: Option<Dimension>,
107    },
108}
109
110/// Quantifier types for first-order and generalized quantifiers.
111///
112/// Extends standard FOL with generalized quantifiers that cannot be
113/// expressed with ∀ and ∃ alone (e.g., "most", "few", "at least 3").
114#[derive(Debug, Clone, Copy, PartialEq, Eq)]
115pub enum QuantifierKind {
116    /// Universal: ∀x ("every", "all", "each").
117    Universal,
118    /// Existential: ∃x ("some", "a", "an").
119    Existential,
120    /// Proportional: "most X are Y" (>50% of domain).
121    Most,
122    /// Proportional: "few X are Y" (<expected proportion).
123    Few,
124    /// Vague large quantity: "many X are Y".
125    Many,
126    /// Exact count: "exactly n X are Y".
127    Cardinal(u32),
128    /// Lower bound: "at least n X are Y".
129    AtLeast(u32),
130    /// Upper bound: "at most n X are Y".
131    AtMost(u32),
132    /// Generic: "cats meow" (characterizing generalization).
133    Generic,
134}
135
136/// Binary logical connectives.
137#[derive(Debug, Clone, Copy, PartialEq, Eq)]
138pub enum BinaryOpKind {
139    /// Conjunction: P ∧ Q.
140    And,
141    /// Disjunction: P ∨ Q.
142    Or,
143    /// Material implication: P → Q.
144    Implies,
145    /// Biconditional: P ↔ Q.
146    Iff,
147}
148
149/// Unary logical operators.
150#[derive(Debug, Clone, Copy, PartialEq, Eq)]
151pub enum UnaryOpKind {
152    /// Negation: ¬P.
153    Not,
154}
155
156// ═══════════════════════════════════════════════════════════════════
157// Temporal & Aspect Operators (Arthur Prior's Tense Logic)
158// ═══════════════════════════════════════════════════════════════════
159
160/// Temporal logic operators.
161///
162/// Prior-style tense operators (Past, Future) for linguistic temporality.
163/// Pnueli-style LTL operators (Always, Eventually, Next) for hardware verification.
164#[derive(Debug, Clone, Copy, PartialEq, Eq)]
165pub enum TemporalOperator {
166    /// Past tense: P(φ) — "it was the case that φ".
167    Past,
168    /// Future tense: F(φ) — "it will be the case that φ".
169    Future,
170    /// Always/Globally: G(φ) — φ holds at every future state.
171    Always,
172    /// Eventually/Finally: F(φ) — φ holds at some future state.
173    Eventually,
174    /// Next: X(φ) — φ holds at the immediate next state.
175    Next,
176    /// Bounded Eventually: F≤n(φ) — φ holds within n steps.
177    /// SVA target: `##[0:n] φ`
178    BoundedEventually(u32),
179}
180
181/// Binary temporal operators (LTL).
182///
183/// These require two operands and express relationships between
184/// properties over time in hardware state machines.
185#[derive(Debug, Clone, Copy, PartialEq, Eq)]
186pub enum BinaryTemporalOp {
187    /// φ U ψ — φ holds until ψ becomes true.
188    Until,
189    /// φ R ψ — dual of Until: ψ holds until φ releases it (or forever).
190    Release,
191    /// φ W ψ — weak until: φ holds until ψ, or φ holds forever.
192    WeakUntil,
193}
194
195// ═══════════════════════════════════════════════════════════════════
196// Event Semantics (Neo-Davidsonian)
197// ═══════════════════════════════════════════════════════════════════
198
199/// Neo-Davidsonian thematic roles for event semantics.
200///
201/// Following Parsons' neo-Davidsonian analysis, events are reified and
202/// participants are related to events via thematic role predicates:
203/// `∃e(Run(e) ∧ Agent(e, john) ∧ Location(e, park))`.
204#[derive(Debug, Clone, Copy, PartialEq, Eq)]
205pub enum ThematicRole {
206    /// Animate initiator of action (e.g., "John" in "John ran").
207    Agent,
208    /// Entity affected by action (e.g., "the window" in "broke the window").
209    Patient,
210    /// Entity involved without change (e.g., "the ball" in "saw the ball").
211    Theme,
212    /// Animate entity receiving something (e.g., "Mary" in "gave Mary a book").
213    Recipient,
214    /// Destination or endpoint (e.g., "Paris" in "went to Paris").
215    Goal,
216    /// Origin or starting point (e.g., "London" in "came from London").
217    Source,
218    /// Tool or means (e.g., "a knife" in "cut with a knife").
219    Instrument,
220    /// Spatial setting (e.g., "the park" in "ran in the park").
221    Location,
222    /// Temporal setting (e.g., "yesterday" in "arrived yesterday").
223    Time,
224    /// How action was performed (e.g., "quickly" in "ran quickly").
225    Manner,
226}
227
228/// Grammatical aspect operators for event structure.
229///
230/// Aspect describes the internal temporal structure of events,
231/// distinct from tense which locates events in time.
232#[derive(Debug, Clone, Copy, PartialEq, Eq)]
233pub enum AspectOperator {
234    /// Ongoing action: "is running" → PROG(Run(e)).
235    Progressive,
236    /// Completed with present relevance: "has eaten" → PERF(Eat(e)).
237    Perfect,
238    /// Characteristic pattern: "smokes" (habitually) → HAB(Smoke(e)).
239    Habitual,
240    /// Repeated action: "kept knocking" → ITER(Knock(e)).
241    Iterative,
242}
243
244/// Grammatical voice operators.
245#[derive(Debug, Clone, Copy, PartialEq, Eq)]
246pub enum VoiceOperator {
247    /// Passive voice: "was eaten" promotes patient to subject position.
248    Passive,
249}
250
251// ═══════════════════════════════════════════════════════════════════
252// Legacy Types (kept during transition)
253// ═══════════════════════════════════════════════════════════════════
254
255/// Parsed noun phrase structure for compositional interpretation.
256///
257/// Captures the internal structure of noun phrases including determiners,
258/// modifiers, and possessives for correct semantic composition.
259#[derive(Debug)]
260pub struct NounPhrase<'a> {
261    /// Definiteness: the (definite), a/an (indefinite), or bare (none).
262    pub definiteness: Option<Definiteness>,
263    /// Pre-nominal adjectives (e.g., "big red" in "big red ball").
264    pub adjectives: &'a [Symbol],
265    /// Head noun (e.g., "ball" in "big red ball").
266    pub noun: Symbol,
267    /// Possessor phrase (e.g., "John's" in "John's book").
268    pub possessor: Option<&'a NounPhrase<'a>>,
269    /// Prepositional phrase modifiers attached to noun.
270    pub pps: &'a [&'a LogicExpr<'a>],
271    /// Superlative adjective if present (e.g., "tallest").
272    pub superlative: Option<Symbol>,
273}
274
275// ═══════════════════════════════════════════════════════════════════
276// Boxed Variant Data (keeps LogicExpr enum small)
277// ═══════════════════════════════════════════════════════════════════
278
279/// Aristotelian categorical proposition data.
280///
281/// Represents the four categorical forms (A, E, I, O):
282/// - A: All S are P
283/// - E: No S are P
284/// - I: Some S are P
285/// - O: Some S are not P
286#[derive(Debug)]
287pub struct CategoricalData<'a> {
288    /// The quantifier (All, No, Some).
289    pub quantifier: TokenType,
290    /// Subject term (S in "All S are P").
291    pub subject: NounPhrase<'a>,
292    /// Whether copula is negated (for O-form: "Some S are not P").
293    pub copula_negative: bool,
294    /// Predicate term (P in "All S are P").
295    pub predicate: NounPhrase<'a>,
296}
297
298/// Simple subject-verb-object relation data.
299#[derive(Debug)]
300pub struct RelationData<'a> {
301    /// Subject noun phrase.
302    pub subject: NounPhrase<'a>,
303    /// Verb predicate.
304    pub verb: Symbol,
305    /// Object noun phrase.
306    pub object: NounPhrase<'a>,
307}
308
309/// Neo-Davidsonian event structure with thematic roles.
310///
311/// Represents a verb event with its participants decomposed into
312/// separate thematic role predicates: `∃e(Run(e) ∧ Agent(e, john))`.
313#[derive(Debug)]
314pub struct NeoEventData<'a> {
315    /// The event variable (e, e1, e2, ...).
316    pub event_var: Symbol,
317    /// The verb predicate name.
318    pub verb: Symbol,
319    /// Thematic role assignments: (Role, Filler) pairs.
320    pub roles: &'a [(ThematicRole, Term<'a>)],
321    /// Adverbial modifiers (e.g., "quickly" → Quickly(e)).
322    pub modifiers: &'a [Symbol],
323    /// When true, suppress local ∃e quantification.
324    /// Used in DRT for generic conditionals where event var is bound by outer ∀.
325    pub suppress_existential: bool,
326    /// World argument for Kripke semantics. None = implicit actual world (w₀).
327    pub world: Option<Symbol>,
328}
329
330impl<'a> NounPhrase<'a> {
331    pub fn simple(noun: Symbol) -> Self {
332        NounPhrase {
333            definiteness: None,
334            adjectives: &[],
335            noun,
336            possessor: None,
337            pps: &[],
338            superlative: None,
339        }
340    }
341
342    pub fn with_definiteness(definiteness: Definiteness, noun: Symbol) -> Self {
343        NounPhrase {
344            definiteness: Some(definiteness),
345            adjectives: &[],
346            noun,
347            possessor: None,
348            pps: &[],
349            superlative: None,
350        }
351    }
352}
353
354/// Modal logic domain classification.
355///
356/// Determines the accessibility relation in Kripke semantics:
357/// what kinds of possible worlds are relevant.
358#[derive(Debug, Clone, Copy, PartialEq)]
359pub enum ModalDomain {
360    /// Alethic modality: logical/metaphysical possibility and necessity.
361    /// "It is possible that P" = P holds in some accessible world.
362    Alethic,
363    /// Deontic modality: obligation and permission.
364    /// "It is obligatory that P" = P holds in all deontically ideal worlds.
365    Deontic,
366    /// Temporal modality: hardware state transitions.
367    /// Accessibility = next-state relation (clock-cycle transitions).
368    Temporal,
369}
370
371/// Modal flavor affecting scope interpretation.
372///
373/// The distinction between root and epistemic modals affects
374/// quantifier scope: root modals scope under quantifiers (de re),
375/// while epistemic modals scope over quantifiers (de dicto).
376#[derive(Debug, Clone, Copy, PartialEq, Eq)]
377pub enum ModalFlavor {
378    /// Root modals express ability, obligation, or circumstantial possibility.
379    /// Verbs: can, must, should, shall, could, would.
380    /// Scope: NARROW (de re) — modal attaches inside quantifier scope.
381    /// Example: "Every student can solve this" = ∀x(Student(x) → ◇Solve(x, this))
382    Root,
383    /// Epistemic modals express possibility or deduction based on evidence.
384    /// Verbs: might, may (epistemic readings).
385    /// Scope: WIDE (de dicto) — modal wraps the entire quantified formula.
386    /// Example: "A student might win" = ◇∃x(Student(x) ∧ Win(x))
387    Epistemic,
388}
389
390/// Modal operator parameters for Kripke semantics.
391///
392/// Combines domain (what kind of modality), force (necessity vs possibility),
393/// and flavor (scope behavior) into a single modal specification.
394#[derive(Debug, Clone, Copy, PartialEq)]
395pub struct ModalVector {
396    /// The modal domain: alethic or deontic.
397    pub domain: ModalDomain,
398    /// Modal force: 1.0 = necessity (□), 0.5 = possibility (◇), graded values between.
399    pub force: f32,
400    /// Scope flavor: root (narrow scope) or epistemic (wide scope).
401    pub flavor: ModalFlavor,
402}
403
404// ═══════════════════════════════════════════════════════════════════
405// Expression Enum (hybrid: old + new variants)
406// ═══════════════════════════════════════════════════════════════════
407
408/// First-order logic expression with modal, temporal, and event extensions.
409///
410/// This is the core AST type representing logical formulas. All nodes are
411/// arena-allocated with the `'a` lifetime tracking the arena's scope.
412///
413/// # Categories
414///
415/// - **Core FOL**: [`Predicate`], [`Quantifier`], [`BinaryOp`], [`UnaryOp`], [`Identity`]
416/// - **Lambda calculus**: [`Lambda`], [`App`], [`Atom`]
417/// - **Modal logic**: [`Modal`], [`Intensional`]
418/// - **Temporal/Aspect**: [`Temporal`], [`Aspectual`], [`Voice`]
419/// - **Event semantics**: [`Event`], [`NeoEvent`]
420/// - **Questions**: [`Question`], [`YesNoQuestion`]
421/// - **Pragmatics**: [`SpeechAct`], [`Focus`], [`Presupposition`]
422/// - **Comparison**: [`Comparative`], [`Superlative`]
423/// - **Other**: [`Counterfactual`], [`Causal`], [`Control`], [`Imperative`]
424///
425/// [`Predicate`]: LogicExpr::Predicate
426/// [`Quantifier`]: LogicExpr::Quantifier
427/// [`BinaryOp`]: LogicExpr::BinaryOp
428/// [`UnaryOp`]: LogicExpr::UnaryOp
429/// [`Identity`]: LogicExpr::Identity
430/// [`Lambda`]: LogicExpr::Lambda
431/// [`App`]: LogicExpr::App
432/// [`Atom`]: LogicExpr::Atom
433/// [`Modal`]: LogicExpr::Modal
434/// [`Intensional`]: LogicExpr::Intensional
435/// [`Temporal`]: LogicExpr::Temporal
436/// [`Aspectual`]: LogicExpr::Aspectual
437/// [`Voice`]: LogicExpr::Voice
438/// [`Event`]: LogicExpr::Event
439/// [`NeoEvent`]: LogicExpr::NeoEvent
440/// [`Question`]: LogicExpr::Question
441/// [`YesNoQuestion`]: LogicExpr::YesNoQuestion
442/// [`SpeechAct`]: LogicExpr::SpeechAct
443/// [`Focus`]: LogicExpr::Focus
444/// [`Presupposition`]: LogicExpr::Presupposition
445/// [`Comparative`]: LogicExpr::Comparative
446/// [`Superlative`]: LogicExpr::Superlative
447/// [`Counterfactual`]: LogicExpr::Counterfactual
448/// [`Causal`]: LogicExpr::Causal
449/// [`Control`]: LogicExpr::Control
450/// [`Imperative`]: LogicExpr::Imperative
451#[derive(Debug)]
452pub enum LogicExpr<'a> {
453    /// Atomic predicate: `P(t1, t2, ...)` with optional world parameter.
454    Predicate {
455        name: Symbol,
456        args: &'a [Term<'a>],
457        /// World argument for Kripke semantics. None = implicit actual world (w₀).
458        world: Option<Symbol>,
459    },
460
461    /// Identity statement: `t1 = t2`.
462    Identity {
463        left: &'a Term<'a>,
464        right: &'a Term<'a>,
465    },
466
467    /// Metaphorical assertion: tenor "is" vehicle (non-literal identity).
468    Metaphor {
469        tenor: &'a Term<'a>,
470        vehicle: &'a Term<'a>,
471    },
472
473    /// Quantified formula: `∀x.φ` or `∃x.φ` with scope island tracking.
474    Quantifier {
475        kind: QuantifierKind,
476        variable: Symbol,
477        body: &'a LogicExpr<'a>,
478        /// Island ID prevents illicit scope interactions across syntactic boundaries.
479        island_id: u32,
480    },
481
482    /// Aristotelian categorical proposition (boxed to keep enum small).
483    Categorical(Box<CategoricalData<'a>>),
484
485    /// Simple S-V-O relation (boxed).
486    Relation(Box<RelationData<'a>>),
487
488    /// Modal operator: □φ (necessity) or ◇φ (possibility).
489    Modal {
490        vector: ModalVector,
491        operand: &'a LogicExpr<'a>,
492    },
493
494    /// Tense/temporal operator: PAST(φ), FUTURE(φ), ALWAYS(φ), EVENTUALLY(φ), NEXT(φ).
495    Temporal {
496        operator: TemporalOperator,
497        body: &'a LogicExpr<'a>,
498    },
499
500    /// Binary temporal operator: φ UNTIL ψ, φ RELEASE ψ, φ WEAKUNTIL ψ.
501    TemporalBinary {
502        operator: BinaryTemporalOp,
503        left: &'a LogicExpr<'a>,
504        right: &'a LogicExpr<'a>,
505    },
506
507    /// Aspect operator: PROG(φ), PERF(φ), HAB(φ), ITER(φ).
508    Aspectual {
509        operator: AspectOperator,
510        body: &'a LogicExpr<'a>,
511    },
512
513    /// Voice operator: PASSIVE(φ).
514    Voice {
515        operator: VoiceOperator,
516        body: &'a LogicExpr<'a>,
517    },
518
519    /// Binary connective: φ ∧ ψ, φ ∨ ψ, φ → ψ, φ ↔ ψ.
520    BinaryOp {
521        left: &'a LogicExpr<'a>,
522        op: TokenType,
523        right: &'a LogicExpr<'a>,
524    },
525
526    /// Unary operator: ¬φ.
527    UnaryOp {
528        op: TokenType,
529        operand: &'a LogicExpr<'a>,
530    },
531
532    /// Wh-question: λx.φ where x is the questioned variable.
533    Question {
534        wh_variable: Symbol,
535        body: &'a LogicExpr<'a>,
536    },
537
538    /// Yes/no question: ?φ (is φ true?).
539    YesNoQuestion {
540        body: &'a LogicExpr<'a>,
541    },
542
543    /// Atomic symbol (variable or constant in lambda context).
544    Atom(Symbol),
545
546    /// Lambda abstraction: λx.φ.
547    Lambda {
548        variable: Symbol,
549        body: &'a LogicExpr<'a>,
550    },
551
552    /// Function application: (φ)(ψ).
553    App {
554        function: &'a LogicExpr<'a>,
555        argument: &'a LogicExpr<'a>,
556    },
557
558    /// Intensional context: `operator[content]` for opaque verbs (believes, seeks).
559    Intensional {
560        operator: Symbol,
561        content: &'a LogicExpr<'a>,
562    },
563
564    /// Legacy event semantics (Davidson-style with adverb list).
565    Event {
566        predicate: &'a LogicExpr<'a>,
567        adverbs: &'a [Symbol],
568    },
569
570    /// Neo-Davidsonian event with thematic roles (boxed).
571    NeoEvent(Box<NeoEventData<'a>>),
572
573    /// Imperative command: !φ.
574    Imperative {
575        action: &'a LogicExpr<'a>,
576    },
577
578    /// Speech act: performative utterance with illocutionary force.
579    SpeechAct {
580        performer: Symbol,
581        act_type: Symbol,
582        content: &'a LogicExpr<'a>,
583    },
584
585    /// Counterfactual conditional: "If P had been, Q would have been".
586    Counterfactual {
587        antecedent: &'a LogicExpr<'a>,
588        consequent: &'a LogicExpr<'a>,
589    },
590
591    /// Causal relation: "effect because cause".
592    Causal {
593        effect: &'a LogicExpr<'a>,
594        cause: &'a LogicExpr<'a>,
595    },
596
597    /// Comparative: "X is taller than Y (by 2 inches)".
598    Comparative {
599        adjective: Symbol,
600        subject: &'a Term<'a>,
601        object: &'a Term<'a>,
602        difference: Option<&'a Term<'a>>,
603    },
604
605    /// Superlative: "X is the tallest among domain".
606    Superlative {
607        adjective: Symbol,
608        subject: &'a Term<'a>,
609        domain: Symbol,
610    },
611
612    /// Scopal adverb: "only", "always", etc. as operators.
613    Scopal {
614        operator: Symbol,
615        body: &'a LogicExpr<'a>,
616    },
617
618    /// Control verb: "wants to VP", "persuaded X to VP".
619    Control {
620        verb: Symbol,
621        subject: &'a Term<'a>,
622        object: Option<&'a Term<'a>>,
623        infinitive: &'a LogicExpr<'a>,
624    },
625
626    /// Presupposition-assertion structure.
627    Presupposition {
628        assertion: &'a LogicExpr<'a>,
629        presupposition: &'a LogicExpr<'a>,
630    },
631
632    /// Focus particle: "only X", "even X" with alternative set.
633    Focus {
634        kind: crate::token::FocusKind,
635        focused: &'a Term<'a>,
636        scope: &'a LogicExpr<'a>,
637    },
638
639    /// Temporal anchor: "yesterday(φ)", "now(φ)".
640    TemporalAnchor {
641        anchor: Symbol,
642        body: &'a LogicExpr<'a>,
643    },
644
645    /// Distributive operator: *P distributes P over group members.
646    Distributive {
647        predicate: &'a LogicExpr<'a>,
648    },
649
650    /// Group quantifier for collective cardinal readings.
651    /// `∃g(Group(g) ∧ Count(g,n) ∧ ∀x(Member(x,g) → Restriction(x)) ∧ Body(g))`
652    GroupQuantifier {
653        group_var: Symbol,
654        count: u32,
655        member_var: Symbol,
656        restriction: &'a LogicExpr<'a>,
657        body: &'a LogicExpr<'a>,
658    },
659}
660
661impl<'a> LogicExpr<'a> {
662    pub fn lambda(var: Symbol, body: &'a LogicExpr<'a>, arena: &'a Arena<LogicExpr<'a>>) -> &'a LogicExpr<'a> {
663        arena.alloc(LogicExpr::Lambda {
664            variable: var,
665            body,
666        })
667    }
668
669    pub fn app(func: &'a LogicExpr<'a>, arg: &'a LogicExpr<'a>, arena: &'a Arena<LogicExpr<'a>>) -> &'a LogicExpr<'a> {
670        arena.alloc(LogicExpr::App {
671            function: func,
672            argument: arg,
673        })
674    }
675}
676
677#[cfg(test)]
678mod size_tests {
679    use super::*;
680    use std::mem::size_of;
681
682    #[test]
683    fn test_ast_node_sizes() {
684        println!("LogicExpr size: {} bytes", size_of::<LogicExpr>());
685        println!("Term size: {} bytes", size_of::<Term>());
686        println!("NounPhrase size: {} bytes", size_of::<NounPhrase>());
687
688        assert!(
689            size_of::<LogicExpr>() <= 48,
690            "LogicExpr is {} bytes - consider boxing large variants",
691            size_of::<LogicExpr>()
692        );
693        assert!(
694            size_of::<Term>() <= 32,
695            "Term is {} bytes",
696            size_of::<Term>()
697        );
698    }
699}
logicaffeine_language/ast/logic.rs

logicaffeine_language/ast/
logic.rs
