diff options
| -rw-r--r-- | dhall/src/typecheck.rs | 84 |
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"), |