summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs60
-rw-r--r--dhall/src/typecheck.rs1
-rw-r--r--dhall/tests/normalization.rs42
3 files changed, 65 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");
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 11:10:17 +0000