Remove all types from Value

5 files changed, 16 insertions, 89 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index b1d12aa..9d4f8a2 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -370,17 +370,9 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
             }
             _ => Ret::DoneAsIs,
         },
-        (ListIndexed, [_, l]) => {
-            let l_whnf = l.kind();
-            match &*l_whnf {
+        (ListIndexed, [t, l]) => {
+            match l.kind() {
                 EmptyListLit(_) | NEListLit(_) => {
-                    // Extract the type of the list elements
-                    let t = match &*l_whnf {
-                        EmptyListLit(t) => t.clone(),
-                        NEListLit(xs) => xs[0].get_type_not_sort(),
-                        _ => unreachable!(),
-                    };
-
                     // Construct the returned record type: { index: Natural, value: t }
                     let mut kts = HashMap::new();
                     kts.insert("index".into(), Value::from_builtin(Natural));
@@ -388,7 +380,7 @@ fn apply_builtin(b: Builtin, args: Vec<Value>, env: NzEnv) -> ValueKind {
                     let t = Value::from_kind(RecordType(kts));
 
                     // Construct the new list, with added indices
-                    let list = match &*l_whnf {
+                    let list = match l.kind() {
                         EmptyListLit(_) => EmptyListLit(t),
                         NEListLit(xs) => NEListLit(
                             xs.iter()
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 80d17fb..28b38e3 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -79,8 +79,8 @@ impl Hir {
     }
     /// Eval a closed Hir fully and recursively (TODO: ish, need to fix under lambdas)
     pub fn rec_eval_closed_expr(&self) -> Value {
-        let mut val = self.eval_closed_expr();
-        val.normalize_mut();
+        let val = self.eval_closed_expr();
+        val.normalize();
         val
     }
 }
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 261e0b6..ff52343 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -60,7 +60,8 @@ impl NzEnv {
         env
     }
     pub fn insert_value_noty(&self, e: Value) -> Self {
-        let ty = e.get_type_not_sort();
+        // TODO
+        let ty = Value::const_sort();
         self.insert_value(e, ty)
     }
     pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 48acdb5..5a7b558 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 use std::rc::Rc;
 
-use crate::error::{TypeError, TypeMessage};
+use crate::error::TypeError;
 use crate::semantics::nze::lazy;
 use crate::semantics::{
     apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
@@ -25,8 +25,6 @@ pub(crate) struct Value(Rc<ValueInternal>);
 #[derive(Debug)]
 struct ValueInternal {
     kind: lazy::Lazy<Thunk, ValueKind>,
-    /// This is None if and only if `form` is `Sort` (which doesn't have a type)
-    ty: Option<Value>,
     span: Span,
 }
 
@@ -103,25 +101,12 @@ pub(crate) enum ValueKind {
 
 impl Value {
     pub(crate) fn const_sort() -> Value {
-        ValueInternal::from_whnf(
-            ValueKind::Const(Const::Sort),
-            None,
-            Span::Artificial,
-        )
-        .into_value()
-    }
-    pub(crate) fn const_kind() -> Value {
-        Value::from_const(Const::Kind)
+        Value::from_const(Const::Sort)
     }
     /// Construct a Value from a completely unnormalized expression.
     pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
         let span = hir.span();
-        ValueInternal::from_thunk(
-            Thunk::new(env, hir),
-            Some(Value::const_kind()),
-            span,
-        )
-        .into_value()
+        ValueInternal::from_thunk(Thunk::new(env, hir), span).into_value()
     }
     /// Construct a Value from a partially normalized expression that's not in WHNF.
     pub(crate) fn from_partial_expr(e: ExprKind<Value, Normalized>) -> Value {
@@ -129,33 +114,17 @@ impl Value {
         let env = NzEnv::new();
         ValueInternal::from_thunk(
             Thunk::from_partial_expr(env, e),
-            Some(Value::const_kind()),
             Span::Artificial,
         )
         .into_value()
     }
     /// Make a Value from a ValueKind
     pub(crate) fn from_kind(v: ValueKind) -> Value {
-        ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
-            .into_value()
+        ValueInternal::from_whnf(v, Span::Artificial).into_value()
     }
     pub(crate) fn from_const(c: Const) -> Self {
         let v = ValueKind::Const(c);
-        match c {
-            Const::Type => ValueInternal::from_whnf(
-                v,
-                Some(Value::from_const(Const::Kind)),
-                Span::Artificial,
-            )
-            .into_value(),
-            Const::Kind => ValueInternal::from_whnf(
-                v,
-                Some(Value::const_sort()),
-                Span::Artificial,
-            )
-            .into_value(),
-            Const::Sort => Value::const_sort(),
-        }
+        ValueInternal::from_whnf(v, Span::Artificial).into_value()
     }
     pub(crate) fn from_builtin(b: Builtin) -> Self {
         Self::from_builtin_env(b, &NzEnv::new())
@@ -193,16 +162,6 @@ impl Value {
         self.to_hir(env.as_varenv()).to_expr_tyenv(env)
     }
 
-    /// Normalizes contents to normal form; faster than `normalize` if
-    /// no one else shares this.
-    pub(crate) fn normalize_mut(&mut self) {
-        match Rc::get_mut(&mut self.0) {
-            // Mutate directly if sole owner
-            Some(vint) => vint.normalize_mut(),
-            // Otherwise mutate through the refcell
-            None => self.normalize(),
-        }
-    }
     pub(crate) fn normalize(&self) {
         self.0.normalize()
     }
@@ -214,13 +173,6 @@ impl Value {
     pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
         self.to_tyexpr_tyenv(tyenv).get_type()
     }
-    /// When we know the value isn't `Sort`, this gets the type directly
-    pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.0
-            .get_type()
-            .expect("Internal type error: value is `Sort` but shouldn't be")
-            .clone()
-    }
 
     pub fn to_hir(&self, venv: VarEnv) -> Hir {
         let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
@@ -340,17 +292,15 @@ impl Value {
 }
 
 impl ValueInternal {
-    fn from_whnf(k: ValueKind, ty: Option<Value>, span: Span) -> Self {
+    fn from_whnf(k: ValueKind, span: Span) -> Self {
         ValueInternal {
             kind: lazy::Lazy::new_completed(k),
-            ty,
             span,
         }
     }
-    fn from_thunk(th: Thunk, ty: Option<Value>, span: Span) -> Self {
+    fn from_thunk(th: Thunk, span: Span) -> Self {
         ValueInternal {
             kind: lazy::Lazy::new(th),
-            ty,
             span,
         }
     }
@@ -364,17 +314,6 @@ impl ValueInternal {
     fn normalize(&self) {
         self.kind().normalize();
     }
-    // TODO: deprecated
-    fn normalize_mut(&mut self) {
-        self.normalize();
-    }
-
-    fn get_type(&self) -> Result<&Value, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t),
-            None => Err(TypeError::new(TypeMessage::Sort)),
-        }
-    }
 }
 
 impl ValueKind {
@@ -616,11 +555,6 @@ impl std::fmt::Debug for Value {
         }
         let mut x = fmt.debug_struct(&format!("Value@WHNF"));
         x.field("kind", kind);
-        if let Some(ty) = vint.ty.as_ref() {
-            x.field("type", &ty);
-        } else {
-            x.field("type", &None::<()>);
-        }
         x.finish()
     }
 }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 29099c5..05fa4b5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -66,8 +66,8 @@ impl TyExpr {
     }
     /// Eval a closed TyExpr fully and recursively;
     pub fn rec_eval_closed_expr(&self) -> Value {
-        let mut val = self.eval_closed_expr();
-        val.normalize_mut();
+        let val = self.eval_closed_expr();
+        val.normalize();
         val
     }
 }