summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/context.rs
diff options
context:
space:
mode:
authorNadrieril2020-01-17 18:57:52 +0000
committerNadrieril2020-01-17 18:57:52 +0000
commitb7d847cc812e6a7ce52354b15a9ed6b41ffeb3b4 (patch)
tree9dd7fb2456aed5e05cd522da2db37e7c2304875c /dhall/src/semantics/core/context.rs
parent0f4a4801ed67826dc82015d39ce8fd05e7950035 (diff)
Simplify
Diffstat (limited to 'dhall/src/semantics/core/context.rs')
-rw-r--r--dhall/src/semantics/core/context.rs12
1 files changed, 7 insertions, 5 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 47d2d2d..8c64c26 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -6,7 +6,9 @@ use crate::syntax::{Label, V};
#[derive(Debug, Clone)]
enum CtxItem {
- Kept(AlphaVar, Value),
+ // Variable is bound with given type
+ Kept(Value),
+ // Variable has been replaced by corresponding value
Replaced(Value),
}
@@ -24,7 +26,7 @@ impl TyCtx {
}
pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
let mut vec = self.ctx.clone();
- vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
+ vec.push((x.clone(), CtxItem::Kept(t.under_binder())));
self.with_vec(vec)
}
pub fn insert_value(
@@ -47,7 +49,7 @@ impl TyCtx {
Some(newvar) => newvar,
None => break item,
};
- if let CtxItem::Kept(_, _) = item {
+ if let CtxItem::Kept(_) = item {
shift_delta += 1;
}
} else {
@@ -57,8 +59,8 @@ impl TyCtx {
};
let v = match found_item {
- CtxItem::Kept(newvar, t) => Value::from_kind_and_type(
- ValueKind::Var(newvar.clone()),
+ CtxItem::Kept(t) => Value::from_kind_and_type(
+ ValueKind::Var(AlphaVar::default()),
t.clone(),
),
CtxItem::Replaced(v) => v.clone(),