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
use std::collections::BTreeMap;
use crate::reduce::*;
use crate::syntax::*;
type Gamma<Name> = BTreeMap<Name, Value<Name>>;
pub fn generate_value<Name: NameTrait>(id: u32) -> Value<Name> {
Value::Neutral(Neutral::Generated(id))
}
pub fn update_gamma<'a, Name: DebuggableNameTrait>(
gamma: &'a mut Gamma<Name>,
pattern: &Pattern<Name>,
type_val: Value<Name>,
val: Value<Name>,
) -> Result<&'a mut Gamma<Name>, String> {
match pattern {
Pattern::Pair(pattern_first, pattern_second) => match type_val {
Value::Sigma(first, second) => {
let val_first = val.clone().first();
update_gamma(gamma, pattern_first, *first, val_first.clone())
.and_then(|gamma| {
update_gamma(
gamma,
pattern_second,
second.instantiate(val_first),
val.second(),
)
})
}
_ => Err(format!("Cannot update Gamma by: {:?}", pattern)),
},
Pattern::Var(name) => {
gamma.insert(name.clone(), type_val);
Ok(gamma)
}
Pattern::Unit => Ok(gamma),
}
}