summaryrefslogtreecommitdiff
path: root/dhall_syntax/src
diff options
context:
space:
mode:
authorNadrieril2019-05-05 00:44:19 +0200
committerNadrieril2019-05-05 00:44:19 +0200
commit559df737c02cc534851ab6e11e930112b03c00ed (patch)
treeafcb15e7567275b0af228099e60e1a7adc50be57 /dhall_syntax/src
parent0e5c93c398645d39fceb98d054f1a7e67025b4fd (diff)
parent8e4182f26b20b28f60fb0c21b3e08e19314de9a0 (diff)
Merge branch 'alpha-normalization'
Diffstat (limited to 'dhall_syntax/src')
-rw-r--r--dhall_syntax/src/core.rs81
1 files changed, 0 insertions, 81 deletions
diff --git a/dhall_syntax/src/core.rs b/dhall_syntax/src/core.rs
index a186d19..7cdda64 100644
--- a/dhall_syntax/src/core.rs
+++ b/dhall_syntax/src/core.rs
@@ -1,9 +1,7 @@
#![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::*;
@@ -436,36 +434,6 @@ impl<N: Clone, E> SubExpr<N, E> {
)),
}
}
-
- /// `shift` is used by both normalization and type-checking to avoid variable
- /// capture by shifting variable indices
- /// See https://github.com/dhall-lang/dhall-lang/blob/master/standard/semantics.md#shift
- /// for details
- pub fn shift(&self, delta: isize, var: &V<Label>) -> Self {
- match self.as_ref() {
- ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(delta, var))),
- _ => self.map_subexprs_with_special_handling_of_binders(
- |e| e.shift(delta, var),
- |x: &Label, e| e.shift(delta, &var.shift(1, &x.into())),
- ),
- }
- }
-
- pub fn subst_shift(&self, var: &V<Label>, val: &Self) -> Self {
- match self.as_ref() {
- ExprF::Var(v) if v == var => val.clone(),
- ExprF::Var(v) => self.rewrap(ExprF::Var(v.shift(-1, var))),
- _ => self.map_subexprs_with_special_handling_of_binders(
- |e| e.subst_shift(var, val),
- |x: &Label, e| {
- e.subst_shift(
- &var.shift(1, &x.into()),
- &val.shift(1, &x.into()),
- )
- },
- ),
- }
- }
}
impl<N: Clone> SubExpr<N, X> {
@@ -512,52 +480,3 @@ impl<Label: PartialEq + Clone> V<Label> {
}
}
}
-
-/// `shift` is used by both normalization and type-checking to avoid variable
-/// 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>,
- in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
- N: Clone,
-{
- in_expr.shift(delta, var)
-}
-
-pub fn shift0_multiple<N, E>(
- deltas: &HashMap<Label, isize>,
- in_expr: &SubExpr<N, E>,
-) -> SubExpr<N, E>
-where
- N: Clone,
-{
- 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>
-where
- N: Clone,
-{
- 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);
- in_expr.rewrap(Var(V(y.clone(), add_ui(*m, *delta))))
- }
- _ => in_expr.map_subexprs_with_special_handling_of_binders(
- |e| shift0_multiple_inner(ctx, deltas, e),
- |x: &Label, e| {
- shift0_multiple_inner(&ctx.insert(x.clone(), ()), deltas, e)
- },
- ),
- }
-}