From 7cbfc1a0d32766a383d1f48902502adaa2234d2f Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Feb 2020 19:12:31 +0000
Subject: Avoid re-typechecking after import

---
 dhall/src/error/mod.rs                 |  1 -
 dhall/src/lib.rs                       |  3 +++
 dhall/src/semantics/nze/normalize.rs   |  1 +
 dhall/src/semantics/resolve/env.rs     |  8 ++++----
 dhall/src/semantics/resolve/hir.rs     |  7 ++++++-
 dhall/src/semantics/resolve/resolve.rs | 20 +++++++++++---------
 dhall/src/semantics/tck/typecheck.rs   |  1 +
 7 files changed, 26 insertions(+), 15 deletions(-)

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index b8f2fca..8829d47 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,7 +1,6 @@
 use std::io::Error as IOError;
 
 use crate::semantics::resolve::ImportStack;
-use crate::semantics::Hir;
 use crate::syntax::{Import, ParseError};
 
 mod builder;
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index c2f5020..9922144 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -123,6 +123,9 @@ impl Typed {
         self.hir.to_expr(ToExprOptions { alpha: false })
     }
 
+    pub(crate) fn ty(&self) -> &Type {
+        &self.ty
+    }
     pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
         Ok(Normalized(self.ty.clone().into_nir()))
     }
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 4c2aa33..604db8f 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -442,6 +442,7 @@ pub(crate) fn normalize_one_layer(expr: ExprKind<Nir>, env: &NzEnv) -> NirKind {
 pub(crate) fn normalize_hir_whnf(env: &NzEnv, hir: &Hir) -> NirKind {
     match hir.kind() {
         HirKind::Var(var) => env.lookup_val(var),
+        HirKind::Import(hir, _) => normalize_hir_whnf(env, hir),
         HirKind::Expr(ExprKind::Lam(binder, annot, body)) => {
             let annot = annot.eval(env);
             NirKind::LamClosure {
diff --git a/dhall/src/semantics/resolve/env.rs b/dhall/src/semantics/resolve/env.rs
index ff743d3..43676cc 100644
--- a/dhall/src/semantics/resolve/env.rs
+++ b/dhall/src/semantics/resolve/env.rs
@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 
 use crate::error::{Error, ImportError};
-use crate::semantics::{AlphaVar, Hir, Import, VarEnv};
+use crate::semantics::{AlphaVar, Import, TypedHir, VarEnv};
 use crate::syntax::{Label, V};
 
 /// Environment for resolving names.
@@ -10,7 +10,7 @@ pub(crate) struct NameEnv {
     names: Vec<Label>,
 }
 
-pub(crate) type ImportCache = HashMap<Import, Hir>;
+pub(crate) type ImportCache = HashMap<Import, TypedHir>;
 pub(crate) type ImportStack = Vec<Import>;
 
 /// Environment for resolving imports
@@ -75,8 +75,8 @@ impl ImportEnv {
     pub fn handle_import(
         &mut self,
         import: Import,
-        mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<Hir, Error>,
-    ) -> Result<Hir, Error> {
+        mut do_resolve: impl FnMut(&mut Self, &Import) -> Result<TypedHir, Error>,
+    ) -> Result<TypedHir, Error> {
         if self.stack.contains(&import) {
             return Err(
                 ImportError::ImportCycle(self.stack.clone(), import).into()
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index 73fc371..2f3464a 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -1,5 +1,5 @@
 use crate::error::TypeError;
-use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv};
+use crate::semantics::{type_with, NameEnv, Nir, NzEnv, Tir, TyEnv, Type};
 use crate::syntax::{Expr, ExprKind, Span, V};
 use crate::{NormalizedExpr, ToExprOptions};
 
@@ -13,6 +13,8 @@ pub struct AlphaVar {
 pub(crate) enum HirKind {
     /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
+    /// Result of resolving an import.
+    Import(Hir, Type),
     // Forbidden ExprKind variants: Var, Import, Completion
     Expr(ExprKind<Hir>),
 }
@@ -96,6 +98,9 @@ fn hir_to_expr(
     let kind = match hir.kind() {
         HirKind::Var(v) if opts.alpha => ExprKind::Var(V("_".into(), v.idx())),
         HirKind::Var(v) => ExprKind::Var(env.label_var(v)),
+        HirKind::Import(hir, _) => {
+            return hir_to_expr(hir, opts, &mut NameEnv::new())
+        }
         HirKind::Expr(e) => {
             let e = e.map_ref_maybe_binder(|l, hir| {
                 if let Some(l) = l {
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 23d4c3d..82800ec 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -3,7 +3,7 @@ use std::path::{Path, PathBuf};
 
 use crate::error::ErrorBuilder;
 use crate::error::{Error, ImportError};
-use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv};
+use crate::semantics::{mkerr, Hir, HirKind, ImportEnv, NameEnv, Type};
 use crate::syntax;
 use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
 use crate::{Parsed, ParsedExpr, Resolved};
@@ -11,6 +11,9 @@ use crate::{Parsed, ParsedExpr, Resolved};
 // TODO: evaluate import headers
 pub(crate) type Import = syntax::Import<()>;
 
+/// Owned Hir with a type. Different from Tir because the Hir is owned.
+pub(crate) type TypedHir = (Hir, Type);
+
 /// A root from which to resolve relative imports.
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum ImportRoot {
@@ -21,7 +24,7 @@ fn resolve_one_import(
     env: &mut ImportEnv,
     import: &Import,
     root: &ImportRoot,
-) -> Result<Hir, Error> {
+) -> Result<TypedHir, Error> {
     use self::ImportRoot::*;
     use syntax::FilePrefix::*;
     use syntax::ImportLocation::*;
@@ -43,12 +46,10 @@ fn resolve_one_import(
     }
 }
 
-fn load_import(env: &mut ImportEnv, f: &Path) -> Result<Hir, Error> {
+fn load_import(env: &mut ImportEnv, f: &Path) -> Result<TypedHir, Error> {
     let parsed = Parsed::parse_file(f)?;
-    Ok(resolve_with_env(env, parsed)?
-        .typecheck()?
-        .normalize()
-        .to_hir())
+    let typed = resolve_with_env(env, parsed)?.typecheck()?;
+    Ok((typed.normalize().to_hir(), typed.ty().clone()))
 }
 
 /// Desugar the first level of the expression.
@@ -85,7 +86,7 @@ fn desugar(expr: &Expr) -> Cow<'_, Expr> {
 fn traverse_resolve_expr(
     name_env: &mut NameEnv,
     expr: &Expr,
-    f: &mut impl FnMut(Import) -> Result<Hir, Error>,
+    f: &mut impl FnMut(Import) -> Result<TypedHir, Error>,
 ) -> Result<Hir, Error> {
     let expr = desugar(expr);
     Ok(match expr.kind() {
@@ -124,7 +125,8 @@ fn traverse_resolve_expr(
                 ExprKind::Import(import) => {
                     // TODO: evaluate import headers
                     let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
-                    f(import)?.kind().clone()
+                    let imported = f(import)?;
+                    HirKind::Import(imported.0, imported.1)
                 }
                 kind => HirKind::Expr(kind),
             };
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 0787b32..972326b 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -710,6 +710,7 @@ pub(crate) fn type_with<'hir>(
 ) -> Result<Tir<'hir>, TypeError> {
     let tir = match hir.kind() {
         HirKind::Var(var) => Tir::from_hir(hir, env.lookup(var)),
+        HirKind::Import(_, ty) => Tir::from_hir(hir, ty.clone()),
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
-- 
cgit v1.2.3