diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/normalize.rs | 60 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 1 |
2 files changed, 44 insertions, 17 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; |