summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs20
-rw-r--r--dhall/src/semantics/core/var.rs10
2 files changed, 25 insertions, 5 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 3a7930e..25e4037 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,4 +1,6 @@
+use std::cell::RefCell;
use std::collections::HashMap;
+use std::rc::Rc;
use crate::error::TypeError;
use crate::semantics::core::value::Value;
@@ -15,14 +17,23 @@ enum CtxItem {
#[derive(Debug, Clone)]
pub(crate) struct TyCtx {
ctx: Vec<(Binder, CtxItem)>,
+ /// Keeps track of the next free binder id to assign. Shared among all the contexts to ensure
+ /// unicity across the expression.
+ next_uid: Rc<RefCell<u64>>,
}
impl TyCtx {
pub fn new() -> Self {
- TyCtx { ctx: Vec::new() }
+ TyCtx {
+ ctx: Vec::new(),
+ next_uid: Rc::new(RefCell::new(0)),
+ }
}
fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
- TyCtx { ctx: vec }
+ TyCtx {
+ ctx: vec,
+ next_uid: self.next_uid.clone(),
+ }
}
pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
let mut vec = self.ctx.clone();
@@ -63,7 +74,10 @@ impl TyCtx {
None
}
pub fn new_binder(&self, l: &Label) -> Binder {
- Binder::new(l.clone())
+ let mut next_uid = self.next_uid.borrow_mut();
+ let uid = *next_uid;
+ *next_uid += 1;
+ Binder::new(l.clone(), uid)
}
/// Given a var that makes sense in the current context, map the given function in such a way
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 {