Remove most TyExpr from normalization

7 files changed, 80 insertions, 108 deletions

diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index a513967..423364d 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -1,5 +1,5 @@
 use crate::semantics::{
-    typecheck, NzEnv, TyExpr, TyExprKind, Value, ValueKind, VarEnv,
+    typecheck, Hir, HirKind, NzEnv, Value, ValueKind, VarEnv,
 };
 use crate::syntax::map::DupTreeMap;
 use crate::syntax::Const::Type;
@@ -48,17 +48,13 @@ impl BuiltinClosure<Value> {
             x.normalize();
         }
     }
-    pub fn to_tyexprkind(&self, venv: VarEnv) -> TyExprKind {
-        TyExprKind::Expr(self.args.iter().zip(self.types.iter()).fold(
+    pub fn to_hirkind(&self, venv: VarEnv) -> HirKind {
+        HirKind::Expr(self.args.iter().zip(self.types.iter()).fold(
             ExprKind::Builtin(self.b),
             |acc, (v, ty)| {
                 ExprKind::App(
-                    TyExpr::new(
-                        TyExprKind::Expr(acc),
-                        Some(ty.clone()),
-                        Span::Artificial,
-                    ),
-                    v.to_tyexpr(venv),
+                    Hir::new(HirKind::Expr(acc), Span::Artificial),
+                    v.to_hir(venv),
                 )
             },
         ))
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 2784ecb..683dbbb 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -62,8 +62,7 @@ impl Hir {
 
     /// Eval the Hir. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: &NzEnv) -> Value {
-        // Value::new_thunk(env, self.clone())
-        todo!()
+        Value::new_thunk(env, self.clone())
     }
     /// Eval a closed Hir (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index b5949f5..acb2e51 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -3,8 +3,7 @@ use std::collections::HashMap;
 
 use crate::semantics::NzEnv;
 use crate::semantics::{
-    Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, TyExpr, TyExprKind,
-    Value, ValueKind,
+    Binder, BuiltinClosure, Closure, Hir, HirKind, TextLit, Value, ValueKind,
 };
 use crate::syntax::{BinOp, Builtin, ExprKind, InterpolatedTextContents};
 use crate::Normalized;
@@ -460,11 +459,11 @@ pub(crate) fn normalize_one_layer(
     }
 }
 
-/// Normalize a TyExpr into WHNF
-pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
-    match tye.kind() {
-        TyExprKind::Var(var) => env.lookup_val(var),
-        TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => {
+/// Normalize Hir into WHNF
+pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> ValueKind {
+    match hir.kind() {
+        HirKind::Var(var) => env.lookup_val(var),
+        HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             ValueKind::LamClosure {
                 binder: Binder::new(binder.clone()),
@@ -472,7 +471,7 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
                 closure: Closure::new(env, body.clone()),
             }
         }
-        TyExprKind::Expr(ExprKind::Pi(binder, annot, body)) => {
+        HirKind::Expr(ExprKind::Pi(binder, annot, body)) => {
             let annot = annot.eval(env);
             ValueKind::PiClosure {
                 binder: Binder::new(binder.clone()),
@@ -480,12 +479,12 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> ValueKind {
                 closure: Closure::new(env, body.clone()),
             }
         }
-        TyExprKind::Expr(ExprKind::Let(_, None, val, body)) => {
+        HirKind::Expr(ExprKind::Let(_, None, val, body)) => {
             let val = val.eval(env);
             body.eval(&env.insert_value_noty(val)).kind().clone()
         }
-        TyExprKind::Expr(e) => {
-            let e = e.map_ref(|tye| tye.eval(env));
+        HirKind::Expr(e) => {
+            let e = e.map_ref(|hir| hir.eval(env));
             normalize_one_layer(e, env)
         }
     }
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index d4213bc..d05c545 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -4,9 +4,9 @@ use std::rc::Rc;
 use crate::error::{TypeError, TypeMessage};
 use crate::semantics::nze::lazy;
 use crate::semantics::{
-    apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
-    type_with, Binder, BuiltinClosure, Hir, NzEnv, NzVar, TyEnv, TyExpr,
-    TyExprKind, VarEnv,
+    apply_any, normalize_hir_whnf, normalize_one_layer, squash_textlit,
+    type_with, Binder, BuiltinClosure, Hir, HirKind, NzEnv, NzVar, TyEnv,
+    TyExpr, VarEnv,
 };
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -34,7 +34,7 @@ struct ValueInternal {
 #[derive(Debug, Clone)]
 pub(crate) enum Thunk {
     /// A completely unnormalized expression.
-    Thunk { env: NzEnv, body: TyExpr },
+    Thunk { env: NzEnv, body: Hir },
     /// A partially normalized expression that may need to go through `normalize_one_layer`.
     PartialExpr {
         env: NzEnv,
@@ -46,7 +46,7 @@ pub(crate) enum Thunk {
 #[derive(Debug, Clone)]
 pub(crate) enum Closure {
     /// Normal closure
-    Closure { env: NzEnv, body: TyExpr },
+    Closure { env: NzEnv, body: Hir },
     /// Closure that ignores the argument passed
     ConstantClosure { body: Value },
 }
@@ -116,11 +116,12 @@ impl Value {
         Value::from_const(Const::Kind)
     }
     /// Construct a Value from a completely unnormalized expression.
-    pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
+    pub(crate) fn new_thunk(env: &NzEnv, hir: Hir) -> Value {
+        let span = hir.span();
         ValueInternal::from_thunk(
-            Thunk::new(env, tye.clone()),
+            Thunk::new(env, hir),
             Some(Value::const_kind()),
-            tye.span().clone(),
+            span,
         )
         .into_value()
     }
@@ -176,13 +177,8 @@ impl Value {
             _ => None,
         }
     }
-    // pub(crate) fn span(&self) -> Span {
-    //     self.0.span.clone()
-    // }
 
     /// This is what you want if you want to pattern-match on the value.
-    /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut
-    /// panics.
     pub(crate) fn kind(&self) -> &ValueKind {
         self.0.kind()
     }
@@ -196,7 +192,7 @@ impl Value {
         self.to_tyexpr_noenv().to_expr(opts)
     }
     pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+        self.to_hir(env.as_varenv()).to_expr_tyenv(env)
     }
 
     /// Normalizes contents to normal form; faster than `normalize` if
@@ -218,8 +214,7 @@ impl Value {
     }
 
     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()
+        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 {
@@ -229,21 +224,21 @@ impl Value {
             .clone()
     }
 
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
         let map_uniontype = |kts: &HashMap<Label, Option<Value>>| {
             ExprKind::UnionType(
                 kts.iter()
                     .map(|(k, v)| {
-                        (k.clone(), v.as_ref().map(|v| v.to_tyexpr(venv)))
+                        (k.clone(), v.as_ref().map(|v| v.to_hir(venv)))
                     })
                     .collect(),
             )
         };
 
-        let tye = match &*self.kind() {
-            ValueKind::Var(v) => TyExprKind::Var(venv.lookup(v)),
-            ValueKind::AppliedBuiltin(closure) => closure.to_tyexprkind(venv),
-            self_kind => TyExprKind::Expr(match self_kind {
+        let hir = match &*self.kind() {
+            ValueKind::Var(v) => HirKind::Var(venv.lookup(v)),
+            ValueKind::AppliedBuiltin(closure) => closure.to_hirkind(venv),
+            self_kind => HirKind::Expr(match self_kind {
                 ValueKind::Var(..) | ValueKind::AppliedBuiltin(..) => {
                     unreachable!()
                 }
@@ -253,8 +248,8 @@ impl Value {
                     closure,
                 } => ExprKind::Lam(
                     binder.to_label(),
-                    annot.to_tyexpr(venv),
-                    closure.to_tyexpr(venv),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
                 ),
                 ValueKind::PiClosure {
                     binder,
@@ -262,8 +257,8 @@ impl Value {
                     closure,
                 } => ExprKind::Pi(
                     binder.to_label(),
-                    annot.to_tyexpr(venv),
-                    closure.to_tyexpr(venv),
+                    annot.to_hir(venv),
+                    closure.to_hir(venv),
                 ),
                 ValueKind::Const(c) => ExprKind::Const(*c),
                 ValueKind::BoolLit(b) => ExprKind::BoolLit(*b),
@@ -271,81 +266,75 @@ impl Value {
                 ValueKind::IntegerLit(n) => ExprKind::IntegerLit(*n),
                 ValueKind::DoubleLit(n) => ExprKind::DoubleLit(*n),
                 ValueKind::EmptyOptionalLit(n) => ExprKind::App(
-                    Value::from_builtin(Builtin::OptionalNone).to_tyexpr(venv),
-                    n.to_tyexpr(venv),
+                    Value::from_builtin(Builtin::OptionalNone).to_hir(venv),
+                    n.to_hir(venv),
                 ),
                 ValueKind::NEOptionalLit(n) => {
-                    ExprKind::SomeLit(n.to_tyexpr(venv))
-                }
-                ValueKind::EmptyListLit(n) => {
-                    ExprKind::EmptyListLit(TyExpr::new(
-                        TyExprKind::Expr(ExprKind::App(
-                            Value::from_builtin(Builtin::List).to_tyexpr(venv),
-                            n.to_tyexpr(venv),
-                        )),
-                        Some(Value::from_const(Const::Type)),
-                        Span::Artificial,
-                    ))
+                    ExprKind::SomeLit(n.to_hir(venv))
                 }
+                ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(Hir::new(
+                    HirKind::Expr(ExprKind::App(
+                        Value::from_builtin(Builtin::List).to_hir(venv),
+                        n.to_hir(venv),
+                    )),
+                    Span::Artificial,
+                )),
                 ValueKind::NEListLit(elts) => ExprKind::NEListLit(
-                    elts.iter().map(|v| v.to_tyexpr(venv)).collect(),
+                    elts.iter().map(|v| v.to_hir(venv)).collect(),
                 ),
                 ValueKind::TextLit(elts) => ExprKind::TextLit(
                     elts.iter()
-                        .map(|t| t.map_ref(|v| v.to_tyexpr(venv)))
+                        .map(|t| t.map_ref(|v| v.to_hir(venv)))
                         .collect(),
                 ),
                 ValueKind::RecordLit(kvs) => ExprKind::RecordLit(
                     kvs.iter()
-                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
                         .collect(),
                 ),
                 ValueKind::RecordType(kts) => ExprKind::RecordType(
                     kts.iter()
-                        .map(|(k, v)| (k.clone(), v.to_tyexpr(venv)))
+                        .map(|(k, v)| (k.clone(), v.to_hir(venv)))
                         .collect(),
                 ),
                 ValueKind::UnionType(kts) => map_uniontype(kts),
                 ValueKind::UnionConstructor(l, kts, t) => ExprKind::Field(
-                    TyExpr::new(
-                        TyExprKind::Expr(map_uniontype(kts)),
-                        Some(t.clone()),
+                    Hir::new(
+                        HirKind::Expr(map_uniontype(kts)),
                         Span::Artificial,
                     ),
                     l.clone(),
                 ),
                 ValueKind::UnionLit(l, v, kts, uniont, ctort) => ExprKind::App(
-                    TyExpr::new(
-                        TyExprKind::Expr(ExprKind::Field(
-                            TyExpr::new(
-                                TyExprKind::Expr(map_uniontype(kts)),
-                                Some(uniont.clone()),
+                    Hir::new(
+                        HirKind::Expr(ExprKind::Field(
+                            Hir::new(
+                                HirKind::Expr(map_uniontype(kts)),
                                 Span::Artificial,
                             ),
                             l.clone(),
                         )),
-                        Some(ctort.clone()),
                         Span::Artificial,
                     ),
-                    v.to_tyexpr(venv),
+                    v.to_hir(venv),
                 ),
                 ValueKind::Equivalence(x, y) => ExprKind::BinOp(
                     BinOp::Equivalence,
-                    x.to_tyexpr(venv),
-                    y.to_tyexpr(venv),
+                    x.to_hir(venv),
+                    y.to_hir(venv),
                 ),
-                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_tyexpr(venv)),
+                ValueKind::PartialExpr(e) => e.map_ref(|v| v.to_hir(venv)),
             }),
         };
 
-        TyExpr::new(tye, self.0.ty.clone(), self.0.span.clone())
+        Hir::new(hir, 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);
+        let expr = self.to_hir(tyenv.as_varenv()).to_expr_tyenv(tyenv);
         type_with(tyenv, &expr).unwrap()
     }
     pub fn to_tyexpr_noenv(&self) -> TyExpr {
-        self.to_tyexpr(VarEnv::new())
+        self.to_tyexpr_tyenv(&TyEnv::new())
     }
 }
 
@@ -461,7 +450,7 @@ impl ValueKind {
 }
 
 impl Thunk {
-    fn new(env: &NzEnv, body: TyExpr) -> Self {
+    fn new(env: &NzEnv, body: Hir) -> Self {
         Thunk::Thunk {
             env: env.clone(),
             body,
@@ -475,14 +464,14 @@ impl Thunk {
     }
     fn eval(self) -> ValueKind {
         match self {
-            Thunk::Thunk { env, body } => normalize_tyexpr_whnf(&body, &env),
+            Thunk::Thunk { env, body } => normalize_hir_whnf(&env, &body),
             Thunk::PartialExpr { env, expr } => normalize_one_layer(expr, &env),
         }
     }
 }
 
 impl Closure {
-    pub fn new(env: &NzEnv, body: TyExpr) -> Self {
+    pub fn new(env: &NzEnv, body: Hir) -> Self {
         Closure::Closure {
             env: env.clone(),
             body,
@@ -512,10 +501,11 @@ impl Closure {
 
     // TODO: somehow normalize the body. Might require to pass an env.
     pub fn normalize(&self) {}
-    /// Convert this closure to a TyExpr
-    pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
+
+    /// Convert this closure to a Hir expression
+    pub fn to_hir(&self, venv: VarEnv) -> Hir {
         self.apply_var(NzVar::new(venv.size()))
-            .to_tyexpr(venv.insert())
+            .to_hir(venv.insert())
     }
     /// If the closure variable is free in the closure, return Err. Otherwise, return the value
     /// with that free variable remove.
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index b3e7895..af955f4 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -21,9 +21,9 @@ pub(crate) struct TyEnv {
 }
 
 impl VarEnv {
-    pub fn new() -> Self {
-        VarEnv { size: 0 }
-    }
+    // pub fn new() -> Self {
+    //     VarEnv { size: 0 }
+    // }
     pub fn size(&self) -> usize {
         self.size
     }
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index fa578c0..29099c5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,8 +1,6 @@
 use crate::error::{TypeError, TypeMessage};
-use crate::semantics::{
-    rc, AlphaVar, Hir, HirKind, NameEnv, NzEnv, TyEnv, Value,
-};
-use crate::syntax::{ExprKind, Span, V};
+use crate::semantics::{AlphaVar, Hir, HirKind, NzEnv, Value};
+use crate::syntax::{ExprKind, Span};
 use crate::Normalized;
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -56,13 +54,10 @@ impl TyExpr {
     pub fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr {
         self.to_hir().to_expr(opts)
     }
-    pub fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
-        self.to_hir().to_expr_tyenv(env)
-    }
 
     /// Eval the TyExpr. It will actually get evaluated only as needed on demand.
     pub fn eval(&self, env: &NzEnv) -> Value {
-        Value::new_thunk(env, self.clone())
+        Value::new_thunk(env, self.to_hir())
     }
     /// Eval a closed TyExpr (i.e. without free variables). It will actually get evaluated only as
     /// needed on demand.
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 810e483..5b233f8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -266,17 +266,10 @@ fn type_one_layer(
             let x_ty = x.get_type()?;
             if x_ty != t {
                 return span_err(&format!(
-                    "annot mismatch: ({} : {}) : {}",
-                    x.to_expr_tyenv(env),
-                    x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
-                    t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
+                    "annot mismatch: {} != {}",
+                    x_ty.to_expr_tyenv(env),
+                    t.to_expr_tyenv(env)
                 ));
-                // return span_err(format!(
-                //     "annot mismatch: {} != {}",
-                //     x_ty.to_tyexpr_tyenv(env).to_expr_tyenv(env),
-                //     t.to_tyexpr_tyenv(env).to_expr_tyenv(env)
-                // ));
-                // return span_err(format!("annot mismatch: {:#?} : {:#?}", x, t,));
             }
             x_ty
         }