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

logicaffeine_language/
view.rs
