Use TyExpr in Typed

5 files changed, 50 insertions, 122 deletions

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 3dcbd38..aa819d2 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -9,9 +9,7 @@ use crate::semantics::phase::normalize::{apply_any, normalize_whnf, NzEnv};
 use crate::semantics::phase::typecheck::{
     builtin_to_value, builtin_to_value_env, const_to_value,
 };
-use crate::semantics::phase::{
-    Normalized, NormalizedExpr, ToExprOptions, Typed,
-};
+use crate::semantics::phase::{Normalized, NormalizedExpr, ToExprOptions};
 use crate::semantics::{TyExpr, TyExprKind};
 use crate::syntax::{
     BinOp, Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label,
@@ -207,9 +205,6 @@ impl Value {
         self.check_type(ty);
         self.to_whnf_ignore_type()
     }
-    pub(crate) fn into_typed(self) -> Typed {
-        Typed::from_value(self)
-    }
 
     /// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
     fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 68c32b2..0f8194c 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -4,6 +4,7 @@ use std::path::Path;
 use crate::error::{EncodeError, Error, ImportError, TypeError};
 use crate::semantics::core::value::Value;
 use crate::semantics::core::value::ValueKind;
+use crate::semantics::tck::tyexpr::TyExpr;
 use crate::syntax::binary;
 use crate::syntax::{Builtin, Const, Expr};
 use resolve::ImportRoot;
@@ -29,7 +30,7 @@ pub struct Resolved(ResolvedExpr);
 
 /// A typed expression
 #[derive(Debug, Clone)]
-pub struct Typed(Value);
+pub struct Typed(TyExpr);
 
 /// A normalized expression.
 ///
@@ -78,11 +79,14 @@ impl Parsed {
 }
 
 impl Resolved {
-    pub fn typecheck(self) -> Result<Typed, TypeError> {
-        Ok(typecheck::typecheck(self.0)?.into_typed())
+    pub fn typecheck(&self) -> Result<Typed, TypeError> {
+        Ok(Typed(crate::semantics::tck::typecheck::typecheck(&self.0)?))
     }
     pub fn typecheck_with(self, ty: &Normalized) -> Result<Typed, TypeError> {
-        Ok(typecheck::typecheck_with(self.0, ty.to_expr())?.into_typed())
+        Ok(Typed(crate::semantics::tck::typecheck::typecheck_with(
+            &self.0,
+            ty.to_expr(),
+        )?))
     }
     /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self) -> ResolvedExpr {
@@ -97,43 +101,22 @@ impl Resolved {
 
 impl Typed {
     /// Reduce an expression to its normal form, performing beta reduction
-    pub fn normalize(mut self) -> Normalized {
-        self.0.normalize_mut();
-        Normalized(self.0)
-    }
-
-    pub(crate) fn from_value(th: Value) -> Self {
-        Typed(th)
+    pub fn normalize(&self) -> Normalized {
+        let mut val = self.0.normalize_whnf_noenv();
+        val.normalize_mut();
+        Normalized(val)
     }
 
     /// Converts a value back to the corresponding AST expression.
-    pub(crate) fn to_expr(&self) -> ResolvedExpr {
+    fn to_expr(&self) -> ResolvedExpr {
         self.0.to_expr(ToExprOptions {
             alpha: false,
             normalize: false,
         })
     }
-    /// Converts a value back to the corresponding AST expression, beta-normalizing in the process.
-    pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr {
-        self.0.to_expr(ToExprOptions {
-            alpha: false,
-            normalize: true,
-        })
-    }
-    /// Converts a value back to the corresponding AST expression, (alpha,beta)-normalizing in the
-    /// process.
-    pub(crate) fn normalize_to_expr_alpha(&self) -> NormalizedExpr {
-        self.0.to_expr(ToExprOptions {
-            alpha: true,
-            normalize: true,
-        })
-    }
-    pub(crate) fn into_value(self) -> Value {
-        self.0
-    }
 
-    pub(crate) fn get_type(&self) -> Result<Typed, TypeError> {
-        Ok(self.0.get_type()?.into_typed())
+    pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
+        Ok(Normalized(self.0.get_type()?))
     }
 }
 
@@ -142,19 +125,19 @@ impl Normalized {
         binary::encode(&self.to_expr())
     }
 
+    /// Converts a value back to the corresponding AST expression.
     pub fn to_expr(&self) -> NormalizedExpr {
-        // TODO: do it directly
-        self.to_typed().normalize_to_expr()
+        self.0.to_expr(ToExprOptions {
+            alpha: false,
+            normalize: false,
+        })
     }
+    /// Converts a value back to the corresponding AST expression, alpha-normalizing in the process.
     pub(crate) fn to_expr_alpha(&self) -> NormalizedExpr {
-        // TODO: do it directly
-        self.to_typed().normalize_to_expr_alpha()
-    }
-    pub(crate) fn to_typed(&self) -> Typed {
-        Typed(self.0.clone())
-    }
-    pub(crate) fn into_typed(self) -> Typed {
-        Typed(self.0)
+        self.0.to_expr(ToExprOptions {
+            alpha: true,
+            normalize: false,
+        })
     }
     pub(crate) fn to_value(&self) -> Value {
         self.0.clone()
@@ -253,7 +236,7 @@ impl std::hash::Hash for Normalized {
 impl Eq for Typed {}
 impl PartialEq for Typed {
     fn eq(&self, other: &Self) -> bool {
-        self.0 == other.0
+        self.normalize() == other.normalize()
     }
 }
 impl Display for Typed {
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index f559323..6de65e8 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -336,7 +336,7 @@ fn type_with(ctx: &TyCtx, e: Expr<Normalized>) -> Result<Value, TypeError> {
             // ))
             Ok(e)
         }
-        Embed(p) => Ok(p.clone().into_typed().into_value()),
+        Embed(p) => Ok(p.clone().into_value()),
         Var(var) => match ctx.lookup(&var) {
             Some(typed) => Ok(typed.clone()),
             None => Err(TypeError::new(TypeMessage::UnboundVariable(span))),
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a83f175..5880d92 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -677,7 +677,7 @@ pub(crate) fn type_with(
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
         ExprKind::Embed(p) => {
-            return Ok(p.clone().into_typed().into_value().to_tyexpr_noenv())
+            return Ok(p.clone().into_value().to_tyexpr_noenv())
         }
         ekind => {
             let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
@@ -692,3 +692,10 @@ pub(crate) fn type_with(
 pub(crate) fn typecheck(e: &Expr<Normalized>) -> Result<TyExpr, TypeError> {
     type_with(&TyEnv::new(), e)
 }
+
+pub(crate) fn typecheck_with(
+    expr: &Expr<Normalized>,
+    ty: Expr<Normalized>,
+) -> Result<TyExpr, TypeError> {
+    typecheck(&expr.rewrap(ExprKind::Annot(expr.clone(), ty)))
+}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 1c687f6..08feadf 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -158,65 +158,24 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             parse_file_str(&file_path)?.resolve().unwrap_err();
         }
         TypeInferenceSuccess(expr_file_path, expected_file_path) => {
-            // let expr =
-            //     parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
-            // let ty = expr.get_type()?.to_expr();
-            // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
-            // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?;
-            // let ty = tyexpr.get_type()?.to_expr();
-            //
-            let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
-            let ty = crate::semantics::tck::typecheck::typecheck(&expr)?
-                .get_type()?
-                .to_expr(crate::semantics::phase::ToExprOptions {
-                    alpha: false,
-                    normalize: true,
-                });
+            let expr =
+                parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
+            let ty = expr.get_type()?.to_expr();
             let expected = parse_file_str(&expected_file_path)?.to_expr();
             assert_eq_display!(ty, expected);
-            //
-            // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
-            // let ty = crate::semantics::tck::typecheck::typecheck(&expr)?
-            //     .get_type()?;
-            // let expected = parse_file_str(&expected_file_path)?.to_expr();
-            // let expected = crate::semantics::tck::typecheck::typecheck(&expected)?
-            //     .normalize_whnf_noenv();
-            // // if ty != expected {
-            // //     assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions {
-            // //         alpha: false,
-            // //         normalize: true,
-            // //     }), expected.to_expr(crate::semantics::phase::ToExprOptions {
-            // //         alpha: false,
-            // //         normalize: true,
-            // //     }))
-            // // }
-            // assert_eq_pretty!(ty, expected);
         }
         TypeInferenceFailure(file_path) => {
-            // let mut res =
-            //     parse_file_str(&file_path)?.skip_resolve()?.typecheck();
-            // if let Ok(e) = &res {
-            //     // If e did typecheck, check that get_type fails
-            //     res = e.get_type();
-            // }
-            // res.unwrap_err();
-
-            let res = crate::semantics::tck::typecheck::typecheck(
-                &parse_file_str(&file_path)?.skip_resolve()?.to_expr(),
-            );
+            let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck();
             if let Ok(e) = &res {
                 // If e did typecheck, check that get_type fails
                 e.get_type().unwrap_err();
-            } else {
-                res.unwrap_err();
             }
         }
         // Checks the output of the type error against a text file. If the text file doesn't exist,
         // we instead write to it the output we got. This makes it easy to update those files: just
         // `rm -r dhall/tests/type-errors` and run the tests again.
         TypeError(file_path) => {
-            let mut res =
-                parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+            let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck();
             let file_path = PathBuf::from(file_path);
             let error_file_path = file_path
                 .strip_prefix("../dhall-lang/tests/type-inference/failure/")
@@ -224,11 +183,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             let error_file_path =
                 PathBuf::from("tests/type-errors/").join(error_file_path);
             let error_file_path = error_file_path.with_extension("txt");
-            if let Ok(e) = &res {
-                // If e did typecheck, check that get_type fails
-                res = e.get_type();
-            }
-            let err: Error = res.unwrap_err().into();
+            let err: Error = match res {
+                Ok(e) => {
+                    // If e did typecheck, check that get_type fails
+                    e.get_type().unwrap_err().into()
+                }
+                Err(e) => e.into(),
+            };
 
             if error_file_path.is_file() {
                 let expected_msg = std::fs::read_to_string(error_file_path)?;
@@ -241,28 +202,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
             }
         }
         Normalization(expr_file_path, expected_file_path) => {
-            // let expr = parse_file_str(&expr_file_path)?
-            //     .resolve()?
-            //     .typecheck()?
-            //     .normalize()
-            //     .to_expr();
-            // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr();
-            // let expr = crate::semantics::nze::nzexpr::typecheck(expr)?
-            //     .normalize()
-            //     .to_expr();
-            // let expr = parse_file_str(&expr_file_path)?
-            //     .resolve()?
-            //     .typecheck()?
-            //     .to_value()
-            //     .to_tyexpr_noenv()
-            //     .normalize_whnf_noenv()
-            //     .to_expr(crate::semantics::phase::ToExprOptions {
-            //         alpha: false,
-            //         normalize: true,
-            //     });
             let expr = parse_file_str(&expr_file_path)?
                 .resolve()?
-                .tck_and_normalize_new_flow()?
+                .typecheck()?
+                .normalize()
                 .to_expr();
             let expected = parse_file_str(&expected_file_path)?.to_expr();