1 files changed, 41 insertions, 121 deletions

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 9230a2e..2bf39c5 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,64 +3,56 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::thunk::Thunk;
 use crate::core::value::Value;
+use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 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, Value),
+    Replaced(Value),
 }
 
 #[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 NormalizationContext(Context<()>);
-
-#[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: Value) -> 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: Value) -> 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)));
+        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<Value> {
         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);
+                    return Some(match i {
+                        CtxItem::Kept(newvar, t) => {
+                            Value::from_valuef_and_type(ValueF::Var(newvar), t)
+                        }
+                        CtxItem::Replaced(v) => v,
+                    });
+                }
                 Some(newvar) => var = newvar,
             };
             if let CtxItem::Kept(_, _) = i {
                 *shift_map.entry(l.clone()).or_insert(0) += 1;
             }
         }
-        // Free variable
-        Err(var)
+        // Unbound variable
+        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.
@@ -69,11 +61,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();
@@ -91,16 +80,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)?)))
@@ -108,117 +94,51 @@ 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: &Value) -> Self {
         self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
             .unwrap()
     }
 }
 
-impl NormalizationContext {
-    pub fn new() -> Self {
-        NormalizationContext(Context::new())
-    }
-    pub fn skip(&self, x: &Label) -> Self {
-        NormalizationContext(self.0.insert_kept(x, ()))
-    }
-    pub fn lookup(&self, var: &V<Label>) -> Value {
-        match self.0.lookup(var) {
-            Ok(CtxItem::Replaced(t, ())) => t.to_value(),
-            Ok(CtxItem::Kept(newvar, ())) => Value::Var(newvar.clone()),
-            Err(var) => Value::Var(AlphaVar::from_var(var)),
-        }
-    }
-}
-
-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) => {
                 CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?)
             }
-            CtxItem::Replaced(e, t) => {
-                CtxItem::Replaced(e.shift(delta, var)?, t.shift(delta, var)?)
-            }
+            CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?),
         })
     }
 }
 
-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 Shift for NormalizationContext {
-    fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
-        Some(NormalizationContext(self.0.shift(delta, var)?))
-    }
-}
-
-impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Value> for CtxItem {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
-            CtxItem::Replaced(e, t) => CtxItem::Replaced(
-                e.subst_shift(var, val),
-                t.subst_shift(var, val),
-            ),
+            CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
             CtxItem::Kept(v, t) => match v.shift(-1, var) {
-                None => {
-                    CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val))
-                }
+                None => CtxItem::Replaced(val.clone()),
                 Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
             },
         }
     }
 }
 
-impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<Value> for TypecheckContext {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         self.subst_shift(var, val)
     }
 }
 
-impl Subst<Typed> for NormalizationContext {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        NormalizationContext(self.0.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
     }
 }