diff options
author | Nadrieril | 2019-04-15 12:22:02 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-15 12:22:02 +0200 |
commit | 63aa21c581933a10b2b1ab96c632c72834cf2115 (patch) | |
tree | 9e534d7a4107fae5aae33637a5ea7c8a2f58c873 /dhall/src/typecheck.rs | |
parent | 75420d0822652d6592b74199ea35281dbdf84efb (diff) |
Handle empty optionals correctly
Closes #78
Diffstat (limited to '')
-rw-r--r-- | dhall/src/typecheck.rs | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index b8f2d86..5162f4f 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -266,6 +266,9 @@ fn type_of_builtin<S>(b: Builtin) -> Expr<S, Normalized<'static>> { forall (nothing: optional) -> optional ), + OptionalNone => dhall::expr!( + forall (a: Type) -> Optional a + ), _ => panic!("Unimplemented typecheck case: {:?}", b), } } @@ -544,6 +547,17 @@ fn type_last_layer( let t = x.get_type_move()?.into_normalized()?.into_expr(); Ok(RetExpr(dhall::expr!(List t))) } + OldOptionalLit(None, t) => { + let t = t.into_expr(); + let e = dhall::subexpr!(None t); + Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) + } + OldOptionalLit(Some(x), t) => { + let x = x.into_expr(); + let t = t.into_expr(); + let e = dhall::subexpr!(Some x : Optional t); + Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) + } EmptyOptionalLit(t) => { let t = t.normalize().into_type(); ensure_simple_type!( |