ravenlang 0.1.2

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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109

use crate::{
    Binder1,
    BinderN,
    Comp,
    Sig,
    Val,
    VName,
    VType,
};

fn expand_types_sig(
    xs: Vec<(VName,Option<VType>)>, sig: &Sig
) -> Vec<(VName,Option<VType>)> {
    xs.into_iter().map(|(x,t)| {
        let t = match t {
            Some(t) => Some(t.expand_aliases(&sig.type_aliases)),
            None => None,
        };
        (x,t)
    }).collect()
}

fn expand_types_q(
    xs: Vec<(VName,VType)>, sig: &Sig
) -> Vec<(VName,VType)> {
    xs.into_iter().map(|(x,t)| {
        (x,t.expand_aliases(&sig.type_aliases))
    }).collect()
}

impl Binder1 {
    pub fn expand_types(self, sig: &Sig) -> Self {
        match self {
            Self::Eq(b, vs1, vs2) => Self::Eq(
                b,
                vs1.into_iter().map(|v| v.expand_types(sig)).collect(),
                vs2.into_iter().map(|v| v.expand_types(sig)).collect(),
            ),
            Self::LogQuantifier(q, xs, m) => Self::LogQuantifier(
                q,
                expand_types_q(xs, sig),
                Box::new(m.expand_types(sig)),
            ),
            Self::LogNot(v) => Self::LogNot(v.expand_types(sig)),
            Self::LogOpN(op, vs) => Self::LogOpN(
                op,
                vs.into_iter().map(|v| v.expand_types(sig)).collect(),
            ),
        }
    }
}

impl BinderN {
    pub fn expand_types(self, sig: &Sig) -> Self {
        match self {
            Self::Call(s, vs) => Self::Call(
                s,
                vs.into_iter().map(|v| v.expand_types(sig)).collect(),
            ),
            Self::Seq(m) => Self::Seq(Box::new(m.expand_types(sig))),
        }
    }
}

impl Comp {
    pub fn expand_types(self, sig: &Sig) -> Self {
        match self {
            Self::Apply(m, vs) => Self::Apply(
                Box::new(m.expand_types(sig)),
                vs.into_iter().map(|v| v.expand_types(sig)).collect(),
            ),
            Self::BindN(b, ps, m) => Self::BindN(
                b.expand_types(sig),
                ps,
                Box::new(m.expand_types(sig)),
            ),
            Self::Bind1(b, x, m) => Self::Bind1(
                b.expand_types(sig),
                x,
                Box::new(m.expand_types(sig)),
            ),
            Self::Force(v) => Self::Force(v.expand_types(sig)),
            Self::Fun(xs, m) => Self::Fun(
                expand_types_sig(xs, sig),
                Box::new(m.expand_types(sig)),
            ),
            Self::Ite(cond, then_b, else_b) => Self::Ite(
                cond.expand_types(sig),
                Box::new(then_b.expand_types(sig)),
                Box::new(else_b.expand_types(sig)),
            ),
            Self::Return(vs) => Self::Return(
                vs.into_iter().map(|v| v.expand_types(sig)).collect()
            ),
        }
    }
}

impl Val {
    pub fn expand_types(self, sig: &Sig) -> Self {
        match self {
            Self::Thunk(m) => Self::Thunk(Box::new(m.expand_types(sig))),
            Self::Tuple(vs) => Self::Tuple(
                vs.into_iter().map(|v| v.expand_types(sig)).collect()
            ),
            v => v,
        }
    }
}