summaryrefslogtreecommitdiff
path: root/dhall/src/phase
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/phase')
-rw-r--r--dhall/src/phase/normalize.rs46
1 files changed, 24 insertions, 22 deletions
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,
}
}