Remove most reliance on types stored in Value

3 files changed, 53 insertions, 38 deletions

diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 0b22a8b..261e0b6 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, Value, ValueKind};
+use crate::semantics::{AlphaVar, Type, Value, ValueKind};
 
 #[derive(Debug, Clone, Copy, PartialEq, Eq)]
 pub(crate) enum NzVar {
@@ -11,9 +11,9 @@ pub(crate) enum NzVar {
 #[derive(Debug, Clone)]
 enum NzEnvItem {
     // Variable is bound with given type
-    Kept(Value),
+    Kept(Type),
     // Variable has been replaced by corresponding value
-    Replaced(Value),
+    Replaced(Value, Type),
 }
 
 #[derive(Debug, Clone)]
@@ -49,28 +49,31 @@ impl NzEnv {
         NzEnv { items: Vec::new() }
     }
 
-    pub fn insert_type(&self, t: Value) -> Self {
+    pub fn insert_type(&self, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Kept(t));
+        env.items.push(NzEnvItem::Kept(ty));
         env
     }
-    pub fn insert_value(&self, e: Value) -> Self {
+    pub fn insert_value(&self, e: Value, ty: Type) -> Self {
         let mut env = self.clone();
-        env.items.push(NzEnvItem::Replaced(e));
+        env.items.push(NzEnvItem::Replaced(e, ty));
         env
     }
+    pub fn insert_value_noty(&self, e: Value) -> Self {
+        let ty = e.get_type_not_sort();
+        self.insert_value(e, ty)
+    }
     pub fn lookup_val(&self, var: &AlphaVar) -> ValueKind {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
             NzEnvItem::Kept(_) => ValueKind::Var(NzVar::new(idx)),
-            NzEnvItem::Replaced(x) => x.kind().clone(),
+            NzEnvItem::Replaced(x, _) => x.kind().clone(),
         }
     }
     pub fn lookup_ty(&self, var: &AlphaVar) -> Value {
         let idx = self.items.len() - 1 - var.idx();
         match &self.items[idx] {
-            NzEnvItem::Kept(ty) => ty.clone(),
-            NzEnvItem::Replaced(x) => x.get_type().unwrap(),
+            NzEnvItem::Kept(ty) | NzEnvItem::Replaced(_, ty) => ty.clone(),
         }
     }
 }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index a00b7ff..3a981f4 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -17,14 +17,14 @@ pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueKind {
             closure.apply(a).to_whnf_check_type(ty)
         }
         ValueKind::AppliedBuiltin(closure) => {
-            closure.apply(a, f.get_type().unwrap(), ty)
+            closure.apply(a, f.get_type_not_sort(), ty)
         }
         ValueKind::UnionConstructor(l, kts, uniont) => ValueKind::UnionLit(
             l.clone(),
             a,
             kts.clone(),
             uniont.clone(),
-            f.get_type().unwrap(),
+            f.get_type_not_sort(),
         ),
         _ => ValueKind::PartialExpr(ExprKind::App(f, a)),
     }
@@ -349,7 +349,7 @@ pub(crate) fn normalize_one_layer(
             UnionType(kts) => Ret::ValueKind(UnionConstructor(
                 l.clone(),
                 kts.clone(),
-                v.get_type().unwrap(),
+                v.get_type_not_sort(),
             )),
             PartialExpr(ExprKind::BinOp(
                 BinOp::RightBiasedRecordMerge,
@@ -536,7 +536,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
         }
         TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
             let val = val.eval(env);
-            body.eval(&env.insert_value(val)).kind().clone()
+            body.eval(&env.insert_value_noty(val)).kind().clone()
         }
         TyExprKind::Expr(e) => {
             let ty = match tye.get_type() {
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 607aa0d..203b479 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -3,13 +3,11 @@ use std::rc::Rc;
 
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
-use crate::semantics::Binder;
 use crate::semantics::{
     apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    TyEnv,
+    type_of_builtin, type_with, typecheck, Binder, BuiltinClosure, NzEnv,
+    NzVar, TyEnv, TyExpr, TyExprKind, VarEnv,
 };
-use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
-use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
     NaiveDouble, Natural, Span,
@@ -119,11 +117,14 @@ impl Value {
         )
         .into_value()
     }
+    pub(crate) fn const_kind() -> Value {
+        Value::from_const(Const::Kind)
+    }
     /// Construct a Value from a completely unnormalized expression.
     pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
         ValueInternal::from_thunk(
             Thunk::new(env, tye.clone()),
-            tye.get_type().ok(),
+            Some(Value::const_kind()),
             tye.span().clone(),
         )
         .into_value()
@@ -137,24 +138,31 @@ impl Value {
         let env = NzEnv::new();
         ValueInternal::from_thunk(
             Thunk::from_partial_expr(env, e, ty.clone()),
-            Some(ty),
+            Some(Value::const_kind()),
             Span::Artificial,
         )
         .into_value()
     }
     /// Make a Value from a ValueKind
     pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
-        ValueInternal::from_whnf(v, Some(t), Span::Artificial).into_value()
+        ValueInternal::from_whnf(v, Some(Value::const_kind()), Span::Artificial)
+            .into_value()
     }
     pub(crate) fn from_const(c: Const) -> Self {
         let v = ValueKind::Const(c);
         match c {
-            Const::Type => {
-                Value::from_kind_and_type(v, Value::from_const(Const::Kind))
-            }
-            Const::Kind => {
-                Value::from_kind_and_type(v, Value::from_const(Const::Sort))
-            }
+            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(),
         }
     }
@@ -226,14 +234,10 @@ impl Value {
     }
 
     pub(crate) fn app(&self, v: Value) -> Value {
-        let body_t = match &*self.get_type_not_sort().kind() {
-            ValueKind::PiClosure { annot, closure, .. } => {
-                v.check_type(annot);
-                closure.apply(v.clone())
-            }
-            _ => unreachable!("Internal type error"),
-        };
-        Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
+        Value::from_kind_and_type(
+            apply_any(self.clone(), v, &Value::const_kind()),
+            Value::const_kind(),
+        )
     }
 
     /// In debug mode, panic if the provided type doesn't match the value's type.
@@ -246,12 +250,16 @@ impl Value {
         //     "Internal type error"
         // );
     }
-    pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
+    pub(crate) fn get_type(&self, tyenv: &TyEnv) -> Result<Value, TypeError> {
+        let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
+        type_with(tyenv, &expr).unwrap().get_type()
+    }
+    pub(crate) fn get_type_noenv(&self) -> Result<Value, TypeError> {
         Ok(self.0.get_type()?.clone())
     }
     /// When we know the value isn't `Sort`, this gets the type directly
     pub(crate) fn get_type_not_sort(&self) -> Value {
-        self.get_type()
+        self.get_type_noenv()
             .expect("Internal type error: value is `Sort` but shouldn't be")
     }
 
@@ -366,6 +374,10 @@ impl Value {
 
         TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
     }
+    pub fn to_tyexpr_tyenv(&self, tyenv: &TyEnv) -> TyExpr {
+        let expr = self.to_tyexpr(tyenv.as_varenv()).to_expr_tyenv(tyenv);
+        type_with(tyenv, &expr).unwrap()
+    }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
         self.to_tyexpr(VarEnv::new())
     }
@@ -522,7 +534,7 @@ impl Closure {
     pub fn apply(&self, val: Value) -> Value {
         match self {
             Closure::Closure { env, body, .. } => {
-                body.eval(&env.insert_value(val))
+                body.eval(&env.insert_value_noty(val))
             }
             Closure::ConstantClosure { body, .. } => body.clone(),
         }