diff options
author | Nadrieril | 2019-12-27 17:03:43 +0000 |
---|---|---|
committer | Nadrieril | 2020-01-17 10:06:00 +0000 |
commit | bc3599b815c6f9cad2f4efd30c009cbe8f765ca1 (patch) | |
tree | 932a57bd6723aa9554e263ed280700bdc314917a /dhall/src/semantics/core/var.rs | |
parent | 654d752c65f0e221d225ed045a0aee62f223855e (diff) |
Assign a unique id to each binder
Diffstat (limited to 'dhall/src/semantics/core/var.rs')
-rw-r--r-- | dhall/src/semantics/core/var.rs | 10 |
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 { |