summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-03-08 22:59:18 +0100
committerNadrieril2019-03-08 22:59:18 +0100
commitc6aafe818ca56ec8bc6d3cd27824eba0a2d6b874 (patch)
tree57e4ef2c9d063744f3dfaf9693ad353b146438a4 /dhall
parentd3f4a32d1e3d39c8d42306e5ca5ad4bb256edcd8 (diff)
Clean up some of the mess
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs20
-rw-r--r--dhall/src/typecheck.rs21
2 files changed, 17 insertions, 24 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(