From ba19f41873fec98bb24ba709f4b76c3f58ca5aaa Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 15 Aug 2019 13:05:23 +0200
Subject: Fix bug in shifting contexts

---
 dhall/src/core/context.rs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 62affcf..8d14415 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -97,7 +97,16 @@ impl<T> Context<T> {
     where
         T: Clone + Shift,
     {
-        Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?)
+        if delta < 0 {
+            Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?)
+        } else {
+            Some(Context(Rc::new(
+                self.0
+                    .iter()
+                    .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?)))
+                    .collect::<Result<_, _>>()?,
+            )))
+        }
     }
     fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self
     where
-- 
cgit v1.2.3


From 88ebc0f9d561a2541aad84a3152511a0439db8b4 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 16 Aug 2019 17:56:19 +0200
Subject: Reduce api surface of dhall crate

Helps detect unused code
---
 dhall/src/core/context.rs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 8d14415..9230a2e 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -10,19 +10,19 @@ use crate::error::TypeError;
 use crate::phase::{Type, Typed};
 
 #[derive(Debug, Clone)]
-pub enum CtxItem<T> {
+enum CtxItem<T> {
     Kept(AlphaVar, T),
     Replaced(Thunk, T),
 }
 
 #[derive(Debug, Clone)]
-pub struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
+struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
 
 #[derive(Debug, Clone)]
-pub struct NormalizationContext(Context<()>);
+pub(crate) struct NormalizationContext(Context<()>);
 
 #[derive(Debug, Clone)]
-pub struct TypecheckContext(Context<Type>);
+pub(crate) struct TypecheckContext(Context<Type>);
 
 impl<T> Context<T> {
     pub fn new() -> Self {
-- 
cgit v1.2.3


From 5f0d69671b44ba1dff6becb9ebc7f6e74241e3e2 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 16 Aug 2019 18:14:55 +0200
Subject: Remove dead code

---
 dhall/src/core/context.rs | 31 -------------------------------
 1 file changed, 31 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 9230a2e..3c07c1c 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -18,9 +18,6 @@ enum CtxItem<T> {
 #[derive(Debug, Clone)]
 struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>);
 
-#[derive(Debug, Clone)]
-pub(crate) struct NormalizationContext(Context<()>);
-
 #[derive(Debug, Clone)]
 pub(crate) struct TypecheckContext(Context<Type>);
 
@@ -117,22 +114,6 @@ impl<T> Context<T> {
     }
 }
 
-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())
@@ -180,12 +161,6 @@ impl<T: Clone + Shift> Shift for Context<T> {
     }
 }
 
-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 {
         match self {
@@ -209,12 +184,6 @@ impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> {
     }
 }
 
-impl Subst<Typed> for NormalizationContext {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
-        NormalizationContext(self.0.subst_shift(var, val))
-    }
-}
-
 impl PartialEq for TypecheckContext {
     fn eq(&self, _: &Self) -> bool {
         // don't count contexts when comparing stuff
-- 
cgit v1.2.3


From 1741bb9e3fe872b3b841a9f394de69c85f523ba5 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 16 Aug 2019 18:34:05 +0200
Subject: No need for generic Context anymore

---
 dhall/src/core/context.rs | 113 ++++++++++++++++------------------------------
 1 file changed, 38 insertions(+), 75 deletions(-)

(limited to 'dhall/src/core/context.rs')

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
     }
 }
-- 
cgit v1.2.3


From fcc9afb3624883c4f99320c37678b7f9d338630d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 16 Aug 2019 18:41:19 +0200
Subject: fixup! No need for generic Context anymore

---
 dhall/src/core/context.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 36542d2..cc25749 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -56,7 +56,7 @@ impl TypecheckContext {
                 *shift_map.entry(l.clone()).or_insert(0) += 1;
             }
         }
-        // Free variable
+        // Unbound variable
         None
     }
     /// Given a var that makes sense in the current context, map the given function in such a way
-- 
cgit v1.2.3


From e0f5216215ccb7a4df85d80e11dd265cdb52a44f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 16 Aug 2019 19:47:36 +0200
Subject: s/Value/ValueF/

---
 dhall/src/core/context.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index cc25749..b1fbde9 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
 use dhall_syntax::{Label, V};
 
 use crate::core::thunk::Thunk;
-use crate::core::value::Value;
+use crate::core::value::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 use crate::phase::{Type, Typed};
@@ -44,7 +44,7 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     let (th, t) = match i {
                         CtxItem::Kept(newvar, t) => {
-                            (Value::Var(newvar).into_thunk(), t)
+                            (ValueF::Var(newvar).into_thunk(), t)
                         }
                         CtxItem::Replaced(th, t) => (th, t),
                     };
-- 
cgit v1.2.3


From 6753a1f97bb674d91dd4d42f2ddb25a8119e070d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 17 Aug 2019 19:00:43 +0200
Subject: s/Thunk/Value/

