summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/typecheck.rs257
1 files changed, 125 insertions, 132 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 9eead93..a0782f8 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -272,22 +272,33 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, X> {
}
}
-fn ensure_equal<S, F1, F2>(
- x: &Type,
- y: &Type,
- mkerr: F1,
- mkmsg: F2,
-) -> Result<(), TypeError<S>>
-where
- S: std::fmt::Debug,
- F1: FnOnce(TypeMessage<S>) -> TypeError<S>,
- F2: FnOnce() -> TypeMessage<S>,
-{
- if prop_equal(x, y) {
- Ok(())
- } else {
- Err(mkerr(mkmsg()))
- }
+macro_rules! ensure_equal {
+ ($x:expr, $y:expr, $err:expr $(,)*) => {
+ if !prop_equal(&$x, &$y) {
+ return Err($err);
+ }
+ };
+}
+
+macro_rules! ensure_matches {
+ ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => {
+ match $x.unroll_ref()? {
+ $pat => $branch,
+ _ => return Err($err),
+ }
+ };
+}
+
+macro_rules! ensure_is_type {
+ ($x:expr, $err:expr $(,)*) => {
+ ensure_matches!($x, Const(Type) => {}, $err)
+ };
+}
+
+macro_rules! ensure_is_const {
+ ($x:expr, $err:expr $(,)*) => {
+ ensure_matches!($x, Const(k) => *k, $err)
+ };
}
/// Type-check an expression and return the expression alongside its type
@@ -301,16 +312,6 @@ 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.unroll_ref()? {
- Const(k) => Ok(*k),
- _ => Err(mkerr(msg)),
- };
- let ensure_is_type =
- |x: &crate::expr::Type, msg: TypeMessage<_>| match x.unroll_ref()? {
- Const(Type) => Ok(()),
- _ => Err(mkerr(msg)),
- };
let mktype =
|ctx, x: SubExpr<X, X>| Ok(type_with(ctx, x)?.normalize().into_type());
@@ -338,27 +339,23 @@ pub fn type_with(
}
Pi(x, tA, tB) => {
let tA = mktype(ctx, tA.clone())?;
- let kA = ensure_const(
+ let kA = ensure_is_const!(
&tA.get_type(),
- InvalidInputType(tA.clone().into_normalized()?),
- )?;
+ mkerr(InvalidInputType(tA.into_normalized()?)),
+ );
let ctx2 = ctx
.insert(x.clone(), tA.clone())
.map(|e| e.shift(1, &V(x.clone(), 0)));
let tB = type_with(&ctx2, tB.clone())?;
- let kB = match tB.get_type().unroll_ref()? {
- Const(k) => *k,
- _ => {
- return Err(TypeError::new(
- &ctx2,
- e.clone(),
- InvalidOutputType(
- tB.get_type_move().into_normalized()?,
- ),
- ));
- }
- };
+ let kB = ensure_is_const!(
+ &tB.get_type(),
+ TypeError::new(
+ &ctx2,
+ e.clone(),
+ InvalidOutputType(tB.get_type_move().into_normalized()?),
+ ),
+ );
match rule(kA, kB) {
Err(()) => Err(mkerr(NoDependentTypes(
@@ -380,19 +377,19 @@ pub fn type_with(
let r = type_with(ctx, r)?;
// Don't bother to provide a `let`-specific version of this error
// message because this should never happen anyway
- let kR = ensure_const(
+ let kR = ensure_is_const!(
&r.get_type().get_type(),
- InvalidInputType(r.get_type().clone().into_normalized()?),
- )?;
+ mkerr(InvalidInputType(r.get_type_move().into_normalized()?)),
+ );
let ctx2 = ctx.insert(f.clone(), r.get_type().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
- let kB = ensure_const(
+ let kB = ensure_is_const!(
&b.get_type().get_type(),
- InvalidOutputType(b.get_type().clone().into_normalized()?),
- )?;
+ mkerr(InvalidOutputType(b.get_type_move().into_normalized()?)),
+ );
if let Err(()) = rule(kR, kB) {
return Err(mkerr(NoDependentLet(
@@ -423,26 +420,23 @@ pub fn type_with(
let mut tf = f.get_type().clone();
while let Some(a) = iter.next() {
seen_args.push(a.as_expr().clone());
- let (x, tx, tb) = match tf.unroll_ref()? {
+ let (x, tx, tb) = ensure_matches!(tf,
Pi(x, tx, tb) => (x, tx, tb),
- _ => {
- return Err(mkerr(NotAFunction(Typed(
- rc(App(f.into_expr(), seen_args)),
- tf,
- ))));
- }
- };
+ mkerr(NotAFunction(Typed(
+ rc(App(f.into_expr(), seen_args)),
+ tf,
+ )))
+ );
let tx = mktype(ctx, tx.clone())?;
- ensure_equal(&tx, &a.get_type(), mkerr, || {
- TypeMismatch(
- Typed(
- rc(App(f.as_expr().clone(), seen_args.clone())),
- tf.clone(),
- ),
- tx.clone().into_normalized().unwrap(),
- a.clone(),
- )
- })?;
+ ensure_equal!(
+ tx,
+ a.get_type(),
+ mkerr(TypeMismatch(
+ Typed(rc(App(f.into_expr(), seen_args)), tf),
+ tx.into_normalized()?,
+ a,
+ ))
+ );
tf = mktype(
ctx,
subst_shift(&V(x.clone(), 0), &a.as_expr(), &tb),
@@ -452,90 +446,93 @@ pub fn type_with(
}
Annot(x, t) => {
let t = t.normalize().into_type();
- ensure_equal(&t, &x.get_type(), mkerr, || {
- AnnotMismatch(
- x.clone(),
- t.clone().into_normalized().unwrap(),
- )
- })?;
+ ensure_equal!(
+ t,
+ x.get_type(),
+ mkerr(AnnotMismatch(x, t.into_normalized()?))
+ );
Ok(RetType(x.get_type_move()))
}
BoolIf(x, y, z) => {
- ensure_equal(
- &x.get_type(),
- &mktype(ctx, rc(Builtin(Bool)))?,
- mkerr,
- || InvalidPredicate(x.clone()),
- )?;
- ensure_is_type(
- &y.get_type().get_type(),
- IfBranchMustBeTerm(true, y.clone()),
- )?;
+ ensure_equal!(
+ x.get_type(),
+ mktype(ctx, rc(Builtin(Bool)))?,
+ mkerr(InvalidPredicate(x)),
+ );
+ ensure_is_type!(
+ y.get_type().get_type(),
+ mkerr(IfBranchMustBeTerm(true, y)),
+ );
- ensure_is_type(
- &z.get_type().get_type(),
- IfBranchMustBeTerm(false, z.clone()),
- )?;
+ ensure_is_type!(
+ z.get_type().get_type(),
+ mkerr(IfBranchMustBeTerm(false, z)),
+ );
- ensure_equal(&y.get_type(), &z.get_type(), mkerr, || {
- IfBranchMismatch(y.clone(), z.clone())
- })?;
+ ensure_equal!(
+ y.get_type(),
+ z.get_type(),
+ mkerr(IfBranchMismatch(y, z))
+ );
Ok(RetType(y.get_type_move()))
}
EmptyListLit(t) => {
let t = t.normalize().into_type();
- ensure_is_type(
- &t.get_type(),
- InvalidListType(t.clone().into_normalized()?),
- )?;
+ ensure_is_type!(
+ t.get_type(),
+ mkerr(InvalidListType(t.into_normalized()?)),
+ );
let t = t.into_normalized()?.into_expr();
Ok(RetExpr(dhall::expr!(List t)))
}
NEListLit(xs) => {
let mut iter = xs.into_iter().enumerate();
let (_, x) = iter.next().unwrap();
- ensure_is_type(
- &x.get_type().get_type(),
- InvalidListType(x.get_type().clone().into_normalized()?),
- )?;
+ ensure_is_type!(
+ x.get_type().get_type(),
+ mkerr(InvalidListType(
+ x.get_type_move().into_normalized()?
+ )),
+ );
for (i, y) in iter {
- ensure_equal(&x.get_type(), &y.get_type(), mkerr, || {
- InvalidListElement(
+ ensure_equal!(
+ x.get_type(),
+ y.get_type(),
+ mkerr(InvalidListElement(
i,
- x.get_type().clone().into_normalized().unwrap(),
- y.clone(),
- )
- })?;
+ x.get_type_move().into_normalized()?,
+ y
+ ))
+ );
}
let t = x.get_type_move().into_normalized()?.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().into_normalized()?),
- )?;
+ ensure_is_type!(
+ t.get_type(),
+ mkerr(InvalidOptionalType(t.into_normalized()?)),
+ );
let t = t.into_normalized()?.into_expr();
Ok(RetExpr(dhall::expr!(Optional t)))
}
NEOptionalLit(x) => {
- ensure_is_type(
- &x.get_type().get_type(),
- InvalidOptionalType(
- x.get_type().clone().into_normalized()?,
- ),
- )?;
- let t = x.get_type_move().into_normalized()?.into_expr();
+ let tx = x.get_type_move();
+ ensure_is_type!(
+ tx.get_type(),
+ mkerr(InvalidOptionalType(tx.into_normalized()?,)),
+ );
+ let t = tx.into_normalized()?.into_expr();
Ok(RetExpr(dhall::expr!(Optional t)))
}
RecordType(kts) => {
for (k, t) in kts {
- ensure_is_type(
- &t.get_type(),
- InvalidFieldType(k.clone(), t.clone()),
- )?;
+ ensure_is_type!(
+ t.get_type(),
+ mkerr(InvalidFieldType(k, t)),
+ );
}
Ok(RetExpr(dhall::expr!(Type)))
}
@@ -543,25 +540,25 @@ pub fn type_with(
let kts = kvs
.into_iter()
.map(|(k, v)| {
- ensure_is_type(
- &v.get_type().get_type(),
- InvalidField(k.clone(), v.clone()),
- )?;
+ ensure_is_type!(
+ v.get_type().get_type(),
+ mkerr(InvalidField(k, v)),
+ );
Ok((
- k.clone(),
+ k,
v.get_type_move().into_normalized()?.into_expr(),
))
})
.collect::<Result<_, _>>()?;
Ok(RetExpr(RecordType(kts)))
}
- Field(r, x) => match r.get_type().unroll_ref()? {
+ Field(r, x) => ensure_matches!(r.get_type(),
RecordType(kts) => match kts.get(&x) {
Some(e) => Ok(RetExpr(e.unroll())),
- None => Err(mkerr(MissingField(x.clone(), r.clone()))),
+ None => Err(mkerr(MissingField(x, r))),
},
- _ => Err(mkerr(NotARecord(x.clone(), r.clone()))),
- },
+ mkerr(NotARecord(x, r))
+ ),
Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
BoolLit(_) => Ok(RetExpr(dhall::expr!(Bool))),
NaturalLit(_) => Ok(RetExpr(dhall::expr!(Natural))),
@@ -584,13 +581,9 @@ pub fn type_with(
},
)?;
- ensure_equal(&l.get_type(), &t, mkerr, || {
- BinOpTypeMismatch(o, l.clone())
- })?;
+ ensure_equal!(l.get_type(), t, mkerr(BinOpTypeMismatch(o, l)));
- ensure_equal(&r.get_type(), &t, mkerr, || {
- BinOpTypeMismatch(o, r.clone())
- })?;
+ ensure_equal!(r.get_type(), t, mkerr(BinOpTypeMismatch(o, r)));
Ok(RetType(t))
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 22:06:31 +0000