From 4cd6c39d6d61c1d5a2670fe52c79bce4f11facdb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 12 Mar 2019 00:14:50 +0100 Subject: Handle Some and None builtins Closes #19 --- dhall/src/normalize.rs | 11 ++++++++- dhall/tests/tests.rs | 64 +++++++++++++++++++++++++------------------------- dhall_core/src/core.rs | 24 ++++++++++++++----- 3 files changed, 60 insertions(+), 39 deletions(-) diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 8948443..50a1625 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -36,6 +36,8 @@ where normalize_whnf(&b3) } (Builtin(b), a) => match (b, normalize_whnf(a)) { + (OptionalSome, a) => OptionalLit(None, vec![a]), + (OptionalNone, a) => OptionalLit(Some(bx(a)), vec![]), (NaturalIsZero, NaturalLit(n)) => BoolLit(n == 0), (NaturalEven, NaturalLit(n)) => BoolLit(n % 2 == 0), (NaturalOdd, NaturalLit(n)) => BoolLit(n % 2 != 0), @@ -149,7 +151,7 @@ where ) => { let e2: Expr<_, _> = xs.into_iter().fold( (**nothing).clone(), - |y, _| { + |_, y| { let y = bx(y); dhall_expr!(just y) }, @@ -186,6 +188,13 @@ where BoolLit(false) => normalize_whnf(f), b2 => BoolIf(bx(b2), t.clone(), f.clone()), }, + OptionalLit(t, es) => { + if !es.is_empty() { + OptionalLit(None, es.clone()) + } else { + OptionalLit(t.clone(), es.clone()) + } + } BinOp(o, x, y) => match (o, normalize_whnf(&x), normalize_whnf(&y)) { (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(x && y), (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(x || y), diff --git a/dhall/tests/tests.rs b/dhall/tests/tests.rs index 70de466..68125a0 100644 --- a/dhall/tests/tests.rs +++ b/dhall/tests/tests.rs @@ -61,14 +61,14 @@ make_spec_test!(normalization, spec_normalization_success_prelude_List_fold_1, " make_spec_test!(normalization, spec_normalization_success_prelude_List_fold_2, "normalization/success/prelude/List/fold/2"); // make_spec_test!(normalization, spec_normalization_success_prelude_List_generate_0, "normalization/success/prelude/List/generate/0"); // make_spec_test!(normalization, spec_normalization_success_prelude_List_generate_1, "normalization/success/prelude/List/generate/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_List_head_0, "normalization/success/prelude/List/head/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_List_head_1, "normalization/success/prelude/List/head/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_List_head_0, "normalization/success/prelude/List/head/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_List_head_1, "normalization/success/prelude/List/head/1"); // make_spec_test!(normalization, spec_normalization_success_prelude_List_indexed_0, "normalization/success/prelude/List/indexed/0"); // make_spec_test!(normalization, spec_normalization_success_prelude_List_indexed_1, "normalization/success/prelude/List/indexed/1"); // make_spec_test!(normalization, spec_normalization_success_prelude_List_iterate_0, "normalization/success/prelude/List/iterate/0"); // make_spec_test!(normalization, spec_normalization_success_prelude_List_iterate_1, "normalization/success/prelude/List/iterate/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_List_last_0, "normalization/success/prelude/List/last/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_List_last_1, "normalization/success/prelude/List/last/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_List_last_0, "normalization/success/prelude/List/last/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_List_last_1, "normalization/success/prelude/List/last/1"); make_spec_test!(normalization, spec_normalization_success_prelude_List_length_0, "normalization/success/prelude/List/length/0"); make_spec_test!(normalization, spec_normalization_success_prelude_List_length_1, "normalization/success/prelude/List/length/1"); make_spec_test!(normalization, spec_normalization_success_prelude_List_map_0, "normalization/success/prelude/List/map/0"); @@ -106,36 +106,36 @@ make_spec_test!(normalization, spec_normalization_success_prelude_Natural_sum_1, // make_spec_test!(normalization, spec_normalization_success_prelude_Natural_toDouble_1, "normalization/success/prelude/Natural/toDouble/1"); make_spec_test!(normalization, spec_normalization_success_prelude_Natural_toInteger_0, "normalization/success/prelude/Natural/toInteger/0"); make_spec_test!(normalization, spec_normalization_success_prelude_Natural_toInteger_1, "normalization/success/prelude/Natural/toInteger/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_all_0, "normalization/success/prelude/Optional/all/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_all_1, "normalization/success/prelude/Optional/all/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_any_0, "normalization/success/prelude/Optional/any/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_any_1, "normalization/success/prelude/Optional/any/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_build_0, "normalization/success/prelude/Optional/build/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_build_1, "normalization/success/prelude/Optional/build/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_concat_0, "normalization/success/prelude/Optional/concat/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_concat_1, "normalization/success/prelude/Optional/concat/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_concat_2, "normalization/success/prelude/Optional/concat/2"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_filter_0, "normalization/success/prelude/Optional/filter/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_filter_1, "normalization/success/prelude/Optional/filter/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_fold_0, "normalization/success/prelude/Optional/fold/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_fold_1, "normalization/success/prelude/Optional/fold/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_head_0, "normalization/success/prelude/Optional/head/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_head_1, "normalization/success/prelude/Optional/head/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_all_0, "normalization/success/prelude/Optional/all/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_all_1, "normalization/success/prelude/Optional/all/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_any_0, "normalization/success/prelude/Optional/any/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_any_1, "normalization/success/prelude/Optional/any/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_build_0, "normalization/success/prelude/Optional/build/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_build_1, "normalization/success/prelude/Optional/build/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_concat_0, "normalization/success/prelude/Optional/concat/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_concat_1, "normalization/success/prelude/Optional/concat/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_concat_2, "normalization/success/prelude/Optional/concat/2"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_filter_0, "normalization/success/prelude/Optional/filter/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_filter_1, "normalization/success/prelude/Optional/filter/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_fold_0, "normalization/success/prelude/Optional/fold/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_fold_1, "normalization/success/prelude/Optional/fold/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_head_0, "normalization/success/prelude/Optional/head/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_head_1, "normalization/success/prelude/Optional/head/1"); make_spec_test!(normalization, spec_normalization_success_prelude_Optional_head_2, "normalization/success/prelude/Optional/head/2"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_last_0, "normalization/success/prelude/Optional/last/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_last_1, "normalization/success/prelude/Optional/last/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_last_0, "normalization/success/prelude/Optional/last/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_last_1, "normalization/success/prelude/Optional/last/1"); make_spec_test!(normalization, spec_normalization_success_prelude_Optional_last_2, "normalization/success/prelude/Optional/last/2"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_length_0, "normalization/success/prelude/Optional/length/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_length_1, "normalization/success/prelude/Optional/length/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_map_0, "normalization/success/prelude/Optional/map/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_map_1, "normalization/success/prelude/Optional/map/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_null_0, "normalization/success/prelude/Optional/null/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_null_1, "normalization/success/prelude/Optional/null/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_toList_0, "normalization/success/prelude/Optional/toList/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_toList_1, "normalization/success/prelude/Optional/toList/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_unzip_0, "normalization/success/prelude/Optional/unzip/0"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Optional_unzip_1, "normalization/success/prelude/Optional/unzip/1"); -// make_spec_test!(normalization, spec_normalization_success_prelude_Text_concat_0, "normalization/success/prelude/Text/concat/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_length_0, "normalization/success/prelude/Optional/length/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_length_1, "normalization/success/prelude/Optional/length/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_map_0, "normalization/success/prelude/Optional/map/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_map_1, "normalization/success/prelude/Optional/map/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_null_0, "normalization/success/prelude/Optional/null/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_null_1, "normalization/success/prelude/Optional/null/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_toList_0, "normalization/success/prelude/Optional/toList/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_toList_1, "normalization/success/prelude/Optional/toList/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_unzip_0, "normalization/success/prelude/Optional/unzip/0"); +make_spec_test!(normalization, spec_normalization_success_prelude_Optional_unzip_1, "normalization/success/prelude/Optional/unzip/1"); +make_spec_test!(normalization, spec_normalization_success_prelude_Text_concat_0, "normalization/success/prelude/Text/concat/0"); make_spec_test!(normalization, spec_normalization_success_prelude_Text_concat_1, "normalization/success/prelude/Text/concat/1"); // make_spec_test!(normalization, spec_normalization_success_prelude_Text_concatMap_0, "normalization/success/prelude/Text/concatMap/0"); make_spec_test!(normalization, spec_normalization_success_prelude_Text_concatMap_1, "normalization/success/prelude/Text/concatMap/1"); diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 9c96b2a..9f4beb3 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -257,6 +257,8 @@ pub enum Builtin { Text, List, Optional, + OptionalSome, + OptionalNone, NaturalBuild, NaturalFold, NaturalIsZero, @@ -462,13 +464,19 @@ impl Expr { Ok(()) } &OptionalLit(ref t, ref es) => { - fmt_list("[", "]", es, f, |e, f| e.fmt(f))?; - match t { - Some(t) => { - write!(f, " : Optional ")?; - t.fmt_e(f)? + match es.iter().next() { + None => { + write!(f, "None ")?; + t.as_ref().unwrap().fmt_e(f)?; + } + Some(e) => { + write!(f, "Some ")?; + e.fmt_e(f)?; + if let Some(t) = t { + write!(f, " : Optional ")?; + t.fmt_e(f)?; + } } - None => {} } Ok(()) } @@ -624,6 +632,8 @@ impl Display for Builtin { Text => "Text", List => "List", Optional => "Optional", + OptionalSome => "Some", + OptionalNone => "None", NaturalBuild => "Natural/build", NaturalFold => "Natural/fold", NaturalIsZero => "Natural/isZero", @@ -659,6 +669,8 @@ impl Builtin { "Text" => Some(Text), "List" => Some(List), "Optional" => Some(Optional), + "Some" => Some(OptionalSome), + "None" => Some(OptionalNone), "Natural/build" => Some(NaturalBuild), "Natural/fold" => Some(NaturalFold), "Natural/isZero" => Some(NaturalIsZero), -- cgit v1.2.3