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 --- 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 - 6 files changed, 187 insertions(+), 4 deletions(-) create mode 100644 dhall/src/normalize.rs (limited to 'dhall') 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() -- cgit v1.2.3