From c6aafe818ca56ec8bc6d3cd27824eba0a2d6b874 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 8 Mar 2019 22:59:18 +0100
Subject: Clean up some of the mess

---
 dhall/src/normalize.rs     | 20 +++++++++-----------
 dhall/src/typecheck.rs     | 21 ++++++++-------------
 dhall_core/src/core.rs     | 15 +++++++++++++--
 dhall_generator/src/lib.rs |  4 ++--
 4 files changed, 32 insertions(+), 28 deletions(-)

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3b8099a..038458f 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -89,12 +89,11 @@ where
                 (Builtin(NaturalOdd), NaturalLit(n)) => BoolLit(n % 2 != 0),
                 (Builtin(NaturalToInteger), NaturalLit(n)) => IntegerLit(n as isize),
                 (Builtin(NaturalShow), NaturalLit(n)) => TextLit(n.to_string()),
-                // 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));
-                //     normalize(&dhall!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)))
-                // }
+                (App(box Builtin(ListBuild), a0), k) => {
+                    let k = bx(k);
+                    let a1 = bx(shift(1, &V("a".into(), 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) => {
                     let e2: Expr<_, _, _> = xs.into_iter().rev().fold(nil, |y, ys| {
                         let y = bx(y);
@@ -139,11 +138,10 @@ where
                     });
                     normalize(&e2)
                 }
-                // TODO: restore when handling variables generically fixed
-                // (App(box Builtin(OptionalBuild), a0), g) => {
-                //     let g = bx(g);
-                //     normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)))
-                // }
+                (App(box Builtin(OptionalBuild), a0), g) => {
+                    let g = bx(g);
+                    normalize(&dhall!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0)))
+                }
                 (f2, a2) => app(f2, a2),
             },
         },
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index b5bdee8..fa938ef 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -145,7 +145,7 @@ where
     go::<L, S, T>(&mut ctx, &normalize(eL0), &normalize(eR0))
 }
 
-fn op2_type<Label: StringLike + From<String>, S, EF>(
+fn op2_type<Label: StringLike, S, EF>(
     ctx: &Context<Label, Expr<Label, S, X>>,
     e: &Expr<Label, S, X>,
     t: core::Builtin,
@@ -178,7 +178,7 @@ where
 /// `type_with` does not necessarily normalize the type since full normalization
 /// is not necessary for just type-checking.  If you actually care about the
 /// returned type then you may want to `normalize` it afterwards.
-pub fn type_with<Label: StringLike + From<String>, S>(
+pub fn type_with<Label: StringLike, S>(
     ctx: &Context<Label, Expr<Label, S, X>>,
     e: &Expr<Label, S, X>,
 ) -> Result<Expr<Label, S, X>, TypeError<Label, S>>
@@ -489,17 +489,12 @@ where
         ).take_ownership_of_labels()),
         Builtin(ListIndexed) => {
             let mut m: BTreeMap<Label, Expr<Label, _, _>> = BTreeMap::new();
-            m.insert("index".to_owned().into(), Builtin(Natural));
-            let var: Expr<Label, _, _> = Var(V(Label::from("a".to_owned()), 0));
-            m.insert("value".to_owned().into(), var.clone());
-            let underscore: Label = Label::from("_".to_owned());
-            let innerinner: Expr<Label, _, _> = app(List, Record(m));
-            let innerinner2: Expr<Label, _, _> = app(List, var);
-            let inner: Expr<Label, _, _> = Pi(underscore, bx(innerinner2), bx(innerinner));
-            Ok(Pi(
-                Label::from("a".to_owned()),
-                bx(Const(Type)),
-                bx(inner),
+            m.insert("index".into(), Builtin(Natural));
+            m.insert("value".into(), Var(V("a".into(), 0)));
+            Ok(pi(
+                "a",
+                Const(Type),
+                pi("_", app(List, Var(V("a".into(), 0))), app(List, Record(m))),
             ))
         }
         Builtin(ListReverse) => Ok(pi(
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 04c3961..72389c5 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -268,7 +268,16 @@ pub enum Builtin {
 }
 
 pub trait StringLike:
-    Display + fmt::Debug + Clone + Hash + Ord + Eq + Into<String> + Default + From<String>
+    Display
+    + fmt::Debug
+    + Clone
+    + Hash
+    + Ord
+    + Eq
+    + Default
+    + Into<String>
+    + From<String>
+    + From<&'static str>
 {
 }
 
@@ -279,8 +288,10 @@ impl<T> StringLike for T where
         + Hash
         + Ord
         + Eq
+        + Default
         + Into<String>
-        + Default + From<String>
+        + From<String>
+        + From<&'static str>
 {
 }
 
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index 75912d0..8745c76 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -32,7 +32,7 @@ fn dhall_to_tokenstream<L: StringLike>(
             let t = dhall_to_tokenstream_bx(t, ctx);
             let b = dhall_to_tokenstream_bx(b, &ctx.insert(x.clone(), ()));
             let x = Literal::string(&x.clone().into());
-            quote! { Lam(#x.to_owned().into(), #t, #b) }
+            quote! { Lam(#x.into(), #t, #b) }
         }
         App(f, a) => {
             let f = dhall_to_tokenstream_bx(f, ctx);
@@ -85,7 +85,7 @@ fn dhall_to_tokenstream_bx<L: StringLike>(
                 // Non-free variable; interpolates as itself
                 Some(()) => {
                     let s: String = s.clone().into();
-                    quote! { bx(Var(V(#s.to_owned().into(), #n))) }
+                    quote! { bx(Var(V(#s.into(), #n))) }
                 }
                 // Free variable; interpolates as a rust variable
                 None => {
-- 
cgit v1.2.3