From 705433487da3cd3b4517fcf74b0497c76dbb4080 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 Aug 2019 22:36:43 +0200 Subject: Prepare for https://github.com/dhall-lang/dhall-lang/pull/630 --- dhall/src/core/value.rs | 8 +++-- dhall/src/phase/binary.rs | 11 +++++-- dhall/src/phase/normalize.rs | 22 ++++++++++--- dhall/src/phase/typecheck.rs | 75 +++++++++++++++++++++++--------------------- 4 files changed, 71 insertions(+), 45 deletions(-) (limited to 'dhall') 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), RecordLit(HashMap), @@ -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> { pub fn normalize_one_layer(expr: ExprF) -> 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) -> 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 { - 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 { - 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 { 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, -- cgit v1.2.3