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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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#[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}