From 93def475f7c9b241b62cd29cfe9ac8410a19cb07 Mon Sep 17 00:00:00 2001 From: NanoTech Date: Sun, 11 Dec 2016 23:04:11 +0000 Subject: Implement all subst cases --- src/core.rs | 59 +++++++++++++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 51 insertions(+), 8 deletions(-) (limited to 'src') diff --git a/src/core.rs b/src/core.rs index 71b6b14..c5a475e 100644 --- a/src/core.rs +++ b/src/core.rs @@ -513,6 +513,13 @@ fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap it.into_iter().map(|(&k, v)| (k, f(v))).collect() } +fn map_op2(f: F, g: G, a: T, b: T) -> V + where F: FnOnce(U, U) -> V, + G: Fn(T) -> U, +{ + f(g(a), g(b)) +} + /// `shift` is used by both normalization and type-checking to avoid variable /// capture by shifting variable indices /// @@ -668,7 +675,7 @@ fn shift_op2<'i, S, T, A, F>(f: F, where F: FnOnce(Box>, Box>) -> Expr<'i, T, A>, A: Clone { - f(bx(shift(d, v, a)), bx(shift(d, v, b))) + map_op2(f, |x| bx(shift(d, v, x)), a, b) } /// Substitute all occurrences of a variable with an expression @@ -678,9 +685,8 @@ fn shift_op2<'i, S, T, A, F>(f: F, /// ``` /// pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> Expr<'i, S, A> - where S: Clone + fmt::Debug, - T: Clone + fmt::Debug, - A: Clone + fmt::Debug + where S: Clone, + A: Clone { use Expr::*; let V(x, n) = v; @@ -711,28 +717,65 @@ pub fn subst<'i, S, T, A>(v: V<'i>, e: &Expr<'i, S, A>, b: &Expr<'i, T, A>) -> E let r2 = subst(V(x, n), e, r); Let(f, mt2, bx(r2), bx(b2)) } + &Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b), &BuiltinType(t) => BuiltinType(t), &BuiltinValue(v) => BuiltinValue(v), &BoolLit(a) => BoolLit(a), + &BoolAnd(ref a, ref b) => subst_op2(BoolAnd, v, e, a, b), + &BoolOr(ref a, ref b) => subst_op2(BoolOr, v, e, a, b), + &BoolEQ(ref a, ref b) => subst_op2(BoolEQ, v, e, a, b), + &BoolNE(ref a, ref b) => subst_op2(BoolNE, v, e, a, b), + &BoolIf(ref a, ref b, ref c) => { + BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c))) + } &NaturalLit(a) => NaturalLit(a), - &NaturalPlus(ref a, ref b) => NaturalPlus(bx(subst(v, e, a)), bx(subst(v, e, b))), - &NaturalTimes(ref a, ref b) => NaturalTimes(bx(subst(v, e, a)), bx(subst(v, e, b))), + &NaturalPlus(ref a, ref b) => subst_op2(NaturalPlus, v, e, a, b), + &NaturalTimes(ref a, ref b) => subst_op2(NaturalTimes, v, e, a, b), &IntegerLit(a) => IntegerLit(a), &DoubleLit(a) => DoubleLit(a), &TextLit(ref a) => TextLit(a.clone()), + &TextAppend(ref a, ref b) => subst_op2(TextAppend, v, e, a, b), &ListLit(ref a, ref b) => { let a2 = subst(v, e, a); let b2 = b.iter().map(|be| subst(v, e, be)).collect(); ListLit(bx(a2), b2) } + &OptionalLit(ref a, ref b) => { + let a2 = subst(v, e, a); + let b2 = b.iter().map(|be| subst(v, e, be)).collect(); + OptionalLit(bx(a2), b2) + } &Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))), - &RecordLit(ref kvs) => Record(map_record_value(kvs, |val| subst(v, e, val))), + &RecordLit(ref kvs) => RecordLit(map_record_value(kvs, |val| subst(v, e, val))), + &Union(ref kts) => Union(map_record_value(kts, |t| subst(v, e, t))), + &UnionLit(k, ref uv, ref kvs) => { + UnionLit(k, + bx(subst(v, e, uv)), + map_record_value(kvs, |val| subst(v, e, val))) + } + &Combine(ref a, ref b) => subst_op2(Combine, v, e, a, b), + &Merge(ref a, ref b, ref c) => { + Merge(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c))) + } &Field(ref a, b) => Field(bx(subst(v, e, a)), b), &Note(_, ref b) => subst(v, e, b), - b => panic!("Unimplemented subst case: {:?}", b), + &Embed(ref p) => Embed(p.clone()), } } +fn subst_op2<'i, S, T, A, F>(f: F, + v: V<'i>, + e: &Expr<'i, S, A>, + a: &Expr<'i, T, A>, + b: &Expr<'i, T, A>) + -> Expr<'i, S, A> + where F: FnOnce(Box>, Box>) -> Expr<'i, S, A>, + S: Clone, + A: Clone +{ + map_op2(f, |x| bx(subst(v, e, x)), a, b) +} + /// Reduce an expression to its normal form, performing beta reduction /// /// `normalize` does not type-check the expression. You may want to type-check -- cgit v1.2.3