summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/core/value.rs8
-rw-r--r--dhall/src/phase/binary.rs11
-rw-r--r--dhall/src/phase/normalize.rs22
-rw-r--r--dhall/src/phase/typecheck.rs75
-rw-r--r--dhall_syntax/src/parser.rs3
-rw-r--r--dhall_syntax/src/printer.rs3
6 files changed, 74 insertions, 48 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index bc8fa34..f47f1b2 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -47,6 +47,7 @@ pub enum Value {
DoubleLit(NaiveDouble),
EmptyOptionalLit(TypeThunk),
NEOptionalLit(Thunk),
+ // EmptyListLit(t) means `[] : List t`
EmptyListLit(TypeThunk),
NEListLit(Vec<Thunk>),
RecordLit(HashMap<Label, Thunk>),
@@ -128,9 +129,10 @@ impl Value {
Value::NEOptionalLit(n) => {
rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha)))
}
- Value::EmptyListLit(n) => {
- rc(ExprF::EmptyListLit(n.normalize_to_expr_maybe_alpha(alpha)))
- }
+ Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App(
+ rc(ExprF::Builtin(Builtin::List)),
+ n.normalize_to_expr_maybe_alpha(alpha),
+ )))),
Value::NEListLit(elts) => rc(ExprF::NEListLit(
elts.iter()
.map(|n| n.normalize_to_expr_maybe_alpha(alpha))
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index bab3fd8..66b235f 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -106,7 +106,7 @@ fn cbor_value_to_dhall(
}
[U64(4), t] => {
let t = cbor_value_to_dhall(&t)?;
- EmptyListLit(t)
+ EmptyListLit(rc(App(rc(ExprF::Builtin(Builtin::List)), t)))
}
[U64(4), Null, rest..] => {
let rest = rest
@@ -413,6 +413,7 @@ where
S: serde::ser::Serializer,
{
use cbor::Value::{String, I64, U64};
+ use dhall_syntax::Builtin;
use dhall_syntax::ExprF::*;
use std::iter::once;
@@ -471,7 +472,13 @@ where
}
Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
- EmptyListLit(x) => ser_seq!(ser; tag(4), expr(x)),
+ EmptyListLit(x) => match x.as_ref() {
+ App(f, a) => match f.as_ref() {
+ ExprF::Builtin(Builtin::List) => ser_seq!(ser; tag(4), expr(a)),
+ _ => unreachable!(),
+ },
+ _ => unreachable!(),
+ },
NEListLit(xs) => ser.collect_seq(
once(tag(4)).chain(once(null())).chain(xs.iter().map(expr)),
),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 4bc0f04..2e9f258 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -622,9 +622,9 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
use Value::{
- BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit,
- NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit,
- UnionConstructor, UnionLit, UnionType,
+ AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
+ NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
+ TextLit, UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
@@ -651,8 +651,20 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
- ExprF::EmptyListLit(t) => {
- Ret::Value(EmptyListLit(TypeThunk::from_thunk(t)))
+ ExprF::EmptyListLit(ref t) => {
+ // Check if the type is of the form `List x`
+ let t_borrow = t.as_value();
+ match &*t_borrow {
+ AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
+ Ret::Value(EmptyListLit(TypeThunk::from_thunk(
+ args[0].clone(),
+ )))
+ }
+ _ => {
+ drop(t_borrow);
+ Ret::Expr(expr)
+ }
+ }
}
ExprF::NEListLit(elts) => {
Ret::Value(NEListLit(elts.into_iter().collect()))
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index fc6c1da..35bf3a9 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -164,37 +164,6 @@ fn tck_union_type(
))
}
-fn tck_list_type(ctx: &TypecheckContext, t: Type) -> Result<Typed, TypeError> {
- use crate::error::TypeMessage::*;
- ensure_simple_type!(
- t,
- TypeError::new(ctx, InvalidListType(t.to_normalized())),
- );
- Ok(Typed::from_thunk_and_type(
- Value::from_builtin(Builtin::List)
- .app(t.to_value())
- .into_thunk(),
- Type::from_const(Const::Type),
- ))
-}
-
-fn tck_optional_type(
- ctx: &TypecheckContext,
- t: Type,
-) -> Result<Typed, TypeError> {
- use crate::error::TypeMessage::*;
- ensure_simple_type!(
- t,
- TypeError::new(ctx, InvalidOptionalType(t.to_normalized())),
- );
- Ok(Typed::from_thunk_and_type(
- Value::from_builtin(Builtin::Optional)
- .app(t.to_value())
- .into_thunk(),
- Type::from_const(Const::Type),
- ))
-}
-
fn function_check(a: Const, b: Const) -> Result<Const, ()> {
use dhall_syntax::Const::*;
match (a, b) {
@@ -460,7 +429,17 @@ fn type_last_layer(
}
EmptyListLit(t) => {
let t = t.to_type();
- Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type()))
+ match &t.to_value() {
+ Value::AppliedBuiltin(dhall_syntax::Builtin::List, args)
+ if args.len() == 1 => {}
+ _ => {
+ return Err(TypeError::new(
+ ctx,
+ InvalidListType(t.to_normalized()),
+ ))
+ }
+ }
+ Ok(RetTypeOnly(t))
}
NEListLit(xs) => {
let mut iter = xs.iter().enumerate();
@@ -476,12 +455,38 @@ fn type_last_layer(
))
);
}
- let t = x.get_type()?.into_owned();
- Ok(RetTypeOnly(tck_list_type(ctx, t)?.to_type()))
+ let t = x.get_type()?;
+ ensure_simple_type!(
+ t,
+ TypeError::new(ctx, InvalidListType(t.to_normalized())),
+ );
+
+ Ok(RetTypeOnly(
+ Typed::from_thunk_and_type(
+ Value::from_builtin(dhall_syntax::Builtin::List)
+ .app(t.to_value())
+ .into_thunk(),
+ Type::from_const(dhall_syntax::Const::Type),
+ )
+ .to_type(),
+ ))
}
SomeLit(x) => {
let t = x.get_type()?.into_owned();
- Ok(RetTypeOnly(tck_optional_type(ctx, t)?.to_type()))
+ ensure_simple_type!(
+ t,
+ TypeError::new(ctx, InvalidOptionalType(t.to_normalized())),
+ );
+
+ Ok(RetTypeOnly(
+ Typed::from_thunk_and_type(
+ Value::from_builtin(dhall_syntax::Builtin::Optional)
+ .app(t.to_value())
+ .into_thunk(),
+ Type::from_const(dhall_syntax::Const::Type),
+ )
+ .to_type(),
+ ))
}
RecordType(kts) => Ok(RetWhole(tck_record_type(
ctx,
diff --git a/dhall_syntax/src/parser.rs b/dhall_syntax/src/parser.rs
index 8355ebf..0832af3 100644
--- a/dhall_syntax/src/parser.rs
+++ b/dhall_syntax/src/parser.rs
@@ -752,7 +752,8 @@ make_parser! {
spanned(span, Merge(x, y, Some(z)))
},
[List(()), expression(x)] => {
- spanned(span, EmptyListLit(x))
+ let list = unspanned(Builtin(crate::Builtin::List));
+ spanned(span, EmptyListLit(unspanned(App(list, x))))
},
[expression(e)] => e,
));
diff --git a/dhall_syntax/src/printer.rs b/dhall_syntax/src/printer.rs
index 2b2bbcc..52d3d81 100644
--- a/dhall_syntax/src/printer.rs
+++ b/dhall_syntax/src/printer.rs
@@ -27,7 +27,7 @@ impl<SE: Display + Clone, E: Display> Display for ExprF<SE, E> {
write!(f, " = {} in {}", c, d)?;
}
EmptyListLit(t) => {
- write!(f, "[] : List {}", t)?;
+ write!(f, "[] : {}", t)?;
}
NEListLit(es) => {
fmt_list("[", ", ", "]", es, f, Display::fmt)?;
@@ -182,7 +182,6 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
a.phase(PrintPhase::BinOp(op)),
b.phase(PrintPhase::BinOp(op)),
),
- EmptyListLit(t) => EmptyListLit(t.phase(Import)),
SomeLit(e) => SomeLit(e.phase(Import)),
ExprF::App(f, a) => ExprF::App(f.phase(Import), a.phase(Import)),
Field(a, b) => Field(a.phase(Primitive), b),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 12:21:43 +0000