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
|
use crate::ast::*;
use crate::checker_state::{CheckerError, CheckerState};
use tracing::{debug, instrument};
impl Programme {
pub fn check(&self) -> Result<(), CheckerError> {
let mut state = CheckerState::default();
state.check(self)
}
}
impl CheckerState {
#[instrument(skip(self, prog), level = "debug")]
pub fn check(&mut self, prog: &Programme) -> Result<(), CheckerError> {
let Programme(decls) = prog;
for decl in decls {
debug!(%self, %decl);
match decl {
Decl::Set { name, set } => {
self.assert_unbound_set(name)?;
let set = self.check_set(set.clone())?;
self.add_set(name.clone(), set.into())
}
Decl::Element { name, element, set } => {
self.assert_unbound_element(name)?;
let set = self.check_set(set.clone())?;
let element = self.check_element(element.clone().into(), &set)?;
self.add_element(name.clone(), element.into(), set)
}
Decl::Signature { name, signature } => {
self.assert_unbound_signature(name)?;
let signature = self.check_signature(signature.clone())?;
self.add_signature(name, signature, false)
}
Decl::Instance {
name,
instance,
signature,
} => {
self.assert_unbound_instance(name)?;
let signature = self.check_signature(signature.clone())?;
let instance = self.check_instance(instance.clone(), (&signature).into())?;
self.add_instance(name.clone(), instance.into(), signature)
}
}?;
}
debug!(%self);
Ok(())
}
}
|
