summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.rustfmt.toml1
-rw-r--r--Cargo.lock7
-rw-r--r--dhall/Cargo.toml3
-rw-r--r--dhall/src/error/builder.rs168
-rw-r--r--dhall/src/error/mod.rs12
-rw-r--r--dhall/src/semantics/nze/value.rs10
-rw-r--r--dhall/src/semantics/tck/env.rs6
-rw-r--r--dhall/src/semantics/tck/tyexpr.rs4
-rw-r--r--dhall/src/semantics/tck/typecheck.rs282
-rw-r--r--dhall/src/syntax/ast/expr.rs6
-rw-r--r--dhall/src/syntax/ast/span.rs30
-rw-r--r--dhall/src/syntax/text/parser.rs39
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt16
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt10
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt7
-rw-r--r--dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt8
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt8
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt10
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt10
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt9
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt10
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt7
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt7
-rw-r--r--serde_dhall/src/lib.rs2
-rw-r--r--serde_dhall/src/serde.rs2
-rw-r--r--tests_buffer2
27 files changed, 539 insertions, 144 deletions
diff --git a/.rustfmt.toml b/.rustfmt.toml
index ee91dbd..0a0f30e 100644
--- a/.rustfmt.toml
+++ b/.rustfmt.toml
@@ -1,3 +1,4 @@
edition = "2018"
max_width = 80
# error_on_line_overflow = true
+format_strings = true
diff --git a/Cargo.lock b/Cargo.lock
index c737e52..450a1da 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -19,6 +19,11 @@ dependencies = [
]
[[package]]
+name = "annotate-snippets"
+version = "0.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+
+[[package]]
name = "ansi_term"
version = "0.11.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
@@ -87,6 +92,7 @@ name = "dhall"
version = "0.2.1"
dependencies = [
"abnf_to_pest 0.2.0",
+ "annotate-snippets 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)",
"hex 0.3.2 (registry+https://github.com/rust-lang/crates.io-index)",
"itertools 0.8.2 (registry+https://github.com/rust-lang/crates.io-index)",
"lazy_static 1.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
@@ -511,6 +517,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
[metadata]
"checksum abnf 0.6.0 (registry+https://github.com/rust-lang/crates.io-index)" = "e065019cf2f9438a593954cc8e774925656b86701b72720b82ec3141e682ac14"
+"checksum annotate-snippets 0.6.1 (registry+https://github.com/rust-lang/crates.io-index)" = "c7021ce4924a3f25f802b2cccd1af585e39ea1a363a1aa2e72afe54b67a3a7a7"
"checksum ansi_term 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)" = "ee49baf6cb617b853aa8d93bf420db2383fab46d314482ca2803b40d5fde979b"
"checksum arrayvec 0.4.12 (registry+https://github.com/rust-lang/crates.io-index)" = "cd9fd44efafa8690358b7408d253adf110036b88f55672a933f01d616ad9b1b9"
"checksum autocfg 0.1.7 (registry+https://github.com/rust-lang/crates.io-index)" = "1d49d90015b3c36167a20fe2810c5cd875ad504b39cff3d4eae7977e6b7c1cb2"
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index 2fbfb23..3281e4a 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -10,10 +10,11 @@ edition = "2018"
build = "build.rs"
[dependencies]
+annotate-snippets = "0.6.1"
itertools = "0.8.0"
hex = "0.3.2"
lazy_static = "1.4.0"
- once_cell = "1.3.1"
+once_cell = "1.3.1"
percent-encoding = "2.1.0"
pest = "2.1"
pest_consume = "1.0"
diff --git a/dhall/src/error/builder.rs b/dhall/src/error/builder.rs
new file mode 100644
index 0000000..39f8dfb
--- /dev/null
+++ b/dhall/src/error/builder.rs
@@ -0,0 +1,168 @@
+use annotate_snippets::{
+ display_list::DisplayList,
+ formatter::DisplayListFormatter,
+ snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation},
+};
+
+use crate::syntax::{ParsedSpan, Span};
+
+#[derive(Debug, Clone, Default)]
+pub struct ErrorBuilder {
+ title: FreeAnnotation,
+ annotations: Vec<SpannedAnnotation>,
+ footer: Vec<FreeAnnotation>,
+ /// Inducate that the current builder has already been consumed and consuming it again should
+ /// panic.
+ consumed: bool,
+}
+
+#[derive(Debug, Clone)]
+struct SpannedAnnotation {
+ span: ParsedSpan,
+ message: String,
+ annotation_type: AnnotationType,
+}
+
+#[derive(Debug, Clone)]
+struct FreeAnnotation {
+ message: String,
+ annotation_type: AnnotationType,
+}
+
+impl SpannedAnnotation {
+ fn into_annotation(self) -> SourceAnnotation {
+ SourceAnnotation {
+ label: self.message,
+ annotation_type: self.annotation_type,
+ range: self.span.as_char_range(),
+ }
+ }
+}
+
+impl FreeAnnotation {
+ fn into_annotation(self) -> Annotation {
+ Annotation {
+ label: Some(self.message),
+ id: None,
+ annotation_type: self.annotation_type,
+ }
+ }
+}
+
+/// A builder that uses the annotate_snippets library to display nice error messages about source
+/// code locations.
+impl ErrorBuilder {
+ pub fn new(message: impl ToString) -> Self {
+ ErrorBuilder {
+ title: FreeAnnotation {
+ message: message.to_string(),
+ annotation_type: AnnotationType::Error,
+ },
+ annotations: Vec::new(),
+ footer: Vec::new(),
+ consumed: false,
+ }
+ }
+
+ pub fn span_annot(
+ &mut self,
+ span: Span,
+ message: impl ToString,
+ annotation_type: AnnotationType,
+ ) -> &mut Self {
+ // Ignore spans not coming from a source file
+ let span = match span {
+ Span::Parsed(span) => span,
+ _ => return self,
+ };
+ self.annotations.push(SpannedAnnotation {
+ span,
+ message: message.to_string(),
+ annotation_type,
+ });
+ self
+ }
+ pub fn footer_annot(
+ &mut self,
+ message: impl ToString,
+ annotation_type: AnnotationType,
+ ) -> &mut Self {
+ self.footer.push(FreeAnnotation {
+ message: message.to_string(),
+ annotation_type,
+ });
+ self
+ }
+
+ pub fn span_err(
+ &mut self,
+ span: Span,
+ message: impl ToString,
+ ) -> &mut Self {
+ self.span_annot(span, message, AnnotationType::Error)
+ }
+ pub fn span_help(
+ &mut self,
+ span: Span,
+ message: impl ToString,
+ ) -> &mut Self {
+ self.span_annot(span, message, AnnotationType::Help)
+ }
+ pub fn help(&mut self, message: impl ToString) -> &mut Self {
+ self.footer_annot(message, AnnotationType::Help)
+ }
+ pub fn note(&mut self, message: impl ToString) -> &mut Self {
+ self.footer_annot(message, AnnotationType::Note)
+ }
+
+ // TODO: handle multiple files
+ pub fn format(&mut self) -> String {
+ if self.consumed {
+ panic!("tried to format the same ErrorBuilder twice")
+ }
+ let this = std::mem::replace(self, ErrorBuilder::default());
+ self.consumed = true;
+ drop(self); // Get rid of the self reference so we don't use it by mistake.
+
+ let slices = if this.annotations.is_empty() {
+ Vec::new()
+ } else {
+ let input = this.annotations[0].span.to_input();
+ let annotations = this
+ .annotations
+ .into_iter()
+ .map(|annot| annot.into_annotation())
+ .collect();
+ vec![Slice {
+ source: input,
+ line_start: 1, // TODO
+ origin: Some("<current file>".to_string()),
+ fold: true,
+ annotations,
+ }]
+ };
+ let footer = this
+ .footer
+ .into_iter()
+ .map(|annot| annot.into_annotation())
+ .collect();
+
+ let snippet = Snippet {
+ title: Some(this.title.into_annotation()),
+ slices,
+ footer,
+ };
+ let dl = DisplayList::from(snippet);
+ let dlf = DisplayListFormatter::new(true, false);
+ format!("{}", dlf.format(&dl))
+ }
+}
+
+impl Default for FreeAnnotation {
+ fn default() -> Self {
+ FreeAnnotation {
+ message: String::new(),
+ annotation_type: AnnotationType::Error,
+ }
+ }
+}
diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs
index 4df018d..6ea7d0c 100644
--- a/dhall/src/error/mod.rs
+++ b/dhall/src/error/mod.rs
@@ -1,10 +1,12 @@
use std::io::Error as IOError;
use crate::semantics::resolve::ImportStack;
-use crate::semantics::Value;
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)]
@@ -46,8 +48,6 @@ pub struct TypeError {
#[derive(Debug)]
pub(crate) enum TypeMessage {
// UnboundVariable(Span),
- InvalidInputType(Value),
- InvalidOutputType(Value),
// NotAFunction(Value),
// TypeMismatch(Value, Value, Value),
// AnnotMismatch(Value, Value),
@@ -97,12 +97,6 @@ impl std::fmt::Display for TypeError {
use TypeMessage::*;
let msg = match &self.message {
// UnboundVariable(var) => var.error("Type error: Unbound variable"),
- InvalidInputType(v) => {
- v.span().error("Type error: Invalid function input")
- }
- InvalidOutputType(v) => {
- v.span().error("Type error: Invalid function output")
- }
// NotAFunction(v) => v.span().error("Type error: Not a function"),
// TypeMismatch(x, y, z) => {
// x.span()
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index ae06942..1143781 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -6,6 +6,7 @@ use crate::semantics::nze::lazy;
use crate::semantics::Binder;
use crate::semantics::{
apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
+ TyEnv,
};
use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
@@ -173,9 +174,9 @@ impl Value {
_ => None,
}
}
- pub(crate) fn span(&self) -> Span {
- self.0.span.clone()
- }
+ // 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
@@ -192,6 +193,9 @@ 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)
+ }
pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
self.kind().clone()
}
diff --git a/dhall/src/semantics/tck/env.rs b/dhall/src/semantics/tck/env.rs
index 812ca7a..1fc711c 100644
--- a/dhall/src/semantics/tck/env.rs
+++ b/dhall/src/semantics/tck/env.rs
@@ -1,4 +1,4 @@
-use crate::semantics::{AlphaVar, NzEnv, NzVar, TyExprKind, Type, Value};
+use crate::semantics::{AlphaVar, NzEnv, NzVar, Type, Value};
use crate::syntax::{Label, V};
/// Environment for indexing variables.
@@ -116,9 +116,9 @@ impl TyEnv {
items: self.items.insert_value(e),
}
}
- pub fn lookup(&self, var: &V) -> Option<(TyExprKind, Type)> {
+ pub fn lookup(&self, var: &V) -> Option<(AlphaVar, Type)> {
let var = self.names.unlabel_var(var)?;
let ty = self.items.lookup_ty(&var);
- Some((TyExprKind::Var(var), ty))
+ Some((var, ty))
}
}
diff --git a/dhall/src/semantics/tck/tyexpr.rs b/dhall/src/semantics/tck/tyexpr.rs
index 1a048f9..1886646 100644
--- a/dhall/src/semantics/tck/tyexpr.rs
+++ b/dhall/src/semantics/tck/tyexpr.rs
@@ -48,8 +48,8 @@ impl TyExpr {
pub fn kind(&self) -> &TyExprKind {
&*self.kind
}
- pub fn span(&self) -> &Span {
- &self.span
+ pub fn span(&self) -> Span {
+ self.span.clone()
}
pub fn get_type(&self) -> Result<Type, TypeError> {
match &self.ty {
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 20076cd..9a1d0d8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
use std::cmp::max;
use std::collections::HashMap;
-use crate::error::{TypeError, TypeMessage};
+use crate::error::{ErrorBuilder, TypeError, TypeMessage};
use crate::semantics::merge_maps;
use crate::semantics::{
type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
@@ -35,19 +35,6 @@ fn function_check(a: Const, b: Const) -> Const {
}
}
-fn type_of_function(src: Type, tgt: Type) -> Result<Type, TypeError> {
- let ks = match src.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(TypeMessage::InvalidInputType(src))),
- };
- let kt = match tgt.as_const() {
- Some(k) => k,
- _ => return Err(TypeError::new(TypeMessage::InvalidOutputType(tgt))),
- };
-
- Ok(Value::from_const(function_check(ks, kt)))
-}
-
fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
Err(TypeError::new(TypeMessage::Custom(x.to_string())))
}
@@ -57,18 +44,61 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
fn type_one_layer(
env: &TyEnv,
kind: &ExprKind<TyExpr, Normalized>,
+ span: Span,
) -> Result<Type, TypeError> {
Ok(match kind {
ExprKind::Import(..) => unreachable!(
"There should remain no imports in a resolved expression"
),
ExprKind::Var(..)
- | ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
| ExprKind::Const(Const::Sort)
| ExprKind::Embed(..) => unreachable!(), // Handled in type_with
+ ExprKind::Lam(binder, annot, body) => {
+ let body_ty = body.get_type()?;
+ let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
+ let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
+ let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
+ let ty = TyExpr::new(
+ TyExprKind::Expr(pi_ekind),
+ Some(pi_ty),
+ Span::Artificial,
+ );
+ ty.eval(env.as_nzenv())
+ }
+ ExprKind::Pi(_, annot, body) => {
+ let ks = match annot.get_type()?.as_const() {
+ Some(k) => k,
+ _ => {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Invalid input type: `{}`",
+ annot.get_type()?.to_expr_tyenv(env),
+ ))
+ .span_err(
+ annot.span(),
+ format!(
+ "this has type: `{}`",
+ annot.get_type()?.to_expr_tyenv(env)
+ ),
+ )
+ .help(format!(
+ "The input type of a function must have type \
+ `Type`, `Kind` or `Sort`",
+ ))
+ .format(),
+ );
+ }
+ };
+ let kt = match body.get_type()?.as_const() {
+ Some(k) => k,
+ _ => return mkerr("Invalid output type"),
+ };
+
+ Value::from_const(function_check(ks, kt))
+ }
+ ExprKind::Let(_, _, _, body) => body.get_type()?,
+
ExprKind::Const(Const::Type) => Value::from_const(Const::Kind),
ExprKind::Const(Const::Kind) => Value::from_const(Const::Sort),
ExprKind::Builtin(b) => {
@@ -201,10 +231,12 @@ fn type_one_layer(
ValueKind::UnionType(kts) => match kts.get(x) {
// Constructor has type T -> < x: T, ... >
Some(Some(ty)) => {
- let pi_ty = type_of_function(
- ty.get_type()?,
- scrut.get_type()?,
- )?;
+ // Can't fail because uniontypes must have type Const(_).
+ let kt = scrut.get_type()?.as_const().unwrap();
+ // The type of the field must be Const smaller than `kt`, thus the
+ // function type has type `kt`.
+ let pi_ty = Value::from_const(kt);
+
Value::from_kind_and_type(
ValueKind::PiClosure {
binder: Binder::new(x.clone()),
@@ -256,21 +288,47 @@ fn type_one_layer(
match f.get_type()?.kind() {
ValueKind::PiClosure { annot, closure, .. } => {
if arg.get_type()? != *annot {
- // return mkerr(format!("function annot mismatch"));
- return mkerr(format!(
- "function annot mismatch: ({} : {}) : {}",
- arg.to_expr_tyenv(env),
- arg.get_type()?
- .to_tyexpr(env.as_varenv())
- .to_expr_tyenv(env),
- annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
- ));
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "wrong type of function argument"
+ ))
+ .span_err(
+ f.span(),
+ format!(
+ "this expects an argument of type: {}",
+ annot.to_expr_tyenv(env),
+ ),
+ )
+ .span_err(
+ arg.span(),
+ format!(
+ "but this has type: {}",
+ arg.get_type()?.to_expr_tyenv(env),
+ ),
+ )
+ .note(format!(
+ "expected type `{}`\n found type `{}`",
+ annot.to_expr_tyenv(env),
+ arg.get_type()?.to_expr_tyenv(env),
+ ))
+ .format(),
+ );
}
let arg_nf = arg.eval(env.as_nzenv());
closure.apply(arg_nf)
}
- _ => return mkerr(format!("apply to not Pi")),
+ _ => return mkerr(
+ ErrorBuilder::new(format!(
+ "expected function, found `{}`",
+ f.get_type()?.to_expr_tyenv(env)
+ ))
+ .span_err(
+ f.span(),
+ format!("function application requires a function",),
+ )
+ .format(),
+ ),
}
}
ExprKind::BoolIf(x, y, z) => {
@@ -323,7 +381,7 @@ fn type_one_layer(
x.get_type()?.to_tyexpr(env.as_varenv()),
y.get_type()?.to_tyexpr(env.as_varenv()),
);
- let ty = type_one_layer(env, &ekind)?;
+ let ty = type_one_layer(env, &ekind, Span::Artificial)?;
TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
.eval(env.as_nzenv())
}
@@ -347,6 +405,7 @@ fn type_one_layer(
tx.to_tyexpr(env.as_varenv()),
ty.to_tyexpr(env.as_varenv()),
),
+ Span::Artificial,
)?;
}
}
@@ -439,14 +498,73 @@ fn type_one_layer(
Some(Some(variant_type)) => match handler_type.kind() {
ValueKind::PiClosure { closure, annot, .. } => {
if variant_type != annot {
- return mkerr("MergeHandlerTypeMismatch");
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "Wrong handler input type"
+ ))
+ .span_err(
+ span,
+ format!("in this merge expression",),
+ )
+ .span_err(
+ record.span(),
+ format!(
+ "the handler for `{}` expects a \
+ value of type: `{}`",
+ x,
+ annot.to_expr_tyenv(env)
+ ),
+ )
+ .span_err(
+ union.span(),
+ format!(
+ "but the corresponding variant \
+ has type: `{}`",
+ variant_type.to_expr_tyenv(env)
+ ),
+ )
+ .format(),
+ );
}
closure.remove_binder().or_else(|()| {
mkerr("MergeReturnTypeIsDependent")
})?
}
- _ => return mkerr("NotAFunction"),
+ _ => {
+ return mkerr(
+ ErrorBuilder::new(format!(
+ "merge handler is not a function"
+ ))
+ .span_err(
+ span,
+ format!("in this merge expression"),
+ )
+ .span_err(
+ record.span(),
+ format!(
+ "the handler for `{}` has type: `{}`",
+ x,
+ handler_type.to_expr_tyenv(env)
+ ),
+ )
+ .span_help(
+ union.span(),
+ format!(
+ "the corresponding variant has type: \
+ `{}`",
+ variant_type.to_expr_tyenv(env)
+ ),
+ )
+ .help(format!(
+ "a handler for this variant must be a \
+ function that takes an input of type: \
+ `{}`",
+ variant_type.to_expr_tyenv(env)
+ ))
+ .format(),
+ )
+ }
},
// Union alternative without type
Some(None) => handler_type.clone(),
@@ -524,62 +642,15 @@ pub(crate) fn type_with(
) -> Result<TyExpr, TypeError> {
let (tyekind, ty) = match expr.as_ref() {
ExprKind::Var(var) => match env.lookup(&var) {
- Some((k, ty)) => (k, Some(ty)),
- None => return mkerr("unbound variable"),
+ Some((v, ty)) => (TyExprKind::Var(v), Some(ty)),
+ None => {
+ return mkerr(
+ ErrorBuilder::new(format!("unbound variable `{}`", var))
+ .span_err(expr.span(), "not found in this scope")
+ .format(),
+ )
+ }
},
- ExprKind::Lam(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body_env = env.insert_type(&binder, annot_nf.clone());
- let body = type_with(&body_env, body)?;
- let body_ty = body.get_type()?;
- let ty = TyExpr::new(
- TyExprKind::Expr(ExprKind::Pi(
- binder.clone(),
- annot.clone(),
- body_ty.to_tyexpr(body_env.as_varenv()),
- )),
- Some(type_of_function(annot.get_type()?, body_ty.get_type()?)?),
- Span::Artificial,
- );
- let ty = ty.eval(env.as_nzenv());
- (
- TyExprKind::Expr(ExprKind::Lam(binder.clone(), annot, body)),
- Some(ty),
- )
- }
- ExprKind::Pi(binder, annot, body) => {
- let annot = type_with(env, annot)?;
- let annot_nf = annot.eval(env.as_nzenv());
- let body =
- type_with(&env.insert_type(binder, annot_nf.clone()), body)?;
- let ty = type_of_function(annot.get_type()?, body.get_type()?)?;
- (
- TyExprKind::Expr(ExprKind::Pi(binder.clone(), annot, body)),
- Some(ty),
- )
- }
- ExprKind::Let(binder, annot, val, body) => {
- let val = if let Some(t) = annot {
- t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
- } else {
- val.clone()
- };
-
- let val = type_with(env, &val)?;
- let val_nf = val.eval(&env.as_nzenv());
- let body = type_with(&env.insert_value(&binder, val_nf), body)?;
- let body_ty = body.get_type().ok();
- (
- TyExprKind::Expr(ExprKind::Let(
- binder.clone(),
- None,
- val,
- body,
- )),
- body_ty,
- )
- }
ExprKind::Const(Const::Sort) => {
(TyExprKind::Expr(ExprKind::Const(Const::Sort)), None)
}
@@ -587,8 +658,37 @@ pub(crate) fn type_with(
return Ok(p.clone().into_value().to_tyexpr_noenv())
}
ekind => {
- let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
- let ty = type_one_layer(env, &ekind)?;
+ let ekind = match ekind {
+ ExprKind::Lam(binder, annot, body) => {
+ let annot = type_with(env, annot)?;
+ let annot_nf = annot.eval(env.as_nzenv());
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Lam(binder.clone(), annot, body)
+ }
+ ExprKind::Pi(binder, annot, body) => {
+ let annot = type_with(env, annot)?;
+ let annot_nf = annot.eval(env.as_nzenv());
+ let body_env = env.insert_type(binder, annot_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Pi(binder.clone(), annot, body)
+ }
+ ExprKind::Let(binder, annot, val, body) => {
+ let val = if let Some(t) = annot {
+ t.rewrap(ExprKind::Annot(val.clone(), t.clone()))
+ } else {
+ val.clone()
+ };
+ let val = type_with(env, &val)?;
+ let val_nf = val.eval(&env.as_nzenv());
+ let body_env = env.insert_value(&binder, val_nf);
+ let body = type_with(&body_env, body)?;
+ ExprKind::Let(binder.clone(), None, val, body)
+ }
+ _ => ekind.traverse_ref(|e| type_with(env, e))?,
+ };
+
+ let ty = type_one_layer(env, &ekind, expr.span())?;
(TyExprKind::Expr(ekind), Some(ty))
}
};
diff --git a/dhall/src/syntax/ast/expr.rs b/dhall/src/syntax/ast/expr.rs
index 28a0aee..b493fdb 100644
--- a/dhall/src/syntax/ast/expr.rs
+++ b/dhall/src/syntax/ast/expr.rs
@@ -275,6 +275,12 @@ impl<E> Expr<E> {
span: self.span.clone(),
}
}
+ pub fn with_span(self, span: Span) -> Self {
+ Expr {
+ kind: self.kind,
+ span,
+ }
+ }
pub fn traverse_resolve_mut<Err, F1>(
&mut self,
diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs
index f9c7008..ffdd82c 100644
--- a/dhall/src/syntax/ast/span.rs
+++ b/dhall/src/syntax/ast/span.rs
@@ -24,6 +24,20 @@ pub enum Span {
Artificial,
}
+impl ParsedSpan {
+ pub(crate) fn to_input(&self) -> String {
+ self.input.to_string()
+ }
+ /// Convert to a char range for consumption by annotate_snippets.
+ /// This compensates for https://github.com/rust-lang/annotate-snippets-rs/issues/24
+ pub(crate) fn as_char_range(&self) -> (usize, usize) {
+ (
+ char_idx_from_byte_idx(&self.input, self.start),
+ char_idx_from_byte_idx(&self.input, self.end),
+ )
+ }
+}
+
impl Span {
pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self {
Span::Parsed(ParsedSpan {
@@ -79,3 +93,19 @@ impl Span {
format!("{}", err)
}
}
+
+/// Convert a byte idx into a string into a char idx for consumption by annotate_snippets.
+fn char_idx_from_byte_idx(input: &str, idx: usize) -> usize {
+ let char_idx = input
+ .char_indices()
+ .enumerate()
+ .find(|(_, (i, _))| *i == idx)
+ .unwrap()
+ .0;
+ // Unix-style newlines are counted as two chars (see
+ // https://github.com/rust-lang/annotate-snippets-rs/issues/24).
+ let nbr_newlines = input[..idx].chars().filter(|c| *c == '\n').count();
+ let nbr_carriage_returns =
+ input[..idx].chars().filter(|c| *c == '\r').count();
+ char_idx + nbr_newlines - nbr_carriage_returns
+}
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 2ec63e2..8d571c0 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -11,7 +11,7 @@ use crate::syntax::ExprKind::*;
use crate::syntax::{
Double, FilePath, FilePrefix, Hash, ImportLocation, ImportMode, Integer,
InterpolatedText, InterpolatedTextContents, Label, NaiveDouble, Natural,
- Scheme, Span, UnspannedExpr, URL, V,
+ Scheme, Span, URL, V,
};
use crate::Normalized;
@@ -21,6 +21,7 @@ use crate::Normalized;
// are here and hopefully you can figure out how they work.
type Expr = syntax::Expr<Normalized>;
+type UnspannedExpr = syntax::UnspannedExpr<Normalized>;
type ParsedText = InterpolatedText<Expr>;
type ParsedTextContents = InterpolatedTextContents<Expr>;
type ParseInput<'input> = pest_consume::Node<'input, Rule, Rc<str>>;
@@ -78,14 +79,10 @@ impl crate::syntax::Builtin {
fn input_to_span(input: ParseInput) -> Span {
Span::make(input.user_data().clone(), input.as_pair().as_span())
}
-fn spanned(input: ParseInput, x: UnspannedExpr<Normalized>) -> Expr {
+fn spanned(input: ParseInput, x: UnspannedExpr) -> Expr {
Expr::new(x, input_to_span(input))
}
-fn spanned_union(
- span1: Span,
- span2: Span,
- x: UnspannedExpr<Normalized>,
-) -> Expr {
+fn spanned_union(span1: Span, span2: Span, x: UnspannedExpr) -> Expr {
Expr::new(x, span1.union(&span2))
}
@@ -845,25 +842,27 @@ impl DhallParser {
[integer_literal(n)] => spanned(input, IntegerLit(n)),
[double_quote_literal(s)] => spanned(input, TextLit(s)),
[single_quote_literal(s)] => spanned(input, TextLit(s)),
+ [record_type_or_literal(e)] => spanned(input, e),
+ [union_type(e)] => spanned(input, e),
[expression(e)] => e,
))
}
- #[alias(expression)]
- fn empty_record_literal(input: ParseInput) -> ParseResult<Expr> {
- Ok(spanned(input, RecordLit(Default::default())))
+ #[alias(record_type_or_literal)]
+ fn empty_record_literal(input: ParseInput) -> ParseResult<UnspannedExpr> {
+ Ok(RecordLit(Default::default()))
}
- #[alias(expression)]
- fn empty_record_type(input: ParseInput) -> ParseResult<Expr> {
- Ok(spanned(input, RecordType(Default::default())))
+ #[alias(record_type_or_literal)]
+ fn empty_record_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
+ Ok(RecordType(Default::default()))
}
- #[alias(expression)]
+ #[alias(record_type_or_literal)]
fn non_empty_record_type_or_literal(
input: ParseInput,
- ) -> ParseResult<Expr> {
- let e = match_nodes!(input.children();
+ ) -> ParseResult<UnspannedExpr> {
+ Ok(match_nodes!(input.children();
[label(first_label), non_empty_record_type(rest)] => {
let (first_expr, mut map) = rest;
map.insert(first_label, first_expr);
@@ -874,8 +873,7 @@ impl DhallParser {
map.insert(first_label, first_expr);
RecordLit(map)
},
- );
- Ok(spanned(input, e))
+ ))
}
fn non_empty_record_type(
@@ -910,13 +908,12 @@ impl DhallParser {
))
}
- #[alias(expression)]
- fn union_type(input: ParseInput) -> ParseResult<Expr> {
+ fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
let map = match_nodes!(input.children();
[empty_union_type(_)] => Default::default(),
[union_type_entry(entries)..] => entries.collect(),
);
- Ok(spanned(input, UnionType(map)))
+ Ok(UnionType(map))
}
fn empty_union_type(_input: ParseInput) -> ParseResult<()> {
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
index 4dfdcf5..522e1a2 100644
--- a/dhall/tests/type-errors/hurkensParadox.txt
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -1 +1,15 @@
-Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:6:23
+ |
+ 1 | let bottom : Type = ∀(any : Type) → any
+ 2 |
+ 3 | in let not : Type → Type = λ(p : Type) → p → bottom
+ 4 |
+...
+10 | : pow (pow U) → U
+11 | = λ(t : pow (pow U))
+ | ^^^ this expects an argument of type: Kind
+ | ^ but this has type: Sort
+ |
+ = note: expected type `Kind`
+ found type `Sort`
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
index 87cf48e..e4584f5 100644
--- a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable ``_``
+ --> <current file>:1:46
+ |
+1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+ | ^ not found in this scope
+ |
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
index 8d101c3..01facbc 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:1
+ |
+1 | (λ(_ : Natural) → _) True
+ | ^^^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+ | ^^^^ but this has type: Bool
+ |
+ = note: expected type `Natural`
+ found type `Bool`
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
index a72e120..f779fd6 100644
--- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: apply to not Pi
+Type error: Unhandled error: error: expected function, found `Bool`
+ --> <current file>:1:0
+ |
+1 | True True
+ | ^^^^ function application requires a function
+ |
diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
index a13fb3a..3fc1652 100644
--- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -1 +1,7 @@
-[unknown location] Type error: Invalid function input
+Type error: Unhandled error: error: Invalid input type: `Natural`
+ --> <current file>:1:6
+ |
+1 | λ(_ : 1) → _
+ | ^ this has type: `Natural`
+ |
+ = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
index a13fb3a..948c6c7 100644
--- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -1 +1,7 @@
-[unknown location] Type error: Invalid function input
+Type error: Unhandled error: error: Invalid input type: `Natural`
+ --> <current file>:1:0
+ |
+1 | 2 → _
+ | ^ this has type: `Natural`
+ |
+ = help: The input type of a function must have type `Type`, `Kind` or `Sort`
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
index 070e461..aa7c8c5 100644
--- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:5
+ |
+1 | [] : List Type
+ | ^^^^ this expects an argument of type: Type
+ | ^^^^ but this has type: Kind
+ |
+ = note: expected type `Type`
+ found type `Kind`
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
index f1cdf92..053a054 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: NotAFunction
+Type error: Unhandled error: error: merge handler is not a function
+ --> <current file>:1:0
+ |
+1 | merge { x = True } (< x : Bool >.x True)
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+ | ^^^^^^^^^^^^ the handler for `x` has type: `Bool`
+ | ------------------- help: the corresponding variant has type: `Bool`
+ |
+ = help: a handler for this variant must be a function that takes an input of type: `Bool`
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
index 8b729a4..faca63a 100644
--- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -1 +1,8 @@
-Type error: Unhandled error: MergeHandlerTypeMismatch
+Type error: Unhandled error: error: Wrong handler input type
+ --> <current file>:1:0
+ |
+1 | merge { x = λ(_ : Bool) → _ } (< x : Natural >.x 1)
+ | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ in this merge expression
+ | ^^^^^^^^^^^^^^^^^^^^^^^ the handler for `x` expects a value of type: `Bool`
+ | ^^^^^^^^^^^^^^^^^^^ but the corresponding variant has type: `Natural`
+ |
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
index 8d101c3..7e410c4 100644
--- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -1 +1,9 @@
-Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural
+Type error: Unhandled error: error: wrong type of function argument
+ --> <current file>:1:0
+ |
+1 | Natural/subtract True True
+ | ^^^^^^^^^^^^^^^^ this expects an argument of type: Natural
+ | ^^^^ but this has type: Bool
+ |
+ = note: expected type `Natural`
+ found type `Bool`
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
index 87cf48e..a234f9f 100644
--- a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable `constructors`
+ --> <current file>:1:0
+ |
+1 | constructors < Left : Natural | Right : Bool >
+ | ^^^^^^^^^^^^ not found in this scope
+ |
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
index 87cf48e..52baa7f 100644
--- a/dhall/tests/type-errors/unit/VariableFree.txt
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -1 +1,6 @@
-Type error: Unhandled error: unbound variable
+Type error: Unhandled error: error: unbound variable `x`
+ --> <current file>:1:0
+ |
+1 | x
+ | ^ not found in this scope
+ |
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index 0381fec..7bf6d30 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -181,8 +181,8 @@ pub use value::Value;
// A Dhall value.
#[doc(hidden)]
pub mod value {
- use dhall::{Normalized, NormalizedExpr, Parsed};
use dhall::syntax::Builtin;
+ use dhall::{Normalized, NormalizedExpr, Parsed};
use super::de::{Error, Result};
diff --git a/serde_dhall/src/serde.rs b/serde_dhall/src/serde.rs
index 336330a..3e78987 100644
--- a/serde_dhall/src/serde.rs
+++ b/serde_dhall/src/serde.rs
@@ -4,8 +4,8 @@ use serde::de::value::{
MapAccessDeserializer, MapDeserializer, SeqDeserializer,
};
-use dhall::NormalizedExpr;
use dhall::syntax::ExprKind;
+use dhall::NormalizedExpr;
use crate::de::{Deserialize, Error, Result};
use crate::Value;
diff --git a/tests_buffer b/tests_buffer
index 34210a9..87d73ef 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -51,6 +51,8 @@ success/
let X = 0 in λ(T : Type) → λ(x : T) → 1
(λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
failure/
+ \(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
+ \(x: let x = 1 in Sort) -> 0
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x