summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/var.rs
diff options
context:
space:
mode:
authorNadrieril2019-12-27 17:03:43 +0000
committerNadrieril2020-01-17 10:06:00 +0000
commitbc3599b815c6f9cad2f4efd30c009cbe8f765ca1 (patch)
tree932a57bd6723aa9554e263ed280700bdc314917a /dhall/src/semantics/core/var.rs
parent654d752c65f0e221d225ed045a0aee62f223855e (diff)
Assign a unique id to each binder
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/var.rs10
1 files changed, 8 insertions, 2 deletions
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index add0500..28ddadd 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -11,11 +11,17 @@ pub struct AlphaVar {
alpha: V<()>,
}
+type BinderUID = u64;
+
// Exactly like a Label, but equality returns always true.
// This is so that ValueKind equality is exactly alpha-equivalence.
#[derive(Clone, Eq)]
pub struct Binder {
name: Label,
+ /// Id of the binder, unique across the current expression. Used to distinguish bindersinstead
+ /// of their name. The id won't actually be unique when there are imports around, but
+ /// typechecking ensures this can't cause a conflict.
+ uid: BinderUID,
}
pub(crate) trait Shift: Sized {
@@ -67,8 +73,8 @@ impl AlphaVar {
}
impl Binder {
- pub(crate) fn new(name: Label) -> Self {
- Binder { name }
+ pub(crate) fn new(name: Label, uid: BinderUID) -> Self {
+ Binder { name, uid }
}
pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
if alpha {