summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs317
1 files changed, 149 insertions, 168 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 90ba993..3c04b9e 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,6 +4,151 @@ use dhall_generator::dhall_expr;
use std::fmt;
use std::rc::Rc;
+fn apply_builtin<S, A>(b: Builtin, args: Vec<SubExpr<S, A>>) -> SubExpr<S, A>
+where
+ S: fmt::Debug,
+ A: fmt::Debug,
+{
+ use dhall_core::BinOp::*;
+ use dhall_core::Builtin::*;
+ use dhall_core::Expr::*;
+ let f = rc(Builtin(b));
+ // How many arguments for each builtin, and which argument
+ // is the important one for pattern-matching
+ let (len_consumption, arg_to_eval) = match b {
+ OptionalSome => (1, None),
+ OptionalNone => (1, None),
+ NaturalIsZero => (1, Some(0)),
+ NaturalEven => (1, Some(0)),
+ NaturalOdd => (1, Some(0)),
+ NaturalToInteger => (1, Some(0)),
+ NaturalShow => (1, Some(0)),
+ ListLength => (2, Some(1)),
+ ListHead => (2, Some(1)),
+ ListLast => (2, Some(1)),
+ ListReverse => (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)),
+ _ => (0, None),
+ };
+ let mut args = args.to_vec();
+ if len_consumption > args.len() {
+ return rc(App(f, args));
+ }
+ if let Some(i) = arg_to_eval {
+ args[i] = Rc::clone(&normalize_whnf(&args[i]));
+ }
+ let evaled_arg = arg_to_eval.map(|i| args[i].as_ref());
+
+ let ret = match (b, evaled_arg, args.as_slice()) {
+ (OptionalSome, _, [x, ..]) => rc(OptionalLit(None, Some(Rc::clone(x)))),
+ (OptionalNone, _, [t, ..]) => rc(OptionalLit(Some(Rc::clone(t)), None)),
+ (NaturalIsZero, Some(NaturalLit(n)), _) => rc(BoolLit(*n == 0)),
+ (NaturalEven, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 == 0)),
+ (NaturalOdd, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 != 0)),
+ (NaturalToInteger, Some(NaturalLit(n)), _) => {
+ rc(IntegerLit(*n as isize))
+ }
+ (NaturalShow, Some(NaturalLit(n)), _) => {
+ rc(TextLit(n.to_string().into()))
+ }
+ (ListLength, Some(ListLit(_, ys)), _) => rc(NaturalLit(ys.len())),
+ (ListHead, Some(ListLit(t, ys)), _) => {
+ rc(OptionalLit(t.clone(), ys.iter().cloned().next()))
+ }
+ (ListLast, Some(ListLit(t, ys)), _) => {
+ rc(OptionalLit(t.clone(), ys.iter().cloned().last()))
+ }
+ (ListReverse, Some(ListLit(t, ys)), _) => {
+ let xs = ys.iter().rev().cloned().collect();
+ rc(ListLit(t.clone(), xs))
+ }
+ (ListBuild, _, [a0, g, ..]) => {
+ loop {
+ if let App(f2, args2) = g.as_ref() {
+ if let (Builtin(ListFold), [_, x, rest..]) =
+ (f2.as_ref(), args2.as_slice())
+ {
+ // fold/build fusion
+ break rc(App(x.clone(), rest.to_vec()));
+ }
+ };
+ let a0 = Rc::clone(a0);
+ let a1 = shift(1, &V("a".into(), 0), &a0);
+ break dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0));
+ }
+ }
+ (OptionalBuild, _, [a0, g, ..]) => {
+ loop {
+ if let App(f2, args2) = g.as_ref() {
+ if let (Builtin(OptionalFold), [_, x, rest..]) =
+ (f2.as_ref(), args2.as_slice())
+ {
+ // fold/build fusion
+ break rc(App(x.clone(), rest.to_vec()));
+ }
+ };
+ let a0 = Rc::clone(a0);
+ break dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0));
+ }
+ }
+ (ListFold, Some(ListLit(_, xs)), [_, _, _, cons, nil, ..]) => {
+ xs.iter().rev().fold(Rc::clone(nil), |acc, x| {
+ let x = x.clone();
+ let acc = acc.clone();
+ let cons = Rc::clone(cons);
+ dhall_expr!(cons x acc)
+ })
+ }
+ // // fold/build fusion
+ // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // }
+ (
+ OptionalFold,
+ Some(OptionalLit(_, Some(x))),
+ [_, _, _, just, _, ..],
+ ) => {
+ let x = x.clone();
+ let just = Rc::clone(just);
+ dhall_expr!(just x)
+ }
+ (
+ OptionalFold,
+ Some(OptionalLit(_, None)),
+ [_, _, _, _, nothing, ..],
+ ) => Rc::clone(nothing),
+ // // fold/build fusion
+ // (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)),
+ }
+ }
+ (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)),
+ };
+ normalize_whnf(&rc(Expr::App(ret, args.split_off(len_consumption))))
+}
+
/// Reduce an expression to its weak head normal form, i.e. normalize
/// just enough to get the first constructor of the final expression
/// Is identical to normalize on primitive types, but not on more complex
@@ -15,7 +160,6 @@ where
A: fmt::Debug,
{
use dhall_core::BinOp::*;
- use dhall_core::Builtin::*;
use dhall_core::Expr::*;
match e.as_ref() {
Let(f, _, r, b) => {
@@ -43,172 +187,8 @@ where
let b3 = shift(-1, vx0, &b2);
normalize_whnf(&rc(App(b3, rest.to_vec())))
}
- (Builtin(b), _) => {
- // How many arguments for each builtin, and which argument
- // is the important one for pattern-matching
- let (len_consumption, arg_to_eval) = match b {
- OptionalSome => (1, None),
- OptionalNone => (1, None),
- NaturalIsZero => (1, Some(0)),
- NaturalEven => (1, Some(0)),
- NaturalOdd => (1, Some(0)),
- NaturalToInteger => (1, Some(0)),
- NaturalShow => (1, Some(0)),
- ListLength => (2, Some(1)),
- ListHead => (2, Some(1)),
- ListLast => (2, Some(1)),
- ListReverse => (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)),
- _ => (0, None),
- };
- let mut args = args.to_vec();
- if len_consumption > args.len() {
- return rc(App(f, args));
- }
- if let Some(i) = arg_to_eval {
- args[i] = Rc::clone(&normalize_whnf(&args[i]));
- }
- let evaled_arg = arg_to_eval.map(|i| args[i].as_ref());
-
- let ret = match (b, evaled_arg, args.as_slice()) {
- (OptionalSome, _, [x, ..]) => {
- rc(OptionalLit(None, Some(Rc::clone(x))))
- }
- (OptionalNone, _, [t, ..]) => {
- rc(OptionalLit(Some(Rc::clone(t)), None))
- }
- (NaturalIsZero, Some(NaturalLit(n)), _) => {
- rc(BoolLit(*n == 0))
- }
- (NaturalEven, Some(NaturalLit(n)), _) => {
- rc(BoolLit(*n % 2 == 0))
- }
- (NaturalOdd, Some(NaturalLit(n)), _) => {
- rc(BoolLit(*n % 2 != 0))
- }
- (NaturalToInteger, Some(NaturalLit(n)), _) => {
- rc(IntegerLit(*n as isize))
- }
- (NaturalShow, Some(NaturalLit(n)), _) => {
- rc(TextLit(n.to_string().into()))
- }
- (ListLength, Some(ListLit(_, ys)), _) => {
- rc(NaturalLit(ys.len()))
- }
- (ListHead, Some(ListLit(t, ys)), _) => rc(OptionalLit(
- t.clone(),
- ys.iter().cloned().next(),
- )),
- (ListLast, Some(ListLit(t, ys)), _) => rc(OptionalLit(
- t.clone(),
- ys.iter().cloned().last(),
- )),
- (ListReverse, Some(ListLit(t, ys)), _) => {
- let xs = ys.iter().rev().cloned().collect();
- rc(ListLit(t.clone(), xs))
- }
- (ListBuild, _, [a0, g, ..]) => {
- loop {
- if let App(f2, args2) = g.as_ref() {
- if let (
- Builtin(ListFold),
- [_, x, rest..],
- ) = (f2.as_ref(), args2.as_slice())
- {
- // fold/build fusion
- break rc(App(
- x.clone(),
- rest.to_vec(),
- ));
- }
- };
- let a0 = Rc::clone(a0);
- let a1 = shift(1, &V("a".into(), 0), &a0);
- break dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0));
- }
- }
- (OptionalBuild, _, [a0, g, ..]) => {
- loop {
- if let App(f2, args2) = g.as_ref() {
- if let (
- Builtin(OptionalFold),
- [_, x, rest..],
- ) = (f2.as_ref(), args2.as_slice())
- {
- // fold/build fusion
- break rc(App(
- x.clone(),
- rest.to_vec(),
- ));
- }
- };
- let a0 = Rc::clone(a0);
- break dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0));
- }
- }
- (
- ListFold,
- Some(ListLit(_, xs)),
- [_, _, _, cons, nil, ..],
- ) => xs.iter().rev().fold(Rc::clone(nil), |acc, x| {
- let x = x.clone();
- let acc = acc.clone();
- let cons = Rc::clone(cons);
- dhall_expr!(cons x acc)
- }),
- // // fold/build fusion
- // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
- // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
- // }
- (
- OptionalFold,
- Some(OptionalLit(_, Some(x))),
- [_, _, _, just, _, ..],
- ) => {
- let x = x.clone();
- let just = Rc::clone(just);
- dhall_expr!(just x)
- }
- (
- OptionalFold,
- Some(OptionalLit(_, None)),
- [_, _, _, _, nothing, ..],
- ) => Rc::clone(nothing),
- // // fold/build fusion
- // (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)),
- }
- }
- (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)),
- }
- }
- (b, _, _) => return rc(App(rc(Builtin(*b)), args)),
- };
- normalize_whnf(&rc(Expr::App(
- ret,
- args.split_off(len_consumption),
- )))
- }
- (_, args) => rc(App(f, args.to_vec())),
+ (Builtin(b), _) => apply_builtin(*b, args.to_vec()),
+ _ => rc(App(f, args.to_vec())),
}
}
BoolIf(b, t, f) => {
@@ -226,6 +206,8 @@ where
rc(OptionalLit(t.clone(), es.clone()))
}
}
+ // TODO: interpolation
+ // TextLit(t) =>
BinOp(o, x, y) => {
let x = normalize_whnf(x);
let y = normalize_whnf(y);
@@ -240,7 +222,6 @@ where
(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
NaturalLit(x * y)
}
- // TODO: interpolation
(TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y),
(ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => {
let t1: Option<Rc<_>> = t1.as_ref().map(Rc::clone);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 19:53:28 +0000