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
|
use crate::error::TypeError;
use crate::semantics::core::value::Value;
use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{AlphaVar, Binder};
use crate::semantics::nze::{NzVar, QuoteEnv};
use crate::semantics::phase::normalize::{NzEnv, NzEnvItem};
use crate::syntax::{Label, V};
#[derive(Debug, Clone)]
enum CtxItem {
// Variable is bound with given type
Kept(Value),
// Variable has been replaced by corresponding value
Replaced(Value),
}
#[derive(Debug, Clone)]
pub(crate) struct TyCtx {
ctx: Vec<(Binder, CtxItem)>,
}
impl TyCtx {
pub fn new() -> Self {
TyCtx { ctx: Vec::new() }
}
fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
TyCtx { ctx: vec }
}
pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
let mut vec = self.ctx.clone();
vec.push((x.clone(), CtxItem::Kept(t.under_binder())));
self.with_vec(vec)
}
pub fn insert_value(
&self,
x: &Binder,
e: Value,
) -> Result<Self, TypeError> {
let mut vec = self.ctx.clone();
vec.push((x.clone(), CtxItem::Replaced(e)));
Ok(self.with_vec(vec))
}
pub fn lookup(&self, var: &V<Label>) -> Option<Value> {
let mut var = var.clone();
let mut shift_delta: isize = 0;
let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i));
let found_item = loop {
if let Some((label, item)) = rev_ctx.next() {
var = match var.over_binder(&label) {
Some(newvar) => newvar,
None => break item,
};
if let CtxItem::Kept(_) = item {
shift_delta += 1;
}
} else {
// Unbound variable
return None;
}
};
let var_idx = rev_ctx
.filter(|(_, i)| match i {
CtxItem::Kept(_) => true,
CtxItem::Replaced(_) => false,
})
.count();
let v = match found_item {
CtxItem::Kept(t) => Value::from_kind_and_type(
ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)),
t.clone(),
),
CtxItem::Replaced(v) => v.clone()
// .to_tyexpr(QuoteEnv::construct(var_idx))
// .normalize_whnf(&NzEnv::construct(
// self.ctx
// .iter()
// .filter_map(|(_, i)| match i {
// CtxItem::Kept(t) => {
// Some(NzEnvItem::Kept(t.clone()))
// }
// CtxItem::Replaced(_) => None,
// })
// .collect(),
// )),
};
// Can't fail because delta is positive
let v = v.shift(shift_delta, &AlphaVar::default()).unwrap();
return Some(v);
}
// pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> {
// self.lookup(&var.normal)
// }
pub fn new_binder(&self, l: &Label) -> Binder {
Binder::new(l.clone())
}
}
|
