summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/core/value.rs54
-rw-r--r--dhall/src/core/valuef.rs9
-rw-r--r--dhall/src/phase/normalize.rs141
-rw-r--r--dhall/src/phase/typecheck.rs17
-rw-r--r--serde_dhall/src/lib.rs8
5 files changed, 153 insertions, 76 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 5055ac2..25fcaae 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,6 +44,14 @@ struct ValueInternal {
#[derive(Clone)]
pub struct Value(Rc<RefCell<ValueInternal>>);
+/// When a function needs to return either a freshly created ValueF or an existing Value, but
+/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to
+/// avoid loss of typ information.
+pub enum VoVF {
+ Value(Value),
+ ValueF(ValueF),
+}
+
impl ValueInternal {
fn into_value(self) -> Value {
Value(Rc::new(RefCell::new(self)))
@@ -56,7 +64,8 @@ impl ValueInternal {
take_mut::take(self, |vint| match &vint.form {
Unevaled => ValueInternal {
form: WHNF,
- value: normalize_whnf(vint.value),
+ // TODO: thunk chaining
+ value: normalize_whnf(vint.value).into_whnf(),
ty: vint.ty,
},
// Already in WHNF
@@ -166,6 +175,9 @@ impl Value {
pub(crate) fn into_typed(self) -> Typed {
Typed::from_value(self)
}
+ pub(crate) fn into_vovf(self) -> VoVF {
+ VoVF::Value(self)
+ }
/// Mutates the contents. If no one else shares this, this avoids a RefCell lock.
fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) {
@@ -212,8 +224,8 @@ impl Value {
self.as_nf().normalize_to_expr_maybe_alpha(alpha)
}
- pub(crate) fn app(&self, th: Value) -> ValueF {
- apply_any(self.clone(), th)
+ pub(crate) fn app(&self, v: Value) -> VoVF {
+ apply_any(self.clone(), v)
}
pub(crate) fn get_type(&self) -> Result<Cow<'_, Value>, TypeError> {
@@ -221,6 +233,42 @@ impl Value {
}
}
+impl VoVF {
+ pub fn into_whnf(self) -> ValueF {
+ match self {
+ VoVF::Value(v) => v.to_whnf(),
+ VoVF::ValueF(v) => v,
+ }
+ }
+ pub(crate) fn into_value_untyped(self) -> Value {
+ match self {
+ VoVF::Value(v) => v,
+ VoVF::ValueF(v) => v.into_value_untyped(),
+ }
+ }
+ pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+ match self {
+ // TODO: check type with debug_assert ?
+ VoVF::Value(v) => v,
+ VoVF::ValueF(v) => v.into_value_with_type(t),
+ }
+ }
+ pub(crate) fn into_value_simple_type(self) -> Value {
+ match self {
+ // TODO: check type with debug_assert ?
+ VoVF::Value(v) => v,
+ VoVF::ValueF(v) => v.into_value_simple_type(),
+ }
+ }
+
+ pub(crate) fn app(self, x: Value) -> Self {
+ match self {
+ VoVF::Value(v) => v.app(x),
+ VoVF::ValueF(v) => v.into_value_untyped().app(x),
+ }
+ }
+}
+
impl Shift for Value {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(Value(self.0.shift(delta, var)?))
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index e9049c7..80978a7 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
NaiveDouble, Natural,
};
-use crate::core::value::Value;
+use crate::core::value::{Value, VoVF};
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::{Normalized, NormalizedSubExpr};
@@ -56,6 +56,9 @@ impl ValueF {
pub(crate) fn into_value_simple_type(self) -> Value {
Value::from_valuef_simple_type(self)
}
+ pub(crate) fn into_vovf(self) -> VoVF {
+ VoVF::ValueF(self)
+ }
/// Convert the value to a fully normalized syntactic expression
pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
@@ -257,8 +260,8 @@ impl ValueF {
}
/// Apply to a value
- pub fn app(self, th: Value) -> ValueF {
- Value::from_valuef_untyped(self).app(th)
+ pub fn app(self, v: Value) -> VoVF {
+ self.into_vovf().app(v)
}
pub fn from_builtin(b: Builtin) -> ValueF {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index afc2e7f..e044018 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,7 +5,7 @@ use dhall_syntax::{
NaiveDouble,
};
-use crate::core::value::Value;
+use crate::core::value::{Value, VoVF};
use crate::core::valuef::ValueF;
use crate::core::var::{Shift, Subst};
use crate::phase::Normalized;
@@ -63,44 +63,48 @@ macro_rules! make_closure {
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
use dhall_syntax::Builtin::*;
use ValueF::*;
// 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(t.clone()))),
+ (OptionalNone, [t, r..]) => {
+ Ok((r, EmptyOptionalLit(t.clone()).into_vovf()))
+ }
(NaturalIsZero, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
+ NaturalLit(n) => Ok((r, BoolLit(*n == 0).into_vovf())),
_ => Err(()),
},
(NaturalEven, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0))),
+ NaturalLit(n) => Ok((r, BoolLit(*n % 2 == 0).into_vovf())),
_ => Err(()),
},
(NaturalOdd, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0))),
+ NaturalLit(n) => Ok((r, BoolLit(*n % 2 != 0).into_vovf())),
_ => Err(()),
},
(NaturalToInteger, [n, r..]) => match &*n.as_whnf() {
- NaturalLit(n) => Ok((r, IntegerLit(*n as isize))),
+ NaturalLit(n) => Ok((r, IntegerLit(*n as isize).into_vovf())),
_ => Err(()),
},
(NaturalShow, [n, r..]) => match &*n.as_whnf() {
NaturalLit(n) => Ok((
r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
+ TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
+ .into_vovf(),
)),
_ => Err(()),
},
(NaturalSubtract, [a, b, r..]) => {
match (&*a.as_whnf(), &*b.as_whnf()) {
- (NaturalLit(a), NaturalLit(b)) => {
- Ok((r, NaturalLit(if b > a { b - a } else { 0 })))
- }
- (NaturalLit(0), b) => Ok((r, b.clone())),
- (_, NaturalLit(0)) => Ok((r, NaturalLit(0))),
- _ if a == b => Ok((r, NaturalLit(0))),
+ (NaturalLit(a), NaturalLit(b)) => Ok((
+ r,
+ NaturalLit(if b > a { b - a } else { 0 }).into_vovf(),
+ )),
+ (NaturalLit(0), _) => Ok((r, b.clone().into_vovf())),
+ (_, NaturalLit(0)) => Ok((r, NaturalLit(0).into_vovf())),
+ _ if a == b => Ok((r, NaturalLit(0).into_vovf())),
_ => Err(()),
}
}
@@ -111,18 +115,25 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
} else {
format!("+{}", n)
};
- Ok((r, TextLit(vec![InterpolatedTextContents::Text(s)])))
+ Ok((
+ r,
+ TextLit(vec![InterpolatedTextContents::Text(s)])
+ .into_vovf(),
+ ))
}
_ => Err(()),
},
(IntegerToDouble, [n, r..]) => match &*n.as_whnf() {
- IntegerLit(n) => Ok((r, DoubleLit(NaiveDouble::from(*n as f64)))),
+ IntegerLit(n) => {
+ Ok((r, DoubleLit(NaiveDouble::from(*n as f64)).into_vovf()))
+ }
_ => Err(()),
},
(DoubleShow, [n, r..]) => match &*n.as_whnf() {
DoubleLit(n) => Ok((
r,
- TextLit(vec![InterpolatedTextContents::Text(n.to_string())]),
+ TextLit(vec![InterpolatedTextContents::Text(n.to_string())])
+ .into_vovf(),
)),
_ => Err(()),
},
@@ -137,7 +148,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
let s = txt.to_string();
Ok((
r,
- TextLit(vec![InterpolatedTextContents::Text(s)]),
+ TextLit(vec![InterpolatedTextContents::Text(s)])
+ .into_vovf(),
))
}
// If there are no interpolations (invariants ensure that when there are no
@@ -152,7 +164,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
let s = txt.to_string();
Ok((
r,
- TextLit(vec![InterpolatedTextContents::Text(s)]),
+ TextLit(vec![InterpolatedTextContents::Text(s)])
+ .into_vovf(),
))
}
_ => Err(()),
@@ -161,29 +174,33 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
_ => Err(()),
},
(ListLength, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ok((r, NaturalLit(0))),
- NEListLit(xs) => Ok((r, NaturalLit(xs.len()))),
+ EmptyListLit(_) => Ok((r, NaturalLit(0).into_vovf())),
+ NEListLit(xs) => Ok((r, NaturalLit(xs.len()).into_vovf())),
_ => Err(()),
},
(ListHead, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().next().unwrap().clone())))
- }
+ EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+ NEListLit(xs) => Ok((
+ r,
+ NEOptionalLit(xs.iter().next().unwrap().clone()).into_vovf(),
+ )),
_ => Err(()),
},
(ListLast, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEOptionalLit(xs.iter().rev().next().unwrap().clone())))
- }
+ EmptyListLit(n) => Ok((r, EmptyOptionalLit(n.clone()).into_vovf())),
+ NEListLit(xs) => Ok((
+ r,
+ NEOptionalLit(xs.iter().rev().next().unwrap().clone())
+ .into_vovf(),
+ )),
_ => Err(()),
},
(ListReverse, [_, l, r..]) => match &*l.as_whnf() {
- EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()))),
- NEListLit(xs) => {
- Ok((r, NEListLit(xs.iter().rev().cloned().collect())))
- }
+ EmptyListLit(n) => Ok((r, EmptyListLit(n.clone()).into_vovf())),
+ NEListLit(xs) => Ok((
+ r,
+ NEListLit(xs.iter().rev().cloned().collect()).into_vovf(),
+ )),
_ => Err(()),
},
(ListIndexed, [_, l, r..]) => match &*l.as_whnf() {
@@ -193,7 +210,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
kts.insert("value".into(), t.clone());
Ok((
r,
- EmptyListLit(Value::from_valuef_untyped(RecordType(kts))),
+ EmptyListLit(Value::from_valuef_untyped(RecordType(kts)))
+ .into_vovf(),
))
}
NEListLit(xs) => {
@@ -211,7 +229,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
Value::from_valuef_untyped(RecordLit(kvs))
})
.collect();
- Ok((r, NEListLit(xs)))
+ Ok((r, NEListLit(xs).into_vovf()))
}
_ => Err(()),
},
@@ -219,7 +237,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
// fold/build fusion
ValueF::AppliedBuiltin(ListFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_whnf()))
+ Ok((r, args[1].clone().into_vovf()))
} else {
// Do we really need to handle this case ?
unimplemented!()
@@ -249,13 +267,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
}
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
- EmptyListLit(_) => Ok((r, nil.to_whnf())),
+ EmptyListLit(_) => Ok((r, nil.clone().into_vovf())),
NEListLit(xs) => {
- let mut v = nil.clone();
- for x in xs.iter().rev() {
- v = cons.clone().app(x.clone()).app(v).into_value_untyped();
+ let mut v = nil.clone().into_vovf();
+ for x in xs.iter().cloned().rev() {
+ v = cons.app(x).app(v.into_value_untyped());
}
- Ok((r, v.to_whnf()))
+ Ok((r, v))
}
_ => Err(()),
},
@@ -263,7 +281,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
// fold/build fusion
ValueF::AppliedBuiltin(OptionalFold, args) => {
if args.len() >= 2 {
- Ok((r, args[1].to_whnf()))
+ Ok((r, args[1].clone().into_vovf()))
} else {
// Do we really need to handle this case ?
unimplemented!()
@@ -285,7 +303,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
}
},
(OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
- EmptyOptionalLit(_) => Ok((r, nothing.to_whnf())),
+ EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())),
NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
_ => Err(()),
},
@@ -293,7 +311,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
// fold/build fusion
ValueF::AppliedBuiltin(NaturalFold, args) => {
if !args.is_empty() {
- Ok((r, args[0].to_whnf()))
+ Ok((r, args[0].clone().into_vovf()))
} else {
// Do we really need to handle this case ?
unimplemented!()
@@ -310,7 +328,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
)),
},
(NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
- NaturalLit(0) => Ok((r, zero.to_whnf())),
+ NaturalLit(0) => Ok((r, zero.clone().into_vovf())),
NaturalLit(n) => {
let fold = Value::from_builtin(NaturalFold)
.app(
@@ -335,23 +353,24 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
}
v
}
- Err(()) => AppliedBuiltin(b, args),
+ Err(()) => AppliedBuiltin(b, args).into_vovf(),
}
}
-pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
- let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Value, a: Value) -> VoVF {
+ let fallback =
+ |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a)).into_vovf();
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).to_whnf(),
+ ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(),
ValueF::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args)
}
ValueF::UnionConstructor(l, kts) => {
- ValueF::UnionLit(l.clone(), a, kts.clone())
+ ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf()
}
_ => {
drop(f_borrow);
@@ -465,6 +484,7 @@ where
enum Ret<'a> {
ValueF(ValueF),
Value(Value),
+ VoVF(VoVF),
ValueRef(&'a Value),
Expr(ExprF<Value, Normalized>),
}
@@ -597,7 +617,7 @@ fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
})
}
-pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
use ValueF::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -615,7 +635,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
- ExprF::App(v, a) => Ret::ValueF(v.app(a)),
+ ExprF::App(v, a) => Ret::VoVF(v.app(a)),
ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -737,7 +757,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => Ret::ValueF(h.app(v.clone())),
+ Some(h) => Ret::VoVF(h.app(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -754,22 +774,23 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
};
match ret {
- Ret::ValueF(v) => v,
- Ret::Value(th) => th.as_whnf().clone(),
- Ret::ValueRef(th) => th.as_whnf().clone(),
- Ret::Expr(expr) => ValueF::PartialExpr(expr),
+ Ret::ValueF(v) => v.into_vovf(),
+ Ret::Value(v) => v.into_vovf(),
+ Ret::VoVF(v) => v,
+ Ret::ValueRef(v) => v.clone().into_vovf(),
+ Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf(),
}
}
/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+pub(crate) fn normalize_whnf(v: ValueF) -> VoVF {
match v {
ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
ValueF::PartialExpr(e) => normalize_one_layer(e),
ValueF::TextLit(elts) => {
- ValueF::TextLit(squash_textlit(elts.into_iter()))
+ ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf()
}
// All other cases are already in WHNF
- v => v,
+ v => v.into_vovf(),
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 440d694..996c26c 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -455,11 +455,11 @@ fn type_last_layer(
return mkerr(InvalidListType(t.into_owned()));
}
- RetTypeOnly(Value::from_valuef_and_type(
+ RetTypeOnly(
ValueF::from_builtin(dhall_syntax::Builtin::List)
- .app(t.into_owned()),
- Value::from_const(Type),
- ))
+ .app(t.into_owned())
+ .into_value_simple_type(),
+ )
}
SomeLit(x) => {
let t = x.get_type()?.into_owned();
@@ -467,10 +467,11 @@ fn type_last_layer(
return mkerr(InvalidOptionalType(t));
}
- RetTypeOnly(Value::from_valuef_and_type(
- ValueF::from_builtin(dhall_syntax::Builtin::Optional).app(t),
- Value::from_const(Type),
- ))
+ RetTypeOnly(
+ Value::from_builtin(dhall_syntax::Builtin::Optional)
+ .app(t)
+ .into_value_simple_type(),
+ )
}
RecordType(kts) => RetWhole(tck_record_type(
ctx,
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index 4171fab..e2449de 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -169,12 +169,16 @@ pub mod value {
}
pub(crate) fn make_optional_type(t: Value) -> Self {
Self::make_simple_type(
- DhallValueF::from_builtin(Builtin::Optional).app(t.to_value()),
+ DhallValueF::from_builtin(Builtin::Optional)
+ .app(t.to_value())
+ .into_whnf(),
)
}
pub(crate) fn make_list_type(t: Value) -> Self {
Self::make_simple_type(
- DhallValueF::from_builtin(Builtin::List).app(t.to_value()),
+ DhallValueF::from_builtin(Builtin::List)
+ .app(t.to_value())
+ .into_whnf(),
)
}
// Made public for the StaticType derive macro
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-29 09:49:34 +0000