From b68c3af578d1f6b0d1e32e7d88ef57774fb468d8 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 11:20:32 +0000 Subject: Capture absence of span in Span itself --- dhall/src/core/valuef.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 4e457e6..e5d0807 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -1,12 +1,13 @@ use std::collections::HashMap; use dhall_syntax::{ - rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, }; use crate::core::value::{ToExprOptions, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::phase::typecheck::rc; use crate::phase::{Normalized, NormalizedExpr}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are -- cgit v1.3.1 From 5d5a356b8eb36e277c312e5550d1cb0a2f82e9fa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 11:34:29 +0000 Subject: Store a `Span` in `Value` --- dhall/src/core/value.rs | 23 +++++++++++++++++++---- dhall/src/phase/typecheck.rs | 14 ++++++++++---- dhall_syntax/src/core/span.rs | 3 +++ 3 files changed, 32 insertions(+), 8 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index b4b6b08..b6c156e 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,7 +1,7 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::{Builtin, Const}; +use dhall_syntax::{Builtin, Const, Span}; use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; @@ -36,6 +36,7 @@ struct ValueInternal { value: ValueF, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, + span: Span, } /// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, @@ -69,18 +70,21 @@ impl ValueInternal { form: Unevaled, value: ValueF::Const(Const::Type), ty: None, + span: Span::Artificial, }, |vint| match (&vint.form, &vint.ty) { (Unevaled, Some(ty)) => ValueInternal { form: WHNF, value: normalize_whnf(vint.value, &ty), ty: vint.ty, + span: vint.span, }, // `value` is `Sort` (Unevaled, None) => ValueInternal { form: NF, value: ValueF::Const(Const::Sort), ty: None, + span: vint.span, }, // Already in WHNF (WHNF, _) | (NF, _) => vint, @@ -113,11 +117,12 @@ impl ValueInternal { } impl Value { - fn new(value: ValueF, form: Form, ty: Value) -> Value { + fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, value, ty: Some(ty), + span, } .into_value() } @@ -126,14 +131,22 @@ impl Value { form: NF, value: ValueF::Const(Const::Sort), ty: None, + span: Span::Artificial, } .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - Value::new(v, Unevaled, t) + Value::new(v, Unevaled, t, Span::PlaceHolder) + } + pub(crate) fn from_valuef_and_type_and_span( + v: ValueF, + t: Value, + span: Span, + ) -> Value { + Value::new(v, Unevaled, t, span) } pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { - Value::new(v, WHNF, t) + Value::new(v, WHNF, t, Span::PlaceHolder) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -258,6 +271,7 @@ impl Shift for ValueInternal { form: self.form, value: self.value.shift(delta, var)?, ty: self.ty.shift(delta, var)?, + span: self.span.clone(), }) } } @@ -285,6 +299,7 @@ impl Subst for ValueInternal { form: Unevaled, value: self.value.subst_shift(var, val), ty: self.ty.subst_shift(var, val), + span: self.span.clone(), } } } diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 4d8c7d3..63f5157 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -304,6 +304,7 @@ fn type_with( e: Expr, ) -> Result { use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var}; + let span = e.span(); Ok(match e.as_ref() { Lam(var, annot, body) => { @@ -348,7 +349,7 @@ fn type_with( |e| type_with(ctx, e.clone()), |_, _| unreachable!(), )?; - type_last_layer(ctx, expr)? + type_last_layer(ctx, expr, span)? } }) } @@ -358,6 +359,7 @@ fn type_with( fn type_last_layer( ctx: &TypecheckContext, e: ExprF, + span: Span, ) -> Result { use crate::error::TypeMessage::*; use dhall_syntax::BinOp::*; @@ -584,6 +586,7 @@ fn type_last_layer( l.get_type()?, r.get_type()?, ), + Span::PlaceHolder, )?), BinOp(RecursiveRecordTypeMerge, l, r) => { use crate::phase::normalize::merge_maps; @@ -619,6 +622,7 @@ fn type_last_layer( l.clone(), r.clone(), ), + Span::PlaceHolder, ) }, )?; @@ -786,9 +790,11 @@ fn type_last_layer( }; Ok(match ret { - RetTypeOnly(typ) => { - Value::from_valuef_and_type(ValueF::PartialExpr(e), typ) - } + RetTypeOnly(typ) => Value::from_valuef_and_type_and_span( + ValueF::PartialExpr(e), + typ, + span, + ), RetWhole(v) => v, }) } diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs index fc8de6e..fa89c30 100644 --- a/dhall_syntax/src/core/span.rs +++ b/dhall_syntax/src/core/span.rs @@ -22,6 +22,9 @@ pub enum Span { Decoded, /// For expressions constructed during normalization/typecheck Artificial, + /// For when there should be a span but it's not done yet + /// TODO: properly handle spans + PlaceHolder, } impl Span { -- cgit v1.3.1 From d28d114552e6c6cb913dce48893fa87e87bf11e2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 13:36:30 +0000 Subject: Propagate more spans --- dhall/src/core/value.rs | 8 ++++++-- dhall/src/phase/typecheck.rs | 6 +++--- dhall_syntax/src/core/span.rs | 3 --- 3 files changed, 9 insertions(+), 8 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index b6c156e..61c7015 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -136,7 +136,7 @@ impl Value { .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - Value::new(v, Unevaled, t, Span::PlaceHolder) + Value::new(v, Unevaled, t, Span::Artificial) } pub(crate) fn from_valuef_and_type_and_span( v: ValueF, @@ -146,7 +146,7 @@ impl Value { Value::new(v, Unevaled, t, span) } pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { - Value::new(v, WHNF, t, Span::PlaceHolder) + Value::new(v, WHNF, t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -154,6 +154,10 @@ impl Value { pub(crate) fn from_builtin(b: Builtin) -> Self { builtin_to_value(b) } + pub(crate) fn with_span(self, span: Span) -> Self { + self.as_internal_mut().span = span; + self + } pub(crate) fn as_const(&self) -> Option { match &*self.as_whnf() { diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 9d2c69b..33919e4 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -586,7 +586,7 @@ fn type_last_layer( l.get_type()?, r.get_type()?, ), - Span::PlaceHolder, + Span::Artificial, )?), BinOp(RecursiveRecordTypeMerge, l, r) => { use crate::phase::normalize::merge_maps; @@ -622,7 +622,7 @@ fn type_last_layer( l.clone(), r.clone(), ), - Span::PlaceHolder, + Span::Artificial, ) }, )?; @@ -795,7 +795,7 @@ fn type_last_layer( typ, span, ), - RetWhole(v) => v, + RetWhole(v) => v.with_span(span), }) } diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs index e2bf26d..d10a53d 100644 --- a/dhall_syntax/src/core/span.rs +++ b/dhall_syntax/src/core/span.rs @@ -22,9 +22,6 @@ pub enum Span { Decoded, /// For expressions constructed during normalization/typecheck Artificial, - /// For when there should be a span but it's not done yet - /// TODO: properly handle spans - PlaceHolder, } impl Span { -- cgit v1.3.1 From c9c248a4cab21fa1ae7692cd193e3b2c698d431d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 13:49:47 +0000 Subject: Add a few more pretty errors --- dhall/src/core/value.rs | 3 +++ dhall/src/error/mod.rs | 16 ++++++++-------- dhall/tests/type-errors/hurkensParadox.txt | 2 +- .../unit/FunctionApplicationArgumentNotMatch.txt | 2 +- .../unit/FunctionApplicationIsNotFunction.txt | 7 ++++++- .../type-errors/unit/FunctionArgumentTypeNotAType.txt | 7 ++++++- .../unit/FunctionTypeArgumentTypeNotAType.txt | 7 ++++++- dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt | 7 ++++++- dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt | 2 +- .../unit/MergeHandlerNotMatchAlternativeType.txt | 2 +- .../tests/type-errors/unit/NaturalSubtractNotNatural.txt | 7 ++++++- dhall_syntax/src/core/span.rs | 2 +- 12 files changed, 46 insertions(+), 18 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 61c7015..d4f5131 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -165,6 +165,9 @@ impl Value { _ => None, } } + pub(crate) fn span(&self) -> Span { + self.as_internal().span.clone() + } fn as_internal(&self) -> Ref { self.0.borrow() diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 02e8ed3..4d59cbb 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -104,16 +104,16 @@ impl std::fmt::Display for TypeError { use TypeMessage::*; let msg = match &self.message { UnboundVariable(span) => span.error("Type error: Unbound variable"), - InvalidInputType(_) => { - "Type error: Invalid function input".to_string() + InvalidInputType(v) => { + v.span().error("Type error: Invalid function input") } - InvalidOutputType(_) => { - "Type error: Invalid function output".to_string() - } - NotAFunction(_) => "Type error: Not a function".to_string(), - TypeMismatch(_, _, _) => { - "Type error: Wrong type of function argument".to_string() + InvalidOutputType(v) => { + v.span().error("Type error: Invalid function output") } + NotAFunction(v) => v.span().error("Type error: Not a function"), + TypeMismatch(v, _, _) => v + .span() + .error("Type error: Wrong type of function argument"), _ => "Type error: Unhandled error".to_string(), }; write!(f, "{}", msg) diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt index ab75f15..69428b8 100644 --- a/dhall/tests/type-errors/hurkensParadox.txt +++ b/dhall/tests/type-errors/hurkensParadox.txt @@ -1 +1 @@ -Type error: Wrong type of function argument +[unknown location] Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt index ab75f15..69428b8 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt @@ -1 +1 @@ -Type error: Wrong type of function argument +[unknown location] Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt index 4757d2d..062f9de 100644 --- a/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt +++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt @@ -1 +1,6 @@ -Type error: Not a function + --> 1:1 + | +1 | True True␊ + | ^--^ + | + = Type error: Not a function diff --git a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt index faea460..9e43c33 100644 --- a/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt @@ -1 +1,6 @@ -Type error: Invalid function input + --> 1:7 + | +1 | λ(_ : 1) → _␊ + | ^ + | + = Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt index faea460..dd2e758 100644 --- a/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt +++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt @@ -1 +1,6 @@ -Type error: Invalid function input + --> 1:1 + | +1 | 2 → _␊ + | ^ + | + = Type error: Invalid function input diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt index ab75f15..bc5cc40 100644 --- a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt +++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt @@ -1 +1,6 @@ -Type error: Wrong type of function argument + --> 1:6 + | +1 | [] : List Type␊ + | ^--^ + | + = Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt index 4757d2d..c5ed223 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt @@ -1 +1 @@ -Type error: Not a function +[unknown location] Type error: Not a function diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt index ab75f15..69428b8 100644 --- a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt +++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt @@ -1 +1 @@ -Type error: Wrong type of function argument +[unknown location] Type error: Wrong type of function argument diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt index ab75f15..fd906bf 100644 --- a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt +++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt @@ -1 +1,6 @@ -Type error: Wrong type of function argument + --> 1:1 + | +1 | Natural/subtract True True␊ + | ^--------------^ + | + = Type error: Wrong type of function argument diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs index 4012cfb..d63a619 100644 --- a/dhall_syntax/src/core/span.rs +++ b/dhall_syntax/src/core/span.rs @@ -69,7 +69,7 @@ impl Span { let message: String = message.into(); let span = match self { self::Span::Parsed(span) => span, - _ => return format!("Unknown location: {}", message), + _ => return format!("[unknown location] {}", message), }; let span = Span::new(&*span.input, span.start, span.end).unwrap(); let err: ErrorVariant = ErrorVariant::CustomError { message }; -- cgit v1.3.1