diff options
| -rw-r--r-- | dhall/src/normalize.rs | 52 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 5 | ||||
| -rw-r--r-- | dhall_core/src/context.rs | 6 |
3 files changed, 31 insertions, 32 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()?, diff --git a/dhall_core/src/context.rs b/dhall_core/src/context.rs index 91eec69..55bfff5 100644 --- a/dhall_core/src/context.rs +++ b/dhall_core/src/context.rs @@ -41,11 +41,13 @@ impl<K: Hash + Eq + Clone, T> Context<K, T> { }) } - pub fn map<U, F: Fn(&T) -> U>(&self, f: F) -> Context<K, U> { + pub fn map<U, F: Fn(&K, &T) -> U>(&self, f: F) -> Context<K, U> { Context( self.0 .iter() - .map(|(k, v)| ((*k).clone(), v.iter().map(&f).collect())) + .map(|(k, vs)| { + ((*k).clone(), vs.iter().map(|v| f(k, v)).collect()) + }) .collect(), ) } |