logicaffeine_language/
view.rs

1//! Owned view types for AST serialization and display.
2//!
3//! This module provides "view" versions of AST types that replace interned symbols
4//! with resolved strings. Views are useful for:
5//!
6//! - Serialization (JSON/Serde) without interner dependency
7//! - Pretty-printing and debugging
8//! - UI display where string values are needed
9//!
10//! The conversion functions take an [`Interner`] reference to resolve symbols.
11
12use crate::ast::{
13    AspectOperator, BinaryTemporalOp, LogicExpr, ModalVector, NounPhrase, QuantifierKind,
14    TemporalOperator, VoiceOperator, Term, ThematicRole,
15};
16use logicaffeine_base::Interner;
17use crate::lexicon::Definiteness;
18use crate::token::{FocusKind, TokenType};
19
20/// View of a term with resolved symbol names.
21#[derive(Debug, Clone, PartialEq)]
22pub enum TermView<'a> {
23    Constant(&'a str),
24    Variable(&'a str),
25    Function(&'a str, Vec<TermView<'a>>),
26    Group(Vec<TermView<'a>>),
27    Possessed {
28        possessor: Box<TermView<'a>>,
29        possessed: &'a str,
30    },
31    Sigma(&'a str),
32    Intension(&'a str),
33    Proposition(Box<ExprView<'a>>),
34    Value {
35        kind: NumberKindView<'a>,
36        unit: Option<&'a str>,
37        dimension: Option<crate::ast::Dimension>,
38    },
39}
40
41#[derive(Debug, Clone, PartialEq)]
42pub enum NumberKindView<'a> {
43    Real(f64),
44    Integer(i64),
45    Symbolic(&'a str),
46}
47
48#[derive(Debug, Clone, PartialEq)]
49pub struct NounPhraseView<'a> {
50    pub definiteness: Option<Definiteness>,
51    pub adjectives: Vec<&'a str>,
52    pub noun: &'a str,
53    pub possessor: Option<Box<NounPhraseView<'a>>>,
54    pub pps: Vec<Box<ExprView<'a>>>,
55    pub superlative: Option<&'a str>,
56}
57
58#[derive(Debug, Clone, PartialEq)]
59pub enum ExprView<'a> {
60    Predicate {
61        name: &'a str,
62        args: Vec<TermView<'a>>,
63    },
64    Identity {
65        left: TermView<'a>,
66        right: TermView<'a>,
67    },
68    Metaphor {
69        tenor: TermView<'a>,
70        vehicle: TermView<'a>,
71    },
72    Quantifier {
73        kind: QuantifierKind,
74        variable: &'a str,
75        body: Box<ExprView<'a>>,
76    },
77    Categorical {
78        quantifier: TokenType,
79        subject: NounPhraseView<'a>,
80        copula_negative: bool,
81        predicate: NounPhraseView<'a>,
82    },
83    Relation {
84        subject: NounPhraseView<'a>,
85        verb: &'a str,
86        object: NounPhraseView<'a>,
87    },
88    Modal {
89        vector: ModalVector,
90        operand: Box<ExprView<'a>>,
91    },
92    Temporal {
93        operator: TemporalOperator,
94        body: Box<ExprView<'a>>,
95    },
96    TemporalBinary {
97        operator: BinaryTemporalOp,
98        left: Box<ExprView<'a>>,
99        right: Box<ExprView<'a>>,
100    },
101    Aspectual {
102        operator: AspectOperator,
103        body: Box<ExprView<'a>>,
104    },
105    Voice {
106        operator: VoiceOperator,
107        body: Box<ExprView<'a>>,
108    },
109    BinaryOp {
110        left: Box<ExprView<'a>>,
111        op: TokenType,
112        right: Box<ExprView<'a>>,
113    },
114    UnaryOp {
115        op: TokenType,
116        operand: Box<ExprView<'a>>,
117    },
118    Question {
119        wh_variable: &'a str,
120        body: Box<ExprView<'a>>,
121    },
122    YesNoQuestion {
123        body: Box<ExprView<'a>>,
124    },
125    Atom(&'a str),
126    Lambda {
127        variable: &'a str,
128        body: Box<ExprView<'a>>,
129    },
130    App {
131        function: Box<ExprView<'a>>,
132        argument: Box<ExprView<'a>>,
133    },
134    Intensional {
135        operator: &'a str,
136        content: Box<ExprView<'a>>,
137    },
138    Event {
139        predicate: Box<ExprView<'a>>,
140        adverbs: Vec<&'a str>,
141    },
142    NeoEvent {
143        event_var: &'a str,
144        verb: &'a str,
145        roles: Vec<(ThematicRole, TermView<'a>)>,
146        modifiers: Vec<&'a str>,
147    },
148    Imperative {
149        action: Box<ExprView<'a>>,
150    },
151    SpeechAct {
152        performer: &'a str,
153        act_type: &'a str,
154        content: Box<ExprView<'a>>,
155    },
156    Counterfactual {
157        antecedent: Box<ExprView<'a>>,
158        consequent: Box<ExprView<'a>>,
159    },
160    Causal {
161        effect: Box<ExprView<'a>>,
162        cause: Box<ExprView<'a>>,
163    },
164    Comparative {
165        adjective: &'a str,
166        subject: TermView<'a>,
167        object: TermView<'a>,
168        difference: Option<Box<TermView<'a>>>,
169    },
170    Superlative {
171        adjective: &'a str,
172        subject: TermView<'a>,
173        domain: &'a str,
174    },
175    Scopal {
176        operator: &'a str,
177        body: Box<ExprView<'a>>,
178    },
179    Control {
180        verb: &'a str,
181        subject: TermView<'a>,
182        object: Option<TermView<'a>>,
183        infinitive: Box<ExprView<'a>>,
184    },
185    Presupposition {
186        assertion: Box<ExprView<'a>>,
187        presupposition: Box<ExprView<'a>>,
188    },
189    Focus {
190        kind: FocusKind,
191        focused: TermView<'a>,
192        scope: Box<ExprView<'a>>,
193    },
194    TemporalAnchor {
195        anchor: &'a str,
196        body: Box<ExprView<'a>>,
197    },
198    Distributive {
199        predicate: Box<ExprView<'a>>,
200    },
201    GroupQuantifier {
202        group_var: &'a str,
203        count: u32,
204        member_var: &'a str,
205        restriction: Box<ExprView<'a>>,
206        body: Box<ExprView<'a>>,
207    },
208}
209
210pub trait Resolve<'a> {
211    type Output;
212    fn resolve(&self, interner: &'a Interner) -> Self::Output;
213}
214
215impl<'a, 'b> Resolve<'a> for Term<'b> {
216    type Output = TermView<'a>;
217
218    fn resolve(&self, interner: &'a Interner) -> TermView<'a> {
219        match self {
220            Term::Constant(s) => TermView::Constant(interner.resolve(*s)),
221            Term::Variable(s) => TermView::Variable(interner.resolve(*s)),
222            Term::Function(name, args) => TermView::Function(
223                interner.resolve(*name),
224                args.iter().map(|a| a.resolve(interner)).collect(),
225            ),
226            Term::Group(members) => {
227                TermView::Group(members.iter().map(|m| m.resolve(interner)).collect())
228            }
229            Term::Possessed {
230                possessor,
231                possessed,
232            } => TermView::Possessed {
233                possessor: Box::new(possessor.resolve(interner)),
234                possessed: interner.resolve(*possessed),
235            },
236            Term::Sigma(predicate) => TermView::Sigma(interner.resolve(*predicate)),
237            Term::Intension(predicate) => TermView::Intension(interner.resolve(*predicate)),
238            Term::Proposition(expr) => {
239                TermView::Proposition(Box::new(expr.resolve(interner)))
240            }
241            Term::Value { kind, unit, dimension } => {
242                use crate::ast::NumberKind;
243                let kind_view = match kind {
244                    NumberKind::Real(r) => NumberKindView::Real(*r),
245                    NumberKind::Integer(i) => NumberKindView::Integer(*i),
246                    NumberKind::Symbolic(s) => NumberKindView::Symbolic(interner.resolve(*s)),
247                };
248                TermView::Value {
249                    kind: kind_view,
250                    unit: unit.map(|u| interner.resolve(u)),
251                    dimension: *dimension,
252                }
253            }
254        }
255    }
256}
257
258impl<'a, 'b> Resolve<'a> for NounPhrase<'b> {
259    type Output = NounPhraseView<'a>;
260
261    fn resolve(&self, interner: &'a Interner) -> NounPhraseView<'a> {
262        NounPhraseView {
263            definiteness: self.definiteness,
264            adjectives: self.adjectives.iter().map(|s| interner.resolve(*s)).collect(),
265            noun: interner.resolve(self.noun),
266            possessor: self.possessor.map(|p| Box::new(p.resolve(interner))),
267            pps: self.pps.iter().map(|pp| Box::new(pp.resolve(interner))).collect(),
268            superlative: self.superlative.map(|s| interner.resolve(s)),
269        }
270    }
271}
272
273impl<'a, 'b> Resolve<'a> for LogicExpr<'b> {
274    type Output = ExprView<'a>;
275
276    fn resolve(&self, interner: &'a Interner) -> ExprView<'a> {
277        match self {
278            LogicExpr::Predicate { name, args, .. } => ExprView::Predicate {
279                name: interner.resolve(*name),
280                args: args.iter().map(|a| a.resolve(interner)).collect(),
281            },
282            LogicExpr::Identity { left, right } => ExprView::Identity {
283                left: left.resolve(interner),
284                right: right.resolve(interner),
285            },
286            LogicExpr::Metaphor { tenor, vehicle } => ExprView::Metaphor {
287                tenor: tenor.resolve(interner),
288                vehicle: vehicle.resolve(interner),
289            },
290            LogicExpr::Quantifier { kind, variable, body, .. } => ExprView::Quantifier {
291                kind: *kind,
292                variable: interner.resolve(*variable),
293                body: Box::new(body.resolve(interner)),
294            },
295            LogicExpr::Categorical(data) => ExprView::Categorical {
296                quantifier: data.quantifier.clone(),
297                subject: data.subject.resolve(interner),
298                copula_negative: data.copula_negative,
299                predicate: data.predicate.resolve(interner),
300            },
301            LogicExpr::Relation(data) => ExprView::Relation {
302                subject: data.subject.resolve(interner),
303                verb: interner.resolve(data.verb),
304                object: data.object.resolve(interner),
305            },
306            LogicExpr::Modal { vector, operand } => ExprView::Modal {
307                vector: *vector,
308                operand: Box::new(operand.resolve(interner)),
309            },
310            LogicExpr::Temporal { operator, body } => ExprView::Temporal {
311                operator: *operator,
312                body: Box::new(body.resolve(interner)),
313            },
314            LogicExpr::TemporalBinary { operator, left, right } => ExprView::TemporalBinary {
315                operator: *operator,
316                left: Box::new(left.resolve(interner)),
317                right: Box::new(right.resolve(interner)),
318            },
319            LogicExpr::Aspectual { operator, body } => ExprView::Aspectual {
320                operator: *operator,
321                body: Box::new(body.resolve(interner)),
322            },
323            LogicExpr::Voice { operator, body } => ExprView::Voice {
324                operator: *operator,
325                body: Box::new(body.resolve(interner)),
326            },
327            LogicExpr::BinaryOp { left, op, right } => ExprView::BinaryOp {
328                left: Box::new(left.resolve(interner)),
329                op: op.clone(),
330                right: Box::new(right.resolve(interner)),
331            },
332            LogicExpr::UnaryOp { op, operand } => ExprView::UnaryOp {
333                op: op.clone(),
334                operand: Box::new(operand.resolve(interner)),
335            },
336            LogicExpr::Question { wh_variable, body } => ExprView::Question {
337                wh_variable: interner.resolve(*wh_variable),
338                body: Box::new(body.resolve(interner)),
339            },
340            LogicExpr::YesNoQuestion { body } => ExprView::YesNoQuestion {
341                body: Box::new(body.resolve(interner)),
342            },
343            LogicExpr::Atom(s) => ExprView::Atom(interner.resolve(*s)),
344            LogicExpr::Lambda { variable, body } => ExprView::Lambda {
345                variable: interner.resolve(*variable),
346                body: Box::new(body.resolve(interner)),
347            },
348            LogicExpr::App { function, argument } => ExprView::App {
349                function: Box::new(function.resolve(interner)),
350                argument: Box::new(argument.resolve(interner)),
351            },
352            LogicExpr::Intensional { operator, content } => ExprView::Intensional {
353                operator: interner.resolve(*operator),
354                content: Box::new(content.resolve(interner)),
355            },
356            LogicExpr::Event { predicate, adverbs } => ExprView::Event {
357                predicate: Box::new(predicate.resolve(interner)),
358                adverbs: adverbs.iter().map(|s| interner.resolve(*s)).collect(),
359            },
360            LogicExpr::NeoEvent(data) => ExprView::NeoEvent {
361                event_var: interner.resolve(data.event_var),
362                verb: interner.resolve(data.verb),
363                roles: data.roles.iter().map(|(role, term)| (*role, term.resolve(interner))).collect(),
364                modifiers: data.modifiers.iter().map(|s| interner.resolve(*s)).collect(),
365            },
366            LogicExpr::Imperative { action } => ExprView::Imperative {
367                action: Box::new(action.resolve(interner)),
368            },
369            LogicExpr::SpeechAct {
370                performer,
371                act_type,
372                content,
373            } => ExprView::SpeechAct {
374                performer: interner.resolve(*performer),
375                act_type: interner.resolve(*act_type),
376                content: Box::new(content.resolve(interner)),
377            },
378            LogicExpr::Counterfactual { antecedent, consequent } => ExprView::Counterfactual {
379                antecedent: Box::new(antecedent.resolve(interner)),
380                consequent: Box::new(consequent.resolve(interner)),
381            },
382            LogicExpr::Causal { effect, cause } => ExprView::Causal {
383                effect: Box::new(effect.resolve(interner)),
384                cause: Box::new(cause.resolve(interner)),
385            },
386            LogicExpr::Comparative { adjective, subject, object, difference } => ExprView::Comparative {
387                adjective: interner.resolve(*adjective),
388                subject: subject.resolve(interner),
389                object: object.resolve(interner),
390                difference: difference.map(|d| Box::new(d.resolve(interner))),
391            },
392            LogicExpr::Superlative { adjective, subject, domain } => ExprView::Superlative {
393                adjective: interner.resolve(*adjective),
394                subject: subject.resolve(interner),
395                domain: interner.resolve(*domain),
396            },
397            LogicExpr::Scopal { operator, body } => ExprView::Scopal {
398                operator: interner.resolve(*operator),
399                body: Box::new(body.resolve(interner)),
400            },
401            LogicExpr::Control {
402                verb,
403                subject,
404                object,
405                infinitive,
406            } => ExprView::Control {
407                verb: interner.resolve(*verb),
408                subject: subject.resolve(interner),
409                object: object.map(|o| o.resolve(interner)),
410                infinitive: Box::new(infinitive.resolve(interner)),
411            },
412            LogicExpr::Presupposition { assertion, presupposition } => ExprView::Presupposition {
413                assertion: Box::new(assertion.resolve(interner)),
414                presupposition: Box::new(presupposition.resolve(interner)),
415            },
416            LogicExpr::Focus { kind, focused, scope } => ExprView::Focus {
417                kind: *kind,
418                focused: focused.resolve(interner),
419                scope: Box::new(scope.resolve(interner)),
420            },
421            LogicExpr::TemporalAnchor { anchor, body } => ExprView::TemporalAnchor {
422                anchor: interner.resolve(*anchor),
423                body: Box::new(body.resolve(interner)),
424            },
425            LogicExpr::Distributive { predicate } => ExprView::Distributive {
426                predicate: Box::new(predicate.resolve(interner)),
427            },
428            LogicExpr::GroupQuantifier { group_var, count, member_var, restriction, body } => ExprView::GroupQuantifier {
429                group_var: interner.resolve(*group_var),
430                count: *count,
431                member_var: interner.resolve(*member_var),
432                restriction: Box::new(restriction.resolve(interner)),
433                body: Box::new(body.resolve(interner)),
434            },
435        }
436    }
437}
438
439#[cfg(test)]
440mod term_view_tests {
441    use super::*;
442    use logicaffeine_base::Arena;
443
444    #[test]
445    fn resolve_term_constant() {
446        let mut interner = Interner::new();
447        let sym = interner.intern("Socrates");
448        let term = Term::Constant(sym);
449        assert_eq!(term.resolve(&interner), TermView::Constant("Socrates"));
450    }
451
452    #[test]
453    fn resolve_term_variable() {
454        let mut interner = Interner::new();
455        let x = interner.intern("x");
456        let term = Term::Variable(x);
457        assert_eq!(term.resolve(&interner), TermView::Variable("x"));
458    }
459
460    #[test]
461    fn resolve_term_function() {
462        let mut interner = Interner::new();
463        let term_arena: Arena<Term> = Arena::new();
464        let father = interner.intern("father");
465        let john = interner.intern("John");
466        let term = Term::Function(father, term_arena.alloc_slice([Term::Constant(john)]));
467
468        assert_eq!(
469            term.resolve(&interner),
470            TermView::Function("father", vec![TermView::Constant("John")])
471        );
472    }
473
474    #[test]
475    fn resolve_term_group() {
476        let mut interner = Interner::new();
477        let term_arena: Arena<Term> = Arena::new();
478        let j = interner.intern("John");
479        let m = interner.intern("Mary");
480        let term = Term::Group(term_arena.alloc_slice([Term::Constant(j), Term::Constant(m)]));
481
482        assert_eq!(
483            term.resolve(&interner),
484            TermView::Group(vec![
485                TermView::Constant("John"),
486                TermView::Constant("Mary")
487            ])
488        );
489    }
490
491    #[test]
492    fn resolve_term_possessed() {
493        let mut interner = Interner::new();
494        let term_arena: Arena<Term> = Arena::new();
495        let john = interner.intern("John");
496        let dog = interner.intern("dog");
497        let term = Term::Possessed {
498            possessor: term_arena.alloc(Term::Constant(john)),
499            possessed: dog,
500        };
501
502        assert_eq!(
503            term.resolve(&interner),
504            TermView::Possessed {
505                possessor: Box::new(TermView::Constant("John")),
506                possessed: "dog",
507            }
508        );
509    }
510
511    #[test]
512    fn term_view_equality_is_bit_exact() {
513        let a = TermView::Constant("test");
514        let b = TermView::Constant("test");
515        let c = TermView::Constant("Test");
516        assert_eq!(a, b);
517        assert_ne!(a, c);
518    }
519
520    #[test]
521    fn nested_function_resolve() {
522        let mut interner = Interner::new();
523        let term_arena: Arena<Term> = Arena::new();
524        let f = interner.intern("f");
525        let g = interner.intern("g");
526        let x = interner.intern("x");
527
528        let inner = Term::Function(g, term_arena.alloc_slice([Term::Variable(x)]));
529        let outer = Term::Function(f, term_arena.alloc_slice([inner]));
530
531        assert_eq!(
532            outer.resolve(&interner),
533            TermView::Function(
534                "f",
535                vec![TermView::Function("g", vec![TermView::Variable("x")])]
536            )
537        );
538    }
539}
540
541#[cfg(test)]
542mod expr_view_tests {
543    use super::*;
544    use logicaffeine_base::Arena;
545    use crate::ast::ModalDomain;
546
547    #[test]
548    fn resolve_expr_predicate() {
549        let mut interner = Interner::new();
550        let term_arena: Arena<Term> = Arena::new();
551        let mortal = interner.intern("Mortal");
552        let x = interner.intern("x");
553        let expr = LogicExpr::Predicate {
554            name: mortal,
555            args: term_arena.alloc_slice([Term::Variable(x)]),
556            world: None,
557        };
558
559        assert_eq!(
560            expr.resolve(&interner),
561            ExprView::Predicate {
562                name: "Mortal",
563                args: vec![TermView::Variable("x")],
564            }
565        );
566    }
567
568    #[test]
569    fn resolve_expr_identity() {
570        let mut interner = Interner::new();
571        let term_arena: Arena<Term> = Arena::new();
572        let clark = interner.intern("Clark");
573        let superman = interner.intern("Superman");
574        let expr = LogicExpr::Identity {
575            left: term_arena.alloc(Term::Constant(clark)),
576            right: term_arena.alloc(Term::Constant(superman)),
577        };
578
579        assert_eq!(
580            expr.resolve(&interner),
581            ExprView::Identity {
582                left: TermView::Constant("Clark"),
583                right: TermView::Constant("Superman"),
584            }
585        );
586    }
587
588    #[test]
589    fn resolve_expr_quantifier() {
590        let mut interner = Interner::new();
591        let expr_arena: Arena<LogicExpr> = Arena::new();
592        let term_arena: Arena<Term> = Arena::new();
593        let x = interner.intern("x");
594        let mortal = interner.intern("Mortal");
595
596        let body = expr_arena.alloc(LogicExpr::Predicate {
597            name: mortal,
598            args: term_arena.alloc_slice([Term::Variable(x)]),
599            world: None,
600        });
601        let expr = LogicExpr::Quantifier {
602            kind: QuantifierKind::Universal,
603            variable: x,
604            body,
605            island_id: 0,
606        };
607
608        assert_eq!(
609            expr.resolve(&interner),
610            ExprView::Quantifier {
611                kind: QuantifierKind::Universal,
612                variable: "x",
613                body: Box::new(ExprView::Predicate {
614                    name: "Mortal",
615                    args: vec![TermView::Variable("x")],
616                }),
617            }
618        );
619    }
620
621    #[test]
622    fn resolve_expr_atom() {
623        let mut interner = Interner::new();
624        let p = interner.intern("P");
625        let expr = LogicExpr::Atom(p);
626
627        assert_eq!(expr.resolve(&interner), ExprView::Atom("P"));
628    }
629
630    #[test]
631    fn resolve_expr_binary_op() {
632        let mut interner = Interner::new();
633        let expr_arena: Arena<LogicExpr> = Arena::new();
634        let p = interner.intern("P");
635        let q = interner.intern("Q");
636        let expr = LogicExpr::BinaryOp {
637            left: expr_arena.alloc(LogicExpr::Atom(p)),
638            op: TokenType::And,
639            right: expr_arena.alloc(LogicExpr::Atom(q)),
640        };
641
642        assert_eq!(
643            expr.resolve(&interner),
644            ExprView::BinaryOp {
645                left: Box::new(ExprView::Atom("P")),
646                op: TokenType::And,
647                right: Box::new(ExprView::Atom("Q")),
648            }
649        );
650    }
651
652    #[test]
653    fn resolve_expr_lambda() {
654        let mut interner = Interner::new();
655        let expr_arena: Arena<LogicExpr> = Arena::new();
656        let x = interner.intern("x");
657        let p = interner.intern("P");
658        let expr = LogicExpr::Lambda {
659            variable: x,
660            body: expr_arena.alloc(LogicExpr::Atom(p)),
661        };
662
663        assert_eq!(
664            expr.resolve(&interner),
665            ExprView::Lambda {
666                variable: "x",
667                body: Box::new(ExprView::Atom("P")),
668            }
669        );
670    }
671
672    #[test]
673    fn resolve_expr_temporal() {
674        let mut interner = Interner::new();
675        let expr_arena: Arena<LogicExpr> = Arena::new();
676        let run = interner.intern("Run");
677        let expr = LogicExpr::Temporal {
678            operator: TemporalOperator::Past,
679            body: expr_arena.alloc(LogicExpr::Atom(run)),
680        };
681
682        assert_eq!(
683            expr.resolve(&interner),
684            ExprView::Temporal {
685                operator: TemporalOperator::Past,
686                body: Box::new(ExprView::Atom("Run")),
687            }
688        );
689    }
690
691    #[test]
692    fn resolve_expr_modal() {
693        use crate::ast::ModalFlavor;
694        let mut interner = Interner::new();
695        let expr_arena: Arena<LogicExpr> = Arena::new();
696        let rain = interner.intern("Rain");
697        let expr = LogicExpr::Modal {
698            vector: ModalVector {
699                domain: ModalDomain::Alethic,
700                force: 1.0,
701                flavor: ModalFlavor::Root,
702            },
703            operand: expr_arena.alloc(LogicExpr::Atom(rain)),
704        };
705
706        assert_eq!(
707            expr.resolve(&interner),
708            ExprView::Modal {
709                vector: ModalVector {
710                    domain: ModalDomain::Alethic,
711                    force: 1.0,
712                    flavor: ModalFlavor::Root,
713                },
714                operand: Box::new(ExprView::Atom("Rain")),
715            }
716        );
717    }
718
719    #[test]
720    fn modal_vector_equality_is_bit_exact() {
721        use crate::ast::ModalFlavor;
722        let v1 = ModalVector {
723            domain: ModalDomain::Alethic,
724            force: 0.5,
725            flavor: ModalFlavor::Root,
726        };
727        let v2 = ModalVector {
728            domain: ModalDomain::Alethic,
729            force: 0.5,
730            flavor: ModalFlavor::Root,
731        };
732        let v3 = ModalVector {
733            domain: ModalDomain::Alethic,
734            force: 0.51,
735            flavor: ModalFlavor::Root,
736        };
737
738        assert_eq!(v1, v2);
739        assert_ne!(v1, v3);
740    }
741
742    #[test]
743    fn resolve_expr_unary_op() {
744        let mut interner = Interner::new();
745        let expr_arena: Arena<LogicExpr> = Arena::new();
746        let p = interner.intern("P");
747        let expr = LogicExpr::UnaryOp {
748            op: TokenType::Not,
749            operand: expr_arena.alloc(LogicExpr::Atom(p)),
750        };
751
752        assert_eq!(
753            expr.resolve(&interner),
754            ExprView::UnaryOp {
755                op: TokenType::Not,
756                operand: Box::new(ExprView::Atom("P")),
757            }
758        );
759    }
760
761    #[test]
762    fn resolve_expr_app() {
763        let mut interner = Interner::new();
764        let expr_arena: Arena<LogicExpr> = Arena::new();
765        let f = interner.intern("f");
766        let x = interner.intern("x");
767        let expr = LogicExpr::App {
768            function: expr_arena.alloc(LogicExpr::Atom(f)),
769            argument: expr_arena.alloc(LogicExpr::Atom(x)),
770        };
771
772        assert_eq!(
773            expr.resolve(&interner),
774            ExprView::App {
775                function: Box::new(ExprView::Atom("f")),
776                argument: Box::new(ExprView::Atom("x")),
777            }
778        );
779    }
780
781    #[test]
782    fn expr_view_equality_complex() {
783        let a = ExprView::Quantifier {
784            kind: QuantifierKind::Universal,
785            variable: "x",
786            body: Box::new(ExprView::Predicate {
787                name: "P",
788                args: vec![TermView::Variable("x")],
789            }),
790        };
791        let b = ExprView::Quantifier {
792            kind: QuantifierKind::Universal,
793            variable: "x",
794            body: Box::new(ExprView::Predicate {
795                name: "P",
796                args: vec![TermView::Variable("x")],
797            }),
798        };
799        assert_eq!(a, b);
800    }
801}
logicaffeine_language/view.rs

logicaffeine_language/
view.rs
