summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-14 00:06:27 +0200
committerNadrieril2019-04-14 00:08:50 +0200
commitd53893de0b45bbe56b3e5825ba6e979485cc1d75 (patch)
tree682eed908115892407961a57d95c37a89c2d0012
parentd69cf504a1c8eb8043c8115c7dcb5cefba67fb06 (diff)
Implement `let` type synonyms
Diffstat (limited to '')
-rw-r--r--dhall/src/typecheck.rs76
1 files changed, 25 insertions, 51 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8ca48eb..8bc1cdd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -271,15 +271,6 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, Normalized<'static>> {
}
}
-macro_rules! function_check {
- ($x:expr, $y:expr, $err:expr $(,)*) => {
- match function_check($x, $y) {
- Ok(k) => k,
- Err(()) => return Err($err),
- }
- };
-}
-
macro_rules! ensure_equal {
($x:expr, $y:expr, $err:expr $(,)*) => {
if !prop_equal($x, $y) {
@@ -379,49 +370,33 @@ fn type_with(
),
);
- let k = function_check!(kA, kB, {
- mkerr(NoDependentTypes(
- tA.clone().into_normalized()?,
- tB.get_type_move()?.into_normalized()?,
- ))
- });
+ let k = match function_check(kA, kB) {
+ Ok(k) => k,
+ Err(()) => {
+ return Err(mkerr(NoDependentTypes(
+ tA.clone().into_normalized()?,
+ tB.get_type_move()?.into_normalized()?,
+ )))
+ }
+ };
Ok(RetExpr(Const(k)))
}
- Let(f, mt, r, b) => {
- let r = if let Some(t) = mt {
- let r = SubExpr::clone(r);
- let t = SubExpr::clone(t);
- dhall::subexpr!(r: t)
+ Let(x, t, v, e) => {
+ let v = if let Some(t) = t {
+ rc(Annot(v.clone(), t.clone()))
} else {
- SubExpr::clone(r)
+ v.clone()
};
- 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_is_const!(
- &r.get_type()?.get_type()?,
- mkerr(InvalidInputType(r.get_type_move()?.into_normalized()?)),
- );
-
- let ctx2 = ctx.insert(f.clone(), r.get_type()?.into_owned());
- 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_is_const!(
- &b.get_type()?.get_type()?,
- mkerr(InvalidOutputType(b.get_type_move()?.into_normalized()?)),
- );
-
- function_check!(kR, kB, {
- mkerr(NoDependentLet(
- r.get_type_move()?.into_normalized()?,
- b.get_type_move()?.into_normalized()?,
- ))
- });
+ let v = type_with(ctx, v)?.normalize();
+ let e = type_with(
+ ctx,
+ // TODO: Use a substitution context
+ subst_shift(&V(x.clone(), 0), &v.as_expr().absurd(), e),
+ )?;
- Ok(RetType(b.get_type_move()?))
+ Ok(RetType(e.get_type_move()?))
}
Embed(p) => return Ok(p.clone().into()),
_ => type_last_layer(
@@ -501,7 +476,7 @@ fn type_last_layer(
});
tf = mktype(
ctx,
- subst_shift(&V(x.clone(), 0), a.as_expr(), &tb.absurd()),
+ rc(Let(x.clone(), None, a.as_expr().clone(), tb.absurd())),
)?;
}
Ok(RetType(tf))
@@ -622,12 +597,12 @@ fn type_last_layer(
DoubleLit(_) => Ok(RetType(simple_type_from_builtin(Double))),
// TODO: check type of interpolations
TextLit(_) => Ok(RetType(simple_type_from_builtin(Text))),
- BinOp(o@ListAppend, l, r) => {
+ BinOp(o @ ListAppend, l, r) => {
match l.get_type()?.as_normalized()?.as_expr().as_ref() {
App(f, args) if args.len() == 1 => match f.as_ref() {
Builtin(List) => {}
_ => return Err(mkerr(BinOpTypeMismatch(o, l))),
- }
+ },
_ => return Err(mkerr(BinOpTypeMismatch(o, l))),
}
@@ -696,7 +671,6 @@ pub(crate) enum TypeMessage<'a> {
NotARecord(Label, Typed<'a>),
MissingField(Label, Typed<'a>),
BinOpTypeMismatch(BinOp, Typed<'a>),
- NoDependentLet(Normalized<'a>, Normalized<'a>),
NoDependentTypes(Normalized<'a>, Normalized<'a>),
Unimplemented,
}
@@ -971,8 +945,8 @@ mod spec_tests {
// ti_success!(ti_success_unit_IntegerToDouble, "unit/IntegerToDouble");
// ti_success!(ti_success_unit_Kind, "unit/Kind");
ti_success!(ti_success_unit_Let, "unit/Let");
- // ti_success!(ti_success_unit_LetNestedTypeSynonym, "unit/LetNestedTypeSynonym");
- // ti_success!(ti_success_unit_LetTypeSynonym, "unit/LetTypeSynonym");
+ ti_success!(ti_success_unit_LetNestedTypeSynonym, "unit/LetNestedTypeSynonym");
+ ti_success!(ti_success_unit_LetTypeSynonym, "unit/LetTypeSynonym");
ti_success!(ti_success_unit_LetWithAnnotation, "unit/LetWithAnnotation");
ti_success!(ti_success_unit_List, "unit/List");
ti_success!(ti_success_unit_ListBuild, "unit/ListBuild");