diff options
| -rw-r--r-- | dhall/build.rs | 3 | ||||
| -rw-r--r-- | dhall/src/semantics/hir.rs | 2 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/normalize.rs | 20 | ||||
| -rw-r--r-- | dhall/src/semantics/resolve.rs | 45 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 34 |
5 files changed, 49 insertions, 55 deletions
diff --git a/dhall/build.rs b/dhall/build.rs index 8deb637..7c62083 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -299,9 +299,6 @@ fn generate_tests() -> std::io::Result<()> { || path == "unit/RecursiveRecordMergeWithinFieldSelection0" || path == "unit/RecursiveRecordMergeWithinFieldSelection2" || path == "unit/RecursiveRecordMergeWithinFieldSelection3" - // TODO: record completion - || path == "simple/completion" - || path == "unit/Completion" }), input_type: FileType::Text, output_type: Some(FileType::Text), 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 { |