diff options
author | Nadrieril | 2019-03-08 18:47:25 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-08 18:47:25 +0100 |
commit | 0916eafc12b0ccbbf5b524a273903a0a84f30e74 (patch) | |
tree | bb00b7028835c54db4787e326abed74678ce3884 | |
parent | 74719869dc8aae53bf9521de55188c08f4ebaf11 (diff) |
Make labels non-Copy
Diffstat (limited to '')
-rw-r--r-- | dhall/src/normalize.rs | 10 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 6 | ||||
-rw-r--r-- | dhall_core/src/core.rs | 187 |
3 files changed, 99 insertions, 104 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index d3766d5..4f07d9a 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -26,9 +26,9 @@ where match e { // Matches that don't normalize everything right away Let(f, _, r, b) => { - let r2 = shift::<Label, _, S, _>(1, V(f.clone(), 0), r); - let b2 = subst::<Label, _, S, _>(V(f.clone(), 0), &r2, b); - let b3 = shift::<Label, _, T, _>(-1, V(f.clone(), 0), &b2); + let r2 = shift::<Label, _, S, _>(1, &V(f.clone(), 0), r); + let b2 = subst::<Label, _, S, _>(&V(f.clone(), 0), &r2, b); + let b3 = shift::<Label, _, T, _>(-1, &V(f.clone(), 0), &b2); normalize(&b3) } BoolIf(b, t, f) => match normalize(b) { @@ -41,7 +41,7 @@ where App(f, a) => match normalize::<Label, S, T, A>(f) { Lam(x, _A, b) => { // Beta reduce - let vx0 = V(x, 0); + let vx0 = &V(x, 0); let a2 = shift::<Label, S, S, A>(1, vx0, a); let b2 = subst::<Label, S, T, A>(vx0, &a2, &b); let b3 = shift::<Label, S, T, A>(-1, vx0, &b2); @@ -92,7 +92,7 @@ where // TODO: restore when handling variables generically fixed // (App(box Builtin(ListBuild), a0), k) => { // let k = bx(k); - // let a1 = bx(shift(1, V("a", 0), &a0)); + // let a1 = bx(shift(1, &V("a", 0), &a0)); // normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0))) // } (App(box App(box App(box App(box Builtin(ListFold), _), box ListLit(_, xs)), _), cons), nil) => { diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index c2a2ca3..b7fead3 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -198,7 +198,7 @@ where Lam(x, ref tA, ref b) => { let ctx2 = ctx .insert(x, (**tA).clone()) - .map(|e| core::shift(1, V(x, 0), e)); + .map(|e| core::shift(1, &V(x, 0), e)); let tB = type_with(&ctx2, b)?; let p = Pi(x, tA.clone(), bx(tB)); let _ = type_with(ctx, &p)?; @@ -220,7 +220,7 @@ where let ctx2 = ctx .insert(x, (**tA).clone()) - .map(|e| core::shift(1, V(x, 0), e)); + .map(|e| core::shift(1, &V(x, 0), e)); let tB = normalize(&type_with(&ctx2, tB)?); let kB = match tB { Const(k) => k, @@ -252,7 +252,7 @@ where }; let tA2 = type_with(ctx, a)?; if prop_equal(&tA, &tA2) { - let vx0 = V(x, 0); + let vx0 = &V(x, 0); let a2 = shift::<&str, S, S, X>(1, vx0, a); let tB2 = subst(vx0, &a2, &tB); let tB3 = shift::<&str, S, S, X>(-1, vx0, &tB2); diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index d832a18..343c631 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -269,7 +269,7 @@ pub enum Builtin { } pub trait StringLike: - Display + fmt::Debug + Clone + Copy + Hash + Ord + Eq + Into<String> + Default + Display + fmt::Debug + Clone + Hash + Ord + Eq + Into<String> + Default { } @@ -277,7 +277,6 @@ impl<T> StringLike for T where T: Display + fmt::Debug + Clone - + Copy + Hash + Ord + Eq @@ -819,11 +818,11 @@ where pub fn map_record_value<'a, I, K, V, U, F>(it: I, f: F) -> BTreeMap<K, U> where I: IntoIterator<Item = (&'a K, &'a V)>, - K: Eq + Ord + Copy + 'a, + K: Eq + Ord + Clone + 'a, V: 'a, F: FnMut(&V) -> U, { - map_record_value_and_keys(it, f, |&x| x) + map_record_value_and_keys(it, f, |x| x.clone()) } pub fn map_record_value_and_keys<'a, I, K, L, V, U, F, G>( @@ -930,92 +929,90 @@ where /// pub fn shift<Label, S, T, A: Clone>( d: isize, - v: V<Label>, + v: &V<Label>, e: &Expr_<Label, S, A>, ) -> Expr_<Label, T, A> where - Label: Copy, - Label: Ord, - Label: PartialEq, + Label: StringLike, { use crate::Expr_::*; let V(x, n) = v; - match *e { - Const(a) => Const(a), + match e { + Const(a) => Const(*a), Var(V(x2, n2)) => { let n3 = if x == x2 && n <= n2 { - add_ui(n2, d) + add_ui(*n2, d) } else { - n2 + *n2 }; - Var(V(x2, n3)) + Var(V(x2.clone(), n3)) } - Lam(x2, ref tA, ref b) => { - let n2 = if x == x2 { n + 1 } else { n }; - let tA2 = shift(d, V(x, n), tA); - let b2 = shift(d, V(x, n2), b); - Lam(x2, bx(tA2), bx(b2)) + Lam(x2, tA, b) => { + let n2 = if x == x2 { n + 1 } else { *n }; + let tA2 = shift(d, v, tA); + let b2 = shift(d, &V(x.clone(), n2), b); + Lam(x2.clone(), bx(tA2), bx(b2)) } - Pi(x2, ref tA, ref tB) => { - let n2 = if x == x2 { n + 1 } else { n }; - let tA2 = shift(d, V(x, n), tA); - let tB2 = shift(d, V(x, n2), tB); - pi(x2, tA2, tB2) + Pi(x2, tA, tB) => { + let n2 = if x == x2 { n + 1 } else { *n }; + let tA2 = shift(d, v, tA); + let tB2 = shift(d, &V(x.clone(), n2), tB); + Pi(x2.clone(), bx(tA2), bx(tB2)) } - App(ref f, ref a) => app(shift(d, v, f), shift(d, v, a)), - Let(f, ref mt, ref r, ref e) => { - let n2 = if x == f { n + 1 } else { n }; - let e2 = shift(d, V(x, n2), e); - let mt2 = mt.as_ref().map(|t| bx(shift(d, V(x, n), t))); - let r2 = shift(d, V(x, n), r); - Let(f, mt2, bx(r2), bx(e2)) + App(f, a) => app(shift(d, v, f), shift(d, v, a)), + Let(f, mt, r, e) => { + let n2 = if x == f { n + 1 } else { *n }; + let e2 = shift(d, &V(x.clone(), n2), e); + let mt2 = mt.as_ref().map(|t| bx(shift(d, v, t))); + let r2 = shift(d, v, r); + Let(f.clone(), mt2, bx(r2), bx(e2)) } - Annot(ref a, ref b) => shift_op2(Annot, d, v, a, b), - Builtin(v) => Builtin(v), - BoolLit(a) => BoolLit(a), - BinOp(o, ref a, ref b) => shift_op2(|x, y| BinOp(o, x, y), d, v, a, b), - BoolIf(ref a, ref b, ref c) => { + Annot(a, b) => shift_op2(Annot, d, v, a, b), + Builtin(v) => Builtin(*v), + BoolLit(a) => BoolLit(*a), + BinOp(o, a, b) => shift_op2(|x, y| BinOp(*o, x, y), d, v, a, b), + BoolIf(a, b, c) => { BoolIf(bx(shift(d, v, a)), bx(shift(d, v, b)), bx(shift(d, v, c))) } - NaturalLit(a) => NaturalLit(a), - IntegerLit(a) => IntegerLit(a), - DoubleLit(a) => DoubleLit(a), - TextLit(ref a) => TextLit(a.clone()), - ListLit(ref t, ref es) => ListLit( + NaturalLit(a) => NaturalLit(*a), + IntegerLit(a) => IntegerLit(*a), + DoubleLit(a) => DoubleLit(*a), + TextLit(a) => TextLit(a.clone()), + ListLit(t, es) => ListLit( t.as_ref().map(|t| bx(shift(d, v, t))), es.iter().map(|e| shift(d, v, e)).collect(), ), - OptionalLit(ref t, ref es) => OptionalLit( + OptionalLit(t, es) => OptionalLit( t.as_ref().map(|t| bx(shift(d, v, t))), es.iter().map(|e| shift(d, v, e)).collect(), ), - Record(ref a) => Record(map_record_value(a, |val| shift(d, v, val))), - RecordLit(ref a) => { + Record(a) => Record(map_record_value(a, |val| shift(d, v, val))), + RecordLit(a) => { RecordLit(map_record_value(a, |val| shift(d, v, val))) } - Union(ref a) => Union(map_record_value(a, |val| shift(d, v, val))), - UnionLit(k, ref uv, ref a) => UnionLit( - k, + Union(a) => Union(map_record_value(a, |val| shift(d, v, val))), + UnionLit(k, uv, a) => UnionLit( + k.clone(), bx(shift(d, v, uv)), map_record_value(a, |val| shift(d, v, val)), ), - Merge(ref a, ref b, ref c) => Merge( + Merge(a, b, c) => Merge( bx(shift(d, v, a)), bx(shift(d, v, b)), c.as_ref().map(|c| bx(shift(d, v, c))), ), - Field(ref a, b) => Field(bx(shift(d, v, a)), b), - Note(_, ref b) => shift(d, v, b), + Field(a, b) => Field(bx(shift(d, v, a)), b.clone()), + Note(_, b) => shift(d, v, b), // The Dhall compiler enforces that all embedded values are closed expressions // and `shift` does nothing to a closed expression - Embed(ref p) => Embed(p.clone()), + Embed(p) => Embed(p.clone()), } } fn shift_op2<Label, S, T, A, F>( f: F, d: isize, - v: V<Label>, + v: &V<Label>, a: &Expr_<Label, S, A>, b: &Expr_<Label, S, A>, ) -> Expr_<Label, T, A> @@ -1025,9 +1022,7 @@ where Box<Expr_<Label, T, A>>, ) -> Expr_<Label, T, A>, A: Clone, - Label: Copy, - Label: Ord, - Label: PartialEq, + Label: StringLike, { map_op2(f, |x| bx(shift(d, v, x)), a, b) } @@ -1039,7 +1034,7 @@ where /// ``` /// pub fn subst<Label: StringLike, S, T, A>( - v: V<Label>, + v: &V<Label>, e: &Expr_<Label, S, A>, b: &Expr_<Label, T, A>, ) -> Expr_<Label, S, A> @@ -1049,21 +1044,21 @@ where { use crate::Expr_::*; let V(x, n) = v; - match *b { - Const(a) => Const(a), - Lam(y, ref tA, ref b) => { - let n2 = if x == y { n + 1 } else { n }; - let b2 = subst(V(x, n2), &shift(1, V(y, 0), e), b); - let tA2 = subst(V(x, n), e, tA); - Lam(y, bx(tA2), bx(b2)) + match b { + Const(a) => Const(*a), + Lam(y, tA, b) => { + let n2 = if x == y { n + 1 } else { *n }; + let b2 = subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), b); + let tA2 = subst(v, e, tA); + Lam(y.clone(), bx(tA2), bx(b2)) } - Pi(y, ref tA, ref tB) => { - let n2 = if x == y { n + 1 } else { n }; - let tB2 = subst(V(x, n2), &shift(1, V(y, 0), e), tB); - let tA2 = subst(V(x, n), e, tA); - Pi(y, bx(tA2), bx(tB2)) + Pi(y, tA, tB) => { + let n2 = if x == y { n + 1 } else { *n }; + let tB2 = subst(&V(x.clone(), n2), &shift(1, &V(y.clone(), 0), e), tB); + let tA2 = subst(v, e, tA); + Pi(y.clone(), bx(tA2), bx(tB2)) } - App(ref f, ref a) => { + App(f, a) => { let f2 = subst(v, e, f); let a2 = subst(v, e, a); app(f2, a2) @@ -1072,61 +1067,61 @@ where if v == v2 { e.clone() } else { - Var(v2) + Var(v2.clone()) } } - Let(f, ref mt, ref r, ref b) => { - let n2 = if x == f { n + 1 } else { n }; - let b2 = subst(V(x, n2), &shift(1, V(f, 0), e), b); - let mt2 = mt.as_ref().map(|t| bx(subst(V(x, n), e, t))); - let r2 = subst(V(x, n), e, r); - Let(f, mt2, bx(r2), bx(b2)) + Let(f, mt, r, b) => { + let n2 = if x == f { n + 1 } else { *n }; + let b2 = subst(&V(x.clone(), n2), &shift(1, &V(f.clone(), 0), e), b); + let mt2 = mt.as_ref().map(|t| bx(subst(v, e, t))); + let r2 = subst(v, e, r); + Let(f.clone(), mt2, bx(r2), bx(b2)) } - Annot(ref a, ref b) => subst_op2(Annot, v, e, a, b), - Builtin(v) => Builtin(v), - BoolLit(a) => BoolLit(a), - BinOp(o, ref a, ref b) => subst_op2(|x, y| BinOp(o, x, y), v, e, a, b), - BoolIf(ref a, ref b, ref c) => { + Annot(a, b) => subst_op2(Annot, v, e, a, b), + Builtin(v) => Builtin(*v), + BoolLit(a) => BoolLit(*a), + BinOp(o, a, b) => subst_op2(|x, y| BinOp(*o, x, y), v, e, a, b), + BoolIf(a, b, c) => { BoolIf(bx(subst(v, e, a)), bx(subst(v, e, b)), bx(subst(v, e, c))) } - NaturalLit(a) => NaturalLit(a), - IntegerLit(a) => IntegerLit(a), - DoubleLit(a) => DoubleLit(a), - TextLit(ref a) => TextLit(a.clone()), - ListLit(ref a, ref b) => { + NaturalLit(a) => NaturalLit(*a), + IntegerLit(a) => IntegerLit(*a), + DoubleLit(a) => DoubleLit(*a), + TextLit(a) => TextLit(a.clone()), + ListLit(a, b) => { let a2 = a.as_ref().map(|a| bx(subst(v, e, a))); let b2 = b.iter().map(|be| subst(v, e, be)).collect(); ListLit(a2, b2) } - OptionalLit(ref a, ref b) => { + OptionalLit(a, b) => { let a2 = a.as_ref().map(|a| bx(subst(v, e, a))); let b2 = b.iter().map(|be| subst(v, e, be)).collect(); OptionalLit(a2, b2) } - Record(ref kts) => Record(map_record_value(kts, |t| subst(v, e, t))), - RecordLit(ref kvs) => { + Record(kts) => Record(map_record_value(kts, |t| subst(v, e, t))), + RecordLit(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, + Union(kts) => Union(map_record_value(kts, |t| subst(v, e, t))), + UnionLit(k, uv, kvs) => UnionLit( + k.clone(), bx(subst(v, e, uv)), map_record_value(kvs, |val| subst(v, e, val)), ), - Merge(ref a, ref b, ref c) => Merge( + Merge(a, b, c) => Merge( bx(subst(v, e, a)), bx(subst(v, e, b)), c.as_ref().map(|c| bx(subst(v, e, c))), ), - Field(ref a, b) => Field(bx(subst(v, e, a)), b), - Note(_, ref b) => subst(v, e, b), - Embed(ref p) => Embed(p.clone()), + Field(a, b) => Field(bx(subst(v, e, a)), b.clone()), + Note(_, b) => subst(v, e, b), + Embed(p) => Embed(p.clone()), } } fn subst_op2<Label: StringLike, S, T, A, F>( f: F, - v: V<Label>, + v: &V<Label>, e: &Expr_<Label, S, A>, a: &Expr_<Label, T, A>, b: &Expr_<Label, T, A>, |