summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2020-02-15 19:10:52 +0000
committerNadrieril2020-02-15 19:15:32 +0000
commit5057144ed99bc4e1a76a0840dd39fc1bd862665c (patch)
tree89b3a5b6bed6732668df9001d5267db503186038 /dhall/src
parentd65d639ff93691adbf0a208edb99736003bc64bd (diff)
Desugar Completion during resolution
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/hir.rs2
-rw-r--r--dhall/src/semantics/nze/normalize.rs20
-rw-r--r--dhall/src/semantics/resolve.rs45
-rw-r--r--dhall/src/semantics/tck/typecheck.rs34
4 files changed, 49 insertions, 52 deletions
diff --git a/dhall/src/semantics/hir.rs b/dhall/src/semantics/hir.rs
index 42f151e..c8258ff 100644
--- a/dhall/src/semantics/hir.rs
+++ b/dhall/src/semantics/hir.rs
@@ -14,7 +14,7 @@ pub struct AlphaVar {
pub(crate) enum HirKind {
/// A resolved variable (i.e. a DeBruijn index)
Var(AlphaVar),
- // Forbidden ExprKind variants: Var, Import
+ // Forbidden ExprKind variants: Var, Import, Completion
Expr(ExprKind<Hir>),
}
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index c8dd5ae..0e09511 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -231,17 +231,16 @@ pub(crate) fn normalize_one_layer(
};
let ret = match expr {
- ExprKind::Import(_) => unreachable!(
- "There should remain no imports in a resolved expression"
- ),
- // Those cases have already been completely handled in the typechecking phase (using
- // `RetWhole`), so they won't appear here.
- ExprKind::Lam(..)
- | ExprKind::Pi(..)
- | ExprKind::Let(..)
- | ExprKind::Var(_) => {
- unreachable!("This case should have been handled in typecheck")
+ ExprKind::Import(..) | ExprKind::Completion(..) => {
+ unreachable!("This case should have been handled in resolution")
}
+ ExprKind::Var(..)
+ | ExprKind::Lam(..)
+ | ExprKind::Pi(..)
+ | ExprKind::Let(..) => unreachable!(
+ "This case should have been handled in normalize_hir_whnf"
+ ),
+
ExprKind::Annot(x, _) => Ret::Value(x),
ExprKind::Const(c) => Ret::Value(Value::from_const(c)),
ExprKind::Builtin(b) => Ret::Value(Value::from_builtin_env(b, env)),
@@ -391,7 +390,6 @@ pub(crate) fn normalize_one_layer(
ExprKind::ProjectionByExpr(_, _) => {
unimplemented!("selection by expression")
}
- ExprKind::Completion(_, _) => unimplemented!("record completion"),
ExprKind::Merge(ref handlers, ref variant, _) => {
match handlers.kind() {
diff --git a/dhall/src/semantics/resolve.rs b/dhall/src/semantics/resolve.rs
index fac88d2..3038597 100644
--- a/dhall/src/semantics/resolve.rs
+++ b/dhall/src/semantics/resolve.rs
@@ -105,9 +105,9 @@ fn traverse_resolve_expr(
expr: &Expr,
f: &mut impl FnMut(Import) -> Result<Hir, Error>,
) -> Result<Hir, Error> {
- let kind = match expr.kind() {
+ Ok(match expr.kind() {
ExprKind::Var(var) => match name_env.unlabel_var(&var) {
- Some(v) => HirKind::Var(v),
+ Some(v) => Hir::new(HirKind::Var(v), expr.span()),
None => mkerr(
ErrorBuilder::new(format!("unbound variable `{}`", var))
.span_err(expr.span(), "not found in this scope")
@@ -115,16 +115,38 @@ fn traverse_resolve_expr(
)?,
},
ExprKind::BinOp(BinOp::ImportAlt, l, r) => {
- return match traverse_resolve_expr(name_env, l, f) {
- Ok(l) => Ok(l),
+ match traverse_resolve_expr(name_env, l, f) {
+ Ok(l) => l,
Err(_) => {
match traverse_resolve_expr(name_env, r, f) {
- Ok(r) => Ok(r),
+ Ok(r) => r,
// TODO: keep track of the other error too
- Err(e) => Err(e),
+ Err(e) => return Err(e),
}
}
- };
+ }
+ }
+ // Desugar
+ ExprKind::Completion(ty, compl) => {
+ let ty_field_default = Expr::new(
+ ExprKind::Field(ty.clone(), "default".into()),
+ expr.span(),
+ );
+ let merged = Expr::new(
+ ExprKind::BinOp(
+ BinOp::RightBiasedRecordMerge,
+ ty_field_default,
+ compl.clone(),
+ ),
+ expr.span(),
+ );
+ let ty_field_type = Expr::new(
+ ExprKind::Field(ty.clone(), "Type".into()),
+ expr.span(),
+ );
+ let desugared =
+ Expr::new(ExprKind::Annot(merged, ty_field_type), expr.span());
+ traverse_resolve_expr(name_env, &desugared, f)?
}
kind => {
let kind = kind.traverse_ref_maybe_binder(|l, e| {
@@ -137,14 +159,13 @@ fn traverse_resolve_expr(
}
Ok::<_, Error>(hir)
})?;
- match kind {
+ let kind = match kind {
ExprKind::Import(import) => f(import)?.kind().clone(),
kind => HirKind::Expr(kind),
- }
+ };
+ Hir::new(kind, expr.span())
}
- };
-
- Ok(Hir::new(kind, expr.span()))
+ })
}
fn resolve_with_env(
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index a8a2d95..36f7173 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -75,12 +75,14 @@ fn type_one_layer(
let span_err = |msg: &str| mk_span_err(span.clone(), msg);
let ty = match &ekind {
- ExprKind::Import(..) => unreachable!(
- "There should remain no imports in a resolved expression"
- ),
+ ExprKind::Import(..) | ExprKind::Completion(..) => {
+ unreachable!("This case should have been handled in resolution")
+ }
ExprKind::Var(..)
| ExprKind::Const(Const::Sort)
- | ExprKind::Annot(..) => unreachable!(), // Handled in type_with
+ | ExprKind::Annot(..) => {
+ unreachable!("This case should have been handled in type_with")
+ }
ExprKind::Lam(binder, annot, body) => {
if annot.ty().as_const().is_none() {
@@ -739,30 +741,6 @@ fn type_one_layer(
selection_val
}
- ExprKind::Completion(ty, compl) => {
- let ty_field_default = type_one_layer(
- env,
- ExprKind::Field(ty.clone(), "default".into()),
- None,
- span.clone(),
- )?;
- let ty_field_type = type_one_layer(
- env,
- ExprKind::Field(ty.clone(), "Type".into()),
- None,
- span.clone(),
- )?;
- return type_one_layer(
- env,
- ExprKind::BinOp(
- BinOp::RightBiasedRecordMerge,
- ty_field_default,
- compl.clone(),
- ),
- Some(ty_field_type.eval(env)),
- span.clone(),
- );
- }
};
if let Some(annot) = annot {