summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril Feneanar2019-11-11 17:01:02 +0100
committerGitHub2019-11-11 17:01:02 +0100
commit84cd6f386d6f4c7952fbc1da87dcd754f26ee404 (patch)
treed348f580a00c4b97f04f3a2e41ea2a23d67af824
parentf58ff637c8d53af1fcee43bfba5a9f8de799084c (diff)
parent8b566b2575096562c2e15d6ac9ee8750db2cf14f (diff)
Merge pull request #114 from Nadrieril/nice-type-errors
Ground work for pretty type errors
Diffstat (limited to '')
-rw-r--r--dhall/build.rs29
-rw-r--r--dhall/src/core/value.rs30
-rw-r--r--dhall/src/core/valuef.rs3
-rw-r--r--dhall/src/error/mod.rs69
-rw-r--r--dhall/src/phase/binary.rs10
-rw-r--r--dhall/src/phase/typecheck.rs24
-rw-r--r--dhall/src/tests.rs68
-rw-r--r--dhall/tests/type-errors/hurkensParadox.txt1
-rw-r--r--dhall/tests/type-errors/mixedUnions.txt1
-rw-r--r--dhall/tests/type-errors/recordOfKind.txt1
-rw-r--r--dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt1
-rw-r--r--dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt1
-rw-r--r--dhall/tests/type-errors/unit/AssertAlphaTrap.txt6
-rw-r--r--dhall/tests/type-errors/unit/AssertNotEquivalence.txt1
-rw-r--r--dhall/tests/type-errors/unit/AssertTriviallyFalse.txt1
-rw-r--r--dhall/tests/type-errors/unit/EquivalenceNotSameType.txt1
-rw-r--r--dhall/tests/type-errors/unit/EquivalenceNotTerms.txt1
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt1
-rw-r--r--dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt6
-rw-r--r--dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt6
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt6
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeKindSort.txt1
-rw-r--r--dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt1
-rw-r--r--dhall/tests/type-errors/unit/IfBranchesNotMatch.txt1
-rw-r--r--dhall/tests/type-errors/unit/IfBranchesNotType.txt1
-rw-r--r--dhall/tests/type-errors/unit/IfNotBool.txt1
-rw-r--r--dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt1
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt6
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralNotType.txt1
-rw-r--r--dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeAnnotationNotType.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeLhsNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeMissingHandler1.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeMissingHandler2.txt1
-rw-r--r--dhall/tests/type-errors/unit/MergeRhsNotUnion.txt1
-rw-r--r--dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt6
-rw-r--r--dhall/tests/type-errors/unit/OperatorAndNotBool.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorEqualNotBool.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorOrNotBool.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt1
-rw-r--r--dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt1
-rw-r--r--dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt1
-rw-r--r--dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordMixedKinds3.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordProjectionEmpty.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordSelectionEmpty.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecordTypeValueMember.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt1
-rw-r--r--dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt1
-rw-r--r--dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt1
-rw-r--r--dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt1
-rw-r--r--dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt1
-rw-r--r--dhall/tests/type-errors/unit/SomeNotType.txt1
-rw-r--r--dhall/tests/type-errors/unit/Sort.txt1
-rw-r--r--dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt1
-rw-r--r--dhall/tests/type-errors/unit/TypeAnnotationWrong.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt6
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt1
-rw-r--r--dhall/tests/type-errors/unit/UnionTypeNotType.txt1
-rw-r--r--dhall/tests/type-errors/unit/VariableFree.txt6
-rw-r--r--dhall_syntax/src/core/expr.rs53
-rw-r--r--dhall_syntax/src/core/mod.rs2
-rw-r--r--dhall_syntax/src/core/span.rs81
-rw-r--r--dhall_syntax/src/parser.rs14
98 files changed, 385 insertions, 125 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index c7d339c..337480f 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -394,5 +394,34 @@ fn main() -> std::io::Result<()> {
},
)?;
+ make_test_module(
+ &mut file,
+ TestFeature {
+ module_name: "type_error",
+ directory: spec_tests_dir.join("type-inference/failure/"),
+ variant: "TypeError",
+ path_filter: |path: &str| {
+ false
+ // TODO: Enable imports in typecheck tests
+ || path == "importBoundary"
+ || path == "customHeadersUsingBoundVariable"
+ // TODO: projection by expression
+ || path == "unit/RecordProjectionByTypeFieldTypeMismatch"
+ || path == "unit/RecordProjectionByTypeNotPresent"
+ // TODO: toMap
+ || path == "unit/EmptyToMap"
+ || path == "unit/HeterogenousToMap"
+ || path == "unit/MistypedToMap1"
+ || path == "unit/MistypedToMap2"
+ || path == "unit/MistypedToMap3"
+ || path == "unit/MistypedToMap4"
+ || path == "unit/NonRecordToMap"
+ || path == "unit/ToMapWrongKind"
+ },
+ input_type: FileType::Text,
+ output_type: None,
+ },
+ )?;
+
Ok(())
}
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index b4b6b08..d4f5131 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<Value>,
+ 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::Artificial)
+ }
+ 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::Artificial)
}
pub(crate) fn from_const(c: Const) -> Self {
const_to_value(c)
@@ -141,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<Const> {
match &*self.as_whnf() {
@@ -148,6 +165,9 @@ impl Value {
_ => None,
}
}
+ pub(crate) fn span(&self) -> Span {
+ self.as_internal().span.clone()
+ }
fn as_internal(&self) -> Ref<ValueInternal> {
self.0.borrow()
@@ -258,6 +278,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 +306,7 @@ impl Subst<Value> 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/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/error/mod.rs b/dhall/src/error/mod.rs
index 6d4e120..4d59cbb 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;
@@ -41,14 +41,14 @@ pub enum EncodeError {
/// A structured type error that includes context
#[derive(Debug)]
pub struct TypeError {
- type_message: TypeMessage,
+ message: TypeMessage,
context: TypecheckContext,
}
/// The specific type error
#[derive(Debug)]
pub(crate) enum TypeMessage {
- UnboundVariable(V<Label>),
+ UnboundVariable(Span),
InvalidInputType(Value),
InvalidOutputType(Value),
NotAFunction(Value),
@@ -90,58 +90,37 @@ 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(span) => span.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(v, _, _) => v
+ .span()
+ .error("Type error: Wrong type of function argument"),
+ _ => "Type error: 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 +130,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, "{}", err),
}
}
}
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<E>(expr: &Expr<E>) -> Result<Vec<u8>, EncodeError> {
.map_err(|e| EncodeError::CBORError(e))
}
+// Should probably rename this
+pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
+ Expr::new(x, Span::Decoded)
+}
+
fn cbor_value_to_dhall(data: &cbor::Value) -> Result<DecodedExpr, DecodeError> {
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..33919e4 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<E>(x: RawExpr<E>) -> Expr<E> {
+ Expr::new(x, Span::Artificial)
+}
+
// Ad-hoc macro to help construct the types of builtins
macro_rules! make_type {
(Type) => { ExprF::Const(Const::Type) };
@@ -300,6 +304,7 @@ fn type_with(
e: Expr<Normalized>,
) -> Result<Value, TypeError> {
use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
+ let span = e.span();
Ok(match e.as_ref() {
Lam(var, annot, body) => {
@@ -334,7 +339,7 @@ fn type_with(
None => {
return Err(TypeError::new(
ctx,
- TypeMessage::UnboundVariable(var.clone()),
+ TypeMessage::UnboundVariable(span),
))
}
},
@@ -344,7 +349,7 @@ fn type_with(
|e| type_with(ctx, e.clone()),
|_, _| unreachable!(),
)?;
- type_last_layer(ctx, expr)?
+ type_last_layer(ctx, expr, span)?
}
})
}
@@ -354,6 +359,7 @@ fn type_with(
fn type_last_layer(
ctx: &TypecheckContext,
e: ExprF<Value, Normalized>,
+ span: Span,
) -> Result<Value, TypeError> {
use crate::error::TypeMessage::*;
use dhall_syntax::BinOp::*;
@@ -580,6 +586,7 @@ fn type_last_layer(
l.get_type()?,
r.get_type()?,
),
+ Span::Artificial,
)?),
BinOp(RecursiveRecordTypeMerge, l, r) => {
use crate::phase::normalize::merge_maps;
@@ -615,6 +622,7 @@ fn type_last_layer(
l.clone(),
r.clone(),
),
+ Span::Artificial,
)
},
)?;
@@ -782,10 +790,12 @@ fn type_last_layer(
};
Ok(match ret {
- RetTypeOnly(typ) => {
- Value::from_valuef_and_type(ValueF::PartialExpr(e), typ)
- }
- RetWhole(v) => v,
+ RetTypeOnly(typ) => Value::from_valuef_and_type_and_span(
+ ValueF::PartialExpr(e),
+ typ,
+ span,
+ ),
+ RetWhole(v) => v.with_span(span),
})
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index b98489f..1037ef9 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -20,8 +20,31 @@ right: `{}`"#,
}};
}
+/// Wrapper around string slice that makes debug output `{:?}` to print string same way as `{}`.
+/// Used in different `assert*!` macros in combination with `pretty_assertions` crate to make
+/// test failures to show nice diffs.
+#[derive(PartialEq, Eq)]
+#[doc(hidden)]
+pub struct PrettyString(String);
+
+/// Make diff to display string as multi-line string
+impl std::fmt::Debug for PrettyString {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
+ f.write_str(&self.0)
+ }
+}
+
+macro_rules! assert_eq_pretty_str {
+ ($left:expr, $right:expr) => {
+ assert_eq_pretty!(
+ PrettyString($left.to_string()),
+ PrettyString($right.to_string())
+ );
+ };
+}
+
use std::fs::File;
-use std::io::Read;
+use std::io::{Read, Write};
use std::path::PathBuf;
use crate::error::{Error, Result};
@@ -40,6 +63,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 +168,41 @@ 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();
+ }
+ // Checks the output of the type error against a text file. If the text file doesn't exist,
+ // we instead write to it the output we got. This makes it easy to update those files: just
+ // `rm -r dhall/tests/type-errors` and run the tests again.
+ 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_str!(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) => {
diff --git a/dhall/tests/type-errors/hurkensParadox.txt b/dhall/tests/type-errors/hurkensParadox.txt
new file mode 100644
index 0000000..69428b8
--- /dev/null
+++ b/dhall/tests/type-errors/hurkensParadox.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/mixedUnions.txt b/dhall/tests/type-errors/mixedUnions.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/mixedUnions.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/recordOfKind.txt b/dhall/tests/type-errors/recordOfKind.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/recordOfKind.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldName.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AnnotationRecordWrongFieldType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AssertAlphaTrap.txt b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
new file mode 100644
index 0000000..2969c18
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertAlphaTrap.txt
@@ -0,0 +1,6 @@
+ --> 1:47
+ |
+1 | assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)␊
+ | ^
+ |
+ = Type error: Unbound variable
diff --git a/dhall/tests/type-errors/unit/AssertNotEquivalence.txt b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertNotEquivalence.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/AssertTriviallyFalse.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EquivalenceNotSameType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/EquivalenceNotTerms.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
new file mode 100644
index 0000000..69428b8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionApplicationArgumentNotMatch.txt
@@ -0,0 +1 @@
+[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
new file mode 100644
index 0000000..062f9de
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionApplicationIsNotFunction.txt
@@ -0,0 +1,6 @@
+ --> 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
new file mode 100644
index 0000000..9e43c33
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionArgumentTypeNotAType.txt
@@ -0,0 +1,6 @@
+ --> 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
new file mode 100644
index 0000000..dd2e758
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeArgumentTypeNotAType.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+ |
+1 | 2 → _␊
+ | ^
+ |
+ = Type error: Invalid function input
diff --git a/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeKindSort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/FunctionTypeTypeSort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfBranchesNotMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/IfBranchesNotType.txt b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfBranchesNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/IfNotBool.txt b/dhall/tests/type-errors/unit/IfNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/IfNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/LetWithWrongAnnotation.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
new file mode 100644
index 0000000..bc5cc40
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralEmptyNotType.txt
@@ -0,0 +1,6 @@
+ --> 1:6
+ |
+1 | [] : List Type␊
+ | ^--^
+ |
+ = Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/ListLiteralNotType.txt b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/ListLiteralTypesNotMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAlternativeHasNoHandler.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAnnotationMismatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeAnnotationNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation1.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyNeedsDirectAnnotation2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeEmptyWithoutAnnotation.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerFreeVar.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
new file mode 100644
index 0000000..c5ed223
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotFunction.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Not a function
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotInUnion.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
new file mode 100644
index 0000000..69428b8
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlerNotMatchAlternativeType.txt
@@ -0,0 +1 @@
+[unknown location] Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeHandlersWithDifferentType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler1.txt b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler1.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeMissingHandler2.txt b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeMissingHandler2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/MergeRhsNotUnion.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
new file mode 100644
index 0000000..fd906bf
--- /dev/null
+++ b/dhall/tests/type-errors/unit/NaturalSubtractNotNatural.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+ |
+1 | Natural/subtract True True␊
+ | ^--------------^
+ |
+ = Type error: Wrong type of function argument
diff --git a/dhall/tests/type-errors/unit/OperatorAndNotBool.txt b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorAndNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorEqualNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateLhsNotList.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateListsNotMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateNotListsButMatch.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorListConcatenateRhsNotList.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorNotEqualNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorOrNotBool.txt b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorOrNotBool.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorPlusNotNatural.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateLhsNotText.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTextConcatenateRhsNotText.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OperatorTimesNotNatural.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxAbsent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/OptionalDeprecatedSyntaxPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordLitDuplicateFields.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordMixedKinds3.txt b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionEmpty.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionNotPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordProjectionNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionEmpty.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordSelectionTypeNotUnionType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordTypeDuplicateFields.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecordTypeValueMember.txt b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecordTypeValueMember.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeOverlapping.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeLhsNotRecordType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeOverlapping.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RecursiveRecordTypeMergeRhsNotRecordType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeLhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/RightBiasedRecordMergeRhsNotRecord.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/SomeNotType.txt b/dhall/tests/type-errors/unit/SomeNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/SomeNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/Sort.txt b/dhall/tests/type-errors/unit/Sort.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/Sort.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/TextLiteralInterpolateNotText.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/TypeAnnotationWrong.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionConstructorFieldNotPresent.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
new file mode 100644
index 0000000..9cc0c19
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionDeprecatedConstructorsKeyword.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+ |
+1 | constructors < Left : Natural | Right : Bool >␊
+ | ^----------^
+ |
+ = Type error: Unbound variable
diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants1.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeDuplicateVariants2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds2.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeMixedKinds3.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/UnionTypeNotType.txt b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
new file mode 100644
index 0000000..4b68fea
--- /dev/null
+++ b/dhall/tests/type-errors/unit/UnionTypeNotType.txt
@@ -0,0 +1 @@
+Type error: Unhandled error
diff --git a/dhall/tests/type-errors/unit/VariableFree.txt b/dhall/tests/type-errors/unit/VariableFree.txt
new file mode 100644
index 0000000..a46aac0
--- /dev/null
+++ b/dhall/tests/type-errors/unit/VariableFree.txt
@@ -0,0 +1,6 @@
+ --> 1:1
+ |
+1 | x␊
+ | ^
+ |
+ = Type error: Unbound variable
diff --git a/dhall_syntax/src/core/expr.rs b/dhall_syntax/src/core/expr.rs
index 2ad3ba8..750b58b 100644
--- a/dhall_syntax/src/core/expr.rs
+++ b/dhall_syntax/src/core/expr.rs
@@ -1,5 +1,3 @@
-use std::rc::Rc;
-
use crate::map::{DupTreeMap, DupTreeSet};
use crate::visitor::{self, ExprFMutVisitor, ExprFVisitor};
use crate::*;
@@ -15,40 +13,6 @@ pub fn trivial_result<T>(x: Result<T, !>) -> T {
}
}
-/// A location in the source text
-#[derive(Debug, Clone)]
-pub struct Span {
- input: Rc<str>,
- /// # Safety
- ///
- /// Must be a valid character boundary index into `input`.
- start: usize,
- /// # Safety
- ///
- /// Must be a valid character boundary index into `input`.
- end: usize,
-}
-
-impl Span {
- pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self {
- Span {
- input,
- start: sp.start(),
- end: sp.end(),
- }
- }
- /// Takes the union of the two spans. Assumes that the spans come from the same input.
- /// This will also capture any input between the spans.
- pub fn union(&self, other: &Span) -> Self {
- use std::cmp::{max, min};
- Span {
- input: self.input.clone(),
- start: min(self.start, other.start),
- end: max(self.start, other.start),
- }
- }
-}
-
/// Double with bitwise equality
#[derive(Debug, Copy, Clone)]
pub struct NaiveDouble(f64);
@@ -178,7 +142,7 @@ pub enum Builtin {
// Each node carries an annotation.
#[derive(Debug, Clone)]
-pub struct Expr<Embed>(Box<(RawExpr<Embed>, Option<Span>)>);
+pub struct Expr<Embed>(Box<(RawExpr<Embed>, Span)>);
pub type RawExpr<Embed> = ExprF<Expr<Embed>, Embed>;
@@ -334,16 +298,12 @@ impl<E> Expr<E> {
pub fn as_mut(&mut self) -> &mut RawExpr<E> {
&mut self.0.as_mut().0
}
- pub fn span(&self) -> Option<Span> {
+ pub fn span(&self) -> Span {
self.0.as_ref().1.clone()
}
- pub(crate) fn new(x: RawExpr<E>, n: Span) -> Self {
- Expr(Box::new((x, Some(n))))
- }
-
- pub fn from_expr_no_span(x: RawExpr<E>) -> Self {
- Expr(Box::new((x, None)))
+ pub fn new(x: RawExpr<E>, n: Span) -> Self {
+ Expr(Box::new((x, n)))
}
pub fn rewrap<E2>(&self, x: RawExpr<E2>) -> Expr<E2> {
@@ -388,11 +348,6 @@ impl<E> Expr<E> {
}
}
-// Should probably rename this
-pub fn rc<E>(x: RawExpr<E>) -> Expr<E> {
- Expr::from_expr_no_span(x)
-}
-
/// Add an isize to an usize
/// Panics on over/underflow
fn add_ui(u: usize, i: isize) -> Option<usize> {
diff --git a/dhall_syntax/src/core/mod.rs b/dhall_syntax/src/core/mod.rs
index fe2c0be..66bf229 100644
--- a/dhall_syntax/src/core/mod.rs
+++ b/dhall_syntax/src/core/mod.rs
@@ -4,6 +4,8 @@ mod import;
pub use import::*;
mod label;
pub use label::*;
+mod span;
+pub use span::*;
mod text;
pub use text::*;
pub mod context;
diff --git a/dhall_syntax/src/core/span.rs b/dhall_syntax/src/core/span.rs
new file mode 100644
index 0000000..f9c7008
--- /dev/null
+++ b/dhall_syntax/src/core/span.rs
@@ -0,0 +1,81 @@
+use std::rc::Rc;
+
+/// A location in the source text
+#[derive(Debug, Clone)]
+pub struct ParsedSpan {
+ input: Rc<str>,
+ /// # Safety
+ ///
+ /// Must be a valid character boundary index into `input`.
+ start: usize,
+ /// # Safety
+ ///
+ /// Must be a valid character boundary index into `input`.
+ end: usize,
+}
+
+#[derive(Debug, Clone)]
+pub enum Span {
+ /// A location in the source text
+ Parsed(ParsedSpan),
+ /// For expressions obtained from decoding binary
+ Decoded,
+ /// For expressions constructed during normalization/typecheck
+ Artificial,
+}
+
+impl Span {
+ pub(crate) fn make(input: Rc<str>, sp: pest::Span) -> Self {
+ Span::Parsed(ParsedSpan {
+ input,
+ start: sp.start(),
+ end: sp.end(),
+ })
+ }
+
+ /// Takes the union of the two spans, i.e. the range of input covered by the two spans plus any
+ /// input between them. Assumes that the spans come from the same input. Fails if one of the
+ /// spans does not point to an input location.
+ pub fn union(&self, other: &Span) -> Self {
+ use std::cmp::{max, min};
+ use Span::*;
+ match (self, other) {
+ (Parsed(x), Parsed(y)) if Rc::ptr_eq(&x.input, &y.input) => {
+ Parsed(ParsedSpan {
+ input: x.input.clone(),
+ start: min(x.start, y.start),
+ end: max(x.end, y.end),
+ })
+ }
+ _ => panic!(
+ "Tried to union incompatible spans: {:?} and {:?}",
+ self, other
+ ),
+ }
+ }
+
+ /// Merges two spans assumed to point to a similar thing. If only one of them points to an
+ /// input location, use that one.
+ pub fn merge(&self, other: &Span) -> Self {
+ use Span::*;
+ match (self, other) {
+ (Parsed(x), _) | (_, Parsed(x)) => Parsed(x.clone()),
+ (Artificial, _) | (_, Artificial) => Artificial,
+ (Decoded, Decoded) => Decoded,
+ }
+ }
+
+ pub fn error(&self, message: impl Into<String>) -> String {
+ use pest::error::{Error, ErrorVariant};
+ use pest::Span;
+ let message: String = message.into();
+ let span = match self {
+ self::Span::Parsed(span) => span,
+ _ => return format!("[unknown location] {}", message),
+ };
+ let span = Span::new(&*span.input, span.start, span.end).unwrap();
+ let err: ErrorVariant<!> = ErrorVariant::CustomError { message };
+ let err = Error::new_from_span(err, span);
+ format!("{}", err)
+ }
+}
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 83f62ee..eaded50 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -650,7 +650,7 @@ impl DhallParser {
final_expr,
|acc, x| {
spanned_union(
- acc.span().unwrap(),
+ acc.span(),
x.3,
Let(x.0, x.1, x.2, acc)
)
@@ -717,11 +717,7 @@ impl DhallParser {
r => Err(op.error(format!("Rule {:?} isn't an operator", r)))?,
};
- Ok(spanned_union(
- l.span().unwrap(),
- r.span().unwrap(),
- BinOp(op, l, r),
- ))
+ Ok(spanned_union(l.span(), r.span(), BinOp(op, l, r)))
}
fn Some_(_input: ParseInput) -> ParseResult<()> {
@@ -739,8 +735,8 @@ impl DhallParser {
first,
|acc, e| {
spanned_union(
- acc.span().unwrap(),
- e.span().unwrap(),
+ acc.span(),
+ e.span(),
App(acc, e)
)
}
@@ -778,7 +774,7 @@ impl DhallParser {
first,
|acc, e| {
spanned_union(
- acc.span().unwrap(),
+ acc.span(),
e.1,
match e.0 {
Either::Left(l) => Field(acc, l),