diff options
| -rw-r--r-- | dhall/src/normalize.rs | 20 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 21 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 15 | ||||
| -rw-r--r-- | 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 => { |