From 4c08c603946fa0ac483317d85a71dd1f709eec74 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 17 Mar 2019 22:02:10 +0100 Subject: Use Rc consistently everywhere --- dhall/src/normalize.rs | 408 ++++++++++++++++++++++++++++--------------------- 1 file changed, 235 insertions(+), 173 deletions(-) (limited to 'dhall/src/normalize.rs') diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 40112f1..fccc938 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -9,7 +9,7 @@ use std::rc::Rc; /// Is identical to normalize on primitive types, but not on more complex /// types like functions and records. /// This allows normalization to be lazy. -pub fn normalize_whnf(e: &Expr) -> Expr +pub fn normalize_whnf(e: &SubExpr) -> SubExpr where S: Clone + fmt::Debug, A: Clone + fmt::Debug, @@ -17,158 +17,204 @@ where use dhall_core::BinOp::*; use dhall_core::Builtin::*; use dhall_core::Expr::*; - match e { + rc(match e.as_ref() { Let(f, _, r, b) => { let vf0 = &V(f.clone(), 0); let r2 = shift::<_, S, _>(1, vf0, r); let b2 = subst::<_, S, _>(vf0, &r2, b); let b3 = shift::<_, S, _>(-1, vf0, &b2); - normalize_whnf(&b3) + return normalize_whnf(&b3); } - Annot(x, _) => normalize_whnf(x), - Note(_, e) => normalize_whnf(e), - App(f, args) => match (normalize_whnf(f), args.as_slice()) { - (f, []) => f, - (App(f, args1), args2) => normalize_whnf(&App( - f.clone(), - args1.iter().chain(args2.iter()).cloned().collect(), - )), - (Lam(ref x, _, ref b), [a, rest..]) => { - // Beta reduce - let vx0 = &V(x.clone(), 0); - let a2 = shift::(1, vx0, a); - let b2 = subst::(vx0, &a2, &b); - let b3 = shift::(-1, vx0, &b2); - normalize_whnf(&App(bx(b3), rest.to_vec())) - } - // TODO: this is more normalization than needed - (Builtin(b), args) => match ( - b, - args.iter() - .map(|x| normalize_whnf(&*x)) - .collect::>>() - .as_slice(), - ) { - (OptionalSome, [a]) => OptionalLit(None, Some(bx(a.clone()))), - (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), None), - (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0), - (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0), - (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0), - (NaturalToInteger, [NaturalLit(n)]) => IntegerLit(*n as isize), - (NaturalShow, [NaturalLit(n)]) => TextLit(n.to_string().into()), - (ListLength, [_, ListLit(_, ys)]) => NaturalLit(ys.len()), - (ListHead, [_, ListLit(t, ys)]) => { - OptionalLit(t.clone(), ys.iter().cloned().next()) - } - (ListLast, [_, ListLit(t, ys)]) => { - OptionalLit(t.clone(), ys.iter().cloned().last()) - } - (ListReverse, [_, ListLit(t, ys)]) => { - let xs = ys.iter().rev().cloned().collect(); - ListLit(t.clone(), xs) + Annot(x, _) => return normalize_whnf(x), + Note(_, e) => return normalize_whnf(e), + App(f, args) => { + let f = normalize_whnf(f); + match (f.as_ref(), args.as_slice()) { + (_, []) => return f, + (App(f, args1), args2) => { + return normalize_whnf(&rc(App( + f.clone(), + args1.iter().chain(args2.iter()).cloned().collect(), + ))) } - (ListBuild, [a0, g]) => { - // fold/build fusion - let g = match g { - App(f, args) => match (&**f, args.as_slice()) { - (Builtin(ListFold), [_, x, rest..]) => { - return normalize_whnf(&App( - x.clone(), - rest.to_vec(), - )) - } - (_, args) => App(f.clone(), args.to_vec()), - }, - g => g.clone(), - }; - let g = bx(g); - let a0 = bx(a0.clone()); - let a1 = bx(shift(1, &V("a".into(), 0), &a0)); - normalize_whnf( - &dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)), - ) + (Lam(ref x, _, ref b), [a, rest..]) => { + // Beta reduce + let vx0 = &V(x.clone(), 0); + let a2 = shift::(1, vx0, a); + let b2 = subst::(vx0, &a2, &b); + let b3 = shift::(-1, vx0, &b2); + return normalize_whnf(&rc(App(b3, rest.to_vec()))); } - (OptionalBuild, [a0, g]) => { - // fold/build fusion - let g = match g { - App(f, args) => match (&**f, args.as_slice()) { - (Builtin(OptionalFold), [_, x, rest..]) => { - return normalize_whnf(&App( - x.clone(), - rest.to_vec(), - )) + // TODO: this is more normalization than needed + (Builtin(b), args) => { + let args = args + .iter() + .map(|x| normalize_whnf(x)) + .collect::>>>(); + + match ( + b, + args.iter() + .map(Rc::as_ref) + .collect::>() + .as_slice(), + ) { + (OptionalSome, [_]) => { + OptionalLit(None, Some(Rc::clone(&args[0]))) + } + (OptionalNone, [_]) => { + OptionalLit(Some(Rc::clone(&args[0])), None) + } + (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0), + (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0), + (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0), + (NaturalToInteger, [NaturalLit(n)]) => { + IntegerLit(*n as isize) + } + (NaturalShow, [NaturalLit(n)]) => { + TextLit(n.to_string().into()) + } + (ListLength, [_, ListLit(_, ys)]) => { + NaturalLit(ys.len()) + } + (ListHead, [_, ListLit(t, ys)]) => { + OptionalLit(t.clone(), ys.iter().cloned().next()) + } + (ListLast, [_, ListLit(t, ys)]) => { + OptionalLit(t.clone(), ys.iter().cloned().last()) + } + (ListReverse, [_, ListLit(t, ys)]) => { + let xs = ys.iter().rev().cloned().collect(); + ListLit(t.clone(), xs) + } + (ListBuild, [_, _]) => { + // fold/build fusion + let g = Rc::clone(&args[1]); + let g = match g.as_ref() { + App(f, args) => { + match (f.as_ref(), args.as_slice()) { + (Builtin(ListFold), [_, x, rest..]) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => { + rc(App(f.clone(), args.to_vec())) + } + } + } + _ => g, + }; + let a0 = Rc::clone(&args[0]); + let a1 = shift(1, &V("a".into(), 0), &a0); + return normalize_whnf( + &dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)), + ); + } + (OptionalBuild, [_, _]) => { + // fold/build fusion + let g = Rc::clone(&args[1]); + let g = match g.as_ref() { + App(f, args) => { + match (f.as_ref(), args.as_slice()) { + ( + Builtin(OptionalFold), + [_, x, rest..], + ) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => { + rc(App(f.clone(), args.to_vec())) + } + } + } + _ => g, + }; + let a0 = Rc::clone(&args[0]); + return normalize_whnf( + &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)), + ); + } + (ListFold, [_, ListLit(_, xs), _, _, _]) => { + let e2: Rc> = xs.iter().rev().fold( + Rc::clone(&args[4]), + |acc, x| { + let x = x.clone(); + let acc = acc.clone(); + let cons = Rc::clone(&args[3]); + dhall_expr!(cons x acc) + }, + ); + return normalize_whnf(&e2); + } + // // fold/build fusion + // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { + // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) + // } + ( + OptionalFold, + [_, OptionalLit(_, Some(x)), _, _, _], + ) => { + let x = x.clone(); + let just = Rc::clone(&args[3]); + return normalize_whnf(&dhall_expr!(just x)); + } + ( + OptionalFold, + [_, OptionalLit(_, None), _, _, nothing], + ) => (*nothing).clone(), + // // fold/build fusion + // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { + // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) + // } + (NaturalBuild, [App(f, args)]) => { + match (f.as_ref(), args.as_slice()) { + // fold/build fusion + (Builtin(NaturalFold), [x, rest..]) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => app( + Builtin(NaturalBuild), + vec![bx(App(f.clone(), args.to_vec()))], + ), } - (_, args) => App(f.clone(), args.to_vec()), - }, - g => g.clone(), - }; - let g = bx(g); - let a0 = bx(a0.clone()); - normalize_whnf( - &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)), - ) - } - (ListFold, [_, ListLit(_, xs), _, cons, nil]) => { - let e2: Expr<_, _> = - xs.iter().rev().fold((*nil).clone(), |acc, x| { - let x = (x).clone(); - let acc = bx((acc).clone()); - let cons = bx((cons).clone()); - dhall_expr!(cons x acc) - }); - normalize_whnf(&e2) - } - // // fold/build fusion - // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => { - // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) - // } - (OptionalFold, [_, OptionalLit(_, Some(x)), _, just, _]) => { - let x = x.clone(); - let just = bx(just.clone()); - normalize_whnf(&dhall_expr!(just x)) - } - (OptionalFold, [_, OptionalLit(_, None), _, _, nothing]) => { - (*nothing).clone() - } - // // fold/build fusion - // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { - // normalize_whnf(&App(bx(x.clone()), rest.to_vec())) - // } - (NaturalBuild, [App(f, args)]) => { - match (&**f, args.as_slice()) { - // fold/build fusion - (Builtin(NaturalFold), [x, rest..]) => { - normalize_whnf(&App(x.clone(), rest.to_vec())) } - (_, args) => app( - Builtin(NaturalBuild), - vec![bx(App(f.clone(), args.to_vec()))], - ), - } - } - (NaturalFold, [App(f, args)]) => { - match (&**f, args.as_slice()) { - // fold/build fusion - (Builtin(NaturalBuild), [x, rest..]) => { - normalize_whnf(&App(x.clone(), rest.to_vec())) + (NaturalFold, [App(f, args)]) => { + match (f.as_ref(), args.as_slice()) { + // fold/build fusion + (Builtin(NaturalBuild), [x, rest..]) => { + return normalize_whnf(&rc(App( + x.clone(), + rest.to_vec(), + ))) + } + (_, args) => app( + Builtin(NaturalFold), + vec![bx(App(f.clone(), args.to_vec()))], + ), + } } - (_, args) => app( - Builtin(NaturalFold), - vec![bx(App(f.clone(), args.to_vec()))], - ), + (b, _) => App(rc(Builtin(*b)), args), } } - (b, args) => { - App(bx(Builtin(b)), args.iter().cloned().map(bx).collect()) - } - }, - (f, args) => App(bx(f), args.to_vec()), - }, - BoolIf(b, t, f) => match normalize_whnf(b) { - BoolLit(true) => normalize_whnf(t), - BoolLit(false) => normalize_whnf(f), - b2 => BoolIf(bx(b2), t.clone(), f.clone()), - }, + (_, args) => App(f, args.to_vec()), + } + } + BoolIf(b, t, f) => { + let b = normalize_whnf(b); + match b.as_ref() { + BoolLit(true) => return normalize_whnf(t), + BoolLit(false) => return normalize_whnf(f), + _ => BoolIf(b, t.clone(), f.clone()), + } + } OptionalLit(t, es) => { if !es.is_none() { OptionalLit(None, es.clone()) @@ -176,36 +222,52 @@ where 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), - (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y), - (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y), - (NaturalPlus, NaturalLit(x), NaturalLit(y)) => NaturalLit(x + y), - (NaturalTimes, NaturalLit(x), NaturalLit(y)) => NaturalLit(x * y), - (TextAppend, TextLit(x), TextLit(y)) => TextLit(x + y), - (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => { - // Drop type annotation if the result is nonempty - let t = if xs.is_empty() && ys.is_empty() { - t1.or(t2) - } else { - None - }; - let xs = xs.into_iter(); - let ys = ys.into_iter(); - ListLit(t, xs.chain(ys).collect()) + BinOp(o, x, y) => { + let x = normalize_whnf(x); + let y = normalize_whnf(y); + match (o, x.as_ref(), y.as_ref()) { + (BoolAnd, BoolLit(x), BoolLit(y)) => BoolLit(*x && *y), + (BoolOr, BoolLit(x), BoolLit(y)) => BoolLit(*x || *y), + (BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y), + (BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y), + (NaturalPlus, NaturalLit(x), NaturalLit(y)) => { + NaturalLit(x + y) + } + (NaturalTimes, NaturalLit(x), NaturalLit(y)) => { + NaturalLit(x * y) + } + // TODO: interpolation + (TextAppend, TextLit(x), TextLit(y)) => { + TextLit(x.clone() + y.clone()) + } + (ListAppend, ListLit(t1, xs), ListLit(t2, ys)) => { + let t1: Option> = t1.as_ref().map(Rc::clone); + let t2: Option> = t2.as_ref().map(Rc::clone); + // Drop type annotation if the result is nonempty + let t = if xs.is_empty() && ys.is_empty() { + t1.or(t2) + } else { + None + }; + let xs = xs.into_iter().cloned(); + let ys = ys.into_iter().cloned(); + ListLit(t, xs.chain(ys).collect()) + } + (o, _, _) => BinOp(*o, x, y), + } + } + Field(e, x) => { + let e = normalize_whnf(e); + match (e.as_ref(), x) { + (RecordLit(kvs), x) => match kvs.get(&x) { + Some(r) => return normalize_whnf(r), + None => Field(e, x.clone()), + }, + (_, x) => Field(e, x.clone()), } - (o, x, y) => BinOp(*o, bx(x), bx(y)), - }, - Field(e, x) => match (normalize_whnf(&e), x) { - (RecordLit(kvs), x) => match kvs.get(&x) { - Some(r) => normalize_whnf(r), - None => Field(bx(RecordLit(kvs)), x.clone()), - }, - (e, x) => Field(bx(e), x.clone()), - }, - e => e.clone(), - } + } + _ => return Rc::clone(e), + }) } /// Reduce an expression to its normal form, performing beta reduction @@ -217,16 +279,16 @@ where /// However, `normalize` will not fail if the expression is ill-typed and will /// leave ill-typed sub-expressions unevaluated. /// -pub fn normalize(e: &Expr) -> Expr +pub fn normalize(e: SubExpr) -> SubExpr where S: Clone + fmt::Debug, T: Clone + fmt::Debug, A: Clone + fmt::Debug, { - normalize_whnf(e).map_shallow( - normalize, + rc(normalize_whnf(&e).map_shallow_rc( + |x| normalize(Rc::clone(x)), |_| unreachable!(), |x| x.clone(), |x| x.clone(), - ) + )) } -- cgit v1.2.3