summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
authorNadrieril2020-01-17 16:09:35 +0000
committerNadrieril2020-01-17 16:20:55 +0000
commit37acac4b972b38e8dbe2d174dae1031e5a8eda67 (patch)
tree02a9105c005d57af110a47130501078254411d0e /dhall/src/semantics
parent06f619e8b1654e506840d17dc1cbff4f2d9795c3 (diff)
Tweak: handle empty lists in typeck
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/phase/normalize.rs20
-rw-r--r--dhall/src/semantics/phase/typecheck.rs14
2 files changed, 14 insertions, 20 deletions
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 615b2ff..8f9a58a 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -590,9 +590,9 @@ pub(crate) fn normalize_one_layer(
ty: &Value,
) -> ValueKind<Value> {
use ValueKind::{
- AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit,
- IntegerLit, NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
- UnionConstructor, UnionLit, UnionType,
+ BoolLit, DoubleLit, EmptyOptionalLit, IntegerLit, NEListLit,
+ NEOptionalLit, NaturalLit, RecordLit, TextLit, UnionConstructor,
+ UnionLit, UnionType,
};
let ret = match expr {
@@ -609,6 +609,7 @@ pub(crate) fn normalize_one_layer(
| ExprKind::Builtin(_)
| ExprKind::Var(_)
| ExprKind::Annot(_, _)
+ | ExprKind::EmptyListLit(_)
| ExprKind::RecordType(_)
| ExprKind::UnionType(_) => {
unreachable!("This case should have been handled in typecheck")
@@ -620,19 +621,6 @@ pub(crate) fn normalize_one_layer(
ExprKind::IntegerLit(n) => Ret::ValueKind(IntegerLit(n)),
ExprKind::DoubleLit(n) => Ret::ValueKind(DoubleLit(n)),
ExprKind::SomeLit(e) => Ret::ValueKind(NEOptionalLit(e)),
- ExprKind::EmptyListLit(ref t) => {
- // Check if the type is of the form `List x`
- let t_borrow = t.as_whnf();
- match &*t_borrow {
- AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
- Ret::ValueKind(EmptyListLit(args[0].clone()))
- }
- _ => {
- drop(t_borrow);
- Ret::Expr(expr)
- }
- }
- }
ExprKind::NEListLit(elts) => {
Ret::ValueKind(NEListLit(elts.into_iter().collect()))
}
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index c77d9c4..852f41b 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -433,12 +433,18 @@ fn type_last_layer(
RetTypeOnly(y.get_type()?)
}
EmptyListLit(t) => {
- match &*t.as_whnf() {
+ let arg = match &*t.as_whnf() {
ValueKind::AppliedBuiltin(syntax::Builtin::List, args)
- if args.len() == 1 => {}
+ if args.len() == 1 =>
+ {
+ args[0].clone()
+ }
_ => return mkerr(InvalidListType(t.clone())),
- }
- RetTypeOnly(t.clone())
+ };
+ RetWhole(Value::from_kind_and_type(
+ ValueKind::EmptyListLit(arg),
+ t.clone(),
+ ))
}
NEListLit(xs) => {
let mut iter = xs.iter().enumerate();