summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
authorNadrieril2020-02-01 22:04:34 +0000
committerNadrieril2020-02-01 22:04:34 +0000
commit70eede4fd012f49dfab0e2e27fb3a4e4bbff6325 (patch)
treef9b4a75b5ffc878f6d5e5a40bd7c13c8de94a9f9 /dhall/src/semantics
parent72a6fef65bb3d34be1f501a1f6de66fb8a54fa04 (diff)
Implement once nice error using annotate_snippets
Diffstat (limited to 'dhall/src/semantics')
-rw-r--r--dhall/src/semantics/nze/value.rs4
-rw-r--r--dhall/src/semantics/tck/typecheck.rs54
2 files changed, 36 insertions, 22 deletions
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index ae06942..d97b8c4 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -6,6 +6,7 @@ use crate::semantics::nze::lazy;
use crate::semantics::Binder;
use crate::semantics::{
apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
+ TyEnv,
};
use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
@@ -192,6 +193,9 @@ impl Value {
self.to_tyexpr_noenv().to_expr(opts)
}
+ pub(crate) fn to_expr_tyenv(&self, env: &TyEnv) -> NormalizedExpr {
+ self.to_tyexpr(env.as_varenv()).to_expr_tyenv(env)
+ }
pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind {
self.kind().clone()
}
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 20076cd..a652663 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -2,7 +2,7 @@ use std::borrow::Cow;
use std::cmp::max;
use std::collections::HashMap;
-use crate::error::{TypeError, TypeMessage};
+use crate::error::{ErrorBuilder, TypeError, TypeMessage};
use crate::semantics::merge_maps;
use crate::semantics::{
type_of_builtin, Binder, BuiltinClosure, Closure, TyEnv, TyExpr,
@@ -57,6 +57,7 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
fn type_one_layer(
env: &TyEnv,
kind: &ExprKind<TyExpr, Normalized>,
+ span: Span,
) -> Result<Type, TypeError> {
Ok(match kind {
ExprKind::Import(..) => unreachable!(
@@ -252,27 +253,35 @@ fn type_one_layer(
}
t
}
- ExprKind::App(f, arg) => {
- match f.get_type()?.kind() {
- ValueKind::PiClosure { annot, closure, .. } => {
- if arg.get_type()? != *annot {
- // return mkerr(format!("function annot mismatch"));
- return mkerr(format!(
- "function annot mismatch: ({} : {}) : {}",
- arg.to_expr_tyenv(env),
- arg.get_type()?
- .to_tyexpr(env.as_varenv())
- .to_expr_tyenv(env),
- annot.to_tyexpr(env.as_varenv()).to_expr_tyenv(env),
- ));
- }
-
- let arg_nf = arg.eval(env.as_nzenv());
- closure.apply(arg_nf)
+ ExprKind::App(f, arg) => match f.get_type()?.kind() {
+ ValueKind::PiClosure { annot, closure, .. } => {
+ if arg.get_type()? != *annot {
+ let mut builder = ErrorBuilder::span_err(
+ &span,
+ format!("function annot mismatch",),
+ );
+ builder.annotate_info(
+ &f.span(),
+ format!(
+ "this expects an argument of type: {}",
+ annot.to_expr_tyenv(env),
+ ),
+ );
+ builder.annotate_info(
+ &arg.span(),
+ format!(
+ "but this has type: {}",
+ arg.get_type()?.to_expr_tyenv(env),
+ ),
+ );
+ return mkerr(builder.format());
}
- _ => return mkerr(format!("apply to not Pi")),
+
+ let arg_nf = arg.eval(env.as_nzenv());
+ closure.apply(arg_nf)
}
- }
+ _ => return mkerr(format!("apply to not Pi")),
+ },
ExprKind::BoolIf(x, y, z) => {
if *x.get_type()?.kind() != ValueKind::from_builtin(Builtin::Bool) {
return mkerr("InvalidPredicate");
@@ -323,7 +332,7 @@ fn type_one_layer(
x.get_type()?.to_tyexpr(env.as_varenv()),
y.get_type()?.to_tyexpr(env.as_varenv()),
);
- let ty = type_one_layer(env, &ekind)?;
+ let ty = type_one_layer(env, &ekind, Span::Artificial)?;
TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
.eval(env.as_nzenv())
}
@@ -347,6 +356,7 @@ fn type_one_layer(
tx.to_tyexpr(env.as_varenv()),
ty.to_tyexpr(env.as_varenv()),
),
+ Span::Artificial,
)?;
}
}
@@ -588,7 +598,7 @@ pub(crate) fn type_with(
}
ekind => {
let ekind = ekind.traverse_ref(|e| type_with(env, e))?;
- let ty = type_one_layer(env, &ekind)?;
+ let ty = type_one_layer(env, &ekind, expr.span())?;
(TyExprKind::Expr(ekind), Some(ty))
}
};