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

logicaffeine_language/
view.rs
