summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2019-04-18 22:20:40 +0200
committerNadrieril2019-04-18 23:24:58 +0200
commit0682a84eadc383e1d5747576298c9160737e0e99 (patch)
treecdc1dabca561c77fc7cf1ad8975eef8ee71c5166 /dhall/src
parent486a26eb7cea0c99818fde2c3fd933f7aca40b52 (diff)
Label is redundant in EnvItem::Skip
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/normalize.rs52
-rw-r--r--dhall/src/typecheck.rs5
2 files changed, 27 insertions, 30 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 4dc5156..7a9ca2f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -216,34 +216,10 @@ where
Continue(ExprF::App(ret, rest))
}
-// Small enum to help with being DRY
-enum WhatNext<'a, N, E> {
- // Recurse on this expression
- Continue(Expr<N, E>),
- // The following expression is the normal form
- Done(Expr<N, E>),
- DoneRef(&'a Expr<N, E>),
- DoneSub(SubExpr<N, E>),
- DoneRefSub(&'a SubExpr<N, E>),
- // The current expression is already in normal form
- DoneAsIs,
-}
-
#[derive(Debug, Clone)]
enum EnvItem {
Expr(SubExpr<X, X>),
- Skip(Label, usize),
-}
-
-impl EnvItem {
- fn shift0(&self, delta: isize, label: &Label) -> Self {
- use EnvItem::*;
- match self {
- Expr(e) => Expr(shift0(delta, label, e)),
- Skip(l, n) if l == label => Skip(l.clone(), *n + 1),
- Skip(l, n) => Skip(l.clone(), *n),
- }
- }
+ Skip(usize),
}
struct NormalizationContext(Context<Label, EnvItem>);
@@ -258,20 +234,40 @@ impl NormalizationContext {
fn skip(&self, x: &Label) -> NormalizationContext {
NormalizationContext(
self.0
- .map(|e| e.shift0(1, x))
- .insert(x.clone(), EnvItem::Skip(x.clone(), 0)),
+ .map(|l, e| {
+ use EnvItem::*;
+ match e {
+ Expr(e) => Expr(shift0(1, x, e)),
+ Skip(n) if l == x => Skip(*n + 1),
+ Skip(n) => Skip(*n),
+ }
+ })
+ .insert(x.clone(), EnvItem::Skip(0)),
)
}
fn lookup(&self, var: &V<Label>) -> SubExpr<X, X> {
let V(x, n) = var;
match self.0.lookup(x, *n) {
Some(EnvItem::Expr(e)) => e.clone(),
- Some(EnvItem::Skip(_, m)) => rc(ExprF::Var(V(x.clone(), *m))),
+ Some(EnvItem::Skip(m)) => rc(ExprF::Var(V(x.clone(), *m))),
None => rc(ExprF::Var(V(x.clone(), *n))),
}
}
}
+// Small enum to help with being DRY
+enum WhatNext<'a, N, E> {
+ // Recurse on this expression
+ Continue(Expr<N, E>),
+ // The following expression is the normal form
+ Done(Expr<N, E>),
+ DoneRef(&'a Expr<N, E>),
+ DoneSub(SubExpr<N, E>),
+ DoneRefSub(&'a SubExpr<N, E>),
+ // The current expression is already in normal form
+ DoneAsIs,
+}
+
fn normalize_value(
ctx: &NormalizationContext,
expr: SubExpr<X, Normalized<'static>>,
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 186384d..65128cd 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -378,7 +378,8 @@ fn type_with(
let ret = match e.as_ref() {
Lam(x, t, b) => {
let t = mktype(ctx, t.clone())?;
- let ctx2 = ctx.insert(x.clone(), t.clone()).map(|e| e.shift0(1, x));
+ let ctx2 =
+ ctx.insert(x.clone(), t.clone()).map(|_, e| e.shift0(1, x));
let b = type_with(&ctx2, b.clone())?;
Ok(RetExpr(Pi(
x.clone(),
@@ -394,7 +395,7 @@ fn type_with(
);
let ctx2 =
- ctx.insert(x.clone(), ta.clone()).map(|e| e.shift0(1, x));
+ ctx.insert(x.clone(), ta.clone()).map(|_, e| e.shift0(1, x));
let tb = type_with(&ctx2, tb.clone())?;
let kB = ensure_is_const!(
&tb.get_type()?,