summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/normalize.rs20
-rw-r--r--dhall/src/typecheck.rs21
-rw-r--r--dhall_core/src/core.rs15
-rw-r--r--dhall_generator/src/lib.rs4
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 => {