From f055754381d17d987664a5df3d3507c610d0f7cd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 6 Mar 2019 21:32:20 +0100 Subject: Merge dhall_normalize back into dhall; that was unnecessary --- Cargo.lock | 16 +--- dhall/Cargo.toml | 2 +- dhall/src/lib.rs | 4 + dhall/src/main.rs | 1 - dhall/src/normalize.rs | 181 +++++++++++++++++++++++++++++++++++++++ dhall/src/typecheck.rs | 2 +- dhall/tests/macros.rs | 1 - dhall_normalize/Cargo.toml | 18 ---- dhall_normalize/src/lib.rs | 6 -- dhall_normalize/src/normalize.rs | 181 --------------------------------------- 10 files changed, 188 insertions(+), 224 deletions(-) create mode 100644 dhall/src/normalize.rs delete mode 100644 dhall_normalize/Cargo.toml delete mode 100644 dhall_normalize/src/lib.rs delete mode 100644 dhall_normalize/src/normalize.rs diff --git a/Cargo.lock b/Cargo.lock index f15b230..cd0a0e0 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -136,7 +136,7 @@ version = "0.1.0" dependencies = [ "bytecount 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)", "dhall_core 0.1.0", - "dhall_normalize 0.1.0", + "dhall_generator 0.1.0", "itertools 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)", "lalrpop-util 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)", "term-painter 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)", @@ -166,20 +166,6 @@ dependencies = [ "quote 0.6.11 (registry+https://github.com/rust-lang/crates.io-index)", ] -[[package]] -name = "dhall_normalize" -version = "0.1.0" -dependencies = [ - "bytecount 0.5.1 (registry+https://github.com/rust-lang/crates.io-index)", - "dhall_core 0.1.0", - "dhall_generator 0.1.0", - "itertools 0.8.0 (registry+https://github.com/rust-lang/crates.io-index)", - "lalrpop-util 0.16.3 (registry+https://github.com/rust-lang/crates.io-index)", - "nom 3.2.1 (registry+https://github.com/rust-lang/crates.io-index)", - "pest 2.1.0 (git+https://github.com/pest-parser/pest)", - "term-painter 0.2.4 (registry+https://github.com/rust-lang/crates.io-index)", -] - [[package]] name = "dhall_parser" version = "0.1.0" diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml index 2505570..c303ac3 100644 --- a/dhall/Cargo.toml +++ b/dhall/Cargo.toml @@ -13,4 +13,4 @@ itertools = "0.8.0" lalrpop-util = "0.16.3" term-painter = "0.2.3" dhall_core = { path = "../dhall_core" } -dhall_normalize = { path = "../dhall_normalize" } +dhall_generator = { path = "../dhall_generator" } diff --git a/dhall/src/lib.rs b/dhall/src/lib.rs index 32662cd..58b29a3 100644 --- a/dhall/src/lib.rs +++ b/dhall/src/lib.rs @@ -1,4 +1,8 @@ #![feature(box_patterns)] #![feature(trace_macros)] +#![feature(proc_macro_hygiene)] +mod normalize; +pub use crate::normalize::*; pub mod typecheck; + diff --git a/dhall/src/main.rs b/dhall/src/main.rs index 182f4a7..3e8aca4 100644 --- a/dhall/src/main.rs +++ b/dhall/src/main.rs @@ -4,7 +4,6 @@ use term_painter::ToStyle; use dhall::*; use dhall_core::*; -use dhall_normalize::*; const ERROR_STYLE: term_painter::Color = term_painter::Color::Red; const BOLD: term_painter::Attr = term_painter::Attr::Bold; diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs new file mode 100644 index 0000000..ec594da --- /dev/null +++ b/dhall/src/normalize.rs @@ -0,0 +1,181 @@ +#![allow(non_snake_case)] +use dhall_core::core::*; +use dhall_generator::dhall; +use std::fmt; + +/// 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 { + // Matches that don't normalize everything right away + Let(f, _, r, 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(b, t, f) => match normalize(b) { + BoolLit(true) => normalize(t), + BoolLit(false) => normalize(f), + b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))), + }, + Annot(x, _) => normalize(x), + Note(_, e) => normalize(e), + App(f, 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 `Optional` + (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), box e2)) | + (App(box Builtin(OptionalFold), _), App(box App(box Builtin(OptionalBuild), _), 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(box Builtin(ListBuild), a0), k) => { + let k = bx(k); + let a1 = bx(shift(1, V("a", 0), &a0)); + normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0))) + } + (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| { + let y = bx(y); + let ys = bx(ys); + dhall!(cons y 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, _| { + let y = bx(y); + dhall!(just y) + }); + normalize(&e2) + } + (App(box Builtin(OptionalBuild), a0), g) => { + let g = bx(g); + normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0))) + } + (f2, a2) => app(f2, a2), + }, + }, + + // Normalize everything else before matching + 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()) + } + Merge(_x, _y, _t) => unimplemented!(), + Field(box RecordLit(kvs), x) => match kvs.get(x) { + Some(r) => r.clone(), + None => Field(bx(RecordLit(kvs)), x), + }, + e => e, + }, + } +} diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 8cab0ac..befd8c4 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -3,6 +3,7 @@ use std::collections::BTreeMap; use std::collections::HashSet; use std::fmt; +use crate::normalize; use dhall_core::context::Context; use dhall_core::core; use dhall_core::core::Builtin::*; @@ -10,7 +11,6 @@ use dhall_core::core::Const::*; use dhall_core::core::Expr::*; use dhall_core::core::{app, pi}; use dhall_core::core::{bx, shift, subst, Expr, V, X}; -use dhall_normalize::normalize; use self::TypeMessage::*; diff --git a/dhall/tests/macros.rs b/dhall/tests/macros.rs index 7c9d458..777a2f6 100644 --- a/dhall/tests/macros.rs +++ b/dhall/tests/macros.rs @@ -92,7 +92,6 @@ macro_rules! make_spec_test { fn $name() { use dhall::*; use dhall_core::*; - use dhall_normalize::*; use std::thread; thread::Builder::new() diff --git a/dhall_normalize/Cargo.toml b/dhall_normalize/Cargo.toml deleted file mode 100644 index ad1cc0d..0000000 --- a/dhall_normalize/Cargo.toml +++ /dev/null @@ -1,18 +0,0 @@ -[package] -name = "dhall_normalize" -version = "0.1.0" -authors = ["NanoTech ", "Nadrieril "] -edition = "2018" - -[lib] -doctest = false - -[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" } -dhall_generator = { path = "../dhall_generator" } diff --git a/dhall_normalize/src/lib.rs b/dhall_normalize/src/lib.rs deleted file mode 100644 index df49146..0000000 --- a/dhall_normalize/src/lib.rs +++ /dev/null @@ -1,6 +0,0 @@ -#![feature(box_patterns)] -#![feature(trace_macros)] -#![feature(proc_macro_hygiene)] - -mod normalize; -pub use crate::normalize::*; diff --git a/dhall_normalize/src/normalize.rs b/dhall_normalize/src/normalize.rs deleted file mode 100644 index ec594da..0000000 --- a/dhall_normalize/src/normalize.rs +++ /dev/null @@ -1,181 +0,0 @@ -#![allow(non_snake_case)] -use dhall_core::core::*; -use dhall_generator::dhall; -use std::fmt; - -/// 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 { - // Matches that don't normalize everything right away - Let(f, _, r, 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(b, t, f) => match normalize(b) { - BoolLit(true) => normalize(t), - BoolLit(false) => normalize(f), - b2 => BoolIf(bx(b2), bx(normalize(t)), bx(normalize(f))), - }, - Annot(x, _) => normalize(x), - Note(_, e) => normalize(e), - App(f, 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 `Optional` - (App(box Builtin(OptionalBuild), _), App(box App(box Builtin(OptionalFold), _), box e2)) | - (App(box Builtin(OptionalFold), _), App(box App(box Builtin(OptionalBuild), _), 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(box Builtin(ListBuild), a0), k) => { - let k = bx(k); - let a1 = bx(shift(1, V("a", 0), &a0)); - normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0))) - } - (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| { - let y = bx(y); - let ys = bx(ys); - dhall!(cons y 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, _| { - let y = bx(y); - dhall!(just y) - }); - normalize(&e2) - } - (App(box Builtin(OptionalBuild), a0), g) => { - let g = bx(g); - normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0))) - } - (f2, a2) => app(f2, a2), - }, - }, - - // Normalize everything else before matching - 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()) - } - Merge(_x, _y, _t) => unimplemented!(), - Field(box RecordLit(kvs), x) => match kvs.get(x) { - Some(r) => r.clone(), - None => Field(bx(RecordLit(kvs)), x), - }, - e => e, - }, - } -} -- cgit v1.2.3