summaryrefslogtreecommitdiff
path: root/dhall_core/src/core.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall_core/src/core.rs')
-rw-r--r--dhall_core/src/core.rs502
1 files changed, 337 insertions, 165 deletions
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index afa3d3f..3d1b9f3 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -100,7 +100,7 @@ pub enum Const {
/// appear as a numeric suffix.
///
#[derive(Debug, Clone, PartialEq, Eq)]
-pub struct V(pub Label, pub usize);
+pub struct V<Label>(pub Label, pub usize);
// Definition order must match precedence order for
// pretty-printing to work correctly
@@ -170,45 +170,42 @@ pub type ParsedExpr = SubExpr<X, Import>;
pub type ResolvedExpr = SubExpr<X, X>;
pub type DhallExpr = ResolvedExpr;
-pub type SubExpr<Note, Embed> = Rc<Expr<Note, Embed>>;
+#[derive(Debug, PartialEq, Eq)]
+pub struct SubExpr<Note, Embed>(pub Rc<Expr<Note, Embed>>);
+
+pub type Expr<Note, Embed> = ExprF<SubExpr<Note, Embed>, Label, Note, Embed>;
/// Syntax tree for expressions
+// Having the recursion out of the enum definition enables writing
+// much more generic code and improves pattern-matching behind
+// smart pointers.
#[derive(Debug, Clone, PartialEq, Eq)]
-pub enum Expr<Note, Embed> {
+pub enum ExprF<SubExpr, Label, Note, Embed> {
/// `Const c ~ c`
Const(Const),
/// `Var (V x 0) ~ x`<br>
/// `Var (V x n) ~ x@n`
- Var(V),
+ Var(V<Label>),
/// `Lam x A b ~ λ(x : A) -> b`
- Lam(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
+ Lam(Label, SubExpr, SubExpr),
/// `Pi "_" A B ~ A -> B`
/// `Pi x A B ~ ∀(x : A) -> B`
- Pi(Label, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
+ Pi(Label, SubExpr, SubExpr),
/// `App f A ~ f A`
- App(SubExpr<Note, Embed>, Vec<SubExpr<Note, Embed>>),
+ App(SubExpr, Vec<SubExpr>),
/// `Let x Nothing r e ~ let x = r in e`
/// `Let x (Just t) r e ~ let x : t = r in e`
- Let(
- Label,
- Option<SubExpr<Note, Embed>>,
- SubExpr<Note, Embed>,
- SubExpr<Note, Embed>,
- ),
+ Let(Label, Option<SubExpr>, SubExpr, SubExpr),
/// `Annot x t ~ x : t`
- Annot(SubExpr<Note, Embed>, SubExpr<Note, Embed>),
+ Annot(SubExpr, SubExpr),
/// Built-in values
Builtin(Builtin),
// Binary operations
- BinOp(BinOp, SubExpr<Note, Embed>, SubExpr<Note, Embed>),
+ BinOp(BinOp, SubExpr, SubExpr),
/// `BoolLit b ~ b`
BoolLit(bool),
/// `BoolIf x y z ~ if x then y else z`
- BoolIf(
- SubExpr<Note, Embed>,
- SubExpr<Note, Embed>,
- SubExpr<Note, Embed>,
- ),
+ BoolIf(SubExpr, SubExpr, SubExpr),
/// `NaturalLit n ~ +n`
NaturalLit(Natural),
/// `IntegerLit n ~ n`
@@ -216,39 +213,31 @@ pub enum Expr<Note, Embed> {
/// `DoubleLit n ~ n`
DoubleLit(Double),
/// `TextLit t ~ t`
- TextLit(InterpolatedText<Note, Embed>),
+ TextLit(InterpolatedText<SubExpr>),
/// [] : List t`
- EmptyListLit(SubExpr<Note, Embed>),
+ EmptyListLit(SubExpr),
/// [x, y, z]
- NEListLit(Vec<SubExpr<Note, Embed>>),
+ NEListLit(Vec<SubExpr>),
/// None t
- EmptyOptionalLit(SubExpr<Note, Embed>),
+ EmptyOptionalLit(SubExpr),
/// Some e
- NEOptionalLit(SubExpr<Note, Embed>),
+ NEOptionalLit(SubExpr),
/// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
- RecordType(BTreeMap<Label, SubExpr<Note, Embed>>),
+ RecordType(BTreeMap<Label, SubExpr>),
/// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
- RecordLit(BTreeMap<Label, SubExpr<Note, Embed>>),
+ RecordLit(BTreeMap<Label, SubExpr>),
/// `Union [(k1, t1), (k2, t2)] ~ < k1 : t1, k2 : t2 >`
- UnionType(BTreeMap<Label, SubExpr<Note, Embed>>),
+ UnionType(BTreeMap<Label, SubExpr>),
/// `UnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1, k2 : t2, k3 : t3 >`
- UnionLit(
- Label,
- SubExpr<Note, Embed>,
- BTreeMap<Label, SubExpr<Note, Embed>>,
- ),
+ UnionLit(Label, SubExpr, BTreeMap<Label, SubExpr>),
/// `Merge x y t ~ merge x y : t`
- Merge(
- SubExpr<Note, Embed>,
- SubExpr<Note, Embed>,
- Option<SubExpr<Note, Embed>>,
- ),
+ Merge(SubExpr, SubExpr, Option<SubExpr>),
/// e.x
- Field(SubExpr<Note, Embed>, Label),
+ Field(SubExpr, Label),
/// e.{ x, y, z }
- Projection(SubExpr<Note, Embed>, Vec<Label>),
+ Projection(SubExpr, Vec<Label>),
/// Annotation on the AST. Unused for now but could hold e.g. file location information
- Note(Note, SubExpr<Note, Embed>),
+ Note(Note, SubExpr),
/// Embeds an import or the result of resolving the import
Embed(Embed),
}
@@ -270,13 +259,12 @@ impl<S, A> Expr<S, A> {
F3: FnOnce(&A) -> B,
F4: Fn(&Label) -> Label,
{
- map_subexpr(
- self,
+ self.map_ref(
|x| rc(map_expr(x.as_ref())),
+ |_, x| rc(map_expr(x.as_ref())),
map_note,
map_embed,
map_label,
- |_, x| rc(map_expr(x.as_ref())),
)
}
@@ -299,12 +287,21 @@ impl<S, A> Expr<S, A> {
let recurse = |e: &Self| -> Self { e.map_label(map_label) };
self.map_shallow(recurse, |x| x.clone(), |x| x.clone(), map_label)
}
+
+ #[inline(always)]
+ pub fn roll(&self) -> SubExpr<S, A>
+ where
+ S: Clone,
+ A: Clone,
+ {
+ rc(ExprF::clone(self))
+ }
}
impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> {
pub fn squash_embed(&self) -> Expr<S, A> {
match self {
- Expr::Embed(e) => e.clone(),
+ ExprF::Embed(e) => e.clone(),
e => e.map_shallow(
|e| e.squash_embed(),
|x| x.clone(),
@@ -315,20 +312,297 @@ impl<S: Clone, A: Clone> Expr<S, Expr<S, A>> {
}
}
+impl<SE, L, N, E> ExprF<SE, L, N, E> {
+ #[inline(always)]
+ pub fn as_ref(&self) -> ExprF<&SE, &L, &N, &E>
+ where
+ L: Ord,
+ {
+ fn opt<T>(x: &Option<T>) -> Option<&T> {
+ x.as_ref()
+ }
+ fn vec<T>(x: &Vec<T>) -> Vec<&T> {
+ x.iter().collect()
+ }
+ fn btmap<L: Ord, SE>(x: &BTreeMap<L, SE>) -> BTreeMap<&L, &SE> {
+ x.iter().collect()
+ }
+
+ use crate::ExprF::*;
+ match self {
+ Var(V(l, n)) => Var(V(l, *n)),
+ Lam(l, t, b) => Lam(l, t, b),
+ Pi(l, t, b) => Pi(l, t, b),
+ Let(l, t, a, b) => Let(l, opt(t), a, b),
+ App(f, args) => App(f, vec(args)),
+ Annot(x, t) => Annot(x, t),
+ Const(k) => Const(*k),
+ Builtin(v) => Builtin(*v),
+ BoolLit(b) => BoolLit(*b),
+ NaturalLit(n) => NaturalLit(*n),
+ IntegerLit(n) => IntegerLit(*n),
+ DoubleLit(n) => DoubleLit(*n),
+ TextLit(t) => TextLit(t.as_ref()),
+ BinOp(o, x, y) => BinOp(*o, x, y),
+ BoolIf(b, t, f) => BoolIf(b, t, f),
+ EmptyListLit(t) => EmptyListLit(t),
+ NEListLit(es) => NEListLit(vec(es)),
+ EmptyOptionalLit(t) => EmptyOptionalLit(t),
+ NEOptionalLit(e) => NEOptionalLit(e),
+ RecordType(kts) => RecordType(btmap(kts)),
+ RecordLit(kvs) => RecordLit(btmap(kvs)),
+ UnionType(kts) => UnionType(btmap(kts)),
+ UnionLit(k, v, kvs) => UnionLit(k, v, btmap(kvs)),
+ Merge(x, y, t) => Merge(x, y, opt(t)),
+ Field(e, l) => Field(e, l),
+ Projection(e, ls) => Projection(e, vec(ls)),
+ Note(n, e) => Note(n, e),
+ Embed(a) => Embed(a),
+ }
+ }
+
+ #[inline(always)]
+ pub fn map<SE2, L2, N2, E2, F1, F2, F3, F4, F5>(
+ self,
+ map_subexpr: F1,
+ map_under_binder: F2,
+ map_note: F3,
+ map_embed: F4,
+ mut map_label: F5,
+ ) -> ExprF<SE2, L2, N2, E2>
+ where
+ L: Ord,
+ L2: Ord,
+ F1: FnMut(SE) -> SE2,
+ F2: FnOnce(&L, SE) -> SE2,
+ F3: FnOnce(N) -> N2,
+ F4: FnOnce(E) -> E2,
+ F5: FnMut(L) -> L2,
+ {
+ let mut map = map_subexpr;
+ fn vec<T, U, F: FnMut(T) -> U>(x: Vec<T>, f: F) -> Vec<U> {
+ x.into_iter().map(f).collect()
+ }
+ fn btmap<K, L, T, U, FK, FV>(
+ x: BTreeMap<K, T>,
+ mut fk: FK,
+ mut fv: FV,
+ ) -> BTreeMap<L, U>
+ where
+ K: Ord,
+ L: Ord,
+ FK: FnMut(K) -> L,
+ FV: FnMut(T) -> U,
+ {
+ x.into_iter().map(|(k, v)| (fk(k), fv(v))).collect()
+ }
+
+ use crate::ExprF::*;
+ match self {
+ Var(V(l, n)) => Var(V(map_label(l), n)),
+ Lam(l, t, b) => {
+ let b = map_under_binder(&l, b);
+ Lam(map_label(l), map(t), b)
+ }
+ Pi(l, t, b) => {
+ let b = map_under_binder(&l, b);
+ Pi(map_label(l), map(t), b)
+ }
+ Let(l, t, a, b) => {
+ let b = map_under_binder(&l, b);
+ Let(map_label(l), t.map(&mut map), map(a), b)
+ }
+ App(f, args) => App(map(f), vec(args, map)),
+ Annot(x, t) => Annot(map(x), map(t)),
+ Const(k) => Const(k),
+ Builtin(v) => Builtin(v),
+ BoolLit(b) => BoolLit(b),
+ NaturalLit(n) => NaturalLit(n),
+ IntegerLit(n) => IntegerLit(n),
+ DoubleLit(n) => DoubleLit(n),
+ TextLit(t) => TextLit(t.map(map)),
+ BinOp(o, x, y) => BinOp(o, map(x), map(y)),
+ BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)),
+ EmptyListLit(t) => EmptyListLit(map(t)),
+ NEListLit(es) => NEListLit(vec(es, map)),
+ EmptyOptionalLit(t) => EmptyOptionalLit(map(t)),
+ NEOptionalLit(e) => NEOptionalLit(map(e)),
+ RecordType(kts) => RecordType(btmap(kts, map_label, map)),
+ RecordLit(kvs) => RecordLit(btmap(kvs, map_label, map)),
+ UnionType(kts) => UnionType(btmap(kts, map_label, map)),
+ UnionLit(k, v, kvs) => {
+ UnionLit(map_label(k), map(v), btmap(kvs, map_label, map))
+ }
+ Merge(x, y, t) => Merge(map(x), map(y), t.map(map)),
+ Field(e, l) => Field(map(e), map_label(l)),
+ Projection(e, ls) => Projection(map(e), vec(ls, map_label)),
+ Note(n, e) => Note(map_note(n), map(e)),
+ Embed(a) => Embed(map_embed(a)),
+ }
+ }
+
+ #[inline(always)]
+ pub fn map_ref<'a, SE2, L2, N2, E2, F1, F2, F3, F4, F5>(
+ &'a self,
+ map_subexpr: F1,
+ map_under_binder: F2,
+ map_note: F3,
+ map_embed: F4,
+ map_label: F5,
+ ) -> ExprF<SE2, L2, N2, E2>
+ where
+ L: Ord,
+ L2: Ord,
+ F1: FnMut(&'a SE) -> SE2,
+ F2: FnOnce(&'a L, &'a SE) -> SE2,
+ F3: FnOnce(&'a N) -> N2,
+ F4: FnOnce(&'a E) -> E2,
+ F5: FnMut(&'a L) -> L2,
+ {
+ // Not optimal: reallocates all the Vecs and BTreeMaps for nothing.
+ self.as_ref().map(
+ map_subexpr,
+ |l, e| map_under_binder(*l, e),
+ map_note,
+ map_embed,
+ map_label,
+ )
+ }
+
+ #[inline(always)]
+ pub fn map_ref_simple<'a, SE2, F1>(
+ &'a self,
+ map_subexpr: F1,
+ ) -> ExprF<SE2, L, N, E>
+ where
+ L: Ord,
+ L: Clone,
+ N: Clone,
+ E: Clone,
+ F1: Fn(&'a SE) -> SE2,
+ {
+ self.map_ref(
+ &map_subexpr,
+ |_, e| map_subexpr(e),
+ N::clone,
+ E::clone,
+ L::clone,
+ )
+ }
+
+ // #[inline(always)]
+ // pub fn zip<SE2, L2, N2, E2>(
+ // self,
+ // other: ExprF<SE2, L2, N2, E2>
+ // ) -> Option<ExprF<(SE, SE2), (L, L2), (N, N2), (E, E2)>>
+ // where
+ // L: Ord,
+ // L2: Ord,
+ // {
+ // // What to do with Var ?
+ // use crate::ExprF::*;
+ // match (self, other) {
+ // // Var(V(l, n)) => Var(V(map_label(l), n)),
+ // // Lam(l, t, b) => {
+ // // Pi(l, t, b) => {
+ // // Let(l, t, a, b) => {
+ // // App(f, args) => App(map(f), vec(args, map)),
+ // // Annot(x, t) => Annot(map(x), map(t)),
+ // (Const(x), Const(y)) if x == y => Some(Const(x)),
+ // (Builtin(x), Builtin(y)) if x == y => Some(Builtin(x)),
+ // (BoolLit(x), BoolLit(y)) if x == y => Some(BoolLit(x)),
+ // (NaturalLit(x), NaturalLit(y)) if x == y => Some(NaturalLit(x)),
+ // (IntegerLit(x), IntegerLit(y)) if x == y => Some(IntegerLit(x)),
+ // (DoubleLit(x), DoubleLit(y)) if x == y => Some(DoubleLit(x)),
+ // // TextLit(t) => TextLit(t.map(map)),
+ // // BinOp(o, x, y) => BinOp(o, map(x), map(y)),
+ // // BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)),
+ // // EmptyListLit(t) => EmptyListLit(map(t)),
+ // // NEListLit(es) => NEListLit(vec(es, map)),
+ // // EmptyOptionalLit(t) => EmptyOptionalLit(map(t)),
+ // // NEOptionalLit(e) => NEOptionalLit(map(e)),
+ // // RecordType(kts) => RecordType(btmap(kts, map_label, map)),
+ // // RecordLit(kvs) => RecordLit(btmap(kvs, map_label, map)),
+ // // UnionType(kts) => UnionType(btmap(kts, map_label, map)),
+ // // UnionLit(k, v, kvs) => {
+ // // Merge(x, y, t) => Merge(map(x), map(y), t.map(map)),
+ // // Field(e, l) => Field(map(e), map_label(l)),
+ // // Projection(e, ls) => Projection(map(e), vec(ls, map_label)),
+ // // Note(n, e) => Note(map_note(n), map(e)),
+ // // Embed(a) => Embed(map_embed(a)),
+ // }
+ // }
+}
+
+impl<N, E> SubExpr<N, E> {
+ #[inline(always)]
+ pub fn as_ref(&self) -> &Expr<N, E> {
+ self.0.as_ref()
+ }
+
+ pub fn map_ref<'a, F1, F2>(
+ &'a self,
+ map_expr: F1,
+ map_under_binder: F2,
+ ) -> Self
+ where
+ F1: FnMut(&'a Self) -> Self,
+ F2: FnOnce(&'a Label, &'a Self) -> Self,
+ {
+ match self.as_ref() {
+ ExprF::Embed(_) => SubExpr::clone(self),
+ // Recursive call
+ ExprF::Note(_, e) => e.map_ref(map_expr, map_under_binder),
+ // Call ExprF::map_ref
+ e => rc(e.map_ref(
+ map_expr,
+ map_under_binder,
+ |_| unreachable!(),
+ |_| unreachable!(),
+ Label::clone,
+ )),
+ }
+ }
+
+ pub fn map_ref_simple<F1>(&self, map_expr: F1) -> Self
+ where
+ F1: Fn(&Self) -> Self,
+ {
+ self.map_ref(&map_expr, |_, e| map_expr(e))
+ }
+
+ #[inline(always)]
+ pub fn unroll(&self) -> Expr<N, E>
+ where
+ N: Clone,
+ E: Clone,
+ {
+ ExprF::clone(self.as_ref())
+ }
+}
+
+impl<N, E> Clone for SubExpr<N, E> {
+ #[inline(always)]
+ fn clone(&self) -> Self {
+ SubExpr(Rc::clone(&self.0))
+ }
+}
+
// Remains of a previous life, where everything was in Boxes
-pub fn bx<T>(x: T) -> Rc<T> {
- Rc::new(x)
+pub fn bx<N, E>(x: Expr<N, E>) -> SubExpr<N, E> {
+ SubExpr(Rc::new(x))
}
-pub fn rc<T>(x: T) -> Rc<T> {
- Rc::new(x)
+// Should probably rename this too
+pub fn rc<N, E>(x: Expr<N, E>) -> SubExpr<N, E> {
+ SubExpr(Rc::new(x))
}
pub fn app<N, E>(f: Expr<N, E>, args: Vec<SubExpr<N, E>>) -> Expr<N, E> {
if args.is_empty() {
f
} else {
- Expr::App(rc(f), args)
+ ExprF::App(rc(f), args)
}
}
@@ -339,7 +613,7 @@ pub fn app_rc<N, E>(
if args.is_empty() {
f
} else {
- rc(Expr::App(f, args))
+ rc(ExprF::App(f, args))
}
}
@@ -351,100 +625,6 @@ fn add_ui(u: usize, i: isize) -> usize {
}
}
-/// Map over the immediate children of the passed Expr
-pub fn map_subexpr<S, T, A, B, F1, F2, F3, F4, F5>(
- e: &Expr<S, A>,
- map: F1,
- map_note: F2,
- map_embed: F3,
- map_label: F4,
- map_under_binder: F5,
-) -> Expr<T, B>
-where
- F1: Fn(&SubExpr<S, A>) -> SubExpr<T, B>,
- F2: FnOnce(&S) -> T,
- F3: FnOnce(&A) -> B,
- F4: Fn(&Label) -> Label,
- F5: FnOnce(&Label, &SubExpr<S, A>) -> SubExpr<T, B>,
-{
- use crate::Expr::*;
- let map = &map;
- let opt = |x: &Option<_>| x.as_ref().map(&map);
- let vec = |x: &Vec<_>| x.iter().map(&map).collect();
- let btmap = |x: &BTreeMap<_, _>| {
- x.into_iter().map(|(k, v)| (map_label(k), map(v))).collect()
- };
- match e {
- Const(k) => Const(*k),
- Var(V(l, n)) => Var(V(map_label(l), *n)),
- Lam(l, t, b) => Lam(map_label(l), map(t), map_under_binder(l, b)),
- Pi(l, t, b) => Pi(map_label(l), map(t), map_under_binder(l, b)),
- App(f, args) => App(map(f), vec(args)),
- Let(l, t, a, b) => {
- Let(map_label(l), opt(t), map(a), map_under_binder(l, b))
- }
- Annot(x, t) => Annot(map(x), map(t)),
- Builtin(v) => Builtin(*v),
- BoolLit(b) => BoolLit(*b),
- BoolIf(b, t, f) => BoolIf(map(b), map(t), map(f)),
- NaturalLit(n) => NaturalLit(*n),
- IntegerLit(n) => IntegerLit(*n),
- DoubleLit(n) => DoubleLit(*n),
- TextLit(t) => TextLit(t.map(&map)),
- BinOp(o, x, y) => BinOp(*o, map(x), map(y)),
- EmptyListLit(t) => EmptyListLit(map(t)),
- NEListLit(es) => NEListLit(vec(es)),
- EmptyOptionalLit(t) => EmptyOptionalLit(map(t)),
- NEOptionalLit(e) => NEOptionalLit(map(e)),
- RecordType(kts) => RecordType(btmap(kts)),
- RecordLit(kvs) => RecordLit(btmap(kvs)),
- UnionType(kts) => UnionType(btmap(kts)),
- UnionLit(k, v, kvs) => UnionLit(map_label(k), map(v), btmap(kvs)),
- Merge(x, y, t) => Merge(map(x), map(y), opt(t)),
- Field(e, l) => Field(map(e), map_label(l)),
- Projection(e, ls) => {
- Projection(map(e), ls.iter().map(&map_label).collect())
- }
- Note(n, e) => Note(map_note(n), map(e)),
- Embed(a) => Embed(map_embed(a)),
- }
-}
-
-pub fn map_subexpr_rc_binder<S, A, F1, F2>(
- e: &SubExpr<S, A>,
- map_expr: F1,
- map_under_binder: F2,
-) -> SubExpr<S, A>
-where
- F1: Fn(&SubExpr<S, A>) -> SubExpr<S, A>,
- F2: FnOnce(&Label, &SubExpr<S, A>) -> SubExpr<S, A>,
-{
- match e.as_ref() {
- Expr::Embed(_) => Rc::clone(e),
- Expr::Note(_, e) => {
- map_subexpr_rc_binder(e, map_expr, map_under_binder)
- }
- _ => rc(map_subexpr(
- e,
- map_expr,
- |_| unreachable!(),
- |_| unreachable!(),
- Label::clone,
- map_under_binder,
- )),
- }
-}
-
-pub fn map_subexpr_rc<S, A, F1>(
- e: &SubExpr<S, A>,
- map_expr: F1,
-) -> SubExpr<S, A>
-where
- F1: Fn(&SubExpr<S, A>) -> SubExpr<S, A>,
-{
- map_subexpr_rc_binder(e, &map_expr, |_, e| map_expr(e))
-}
-
/// `shift` is used by both normalization and type-checking to avoid variable
/// capture by shifting variable indices
///
@@ -518,10 +698,10 @@ where
///
pub fn shift<S, A>(
delta: isize,
- var: &V,
- in_expr: &Rc<Expr<S, A>>,
-) -> Rc<Expr<S, A>> {
- use crate::Expr::*;
+ var: &V<Label>,
+ in_expr: &SubExpr<S, A>,
+) -> SubExpr<S, A> {
+ use crate::ExprF::*;
let V(x, n) = var;
let under_binder = |y: &Label, e: &SubExpr<_, _>| {
let n = if x == y { n + 1 } else { *n };
@@ -532,11 +712,7 @@ pub fn shift<S, A>(
Var(V(y, m)) if x == y && n <= m => {
rc(Var(V(y.clone(), add_ui(*m, delta))))
}
- _ => map_subexpr_rc_binder(
- in_expr,
- |e| shift(delta, var, e),
- under_binder,
- ),
+ _ => in_expr.map_ref(|e| shift(delta, var, e), under_binder),
}
}
@@ -547,11 +723,11 @@ pub fn shift<S, A>(
/// ```
///
pub fn subst<S, A>(
- var: &V,
- value: &Rc<Expr<S, A>>,
- in_expr: &Rc<Expr<S, A>>,
-) -> Rc<Expr<S, A>> {
- use crate::Expr::*;
+ var: &V<Label>,
+ value: &SubExpr<S, A>,
+ in_expr: &SubExpr<S, A>,
+) -> SubExpr<S, A> {
+ use crate::ExprF::*;
let under_binder = |y: &Label, e: &SubExpr<_, _>| {
let V(x, n) = var;
let n = if x == y { n + 1 } else { *n };
@@ -559,11 +735,7 @@ pub fn subst<S, A>(
subst(newvar, &shift(1, &V(y.clone(), 0), value), e)
};
match in_expr.as_ref() {
- Var(v) if var == v => Rc::clone(value),
- _ => map_subexpr_rc_binder(
- in_expr,
- |e| subst(var, value, e),
- under_binder,
- ),
+ Var(v) if var == v => SubExpr::clone(value),
+ _ => in_expr.map_ref(|e| subst(var, value, e), under_binder),
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-08 03:42:59 +0000