summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/context.rs113
1 files changed, 38 insertions, 75 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 3c07c1c..36542d2 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -10,46 +10,46 @@ use crate::error::TypeError;
use crate::phase::{Type, Typed};
#[derive(Debug, Clone)]
-enum CtxItem<T> {
- Kept(AlphaVar, T),
- Replaced(Thunk, T),
+enum CtxItem {
+ Kept(AlphaVar, Type),
+ Replaced(Thunk, Type),
}
#[derive(Debug, Clone)]
-struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
+pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>);
-#[derive(Debug, Clone)]
-pub(crate) struct TypecheckContext(Context<Type>);
-
-impl<T> Context<T> {
+impl TypecheckContext {
pub fn new() -> Self {
- Context(Rc::new(Vec::new()))
+ TypecheckContext(Rc::new(Vec::new()))
}
- pub fn insert_kept(&self, x: &Label, t: T) -> Self
- where
- T: Shift + Clone,
- {
+ pub fn insert_type(&self, x: &Label, t: Type) -> Self {
let mut vec = self.0.as_ref().clone();
vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
- Context(Rc::new(vec))
+ TypecheckContext(Rc::new(vec))
}
- pub fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self
- where
- T: Clone,
- {
+ pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> {
let mut vec = self.0.as_ref().clone();
- vec.push((x.clone(), CtxItem::Replaced(th, t)));
- Context(Rc::new(vec))
+ vec.push((
+ x.clone(),
+ CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()),
+ ));
+ Ok(TypecheckContext(Rc::new(vec)))
}
- pub fn lookup(&self, var: &V<Label>) -> Result<CtxItem<T>, V<Label>>
- where
- T: Clone + Shift,
- {
+ pub fn lookup(&self, var: &V<Label>) -> Option<Typed> {
let mut var = var.clone();
let mut shift_map: HashMap<Label, _> = HashMap::new();
for (l, i) in self.0.iter().rev() {
match var.over_binder(l) {
- None => return Ok(i.under_multiple_binders(&shift_map)),
+ None => {
+ let i = i.under_multiple_binders(&shift_map);
+ let (th, t) = match i {
+ CtxItem::Kept(newvar, t) => {
+ (Value::Var(newvar).into_thunk(), t)
+ }
+ CtxItem::Replaced(th, t) => (th, t),
+ };
+ return Some(Typed::from_thunk_and_type(th, t));
+ }
Some(newvar) => var = newvar,
};
if let CtxItem::Kept(_, _) = i {
@@ -57,7 +57,7 @@ impl<T> Context<T> {
}
}
// Free variable
- Err(var)
+ None
}
/// Given a var that makes sense in the current context, map the given function in such a way
/// that the passed variable always makes sense in the context of the passed item.
@@ -66,11 +66,8 @@ impl<T> Context<T> {
fn do_with_var<E>(
&self,
var: &AlphaVar,
- mut f: impl FnMut(&AlphaVar, &CtxItem<T>) -> Result<CtxItem<T>, E>,
- ) -> Result<Self, E>
- where
- T: Clone,
- {
+ mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>,
+ ) -> Result<Self, E> {
let mut vec = Vec::new();
vec.reserve(self.0.len());
let mut var = var.clone();
@@ -88,16 +85,13 @@ impl<T> Context<T> {
vec.push((l.clone(), (*i).clone()));
}
vec.reverse();
- Ok(Context(Rc::new(vec)))
+ Ok(TypecheckContext(Rc::new(vec)))
}
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self>
- where
- T: Clone + Shift,
- {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
if delta < 0 {
Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?)
} else {
- Some(Context(Rc::new(
+ Some(TypecheckContext(Rc::new(
self.0
.iter()
.map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?)))
@@ -105,44 +99,13 @@ impl<T> Context<T> {
)))
}
}
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self
- where
- T: Clone + Subst<Typed>,
- {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
.unwrap()
}
}
-impl TypecheckContext {
- pub fn new() -> Self {
- TypecheckContext(Context::new())
- }
- pub fn insert_type(&self, x: &Label, t: Type) -> Self {
- TypecheckContext(self.0.insert_kept(x, t))
- }
- pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> {
- Ok(TypecheckContext(self.0.insert_replaced(
- x,
- e.to_thunk(),
- e.get_type()?.into_owned(),
- )))
- }
- pub fn lookup(&self, var: &V<Label>) -> Option<Typed> {
- match self.0.lookup(var) {
- Ok(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type(
- Thunk::from_value(Value::Var(newvar.clone())),
- t.clone(),
- )),
- Ok(CtxItem::Replaced(th, t)) => {
- Some(Typed::from_thunk_and_type(th.clone(), t.clone()))
- }
- Err(_) => None,
- }
- }
-}
-
-impl<T: Shift> Shift for CtxItem<T> {
+impl Shift for CtxItem {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
CtxItem::Kept(v, t) => {
@@ -155,13 +118,13 @@ impl<T: Shift> Shift for CtxItem<T> {
}
}
-impl<T: Clone + Shift> Shift for Context<T> {
+impl Shift for TypecheckContext {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
self.shift(delta, var)
}
}
-impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> {
+impl Subst<Typed> for CtxItem {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
CtxItem::Replaced(e, t) => CtxItem::Replaced(
@@ -178,16 +141,16 @@ impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> {
}
}
-impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> {
+impl Subst<Typed> for TypecheckContext {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
self.subst_shift(var, val)
}
}
+/// Don't count contexts when comparing stuff.
+/// This is dirty but needed.
impl PartialEq for TypecheckContext {
fn eq(&self, _: &Self) -> bool {
- // don't count contexts when comparing stuff
- // this is dirty but needed for now
true
}
}