diff options
| -rw-r--r-- | dhall/src/expr.rs | 5 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 71 |
2 files changed, 39 insertions, 37 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 6458be9..30ca6c6 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -88,3 +88,8 @@ impl Normalized { } } +impl SimpleType { + pub(crate) fn into_type(self) -> Type { + Normalized(self.0, Some(Type::const_type())).into_type() + } +} diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 3350964..cab734e 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -278,9 +278,10 @@ macro_rules! ensure_matches { }; } -macro_rules! ensure_is_type { +// Ensure the provided type has type `Type` +macro_rules! ensure_simple_type { ($x:expr, $err:expr $(,)*) => { - ensure_matches!($x, Const(Type) => {}, $err) + ensure_matches!($x.get_type()?, Const(Type) => {}, $err) }; } @@ -297,7 +298,6 @@ pub fn type_with( e: SubExpr<X, X>, ) -> Result<Typed, TypeError<X>> { use dhall_core::BinOp::*; - use dhall_core::Builtin::*; use dhall_core::Const::*; use dhall_core::ExprF::*; let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg); @@ -305,6 +305,8 @@ pub fn type_with( let mktype = |ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type()); + let mksimpletype = |x: SubExpr<X, X>| SimpleType(x).into_type(); + enum Ret { RetType(crate::expr::Type), RetExpr(Expr<X, X>), @@ -396,8 +398,8 @@ pub fn type_with( Lam(_, _, _) => unreachable!(), Pi(_, _, _) => unreachable!(), Let(_, _, _, _) => unreachable!(), - Const(Type) => Ok(RetExpr(dhall::expr!(Kind))), - Const(Kind) => Ok(RetExpr(dhall::expr!(Sort))), + Const(Type) => Ok(RetType(crate::expr::Type::const_kind())), + Const(Kind) => Ok(RetType(crate::expr::Type::const_sort())), Const(Sort) => { Ok(RetType(crate::expr::Type(TypeInternal::SuperType))) } @@ -446,16 +448,17 @@ pub fn type_with( BoolIf(x, y, z) => { ensure_equal!( x.get_type()?, - &mktype(ctx, rc(Builtin(Bool)))?, + &mksimpletype(dhall::subexpr!(Bool)), mkerr(InvalidPredicate(x)), ); - ensure_is_type!( - y.get_type()?.get_type()?, + + ensure_simple_type!( + y.get_type()?, mkerr(IfBranchMustBeTerm(true, y)), ); - ensure_is_type!( - z.get_type()?.get_type()?, + ensure_simple_type!( + z.get_type()?, mkerr(IfBranchMustBeTerm(false, z)), ); @@ -469,8 +472,8 @@ pub fn type_with( } EmptyListLit(t) => { let t = t.normalize().into_type(); - ensure_is_type!( - t.get_type()?, + ensure_simple_type!( + t, mkerr(InvalidListType(t.into_normalized()?)), ); let t = t.into_normalized()?.into_expr(); @@ -479,8 +482,8 @@ pub fn type_with( NEListLit(xs) => { let mut iter = xs.into_iter().enumerate(); let (_, x) = iter.next().unwrap(); - ensure_is_type!( - x.get_type()?.get_type()?, + ensure_simple_type!( + x.get_type()?, mkerr(InvalidListType( x.get_type_move()?.into_normalized()? )), @@ -501,8 +504,8 @@ pub fn type_with( } EmptyOptionalLit(t) => { let t = t.normalize().into_type(); - ensure_is_type!( - t.get_type()?, + ensure_simple_type!( + t, mkerr(InvalidOptionalType(t.into_normalized()?)), ); let t = t.into_normalized()?.into_expr(); @@ -510,8 +513,8 @@ pub fn type_with( } NEOptionalLit(x) => { let tx = x.get_type_move()?; - ensure_is_type!( - tx.get_type()?, + ensure_simple_type!( + tx, mkerr(InvalidOptionalType(tx.into_normalized()?,)), ); let t = tx.into_normalized()?.into_expr(); @@ -519,10 +522,7 @@ pub fn type_with( } RecordType(kts) => { for (k, t) in kts { - ensure_is_type!( - t.get_type()?, - mkerr(InvalidFieldType(k, t)), - ); + ensure_simple_type!(t, mkerr(InvalidFieldType(k, t)),); } Ok(RetExpr(dhall::expr!(Type))) } @@ -530,8 +530,8 @@ pub fn type_with( let kts = kvs .into_iter() .map(|(k, v)| { - ensure_is_type!( - v.get_type()?.get_type()?, + ensure_simple_type!( + v.get_type()?, mkerr(InvalidField(k, v)), ); Ok(( @@ -557,19 +557,16 @@ pub fn type_with( // TODO: check type of interpolations TextLit(_) => Ok(RetExpr(dhall::expr!(Text))), BinOp(o, l, r) => { - let t = mktype( - ctx, - match o { - BoolAnd => dhall::subexpr!(Bool), - BoolOr => dhall::subexpr!(Bool), - BoolEQ => dhall::subexpr!(Bool), - BoolNE => dhall::subexpr!(Bool), - NaturalPlus => dhall::subexpr!(Natural), - NaturalTimes => dhall::subexpr!(Natural), - TextAppend => dhall::subexpr!(Text), - _ => panic!("Unimplemented typecheck case: {:?}", e), - }, - )?; + let t = mksimpletype(match o { + BoolAnd => dhall::subexpr!(Bool), + BoolOr => dhall::subexpr!(Bool), + BoolEQ => dhall::subexpr!(Bool), + BoolNE => dhall::subexpr!(Bool), + NaturalPlus => dhall::subexpr!(Natural), + NaturalTimes => dhall::subexpr!(Natural), + TextAppend => dhall::subexpr!(Text), + _ => panic!("Unimplemented typecheck case: {:?}", e), + }); ensure_equal!( l.get_type()?, |