ravenlang 0.3.0

Language core for ravencheck.
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71

use crate::{
    CaseName,
    Comp,
    CType,
    Gen,
    parse_str_cbpv,
    Sig,
};

use std::fmt;

/// The Comp cases in a Prop are normal-form and prop-type.
pub struct Prop {
    pub cases: Vec<(CaseName, Comp)>,
    vgen: Gen,
}

pub enum Error {
    Parse(syn::Error),
    Type(String),
}

impl fmt::Display for Error {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Error::Parse(e) =>
                write!(f, "parse error: {}", e),
            Error::Type(s) =>
                write!(f, "type error: {}", s),
        }
    }
}

pub type Result<A> = std::result::Result<A, Error>;

impl Prop {
    pub fn parse(input: &str, sig: &Sig) -> Result<Self> {
        match parse_str_cbpv(input) {
            Ok(c) => c.as_prop(sig),
            Err(e) => Err(Error::Parse(e)),
        }
    }

    pub fn negate(&mut self, sig: &Sig) {
        for (_,c) in self.cases.iter_mut() {
            *c = c.negate().normal_form_single_case(sig, &mut self.vgen);
        }
    }

    pub fn is_single_case(&self) -> bool {
        self.cases.len() == 1
    }
}

impl Comp {
    pub fn as_prop(mut self, sig: &Sig) -> Result<Prop> {
        self = self.expand_types(&sig.type_aliases);
        match self.type_check(&CType::return_prop(), sig) {
            Ok(()) => {
                let mut vgen = self.get_gen();
                let cases = self.normal_form_x(
                    sig,
                    &mut vgen,
                    CaseName::root()
                );
                Ok(Prop{cases, vgen})
            }
            Err(e) => Err(Error::Type(e)),
        }
    }
}