From a709c65eb28f1b6a666f15bfc2255da7bc7105ab Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 9 Feb 2020 21:38:37 +0000
Subject: Resolve variables alongside import resolution

---
 dhall/src/error/mod.rs | 56 +++++++++++++++++++++++++++++++++-----------------
 1 file changed, 37 insertions(+), 19 deletions(-)

(limited to 'dhall/src/error')

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 13b61fa..9cb8a41 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,17 +1,22 @@
 use std::io::Error as IOError;
 
 use crate::semantics::resolve::ImportStack;
+use crate::semantics::Hir;
 use crate::syntax::{Import, ParseError};
-use crate::NormalizedExpr;
 
 mod builder;
 pub(crate) use builder::*;
 
 pub type Result<T> = std::result::Result<T, Error>;
 
+#[derive(Debug)]
+pub struct Error {
+    kind: ErrorKind,
+}
+
 #[derive(Debug)]
 #[non_exhaustive]
-pub enum Error {
+pub(crate) enum ErrorKind {
     IO(IOError),
     Parse(ParseError),
     Decode(DecodeError),
@@ -21,10 +26,9 @@ pub enum Error {
 }
 
 #[derive(Debug)]
-pub enum ImportError {
-    Recursive(Import<NormalizedExpr>, Box<Error>),
-    UnexpectedImport(Import<NormalizedExpr>),
-    ImportCycle(ImportStack, Import<NormalizedExpr>),
+pub(crate) enum ImportError {
+    UnexpectedImport(Import<Hir>),
+    ImportCycle(ImportStack, Import<Hir>),
 }
 
 #[derive(Debug)]
@@ -51,6 +55,15 @@ pub(crate) enum TypeMessage {
     Custom(String),
 }
 
+impl Error {
+    pub(crate) fn new(kind: ErrorKind) -> Self {
+        Error { kind }
+    }
+    pub(crate) fn kind(&self) -> &ErrorKind {
+        &self.kind
+    }
+}
+
 impl TypeError {
     pub(crate) fn new(message: TypeMessage) -> Self {
         TypeError { message }
@@ -72,45 +85,50 @@ impl std::error::Error for TypeError {}
 
 impl std::fmt::Display for Error {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        match self {
-            Error::IO(err) => write!(f, "{}", err),
-            Error::Parse(err) => write!(f, "{}", err),
-            Error::Decode(err) => write!(f, "{:?}", err),
-            Error::Encode(err) => write!(f, "{:?}", err),
-            Error::Resolve(err) => write!(f, "{:?}", err),
-            Error::Typecheck(err) => write!(f, "{}", err),
+        match &self.kind {
+            ErrorKind::IO(err) => write!(f, "{}", err),
+            ErrorKind::Parse(err) => write!(f, "{}", err),
+            ErrorKind::Decode(err) => write!(f, "{:?}", err),
+            ErrorKind::Encode(err) => write!(f, "{:?}", err),
+            ErrorKind::Resolve(err) => write!(f, "{:?}", err),
+            ErrorKind::Typecheck(err) => write!(f, "{}", err),
         }
     }
 }
 
 impl std::error::Error for Error {}
+impl From<ErrorKind> for Error {
+    fn from(kind: ErrorKind) -> Error {
+        Error::new(kind)
+    }
+}
 impl From<IOError> for Error {
     fn from(err: IOError) -> Error {
-        Error::IO(err)
+        ErrorKind::IO(err).into()
     }
 }
 impl From<ParseError> for Error {
     fn from(err: ParseError) -> Error {
-        Error::Parse(err)
+        ErrorKind::Parse(err).into()
     }
 }
 impl From<DecodeError> for Error {
     fn from(err: DecodeError) -> Error {
-        Error::Decode(err)
+        ErrorKind::Decode(err).into()
     }
 }
 impl From<EncodeError> for Error {
     fn from(err: EncodeError) -> Error {
-        Error::Encode(err)
+        ErrorKind::Encode(err).into()
     }
 }
 impl From<ImportError> for Error {
     fn from(err: ImportError) -> Error {
-        Error::Resolve(err)
+        ErrorKind::Resolve(err).into()
     }
 }
 impl From<TypeError> for Error {
     fn from(err: TypeError) -> Error {
-        Error::Typecheck(err)
+        ErrorKind::Typecheck(err).into()
     }
 }
-- 
cgit v1.3.1


From 350d1cf7d9c114b1334b2743071b0b99ea64c1ec Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 13 Feb 2020 20:56:38 +0000
Subject: TyExpr always carries a type

---
 dhall/src/error/mod.rs               |   2 -
 dhall/src/lib.rs                     |   2 +-
 dhall/src/semantics/tck/tyexpr.rs    |  41 ++++---------
 dhall/src/semantics/tck/typecheck.rs | 112 +++++++++++++++++------------------
 4 files changed, 68 insertions(+), 89 deletions(-)

(limited to 'dhall/src/error')

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 9cb8a41..51bd549 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -51,7 +51,6 @@ pub struct TypeError {
 /// The specific type error
 #[derive(Debug)]
 pub(crate) enum TypeMessage {
-    Sort,
     Custom(String),
 }
 
@@ -74,7 +73,6 @@ impl std::fmt::Display for TypeError {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
         use TypeMessage::*;
         let msg = match &self.message {
-            Sort => format!("Type error: Unhandled error: {:?}", self.message),
             Custom(s) => format!("Type error: {}", s),
         };
         write!(f, "{}", msg)
diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs
index 2f0ed4b..ad54c9f 100644
--- a/dhall/src/lib.rs
+++ b/dhall/src/lib.rs
@@ -120,7 +120,7 @@ impl Typed {
     }
 
     pub(crate) fn get_type(&self) -> Result<Normalized, TypeError> {
-        Ok(Normalized(self.0.get_type()?))
+        Ok(Normalized(self.0.ty().clone()))
     }
 }
 
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index dc14cd2..ac15ac5 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -1,4 +1,3 @@
-use crate::error::{TypeError, TypeMessage};
 use crate::semantics::{Hir, HirKind, NzEnv, TyEnv, Value};
 use crate::syntax::{Const, Span};
 use crate::{NormalizedExpr, ToExprOptions};
@@ -6,39 +5,36 @@ use crate::{NormalizedExpr, ToExprOptions};
 pub(crate) type Type = Value;
 
 // A hir expression plus its inferred type.
-#[derive(Clone)]
+#[derive(Debug, Clone)]
 pub(crate) struct TyExpr {
     hir: Hir,
-    ty: Option<Type>,
+    ty: Type,
 }
 
 impl TyExpr {
-    pub fn new(kind: HirKind, ty: Option<Type>, span: Span) -> Self {
+    pub fn new(kind: HirKind, ty: Type, span: Span) -> Self {
         TyExpr {
             hir: Hir::new(kind, span),
             ty,
         }
     }
 
-    pub fn kind(&self) -> &HirKind {
-        self.hir.kind()
-    }
     pub fn span(&self) -> Span {
         self.as_hir().span()
     }
-    pub fn get_type(&self) -> Result<Type, TypeError> {
-        match &self.ty {
-            Some(t) => Ok(t.clone()),
-            None => Err(TypeError::new(TypeMessage::Sort)),
-        }
+    pub fn ty(&self) -> &Type {
+        &self.ty
     }
-    pub fn get_type_tyexpr(&self, env: &TyEnv) -> Result<TyExpr, TypeError> {
-        Ok(self.get_type()?.to_hir(env.as_varenv()).typecheck(env)?)
+    pub fn get_type_tyexpr(&self, env: &TyEnv) -> TyExpr {
+        self.ty()
+            .to_hir(env.as_varenv())
+            .typecheck(env)
+            .expect("Internal type error")
     }
     /// Get the kind (the type of the type) of this value
     // TODO: avoid recomputing so much
-    pub fn get_kind(&self, env: &TyEnv) -> Result<Option<Const>, TypeError> {
-        Ok(self.get_type_tyexpr(env)?.get_type()?.as_const())
+    pub fn get_kind(&self, env: &TyEnv) -> Option<Const> {
+        self.get_type_tyexpr(env).ty().as_const()
     }
 
     pub fn to_hir(&self) -> Hir {
@@ -68,16 +64,3 @@ impl TyExpr {
         val
     }
 }
-
-impl std::fmt::Debug for TyExpr {
-    fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        let mut x = fmt.debug_struct("TyExpr");
-        x.field("kind", self.kind());
-        if let Some(ty) = self.ty.as_ref() {
-            x.field("type", &ty);
-        } else {
-            x.field("type", &None::<()>);
-        }
-        x.finish()
-    }
-}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a4ab31f..b3c9353 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -53,24 +53,24 @@ fn type_one_layer(
         ExprKind::Lam(binder, annot, body) => {
             let body_ty = body.get_type_tyexpr(
                 &env.insert_type(&binder.clone(), annot.eval(env)),
-            )?;
+            );
             let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
             type_one_layer(env, pi_ekind, None, Span::Artificial)?.eval(env)
         }
         ExprKind::Pi(_, annot, body) => {
-            let ks = match annot.get_type()?.as_const() {
+            let ks = match annot.ty().as_const() {
                 Some(k) => k,
                 _ => {
                     return mkerr(
                         ErrorBuilder::new(format!(
                             "Invalid input type: `{}`",
-                            annot.get_type()?.to_expr_tyenv(env),
+                            annot.ty().to_expr_tyenv(env),
                         ))
                         .span_err(
                             annot.span(),
                             format!(
                                 "this has type: `{}`",
-                                annot.get_type()?.to_expr_tyenv(env)
+                                annot.ty().to_expr_tyenv(env)
                             ),
                         )
                         .help(format!(
@@ -81,14 +81,14 @@ fn type_one_layer(
                     );
                 }
             };
-            let kt = match body.get_type()?.as_const() {
+            let kt = match body.ty().as_const() {
                 Some(k) => k,
                 _ => return span_err("Invalid output type"),
             };
 
             Value::from_const(function_check(ks, kt))
         }
-        ExprKind::Let(_, _, _, body) => body.get_type()?,
+        ExprKind::Let(_, _, _, body) => body.ty().clone(),
 
         ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
         ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
@@ -112,7 +112,7 @@ fn type_one_layer(
             for contents in interpolated.iter() {
                 use InterpolatedTextContents::Expr;
                 if let Expr(x) = contents {
-                    if x.get_type()? != text_type {
+                    if *x.ty() != text_type {
                         return span_err("InvalidTextInterpolation");
                     }
                 }
@@ -121,7 +121,7 @@ fn type_one_layer(
         }
         ExprKind::EmptyListLit(t) => {
             let t = t.eval(env);
-            match &*t.kind() {
+            match t.kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     args,
@@ -135,23 +135,23 @@ fn type_one_layer(
             let mut iter = xs.iter();
             let x = iter.next().unwrap();
             for y in iter {
-                if x.get_type()? != y.get_type()? {
+                if x.ty() != y.ty() {
                     return span_err("InvalidListElement");
                 }
             }
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.get_kind(env) != Some(Const::Type) {
                 return span_err("InvalidListType");
             }
 
-            let t = x.get_type()?;
+            let t = x.ty().clone();
             Value::from_builtin(Builtin::List).app(t)
         }
         ExprKind::SomeLit(x) => {
-            if x.get_kind(env)? != Some(Const::Type) {
+            if x.get_kind(env) != Some(Const::Type) {
                 return span_err("InvalidOptionalType");
             }
 
-            let t = x.get_type()?;
+            let t = x.ty().clone();
             Value::from_builtin(Builtin::Optional).app(t)
         }
         ExprKind::RecordLit(kvs) => {
@@ -163,11 +163,11 @@ fn type_one_layer(
                     Entry::Occupied(_) => {
                         return span_err("RecordTypeDuplicateField")
                     }
-                    Entry::Vacant(e) => e.insert(v.get_type()?),
+                    Entry::Vacant(e) => e.insert(v.ty().clone()),
                 };
 
                 // Check that the fields have a valid kind
-                match v.get_kind(env)? {
+                match v.get_kind(env) {
                     Some(_) => {}
                     None => return span_err("InvalidFieldType"),
                 }
@@ -191,7 +191,7 @@ fn type_one_layer(
                 };
 
                 // Check the type is a Const and compute final type
-                match t.get_type()?.as_const() {
+                match t.ty().as_const() {
                     Some(c) => k = max(k, c),
                     None => return span_err("InvalidFieldType"),
                 }
@@ -206,7 +206,7 @@ fn type_one_layer(
             let mut k = None;
             for (x, t) in kts {
                 if let Some(t) = t {
-                    match (k, t.get_type()?.as_const()) {
+                    match (k, t.ty().as_const()) {
                         (None, Some(k2)) => k = Some(k2),
                         (Some(k1), Some(k2)) if k1 == k2 => {}
                         _ => return span_err("InvalidFieldType"),
@@ -227,12 +227,12 @@ fn type_one_layer(
             Value::from_const(k)
         }
         ExprKind::Field(scrut, x) => {
-            match &*scrut.get_type()?.kind() {
+            match scrut.ty().kind() {
                 ValueKind::RecordType(kts) => match kts.get(&x) {
                     Some(tth) => tth.clone(),
                     None => return span_err("MissingRecordField"),
                 },
-                // TODO: branch here only when scrut.get_type() is a Const
+                // TODO: branch here only when scrut.ty() is a Const
                 _ => {
                     let scrut_nf = scrut.eval(env);
                     match scrut_nf.kind() {
@@ -255,7 +255,7 @@ fn type_one_layer(
         }
         ExprKind::Assert(t) => {
             let t = t.eval(env);
-            match &*t.kind() {
+            match t.kind() {
                 ValueKind::Equivalence(x, y) if x == y => {}
                 ValueKind::Equivalence(..) => {
                     return span_err("AssertMismatch")
@@ -265,9 +265,9 @@ fn type_one_layer(
             t
         }
         ExprKind::App(f, arg) => {
-            match f.get_type()?.kind() {
+            match f.ty().kind() {
                 ValueKind::PiClosure { annot, closure, .. } => {
-                    if arg.get_type()? != *annot {
+                    if arg.ty() != annot {
                         return mkerr(
                             ErrorBuilder::new(format!(
                                 "wrong type of function argument"
@@ -283,13 +283,13 @@ fn type_one_layer(
                                 arg.span(),
                                 format!(
                                     "but this has type: {}",
-                                    arg.get_type()?.to_expr_tyenv(env),
+                                    arg.ty().to_expr_tyenv(env),
                                 ),
                             )
                             .note(format!(
                                 "expected type `{}`\n   found type `{}`",
                                 annot.to_expr_tyenv(env),
-                                arg.get_type()?.to_expr_tyenv(env),
+                                arg.ty().to_expr_tyenv(env),
                             ))
                             .format(),
                         );
@@ -301,7 +301,7 @@ fn type_one_layer(
                 _ => return mkerr(
                     ErrorBuilder::new(format!(
                         "expected function, found `{}`",
-                        f.get_type()?.to_expr_tyenv(env)
+                        f.ty().to_expr_tyenv(env)
                     ))
                     .span_err(
                         f.span(),
@@ -312,21 +312,21 @@ fn type_one_layer(
             }
         }
         ExprKind::BoolIf(x, y, z) => {
-            if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
+            if *x.ty().kind() != ValueKind::from_builtin(Builtin::Bool) {
                 return span_err("InvalidPredicate");
             }
-            if y.get_kind(env)? != Some(Const::Type) {
+            if y.get_kind(env) != Some(Const::Type) {
                 return span_err("IfBranchMustBeTerm");
             }
-            if y.get_type()? != z.get_type()? {
+            if y.ty() != z.ty() {
                 return span_err("IfBranchMismatch");
             }
 
-            y.get_type()?
+            y.ty().clone()
         }
         ExprKind::BinOp(BinOp::RightBiasedRecordMerge, x, y) => {
-            let x_type = x.get_type()?;
-            let y_type = y.get_type()?;
+            let x_type = x.ty();
+            let y_type = y.ty();
 
             // Extract the LHS record type
             let kts_x = match x_type.kind() {
@@ -350,8 +350,8 @@ fn type_one_layer(
         ExprKind::BinOp(BinOp::RecursiveRecordMerge, x, y) => {
             let ekind = ExprKind::BinOp(
                 BinOp::RecursiveRecordTypeMerge,
-                x.get_type_tyexpr(env)?,
-                y.get_type_tyexpr(env)?,
+                x.get_type_tyexpr(env),
+                y.get_type_tyexpr(env),
             );
             type_one_layer(env, ekind, None, span.clone())?.eval(env)
         }
@@ -390,13 +390,12 @@ fn type_one_layer(
             check_rectymerge(&span, env, x.eval(env), y.eval(env))?;
 
             // A RecordType's type is always a const
-            let xk = x.get_type()?.as_const().unwrap();
-            let yk = y.get_type()?.as_const().unwrap();
+            let xk = x.ty().as_const().unwrap();
+            let yk = y.ty().as_const().unwrap();
             Value::from_const(max(xk, yk))
         }
         ExprKind::BinOp(BinOp::ListAppend, l, r) => {
-            let l_ty = l.get_type()?;
-            match &*l_ty.kind() {
+            match l.ty().kind() {
                 ValueKind::AppliedBuiltin(BuiltinClosure {
                     b: Builtin::List,
                     ..
@@ -404,17 +403,17 @@ fn type_one_layer(
                 _ => return span_err("BinOpTypeMismatch"),
             }
 
-            if l_ty != r.get_type()? {
+            if l.ty() != r.ty() {
                 return span_err("BinOpTypeMismatch");
             }
 
-            l_ty
+            l.ty().clone()
         }
         ExprKind::BinOp(BinOp::Equivalence, l, r) => {
-            if l.get_type()? != r.get_type()? {
+            if l.ty() != r.ty() {
                 return span_err("EquivalenceTypeMismatch");
             }
-            if l.get_kind(env)? != Some(Const::Type) {
+            if l.get_kind(env) != Some(Const::Type) {
                 return span_err("EquivalenceArgumentsMustBeTerms");
             }
 
@@ -436,24 +435,24 @@ fn type_one_layer(
                 BinOp::ImportAlt => unreachable!("ImportAlt leftover in tck"),
             });
 
-            if l.get_type()? != t {
+            if *l.ty() != t {
                 return span_err("BinOpTypeMismatch");
             }
 
-            if r.get_type()? != t {
+            if *r.ty() != t {
                 return span_err("BinOpTypeMismatch");
             }
 
             t
         }
         ExprKind::Merge(record, union, type_annot) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let handlers = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("Merge1ArgMustBeRecord"),
             };
 
-            let union_type = union.get_type()?;
+            let union_type = union.ty();
             let variants = match union_type.kind() {
                 ValueKind::UnionType(kts) => Cow::Borrowed(kts),
                 ValueKind::AppliedBuiltin(BuiltinClosure {
@@ -583,10 +582,10 @@ fn type_one_layer(
             }
         }
         ExprKind::ToMap(record, annot) => {
-            if record.get_kind(env)? != Some(Const::Type) {
+            if record.get_kind(env) != Some(Const::Type) {
                 return span_err("`toMap` only accepts records of type `Type`");
             }
-            let record_t = record.get_type()?;
+            let record_t = record.ty();
             let kts = match record_t.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => {
@@ -656,7 +655,7 @@ fn type_one_layer(
             }
         }
         ExprKind::Projection(record, labels) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let kts = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
@@ -681,7 +680,7 @@ fn type_one_layer(
             Value::from_kind(ValueKind::RecordType(new_kts))
         }
         ExprKind::ProjectionByExpr(record, selection) => {
-            let record_type = record.get_type()?;
+            let record_type = record.ty();
             let rec_kts = match record_type.kind() {
                 ValueKind::RecordType(kts) => kts,
                 _ => return span_err("ProjectionMustBeRecord"),
@@ -742,9 +741,10 @@ fn type_one_layer(
         }
     }
 
+    // TODO: avoid retraversing
     Ok(TyExpr::new(
         HirKind::Expr(ekind.map_ref(|tye| tye.to_hir())),
-        Some(ty),
+        ty,
         span,
     ))
 }
@@ -757,11 +757,9 @@ pub(crate) fn type_with(
     annot: Option<Type>,
 ) -> Result<TyExpr, TypeError> {
     match hir.kind() {
-        HirKind::Var(var) => Ok(TyExpr::new(
-            HirKind::Var(*var),
-            Some(env.lookup(var)),
-            hir.span(),
-        )),
+        HirKind::Var(var) => {
+            Ok(TyExpr::new(HirKind::Var(*var), env.lookup(var), hir.span()))
+        }
         HirKind::Expr(ExprKind::Var(_)) => {
             unreachable!("Hir should contain no unresolved variables")
         }
@@ -800,9 +798,9 @@ pub(crate) fn type_with(
                         None
                     };
                     let val = type_with(env, &val, val_annot)?;
-                    let val_ty = val.get_type()?;
                     let val_nf = val.eval(env);
-                    let body_env = env.insert_value(&binder, val_nf, val_ty);
+                    let body_env =
+                        env.insert_value(&binder, val_nf, val.ty().clone());
                     let body = type_with(&body_env, body, None)?;
                     ExprKind::Let(binder.clone(), None, val, body)
                 }
-- 
cgit v1.3.1


From a3990858840a737d7831be45953b38bd67361fb7 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 18 Feb 2020 19:08:53 +0000
Subject: Discard import headers while we don't use them

---
 dhall/src/error/mod.rs                 |  4 ++--
 dhall/src/semantics/resolve/hir.rs     | 10 +---------
 dhall/src/semantics/resolve/resolve.rs |  9 +++++++--
 3 files changed, 10 insertions(+), 13 deletions(-)

(limited to 'dhall/src/error')

diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 51bd549..b8f2fca 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -27,8 +27,8 @@ pub(crate) enum ErrorKind {
 
 #[derive(Debug)]
 pub(crate) enum ImportError {
-    UnexpectedImport(Import<Hir>),
-    ImportCycle(ImportStack, Import<Hir>),
+    UnexpectedImport(Import<()>),
+    ImportCycle(ImportStack, Import<()>),
 }
 
 #[derive(Debug)]
diff --git a/dhall/src/semantics/resolve/hir.rs b/dhall/src/semantics/resolve/hir.rs
index d0bec5a..73fc371 100644
--- a/dhall/src/semantics/resolve/hir.rs
+++ b/dhall/src/semantics/resolve/hir.rs
@@ -9,7 +9,7 @@ pub struct AlphaVar {
     idx: usize,
 }
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Debug, Clone, PartialEq, Eq)]
 pub(crate) enum HirKind {
     /// A resolved variable (i.e. a DeBruijn index)
     Var(AlphaVar),
@@ -128,11 +128,3 @@ impl std::cmp::PartialEq for Hir {
     }
 }
 impl std::cmp::Eq for Hir {}
-impl std::hash::Hash for Hir {
-    fn hash<H>(&self, state: &mut H)
-    where
-        H: std::hash::Hasher,
-    {
-        self.kind.hash(state)
-    }
-}
diff --git a/dhall/src/semantics/resolve/resolve.rs b/dhall/src/semantics/resolve/resolve.rs
index 22fb1a0..23d4c3d 100644
--- a/dhall/src/semantics/resolve/resolve.rs
+++ b/dhall/src/semantics/resolve/resolve.rs
@@ -8,7 +8,8 @@ use crate::syntax;
 use crate::syntax::{BinOp, Expr, ExprKind, FilePath, ImportLocation, URL};
 use crate::{Parsed, ParsedExpr, Resolved};
 
-pub(crate) type Import = syntax::Import<Hir>;
+// TODO: evaluate import headers
+pub(crate) type Import = syntax::Import<()>;
 
 /// A root from which to resolve relative imports.
 #[derive(Debug, Clone, PartialEq, Eq)]
@@ -120,7 +121,11 @@ fn traverse_resolve_expr(
                 Ok::<_, Error>(hir)
             })?;
             let kind = match kind {
-                ExprKind::Import(import) => f(import)?.kind().clone(),
+                ExprKind::Import(import) => {
+                    // TODO: evaluate import headers
+                    let import = import.traverse_ref(|_| Ok::<_, Error>(()))?;
+                    f(import)?.kind().clone()
+                }
                 kind => HirKind::Expr(kind),
             };
             Hir::new(kind, expr.span())
-- 
cgit v1.3.1


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(-)

(limited to 'dhall/src/error')

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.3.1