summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/typecheck.rs95
1 files changed, 55 insertions, 40 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 37c95c5..6fb7cac 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -176,6 +176,18 @@ impl TypedImproved {
TypedImproved::Expr(e) => Ok(e),
}
}
+ fn normalize_to_type(self) -> Result<Type<'static>, TypeError> {
+ Ok(self.into_typed()?.normalize_to_type())
+ }
+ fn get_type(&self) -> Result<Cow<'_, Type<'static>>, TypeError> {
+ Ok(Cow::Owned(self.clone().get_type_move()?))
+ }
+ fn get_type_move(self) -> Result<Type<'static>, TypeError> {
+ Ok(self.into_typed()?.get_type_move()?)
+ }
+ fn normalize(self) -> Result<Normalized<'static>, TypeError> {
+ Ok(self.into_typed()?.normalize())
+ }
}
#[derive(Debug, Clone)]
@@ -453,7 +465,7 @@ fn mktype(
ctx: &TypecheckContext,
e: SubExpr<X, Normalized<'static>>,
) -> Result<Type<'static>, TypeError> {
- Ok(type_with(ctx, e)?.into_typed()?.normalize_to_type())
+ Ok(type_with(ctx, e)?.normalize_to_type()?)
}
fn into_simple_type<'a>(e: SubExpr<X, X>) -> Type<'a> {
@@ -549,7 +561,7 @@ fn type_with(
ctx,
// Typecheck recursively all subexpressions
e.as_ref().traverse_ref_simple(|e| {
- Ok(type_with(ctx, e.clone())?.into_typed()?)
+ Ok(type_with(ctx, e.clone())?)
})?,
e.clone(),
),
@@ -574,7 +586,7 @@ fn type_with(
/// layer.
fn type_last_layer(
ctx: &TypecheckContext,
- e: ExprF<Typed<'static>, Label, X, Normalized<'static>>,
+ e: ExprF<TypedImproved, Label, X, Normalized<'static>>,
original_e: SubExpr<X, Normalized<'static>>,
) -> Result<Ret, TypeError> {
use dhall_core::BinOp::*;
@@ -609,12 +621,12 @@ fn type_last_layer(
Ok(RetExpr(Let(
x.clone(),
None,
- a.normalize().embed(),
+ a.normalize()?.embed(),
tb.embed_absurd(),
)))
}
Annot(x, t) => {
- let t = t.normalize_to_type();
+ let t = t.normalize_to_type()?;
ensure_equal!(
&t,
x.get_type()?,
@@ -648,7 +660,7 @@ fn type_last_layer(
Ok(RetType(y.get_type_move()?))
}
EmptyListLit(t) => {
- let t = t.normalize_to_type();
+ let t = t.normalize_to_type()?;
ensure_simple_type!(
t,
mkerr(InvalidListType(t.into_normalized()?)),
@@ -679,15 +691,15 @@ fn type_last_layer(
Ok(RetExpr(dhall::expr!(List t)))
}
OldOptionalLit(None, t) => {
- let t = t.normalize().embed();
+ let t = t.normalize()?.embed();
let e = dhall::subexpr!(None t);
Ok(RetType(
type_with(ctx, e)?.into_typed()?.get_type()?.into_owned(),
))
}
OldOptionalLit(Some(x), t) => {
- let t = t.normalize().embed();
- let x = x.normalize().embed();
+ let t = t.normalize()?.embed();
+ let x = x.normalize()?.embed();
let e = dhall::subexpr!(Some x : Optional t);
Ok(RetType(
type_with(ctx, e)?.into_typed()?.get_type()?.into_owned(),
@@ -759,7 +771,10 @@ fn type_last_layer(
let mut kts: std::collections::BTreeMap<_, _> = kvs
.into_iter()
.map(|(x, v)| {
- let t = v.map(|x| x.normalize().embed());
+ let t = match v {
+ Some(x) => Some(x.normalize()?.embed()),
+ None => None,
+ };
Ok((x, t))
})
.collect::<Result<_, _>>()?;
@@ -773,7 +788,7 @@ fn type_last_layer(
None => Err(mkerr(MissingRecordField(x, r))),
},
_ => {
- let r = r.normalize_to_type();
+ let r = r.normalize_to_type()?;
match r.as_normalized()?.as_expr().as_ref() {
UnionType(kts) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
@@ -860,21 +875,21 @@ pub(crate) enum TypeMessage<'a> {
UnboundVariable(V<Label>),
InvalidInputType(Normalized<'a>),
InvalidOutputType(Normalized<'a>),
- NotAFunction(Typed<'a>),
- TypeMismatch(Typed<'a>, Normalized<'a>, Typed<'a>),
- AnnotMismatch(Typed<'a>, Normalized<'a>),
+ NotAFunction(TypedImproved),
+ TypeMismatch(TypedImproved, Normalized<'a>, TypedImproved),
+ AnnotMismatch(TypedImproved, Normalized<'a>),
Untyped,
- InvalidListElement(usize, Normalized<'a>, Typed<'a>),
+ InvalidListElement(usize, Normalized<'a>, TypedImproved),
InvalidListType(Normalized<'a>),
InvalidOptionalType(Normalized<'a>),
- InvalidPredicate(Typed<'a>),
- IfBranchMismatch(Typed<'a>, Typed<'a>),
- IfBranchMustBeTerm(bool, Typed<'a>),
- InvalidFieldType(Label, Typed<'a>),
+ InvalidPredicate(TypedImproved),
+ IfBranchMismatch(TypedImproved, TypedImproved),
+ IfBranchMustBeTerm(bool, TypedImproved),
+ InvalidFieldType(Label, TypedImproved),
NotARecord(Label, Normalized<'a>),
- MissingRecordField(Label, Typed<'a>),
+ MissingRecordField(Label, TypedImproved),
MissingUnionField(Label, Normalized<'a>),
- BinOpTypeMismatch(BinOp, Typed<'a>),
+ BinOpTypeMismatch(BinOp, TypedImproved),
NoDependentTypes(Normalized<'a>, Normalized<'a>),
Unimplemented,
}
@@ -926,25 +941,25 @@ impl fmt::Display for TypeMessage<'static> {
// 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)
- }
+ // 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"),
}
}