summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/tck
diff options
context:
space:
mode:
authorNadrieril2020-02-05 18:10:41 +0000
committerNadrieril2020-02-05 18:10:41 +0000
commitde7664d9dda95dd16742bc30e16a967c43d687ee (patch)
treeba757f557e694f63c9206394d6a162f6db21ae55 /dhall/src/semantics/tck
parent7ff5974052e3e18109acbe6e4f0588698d6129ba (diff)
Typecheck record completion
Diffstat (limited to 'dhall/src/semantics/tck')
-rw-r--r--dhall/src/semantics/tck/typecheck.rs76
1 files changed, 51 insertions, 25 deletions
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index e3ae129..6817712 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -51,9 +51,9 @@ fn mkerr<T, S: ToString>(x: S) -> Result<T, TypeError> {
/// layer.
fn type_one_layer(
env: &TyEnv,
- kind: &ExprKind<TyExpr, Normalized>,
+ ekind: ExprKind<TyExpr, Normalized>,
span: Span,
-) -> Result<Type, TypeError> {
+) -> Result<TyExpr, TypeError> {
let span_err = |msg: &str| {
mkerr(
ErrorBuilder::new(msg.to_string())
@@ -62,7 +62,7 @@ fn type_one_layer(
)
};
- Ok(match kind {
+ let ty = match &ekind {
ExprKind::Import(..) => unreachable!(
"There should remain no imports in a resolved expression"
),
@@ -74,13 +74,8 @@ fn type_one_layer(
let body_ty = body.get_type()?;
let body_ty = body_ty.to_tyexpr(env.as_varenv().insert());
let pi_ekind = ExprKind::Pi(binder.clone(), annot.clone(), body_ty);
- let pi_ty = type_one_layer(env, &pi_ekind, Span::Artificial)?;
- let ty = TyExpr::new(
- TyExprKind::Expr(pi_ekind),
- Some(pi_ty),
- Span::Artificial,
- );
- ty.eval(env.as_nzenv())
+ type_one_layer(env, pi_ekind, Span::Artificial)?
+ .eval(env.as_nzenv())
}
ExprKind::Pi(_, annot, body) => {
let ks = match annot.get_type()?.as_const() {
@@ -187,7 +182,7 @@ fn type_one_layer(
}
let ty = type_of_recordtype(
- span,
+ span.clone(),
kts.iter()
.map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
)?;
@@ -206,7 +201,10 @@ fn type_one_layer(
};
}
- type_of_recordtype(span, kts.iter().map(|(_, t)| Cow::Borrowed(t)))?
+ type_of_recordtype(
+ span.clone(),
+ kts.iter().map(|(_, t)| Cow::Borrowed(t)),
+ )?
}
ExprKind::UnionType(kts) => {
use std::collections::hash_map::Entry;
@@ -389,7 +387,7 @@ fn type_one_layer(
// Construct the final record type
let ty = type_of_recordtype(
- span,
+ span.clone(),
kts.iter()
.map(|(_, t)| Cow::Owned(t.to_tyexpr(env.as_varenv()))),
)?;
@@ -401,9 +399,7 @@ fn type_one_layer(
x.get_type()?.to_tyexpr(env.as_varenv()),
y.get_type()?.to_tyexpr(env.as_varenv()),
);
- let ty = type_one_layer(env, &ekind, Span::Artificial)?;
- TyExpr::new(TyExprKind::Expr(ekind), Some(ty), Span::Artificial)
- .eval(env.as_nzenv())
+ type_one_layer(env, ekind, Span::Artificial)?.eval(env.as_nzenv())
}
ExprKind::BinOp(BinOp::RecursiveRecordTypeMerge, x, y) => {
let x_val = x.eval(env.as_nzenv());
@@ -420,7 +416,7 @@ fn type_one_layer(
if let Some(ty) = kts_y.get(k) {
type_one_layer(
env,
- &ExprKind::BinOp(
+ ExprKind::BinOp(
BinOp::RecursiveRecordTypeMerge,
tx.to_tyexpr(env.as_varenv()),
ty.to_tyexpr(env.as_varenv()),
@@ -547,9 +543,14 @@ fn type_one_layer(
);
}
- closure.remove_binder().or_else(|()| {
- span_err("MergeReturnTypeIsDependent")
- })?
+ match closure.remove_binder() {
+ Ok(v) => v,
+ Err(()) => {
+ return span_err(
+ "MergeReturnTypeIsDependent",
+ )
+ }
+ }
}
_ => {
return mkerr(
@@ -752,8 +753,35 @@ fn type_one_layer(
selection_val
}
- ExprKind::Completion(_, _) => unimplemented!("record completion"),
- })
+ ExprKind::Completion(ty, compl) => {
+ let ty_field_default = type_one_layer(
+ env,
+ ExprKind::Field(ty.clone(), "default".into()),
+ span.clone(),
+ )?;
+ let ty_field_type = type_one_layer(
+ env,
+ ExprKind::Field(ty.clone(), "Type".into()),
+ span.clone(),
+ )?;
+ let merge = type_one_layer(
+ env,
+ ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ ty_field_default,
+ compl.clone(),
+ ),
+ span.clone(),
+ )?;
+ return type_one_layer(
+ env,
+ ExprKind::Annot(merge, ty_field_type),
+ span.clone(),
+ );
+ }
+ };
+
+ Ok(TyExpr::new(TyExprKind::Expr(ekind), Some(ty), span))
}
/// `type_with` typechecks an expressio in the provided environment.
@@ -809,9 +837,7 @@ pub(crate) fn type_with(
}
_ => ekind.traverse_ref(|e| type_with(env, e))?,
};
-
- let ty = type_one_layer(env, &ekind, expr.span())?;
- (TyExprKind::Expr(ekind), Some(ty))
+ return type_one_layer(env, ekind, expr.span());
}
};