diff options
-rw-r--r-- | Cargo.lock | 7 | ||||
-rw-r--r-- | dhall/Cargo.toml | 3 | ||||
-rw-r--r-- | dhall/src/error/builder.rs | 100 | ||||
-rw-r--r-- | dhall/src/error/mod.rs | 3 | ||||
-rw-r--r-- | dhall/src/semantics/nze/value.rs | 4 | ||||
-rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 54 | ||||
-rw-r--r-- | dhall/src/syntax/ast/span.rs | 30 | ||||
-rw-r--r-- | dhall/tests/type-errors/hurkensParadox.txt | 15 | ||||
-rw-r--r-- | dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt | 9 | ||||
-rw-r--r-- | dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 9 | ||||
-rw-r--r-- | dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt | 9 |
11 files changed, 216 insertions, 27 deletions
@@ -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..e293220 --- /dev/null +++ b/dhall/src/error/builder.rs @@ -0,0 +1,100 @@ +use annotate_snippets::{ + display_list::DisplayList, + formatter::DisplayListFormatter, + snippet::{Annotation, AnnotationType, Slice, Snippet, SourceAnnotation}, +}; + +use crate::syntax::Span; + +#[derive(Debug, Clone)] +pub struct ErrorBuilder { + message: String, + annotation_type: AnnotationType, + annotations: Vec<BuilderAnnotation>, +} + +#[derive(Debug, Clone)] +struct BuilderAnnotation { + span: Span, + message: String, + annotation_type: AnnotationType, +} + +/// A builder that uses the annotate_snippets library to display nice error messages about source +/// code locations. +impl ErrorBuilder { + pub fn new(message: String) -> Self { + ErrorBuilder { + message, + annotation_type: AnnotationType::Error, + annotations: Vec::new(), + } + } + pub fn span_err(span: &Span, message: String) -> Self { + let mut builder = Self::new(message.clone()); + builder.annotate_err(span, message); + builder + } + + pub fn annotate_err(&mut self, span: &Span, message: String) { + self.annotations.push(BuilderAnnotation { + span: span.clone(), + message, + annotation_type: AnnotationType::Error, + }) + } + pub fn annotate_info(&mut self, span: &Span, message: String) { + self.annotations.push(BuilderAnnotation { + span: span.clone(), + message, + annotation_type: AnnotationType::Help, + }) + } + + // TODO: handle multiple files + pub fn format(self) -> String { + let mut input = None; + let annotations = self + .annotations + .into_iter() + .filter_map(|annot| { + let span = match annot.span { + Span::Parsed(span) => span, + _ => return None, + }; + if input.is_none() { + input = Some(span.to_input()); + } + Some(SourceAnnotation { + label: annot.message, + annotation_type: annot.annotation_type, + range: span.as_char_range(), + }) + }) + .collect(); + + let input = match input { + Some(input) => input, + None => return format!("[unknown location] {}", self.message), + }; + + let snippet = Snippet { + title: Some(Annotation { + label: Some(self.message), + id: None, + annotation_type: self.annotation_type, + }), + footer: vec![], + slices: vec![Slice { + source: input, + line_start: 1, // TODO + origin: Some("<current file>".to_string()), + fold: true, + annotations, + }], + }; + let dl = DisplayList::from(snippet); + let dlf = DisplayListFormatter::new(true, false); + format!("{}", dlf.format(&dl)) + } +} diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 4df018d..5b7693e 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -5,6 +5,9 @@ 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)] diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs index ae06942..d97b8c4 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}; @@ -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/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs index 20076cd..a652663 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, @@ -57,6 +57,7 @@ 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!( @@ -252,27 +253,35 @@ fn type_one_layer( } t } - ExprKind::App(f, arg) => { - 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), - )); - } - - let arg_nf = arg.eval(env.as_nzenv()); - closure.apply(arg_nf) + ExprKind::App(f, arg) => match f.get_type()?.kind() { + ValueKind::PiClosure { annot, closure, .. } => { + if arg.get_type()? != *annot { + let mut builder = ErrorBuilder::span_err( + &span, + format!("function annot mismatch",), + ); + builder.annotate_info( + &f.span(), + format!( + "this expects an argument of type: {}", + annot.to_expr_tyenv(env), + ), + ); + builder.annotate_info( + &arg.span(), + format!( + "but this has type: {}", + arg.get_type()?.to_expr_tyenv(env), + ), + ); + return mkerr(builder.format()); } - _ => return mkerr(format!("apply to not Pi")), + + let arg_nf = arg.eval(env.as_nzenv()); + closure.apply(arg_nf) } - } + _ => return mkerr(format!("apply to not Pi")), + }, ExprKind::BoolIf(x, y, z) => { if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) { return mkerr("InvalidPredicate"); @@ -323,7 +332,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 +356,7 @@ fn type_one_layer( tx.to_tyexpr(env.as_varenv()), ty.to_tyexpr(env.as_varenv()), ), + Span::Artificial, )?; } } @@ -588,7 +598,7 @@ pub(crate) fn type_with( } ekind => { let ekind = ekind.traverse_ref(|e| type_with(env, e))?; - let ty = type_one_layer(env, &ekind)?; + let ty = type_one_layer(env, &ekind, expr.span())?; (TyExprKind::Expr(ekind), Some(ty)) } }; 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/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index 4dfdcf5..10bb9a4 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1 +1,14 @@ -Type error: Unhandled error: function annot mismatch: (U : Sort) : Kind +Type error: Unhandled error: error: function annot mismatch + --> <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)) + | ^^^^^ function annot mismatch + | --- help: this expects an argument of type: Kind + | - help: but this has type: Sort + | diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index 8d101c3..7aa2281 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1 +1,8 @@ -Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural +Type error: Unhandled error: error: function annot mismatch + --> <current file>:1:1 + | +1 | (λ(_ : Natural) → _) True + | ^^^^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ------------------ help: this expects an argument of type: Natural + | ---- help: but this has type: Bool + | diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index 070e461..3673338 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1 +1,8 @@ -Type error: Unhandled error: function annot mismatch: (Type : Kind) : Type +Type error: Unhandled error: error: function annot mismatch + --> <current file>:1:5 + | +1 | [] : List Type + | ^^^^^^^^^ function annot mismatch + | ---- help: this expects an argument of type: Type + | ---- help: but this has type: Kind + | diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index 8d101c3..795c97c 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1 +1,8 @@ -Type error: Unhandled error: function annot mismatch: (True : Bool) : Natural +Type error: Unhandled error: error: function annot mismatch + --> <current file>:1:0 + | +1 | Natural/subtract True True + | ^^^^^^^^^^^^^^^^^^^^^ function annot mismatch + | ---------------- help: this expects an argument of type: Natural + | ---- help: but this has type: Bool + | |