summaryrefslogtreecommitdiff
path: root/dhall/src/typecheck.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/typecheck.rs')
-rw-r--r--dhall/src/typecheck.rs126
1 files changed, 70 insertions, 56 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 23ab7a6..c2a2ca3 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -10,7 +10,7 @@ use dhall_core::core::Builtin::*;
use dhall_core::core::Const::*;
use dhall_core::core::Expr_::*;
use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, shift, subst, Expr, V, X};
+use dhall_core::core::{bx, shift, subst, Expr, Expr_, V, X};
use self::TypeMessage::*;
@@ -155,7 +155,7 @@ fn op2_type<'i, S, EF>(
) -> Result<Expr<'i, S, X>, TypeError<'i, S>>
where
S: Clone + ::std::fmt::Debug + 'i,
- EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<'i, S>,
+ EF: FnOnce(Expr<'i, S, X>, Expr<'i, S, X>) -> TypeMessage<&'i str, S>,
{
let tl = normalize(&type_with(ctx, l)?);
match tl {
@@ -189,7 +189,7 @@ where
use dhall_core::Expr_;
match *e {
Const(c) => axiom(c).map(Const), //.map(Cow::Owned),
- Var(V(x, n)) => {
+ Var(V(ref x, n)) => {
ctx.lookup(x, n)
.cloned()
//.map(Cow::Borrowed)
@@ -206,7 +206,7 @@ where
Ok(p)
}
Pi(x, ref tA, ref tB) => {
- let tA2 = normalize::<S, S, X>(&type_with(ctx, tA)?);
+ let tA2 = normalize::<_, S, S, X>(&type_with(ctx, tA)?);
let kA = match tA2 {
Const(k) => k,
_ => {
@@ -253,9 +253,9 @@ where
let tA2 = type_with(ctx, a)?;
if prop_equal(&tA, &tA2) {
let vx0 = V(x, 0);
- let a2 = shift::<S, S, X>(1, vx0, a);
+ let a2 = shift::<&str, S, S, X>(1, vx0, a);
let tB2 = subst(vx0, &a2, &tB);
- let tB3 = shift::<S, S, X>(-1, vx0, &tB2);
+ let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2);
Ok(tB3)
} else {
let nf_A = normalize(&tA);
@@ -269,7 +269,7 @@ where
}
Let(f, ref mt, ref r, ref b) => {
let tR = type_with(ctx, r)?;
- let ttR = normalize::<S, S, X>(&type_with(ctx, &tR)?);
+ let ttR = normalize::<_, S, S, X>(&type_with(ctx, &tR)?);
let kR = match ttR {
Const(k) => k,
// Don't bother to provide a `let`-specific version of this error
@@ -279,7 +279,7 @@ where
let ctx2 = ctx.insert(f, tR.clone());
let tB = type_with(&ctx2, b)?;
- let ttB = normalize::<S, S, X>(&type_with(ctx, &tB)?);
+ let ttB = normalize::<_, S, S, X>(&type_with(ctx, &tB)?);
let kB = match ttB {
Const(k) => k,
// Don't bother to provide a `let`-specific version of this error
@@ -426,7 +426,7 @@ where
}
};
- let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
+ let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
match s {
Const(Type) => {}
_ => return Err(TypeError::new(ctx, e, InvalidListType(*t))),
@@ -512,7 +512,7 @@ where
}
};
- let s = normalize::<_, S, _>(&type_with(ctx, &t)?);
+ let s = normalize::<_, _, S, _>(&type_with(ctx, &t)?);
match s {
Const(Type) => {}
_ => {
@@ -561,7 +561,7 @@ where
| Builtin(Double) | Builtin(Text) => Ok(Const(Type)),
Record(ref kts) => {
for (k, t) in kts {
- let s = normalize::<S, S, X>(&type_with(ctx, t)?);
+ let s = normalize::<_, S, S, X>(&type_with(ctx, t)?);
match s {
Const(Type) => {}
_ => {
@@ -580,7 +580,7 @@ where
.iter()
.map(|(&k, v)| {
let t = type_with(ctx, v)?;
- let s = normalize::<S, S, X>(&type_with(ctx, &t)?);
+ let s = normalize::<_, S, S, X>(&type_with(ctx, &t)?);
match s {
Const(Type) => {}
_ => {
@@ -717,57 +717,71 @@ pub fn type_of<'i, S: Clone + ::std::fmt::Debug + 'i>(
/// The specific type error
#[derive(Debug)]
-pub enum TypeMessage<'i, S> {
+pub enum TypeMessage<Label, S> {
UnboundVariable,
- InvalidInputType(Expr<'i, S, X>),
- InvalidOutputType(Expr<'i, S, X>),
- NotAFunction(Expr<'i, S, X>, Expr<'i, S, X>),
+ InvalidInputType(Expr_<Label, S, X>),
+ InvalidOutputType(Expr_<Label, S, X>),
+ NotAFunction(Expr_<Label, S, X>, Expr_<Label, S, X>),
TypeMismatch(
- Expr<'i, S, X>,
- Expr<'i, S, X>,
- Expr<'i, S, X>,
- Expr<'i, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
),
- AnnotMismatch(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+ AnnotMismatch(Expr_<Label, S, X>, Expr_<Label, S, X>, Expr_<Label, S, X>),
Untyped,
- InvalidListElement(usize, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- InvalidListType(Expr<'i, S, X>),
- InvalidOptionalElement(Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
+ InvalidListElement(
+ usize,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ ),
+ InvalidListType(Expr_<Label, S, X>),
+ InvalidOptionalElement(
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ ),
InvalidOptionalLiteral(usize),
- InvalidOptionalType(Expr<'i, S, X>),
- InvalidPredicate(Expr<'i, S, X>, Expr<'i, S, X>),
+ InvalidOptionalType(Expr_<Label, S, X>),
+ InvalidPredicate(Expr_<Label, S, X>, Expr_<Label, S, X>),
IfBranchMismatch(
- Expr<'i, S, X>,
- Expr<'i, S, X>,
- Expr<'i, S, X>,
- Expr<'i, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ ),
+ IfBranchMustBeTerm(
+ bool,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
+ Expr_<Label, S, X>,
),
- IfBranchMustBeTerm(bool, Expr<'i, S, X>, Expr<'i, S, X>, Expr<'i, S, X>),
- InvalidField(String, Expr<'i, S, X>),
- InvalidFieldType(String, Expr<'i, S, X>),
- InvalidAlternative(String, Expr<'i, S, X>),
- InvalidAlternativeType(String, Expr<'i, S, X>),
+ InvalidField(String, Expr_<Label, S, X>),
+ InvalidFieldType(String, Expr_<Label, S, X>),
+ InvalidAlternative(String, Expr_<Label, S, X>),
+ InvalidAlternativeType(String, Expr_<Label, S, X>),
DuplicateAlternative(String),
- MustCombineARecord(Expr<'i, S, X>, Expr<'i, S, X>),
+ MustCombineARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
FieldCollision(String),
- MustMergeARecord(Expr<'i, S, X>, Expr<'i, S, X>),
- MustMergeUnion(Expr<'i, S, X>, Expr<'i, S, X>),
+ MustMergeARecord(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ MustMergeUnion(Expr_<Label, S, X>, Expr_<Label, S, X>),
UnusedHandler(HashSet<String>),
MissingHandler(HashSet<String>),
- HandlerInputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
- HandlerOutputTypeMismatch(String, Expr<'i, S, X>, Expr<'i, S, X>),
- HandlerNotAFunction(String, Expr<'i, S, X>),
- NotARecord(String, Expr<'i, S, X>, Expr<'i, S, X>),
- MissingField(String, Expr<'i, S, X>),
- CantAnd(Expr<'i, S, X>, Expr<'i, S, X>),
- CantOr(Expr<'i, S, X>, Expr<'i, S, X>),
- CantEQ(Expr<'i, S, X>, Expr<'i, S, X>),
- CantNE(Expr<'i, S, X>, Expr<'i, S, X>),
- CantTextAppend(Expr<'i, S, X>, Expr<'i, S, X>),
- CantAdd(Expr<'i, S, X>, Expr<'i, S, X>),
- CantMultiply(Expr<'i, S, X>, Expr<'i, S, X>),
- NoDependentLet(Expr<'i, S, X>, Expr<'i, S, X>),
- NoDependentTypes(Expr<'i, S, X>, Expr<'i, S, X>),
+ HandlerInputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+ HandlerOutputTypeMismatch(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+ HandlerNotAFunction(String, Expr_<Label, S, X>),
+ NotARecord(String, Expr_<Label, S, X>, Expr_<Label, S, X>),
+ MissingField(String, Expr_<Label, S, X>),
+ CantAnd(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ CantOr(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ CantEQ(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ CantNE(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ CantTextAppend(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ CantAdd(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ CantMultiply(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ NoDependentLet(Expr_<Label, S, X>, Expr_<Label, S, X>),
+ NoDependentTypes(Expr_<Label, S, X>, Expr_<Label, S, X>),
}
/// A structured type error that includes context
@@ -775,14 +789,14 @@ pub enum TypeMessage<'i, S> {
pub struct TypeError<'i, S> {
pub context: Context<&'i str, Expr<'i, S, X>>,
pub current: Expr<'i, S, X>,
- pub type_message: TypeMessage<'i, S>,
+ pub type_message: TypeMessage<&'i str, S>,
}
impl<'i, S: Clone> TypeError<'i, S> {
pub fn new(
context: &Context<&'i str, Expr<'i, S, X>>,
current: &Expr<'i, S, X>,
- type_message: TypeMessage<'i, S>,
+ type_message: TypeMessage<&'i str, S>,
) -> Self {
TypeError {
context: context.clone(),
@@ -792,7 +806,7 @@ impl<'i, S: Clone> TypeError<'i, S> {
}
}
-impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
+impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<&'i str, S> {
fn description(&self) -> &str {
match *self {
UnboundVariable => "Unbound variable",
@@ -805,7 +819,7 @@ impl<'i, S: fmt::Debug> ::std::error::Error for TypeMessage<'i, S> {
}
}
-impl<'i, S> fmt::Display for TypeMessage<'i, S> {
+impl<'i, S> fmt::Display for TypeMessage<&'i str, S> {
fn fmt(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
match *self {
UnboundVariable => {
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 22:31:30 +0000