---
 dhall/src/core/context.rs | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index b1fbde9..e1a23a9 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,8 +3,8 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::thunk::Thunk;
-use crate::core::value::ValueF;
+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};
@@ -12,7 +12,7 @@ use crate::phase::{Type, Typed};
 #[derive(Debug, Clone)]
 enum CtxItem {
     Kept(AlphaVar, Type),
-    Replaced(Thunk, Type),
+    Replaced(Value, Type),
 }
 
 #[derive(Debug, Clone)]
@@ -31,7 +31,7 @@ impl TypecheckContext {
         let mut vec = self.0.as_ref().clone();
         vec.push((
             x.clone(),
-            CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()),
+            CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()),
         ));
         Ok(TypecheckContext(Rc::new(vec)))
     }
@@ -44,11 +44,11 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     let (th, t) = match i {
                         CtxItem::Kept(newvar, t) => {
-                            (ValueF::Var(newvar).into_thunk(), t)
+                            (ValueF::Var(newvar).into_value(), t)
                         }
                         CtxItem::Replaced(th, t) => (th, t),
                     };
-                    return Some(Typed::from_thunk_and_type(th, t));
+                    return Some(Typed::from_value_and_type(th, t));
                 }
                 Some(newvar) => var = newvar,
             };
@@ -133,7 +133,7 @@ impl Subst<Typed> for CtxItem {
             ),
             CtxItem::Kept(v, t) => match v.shift(-1, var) {
                 None => {
-                    CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val))
+                    CtxItem::Replaced(val.to_value(), t.subst_shift(var, val))
                 }
                 Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
             },
-- 
cgit v1.2.3


From 26a1fd0f0861038a76a0f9b09eaef16d808d4139 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 19 Aug 2019 21:52:26 +0200
Subject: Use TypedValue instead of Typed in normalize and typecheck

Now Typed is only used in dhall::phase, similarly to
Parsed/Resolved/Normalized
---
 dhall/src/core/context.rs | 29 ++++++++++++++++-------------
 1 file changed, 16 insertions(+), 13 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index e1a23a9..851e4c4 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,16 +3,15 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::value::Value;
+use crate::core::value::{TypedValue, 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 {
-    Kept(AlphaVar, Type),
-    Replaced(Value, Type),
+    Kept(AlphaVar, TypedValue),
+    Replaced(Value, TypedValue),
 }
 
 #[derive(Debug, Clone)]
@@ -22,12 +21,16 @@ impl TypecheckContext {
     pub fn new() -> Self {
         TypecheckContext(Rc::new(Vec::new()))
     }
-    pub fn insert_type(&self, x: &Label, t: Type) -> Self {
+    pub fn insert_type(&self, x: &Label, t: TypedValue) -> Self {
         let mut vec = self.0.as_ref().clone();
         vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x))));
         TypecheckContext(Rc::new(vec))
     }
-    pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> {
+    pub fn insert_value(
+        &self,
+        x: &Label,
+        e: TypedValue,
+    ) -> Result<Self, TypeError> {
         let mut vec = self.0.as_ref().clone();
         vec.push((
             x.clone(),
@@ -35,7 +38,7 @@ impl TypecheckContext {
         ));
         Ok(TypecheckContext(Rc::new(vec)))
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<Typed> {
+    pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
         let mut var = var.clone();
         let mut shift_map: HashMap<Label, _> = HashMap::new();
         for (l, i) in self.0.iter().rev() {
@@ -48,7 +51,7 @@ impl TypecheckContext {
                         }
                         CtxItem::Replaced(th, t) => (th, t),
                     };
-                    return Some(Typed::from_value_and_type(th, t));
+                    return Some(TypedValue::from_value_and_type(th, t));
                 }
                 Some(newvar) => var = newvar,
             };
@@ -99,7 +102,7 @@ impl TypecheckContext {
             )))
         }
     }
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
         self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
             .unwrap()
     }
@@ -124,8 +127,8 @@ impl Shift for TypecheckContext {
     }
 }
 
