From 70263bb4535c40ffa73548e3f0b4b574a856d764 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 09:44:24 +0000 Subject: Test type error messages --- dhall/src/tests.rs | 42 ++++++++++++++++++++++++++++++++++-------- 1 file changed, 34 insertions(+), 8 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index b98489f..9790b95 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -21,7 +21,7 @@ right: `{}`"#, } use std::fs::File; -use std::io::Read; +use std::io::{Read, Write}; use std::path::PathBuf; use crate::error::{Error, Result}; @@ -40,6 +40,7 @@ pub enum Test<'a> { ImportFailure(&'a str), TypeInferenceSuccess(&'a str, &'a str), TypeInferenceFailure(&'a str), + TypeError(&'a str), Normalization(&'a str, &'a str), AlphaNormalization(&'a str, &'a str), } @@ -144,13 +145,38 @@ pub fn run_test(test: Test<'_>) -> Result<()> { assert_eq_display!(ty, expected); } TypeInferenceFailure(file_path) => { - let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); - match res { - Err(_) => {} - // If e did typecheck, check that it doesn't have a type - Ok(e) => { - e.get_type().unwrap_err(); - } + let mut res = + parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + if let Ok(e) = &res { + // If e did typecheck, check that get_type fails + res = e.get_type(); + } + res.unwrap_err(); + } + TypeError(file_path) => { + let mut res = + parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + let file_path = PathBuf::from(file_path); + let error_file_path = file_path + .strip_prefix("../dhall-lang/tests/type-inference/failure/") + .unwrap(); + let error_file_path = + PathBuf::from("tests/type-errors/").join(error_file_path); + let error_file_path = error_file_path.with_extension("txt"); + if let Ok(e) = &res { + // If e did typecheck, check that get_type fails + res = e.get_type(); + } + let err: Error = res.unwrap_err().into(); + + if error_file_path.is_file() { + let expected_msg = std::fs::read_to_string(error_file_path)?; + let msg = format!("{}\n", err); + assert_eq_pretty!(msg, expected_msg); + } else { + std::fs::create_dir_all(error_file_path.parent().unwrap())?; + let mut file = File::create(error_file_path)?; + writeln!(file, "{}", err)?; } } Normalization(expr_file_path, expected_file_path) => { -- cgit v1.2.3 From 539ab468dfeca7a7b863d5166b2516a2573c044e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 10:33:45 +0000 Subject: Implement basicest Display for TypeError --- dhall/src/error/mod.rs | 61 +++++++++++++++----------------------------------- 1 file changed, 18 insertions(+), 43 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 6d4e120..5338e2d 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -41,7 +41,7 @@ pub enum EncodeError { /// A structured type error that includes context #[derive(Debug)] pub struct TypeError { - type_message: TypeMessage, + message: TypeMessage, context: TypecheckContext, } @@ -90,58 +90,33 @@ pub(crate) enum TypeMessage { impl TypeError { pub(crate) fn new( context: &TypecheckContext, - type_message: TypeMessage, + message: TypeMessage, ) -> Self { TypeError { context: context.clone(), - type_message, + message, } } } -impl std::error::Error for TypeMessage { - fn description(&self) -> &str { +impl std::fmt::Display for TypeError { + fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use TypeMessage::*; - match *self { - // UnboundVariable => "Unbound variable", - InvalidInputType(_) => "Invalid function input", - InvalidOutputType(_) => "Invalid function output", - NotAFunction(_) => "Not a function", - TypeMismatch(_, _, _) => "Wrong type of function argument", - _ => "Unhandled error", - } + let msg = match self.message { + UnboundVariable(_) => "Unbound variable".to_string(), + InvalidInputType(_) => "Invalid function input".to_string(), + InvalidOutputType(_) => "Invalid function output".to_string(), + NotAFunction(_) => "Not a function".to_string(), + TypeMismatch(_, _, _) => { + "Wrong type of function argument".to_string() + } + _ => "Unhandled error".to_string(), + }; + write!(f, "{}", msg) } } -impl std::fmt::Display for TypeMessage { - fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { - match self { - // UnboundVariable(_) => { - // f.write_str(include_str!("errors/UnboundVariable.txt")) - // } - // TypeMismatch(e0, e1, e2) => { - // let template = include_str!("errors/TypeMismatch.txt"); - // let s = template - // .replace("$txt0", &format!("{}", e0.as_expr())) - // .replace("$txt1", &format!("{}", e1.as_expr())) - // .replace("$txt2", &format!("{}", e2.as_expr())) - // .replace( - // "$txt3", - // &format!( - // "{}", - // e2.get_type() - // .unwrap() - // .as_normalized() - // .unwrap() - // .as_expr() - // ), - // ); - // f.write_str(&s) - // } - _ => f.write_str("Unhandled error message"), - } - } -} +impl std::error::Error for TypeError {} impl std::fmt::Display for Error { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { @@ -151,7 +126,7 @@ impl std::fmt::Display for Error { Error::Decode(err) => write!(f, "{:?}", err), Error::Encode(err) => write!(f, "{:?}", err), Error::Resolve(err) => write!(f, "{:?}", err), - Error::Typecheck(err) => write!(f, "{:?}", err), + Error::Typecheck(err) => write!(f, "Type error: {}", err), } } } -- cgit v1.2.3 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 ++- dhall/src/phase/binary.rs | 10 ++++++++-- dhall/src/phase/typecheck.rs | 6 +++++- 3 files changed, 15 insertions(+), 4 deletions(-) (limited to 'dhall/src') 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 diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs index 8c98f77..b4f18da 100644 --- a/dhall/src/phase/binary.rs +++ b/dhall/src/phase/binary.rs @@ -5,8 +5,9 @@ use std::vec; use dhall_syntax::map::DupTreeMap; use dhall_syntax::{ - rc, Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation, - ImportMode, Integer, InterpolatedText, Label, Natural, Scheme, URL, V, + Expr, ExprF, FilePath, FilePrefix, Hash, Import, ImportLocation, + ImportMode, Integer, InterpolatedText, Label, Natural, RawExpr, Scheme, + Span, URL, V, }; use crate::error::{DecodeError, EncodeError}; @@ -24,6 +25,11 @@ pub(crate) fn encode(expr: &Expr) -> Result, EncodeError> { .map_err(|e| EncodeError::CBORError(e)) } +// Should probably rename this +pub fn rc(x: RawExpr) -> Expr { + Expr::new(x, Span::Decoded) +} + fn cbor_value_to_dhall(data: &cbor::Value) -> Result { use cbor::Value::*; use dhall_syntax::{BinOp, Builtin, Const}; diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs index 9013c1f..4d8c7d3 100644 --- a/dhall/src/phase/typecheck.rs +++ b/dhall/src/phase/typecheck.rs @@ -2,7 +2,7 @@ use std::cmp::max; use std::collections::HashMap; use dhall_syntax::{ - rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, + Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, RawExpr, Span, }; use crate::core::context::TypecheckContext; @@ -142,6 +142,10 @@ pub(crate) fn const_to_value(c: Const) -> Value { } } +pub fn rc(x: RawExpr) -> Expr { + Expr::new(x, Span::Artificial) +} + // Ad-hoc macro to help construct the types of builtins macro_rules! make_type { (Type) => { ExprF::Const(Const::Type) }; -- cgit v1.2.3 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 ++++++++++---- 2 files changed, 29 insertions(+), 8 deletions(-) (limited to 'dhall/src') 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, }) } -- cgit v1.2.3 From 330f063e80a51f8f399864f9d01412e1bff34fe9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 11 Nov 2019 12:43:09 +0000 Subject: Display first pretty type error --- dhall/src/error/mod.rs | 8 ++++---- dhall/src/phase/typecheck.rs | 2 +- dhall/src/tests.rs | 25 ++++++++++++++++++++++++- 3 files changed, 29 insertions(+), 6 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/error/mod.rs b/dhall/src/error/mod.rs index 5338e2d..efbd578 100644 --- a/dhall/src/error/mod.rs +++ b/dhall/src/error/mod.rs @@ -1,6 +1,6 @@ use std::io::Error as IOError; -use dhall_syntax::{BinOp, Import, Label, ParseError, V}; +use dhall_syntax::{BinOp, Import, Label, ParseError, Span}; use crate::core::context::TypecheckContext; use crate::core::value::Value; @@ -48,7 +48,7 @@ pub struct TypeError { /// The specific type error #[derive(Debug)] pub(crate) enum TypeMessage { - UnboundVariable(V