From 2e02360dc12b55f3811ba58bb17c21514990134c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 6 Mar 2019 12:25:05 +0100 Subject: Split-off normalization into its own crate --- dhall_normalize/Cargo.toml | 14 ++ dhall_normalize/src/lib.rs | 5 + dhall_normalize/src/normalize.rs | 286 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 305 insertions(+) create mode 100644 dhall_normalize/Cargo.toml create mode 100644 dhall_normalize/src/lib.rs create mode 100644 dhall_normalize/src/normalize.rs (limited to 'dhall_normalize') diff --git a/dhall_normalize/Cargo.toml b/dhall_normalize/Cargo.toml new file mode 100644 index 0000000..65524ed --- /dev/null +++ b/dhall_normalize/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "dhall_normalize" +version = "0.1.0" +authors = ["NanoTech ", "Nadrieril "] +edition = "2018" + +[dependencies] +bytecount = "0.5.1" +itertools = "0.8.0" +lalrpop-util = "0.16.3" +nom = "3.0.0" +term-painter = "0.2.3" +pest = { git = "https://github.com/pest-parser/pest" } +dhall_core = { path = "../dhall_core" } diff --git a/dhall_normalize/src/lib.rs b/dhall_normalize/src/lib.rs new file mode 100644 index 0000000..a2f7041 --- /dev/null +++ b/dhall_normalize/src/lib.rs @@ -0,0 +1,5 @@ +#![feature(box_patterns)] +#![feature(trace_macros)] + +mod normalize; +pub use crate::normalize::*; diff --git a/dhall_normalize/src/normalize.rs b/dhall_normalize/src/normalize.rs new file mode 100644 index 0000000..1fa5524 --- /dev/null +++ b/dhall_normalize/src/normalize.rs @@ -0,0 +1,286 @@ +#![allow(non_snake_case)] +use std::fmt; +use dhall_core::core::*; + +/// Reduce an expression to its normal form, performing beta reduction +/// +/// `normalize` does not type-check the expression. You may want to type-check +/// expressions before normalizing them since normalization can convert an +/// ill-typed expression into a well-typed expression. +/// +/// However, `normalize` will not fail if the expression is ill-typed and will +/// leave ill-typed sub-expressions unevaluated. +/// +pub fn normalize<'i, S, T, A>(e: &Expr<'i, S, A>) -> Expr<'i, T, A> +where + S: Clone + fmt::Debug, + T: Clone + fmt::Debug, + A: Clone + fmt::Debug, +{ + use dhall_core::BinOp::*; + 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) + } + App(ref f, ref a) => match normalize::(f) { + Lam(x, _A, b) => { + // Beta reduce + let vx0 = V(x, 0); + let a2 = shift::(1, vx0, a); + let b2 = subst::(vx0, &a2, &b); + let b3 = shift::(-1, vx0, &b2); + normalize(&b3) + } + f2 => match (f2, normalize::(a)) { + // fold/build fusion for `List` + (App(box Builtin(ListBuild), _), App(box App(box Builtin(ListFold), _), box e2)) | + (App(box Builtin(ListFold), _), App(box App(box Builtin(ListBuild), _), box e2)) | + + // fold/build fusion for `Natural` + (Builtin(NaturalBuild), App(box Builtin(NaturalFold), box e2)) | + (Builtin(NaturalFold), App(box Builtin(NaturalBuild), box e2)) => normalize(&e2), + + /* + App (App (App (App NaturalFold (NaturalLit n0)) _) succ') zero -> + normalize (go n0) + where + go !0 = zero + go !n = App succ' (go (n - 1)) + App NaturalBuild k + | check -> NaturalLit n + | otherwise -> App f' a' + where + labeled = + normalize (App (App (App k Natural) "Succ") "Zero") + + n = go 0 labeled + where + go !m (App (Var "Succ") e') = go (m + 1) e' + go !m (Var "Zero") = m + go !_ _ = internalError text + check = go labeled + where + go (App (Var "Succ") e') = go e' + go (Var "Zero") = True + go _ = False + */ + (Builtin(NaturalIsZero), NaturalLit(n)) => BoolLit(n == 0), + (Builtin(NaturalEven), NaturalLit(n)) => BoolLit(n % 2 == 0), + (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0), + (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize), + (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()), + (App(f@box Builtin(ListBuild), box t), k) => { + let labeled = + normalize::<_, T, _>(&app(app(app(k.clone(), app( + Builtin(self::Builtin::List), t.clone())), "Cons"), "Nil")); + + fn list_to_vector<'i, S, A>(v: &mut Vec>, e: Expr<'i, S, A>) + where S: Clone, A: Clone + { + match e { + App(box App(box Var(V("Cons", _)), box x), box e2) => { + v.push(x); + list_to_vector(v, e2) + } + Var(V("Nil", _)) => {} + _ => panic!("internalError list_to_vector"), + } + } + fn check(e: &Expr) -> bool { + match *e { + App(box App(box Var(V("Cons", _)), _), ref e2) => check(e2), + Var(V("Nil", _)) => true, + _ => false, + } + } + + if check(&labeled) { + let mut v = vec![]; + list_to_vector(&mut v, labeled); + ListLit(Some(bx(t)), v) + } else { + app(App(f, bx(t)), k) + } + } + (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => { + let e2: Expr<_, _> = xs.into_iter().rev().fold(nil, |y, ys| // foldr + App(bx(App(cons.clone(), bx(y))), bx(ys)) + ); + normalize(&e2) + } + (App(f, x_), ListLit(t, ys)) => match *f { + Builtin(ListLength) => + NaturalLit(ys.len()), + Builtin(ListHead) => + normalize(&OptionalLit(t, ys.into_iter().take(1).collect())), + Builtin(ListLast) => + normalize(&OptionalLit(t, ys.into_iter().last().into_iter().collect())), + Builtin(ListReverse) => { + let mut xs = ys; + xs.reverse(); + normalize(&ListLit(t, xs)) + } + _ => app(App(f, x_), ListLit(t, ys)), + }, + /* + App (App ListIndexed _) (ListLit t xs) -> + normalize (ListLit t' (fmap adapt (Data.Vector.indexed xs))) + where + t' = Record (Data.Map.fromList kts) + where + kts = [ ("index", Natural) + , ("value", t) + ] + adapt (n, x) = RecordLit (Data.Map.fromList kvs) + where + kvs = [ ("index", NaturalLit (fromIntegral n)) + , ("value", x) + ] + */ + (App(box App(box App(box App(box Builtin(OptionalFold), _), box OptionalLit(_, xs)), _), just), nothing) => { + let e2: Expr<_, _> = xs.into_iter().fold(nothing, |y, _| + App(just.clone(), bx(y)) + ); + normalize(&e2) + } + (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), b)) => { + normalize(&b) + } + (App(box Builtin(OptionalBuild), a0), g) => { + let e2: Expr<_, _> = app(app(app(g, + App(bx(Builtin(Optional)), a0.clone())), + Lam("x", a0.clone(), + bx(OptionalLit(Some(a0.clone()), vec![Var(V("x", 0))])))), + OptionalLit(Some(a0), vec![])); + normalize(&e2) + } + (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), + ), + 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) + } + }, + r2 => Field(bx(r2), x), + }, + Note(_, ref e) => normalize(e), + Embed(ref a) => Embed(a.clone()), + _ => unimplemented!(), + } +} + +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, + 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)) + } +} -- cgit v1.2.3