summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/var.rs24
-rw-r--r--dhall/src/semantics/phase/typecheck.rs3
2 files changed, 16 insertions, 11 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index 28ddadd..98b315e 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -9,6 +9,8 @@ use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V};
pub struct AlphaVar {
normal: V<Label>,
alpha: V<()>,
+ /// Id of the corresponding binder.
+ binder_uid: BinderUID,
}
type BinderUID = u64;
@@ -93,6 +95,7 @@ impl Shift for AlphaVar {
Some(AlphaVar {
normal: self.normal.shift(delta, &var.normal)?,
alpha: self.alpha.shift(delta, &var.alpha)?,
+ binder_uid: self.binder_uid,
})
}
}
@@ -121,23 +124,24 @@ impl std::fmt::Debug for Binder {
}
}
-impl From<Label> for AlphaVar {
- fn from(x: Label) -> AlphaVar {
+impl<'a> From<&'a Label> for AlphaVar {
+ fn from(x: &'a Label) -> AlphaVar {
AlphaVar {
- normal: V(x, 0),
+ normal: V(x.clone(), 0),
alpha: V((), 0),
+ // TODO: evil evil but only used in shift
+ binder_uid: 0,
}
}
}
-impl<'a> From<&'a Label> for AlphaVar {
- fn from(x: &'a Label) -> AlphaVar {
- x.clone().into()
- }
-}
impl From<Binder> for AlphaVar {
fn from(x: Binder) -> AlphaVar {
- let l: Label = x.into();
- l.into()
+ let binder_uid = x.uid;
+ AlphaVar {
+ normal: V(x.into(), 0),
+ alpha: V((), 0),
+ binder_uid,
+ }
}
}
impl<'a> From<&'a Binder> for AlphaVar {
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index 926598d..7e408eb 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -494,10 +494,11 @@ fn type_last_layer(
ValueKind::UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
Some(Some(t)) => {
+ let x = ctx.new_binder(x);
RetTypeOnly(
tck_pi_type(
ctx,
- ctx.new_binder(x),
+ x.clone(),
t.clone(),
r.under_binder(x),
)?