summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-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
6 files changed, 137 insertions, 67 deletions
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) => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 13:54:43 +0000