summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNanoTech2016-12-11 23:04:11 +0000
committerNanoTech2017-03-10 23:48:29 -0600
commit93def475f7c9b241b62cd29cfe9ac8410a19cb07 (patch)
tree3fa4b4048bc425c8ccef9f51798b868d1b1a432f
parent2893c14936a3c5f03ad520347e3c2b281b65555e (diff)
Implement all subst cases
Diffstat (limited to '')
-rw-r--r--src/core.rs59
1 files changed, 51 insertions, 8 deletions
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<K, U>
it.into_iter().map(|(&k, v)| (k, f(v))).collect()
}
+fn map_op2<T, U, V, F, G>(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<Expr<'i, T, A>>, Box<Expr<'i, T, A>>) -> 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<Expr<'i, S, A>>, Box<Expr<'i, S, A>>) -> 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