summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/lib.rs4
-rw-r--r--dhall/src/main.rs1
-rw-r--r--dhall/src/normalize.rs181
-rw-r--r--dhall/src/typecheck.rs2
4 files changed, 186 insertions, 2 deletions
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::<S, T, A>(f) {
+ Lam(x, _A, b) => {
+ // Beta reduce
+ let vx0 = V(x, 0);
+ let a2 = shift::<S, S, A>(1, vx0, a);
+ let b2 = subst::<S, T, A>(vx0, &a2, &b);
+ let b3 = shift::<S, T, A>(-1, vx0, &b2);
+ normalize(&b3)
+ }
+ f2 => match (f2, normalize::<S, T, A>(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::*;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 14:02:18 +0000