diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/build.rs | 13 | ||||
| -rw-r--r-- | dhall/src/semantics/tck/typecheck.rs | 76 |
2 files changed, 51 insertions, 38 deletions
diff --git a/dhall/build.rs b/dhall/build.rs index 36acc02..ab709b8 100644 --- a/dhall/build.rs +++ b/dhall/build.rs @@ -309,9 +309,6 @@ fn generate_tests() -> std::io::Result<()> { false // Too slow || path == "prelude" - // TODO: record completion - || path == "simple/completion" - || path == "unit/Completion" }), input_type: FileType::Text, output_type: Some(FileType::Text), @@ -322,11 +319,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeInferenceFailure", path_filter: Box::new(|path: &str| { false - // TODO: record completion - || path == "unit/CompletionMissingRequiredField" - || path == "unit/CompletionWithWrongDefaultType" - || path == "unit/CompletionWithWrongFieldName" - || path == "unit/CompletionWithWrongOverridenType" // TODO: enable free variable checking || path == "unit/MergeHandlerFreeVar" }), @@ -339,11 +331,6 @@ fn generate_tests() -> std::io::Result<()> { variant: "TypeError", path_filter: Box::new(|path: &str| { false - // TODO: record completion - || path == "unit/CompletionMissingRequiredField" - || path == "unit/CompletionWithWrongDefaultType" - || path == "unit/CompletionWithWrongFieldName" - || path == "unit/CompletionWithWrongOverridenType" // TODO: enable free variable checking || path == "unit/MergeHandlerFreeVar" }), 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()); } }; |