summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-18 19:34:38 +0200
committerNadrieril2019-04-18 19:34:38 +0200
commit588127bf4105d8d4629304521abc3d992326a63a (patch)
tree57c8c0255ed21cba0f6f6229e4207d6d6582175c
parentf4a50a5da10eb2de1d7cf00ad6f6765605da366d (diff)
subst_shift in a single pass
-rw-r--r--dhall/src/typecheck.rs17
-rw-r--r--dhall_core/src/context.rs14
-rw-r--r--dhall_core/src/core.rs62
3 files changed, 78 insertions, 15 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 5aaeb08..186384d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -44,9 +44,9 @@ impl<'a> Normalized<'a> {
fn unroll_ref(&self) -> &Expr<X, X> {
self.as_expr().as_ref()
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
// shift the type too ?
- Normalized(shift(delta, var, &self.0), self.1.clone(), self.2)
+ Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2)
}
}
impl Normalized<'static> {
@@ -86,10 +86,10 @@ impl<'a> Type<'a> {
Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
}
}
- fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ fn shift0(&self, delta: isize, label: &Label) -> Self {
use TypeInternal::*;
Type(match &self.0 {
- Expr(e) => Expr(Box::new(e.shift(delta, var))),
+ Expr(e) => Expr(Box::new(e.shift0(delta, label))),
Const(c) => Const(*c),
SuperType => SuperType,
})
@@ -378,9 +378,7 @@ 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.shift(1, &V(x.clone(), 0)));
+ 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(),
@@ -395,9 +393,8 @@ fn type_with(
mkerr(InvalidInputType(ta.into_normalized()?)),
);
- let ctx2 = ctx
- .insert(x.clone(), ta.clone())
- .map(|e| e.shift(1, &V(x.clone(), 0)));
+ let ctx2 =
+ 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 877843d..b500226 100644
--- a/dhall_core/src/context.rs
+++ b/dhall_core/src/context.rs
@@ -43,6 +43,20 @@ impl<K: Hash + Eq + Clone, T> Context<K, T> {
.collect(),
)
}
+
+ pub fn lookup_all<'a>(&'a self, k: &K) -> impl Iterator<Item = &T> {
+ self.0.get(k).into_iter().flat_map(|v| v.iter())
+ }
+
+ pub fn iter<'a>(&'a self) -> impl Iterator<Item = (&K, &T)> {
+ self.0
+ .iter()
+ .flat_map(|(k, vs)| vs.iter().map(move |v| (k, v)))
+ }
+
+ pub fn iter_keys<'a>(&'a self) -> impl Iterator<Item = (&K, &Vec<T>)> {
+ self.0.iter()
+ }
}
impl<K: Hash + Eq + Clone, T: Clone> Context<K, T> {
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index aeb6f23..56ab66c 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -1,7 +1,9 @@
#![allow(non_snake_case)]
use std::collections::BTreeMap;
+use std::collections::HashMap;
use std::rc::Rc;
+use crate::context::Context;
use crate::visitor;
use crate::*;
@@ -486,6 +488,7 @@ fn shift_var(delta: isize, var: &V<Label>, in_expr: &V<Label>) -> V<Label> {
/// capture by shifting variable indices
/// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
/// for details
+///
pub fn shift<N, E>(
delta: isize,
var: &V<Label>,
@@ -505,6 +508,41 @@ pub fn shift<N, E>(
}
}
+pub fn shift0<N, E>(
+ delta: isize,
+ label: &Label,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
+ shift(delta, &V(label.clone(), 0), in_expr)
+}
+
+fn shift0_multiple<N, E>(
+ deltas: &HashMap<Label, isize>,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
+ shift0_multiple_inner(&Context::new(), deltas, in_expr)
+}
+
+fn shift0_multiple_inner<N, E>(
+ ctx: &Context<Label, ()>,
+ deltas: &HashMap<Label, isize>,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
+ use crate::ExprF::*;
+ match in_expr.as_ref() {
+ Var(V(y, m)) if ctx.lookup(y, *m).is_none() => {
+ let delta = deltas.get(y).unwrap_or(&0);
+ rc(Var(V(y.clone(), add_ui(*m, *delta))))
+ }
+ _ => in_expr.map_subexprs_with_special_handling_of_binders(
+ |e| shift0_multiple_inner(ctx, deltas, e),
+ |l: &Label, e| {
+ shift0_multiple_inner(&ctx.insert(l.clone(), ()), deltas, e)
+ },
+ ),
+ }
+}
+
/// Substitute all occurrences of a variable with an expression, and
/// removes the variable from the environment by shifting the indices
/// of other variables appropriately.
@@ -518,15 +556,29 @@ pub fn subst_shift<N, E>(
value: &SubExpr<N, E>,
in_expr: &SubExpr<N, E>,
) -> SubExpr<N, E> {
+ subst_shift_inner(&HashMap::new(), var, value, in_expr)
+}
+
+fn subst_shift_inner<N, E>(
+ ctx: &HashMap<Label, isize>,
+ var: &V<Label>,
+ value: &SubExpr<N, E>,
+ in_expr: &SubExpr<N, E>,
+) -> SubExpr<N, E> {
use crate::ExprF::*;
+ let V(x, n) = var;
+ let dn = ctx.get(x).unwrap_or(&0);
+ let actual_var = V(x.clone(), add_ui(*n, *dn));
match in_expr.as_ref() {
- Var(v) if v == var => SubExpr::clone(value),
- Var(v) => rc(Var(shift_var(-1, var, v))),
+ Var(v) if v == &actual_var => shift0_multiple(ctx, value),
+ Var(v) => rc(Var(shift_var(-1, &actual_var, v))),
_ => in_expr.map_subexprs_with_special_handling_of_binders(
- |e| subst_shift(var, &value, e),
+ |e| subst_shift_inner(ctx, var, value, e),
|l: &Label, e| {
- let vl = V(l.clone(), 0);
- subst_shift(&shift_var(1, &vl, var), &shift(1, &vl, value), e)
+ let mut ctx = ctx.clone();
+ let count = ctx.entry(l.clone()).or_insert(0);
+ *count += 1;
+ subst_shift_inner(&ctx, var, value, e)
},
),
}