From 0916eafc12b0ccbbf5b524a273903a0a84f30e74 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 8 Mar 2019 18:47:25 +0100
Subject: Make labels non-Copy

---
 dhall/src/normalize.rs |  10 +--
 dhall/src/typecheck.rs |   6 +-
 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>,
-- 
cgit v1.2.3