summaryrefslogtreecommitdiff
path: root/dhall/src/normalize.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/normalize.rs')
-rw-r--r--dhall/src/normalize.rs185
1 files changed, 173 insertions, 12 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 88a55a1..dd9474d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -25,9 +25,9 @@ impl<'a> Typed<'a> {
/// leave ill-typed sub-expressions unevaluated.
///
pub fn normalize(self) -> Normalized<'a> {
- self.normalize_whnf().normalize()
+ self.partially_normalize().normalize()
}
- pub(crate) fn normalize_whnf(self) -> PartiallyNormalized<'a> {
+ pub(crate) fn partially_normalize(self) -> PartiallyNormalized<'a> {
PartiallyNormalized(
normalize_whnf(
NormalizationContext::from_typecheck_ctx(&self.2),
@@ -61,6 +61,20 @@ impl<'a> PartiallyNormalized<'a> {
self.2,
)
}
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &PartiallyNormalized<'static>,
+ ) -> Self {
+ PartiallyNormalized(
+ self.0.subst_shift(var, val),
+ self.1.as_ref().map(|x| x.subst_shift(var, val)),
+ self.2,
+ )
+ }
+ pub(crate) fn into_whnf(self) -> WHNF {
+ self.0
+ }
}
fn shift_mut<N, E>(delta: isize, var: &V<Label>, in_expr: &mut SubExpr<N, E>) {
@@ -273,6 +287,18 @@ impl EnvItem {
Skip(var) => Skip(var.shift0(delta, x)),
}
}
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &PartiallyNormalized<'static>,
+ ) -> Self {
+ use EnvItem::*;
+ match self {
+ Expr(e) => Expr(e.subst_shift(var, val)),
+ Skip(v) if v == var => Expr(val.clone().into_whnf()),
+ Skip(v) => Skip(v.shift(-1, var)),
+ }
+ }
}
#[derive(Debug, Clone)]
@@ -298,10 +324,8 @@ impl NormalizationContext {
let V(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Expr(e)) => e.clone(),
- Some(EnvItem::Skip(newvar)) => {
- WHNF::Expr(rc(ExprF::Var(newvar.clone())))
- }
- None => WHNF::Expr(rc(ExprF::Var(var.clone()))),
+ Some(EnvItem::Skip(newvar)) => WHNF::Var(newvar.clone()),
+ None => WHNF::Var(var.clone()),
}
}
fn from_typecheck_ctx(tc_ctx: &crate::typecheck::TypecheckContext) -> Self {
@@ -321,6 +345,16 @@ impl NormalizationContext {
}
NormalizationContext(Rc::new(ctx))
}
+
+ fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &PartiallyNormalized<'static>,
+ ) -> Self {
+ NormalizationContext(Rc::new(
+ self.0.map(|_, e| e.subst_shift(var, val)),
+ ))
+ }
}
/// A semantic value. This is partially redundant with `dhall_core::Expr`, on purpose. `Expr` should
@@ -347,6 +381,7 @@ pub(crate) enum WHNF {
NaturalSuccClosure,
Pi(Label, TypeThunk, TypeThunk),
+ Var(V<Label>),
Const(Const),
BoolLit(bool),
NaturalLit(Natural),
@@ -397,6 +432,8 @@ impl WHNF {
WHNF::ListConsClosure(n, Some(v)) => {
let v = v.normalize().normalize_to_expr();
let a = n.normalize().normalize_to_expr();
+ // Avoid accidental capture of the new `xs` variable
+ let v = shift0(1, &"xs".into(), &v);
dhall::subexpr!(λ(xs : List a) -> [ v ] # xs)
}
WHNF::NaturalSuccClosure => {
@@ -407,6 +444,7 @@ impl WHNF {
t.normalize().normalize_to_expr(),
e.normalize().normalize_to_expr(),
)),
+ WHNF::Var(v) => rc(ExprF::Var(v)),
WHNF::Const(c) => rc(ExprF::Const(c)),
WHNF::BoolLit(b) => rc(ExprF::BoolLit(b)),
WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
@@ -539,6 +577,9 @@ impl WHNF {
fn shift(&mut self, delta: isize, var: &V<Label>) {
match self {
+ WHNF::Var(v) => {
+ std::mem::replace(v, v.shift(delta, var));
+ }
WHNF::NaturalSuccClosure
| WHNF::Const(_)
| WHNF::BoolLit(_)
@@ -609,6 +650,103 @@ impl WHNF {
WHNF::Expr(e) => shift_mut(delta, var, e),
}
}
+
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &PartiallyNormalized<'static>,
+ ) -> Self {
+ match self {
+ WHNF::Lam(x, t, (ctx, e)) => WHNF::Lam(
+ x.clone(),
+ t.subst_shift(var, val),
+ (ctx.subst_shift(var, val), e.clone()),
+ ),
+ WHNF::AppliedBuiltin(b, args) => WHNF::AppliedBuiltin(
+ *b,
+ args.iter().map(|v| v.subst_shift(var, val)).collect(),
+ ),
+ WHNF::NaturalSuccClosure => WHNF::NaturalSuccClosure,
+ WHNF::OptionalSomeClosure(tth) => {
+ WHNF::OptionalSomeClosure(tth.subst_shift(var, val))
+ }
+ WHNF::ListConsClosure(t, v) => WHNF::ListConsClosure(
+ t.subst_shift(var, val),
+ v.as_ref().map(|v| v.subst_shift(var, val)),
+ ),
+ WHNF::Pi(x, t, e) => WHNF::Pi(
+ x.clone(),
+ t.subst_shift(var, val),
+ e.subst_shift(&var.shift0(1, x), val),
+ ),
+ WHNF::Var(v) if v == var => val.clone().into_whnf(),
+ WHNF::Var(v) => WHNF::Var(v.shift(-1, var)),
+ WHNF::Const(c) => WHNF::Const(*c),
+ WHNF::BoolLit(b) => WHNF::BoolLit(*b),
+ WHNF::NaturalLit(n) => WHNF::NaturalLit(*n),
+ WHNF::IntegerLit(n) => WHNF::IntegerLit(*n),
+ WHNF::EmptyOptionalLit(tth) => {
+ WHNF::EmptyOptionalLit(tth.subst_shift(var, val))
+ }
+ WHNF::NEOptionalLit(th) => {
+ WHNF::NEOptionalLit(th.subst_shift(var, val))
+ }
+ WHNF::EmptyListLit(tth) => {
+ WHNF::EmptyListLit(tth.subst_shift(var, val))
+ }
+ WHNF::NEListLit(elts) => WHNF::NEListLit(
+ elts.iter().map(|v| v.subst_shift(var, val)).collect(),
+ ),
+ WHNF::RecordLit(kvs) => WHNF::RecordLit(
+ kvs.iter()
+ .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+ .collect(),
+ ),
+ WHNF::RecordType(kvs) => WHNF::RecordType(
+ kvs.iter()
+ .map(|(k, v)| (k.clone(), v.subst_shift(var, val)))
+ .collect(),
+ ),
+ WHNF::UnionType(kts) => WHNF::UnionType(
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+ })
+ .collect(),
+ ),
+ WHNF::UnionConstructor(x, kts) => WHNF::UnionConstructor(
+ x.clone(),
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+ })
+ .collect(),
+ ),
+ WHNF::UnionLit(x, v, kts) => WHNF::UnionLit(
+ x.clone(),
+ v.subst_shift(var, val),
+ kts.iter()
+ .map(|(k, v)| {
+ (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val)))
+ })
+ .collect(),
+ ),
+ WHNF::TextLit(elts) => WHNF::TextLit(
+ elts.iter()
+ .map(|contents| {
+ use InterpolatedTextContents::{Expr, Text};
+ match contents {
+ Expr(th) => Expr(th.subst_shift(var, val)),
+ Text(s) => Text(s.clone()),
+ }
+ })
+ .collect(),
+ ),
+ WHNF::Expr(e) => WHNF::Expr(
+ e.subst_shift(var, &val.clone().normalize().as_expr()),
+ ),
+ }
+ }
}
/// Contains either a (partially) normalized value or a
@@ -641,6 +779,21 @@ impl Thunk {
Thunk::Unnormalized(_, e) => shift_mut(delta, var, e),
}
}
+
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &PartiallyNormalized<'static>,
+ ) -> Self {
+ match self {
+ Thunk::Normalized(v) => {
+ Thunk::Normalized(Box::new(v.subst_shift(var, val)))
+ }
+ Thunk::Unnormalized(ctx, e) => {
+ Thunk::Unnormalized(ctx.subst_shift(var, val), e.clone())
+ }
+ }
+ }
}
/// A thunk in type position.
@@ -667,14 +820,11 @@ impl TypeThunk {
TypeThunk::from_thunk(Thunk::from_whnf(v))
}
- fn normalize(self) -> WHNF {
+ pub(crate) fn normalize(self) -> WHNF {
match self {
TypeThunk::Thunk(th) => th.normalize(),
- // TODO: let's hope for the best with the unwraps
- TypeThunk::Type(t) => normalize_whnf(
- NormalizationContext::new(),
- t.into_normalized().unwrap().0.embed_absurd(),
- ),
+ // TODO: let's hope for the best with the unwrap
+ TypeThunk::Type(t) => t.partially_normalize().unwrap().into_whnf(),
}
}
@@ -687,6 +837,17 @@ impl TypeThunk {
}
}
}
+
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &PartiallyNormalized<'static>,
+ ) -> Self {
+ match self {
+ TypeThunk::Thunk(th) => TypeThunk::Thunk(th.subst_shift(var, val)),
+ TypeThunk::Type(t) => TypeThunk::Type(t.subst_shift(var, val)),
+ }
+ }
}
/// Reduces the imput expression to WHNF. See doc on `WHNF` for details.
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 22:41:14 +0000