summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Cargo.lock14
-rw-r--r--dhall/Cargo.toml1
-rw-r--r--dhall/src/main.rs1
-rw-r--r--dhall/src/typecheck.rs3
-rw-r--r--dhall/tests/macros.rs1
-rw-r--r--dhall_core/src/core.rs290
-rw-r--r--dhall_normalize/Cargo.toml14
-rw-r--r--dhall_normalize/src/lib.rs5
-rw-r--r--dhall_normalize/src/normalize.rs286
9 files changed, 328 insertions, 287 deletions
diff --git a/Cargo.lock b/Cargo.lock
index 58fdd1c..57ad661 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -136,6 +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",
"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)",
@@ -156,6 +157,19 @@ dependencies = [
]
[[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",
+ "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"
dependencies = [
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index db62d5b..80df0c3 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -10,3 +10,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" }
diff --git a/dhall/src/main.rs b/dhall/src/main.rs
index 3e8aca4..182f4a7 100644
--- a/dhall/src/main.rs
+++ b/dhall/src/main.rs
@@ -4,6 +4,7 @@ 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/typecheck.rs b/dhall/src/typecheck.rs
index 61a83e7..26192d2 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -9,7 +9,8 @@ use dhall_core::core::Builtin::*;
use dhall_core::core::Const::*;
use dhall_core::core::Expr::*;
use dhall_core::core::{app, pi};
-use dhall_core::core::{bx, normalize, shift, subst, Expr, V, X};
+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 777a2f6..7c9d458 100644
--- a/dhall/tests/macros.rs
+++ b/dhall/tests/macros.rs
@@ -92,6 +92,7 @@ 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_core/src/core.rs b/dhall_core/src/core.rs
index 340cb04..0787862 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -233,21 +233,21 @@ impl<'i, S, A> From<Builtin> for Expr<'i, S, A> {
}
impl<'i, S, A> Expr<'i, S, A> {
- fn bool_lit(&self) -> Option<bool> {
+ pub fn bool_lit(&self) -> Option<bool> {
match *self {
Expr::BoolLit(v) => Some(v),
_ => None,
}
}
- fn natural_lit(&self) -> Option<usize> {
+ pub fn natural_lit(&self) -> Option<usize> {
match *self {
Expr::NaturalLit(v) => Some(v),
_ => None,
}
}
- fn text_lit(&self) -> Option<String> {
+ pub fn text_lit(&self) -> Option<String> {
match *self {
Expr::TextLit(ref t) => Some(t.clone()), // FIXME?
_ => None,
@@ -630,7 +630,7 @@ fn add_ui(u: usize, i: isize) -> usize {
}
}
-fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
+pub fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U>
where
I: IntoIterator<Item = (&'a K, &'a V)>,
K: Eq + Ord + Copy + 'a,
@@ -921,285 +921,3 @@ where
map_op2(f, |x| bx(subst(v, e, x)), a, b)
}
-/// 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 crate::BinOp::*;
- use crate::Builtin::*;
- use crate::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::<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 `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<Expr<'i, S, A>>, 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<S, A>(e: &Expr<S, A>) -> 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<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))
- }
-}
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 <nanotech@nanotechcorp.net>", "Nadrieril <nadrieril@users.noreply.github.com>"]
+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::<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 `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<Expr<'i, S, A>>, 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<S, A>(e: &Expr<S, A>) -> 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<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))
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 12:08:37 +0000