From 5f0331e9a339768dfa40018d1f82c4815dbd11af Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 18 Mar 2019 05:50:09 +0100 Subject: Implement a few more primitives --- dhall/src/normalize.rs | 60 ++++++++++++++++++++++++++++++++------------ dhall/src/typecheck.rs | 1 - dhall/tests/normalization.rs | 42 +++++++++++++++---------------- dhall_generator/src/lib.rs | 8 ++++++ 4 files changed, 73 insertions(+), 38 deletions(-) diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index c728dd0..e335fbb 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -27,12 +27,13 @@ where ListHead => (2, Some(1)), ListLast => (2, Some(1)), ListReverse => (2, Some(1)), + ListIndexed => (2, Some(1)), ListBuild => (2, Some(1)), OptionalBuild => (2, Some(1)), ListFold => (5, Some(1)), OptionalFold => (5, Some(1)), NaturalBuild => (1, Some(0)), - NaturalFold => (1, Some(0)), + NaturalFold => (4, Some(0)), _ => (0, None), }; // Abort if not enough arguments present @@ -78,6 +79,17 @@ where let ys = ys.iter().rev().cloned().collect(); rc(NEListLit(ys)) } + (ListIndexed, Some(EmptyListLit(t)), _) => { + let t = Rc::clone(t); + dhall_expr!([] : List ({ index : Natural, value : t })) + } + (ListIndexed, Some(NEListLit(xs)), _) => { + let xs = xs.iter().cloned().enumerate().map(|(i, e)| { + let i = rc(NaturalLit(i)); + dhall_expr!({ index = i, value = e }) + }).collect(); + rc(NEListLit(xs)) + } (ListBuild, _, [a0, g, ..]) => { loop { if let App(f2, args2) = g.as_ref() { @@ -142,24 +154,40 @@ where // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) // } - (NaturalBuild, Some(App(f2, args2)), _) => { - match (f2.as_ref(), args2.as_slice()) { - // fold/build fusion - (Builtin(NaturalFold), [x, rest..]) => { - rc(App(x.clone(), rest.to_vec())) - } - _ => return rc(App(f, args)), + (NaturalBuild, _, [g, ..]) => { + loop { + if let App(f2, args2) = g.as_ref() { + if let (Builtin(NaturalFold), [x, rest..]) = + (f2.as_ref(), args2.as_slice()) + { + // fold/build fusion + break rc(App(x.clone(), rest.to_vec())); + } + }; + // TODO: use Embed to avoid reevaluating g + break dhall_expr!(g Natural (λ(x : Natural) -> x + 1) 0) } } - (NaturalFold, Some(App(f2, args2)), _) => { - match (f2.as_ref(), args2.as_slice()) { - // fold/build fusion - (Builtin(NaturalBuild), [x, rest..]) => { - rc(App(x.clone(), rest.to_vec())) - } - _ => return rc(App(f, args)), - } + (NaturalFold, Some(NaturalLit(0)), [_, _, _, zero]) => { + Rc::clone(zero) } + (NaturalFold, Some(NaturalLit(n)), [_, t, succ, zero]) => { + let fold = rc(Builtin(NaturalFold)); + let n = rc(NaturalLit(n-1)); + let t = Rc::clone(t); + let succ = Rc::clone(succ); + let zero = Rc::clone(zero); + dhall_expr!(succ (fold n t succ zero)) + } + // (NaturalFold, Some(App(f2, args2)), _) => { + // match (f2.as_ref(), args2.as_slice()) { + // // fold/build fusion + // (Builtin(NaturalBuild), [x, rest..]) => { + // rc(App(x.clone(), rest.to_vec())) + // } + // _ => return rc(App(f, args)), + // } + // } _ => return rc(App(f, args)), }; // Put the remaining arguments back and eval again. In most cases diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 387327a..62dda08 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,5 +1,4 @@ #![allow(non_snake_case)] -use std::collections::BTreeMap; use std::collections::HashSet; use std::fmt; use std::rc::Rc; diff --git a/dhall/tests/normalization.rs b/dhall/tests/normalization.rs index c1ea81d..9f3c547 100644 --- a/dhall/tests/normalization.rs +++ b/dhall/tests/normalization.rs @@ -65,14 +65,14 @@ norm!(spec_normalization_success_prelude_List_filter_1, "prelude/List/filter/1") norm!(spec_normalization_success_prelude_List_fold_0, "prelude/List/fold/0"); norm!(spec_normalization_success_prelude_List_fold_1, "prelude/List/fold/1"); norm!(spec_normalization_success_prelude_List_fold_2, "prelude/List/fold/2"); -// norm!(spec_normalization_success_prelude_List_generate_0, "prelude/List/generate/0"); -// norm!(spec_normalization_success_prelude_List_generate_1, "prelude/List/generate/1"); +norm!(spec_normalization_success_prelude_List_generate_0, "prelude/List/generate/0"); +norm!(spec_normalization_success_prelude_List_generate_1, "prelude/List/generate/1"); norm!(spec_normalization_success_prelude_List_head_0, "prelude/List/head/0"); norm!(spec_normalization_success_prelude_List_head_1, "prelude/List/head/1"); -// norm!(spec_normalization_success_prelude_List_indexed_0, "prelude/List/indexed/0"); -// norm!(spec_normalization_success_prelude_List_indexed_1, "prelude/List/indexed/1"); -// norm!(spec_normalization_success_prelude_List_iterate_0, "prelude/List/iterate/0"); -// norm!(spec_normalization_success_prelude_List_iterate_1, "prelude/List/iterate/1"); +norm!(spec_normalization_success_prelude_List_indexed_0, "prelude/List/indexed/0"); +norm!(spec_normalization_success_prelude_List_indexed_1, "prelude/List/indexed/1"); +norm!(spec_normalization_success_prelude_List_iterate_0, "prelude/List/iterate/0"); +norm!(spec_normalization_success_prelude_List_iterate_1, "prelude/List/iterate/1"); norm!(spec_normalization_success_prelude_List_last_0, "prelude/List/last/0"); norm!(spec_normalization_success_prelude_List_last_1, "prelude/List/last/1"); norm!(spec_normalization_success_prelude_List_length_0, "prelude/List/length/0"); @@ -81,23 +81,23 @@ norm!(spec_normalization_success_prelude_List_map_0, "prelude/List/map/0"); norm!(spec_normalization_success_prelude_List_map_1, "prelude/List/map/1"); norm!(spec_normalization_success_prelude_List_null_0, "prelude/List/null/0"); norm!(spec_normalization_success_prelude_List_null_1, "prelude/List/null/1"); -// norm!(spec_normalization_success_prelude_List_replicate_0, "prelude/List/replicate/0"); -// norm!(spec_normalization_success_prelude_List_replicate_1, "prelude/List/replicate/1"); +norm!(spec_normalization_success_prelude_List_replicate_0, "prelude/List/replicate/0"); +norm!(spec_normalization_success_prelude_List_replicate_1, "prelude/List/replicate/1"); norm!(spec_normalization_success_prelude_List_reverse_0, "prelude/List/reverse/0"); norm!(spec_normalization_success_prelude_List_reverse_1, "prelude/List/reverse/1"); norm!(spec_normalization_success_prelude_List_shifted_0, "prelude/List/shifted/0"); norm!(spec_normalization_success_prelude_List_shifted_1, "prelude/List/shifted/1"); norm!(spec_normalization_success_prelude_List_unzip_0, "prelude/List/unzip/0"); norm!(spec_normalization_success_prelude_List_unzip_1, "prelude/List/unzip/1"); -// norm!(spec_normalization_success_prelude_Natural_build_0, "prelude/Natural/build/0"); -// norm!(spec_normalization_success_prelude_Natural_build_1, "prelude/Natural/build/1"); -// norm!(spec_normalization_success_prelude_Natural_enumerate_0, "prelude/Natural/enumerate/0"); -// norm!(spec_normalization_success_prelude_Natural_enumerate_1, "prelude/Natural/enumerate/1"); +norm!(spec_normalization_success_prelude_Natural_build_0, "prelude/Natural/build/0"); +norm!(spec_normalization_success_prelude_Natural_build_1, "prelude/Natural/build/1"); +norm!(spec_normalization_success_prelude_Natural_enumerate_0, "prelude/Natural/enumerate/0"); +norm!(spec_normalization_success_prelude_Natural_enumerate_1, "prelude/Natural/enumerate/1"); norm!(spec_normalization_success_prelude_Natural_even_0, "prelude/Natural/even/0"); norm!(spec_normalization_success_prelude_Natural_even_1, "prelude/Natural/even/1"); -// norm!(spec_normalization_success_prelude_Natural_fold_0, "prelude/Natural/fold/0"); -// norm!(spec_normalization_success_prelude_Natural_fold_1, "prelude/Natural/fold/1"); -// norm!(spec_normalization_success_prelude_Natural_fold_2, "prelude/Natural/fold/2"); +norm!(spec_normalization_success_prelude_Natural_fold_0, "prelude/Natural/fold/0"); +norm!(spec_normalization_success_prelude_Natural_fold_1, "prelude/Natural/fold/1"); +norm!(spec_normalization_success_prelude_Natural_fold_2, "prelude/Natural/fold/2"); norm!(spec_normalization_success_prelude_Natural_isZero_0, "prelude/Natural/isZero/0"); norm!(spec_normalization_success_prelude_Natural_isZero_1, "prelude/Natural/isZero/1"); norm!(spec_normalization_success_prelude_Natural_odd_0, "prelude/Natural/odd/0"); @@ -161,7 +161,7 @@ norm!(spec_normalization_success_prelude_Text_concatMap_1, "prelude/Text/concatM // norm!(spec_normalization_success_simple_letlet, "simple/letlet"); norm!(spec_normalization_success_simple_listBuild, "simple/listBuild"); norm!(spec_normalization_success_simple_multiLine, "simple/multiLine"); -// norm!(spec_normalization_success_simple_naturalBuild, "simple/naturalBuild"); +norm!(spec_normalization_success_simple_naturalBuild, "simple/naturalBuild"); norm!(spec_normalization_success_simple_naturalPlus, "simple/naturalPlus"); norm!(spec_normalization_success_simple_naturalShow, "simple/naturalShow"); norm!(spec_normalization_success_simple_naturalToInteger, "simple/naturalToInteger"); @@ -215,8 +215,8 @@ norm!(spec_normalization_success_unit_ListHead, "unit/ListHead"); norm!(spec_normalization_success_unit_ListHeadEmpty, "unit/ListHeadEmpty"); norm!(spec_normalization_success_unit_ListHeadOne, "unit/ListHeadOne"); norm!(spec_normalization_success_unit_ListIndexed, "unit/ListIndexed"); -// norm!(spec_normalization_success_unit_ListIndexedEmpty, "unit/ListIndexedEmpty"); -// norm!(spec_normalization_success_unit_ListIndexedOne, "unit/ListIndexedOne"); +norm!(spec_normalization_success_unit_ListIndexedEmpty, "unit/ListIndexedEmpty"); +norm!(spec_normalization_success_unit_ListIndexedOne, "unit/ListIndexedOne"); norm!(spec_normalization_success_unit_ListLast, "unit/ListLast"); norm!(spec_normalization_success_unit_ListLastEmpty, "unit/ListLastEmpty"); norm!(spec_normalization_success_unit_ListLastOne, "unit/ListLastOne"); @@ -235,13 +235,13 @@ norm!(spec_normalization_success_unit_MergeWithTypeNormalizeArguments, "unit/Mer norm!(spec_normalization_success_unit_Natural, "unit/Natural"); norm!(spec_normalization_success_unit_NaturalBuild, "unit/NaturalBuild"); norm!(spec_normalization_success_unit_NaturalBuildFoldFusion, "unit/NaturalBuildFoldFusion"); -// norm!(spec_normalization_success_unit_NaturalBuildImplementation, "unit/NaturalBuildImplementation"); +norm!(spec_normalization_success_unit_NaturalBuildImplementation, "unit/NaturalBuildImplementation"); norm!(spec_normalization_success_unit_NaturalEven, "unit/NaturalEven"); norm!(spec_normalization_success_unit_NaturalEvenOne, "unit/NaturalEvenOne"); norm!(spec_normalization_success_unit_NaturalEvenZero, "unit/NaturalEvenZero"); norm!(spec_normalization_success_unit_NaturalFold, "unit/NaturalFold"); -// norm!(spec_normalization_success_unit_NaturalFoldOne, "unit/NaturalFoldOne"); -// norm!(spec_normalization_success_unit_NaturalFoldZero, "unit/NaturalFoldZero"); +norm!(spec_normalization_success_unit_NaturalFoldOne, "unit/NaturalFoldOne"); +norm!(spec_normalization_success_unit_NaturalFoldZero, "unit/NaturalFoldZero"); norm!(spec_normalization_success_unit_NaturalIsZero, "unit/NaturalIsZero"); norm!(spec_normalization_success_unit_NaturalIsZeroOne, "unit/NaturalIsZeroOne"); norm!(spec_normalization_success_unit_NaturalIsZeroZero, "unit/NaturalIsZeroZero"); diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index 528f0ea..107144c 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -60,6 +60,9 @@ fn dhall_to_tokenstream( let b = dhall_to_tokenstream_bx(b, ctx); quote! { BinOp(#o, #a, #b) } } + NaturalLit(n) => { + quote! { NaturalLit(#n) } + } OptionalLit(t, e) => { let t = option_to_tokenstream(t, ctx); let e = option_to_tokenstream(e, ctx); @@ -77,6 +80,10 @@ fn dhall_to_tokenstream( let m = map_to_tokenstream(m, ctx); quote! { Record(#m) } } + RecordLit(m) => { + let m = map_to_tokenstream(m, ctx); + quote! { RecordLit(#m) } + } e => unimplemented!("{:?}", e), } } @@ -139,6 +146,7 @@ fn map_to_tokenstream( }) .unzip(); quote! { { + use std::collections::BTreeMap; let mut m = BTreeMap::new(); #( m.insert(#keys, #values); )* m -- cgit v1.2.3