summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/normalize.rs951
1 files changed, 494 insertions, 457 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 1c90c77..13a3678 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use dhall_core::context::Context;
use dhall_core::{
- rc, Builtin, Const, ExprF, Integer, InterpolatedText,
+ rc, BinOp, Builtin, Const, ExprF, Integer, InterpolatedText,
InterpolatedTextContents, Label, Natural, SubExpr, V, X,
};
use dhall_generator as dhall;
@@ -59,194 +59,6 @@ impl<'a> Typed<'a> {
}
}
-fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
- use dhall_core::Builtin::*;
- use Value::*;
-
- // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
- let ret = match (b, args.as_slice()) {
- (OptionalNone, [t, r..]) => {
- Ok((r, EmptyOptionalLit(TypeThunk::from_thunk(t.clone()))))
- }
- (NaturalIsZero, [n, r..]) => match &*n.as_value() {
- NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
- _ => Err(()),
- },
- (NaturalEven, [n, r..]) => match &*n.as_value() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
- _ => Err(()),
- },
- (NaturalOdd, [n, r..]) => match &*n.as_value() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
- _ => Err(()),
- },
- (NaturalToInteger, [n, r..]) => match &*n.as_value() {
- NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
- _ => Err(()),
- },
- (NaturalShow, [n, r..]) => match &*n.as_value() {
- NaturalLit(n) => Ok((
- r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
- )),
- _ => Err(()),
- },
- (ListLength, [_, l, r..]) => match &*l.as_value() {
- EmptyListLit(_) => Ok((r, NaturalLit(0))),
- NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
- _ => Err(()),
- },
- (ListHead, [_, l, r..]) => match &*l.as_value() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
- }
- _ => Err(()),
- },
- (ListLast, [_, l, r..]) => match &*l.as_value() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
- }
- _ => Err(()),
- },
- (ListReverse, [_, l, r..]) => match &*l.as_value() {
- EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
- }
- _ => Err(()),
- },
- (ListIndexed, [_, l, r..]) => match &*l.as_value() {
- EmptyListLit(t) => {
- let mut kts = BTreeMap::new();
- kts.insert(
- "index".into(),
- TypeThunk::from_whnf(Value::from_builtin(Natural)),
- );
- kts.insert("value".into(), t.clone());
- Ok((r, EmptyListLit(TypeThunk::from_whnf(RecordType(kts)))))
- }
- NEListLit(xs) => {
- let xs = xs
- .iter()
- .enumerate()
- .map(|(i, e)| {
- let i = NaturalLit(i);
- let mut kvs = BTreeMap::new();
- kvs.insert("index".into(), Thunk::from_whnf(i));
- kvs.insert("value".into(), e.clone());
- Thunk::from_whnf(RecordLit(kvs))
- })
- .collect();
- Ok((r, NEListLit(xs)))
- }
- _ => Err(()),
- },
- (ListBuild, [t, f, r..]) => match &*f.as_value() {
- // fold/build fusion
- Value::AppliedBuiltin(ListFold, args) => {
- if args.len() >= 2 {
- Ok((r, args[1].to_value()))
- } else {
- // Do we really need to handle this case ?
- unimplemented!()
- }
- }
- _ => Ok((
- r,
- f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
- .app_val(ListConsClosure(
- TypeThunk::from_thunk(t.clone()),
- None,
- ))
- .app_val(EmptyListLit(TypeThunk::from_thunk(t.clone()))),
- )),
- },
- (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
- EmptyListLit(_) => Ok((r, nil.to_value())),
- NEListLit(xs) => {
- let mut v = nil.clone();
- for x in xs.iter().rev() {
- v = cons
- .clone()
- .app_thunk(x.clone())
- .app_thunk(v)
- .into_thunk();
- }
- Ok((r, v.to_value()))
- }
- _ => Err(()),
- },
- (OptionalBuild, [t, f, r..]) => match &*f.as_value() {
- // fold/build fusion
- Value::AppliedBuiltin(OptionalFold, args) => {
- if args.len() >= 2 {
- Ok((r, args[1].to_value()))
- } else {
- // Do we really need to handle this case ?
- unimplemented!()
- }
- }
- _ => Ok((
- r,
- f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
- .app_val(OptionalSomeClosure(TypeThunk::from_thunk(
- t.clone(),
- )))
- .app_val(EmptyOptionalLit(TypeThunk::from_thunk(
- t.clone(),
- ))),
- )),
- },
- (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() {
- EmptyOptionalLit(_) => Ok((r, nothing.to_value())),
- NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
- _ => Err(()),
- },
- (NaturalBuild, [f, r..]) => match &*f.as_value() {
- // fold/build fusion
- Value::AppliedBuiltin(NaturalFold, args) => {
- if args.len() >= 1 {
- Ok((r, args[0].to_value()))
- } else {
- // Do we really need to handle this case ?
- unimplemented!()
- }
- }
- _ => Ok((
- r,
- f.app_val(Value::from_builtin(Natural))
- .app_val(NaturalSuccClosure)
- .app_val(NaturalLit(0)),
- )),
- },
- (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() {
- NaturalLit(0) => Ok((r, zero.to_value())),
- NaturalLit(n) => {
- let fold = Value::from_builtin(NaturalFold)
- .app(NaturalLit(n - 1))
- .app_thunk(t.clone())
- .app_thunk(succ.clone())
- .app_thunk(zero.clone());
- Ok((r, succ.app_val(fold)))
- }
- _ => Err(()),
- },
- _ => Err(()),
- };
- match ret {
- Ok((unconsumed_args, mut v)) => {
- let n_consumed_args = args.len() - unconsumed_args.len();
- for x in args.into_iter().skip(n_consumed_args) {
- v = v.app_thunk(x);
- }
- v
- }
- Err(()) => AppliedBuiltin(b, args),
- }
-}
-
#[derive(Debug, Clone)]
enum EnvItem {
Thunk(Thunk),
@@ -282,11 +94,6 @@ impl NormalizationContext {
pub(crate) fn new() -> Self {
NormalizationContext(Rc::new(Context::new()))
}
- fn insert(&self, x: &Label, e: Thunk) -> Self {
- NormalizationContext(Rc::new(
- self.0.insert(x.clone(), EnvItem::Thunk(e)),
- ))
- }
fn skip(&self, x: &Label) -> Self {
NormalizationContext(Rc::new(
self.0
@@ -297,7 +104,7 @@ impl NormalizationContext {
fn lookup(&self, var: &V<Label>) -> Value {
let V(x, n) = var;
match self.0.lookup(x, *n) {
- Some(EnvItem::Thunk(t)) => t.normalize_whnf().clone(),
+ Some(EnvItem::Thunk(t)) => t.to_value(),
Some(EnvItem::Skip(newvar)) => Value::Var(newvar.clone()),
None => Value::Var(var.clone()),
}
@@ -364,8 +171,7 @@ pub(crate) enum Value {
UnionLit(Label, Thunk, BTreeMap<Label, Option<TypeThunk>>),
TextLit(Vec<InterpolatedTextContents<Thunk>>),
/// Invariant: This must not contain a value captured by one of the variants above.
- PartialExpr(Box<ExprF<Value, Label, X, X>>),
- Expr(OutputSubExpr),
+ PartialExpr(ExprF<Thunk, Label, X, X>),
}
impl Value {
@@ -498,7 +304,6 @@ impl Value {
Value::PartialExpr(e) => {
rc(e.map_ref_simple(|v| v.normalize_to_expr()))
}
- Value::Expr(e) => e.clone(),
}
}
@@ -581,10 +386,9 @@ impl Value {
})
.collect(),
),
- Value::PartialExpr(e) => Value::PartialExpr(Box::new(
- e.map_ref_simple(|v| v.normalize()),
- )),
- Value::Expr(e) => Value::Expr(e.clone()),
+ Value::PartialExpr(e) => {
+ Value::PartialExpr(e.map_ref_simple(|v| v.normalize()))
+ }
}
}
@@ -595,8 +399,7 @@ impl Value {
| Value::Const(_)
| Value::BoolLit(_)
| Value::NaturalLit(_)
- | Value::IntegerLit(_)
- | Value::Expr(_) => {}
+ | Value::IntegerLit(_) => {}
Value::EmptyOptionalLit(tth)
| Value::OptionalSomeClosure(tth)
@@ -663,9 +466,7 @@ impl Value {
}
Value::PartialExpr(e) => {
// TODO: need map_mut_simple
- *self = Value::PartialExpr(Box::new(
- e.map_ref_simple(|v| v.normalize()),
- ))
+ *self = Value::PartialExpr(e.map_ref_simple(|v| v.normalize()))
}
}
}
@@ -682,57 +483,7 @@ impl Value {
/// Apply to a thunk
pub(crate) fn app_thunk(self, th: Thunk) -> Value {
- let fallback = |f: Value, a: Thunk| {
- Value::PartialExpr(Box::new(ExprF::App(
- f,
- a.normalize_whnf().clone(),
- )))
- };
-
- match self {
- Value::Lam(x, _, e) => {
- let val = Typed(
- TypedInternal::Value(th, None),
- std::marker::PhantomData,
- );
- e.subst_shift(&V(x, 0), &val).normalize_whnf().clone()
- }
- Value::AppliedBuiltin(b, mut args) => {
- args.push(th.clone());
- apply_builtin(b, args)
- }
- Value::OptionalSomeClosure(_) => Value::NEOptionalLit(th),
- Value::ListConsClosure(t, None) => {
- Value::ListConsClosure(t, Some(th))
- }
- Value::ListConsClosure(t, Some(x)) => {
- let v = th.normalize_whnf();
- match &*v {
- Value::EmptyListLit(_) => Value::NEListLit(vec![x]),
- Value::NEListLit(xs) => {
- let mut xs = xs.clone();
- xs.insert(0, x);
- Value::NEListLit(xs)
- }
- _ => {
- drop(v);
- fallback(Value::ListConsClosure(t, Some(x)), th)
- }
- }
- }
- Value::NaturalSuccClosure => {
- let v = th.normalize_whnf();
- match &*v {
- Value::NaturalLit(n) => Value::NaturalLit(n + 1),
- _ => {
- drop(v);
- fallback(Value::NaturalSuccClosure, th)
- }
- }
- }
- Value::UnionConstructor(l, kts) => Value::UnionLit(l, th, kts),
- f => fallback(f, th),
- }
+ Thunk::from_whnf(self).app_thunk(th)
}
pub(crate) fn from_builtin(b: Builtin) -> Value {
@@ -825,16 +576,15 @@ impl Value {
})
.collect(),
),
- Value::PartialExpr(e) => Value::PartialExpr(Box::new(
- e.map_ref_with_special_handling_of_binders(
+ Value::PartialExpr(e) => {
+ Value::PartialExpr(e.map_ref_with_special_handling_of_binders(
|v| v.shift(delta, var),
|x, v| v.shift(delta, &var.shift(1, &x.into())),
X::clone,
X::clone,
Label::clone,
- ),
- )),
- Value::Expr(e) => Value::Expr(e.shift(delta, var)),
+ ))
+ }
}
}
@@ -935,8 +685,8 @@ impl Value {
})
.collect(),
),
- Value::PartialExpr(e) => Value::PartialExpr(Box::new(
- e.map_ref_with_special_handling_of_binders(
+ Value::PartialExpr(e) => {
+ Value::PartialExpr(e.map_ref_with_special_handling_of_binders(
|v| v.subst_shift(var, val),
|x, v| {
v.subst_shift(
@@ -947,19 +697,16 @@ impl Value {
X::clone,
X::clone,
Label::clone,
- ),
- )),
- Value::Expr(e) => Value::Expr(
- e.subst_shift(var, &val.clone().normalize().as_expr()),
- ),
+ ))
+ }
}
}
}
mod thunk {
use super::{
- normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr,
- Value,
+ apply_any, normalize_whnf, InputSubExpr, NormalizationContext,
+ OutputSubExpr, Value,
};
use crate::expr::Typed;
use dhall_core::{Label, V};
@@ -1151,11 +898,11 @@ mod thunk {
}
pub(crate) fn app_val(&self, val: Value) -> Value {
- self.to_value().app(val)
+ self.app_thunk(val.into_thunk())
}
pub(crate) fn app_thunk(&self, th: Thunk) -> Value {
- self.to_value().app_thunk(th)
+ apply_any(self.clone(), th)
}
pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
@@ -1182,10 +929,6 @@ pub(crate) enum TypeThunk {
}
impl TypeThunk {
- fn new(ctx: NormalizationContext, e: InputSubExpr) -> TypeThunk {
- TypeThunk::from_thunk(Thunk::new(ctx, e))
- }
-
fn from_whnf(v: Value) -> TypeThunk {
TypeThunk::from_thunk(Thunk::from_whnf(v))
}
@@ -1243,215 +986,509 @@ impl TypeThunk {
}
}
-/// Reduces the imput expression to Value. See doc on `Value` for details.
+fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> Value {
+ use dhall_core::Builtin::*;
+ use Value::*;
+
+ // Return Ok((unconsumed args, returned value)), or Err(()) if value could not be produced.
+ let ret = match (b, args.as_slice()) {
+ (OptionalNone, [t, r..]) => {
+ Ok((r, EmptyOptionalLit(TypeThunk::from_thunk(t.clone()))))
+ }
+ (NaturalIsZero, [n, r..]) => match &*n.as_value() {
+ NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
+ _ => Err(()),
+ },
+ (NaturalEven, [n, r..]) => match &*n.as_value() {
+ NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
+ _ => Err(()),
+ },
+ (NaturalOdd, [n, r..]) => match &*n.as_value() {
+ NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
+ _ => Err(()),
+ },
+ (NaturalToInteger, [n, r..]) => match &*n.as_value() {
+ NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
+ _ => Err(()),
+ },
+ (NaturalShow, [n, r..]) => match &*n.as_value() {
+ NaturalLit(n) => Ok((
+ r,
+ TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
+ )),
+ _ => Err(()),
+ },
+ (ListLength, [_, l, r..]) => match &*l.as_value() {
+ EmptyListLit(_) => Ok((r, NaturalLit(0))),
+ NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
+ _ => Err(()),
+ },
+ (ListHead, [_, l, r..]) => match &*l.as_value() {
+ EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
+ NEListLit(xs) => {
+ Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
+ }
+ _ => Err(()),
+ },
+ (ListLast, [_, l, r..]) => match &*l.as_value() {
+ EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
+ NEListLit(xs) => {
+ Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
+ }
+ _ => Err(()),
+ },
+ (ListReverse, [_, l, r..]) => match &*l.as_value() {
+ EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
+ NEListLit(xs) => {
+ Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
+ }
+ _ => Err(()),
+ },
+ (ListIndexed, [_, l, r..]) => match &*l.as_value() {
+ EmptyListLit(t) => {
+ let mut kts = BTreeMap::new();
+ kts.insert(
+ "index".into(),
+ TypeThunk::from_whnf(Value::from_builtin(Natural)),
+ );
+ kts.insert("value".into(), t.clone());
+ Ok((r, EmptyListLit(TypeThunk::from_whnf(RecordType(kts)))))
+ }
+ NEListLit(xs) => {
+ let xs = xs
+ .iter()
+ .enumerate()
+ .map(|(i, e)| {
+ let i = NaturalLit(i);
+ let mut kvs = BTreeMap::new();
+ kvs.insert("index".into(), Thunk::from_whnf(i));
+ kvs.insert("value".into(), e.clone());
+ Thunk::from_whnf(RecordLit(kvs))
+ })
+ .collect();
+ Ok((r, NEListLit(xs)))
+ }
+ _ => Err(()),
+ },
+ (ListBuild, [t, f, r..]) => match &*f.as_value() {
+ // fold/build fusion
+ Value::AppliedBuiltin(ListFold, args) => {
+ if args.len() >= 2 {
+ Ok((r, args[1].to_value()))
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => Ok((
+ r,
+ f.app_val(Value::from_builtin(List).app_thunk(t.clone()))
+ .app_val(ListConsClosure(
+ TypeThunk::from_thunk(t.clone()),
+ None,
+ ))
+ .app_val(EmptyListLit(TypeThunk::from_thunk(t.clone()))),
+ )),
+ },
+ (ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_value() {
+ EmptyListLit(_) => Ok((r, nil.to_value())),
+ NEListLit(xs) => {
+ let mut v = nil.clone();
+ for x in xs.iter().rev() {
+ v = cons
+ .clone()
+ .app_thunk(x.clone())
+ .app_thunk(v)
+ .into_thunk();
+ }
+ Ok((r, v.to_value()))
+ }
+ _ => Err(()),
+ },
+ (OptionalBuild, [t, f, r..]) => match &*f.as_value() {
+ // fold/build fusion
+ Value::AppliedBuiltin(OptionalFold, args) => {
+ if args.len() >= 2 {
+ Ok((r, args[1].to_value()))
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => Ok((
+ r,
+ f.app_val(Value::from_builtin(Optional).app_thunk(t.clone()))
+ .app_val(OptionalSomeClosure(TypeThunk::from_thunk(
+ t.clone(),
+ )))
+ .app_val(EmptyOptionalLit(TypeThunk::from_thunk(
+ t.clone(),
+ ))),
+ )),
+ },
+ (OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_value() {
+ EmptyOptionalLit(_) => Ok((r, nothing.to_value())),
+ NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
+ _ => Err(()),
+ },
+ (NaturalBuild, [f, r..]) => match &*f.as_value() {
+ // fold/build fusion
+ Value::AppliedBuiltin(NaturalFold, args) => {
+ if args.len() >= 1 {
+ Ok((r, args[0].to_value()))
+ } else {
+ // Do we really need to handle this case ?
+ unimplemented!()
+ }
+ }
+ _ => Ok((
+ r,
+ f.app_val(Value::from_builtin(Natural))
+ .app_val(NaturalSuccClosure)
+ .app_val(NaturalLit(0)),
+ )),
+ },
+ (NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_value() {
+ NaturalLit(0) => Ok((r, zero.to_value())),
+ NaturalLit(n) => {
+ let fold = Value::from_builtin(NaturalFold)
+ .app(NaturalLit(n - 1))
+ .app_thunk(t.clone())
+ .app_thunk(succ.clone())
+ .app_thunk(zero.clone());
+ Ok((r, succ.app_val(fold)))
+ }
+ _ => Err(()),
+ },
+ _ => Err(()),
+ };
+ match ret {
+ Ok((unconsumed_args, mut v)) => {
+ let n_consumed_args = args.len() - unconsumed_args.len();
+ for x in args.into_iter().skip(n_consumed_args) {
+ v = v.app_thunk(x);
+ }
+ v
+ }
+ Err(()) => AppliedBuiltin(b, args),
+ }
+}
+
+fn apply_any(f: Thunk, a: Thunk) -> Value {
+ let fallback = |f: Thunk, a: Thunk| Value::PartialExpr(ExprF::App(f, a));
+
+ let f_borrow = f.as_value();
+ match &*f_borrow {
+ Value::Lam(x, _, e) => {
+ let val = Typed::from_thunk_untyped(a);
+ e.subst_shift(&x.into(), &val).to_value()
+ }
+ Value::AppliedBuiltin(b, args) => {
+ use std::iter::once;
+ let args = args.iter().cloned().chain(once(a.clone())).collect();
+ apply_builtin(*b, args)
+ }
+ Value::OptionalSomeClosure(_) => Value::NEOptionalLit(a),
+ Value::ListConsClosure(t, None) => {
+ Value::ListConsClosure(t.clone(), Some(a))
+ }
+ Value::ListConsClosure(_, Some(x)) => {
+ let a_borrow = a.as_value();
+ match &*a_borrow {
+ Value::EmptyListLit(_) => Value::NEListLit(vec![x.clone()]),
+ Value::NEListLit(xs) => {
+ use std::iter::once;
+ let xs =
+ once(x.clone()).chain(xs.iter().cloned()).collect();
+ Value::NEListLit(xs)
+ }
+ _ => {
+ drop(f_borrow);
+ drop(a_borrow);
+ fallback(f, a)
+ }
+ }
+ }
+ Value::NaturalSuccClosure => {
+ let a_borrow = a.as_value();
+ match &*a_borrow {
+ Value::NaturalLit(n) => Value::NaturalLit(n + 1),
+ _ => {
+ drop(f_borrow);
+ drop(a_borrow);
+ fallback(f, a)
+ }
+ }
+ }
+ Value::UnionConstructor(l, kts) => {
+ Value::UnionLit(l.clone(), a, kts.clone())
+ }
+ _ => {
+ drop(f_borrow);
+ fallback(f, a)
+ }
+ }
+}
+
+/// Reduces the imput expression to a Value. Evaluates as little as possible.
fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> Value {
match expr.as_ref() {
- ExprF::Var(v) => ctx.lookup(&v),
- ExprF::Annot(x, _) => normalize_whnf(ctx, x.clone()),
- ExprF::Note(_, e) => normalize_whnf(ctx, e.clone()),
- ExprF::Embed(e) => e.to_value(),
- ExprF::Let(x, _, r, b) => {
- let t = Thunk::new(ctx.clone(), r.clone());
- normalize_whnf(ctx.insert(x, t), b.clone())
+ ExprF::Embed(e) => return e.to_value(),
+ ExprF::Var(v) => return ctx.lookup(&v),
+ _ => {}
+ }
+
+ // Thunk subexpressions
+ let expr: ExprF<Thunk, Label, X, X> =
+ expr.as_ref().map_ref_with_special_handling_of_binders(
+ |e| Thunk::new(ctx.clone(), e.clone()),
+ |x, e| Thunk::new(ctx.skip(x), e.clone()),
+ X::clone,
+ |_| unreachable!(),
+ Label::clone,
+ );
+
+ normalize_one_layer(expr)
+}
+
+fn normalize_one_layer(expr: ExprF<Thunk, Label, X, X>) -> Value {
+ use Value::{
+ BoolLit, EmptyListLit, EmptyOptionalLit, Lam, NEListLit, NEOptionalLit,
+ NaturalLit, Pi, RecordLit, RecordType, TextLit, UnionConstructor,
+ UnionLit, UnionType,
+ };
+
+ // Small helper enum to avoid repetition
+ enum Ret<'a> {
+ RetValue(Value),
+ RetThunk(Thunk),
+ RetThunkRef(&'a Thunk),
+ RetExpr(ExprF<Thunk, Label, X, X>),
+ }
+ use Ret::{RetExpr, RetThunk, RetThunkRef, RetValue};
+
+ let ret = match expr {
+ ExprF::Embed(_) => unreachable!(),
+ ExprF::Var(_) => unreachable!(),
+ ExprF::Annot(x, _) => RetThunk(x),
+ ExprF::Note(_, e) => RetThunk(e),
+ ExprF::Lam(x, t, e) => RetValue(Lam(x, t, e)),
+ ExprF::Pi(x, t, e) => {
+ RetValue(Pi(x, TypeThunk::from_thunk(t), TypeThunk::from_thunk(e)))
}
- ExprF::Lam(x, t, e) => Value::Lam(
- x.clone(),
- Thunk::new(ctx.clone(), t.clone()),
- Thunk::new(ctx.skip(x), e.clone()),
- ),
- ExprF::Builtin(b) => Value::from_builtin(*b),
- ExprF::Const(c) => Value::Const(*c),
- ExprF::BoolLit(b) => Value::BoolLit(*b),
- ExprF::NaturalLit(n) => Value::NaturalLit(*n),
- ExprF::OldOptionalLit(None, e) => {
- Value::EmptyOptionalLit(TypeThunk::new(ctx, e.clone()))
+ ExprF::Let(x, _, v, b) => {
+ let v = Typed::from_thunk_untyped(v);
+ RetThunk(b.subst_shift(&x.into(), &v))
}
- ExprF::OldOptionalLit(Some(e), _) => {
- Value::NEOptionalLit(Thunk::new(ctx, e.clone()))
+ ExprF::App(v, a) => RetValue(v.app_thunk(a)),
+ ExprF::Builtin(b) => RetValue(Value::from_builtin(b)),
+ ExprF::Const(c) => RetValue(Value::Const(c)),
+ ExprF::BoolLit(b) => RetValue(BoolLit(b)),
+ ExprF::NaturalLit(n) => RetValue(NaturalLit(n)),
+ ExprF::IntegerLit(_) | ExprF::DoubleLit(_) => RetExpr(expr),
+ ExprF::OldOptionalLit(None, t) => {
+ RetValue(EmptyOptionalLit(TypeThunk::from_thunk(t)))
}
- ExprF::SomeLit(e) => Value::NEOptionalLit(Thunk::new(ctx, e.clone())),
- ExprF::EmptyListLit(e) => {
- Value::EmptyListLit(TypeThunk::new(ctx, e.clone()))
+ ExprF::OldOptionalLit(Some(e), _) => RetValue(NEOptionalLit(e)),
+ ExprF::SomeLit(e) => RetValue(NEOptionalLit(e)),
+ ExprF::EmptyListLit(t) => {
+ RetValue(EmptyListLit(TypeThunk::from_thunk(t)))
}
- ExprF::NEListLit(elts) => Value::NEListLit(
- elts.iter()
- .map(|e| Thunk::new(ctx.clone(), e.clone()))
- .collect(),
- ),
- ExprF::RecordLit(kvs) => Value::RecordLit(
- kvs.iter()
- .map(|(k, e)| (k.clone(), Thunk::new(ctx.clone(), e.clone())))
+ ExprF::NEListLit(elts) => {
+ RetValue(NEListLit(elts.into_iter().collect()))
+ }
+ ExprF::RecordLit(kvs) => RetValue(RecordLit(kvs.into_iter().collect())),
+ ExprF::RecordType(kts) => RetValue(RecordType(
+ kts.into_iter()
+ .map(|(k, t)| (k, TypeThunk::from_thunk(t)))
.collect(),
- ),
- ExprF::UnionType(kts) => Value::UnionType(
- kts.iter()
- .map(|(k, t)| {
- (
- k.clone(),
- t.as_ref()
- .map(|t| TypeThunk::new(ctx.clone(), t.clone())),
- )
- })
+ )),
+ ExprF::UnionLit(l, x, kts) => RetValue(UnionLit(
+ l,
+ x,
+ kts.into_iter()
+ .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
.collect(),
- ),
- ExprF::UnionLit(l, x, kts) => Value::UnionLit(
- l.clone(),
- Thunk::new(ctx.clone(), x.clone()),
- kts.iter()
- .map(|(k, t)| {
- (
- k.clone(),
- t.as_ref()
- .map(|t| TypeThunk::new(ctx.clone(), t.clone())),
- )
- })
+ )),
+ ExprF::UnionType(kts) => RetValue(UnionType(
+ kts.into_iter()
+ .map(|(k, t)| (k, t.map(|t| TypeThunk::from_thunk(t))))
.collect(),
- ),
+ )),
ExprF::TextLit(elts) => {
- use InterpolatedTextContents::{Expr, Text};
- let elts: Vec<_> = elts
- .iter()
- .map(|contents| match contents {
- Expr(n) => Expr(Thunk::new(ctx.clone(), n.clone())),
- Text(s) => Text(s.clone()),
- })
- .collect();
- if elts.len() == 1 {
- if let Expr(th) = &elts[0] {
- return th.normalize_whnf().clone();
- }
+ use InterpolatedTextContents::Expr;
+ let elts: Vec<_> = elts.into_iter().collect();
+ // Simplify bare interpolation
+ if let [Expr(th)] = elts.as_slice() {
+ RetThunk(th.clone())
+ } else {
+ RetValue(TextLit(elts))
}
- Value::TextLit(elts)
}
- ExprF::BoolIf(b, e1, e2) => {
- let b = normalize_whnf(ctx.clone(), b.clone());
- match b {
- Value::BoolLit(true) => normalize_whnf(ctx, e1.clone()),
- Value::BoolLit(false) => normalize_whnf(ctx, e2.clone()),
- b => {
- let e1 = normalize_whnf(ctx.clone(), e1.clone());
- let e2 = normalize_whnf(ctx, e2.clone());
- match (e1, e2) {
- (Value::BoolLit(true), Value::BoolLit(false)) => b,
- (e1, e2) => {
- normalize_last_layer(ExprF::BoolIf(b, e1, e2))
+ ExprF::BoolIf(ref b, ref e1, ref e2) => {
+ let b_borrow = b.as_value();
+ match &*b_borrow {
+ BoolLit(true) => RetThunkRef(e1),
+ BoolLit(false) => RetThunkRef(e2),
+ _ => {
+ let e1_borrow = e1.as_value();
+ let e2_borrow = e2.as_value();
+ match (&*e1_borrow, &*e2_borrow) {
+ // Simplify `if b then True else False`
+ (BoolLit(true), BoolLit(false)) => RetThunkRef(b),
+ _ => {
+ drop(b_borrow);
+ drop(e1_borrow);
+ drop(e2_borrow);
+ RetExpr(expr)
}
}
}
}
}
- expr => {
- // Recursively normalize subexpressions
- let expr: ExprF<Value, Label, X, X> = expr
- .map_ref_with_special_handling_of_binders(
- |e| normalize_whnf(ctx.clone(), e.clone()),
- |x, e| normalize_whnf(ctx.skip(x), e.clone()),
- X::clone,
- |_| unreachable!(),
- Label::clone,
- );
+ ExprF::BinOp(o, ref x, ref y) => {
+ use BinOp::{
+ BoolAnd, BoolEQ, BoolNE, BoolOr, ListAppend, NaturalPlus,
+ NaturalTimes, TextAppend,
+ };
+ let x_borrow = x.as_value();
+ let y_borrow = y.as_value();
+ match (o, &*x_borrow, &*y_borrow) {
+ (BoolAnd, BoolLit(true), _) => RetThunkRef(y),
+ (BoolAnd, _, BoolLit(true)) => RetThunkRef(x),
+ (BoolAnd, BoolLit(false), _) => RetValue(BoolLit(false)),
+ (BoolAnd, _, BoolLit(false)) => RetValue(BoolLit(false)),
+ (BoolOr, BoolLit(true), _) => RetValue(BoolLit(true)),
+ (BoolOr, _, BoolLit(true)) => RetValue(BoolLit(true)),
+ (BoolOr, BoolLit(false), _) => RetThunkRef(y),
+ (BoolOr, _, BoolLit(false)) => RetThunkRef(x),
+ (BoolEQ, BoolLit(true), _) => RetThunkRef(y),
+ (BoolEQ, _, BoolLit(true)) => RetThunkRef(x),
+ (BoolEQ, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x == y)),
+ (BoolNE, BoolLit(false), _) => RetThunkRef(y),
+ (BoolNE, _, BoolLit(false)) => RetThunkRef(x),
+ (BoolNE, BoolLit(x), BoolLit(y)) => RetValue(BoolLit(x != y)),
+
+ (NaturalPlus, NaturalLit(0), _) => RetThunkRef(y),
+ (NaturalPlus, _, NaturalLit(0)) => RetThunkRef(x),
+ (NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
+ RetValue(NaturalLit(x + y))
+ }
+ (NaturalTimes, NaturalLit(0), _) => RetValue(NaturalLit(0)),
+ (NaturalTimes, _, NaturalLit(0)) => RetValue(NaturalLit(0)),
+ (NaturalTimes, NaturalLit(1), _) => RetThunkRef(y),
+ (NaturalTimes, _, NaturalLit(1)) => RetThunkRef(x),
+ (NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
+ RetValue(NaturalLit(x * y))
+ }
- normalize_last_layer(expr)
- }
- }
-}
+ (ListAppend, EmptyListLit(_), _) => RetThunkRef(y),
+ (ListAppend, _, EmptyListLit(_)) => RetThunkRef(x),
+ (ListAppend, NEListLit(xs), NEListLit(ys)) => RetValue(
+ NEListLit(xs.iter().chain(ys.iter()).cloned().collect()),
+ ),
-/// When all sub-expressions have been (partially) normalized, eval the remaining toplevel layer.
-fn normalize_last_layer(expr: ExprF<Value, Label, X, X>) -> Value {
- use dhall_core::BinOp::*;
- use Value::*;
+ (TextAppend, TextLit(x), _) if x.is_empty() => RetThunkRef(y),
+ (TextAppend, _, TextLit(y)) if y.is_empty() => RetThunkRef(x),
+ (TextAppend, TextLit(x), TextLit(y)) => RetValue(TextLit(
+ x.iter().chain(y.iter()).cloned().collect(),
+ )),
+ (TextAppend, TextLit(x), _) => {
+ use std::iter::once;
+ let y = InterpolatedTextContents::Expr(y.clone());
+ RetValue(TextLit(
+ x.iter().cloned().chain(once(y)).collect(),
+ ))
+ }
+ (TextAppend, _, TextLit(y)) => {
+ use std::iter::once;
+ let x = InterpolatedTextContents::Expr(x.clone());
+ RetValue(TextLit(
+ once(x).chain(y.iter().cloned()).collect(),
+ ))
+ }
- match expr {
- ExprF::App(v, a) => v.app(a),
-
- ExprF::BinOp(BoolAnd, BoolLit(true), y) => y,
- ExprF::BinOp(BoolAnd, x, BoolLit(true)) => x,
- ExprF::BinOp(BoolAnd, BoolLit(false), _) => BoolLit(false),
- ExprF::BinOp(BoolAnd, _, BoolLit(false)) => BoolLit(false),
- ExprF::BinOp(BoolOr, BoolLit(true), _) => BoolLit(true),
- ExprF::BinOp(BoolOr, _, BoolLit(true)) => BoolLit(true),
- ExprF::BinOp(BoolOr, BoolLit(false), y) => y,
- ExprF::BinOp(BoolOr, x, BoolLit(false)) => x,
- ExprF::BinOp(BoolEQ, BoolLit(true), y) => y,
- ExprF::BinOp(BoolEQ, x, BoolLit(true)) => x,
- ExprF::BinOp(BoolNE, BoolLit(false), y) => y,
- ExprF::BinOp(BoolNE, x, BoolLit(false)) => x,
- ExprF::BinOp(BoolEQ, BoolLit(x), BoolLit(y)) => BoolLit(x == y),
- ExprF::BinOp(BoolNE, BoolLit(x), BoolLit(y)) => BoolLit(x != y),
-
- ExprF::BinOp(NaturalPlus, NaturalLit(0), y) => y,
- ExprF::BinOp(NaturalPlus, x, NaturalLit(0)) => x,
- ExprF::BinOp(NaturalTimes, NaturalLit(0), _) => NaturalLit(0),
- ExprF::BinOp(NaturalTimes, _, NaturalLit(0)) => NaturalLit(0),
- ExprF::BinOp(NaturalTimes, NaturalLit(1), y) => y,
- ExprF::BinOp(NaturalTimes, x, NaturalLit(1)) => x,
- ExprF::BinOp(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
- NaturalLit(x + y)
- }
- ExprF::BinOp(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
- NaturalLit(x * y)
+ _ => {
+ drop(x_borrow);
+ drop(y_borrow);
+ RetExpr(expr)
+ }
+ }
}
- ExprF::BinOp(ListAppend, EmptyListLit(_), y) => y,
- ExprF::BinOp(ListAppend, x, EmptyListLit(_)) => x,
- ExprF::BinOp(ListAppend, NEListLit(mut xs), NEListLit(mut ys)) => {
- xs.append(&mut ys);
- NEListLit(xs)
- }
- ExprF::BinOp(TextAppend, TextLit(mut x), TextLit(mut y)) => {
- x.append(&mut y);
- TextLit(x)
- }
- ExprF::BinOp(TextAppend, TextLit(x), y) if x.is_empty() => y,
- ExprF::BinOp(TextAppend, x, TextLit(y)) if y.is_empty() => x,
- ExprF::BinOp(TextAppend, TextLit(mut x), y) => {
- x.push(InterpolatedTextContents::Expr(Thunk::from_whnf(y)));
- TextLit(x)
+ ExprF::Projection(_, ls) if ls.is_empty() => {
+ RetValue(RecordLit(std::collections::BTreeMap::new()))
}
- ExprF::BinOp(TextAppend, x, TextLit(mut y)) => {
- y.insert(0, InterpolatedTextContents::Expr(Thunk::from_whnf(x)));
- TextLit(y)
+ ExprF::Projection(ref v, ref ls) => {
+ let v_borrow = v.as_value();
+ match &*v_borrow {
+ RecordLit(kvs) => RetValue(RecordLit(
+ ls.iter()
+ .filter_map(|l| {
+ kvs.get(l).map(|x| (l.clone(), x.clone()))
+ })
+ .collect(),
+ )),
+ _ => {
+ drop(v_borrow);
+ RetExpr(expr)
+ }
+ }
}
-
- ExprF::Field(UnionType(kts), l) => UnionConstructor(l, kts),
- ExprF::Field(RecordLit(mut kvs), l) => match kvs.remove(&l) {
- Some(r) => r.normalize_whnf().clone(),
- None => {
- // Couldn't do anything useful, so just normalize subexpressions
- Expr(rc(ExprF::Field(RecordLit(kvs).normalize_to_expr(), l)))
+ ExprF::Field(ref v, ref l) => {
+ let v_borrow = v.as_value();
+ match &*v_borrow {
+ RecordLit(kvs) => match kvs.get(l) {
+ Some(r) => RetThunk(r.clone()),
+ None => {
+ drop(v_borrow);
+ RetExpr(expr)
+ }
+ },
+ UnionType(kts) => {
+ RetValue(UnionConstructor(l.clone(), kts.clone()))
+ }
+ _ => {
+ drop(v_borrow);
+ RetExpr(expr)
+ }
}
- },
- ExprF::Projection(_, ls) if ls.is_empty() => {
- RecordLit(std::collections::BTreeMap::new())
}
- ExprF::Projection(RecordLit(mut kvs), ls) => RecordLit(
- ls.into_iter()
- .filter_map(|l| kvs.remove(&l).map(|x| (l, x)))
- .collect(),
- ),
- ExprF::Merge(RecordLit(mut handlers), e, t) => {
- let e = match e {
- UnionConstructor(l, kts) => match handlers.remove(&l) {
- Some(h) => return h.normalize_whnf().clone(),
- None => UnionConstructor(l, kts),
+
+ ExprF::Merge(ref handlers, ref variant, _) => {
+ let handlers_borrow = handlers.as_value();
+ let variant_borrow = variant.as_value();
+ match (&*handlers_borrow, &*variant_borrow) {
+ (RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
+ Some(h) => RetThunk(h.clone()),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ RetExpr(expr)
+ }
},
- UnionLit(l, v, kts) => match handlers.remove(&l) {
- Some(h) => {
- let h = h.normalize_whnf().clone();
- return h.app_thunk(v);
+ (RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
+ Some(h) => RetValue(h.app_thunk(v.clone())),
+ None => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ RetExpr(expr)
}
- None => UnionLit(l, v, kts),
},
- e => e,
- };
- // Couldn't do anything useful, so just normalize subexpressions
- Expr(rc(ExprF::Merge(
- RecordLit(handlers).normalize_to_expr(),
- e.normalize_to_expr(),
- t.as_ref().map(Value::normalize_to_expr),
- )))
+ _ => {
+ drop(handlers_borrow);
+ drop(variant_borrow);
+ RetExpr(expr)
+ }
+ }
}
- expr => PartialExpr(Box::new(expr)),
+ };
+
+ match ret {
+ RetValue(v) => v,
+ RetThunk(th) => th.to_value(),
+ RetThunkRef(th) => th.to_value(),
+ RetExpr(expr) => Value::PartialExpr(expr),
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 01:34:00 +0000