tptp/
tfx.rs

1use alloc::boxed::Box;
2use alloc::vec::Vec;
3use derive_more::Display;
4use nom::branch::alt;
5use nom::bytes::streaming::tag;
6use nom::combinator::{map, opt};
7use nom::multi::separated_list1;
8use nom::sequence::{delimited, pair, preceded, tuple};
9#[cfg(feature = "serde")]
10use serde::Serialize;
11
12use crate::common;
13use crate::common::*;
14use crate::fof;
15use crate::utils::{fold_many0_once, GarbageFirstVec, Separated};
16use crate::{Error, Parse, Result};
17
18/// [`tff_type_arguments`](http://tptp.org/TPTP/SyntaxBNF.html#tff_type_arguments)
19#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
20#[display(fmt = "{}", "Separated(',', _0)")]
21#[cfg_attr(feature = "serde", derive(Serialize))]
22pub struct TypeArguments<'a>(pub Vec<AtomicType<'a>>);
23
24impl<'a, E: Error<'a>> Parse<'a, E> for TypeArguments<'a> {
25    fn parse(x: &'a [u8]) -> Result<Self, E> {
26        map(
27            separated_list1(
28                delimited(ignored, tag(","), ignored),
29                AtomicType::parse,
30            ),
31            Self,
32        )(x)
33    }
34}
35
36/// [`tff_atomic_type`](http://tptp.org/TPTP/SyntaxBNF.html#tff_atomic_type)
37#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
38#[cfg_attr(feature = "serde", derive(Serialize))]
39pub enum AtomicType<'a> {
40    Constant(TypeConstant<'a>),
41    Defined(DefinedType<'a>),
42    Variable(common::Variable<'a>),
43    #[display(fmt = "{}({})", _0, _1)]
44    Function(TypeFunctor<'a>, Box<TypeArguments<'a>>),
45}
46
47impl<'a, E: Error<'a>> Parse<'a, E> for AtomicType<'a> {
48    fn parse(x: &'a [u8]) -> Result<Self, E> {
49        alt((
50            map(DefinedType::parse, Self::Defined),
51            map(common::Variable::parse, Self::Variable),
52            map(
53                pair(TypeFunctor::parse, opt(preceded(ignored, parens))),
54                |(f, args)| match args {
55                    Some(args) => Self::Function(f, Box::new(args)),
56                    None => Self::Constant(TypeConstant(f)),
57                },
58            ),
59        ))(x)
60    }
61}
62
63struct TypedVariableTail<'a>(AtomicType<'a>);
64
65impl<'a> TypedVariableTail<'a> {
66    fn finish(self, variable: common::Variable<'a>) -> TypedVariable<'a> {
67        let Self(typ) = self;
68        TypedVariable { variable, typ }
69    }
70}
71
72impl<'a, E: Error<'a>> Parse<'a, E> for TypedVariableTail<'a> {
73    fn parse(x: &'a [u8]) -> Result<Self, E> {
74        preceded(
75            delimited(ignored, tag(":"), ignored),
76            map(AtomicType::parse, Self),
77        )(x)
78    }
79}
80
81/// [`tff_typed_variable`](http://tptp.org/TPTP/SyntaxBNF.html#tff_typed_variable)
82#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
83#[display(fmt = "{}:{}", variable, typ)]
84#[cfg_attr(feature = "serde", derive(Serialize))]
85pub struct TypedVariable<'a> {
86    pub variable: common::Variable<'a>,
87    pub typ: AtomicType<'a>,
88}
89
90impl<'a, E: Error<'a>> Parse<'a, E> for TypedVariable<'a> {
91    fn parse(x: &'a [u8]) -> Result<Self, E> {
92        map(
93            pair(common::Variable::parse, TypedVariableTail::parse),
94            |(variable, tail)| tail.finish(variable),
95        )(x)
96    }
97}
98
99/// [`tff_variable`](http://tptp.org/TPTP/SyntaxBNF.html#tff_variable)
100#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
101#[cfg_attr(feature = "serde", derive(Serialize))]
102pub enum Variable<'a> {
103    Typed(TypedVariable<'a>),
104    Untyped(common::Variable<'a>),
105}
106
107impl<'a, E: Error<'a>> Parse<'a, E> for Variable<'a> {
108    fn parse(x: &'a [u8]) -> Result<Self, E> {
109        map(
110            pair(common::Variable::parse, opt(TypedVariableTail::parse)),
111            |(var, tail)| match tail {
112                Some(tail) => Self::Typed(tail.finish(var)),
113                None => Self::Untyped(var),
114            },
115        )(x)
116    }
117}
118
119/// [`tff_variable_list`](http://tptp.org/TPTP/SyntaxBNF.html#tff_variable_list)
120#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
121#[display(fmt = "{}", "Separated(',', _0)")]
122#[cfg_attr(feature = "serde", derive(Serialize))]
123pub struct VariableList<'a>(pub Vec<Variable<'a>>);
124
125impl<'a, E: Error<'a>> Parse<'a, E> for VariableList<'a> {
126    fn parse(x: &'a [u8]) -> Result<Self, E> {
127        map(
128            separated_list1(
129                delimited(ignored, tag(","), ignored),
130                Variable::parse,
131            ),
132            Self,
133        )(x)
134    }
135}
136
137/// [`tff_unitary_type`](http://tptp.org/TPTP/SyntaxBNF.html#tff_unitary_type)
138#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
139#[cfg_attr(feature = "serde", derive(Serialize))]
140pub enum UnitaryType<'a> {
141    Atomic(AtomicType<'a>),
142    #[display(fmt = "({})", _0)]
143    Product(XprodType<'a>),
144}
145
146impl<'a, E: Error<'a>> Parse<'a, E> for UnitaryType<'a> {
147    fn parse(x: &'a [u8]) -> Result<Self, E> {
148        alt((
149            map(AtomicType::parse, Self::Atomic),
150            map(parens, Self::Product),
151        ))(x)
152    }
153}
154
155/// [`tff_xprod_type`](http://tptp.org/TPTP/SyntaxBNF.html#tff_xprod_type)
156#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
157#[display(fmt = "{}", "Separated('*', _0)")]
158#[cfg_attr(feature = "serde", derive(Serialize))]
159pub struct XprodType<'a>(pub Vec<UnitaryType<'a>>);
160
161impl<'a, E: Error<'a>> Parse<'a, E> for XprodType<'a> {
162    fn parse(x: &'a [u8]) -> Result<Self, E> {
163        map(
164            separated_list1(
165                delimited(ignored, tag("*"), ignored),
166                UnitaryType::parse,
167            ),
168            Self,
169        )(x)
170    }
171}
172
173/// [`tff_mapping_type`](http://tptp.org/TPTP/SyntaxBNF.html#tff_mapping_type)
174#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
175#[display(fmt = "{}>{}", domain, range)]
176#[cfg_attr(feature = "serde", derive(Serialize))]
177pub struct MappingType<'a> {
178    pub domain: Box<UnitaryType<'a>>,
179    pub range: AtomicType<'a>,
180}
181
182impl<'a, E: Error<'a>> Parse<'a, E> for MappingType<'a> {
183    fn parse(x: &'a [u8]) -> Result<Self, E> {
184        map(
185            pair(
186                UnitaryType::parse,
187                preceded(
188                    delimited(ignored, tag(">"), ignored),
189                    AtomicType::parse,
190                ),
191            ),
192            |(domain, range)| Self {
193                domain: Box::new(domain),
194                range,
195            },
196        )(x)
197    }
198}
199
200/// [`tf1_quantified_type`](http://tptp.org/TPTP/SyntaxBNF.html#tf1_quantified_type)
201#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
202#[display(fmt = "!>[{}]:{}", bound, typ)]
203#[cfg_attr(feature = "serde", derive(Serialize))]
204pub struct QuantifiedType<'a> {
205    pub bound: VariableList<'a>,
206    pub typ: Box<Monotype<'a>>,
207}
208
209impl<'a, E: Error<'a>> Parse<'a, E> for QuantifiedType<'a> {
210    fn parse(x: &'a [u8]) -> Result<Self, E> {
211        preceded(
212            tag("!>"),
213            preceded(
214                ignored,
215                map(
216                    pair(
217                        delimited(
218                            tag("["),
219                            delimited(ignored, VariableList::parse, ignored),
220                            tag("]"),
221                        ),
222                        preceded(
223                            delimited(ignored, tag(":"), ignored),
224                            Monotype::parse,
225                        ),
226                    ),
227                    |(bound, typ)| Self {
228                        bound,
229                        typ: Box::new(typ),
230                    },
231                ),
232            ),
233        )(x)
234    }
235}
236
237/// [`tff_monotype`](http://tptp.org/TPTP/SyntaxBNF.html#tff_monotype)
238#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
239#[cfg_attr(feature = "serde", derive(Serialize))]
240pub enum Monotype<'a> {
241    Atomic(AtomicType<'a>),
242    #[display(fmt = "({})", _0)]
243    Mapping(MappingType<'a>),
244    Quantified(QuantifiedType<'a>),
245}
246
247impl<'a, E: Error<'a>> Parse<'a, E> for Monotype<'a> {
248    fn parse(x: &'a [u8]) -> Result<Self, E> {
249        alt((
250            map(AtomicType::parse, Self::Atomic),
251            map(parens, Self::Mapping),
252            map(QuantifiedType::parse, Self::Quantified),
253        ))(x)
254    }
255}
256
257/// [`tff_non_atomic_type`](http://tptp.org/TPTP/SyntaxBNF.html#tff_non_atomic_type)
258#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
259#[cfg_attr(feature = "serde", derive(Serialize))]
260pub enum NonAtomicType<'a> {
261    Mapping(MappingType<'a>),
262    Quantified(QuantifiedType<'a>),
263    #[display(fmt = "({})", _0)]
264    Parenthesised(Box<NonAtomicType<'a>>),
265}
266
267impl<'a, E: Error<'a>> Parse<'a, E> for NonAtomicType<'a> {
268    fn parse(x: &'a [u8]) -> Result<Self, E> {
269        alt((
270            map(MappingType::parse, Self::Mapping),
271            map(QuantifiedType::parse, Self::Quantified),
272            map(map(parens, Box::new), Self::Parenthesised),
273        ))(x)
274    }
275}
276
277/// [`tff_top_level_type`](http://tptp.org/TPTP/SyntaxBNF.html#tff_top_level_type)
278#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
279#[cfg_attr(feature = "serde", derive(Serialize))]
280pub enum TopLevelType<'a> {
281    Atomic(Box<AtomicType<'a>>),
282    NonAtomic(Box<NonAtomicType<'a>>),
283}
284
285impl<'a, E: Error<'a>> Parse<'a, E> for TopLevelType<'a> {
286    fn parse(x: &'a [u8]) -> Result<Self, E> {
287        alt((
288            map(map(NonAtomicType::parse, Box::new), Self::NonAtomic),
289            map(map(AtomicType::parse, Box::new), Self::Atomic),
290        ))(x)
291    }
292}
293
294/// [`tff_atom_typing`](http://tptp.org/TPTP/SyntaxBNF.html#tff_atom_typing)
295#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
296#[cfg_attr(feature = "serde", derive(Serialize))]
297pub enum AtomTyping<'a> {
298    #[display(fmt = "{}:{}", _0, _1)]
299    Typing(UntypedAtom<'a>, TopLevelType<'a>),
300    #[display(fmt = "({})", _0)]
301    Parenthesised(Box<AtomTyping<'a>>),
302}
303
304impl<'a, E: Error<'a>> Parse<'a, E> for AtomTyping<'a> {
305    fn parse(x: &'a [u8]) -> Result<Self, E> {
306        alt((
307            map(
308                pair(
309                    UntypedAtom::parse,
310                    preceded(
311                        delimited(ignored, tag(":"), ignored),
312                        TopLevelType::parse,
313                    ),
314                ),
315                |(atom, typ)| Self::Typing(atom, typ),
316            ),
317            map(parens, |typing| Self::Parenthesised(Box::new(typing))),
318        ))(x)
319    }
320}
321
322/// [`tff_term`](http://tptp.org/TPTP/SyntaxBNF.html#tff_term)
323#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
324#[cfg_attr(feature = "serde", derive(Serialize))]
325pub enum Term<'a> {
326    Logic(Box<LogicFormula<'a>>),
327    Defined(DefinedTerm<'a>),
328}
329
330impl<'a, E: Error<'a>> Parse<'a, E> for Term<'a> {
331    fn parse(x: &'a [u8]) -> Result<Self, E> {
332        alt((
333            map(map(LogicFormula::parse, Box::new), Self::Logic),
334            map(DefinedTerm::parse, Self::Defined),
335        ))(x)
336    }
337}
338
339/// [`tff_unitary_term`](http://tptp.org/TPTP/SyntaxBNF.html#tff_unitary_term)
340#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
341#[cfg_attr(feature = "serde", derive(Serialize))]
342pub enum UnitaryTerm<'a> {
343    Atomic(AtomicFormula<'a>),
344    Defined(DefinedTerm<'a>),
345    Variable(common::Variable<'a>),
346    #[display(fmt = "({})", _0)]
347    Logic(Box<LogicFormula<'a>>),
348}
349
350impl<'a, E: Error<'a>> Parse<'a, E> for UnitaryTerm<'a> {
351    fn parse(x: &'a [u8]) -> Result<Self, E> {
352        alt((
353            map(AtomicFormula::parse, Self::Atomic),
354            map(DefinedTerm::parse, Self::Defined),
355            map(common::Variable::parse, Self::Variable),
356            map(map(parens, Box::new), Self::Logic),
357        ))(x)
358    }
359}
360
361/// [`tff_arguments`](http://tptp.org/TPTP/SyntaxBNF.html#tff-arguments)
362#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
363#[display(fmt = "{}", "Separated(',', _0)")]
364#[cfg_attr(feature = "serde", derive(Serialize))]
365pub struct Arguments<'a>(pub Vec<Term<'a>>);
366
367impl<'a, E: Error<'a>> Parse<'a, E> for Arguments<'a> {
368    fn parse(x: &'a [u8]) -> Result<Self, E> {
369        map(
370            separated_list1(
371                delimited(ignored, tag(","), ignored),
372                Term::parse,
373            ),
374            Self,
375        )(x)
376    }
377}
378
379/// [`tff_system_atomic`](http://tptp.org/TPTP/SyntaxBNF.html#tff_system_atomic)
380#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
381#[cfg_attr(feature = "serde", derive(Serialize))]
382pub enum SystemAtomic<'a> {
383    Constant(SystemConstant<'a>),
384    #[display(fmt = "{}({})", _0, _1)]
385    Function(SystemFunctor<'a>, Box<Arguments<'a>>),
386}
387
388impl<'a, E: Error<'a>> Parse<'a, E> for SystemAtomic<'a> {
389    fn parse(x: &'a [u8]) -> Result<Self, E> {
390        map(
391            pair(SystemFunctor::parse, opt(preceded(ignored, parens))),
392            |(f, args)| match args {
393                None => Self::Constant(SystemConstant(f)),
394                Some(args) => Self::Function(f, Box::new(args)),
395            },
396        )(x)
397    }
398}
399
400/// [`tff_plain_atomic`](http://tptp.org/TPTP/SyntaxBNF.html#tff_plain_atomic)
401#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
402#[cfg_attr(feature = "serde", derive(Serialize))]
403pub enum PlainAtomic<'a> {
404    Constant(Constant<'a>),
405    #[display(fmt = "{}({})", _0, _1)]
406    Function(Functor<'a>, Box<Arguments<'a>>),
407}
408
409impl<'a, E: Error<'a>> Parse<'a, E> for PlainAtomic<'a> {
410    fn parse(x: &'a [u8]) -> Result<Self, E> {
411        map(
412            pair(Functor::parse, opt(preceded(ignored, parens))),
413            |(f, args)| match args {
414                None => Self::Constant(Constant(f)),
415                Some(args) => Self::Function(f, Box::new(args)),
416            },
417        )(x)
418    }
419}
420
421/// [`tff_defined_plain`](http://tptp.org/TPTP/SyntaxBNF.html#tff_defined_plain)
422#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
423#[cfg_attr(feature = "serde", derive(Serialize))]
424pub enum DefinedPlain<'a> {
425    Constant(DefinedConstant<'a>),
426    #[display(fmt = "{}({})", _0, _1)]
427    Function(DefinedFunctor<'a>, Box<Arguments<'a>>),
428}
429
430impl<'a, E: Error<'a>> Parse<'a, E> for DefinedPlain<'a> {
431    fn parse(x: &'a [u8]) -> Result<Self, E> {
432        map(
433            pair(DefinedFunctor::parse, opt(preceded(ignored, parens))),
434            |(f, args)| match args {
435                None => Self::Constant(DefinedConstant(f)),
436                Some(args) => Self::Function(f, Box::new(args)),
437            },
438        )(x)
439    }
440}
441
442/// [`tff_defined_atomic`](http://tptp.org/TPTP/SyntaxBNF.html#tff_defined_atomic)
443#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
444#[cfg_attr(feature = "serde", derive(Serialize))]
445pub struct DefinedAtomic<'a>(pub DefinedPlain<'a>);
446
447impl<'a, E: Error<'a>> Parse<'a, E> for DefinedAtomic<'a> {
448    fn parse(x: &'a [u8]) -> Result<Self, E> {
449        map(DefinedPlain::parse, Self)(x)
450    }
451}
452
453/// [`tff_atomic_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_atomic_formula)
454#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
455#[cfg_attr(feature = "serde", derive(Serialize))]
456pub enum AtomicFormula<'a> {
457    Plain(PlainAtomic<'a>),
458    Defined(DefinedAtomic<'a>),
459    System(SystemAtomic<'a>),
460}
461
462impl<'a, E: Error<'a>> Parse<'a, E> for AtomicFormula<'a> {
463    fn parse(x: &'a [u8]) -> Result<Self, E> {
464        alt((
465            map(PlainAtomic::parse, Self::Plain),
466            map(SystemAtomic::parse, Self::System),
467            map(DefinedAtomic::parse, Self::Defined),
468        ))(x)
469    }
470}
471
472struct DefinedInfixTail<'a>(DefinedInfixPred, Box<UnitaryTerm<'a>>);
473
474impl<'a> DefinedInfixTail<'a> {
475    fn finish(self, left: UnitaryTerm<'a>) -> DefinedInfix<'a> {
476        let left = Box::new(left);
477        let op = self.0;
478        let right = self.1;
479        DefinedInfix { left, op, right }
480    }
481}
482
483impl<'a, E: Error<'a>> Parse<'a, E> for DefinedInfixTail<'a> {
484    fn parse(x: &'a [u8]) -> Result<Self, E> {
485        map(
486            pair(
487                preceded(ignored, DefinedInfixPred::parse),
488                preceded(ignored, map(UnitaryTerm::parse, Box::new)),
489            ),
490            |(op, right)| Self(op, right),
491        )(x)
492    }
493}
494
495/// [`tff_defined_infix`](http://tptp.org/TPTP/SyntaxBNF.html#tff_defined_infix)
496#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
497#[display(fmt = "{}{}{}", left, op, right)]
498#[cfg_attr(feature = "serde", derive(Serialize))]
499pub struct DefinedInfix<'a> {
500    pub left: Box<UnitaryTerm<'a>>,
501    pub op: DefinedInfixPred,
502    pub right: Box<UnitaryTerm<'a>>,
503}
504
505impl<'a, E: Error<'a>> Parse<'a, E> for DefinedInfix<'a> {
506    fn parse(x: &'a [u8]) -> Result<Self, E> {
507        map(
508            pair(UnitaryTerm::parse, DefinedInfixTail::parse),
509            |(left, tail)| tail.finish(left),
510        )(x)
511    }
512}
513
514struct InfixUnaryTail<'a>(InfixInequality, Box<UnitaryTerm<'a>>);
515
516impl<'a> InfixUnaryTail<'a> {
517    fn finish(self, left: UnitaryTerm<'a>) -> InfixUnary<'a> {
518        let left = Box::new(left);
519        let op = self.0;
520        let right = self.1;
521        InfixUnary { left, op, right }
522    }
523}
524
525impl<'a, E: Error<'a>> Parse<'a, E> for InfixUnaryTail<'a> {
526    fn parse(x: &'a [u8]) -> Result<Self, E> {
527        map(
528            pair(
529                preceded(ignored, InfixInequality::parse),
530                preceded(ignored, map(UnitaryTerm::parse, Box::new)),
531            ),
532            |(op, right)| Self(op, right),
533        )(x)
534    }
535}
536
537/// [`tff_infix_unary`](http://tptp.org/TPTP/SyntaxBNF.html#tff_infix_unary)
538#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
539#[display(fmt = "{}{}{}", left, op, right)]
540#[cfg_attr(feature = "serde", derive(Serialize))]
541pub struct InfixUnary<'a> {
542    pub left: Box<UnitaryTerm<'a>>,
543    pub op: InfixInequality,
544    pub right: Box<UnitaryTerm<'a>>,
545}
546
547impl<'a, E: Error<'a>> Parse<'a, E> for InfixUnary<'a> {
548    fn parse(x: &'a [u8]) -> Result<Self, E> {
549        map(
550            pair(UnitaryTerm::parse, InfixUnaryTail::parse),
551            |(left, tail)| tail.finish(left),
552        )(x)
553    }
554}
555
556/// [`tff_prefix_unary`](http://tptp.org/TPTP/SyntaxBNF.html#tff_prefix_unary)
557#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
558#[display(fmt = "{}{}", op, formula)]
559#[cfg_attr(feature = "serde", derive(Serialize))]
560pub struct PrefixUnary<'a> {
561    pub op: UnaryConnective,
562    pub formula: Box<PreunitFormula<'a>>,
563}
564
565impl<'a, E: Error<'a>> Parse<'a, E> for PrefixUnary<'a> {
566    fn parse(x: &'a [u8]) -> Result<Self, E> {
567        map(
568            pair(
569                UnaryConnective::parse,
570                preceded(ignored, PreunitFormula::parse),
571            ),
572            |(op, formula)| Self {
573                op,
574                formula: Box::new(formula),
575            },
576        )(x)
577    }
578}
579
580/// [`tff_unary_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_unary_formula)
581#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
582#[cfg_attr(feature = "serde", derive(Serialize))]
583pub enum UnaryFormula<'a> {
584    Prefix(PrefixUnary<'a>),
585    Infix(InfixUnary<'a>),
586}
587
588impl<'a, E: Error<'a>> Parse<'a, E> for UnaryFormula<'a> {
589    fn parse(x: &'a [u8]) -> Result<Self, E> {
590        alt((
591            map(PrefixUnary::parse, Self::Prefix),
592            map(InfixUnary::parse, Self::Infix),
593        ))(x)
594    }
595}
596
597/// [`tff_preunit_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_preunit_formula)
598#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
599#[cfg_attr(feature = "serde", derive(Serialize))]
600pub enum PreunitFormula<'a> {
601    Unitary(UnitaryFormula<'a>),
602    Prefix(PrefixUnary<'a>),
603}
604
605impl<'a, E: Error<'a>> Parse<'a, E> for PreunitFormula<'a> {
606    fn parse(x: &'a [u8]) -> Result<Self, E> {
607        alt((
608            map(PrefixUnary::parse, Self::Prefix),
609            map(UnitaryFormula::parse, Self::Unitary),
610        ))(x)
611    }
612}
613
614/// [`tff_quantified_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_quantified_formula)
615#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
616#[display(fmt = "{}[{}]:{}", quantifier, bound, formula)]
617#[cfg_attr(feature = "serde", derive(Serialize))]
618pub struct QuantifiedFormula<'a> {
619    pub quantifier: fof::Quantifier,
620    pub bound: VariableList<'a>,
621    pub formula: Box<UnitFormula<'a>>,
622}
623
624impl<'a, E: Error<'a>> Parse<'a, E> for QuantifiedFormula<'a> {
625    fn parse(x: &'a [u8]) -> Result<Self, E> {
626        map(
627            tuple((
628                fof::Quantifier::parse,
629                delimited(ignored, brackets, ignored),
630                preceded(tag(":"), preceded(ignored, UnitFormula::parse)),
631            )),
632            |(quantifier, bound, formula)| Self {
633                quantifier,
634                bound,
635                formula: Box::new(formula),
636            },
637        )(x)
638    }
639}
640
641/// [`tff_unitary_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_unitary_formula)
642#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
643#[cfg_attr(feature = "serde", derive(Serialize))]
644pub enum UnitaryFormula<'a> {
645    Quantified(QuantifiedFormula<'a>),
646    Atomic(AtomicFormula<'a>),
647    Variable(common::Variable<'a>),
648    #[display(fmt = "({})", _0)]
649    Logic(Box<LogicFormula<'a>>),
650}
651
652impl<'a, E: Error<'a>> Parse<'a, E> for UnitaryFormula<'a> {
653    fn parse(x: &'a [u8]) -> Result<Self, E> {
654        alt((
655            map(QuantifiedFormula::parse, Self::Quantified),
656            map(AtomicFormula::parse, Self::Atomic),
657            map(common::Variable::parse, Self::Variable),
658            map(map(parens, Box::new), Self::Logic),
659        ))(x)
660    }
661}
662
663enum UnitFormulaTail<'a> {
664    Equality(DefinedInfixTail<'a>),
665    Inequality(InfixUnaryTail<'a>),
666}
667
668impl<'a> UnitFormulaTail<'a> {
669    fn finish(self, left: UnitaryTerm<'a>) -> UnitFormula<'a> {
670        match self {
671            Self::Equality(tail) => {
672                UnitFormula::DefinedInfix(tail.finish(left))
673            }
674            Self::Inequality(tail) => {
675                UnitFormula::Unary(UnaryFormula::Infix(tail.finish(left)))
676            }
677        }
678    }
679}
680
681impl<'a, E: Error<'a>> Parse<'a, E> for UnitFormulaTail<'a> {
682    fn parse(x: &'a [u8]) -> Result<Self, E> {
683        alt((
684            map(DefinedInfixTail::parse, Self::Equality),
685            map(InfixUnaryTail::parse, Self::Inequality),
686        ))(x)
687    }
688}
689
690enum UnitaryTermOrFormula<'a> {
691    Atomic(AtomicFormula<'a>),
692    Variable(common::Variable<'a>),
693    Logic(Box<LogicFormula<'a>>),
694}
695
696impl<'a, E: Error<'a>> Parse<'a, E> for UnitaryTermOrFormula<'a> {
697    fn parse(x: &'a [u8]) -> Result<Self, E> {
698        alt((
699            map(AtomicFormula::parse, Self::Atomic),
700            map(common::Variable::parse, Self::Variable),
701            map(map(parens, Box::new), Self::Logic),
702        ))(x)
703    }
704}
705
706impl<'a> From<UnitaryTermOrFormula<'a>> for UnitaryTerm<'a> {
707    fn from(unit: UnitaryTermOrFormula<'a>) -> Self {
708        match unit {
709            UnitaryTermOrFormula::Atomic(f) => Self::Atomic(f),
710            UnitaryTermOrFormula::Variable(v) => Self::Variable(v),
711            UnitaryTermOrFormula::Logic(f) => Self::Logic(f),
712        }
713    }
714}
715
716impl<'a> From<UnitaryTermOrFormula<'a>> for UnitaryFormula<'a> {
717    fn from(unit: UnitaryTermOrFormula<'a>) -> Self {
718        match unit {
719            UnitaryTermOrFormula::Atomic(f) => Self::Atomic(f),
720            UnitaryTermOrFormula::Variable(v) => Self::Variable(v),
721            UnitaryTermOrFormula::Logic(f) => Self::Logic(f),
722        }
723    }
724}
725
726/// [`tff_unit_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_unit_formula)
727#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
728#[cfg_attr(feature = "serde", derive(Serialize))]
729pub enum UnitFormula<'a> {
730    Unitary(UnitaryFormula<'a>),
731    Unary(UnaryFormula<'a>),
732    DefinedInfix(DefinedInfix<'a>),
733}
734
735impl<'a, E: Error<'a>> Parse<'a, E> for UnitFormula<'a> {
736    fn parse(x: &'a [u8]) -> Result<Self, E> {
737        alt((
738            map(
739                pair(UnitaryTermOrFormula::parse, opt(UnitFormulaTail::parse)),
740                |(left, tail)| {
741                    if let Some(tail) = tail {
742                        tail.finish(left.into())
743                    } else {
744                        UnitFormula::Unitary(left.into())
745                    }
746                },
747            ),
748            map(
749                map(QuantifiedFormula::parse, UnitaryFormula::Quantified),
750                Self::Unitary,
751            ),
752            map(map(PrefixUnary::parse, UnaryFormula::Prefix), Self::Unary),
753            map(
754                pair(DefinedTerm::parse, UnitFormulaTail::parse),
755                |(left, tail)| tail.finish(UnitaryTerm::Defined(left)),
756            ),
757        ))(x)
758    }
759}
760
761fn assoc_tail<'a, E: Error<'a>>(
762    sep: u8,
763) -> impl Fn(&'a [u8]) -> Result<'a, GarbageFirstVec<UnitFormula<'a>>, E> {
764    move |x| {
765        let sep = &[sep];
766        let (x, second) =
767            preceded(tag(sep), preceded(ignored, UnitFormula::parse))(x)?;
768        let mut result = GarbageFirstVec::default();
769        result.push(second);
770        fold_many0_once(
771            preceded(
772                delimited(ignored, tag(sep), ignored),
773                UnitFormula::parse,
774            ),
775            result,
776            |mut result, next| {
777                result.push(next);
778                result
779            },
780        )(x)
781    }
782}
783
784struct OrTail<'a>(GarbageFirstVec<UnitFormula<'a>>);
785
786impl<'a> OrTail<'a> {
787    fn finish(self, left: UnitFormula<'a>) -> OrFormula<'a> {
788        OrFormula(self.0.finish(left))
789    }
790}
791
792impl<'a, E: Error<'a>> Parse<'a, E> for OrTail<'a> {
793    fn parse(x: &'a [u8]) -> Result<Self, E> {
794        map(assoc_tail(b'|'), Self)(x)
795    }
796}
797
798/// [`tff_or_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_or_formula)
799#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
800#[display(fmt = "{}", "Separated('|', _0)")]
801#[cfg_attr(feature = "serde", derive(Serialize))]
802pub struct OrFormula<'a>(pub Vec<UnitFormula<'a>>);
803
804impl<'a, E: Error<'a>> Parse<'a, E> for OrFormula<'a> {
805    fn parse(x: &'a [u8]) -> Result<Self, E> {
806        map(
807            pair(UnitFormula::parse, preceded(ignored, OrTail::parse)),
808            |(first, tail)| tail.finish(first),
809        )(x)
810    }
811}
812
813struct AndTail<'a>(GarbageFirstVec<UnitFormula<'a>>);
814
815impl<'a> AndTail<'a> {
816    fn finish(self, left: UnitFormula<'a>) -> AndFormula<'a> {
817        AndFormula(self.0.finish(left))
818    }
819}
820
821impl<'a, E: Error<'a>> Parse<'a, E> for AndTail<'a> {
822    fn parse(x: &'a [u8]) -> Result<Self, E> {
823        map(assoc_tail(b'&'), Self)(x)
824    }
825}
826
827/// [`tff_and_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_and_formula)
828#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
829#[display(fmt = "{}", "Separated('&', _0)")]
830#[cfg_attr(feature = "serde", derive(Serialize))]
831pub struct AndFormula<'a>(pub Vec<UnitFormula<'a>>);
832
833impl<'a, E: Error<'a>> Parse<'a, E> for AndFormula<'a> {
834    fn parse(x: &'a [u8]) -> Result<Self, E> {
835        map(
836            pair(UnitFormula::parse, preceded(ignored, AndTail::parse)),
837            |(first, tail)| tail.finish(first),
838        )(x)
839    }
840}
841
842enum BinaryAssocTail<'a> {
843    Or(OrTail<'a>),
844    And(AndTail<'a>),
845}
846
847impl<'a> BinaryAssocTail<'a> {
848    fn finish(self, left: UnitFormula<'a>) -> BinaryAssoc {
849        match self {
850            Self::Or(tail) => BinaryAssoc::Or(tail.finish(left)),
851            Self::And(tail) => BinaryAssoc::And(tail.finish(left)),
852        }
853    }
854}
855
856impl<'a, E: Error<'a>> Parse<'a, E> for BinaryAssocTail<'a> {
857    fn parse(x: &'a [u8]) -> Result<Self, E> {
858        alt((
859            map(OrTail::parse, BinaryAssocTail::Or),
860            map(AndTail::parse, BinaryAssocTail::And),
861        ))(x)
862    }
863}
864
865/// [`tff_binary_assoc`](http://tptp.org/TPTP/SyntaxBNF.html#tff_binary_assoc)
866#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
867#[cfg_attr(feature = "serde", derive(Serialize))]
868pub enum BinaryAssoc<'a> {
869    Or(OrFormula<'a>),
870    And(AndFormula<'a>),
871}
872
873impl<'a, E: Error<'a>> Parse<'a, E> for BinaryAssoc<'a> {
874    fn parse(x: &'a [u8]) -> Result<Self, E> {
875        map(
876            pair(
877                UnitFormula::parse,
878                preceded(ignored, BinaryAssocTail::parse),
879            ),
880            |(first, tail)| tail.finish(first),
881        )(x)
882    }
883}
884
885struct BinaryNonassocTail<'a>(NonassocConnective, Box<UnitFormula<'a>>);
886
887impl<'a> BinaryNonassocTail<'a> {
888    fn finish(self, left: UnitFormula<'a>) -> BinaryNonassoc<'a> {
889        let left = Box::new(left);
890        let op = self.0;
891        let right = self.1;
892        BinaryNonassoc { left, op, right }
893    }
894}
895
896impl<'a, E: Error<'a>> Parse<'a, E> for BinaryNonassocTail<'a> {
897    fn parse(x: &'a [u8]) -> Result<Self, E> {
898        map(
899            pair(
900                NonassocConnective::parse,
901                preceded(ignored, map(UnitFormula::parse, Box::new)),
902            ),
903            |(connective, right)| Self(connective, right),
904        )(x)
905    }
906}
907
908/// [`tff_binary_nonassoc`](http://tptp.org/TPTP/SyntaxBNF.html#tff_binary_nonassoc)
909#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
910#[display(fmt = "{}{}{}", left, op, right)]
911#[cfg_attr(feature = "serde", derive(Serialize))]
912pub struct BinaryNonassoc<'a> {
913    pub left: Box<UnitFormula<'a>>,
914    pub op: NonassocConnective,
915    pub right: Box<UnitFormula<'a>>,
916}
917
918impl<'a, E: Error<'a>> Parse<'a, E> for BinaryNonassoc<'a> {
919    fn parse(x: &'a [u8]) -> Result<Self, E> {
920        map(
921            pair(
922                UnitFormula::parse,
923                preceded(ignored, BinaryNonassocTail::parse),
924            ),
925            |(left, tail)| tail.finish(left),
926        )(x)
927    }
928}
929
930enum BinaryFormulaTail<'a> {
931    Assoc(BinaryAssocTail<'a>),
932    Nonassoc(BinaryNonassocTail<'a>),
933}
934
935impl<'a> BinaryFormulaTail<'a> {
936    fn finish(self, left: UnitFormula<'a>) -> BinaryFormula<'a> {
937        match self {
938            Self::Assoc(tail) => BinaryFormula::Assoc(tail.finish(left)),
939            Self::Nonassoc(tail) => BinaryFormula::Nonassoc(tail.finish(left)),
940        }
941    }
942}
943
944impl<'a, E: Error<'a>> Parse<'a, E> for BinaryFormulaTail<'a> {
945    fn parse(x: &'a [u8]) -> Result<Self, E> {
946        alt((
947            map(BinaryAssocTail::parse, Self::Assoc),
948            map(BinaryNonassocTail::parse, Self::Nonassoc),
949        ))(x)
950    }
951}
952
953/// [`tff_binary_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_binary_formula)
954#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
955#[cfg_attr(feature = "serde", derive(Serialize))]
956pub enum BinaryFormula<'a> {
957    Assoc(BinaryAssoc<'a>),
958    Nonassoc(BinaryNonassoc<'a>),
959}
960
961impl<'a, E: Error<'a>> Parse<'a, E> for BinaryFormula<'a> {
962    fn parse(x: &'a [u8]) -> Result<Self, E> {
963        map(
964            pair(
965                UnitFormula::parse,
966                preceded(ignored, BinaryFormulaTail::parse),
967            ),
968            |(left, tail)| tail.finish(left),
969        )(x)
970    }
971}
972
973/// [`tfx_logic_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tfx_logic_formula)
974#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
975#[cfg_attr(feature = "serde", derive(Serialize))]
976pub enum LogicFormula<'a> {
977    Unary(UnaryFormula<'a>),
978    Unitary(UnitaryFormula<'a>),
979    Binary(BinaryFormula<'a>),
980    DefinedInfix(DefinedInfix<'a>),
981}
982
983impl<'a, E: Error<'a>> Parse<'a, E> for LogicFormula<'a> {
984    fn parse(x: &'a [u8]) -> Result<Self, E> {
985        map(
986            pair(
987                UnitFormula::parse,
988                opt(preceded(ignored, BinaryFormulaTail::parse)),
989            ),
990            |(left, tail)| match tail {
991                Some(tail) => Self::Binary(tail.finish(left)),
992                None => match left {
993                    UnitFormula::Unary(u) => Self::Unary(u),
994                    UnitFormula::Unitary(u) => Self::Unitary(u),
995                    UnitFormula::DefinedInfix(i) => Self::DefinedInfix(i),
996                },
997            },
998        )(x)
999    }
1000}
1001
1002/// [`tff_formula`](http://tptp.org/TPTP/SyntaxBNF.html#tff_formula)
1003#[derive(Clone, Debug, Display, PartialOrd, Ord, PartialEq, Eq, Hash)]
1004#[cfg_attr(feature = "serde", derive(Serialize))]
1005pub enum Formula<'a> {
1006    Logic(Box<LogicFormula<'a>>),
1007    AtomTyping(Box<AtomTyping<'a>>),
1008}
1009
1010impl<'a, E: Error<'a>> Parse<'a, E> for Formula<'a> {
1011    fn parse(x: &'a [u8]) -> Result<Self, E> {
1012        alt((
1013            map(map(AtomTyping::parse, Box::new), Self::AtomTyping),
1014            map(map(LogicFormula::parse, Box::new), Self::Logic),
1015        ))(x)
1016    }
1017}
1018
1019#[cfg(test)]
1020mod tests {
1021    use super::*;
1022    use crate::tests::*;
1023
1024    #[test]
1025    fn test_tfx_type_arguments() {
1026        check_size::<TypeArguments>();
1027        parse::<TypeArguments>(b"A\0");
1028        parse::<TypeArguments>(b"A , c\0");
1029    }
1030
1031    #[test]
1032    fn test_tfx_atomic_type() {
1033        check_size::<AtomicType>();
1034        parse::<AtomicType>(b"type_constant\0");
1035        parse::<AtomicType>(b"$defined_type\0");
1036        parse::<AtomicType>(b"TypeVariable\0");
1037        parse::<AtomicType>(b"type_function (A, B)\0");
1038    }
1039
1040    #[test]
1041    fn test_tfx_typed_variable() {
1042        check_size::<TypedVariable>();
1043        parse::<TypedVariable>(b"X : A\0");
1044    }
1045
1046    #[test]
1047    fn test_tfx_variable() {
1048        check_size::<super::Variable>();
1049        parse::<super::Variable>(b"X\0");
1050        parse::<super::Variable>(b"X : A\0");
1051    }
1052
1053    #[test]
1054    fn test_tfx_variable_list() {
1055        check_size::<VariableList>();
1056        parse::<VariableList>(b"X\0");
1057        parse::<VariableList>(b"X , Y : A , Z : c\0");
1058    }
1059
1060    #[test]
1061    fn test_tfx_xprod_type() {
1062        check_size::<XprodType>();
1063        parse::<XprodType>(b"A * c\0");
1064        parse::<XprodType>(b"A * B * c\0");
1065    }
1066
1067    #[test]
1068    fn test_tfx_unitary_type() {
1069        check_size::<UnitaryType>();
1070        parse::<UnitaryType>(b"A\0");
1071        parse::<UnitaryType>(b"( A * B )\0");
1072        parse::<UnitaryType>(b"( ( A * c ) * ( B * d ) )\0");
1073    }
1074
1075    #[test]
1076    fn test_tfx_mapping_type() {
1077        check_size::<MappingType>();
1078        parse::<MappingType>(b"A > B\0");
1079        parse::<MappingType>(b"( A * c ) > B\0");
1080    }
1081
1082    #[test]
1083    fn test_tfx_quantified_type() {
1084        check_size::<QuantifiedType>();
1085        parse::<QuantifiedType>(b"!> [ A : $tType , B ] : A\0");
1086    }
1087
1088    #[test]
1089    fn test_tfx_monotype() {
1090        check_size::<Monotype>();
1091        parse::<Monotype>(b"A\0");
1092        parse::<Monotype>(b"( A > A )\0");
1093        parse::<Monotype>(b"!>[A]: A\0");
1094    }
1095
1096    #[test]
1097    fn test_tfx_non_atomic_type() {
1098        check_size::<NonAtomicType>();
1099        parse::<NonAtomicType>(b"A > A\0");
1100        parse::<NonAtomicType>(b"!>[A]: A\0");
1101        parse::<NonAtomicType>(b"( A > A )\0");
1102    }
1103
1104    #[test]
1105    fn test_tfx_top_level_type() {
1106        check_size::<TopLevelType>();
1107        parse::<TopLevelType>(b"A\0");
1108        parse::<TopLevelType>(b"A > A\0");
1109    }
1110
1111    #[test]
1112    fn test_tfx_atom_typing() {
1113        check_size::<AtomTyping>();
1114        parse::<AtomTyping>(b"c : A\0");
1115        parse::<AtomTyping>(b"( c : A )\0");
1116    }
1117
1118    #[test]
1119    fn test_tfx_term() {
1120        check_size::<Term>();
1121        parse::<Term>(b"$true\0");
1122        parse::<Term>(b"123\0");
1123    }
1124
1125    #[test]
1126    fn test_tfx_unitary_term() {
1127        check_size::<UnitaryTerm>();
1128        parse::<UnitaryTerm>(b"p\0");
1129        parse::<UnitaryTerm>(b"123\0");
1130        parse::<UnitaryTerm>(b"X\0");
1131        parse::<UnitaryTerm>(b"( $true )\0");
1132    }
1133
1134    #[test]
1135    fn test_tfx_arguments() {
1136        check_size::<Arguments>();
1137        parse::<Arguments>(b"$true\0");
1138        parse::<Arguments>(b"$true , $true\0");
1139    }
1140
1141    #[test]
1142    fn test_tfx_system_atomic() {
1143        check_size::<SystemAtomic>();
1144        parse::<SystemAtomic>(b"$$system\0");
1145        parse::<SystemAtomic>(b"$$system ( $true )\0");
1146    }
1147
1148    #[test]
1149    fn test_tfx_plain_atomic() {
1150        check_size::<PlainAtomic>();
1151        parse::<PlainAtomic>(b"c\0");
1152        parse::<PlainAtomic>(b"f ( $true )\0");
1153    }
1154
1155    #[test]
1156    fn test_tfx_defined_plain() {
1157        check_size::<DefinedPlain>();
1158        parse::<DefinedPlain>(b"$defined\0");
1159        parse::<DefinedPlain>(b"$defined ( $true )\0");
1160    }
1161
1162    #[test]
1163    fn test_tfx_defined_atomic() {
1164        check_size::<DefinedAtomic>();
1165        parse::<DefinedAtomic>(b"$defined\0");
1166    }
1167
1168    #[test]
1169    fn test_tfx_atomic_formula() {
1170        check_size::<AtomicFormula>();
1171        parse::<AtomicFormula>(b"p\0");
1172        parse::<AtomicFormula>(b"$defined\0");
1173        parse::<AtomicFormula>(b"$$system\0");
1174    }
1175
1176    #[test]
1177    fn test_tfx_defined_infix() {
1178        check_size::<DefinedInfix>();
1179        parse::<DefinedInfix>(b"X = Y\0");
1180    }
1181
1182    #[test]
1183    fn test_tfx_infix_unary() {
1184        check_size::<InfixUnary>();
1185        parse::<InfixUnary>(b"X != Y\0");
1186    }
1187
1188    #[test]
1189    fn test_tfx_prefix_unary() {
1190        check_size::<PrefixUnary>();
1191        parse::<PrefixUnary>(b"~ $true\0");
1192    }
1193
1194    #[test]
1195    fn test_tfx_unary_formula() {
1196        check_size::<UnaryFormula>();
1197        parse::<UnaryFormula>(b"X != Y\0");
1198        parse::<UnaryFormula>(b"~ $true\0");
1199    }
1200
1201    #[test]
1202    fn test_tfx_preunit_formula() {
1203        check_size::<PreunitFormula>();
1204        parse::<PreunitFormula>(b"$true\0");
1205        parse::<PreunitFormula>(b"~ $true\0");
1206    }
1207
1208    #[test]
1209    fn test_tfx_quantified_formula() {
1210        check_size::<QuantifiedFormula>();
1211        parse::<QuantifiedFormula>(b"! [ X : A ] : $true\0");
1212    }
1213
1214    #[test]
1215    fn test_tfx_unitary_formula() {
1216        check_size::<UnitaryFormula>();
1217        parse::<UnitaryFormula>(b"![X : A]: $true\0");
1218        parse::<UnitaryFormula>(b"$true\0");
1219        parse::<UnitaryFormula>(b"X\0");
1220        parse::<UnitaryFormula>(b"( $true )\0");
1221    }
1222
1223    #[test]
1224    fn test_tfx_unit_formula() {
1225        check_size::<UnitFormula>();
1226        parse::<UnitFormula>(b"$true\0");
1227        parse::<UnitFormula>(b"~$true\0");
1228        parse::<UnitFormula>(b"X = Y\0");
1229    }
1230
1231    #[test]
1232    fn test_tfx_binary_nonassoc() {
1233        check_size::<BinaryNonassoc>();
1234        parse::<BinaryNonassoc>(b"p => q\0");
1235    }
1236
1237    #[test]
1238    fn test_tfx_or_formula() {
1239        check_size::<OrFormula>();
1240        parse::<OrFormula>(b"p | q | r\0");
1241    }
1242
1243    #[test]
1244    fn test_tfx_and_formula() {
1245        check_size::<AndFormula>();
1246        parse::<AndFormula>(b"p & q\0");
1247    }
1248
1249    #[test]
1250    fn test_tfx_binary_assoc() {
1251        check_size::<BinaryAssoc>();
1252        parse::<BinaryAssoc>(b"p | q | r\0");
1253        parse::<BinaryAssoc>(b"p & q\0");
1254    }
1255
1256    #[test]
1257    fn test_tfx_binary_formula() {
1258        check_size::<BinaryFormula>();
1259        parse::<BinaryFormula>(b"p => q\0");
1260        parse::<BinaryFormula>(b"p | q | r\0");
1261    }
1262
1263    #[test]
1264    fn test_tfx_logic_formula() {
1265        check_size::<LogicFormula>();
1266        parse::<LogicFormula>(b"$true\0");
1267        parse::<LogicFormula>(b"~ p\0");
1268        parse::<LogicFormula>(b"p => q\0");
1269        parse::<LogicFormula>(b"X = Y\0");
1270    }
1271
1272    #[test]
1273    fn test_tfx_formula() {
1274        check_size::<Formula>();
1275        parse::<Formula>(b"$true\0");
1276        parse::<Formula>(b"c : A\0");
1277    }
1278}