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
use std::collections::BTreeMap;
use super::read_back::{generate_value, ReadBack};
use super::tcm::{TCE, TCM, TCS};
use crate::ast::{Case, Value};
pub fn check_subtype(
index: u32,
tcs: TCS,
subtype: Value,
supertype: Value,
read_back: bool,
) -> TCM<TCS> {
use crate::ast::Value::*;
match (subtype, supertype) {
(Type(sub_level), Type(super_level)) => {
if sub_level <= super_level {
Ok(tcs)
} else {
Err(TCE::TypeMismatch(Type(sub_level), Type(super_level)))
}
}
(Sum(sub_tree), Sum(super_tree)) => check_subtype_sum(index, tcs, sub_tree, super_tree),
(Pi(sub_param, sub_closure), Pi(super_param, super_closure))
| (Sigma(sub_param, sub_closure), Sigma(super_param, super_closure)) => {
let tcs = check_subtype(index, tcs, *super_param, *sub_param, true)?;
let generated = generate_value(index);
check_subtype(
index + 1,
tcs_borrow!(tcs),
sub_closure.instantiate(generated.clone()),
super_closure.instantiate(generated),
true,
)?;
Ok(tcs)
}
(subtype, supertype) => {
if read_back {
compare_normal(index, tcs, subtype, supertype)
} else {
Err(TCE::TypeMismatch(subtype, supertype))
}
}
}
}
#[inline]
pub fn check_subtype_sum(
index: u32,
tcs: TCS,
sub_tree: BTreeMap<String, Box<Case>>,
mut super_tree: BTreeMap<String, Box<Case>>,
) -> TCM<TCS> {
for (constructor, sub_parameter) in sub_tree.into_iter() {
let super_parameter = super_tree
.remove(constructor.as_str())
.ok_or_else(|| TCE::UnexpectedCases(constructor))?;
let sub_parameter = sub_parameter.reduce_to_value();
let super_parameter = super_parameter.reduce_to_value();
compare_normal(
index,
tcs_borrow!(tcs),
sub_parameter.clone(),
super_parameter.clone(),
)
.or_else(|_err| {
check_subtype(
index,
tcs_borrow!(tcs),
sub_parameter,
super_parameter,
false,
)
})?;
}
Ok(tcs)
}
pub fn compare_normal(index: u32, tcs: TCS, subtype: Value, supertype: Value) -> TCM<TCS> {
let (inferred_normal, expected_normal) = ReadBack::normal(index, subtype, supertype);
if inferred_normal == expected_normal {
Ok(tcs)
} else {
Err(TCE::ReadBackTypeMismatch(inferred_normal, expected_normal))
}
}