From c3ed75dc4b354becac0821e4288105dc2a300c4c Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 10 Feb 2020 19:14:07 +0000
Subject: Remove need for Embed

This was an archaic leftover from copying the Haskell datatypes anyway
---
 dhall/src/semantics/hir.rs           |  1 +
 dhall/src/semantics/nze/env.rs       |  6 ++++++
 dhall/src/semantics/resolve.rs       | 25 ++++++++++++++-----------
 dhall/src/semantics/tck/typecheck.rs | 10 +---------
 4 files changed, 22 insertions(+), 20 deletions(-)

(limited to 'dhall/src')

diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 9ad7374..b45851f 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -11,6 +11,7 @@ pub struct AlphaVar {
 
 #[derive(Debug, Clone, PartialEq, Eq, Hash)]
 pub(crate) enum HirKind {
+    /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
     // Forbidden ExprKind variants: Var, Import, Embed
     Expr(ExprKind<Hir, Normalized>),
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index 5b036f0..241af40 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -86,3 +86,9 @@ impl<Type: Clone> ValEnv<Type> {
         }
     }
 }
+
+impl<'a> From<&'a NzEnv> for NzEnv {
+    fn from(x: &'a NzEnv) -> Self {
+        x.clone()
+    }
+}
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
index 8c9bb05..80e5132 100644
--- a/dhall/src/semantics/resolve.rs
+++ b/dhall/src/semantics/resolve.rs
@@ -16,7 +16,7 @@ pub(crate) enum ImportRoot {
     LocalDir(PathBuf),
 }
 
-type ImportCache = HashMap<Import, Normalized>;
+type ImportCache = HashMap<Import, Hir>;
 
 pub(crate) type ImportStack = Vec<Import>;
 
@@ -36,8 +36,8 @@ impl ResolveEnv {
     pub fn handle_import(
         &mut self,
         import: Import,
-        mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<Normalized, Error>,
-    ) -> Result<Normalized, Error> {
+        mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<Hir, Error>,
+    ) -> Result<Hir, Error> {
         if self.stack.contains(&import) {
             return Err(
                 ImportError::ImportCycle(self.stack.clone(), import).into()
@@ -68,7 +68,7 @@ fn resolve_one_import(
     env: &mut ResolveEnv,
     import: &Import,
     root: &ImportRoot,
-) -> Result<Normalized, Error> {
+) -> Result<Hir, Error> {
     use self::ImportRoot::*;
     use syntax::FilePrefix::*;
     use syntax::ImportLocation::*;
@@ -90,9 +90,12 @@ fn resolve_one_import(
     }
 }
 
-fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Normalized, Error> {
+fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Hir, Error> {
     let parsed = Parsed::parse_file(f)?;
-    Ok(resolve_with_env(env, parsed)?.typecheck()?.normalize())
+    Ok(resolve_with_env(env, parsed)?
+        .typecheck()?
+        .normalize()
+        .to_hir())
 }
 
 /// Traverse the expression, handling import alternatives and passing
@@ -100,7 +103,7 @@ fn load_import(env: &mut ResolveEnv, f: &Path) -> Result<Normalized, Error> {
 fn traverse_resolve_expr(
     name_env: &mut NameEnv,
     expr: &Expr<Normalized>,
-    f: &mut impl FnMut(Import) -> Result<Normalized, Error>,
+    f: &mut impl FnMut(Import) -> Result<Hir, Error>,
 ) -> Result<Hir, Error> {
     let kind = match expr.kind() {
         ExprKind::Var(var) => match name_env.unlabel_var(&var) {
@@ -134,10 +137,10 @@ fn traverse_resolve_expr(
                 }
                 Ok::<_, Error>(hir)
             })?;
-            HirKind::Expr(match kind {
-                ExprKind::Import(import) => ExprKind::Embed(f(import)?),
-                kind => kind,
-            })
+            match kind {
+                ExprKind::Import(import) => f(import)?.kind().clone(),
+                kind => HirKind::Expr(kind),
+            }
         }
     };
 
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 7f02832..4e45637 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -761,21 +761,13 @@ fn type_one_layer(
 /// `type_with` typechecks an expressio in the provided environment.
 pub(crate) fn type_with(env: &TyEnv, hir: &Hir) -> Result<TyExpr, TypeError> {
     let (tyekind, ty) = match hir.kind() {
-        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(&var))),
+        HirKind::Var(var) => (TyExprKind::Var(*var), Some(env.lookup(var))),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
         HirKind::Expr(ExprKind::Const(Const::Sort)) => {
             (TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
         }
-        HirKind::Expr(ExprKind::Embed(p)) => {
-            let val = p.clone().into_value();
-            (
-                val.to_tyexpr_noenv().kind().clone(),
-                Some(val.get_type(&TyEnv::new())?),
-            )
-            // return Ok(p.clone().into_value().to_tyexpr_noenv())
-        }
         HirKind::Expr(ekind) => {
             let ekind = match ekind {
                 ExprKind::Lam(binder, annot, body) => {
-- 
cgit v1.2.3