From 906cbf5fc4c3bee65f24df1604497e33c6a20833 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:52:59 +0200 Subject: Remove now unnecessary VoVF enum --- dhall/src/core/value.rs | 95 +++++++++++++------------------------------- dhall/src/core/valuef.rs | 10 +---- dhall/src/phase/normalize.rs | 46 +++++++++++---------- 3 files changed, 53 insertions(+), 98 deletions(-) (limited to 'dhall') 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>); -/// 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 { @@ -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 { Some(Value(self.0.shift(delta, var)?)) @@ -324,6 +282,7 @@ impl Subst 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 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, _ty: &Value) -> VoVF { +pub(crate) fn apply_builtin( + b: Builtin, + args: Vec, + ty: &Value, +) -> ValueF { use dhall_syntax::Builtin::*; use ValueF::*; @@ -370,38 +374,36 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec, _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, 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, } } -- cgit v1.2.3