diff options
Diffstat (limited to 'dhall/src')
| -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 |
5 files changed, 169 insertions, 22 deletions
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 +} |