why3 0.13.0

Why3 AST and pretty printers
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34

use crate::{Ident, Name, QName};

#[cfg(feature = "serialize")]
use serde::{Deserialize, Serialize};

#[derive(Debug, Clone, PartialEq, Eq)]
#[cfg_attr(feature = "serialize", derive(Serialize, Deserialize))]
pub enum Type {
    TVar(Ident),
    TConstructor(Name),
    TApp(Box<Type>, Box<[Type]>),
    Tuple(Box<[Type]>),
    TFun(Box<Type>, Box<Type>),
}

impl Type {
    pub fn unit() -> Self {
        Self::Tuple(Box::new([]))
    }

    pub fn tapp(self, args: impl IntoIterator<Item = Self>) -> Self {
        let mut args = args.into_iter().peekable();
        if args.peek().is_none() { self } else { Self::TApp(Box::new(self), args.collect()) }
    }

    pub(crate) fn complex(&self) -> bool {
        use Type::*;
        !matches!(self, TVar(_) | Tuple(_) | TConstructor(_))
    }

    pub fn qconstructor(qname: QName) -> Self {
        Self::TConstructor(Name::Global(qname))
    }
}