summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-07 01:18:31 +0200
committerNadrieril2019-04-07 01:18:31 +0200
commitb96f187dfc6373b6e2faee01e085d7e3dff893ca (patch)
tree191730bc5c4dd7cf7800561785246df21bdc0895
parentda9937f623f2698adec50718e1e703958e837c85 (diff)
Handle universe error properly
-rw-r--r--dhall/src/typecheck.rs84
1 files changed, 49 insertions, 35 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index a703821..becabbd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -51,18 +51,26 @@ impl<'a> Type<'a> {
Cow::Borrowed(x) => crate::expr::Type(Cow::Borrowed(x)),
}
}
- fn as_expr(&'a self) -> &'a SubExpr<X, X> {
+ fn as_expr(&'a self) -> Result<&'a SubExpr<X, X>, TypeError<X>> {
use TypeInternal::*;
match self.0.as_ref() {
- Expr(e) => e.as_expr(),
- Universe(_) => unimplemented!(),
+ Expr(e) => Ok(e.as_expr()),
+ Universe(_) => Err(TypeError::new(
+ &Context::new(),
+ rc(ExprF::Const(Const::Sort)),
+ TypeMessage::Untyped,
+ )),
}
}
- fn into_expr(self) -> SubExpr<X, X> {
+ fn into_expr(self) -> Result<SubExpr<X, X>, TypeError<X>> {
use TypeInternal::*;
match self.0.into_owned() {
- Expr(e) => e.into_expr(),
- Universe(_) => unimplemented!(),
+ Expr(e) => Ok(e.into_expr()),
+ Universe(_) => Err(TypeError::new(
+ &Context::new(),
+ rc(ExprF::Const(Const::Sort)),
+ TypeMessage::Untyped,
+ )),
}
}
pub fn get_type<'b>(&'b self) -> Type<'b> {
@@ -270,18 +278,20 @@ pub fn type_with(
use dhall_core::Const::*;
use dhall_core::ExprF::*;
let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
- let ensure_const =
- |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref()
- {
- Const(k) => Ok(*k),
- _ => Err(mkerr(msg)),
- };
- let ensure_is_type =
- |x: &crate::expr::Type, msg: TypeMessage<_>| match x.as_expr().as_ref()
- {
- Const(Type) => Ok(()),
- _ => Err(mkerr(msg)),
- };
+ let ensure_const = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
+ .as_expr()?
+ .as_ref()
+ {
+ Const(k) => Ok(*k),
+ _ => Err(mkerr(msg)),
+ };
+ let ensure_is_type = |x: &crate::expr::Type, msg: TypeMessage<_>| match x
+ .as_expr()?
+ .as_ref()
+ {
+ Const(Type) => Ok(()),
+ _ => Err(mkerr(msg)),
+ };
let mktype =
|ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
@@ -295,17 +305,17 @@ pub fn type_with(
Lam(x, t, b) => {
let t2 = mktype(ctx, t.clone())?;
let ctx2 = ctx
- .insert(x.clone(), t2.as_expr().clone())
+ .insert(x.clone(), t2.as_expr()?.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
let b = type_with(&ctx2, b.clone())?;
let _ = type_with(
ctx,
- rc(Pi(x.clone(), t.clone(), b.get_type().as_expr().clone())),
+ rc(Pi(x.clone(), t.clone(), b.get_type().as_expr()?.clone())),
)?;
Ok(RetExpr(Pi(
x.clone(),
- t2.as_expr().clone(),
- b.get_type().into_expr(),
+ t2.as_expr()?.clone(),
+ b.get_type().into_expr()?,
)))
}
Pi(x, tA, tB) => {
@@ -314,10 +324,10 @@ pub fn type_with(
ensure_const(&tA.get_type(), InvalidInputType(tA.clone()))?;
let ctx2 = ctx
- .insert(x.clone(), tA.as_expr().clone())
+ .insert(x.clone(), tA.as_expr()?.clone())
.map(|e| shift(1, &V(x.clone(), 0), e));
let tB = type_with(&ctx2, tB.clone())?;
- let kB = match tB.get_type().as_expr().as_ref() {
+ let kB = match tB.get_type().as_expr()?.as_ref() {
Const(k) => *k,
_ => {
return Err(TypeError::new(
@@ -351,7 +361,7 @@ pub fn type_with(
InvalidInputType(r.get_type().into_owned()),
)?;
- let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr().clone());
+ let ctx2 = ctx.insert(f.clone(), r.get_type().as_expr()?.clone());
let b = type_with(&ctx2, b.clone())?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
@@ -389,7 +399,7 @@ pub fn type_with(
let mut tf = f.get_type().into_owned();
while let Some(a) = iter.next() {
seen_args.push(a.as_expr().clone());
- let (x, tx, tb) = match tf.as_expr().as_ref() {
+ let (x, tx, tb) = match tf.as_expr()?.as_ref() {
Pi(x, tx, tb) => (x, tx, tb),
_ => {
return Err(mkerr(NotAFunction(Typed(
@@ -449,7 +459,7 @@ pub fn type_with(
EmptyListLit(t) => {
let t = t.normalize().into_type();
ensure_is_type(&t.get_type(), InvalidListType(t.clone()))?;
- let t = t.into_expr();
+ let t = t.into_expr()?;
Ok(RetExpr(dhall::expr!(List t)))
}
NEListLit(xs) => {
@@ -468,13 +478,13 @@ pub fn type_with(
)
})?;
}
- let t = x.get_type().into_expr();
+ let t = x.get_type().into_expr()?;
Ok(RetExpr(dhall::expr!(List t)))
}
EmptyOptionalLit(t) => {
let t = t.normalize().into_type();
ensure_is_type(&t.get_type(), InvalidOptionalType(t.clone()))?;
- let t = t.into_expr();
+ let t = t.into_expr()?;
Ok(RetExpr(dhall::expr!(Optional t)))
}
NEOptionalLit(x) => {
@@ -482,7 +492,7 @@ pub fn type_with(
&x.get_type().get_type(),
InvalidOptionalType(x.get_type().into_owned()),
)?;
- let t = x.get_type().into_expr();
+ let t = x.get_type().into_expr()?;
Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
@@ -502,12 +512,12 @@ pub fn type_with(
&v.get_type().get_type(),
InvalidField(k.clone(), v.clone()),
)?;
- Ok((k.clone(), v.get_type().into_expr()))
+ Ok((k.clone(), v.get_type().into_expr()?))
})
.collect::<Result<_, _>>()?;
Ok(RetExpr(RecordType(kts)))
}
- Field(r, x) => match r.get_type().as_expr().as_ref() {
+ Field(r, x) => match r.get_type().as_expr()?.as_ref() {
RecordType(kts) => match kts.get(&x) {
Some(e) => Ok(RetExpr(e.unroll())),
None => Err(mkerr(MissingField(x.clone(), r.clone()))),
@@ -561,7 +571,8 @@ pub fn type_with(
/// will fail.
pub fn type_of(e: SubExpr<X, X>) -> Result<SubExpr<X, X>, TypeError<X>> {
let ctx = Context::new();
- type_with(&ctx, e).map(|e| e.get_type().into_expr())
+ let e = type_with(&ctx, e)?;
+ e.get_type().into_expr()
}
pub fn type_of_(e: SubExpr<X, X>) -> Result<Typed, TypeError<X>> {
@@ -642,9 +653,12 @@ impl<S> fmt::Display for TypeMessage<S> {
let template = include_str!("errors/TypeMismatch.txt");
let s = template
.replace("$txt0", &format!("{}", e0.as_expr()))
- .replace("$txt1", &format!("{}", e1.as_expr()))
+ .replace("$txt1", &format!("{}", e1.as_expr().unwrap()))
.replace("$txt2", &format!("{}", e2.as_expr()))
- .replace("$txt3", &format!("{}", e2.get_type().as_expr()));
+ .replace(
+ "$txt3",
+ &format!("{}", e2.get_type().as_expr().unwrap()),
+ );
f.write_str(&s)
}
_ => f.write_str("Unhandled error message"),