diff options
author | Nadrieril | 2019-03-06 20:25:13 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-06 20:25:13 +0100 |
commit | 479b2cfcd650c4f1ad6c1044528d31874aca890b (patch) | |
tree | f20f5bdfeb57867e427945ae9f3f2c88000a7fbc | |
parent | 0184b60dc6bbe7384f5fce24da848bcd1fc65fb3 (diff) |
Considerably remove clutter in normalize
-rw-r--r-- | dhall_core/src/core.rs | 71 | ||||
-rw-r--r-- | dhall_normalize/src/normalize.rs | 178 |
2 files changed, 107 insertions, 142 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index 6795c2c..675345e 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -231,6 +231,17 @@ impl<'i, S, A> From<Builtin> for Expr<'i, S, A> { } impl<'i, S, A> Expr<'i, S, A> { + pub fn map_shallow<T, F1, F2>(&self, map_expr: F1, map_note: F2) -> Expr<'i, T, A> + where + A: Clone, + T: Clone, + S: Clone, + F1: Fn(&Self) -> Expr<'i, T, A>, + F2: FnOnce(&S) -> T, + { + map_shallow(self, map_expr, map_note) + } + pub fn bool_lit(&self) -> Option<bool> { match *self { Expr::BoolLit(v) => Some(v), @@ -628,16 +639,71 @@ fn add_ui(u: usize, i: isize) -> usize { } } -pub fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U> +pub fn map_shallow<'i, S, T, A, F1, F2>(e: &Expr<'i, S, A>, map: F1, map_note: F2) -> Expr<'i, T, A> +where + A: Clone, + S: Clone, + T: Clone, + F1: Fn(&Expr<'i, S, A>) -> Expr<'i, T, A>, + F2: FnOnce(&S) -> T, +{ + use crate::Expr::*; + let bxmap = |x: &Expr<'i, S, A>| -> Box<Expr<'i, T, A>> { bx(map(x)) }; + let opt = |x| map_opt_box(x, &map); + match *e { + Const(k) => Const(k), + Var(v) => Var(v), + Lam(x, ref t, ref b) => Lam(x, bxmap(t), bxmap(b)), + Pi(x, ref t, ref b) => Pi(x, bxmap(t), bxmap(b)), + App(ref f, ref a) => App(bxmap(f), bxmap(a)), + Let(l, ref t, ref a, ref b) => Let(l, opt(t), bxmap(a), bxmap(b)), + Annot(ref x, ref t) => Annot(bxmap(x), bxmap(t)), + Builtin(v) => Builtin(v), + BoolLit(b) => BoolLit(b), + BoolIf(ref b, ref t, ref f) => BoolIf(bxmap(b), bxmap(t), bxmap(f)), + NaturalLit(n) => NaturalLit(n), + IntegerLit(n) => IntegerLit(n), + DoubleLit(n) => DoubleLit(n), + TextLit(ref t) => TextLit(t.clone()), + BinOp(o, ref x, ref y) => BinOp(o, bxmap(x), bxmap(y)), + ListLit(ref t, ref es) => { + let es = es.iter().map(&map).collect(); + ListLit(opt(t), es) + } + OptionalLit(ref t, ref es) => { + let es = es.iter().map(&map).collect(); + OptionalLit(opt(t), es) + } + Record(ref kts) => Record(map_record_value(kts, map)), + RecordLit(ref kvs) => RecordLit(map_record_value(kvs, map)), + Union(ref kts) => Union(map_record_value(kts, map)), + UnionLit(k, ref v, ref kvs) => { + UnionLit(k, bxmap(v), map_record_value(kvs, map)) + } + Merge(ref x, ref y, ref t) => Merge(bxmap(x), bxmap(y), opt(t)), + Field(ref r, x) => Field(bxmap(r), x), + Note(ref n, ref e) => Note(map_note(n), bxmap(e)), + Embed(ref a) => Embed(a.clone()), + } +} + +pub fn map_record_value<'a, I, K, V, U, F>(it: I, mut f: F) -> BTreeMap<K, U> where I: IntoIterator<Item = (&'a K, &'a V)>, K: Eq + Ord + Copy + 'a, V: 'a, - F: Fn(&V) -> U, + F: FnMut(&V) -> U, { it.into_iter().map(|(&k, v)| (k, f(v))).collect() } +pub fn map_opt_box<T, U, F>(x: &Option<Box<T>>, f: F) -> Option<Box<U>> +where + F: FnOnce(&T) -> U, +{ + x.as_ref().map(|x| x.as_ref()).map(f).map(bx) +} + fn map_op2<T, U, V, F, G>(f: F, g: G, a: T, b: T) -> V where F: FnOnce(U, U) -> V, @@ -916,4 +982,3 @@ where { map_op2(f, |x| bx(subst(v, e, x)), a, b) } - diff --git a/dhall_normalize/src/normalize.rs b/dhall_normalize/src/normalize.rs index 2068ae3..0e46ee0 100644 --- a/dhall_normalize/src/normalize.rs +++ b/dhall_normalize/src/normalize.rs @@ -1,7 +1,7 @@ #![allow(non_snake_case)] -use std::fmt; use dhall_core::core::*; use dhall_generator::dhall; +use std::fmt; /// Reduce an expression to its normal form, performing beta reduction /// @@ -22,18 +22,20 @@ where use dhall_core::Builtin::*; use dhall_core::Expr::*; match *e { - Const(k) => Const(k), - Var(v) => Var(v), - Lam(x, ref tA, ref b) => { - let tA2 = normalize(tA); - let b2 = normalize(b); - Lam(x, bx(tA2), bx(b2)) - } - Pi(x, ref tA, ref tB) => { - let tA2 = normalize(tA); - let tB2 = normalize(tB); - pi(x, tA2, tB2) + // Matches that don't normalize everything right away + Let(f, _, ref r, ref b) => { + let r2 = shift::<_, S, _>(1, V(f, 0), r); + let b2 = subst(V(f, 0), &r2, b); + let b3 = shift::<_, T, _>(-1, V(f, 0), &b2); + normalize(&b3) } + BoolIf(ref b, ref t, ref f) => match normalize(b) { + BoolLit(true) => normalize(t), + BoolLit(false) => normalize(f), + b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))), + }, + Annot(ref x, _) => normalize(x), + Note(_, ref e) => normalize(e), App(ref f, ref a) => match normalize::<S, T, A>(f) { Lam(x, _A, b) => { // Beta reduce @@ -144,135 +146,33 @@ where (f2, a2) => app(f2, a2), }, }, - Let(f, _, ref r, ref b) => { - let r2 = shift::<_, S, _>(1, V(f, 0), r); - let b2 = subst(V(f, 0), &r2, b); - let b3 = shift::<_, T, _>(-1, V(f, 0), &b2); - normalize(&b3) - } - Annot(ref x, _) => normalize(x), - Builtin(v) => Builtin(v), - BoolLit(b) => BoolLit(b), - BinOp(BoolAnd, ref x, ref y) => with_binop( - BoolAnd, - Expr::bool_lit, - |xn, yn| BoolLit(xn && yn), - normalize(x), - normalize(y), - ), - BinOp(BoolOr, ref x, ref y) => with_binop( - BoolOr, - Expr::bool_lit, - |xn, yn| BoolLit(xn || yn), - normalize(x), - normalize(y), - ), - BinOp(BoolEQ, ref x, ref y) => with_binop( - BoolEQ, - Expr::bool_lit, - |xn, yn| BoolLit(xn == yn), - normalize(x), - normalize(y), - ), - BinOp(BoolNE, ref x, ref y) => with_binop( - BoolNE, - Expr::bool_lit, - |xn, yn| BoolLit(xn != yn), - normalize(x), - normalize(y), - ), - BoolIf(ref b, ref t, ref f) => match normalize(b) { - BoolLit(true) => normalize(t), - BoolLit(false) => normalize(f), - b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))), - }, - NaturalLit(n) => NaturalLit(n), - BinOp(NaturalPlus, ref x, ref y) => with_binop( - NaturalPlus, - Expr::natural_lit, - |xn, yn| NaturalLit(xn + yn), - normalize(x), - normalize(y), - ), - BinOp(NaturalTimes, ref x, ref y) => with_binop( - NaturalTimes, - Expr::natural_lit, - |xn, yn| NaturalLit(xn * yn), - normalize(x), - normalize(y), - ), - IntegerLit(n) => IntegerLit(n), - DoubleLit(n) => DoubleLit(n), - TextLit(ref t) => TextLit(t.clone()), - BinOp(TextAppend, ref x, ref y) => with_binop( - TextAppend, - Expr::text_lit, - |xt, yt| TextLit(xt + &yt), - normalize(x), - normalize(y), - ), - BinOp(ListAppend, ref x, ref y) => { - match (normalize(x), normalize(y)) { - (ListLit(t1, xs), ListLit(t2, ys)) => { - // Drop type annotation if the result is not empty - let t = if xs.len() == 0 && ys.len() == 0 { - t1.or(t2) - } else { - None - }; - let xs = xs.into_iter(); - let ys = ys.into_iter(); - ListLit(t, xs.chain(ys).collect()) - } - (x, y) => BinOp(ListAppend, bx(x), bx(y)), + + // Normalize everything else before matching + ref e => match e.map_shallow(normalize, |_| unreachable!()) { + BinOp(BoolAnd, box BoolLit(x), box BoolLit(y)) => BoolLit(x && y), + BinOp(BoolOr, box BoolLit(x), box BoolLit(y)) => BoolLit(x || y), + BinOp(BoolEQ, box BoolLit(x), box BoolLit(y)) => BoolLit(x == y), + BinOp(BoolNE, box BoolLit(x), box BoolLit(y)) => BoolLit(x != y), + BinOp(NaturalPlus, box NaturalLit(x), box NaturalLit(y)) => NaturalLit(x + y), + BinOp(NaturalTimes, box NaturalLit(x), box NaturalLit(y)) => NaturalLit(x * y), + BinOp(TextAppend, box TextLit(x), box TextLit(y)) => TextLit(x + &y), + BinOp(ListAppend, box ListLit(t1, xs), box ListLit(t2, ys)) => { + // Drop type annotation if the result is nonempty + let t = if xs.len() == 0 && ys.len() == 0 { + t1.or(t2) + } else { + None + }; + let xs = xs.into_iter(); + let ys = ys.into_iter(); + ListLit(t, xs.chain(ys).collect()) } - }, - ListLit(ref t, ref es) => { - let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx); - let es2 = es.iter().map(normalize).collect(); - ListLit(t2, es2) - } - OptionalLit(ref t, ref es) => { - let t2 = t.as_ref().map(|x| x.as_ref()).map(normalize).map(bx); - let es2 = es.iter().map(normalize).collect(); - OptionalLit(t2, es2) - } - Record(ref kts) => Record(map_record_value(kts, normalize)), - RecordLit(ref kvs) => RecordLit(map_record_value(kvs, normalize)), - Union(ref kts) => Union(map_record_value(kts, normalize)), - UnionLit(k, ref v, ref kvs) => { - UnionLit(k, bx(normalize(v)), map_record_value(kvs, normalize)) - } - Merge(ref _x, ref _y, ref _t) => unimplemented!(), - Field(ref r, x) => match normalize(r) { - RecordLit(kvs) => match kvs.get(x) { - Some(r2) => normalize(r2), - None => { - Field(bx(RecordLit(map_record_value(&kvs, normalize))), x) - } + Merge(_x, _y, _t) => unimplemented!(), + Field(box RecordLit(kvs), x) => match kvs.get(x) { + Some(r) => r.clone(), + None => Field(bx(RecordLit(kvs)), x), }, - r2 => Field(bx(r2), x), + e => e, }, - Note(_, ref e) => normalize(e), - Embed(ref a) => Embed(a.clone()), - ref e => unimplemented!("{:?}", e), - } -} - -fn with_binop<'a, S, A, U, Get, Set>( - op: BinOp, - get: Get, - set: Set, - x: Expr<'a, S, A>, - y: Expr<'a, S, A>, -) -> Expr<'a, S, A> -where - Get: Fn(&Expr<'a, S, A>) -> Option<U>, - Set: FnOnce(U, U) -> Expr<'a, S, A>, -{ - if let (Some(xv), Some(yv)) = (get(&x), get(&y)) { - set(xv, yv) - } else { - Expr::BinOp(op, bx(x), bx(y)) } } |