summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/value.rs95
-rw-r--r--dhall/src/core/valuef.rs10
-rw-r--r--dhall/src/phase/normalize.rs46
3 files changed, 53 insertions, 98 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 2554da1..13f8e59 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -44,15 +44,6 @@ struct ValueInternal {
#[derive(Clone)]
pub(crate) 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.
-#[derive(Debug, Clone)]
-pub(crate) enum VoVF {
- Value(Value),
- ValueF { val: ValueF, form: Form },
-}
-
impl ValueInternal {
fn into_value(self) -> Value {
Value(Rc::new(RefCell::new(self)))
@@ -76,15 +67,11 @@ impl ValueInternal {
value: ValueF::Const(Const::Sort),
ty: None,
},
- (Unevaled, Some(ty)) => {
- let new_value =
- normalize_whnf(vint.value, &ty).into_whnf(&ty);
- ValueInternal {
- form: WHNF,
- value: new_value,
- ty: vint.ty,
- }
- }
+ (Unevaled, Some(ty)) => ValueInternal {
+ form: WHNF,
+ value: normalize_whnf(vint.value, &ty),
+ ty: vint.ty,
+ },
// Already in WHNF
(WHNF, _) | (NF, _) => vint,
},
@@ -135,6 +122,9 @@ impl Value {
pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value {
Value::new(v, Unevaled, t)
}
+ pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value {
+ Value::new(v, WHNF, t)
+ }
pub(crate) fn from_const(c: Const) -> Self {
const_to_value(c)
}
@@ -182,16 +172,22 @@ impl Value {
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
self.as_whnf().normalize_to_expr_maybe_alpha(true)
}
- /// TODO: cloning a valuef can often be avoided
- pub(crate) fn to_whnf(&self) -> ValueF {
+ pub(crate) fn to_whnf_ignore_type(&self) -> ValueF {
self.as_whnf().clone()
}
+ /// Before discarding type information, check that it matches the expected return type.
+ pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF {
+ let self_ty = self.get_type().ok();
+ debug_assert_eq!(
+ Some(ty),
+ self_ty.as_ref(),
+ "The value returned from normalization doesn't have the expected type."
+ );
+ self.to_whnf_ignore_type()
+ }
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)) {
@@ -239,16 +235,14 @@ impl Value {
}
pub(crate) fn app(&self, v: Value) -> Value {
- let t = self.get_type_not_sort();
- let vovf = apply_any(self.clone(), v.clone(), &t);
- let t_borrow = t.as_whnf();
- match &*t_borrow {
- ValueF::Pi(x, _, e) => {
- let t = e.subst_shift(&x.into(), &v);
- vovf.into_value_with_type(t)
- }
+ let body_t = match &*self.get_type_not_sort().as_whnf() {
+ ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v),
_ => unreachable!("Internal type error"),
- }
+ };
+ Value::from_valuef_and_type_whnf(
+ apply_any(self.clone(), v, &body_t),
+ body_t,
+ )
}
pub(crate) fn get_type(&self) -> Result<Value, TypeError> {
@@ -261,42 +255,6 @@ impl Value {
}
}
-impl VoVF {
- pub(crate) fn into_whnf(self, ty: &Value) -> ValueF {
- match self {
- VoVF::ValueF {
- val,
- form: Unevaled,
- } => normalize_whnf(val, ty).into_whnf(ty),
- // Already at lest in WHNF
- VoVF::ValueF { val, .. } => val,
- VoVF::Value(v) => {
- let v_ty = v.get_type().ok();
- debug_assert_eq!(
- Some(ty),
- v_ty.as_ref(),
- "The type recovered from normalization doesn't match the stored type."
- );
- v.to_whnf()
- }
- }
- }
- pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
- match self {
- VoVF::Value(v) => {
- let v_ty = v.get_type().ok();
- debug_assert_eq!(
- Some(&ty),
- v_ty.as_ref(),
- "The type recovered from normalization doesn't match the stored type."
- );
- v
- }
- VoVF::ValueF { val, form } => Value::new(val, form, ty),
- }
- }
-}
-
impl Shift for Value {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(Value(self.0.shift(delta, var)?))
@@ -324,6 +282,7 @@ impl Subst<Value> for ValueInternal {
ValueInternal {
// The resulting value may not stay in wnhf after substitution
form: Unevaled,
+ // TODO: check type info if self.value if Var(v) and v == var
value: self.value.subst_shift(var, val),
ty: self.ty.subst_shift(var, val),
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index 5638078..9ea2467 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::{Form, Value, VoVF};
+use crate::core::value::Value;
use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::phase::{Normalized, NormalizedSubExpr};
@@ -50,12 +50,6 @@ impl ValueF {
pub(crate) fn into_value_with_type(self, t: Value) -> Value {
Value::from_valuef_and_type(self, t)
}
- pub(crate) fn into_vovf_whnf(self) -> VoVF {
- VoVF::ValueF {
- val: self,
- form: Form::WHNF,
- }
- }
/// Convert the value to a fully normalized syntactic expression
pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr {
@@ -339,7 +333,7 @@ impl Subst<Value> for ValueF {
t.subst_shift(var, val),
e.subst_shift(&var.under_binder(x), &val.under_binder(x)),
),
- ValueF::Var(v) if v == var => val.to_whnf(),
+ ValueF::Var(v) if v == var => val.to_whnf_ignore_type(),
ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()),
ValueF::Const(c) => ValueF::Const(*c),
ValueF::BoolLit(b) => ValueF::BoolLit(*b),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 77f5023..82a378c 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -6,7 +6,7 @@ use dhall_syntax::{
NaiveDouble,
};
-use crate::core::value::{Value, VoVF};
+use crate::core::value::Value;
use crate::core::valuef::ValueF;
use crate::core::var::{AlphaLabel, Shift, Subst};
use crate::phase::Normalized;
@@ -71,7 +71,11 @@ macro_rules! make_closure {
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
+pub(crate) fn apply_builtin(
+ b: Builtin,
+ args: Vec<Value>,
+ ty: &Value,
+) -> ValueF {
use dhall_syntax::Builtin::*;
use ValueF::*;
@@ -370,38 +374,36 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>, _ty: &Value) -> VoVF {
_ => Ret::DoneAsIs,
};
match ret {
- Ret::ValueF(v) => v.into_vovf_whnf(),
- Ret::Value(v) => v.into_vovf(),
+ Ret::ValueF(v) => v,
+ Ret::Value(v) => v.to_whnf_check_type(ty),
Ret::ValueWithRemainingArgs(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(x);
}
- v.into_vovf()
+ v.to_whnf_check_type(ty)
}
- Ret::DoneAsIs => AppliedBuiltin(b, args).into_vovf_whnf(),
+ Ret::DoneAsIs => AppliedBuiltin(b, args),
}
}
-pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> VoVF {
- let fallback = |f: Value, a: Value| {
- ValueF::PartialExpr(ExprF::App(f, a)).into_vovf_whnf()
- };
-
+pub(crate) fn apply_any(f: Value, a: Value, ty: &Value) -> ValueF {
let f_borrow = f.as_whnf();
match &*f_borrow {
- ValueF::Lam(x, _, e) => e.subst_shift(&x.into(), &a).into_vovf(),
+ ValueF::Lam(x, _, e) => {
+ e.subst_shift(&x.into(), &a).to_whnf_check_type(ty)
+ }
ValueF::AppliedBuiltin(b, args) => {
use std::iter::once;
let args = args.iter().cloned().chain(once(a.clone())).collect();
apply_builtin(*b, args, ty)
}
ValueF::UnionConstructor(l, kts) => {
- ValueF::UnionLit(l.clone(), a, kts.clone()).into_vovf_whnf()
+ ValueF::UnionLit(l.clone(), a, kts.clone())
}
_ => {
drop(f_borrow);
- fallback(f, a)
+ ValueF::PartialExpr(ExprF::App(f, a))
}
}
}
@@ -609,7 +611,7 @@ fn apply_binop<'a>(
pub(crate) fn normalize_one_layer(
expr: ExprF<Value, Normalized>,
ty: &Value,
-) -> VoVF {
+) -> ValueF {
use ValueF::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit,
NEListLit, NEOptionalLit, NaturalLit, RecordLit, TextLit,
@@ -766,22 +768,22 @@ pub(crate) fn normalize_one_layer(
};
match ret {
- Ret::ValueF(v) => v.into_vovf_whnf(),
- Ret::Value(v) => v.into_vovf(),
- Ret::ValueRef(v) => v.clone().into_vovf(),
- Ret::Expr(expr) => ValueF::PartialExpr(expr).into_vovf_whnf(),
+ Ret::ValueF(v) => v,
+ Ret::Value(v) => v.to_whnf_check_type(ty),
+ Ret::ValueRef(v) => v.to_whnf_check_type(ty),
+ Ret::Expr(expr) => ValueF::PartialExpr(expr),
}
}
/// Normalize a ValueF into WHNF
-pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> VoVF {
+pub(crate) fn normalize_whnf(v: ValueF, ty: &Value) -> ValueF {
match v {
ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args, ty),
ValueF::PartialExpr(e) => normalize_one_layer(e, ty),
ValueF::TextLit(elts) => {
- ValueF::TextLit(squash_textlit(elts.into_iter())).into_vovf_whnf()
+ ValueF::TextLit(squash_textlit(elts.into_iter()))
}
// All other cases are already in WHNF
- v => v.into_vovf_whnf(),
+ v => v,
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 06:20:01 +0000