-impl Subst<Typed> for CtxItem {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for CtxItem {
+    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
         match self {
             CtxItem::Replaced(e, t) => CtxItem::Replaced(
                 e.subst_shift(var, val),
@@ -141,8 +144,8 @@ impl Subst<Typed> for CtxItem {
     }
 }
 
-impl Subst<Typed> for TypecheckContext {
-    fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+impl Subst<TypedValue> for TypecheckContext {
+    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
         self.subst_shift(var, val)
     }
 }
-- 
cgit v1.2.3


From 07a276c1d6ee892b93abbd7a73c78c96d56f4fe7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 19 Aug 2019 22:26:17 +0200
Subject: Reduce untyped construction of Values

---
 dhall/src/core/context.rs | 34 +++++++++++++---------------------
 1 file changed, 13 insertions(+), 21 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index 851e4c4..deabe44 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,7 +3,7 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::value::{TypedValue, Value};
+use crate::core::value::TypedValue;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
@@ -11,7 +11,7 @@ use crate::error::TypeError;
 #[derive(Debug, Clone)]
 enum CtxItem {
     Kept(AlphaVar, TypedValue),
-    Replaced(Value, TypedValue),
+    Replaced(TypedValue),
 }
 
 #[derive(Debug, Clone)]
@@ -32,10 +32,7 @@ impl TypecheckContext {
         e: TypedValue,
     ) -> Result<Self, TypeError> {
         let mut vec = self.0.as_ref().clone();
-        vec.push((
-            x.clone(),
-            CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()),
-        ));
+        vec.push((x.clone(), CtxItem::Replaced(e)));
         Ok(TypecheckContext(Rc::new(vec)))
     }
     pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
@@ -45,13 +42,15 @@ impl TypecheckContext {
             match var.over_binder(l) {
                 None => {
                     let i = i.under_multiple_binders(&shift_map);
-                    let (th, t) = match i {
+                    return Some(match i {
                         CtxItem::Kept(newvar, t) => {
-                            (ValueF::Var(newvar).into_value(), t)
+                            TypedValue::from_valuef_and_type(
+                                ValueF::Var(newvar),
+                                t,
+                            )
                         }
-                        CtxItem::Replaced(th, t) => (th, t),
-                    };
-                    return Some(TypedValue::from_value_and_type(th, t));
+                        CtxItem::Replaced(v) => v,
+                    });
                 }
                 Some(newvar) => var = newvar,
             };
@@ -114,9 +113,7 @@ impl Shift for CtxItem {
             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)?),
         })
     }
 }
@@ -130,14 +127,9 @@ impl Shift for TypecheckContext {
 impl Subst<TypedValue> for CtxItem {
     fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> 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_value(), t.subst_shift(var, val))
-                }
+                None => CtxItem::Replaced(val.clone()),
                 Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
             },
         }
-- 
cgit v1.2.3


From 730f2ebb146792994c7492b6c05f7d09d42cbccf Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 19 Aug 2019 23:00:49 +0200
Subject: Merge TypedValue and Value

---
 dhall/src/core/context.rs | 31 ++++++++++++-------------------
 1 file changed, 12 insertions(+), 19 deletions(-)

(limited to 'dhall/src/core/context.rs')

diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index deabe44..2bf39c5 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,15 +3,15 @@ use std::rc::Rc;
 
 use dhall_syntax::{Label, V};
 
-use crate::core::value::TypedValue;
+use crate::core::value::Value;
 use crate::core::valuef::ValueF;
 use crate::core::var::{AlphaVar, Shift, Subst};
 use crate::error::TypeError;
 
 #[derive(Debug, Clone)]
 enum CtxItem {
-    Kept(AlphaVar, TypedValue),
-    Replaced(TypedValue),
+    Kept(AlphaVar, Value),
+    Replaced(Value),
 }
 
 #[derive(Debug, Clone)]
@@ -21,21 +21,17 @@ impl TypecheckContext {
     pub fn new() -> Self {
         TypecheckContext(Rc::new(Vec::new()))
     }
-    pub fn insert_type(&self, x: &Label, t: TypedValue) -> Self {
+    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))));
         TypecheckContext(Rc::new(vec))
     }
-    pub fn insert_value(
-        &self,
-        x: &Label,
-        e: TypedValue,
-    ) -> Result<Self, TypeError> {
+    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(e)));
         Ok(TypecheckContext(Rc::new(vec)))
     }
-    pub fn lookup(&self, var: &V<Label>) -> Option<TypedValue> {
+    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() {
@@ -44,10 +40,7 @@ impl TypecheckContext {
                     let i = i.under_multiple_binders(&shift_map);
                     return Some(match i {
                         CtxItem::Kept(newvar, t) => {
-                            TypedValue::from_valuef_and_type(
-                                ValueF::Var(newvar),
-                                t,
-                            )
+                            Value::from_valuef_and_type(ValueF::Var(newvar), t)
                         }
                         CtxItem::Replaced(v) => v,
                     });
@@ -101,7 +94,7 @@ impl TypecheckContext {
             )))
         }
     }
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val)))
             .unwrap()
     }
@@ -124,8 +117,8 @@ impl Shift for TypecheckContext {
     }
 }
 
-impl Subst<TypedValue> for CtxItem {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for CtxItem {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         match self {
             CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)),
             CtxItem::Kept(v, t) => match v.shift(-1, var) {
@@ -136,8 +129,8 @@ impl Subst<TypedValue> for CtxItem {
     }
 }
 
-impl Subst<TypedValue> for TypecheckContext {
-    fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self {
+impl Subst<Value> for TypecheckContext {
+    fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
         self.subst_shift(var, val)
     }
 }
-- 
cgit v1.2.3