summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/binary.rs18
-rw-r--r--dhall/src/normalize.rs273
-rw-r--r--dhall/src/typecheck.rs17
3 files changed, 147 insertions, 161 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 6d0f1e9..694043b 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -25,20 +25,20 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
String(s) => match Builtin::parse(s) {
Some(b) => Ok(Expr::Builtin(b)),
None => match s.as_str() {
- "True" => Ok(Expr::BoolLit(true)),
- "False" => Ok(Expr::BoolLit(false)),
- "Type" => Ok(Expr::Const(Const::Type)),
- "Kind" => Ok(Expr::Const(Const::Kind)),
- s => Ok(Expr::Var(V(Label::from(s), 0))),
+ "True" => Ok(BoolLit(true)),
+ "False" => Ok(BoolLit(false)),
+ "Type" => Ok(Const(Const::Type)),
+ "Kind" => Ok(Const(Const::Kind)),
+ s => Ok(Var(V(Label::from(s), 0))),
},
},
- U64(n) => Ok(Expr::Var(V(Label::from("_"), *n as usize))),
+ U64(n) => Ok(Var(V(Label::from("_"), *n as usize))),
F64(x) => Ok(DoubleLit(*x)),
Bool(b) => Ok(BoolLit(*b)),
Array(vec) => match vec.as_slice() {
[String(l), U64(n)] => {
let l = Label::from(l.as_str());
- Ok(Expr::Var(V(l, *n as usize)))
+ Ok(Var(V(l, *n as usize)))
}
[U64(0), f, args..] => {
let f = cbor_value_to_dhall(&f)?;
@@ -46,9 +46,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
.iter()
.map(cbor_value_to_dhall)
.collect::<Result<Vec<_>, _>>()?;
- Ok(args
- .into_iter()
- .fold(f, |acc, e| (Expr::App(bx(acc), bx(e)))))
+ Ok(App(bx(f), args))
}
[U64(1), x, y] => {
let x = bx(cbor_value_to_dhall(&x)?);
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 5003ccd..9f246e4 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -26,162 +26,145 @@ where
}
Annot(x, _) => normalize_whnf(x),
Note(_, e) => normalize_whnf(e),
- App(f, a) => match (normalize_whnf(f), a) {
- (Lam(x, _, b), a) => {
+ App(f, args) => match (normalize_whnf(f), args.as_slice()) {
+ (f, []) => f,
+ (App(f, args1), args2) => normalize_whnf(&App(
+ f.clone(),
+ args1.iter().chain(args2.iter()).cloned().collect(),
+ )),
+ (Lam(ref x, _, ref b), [a, rest..]) => {
// Beta reduce
- let vx0 = &V(x, 0);
+ let vx0 = &V(x.clone(), 0);
let a2 = shift::<S, S, A>(1, vx0, a);
let b2 = subst::<S, S, A>(vx0, &a2, &b);
let b3 = shift::<S, S, A>(-1, vx0, &b2);
- normalize_whnf(&b3)
+ normalize_whnf(&App(bx(b3), rest.to_vec()))
}
- (Builtin(b), a) => match (b, normalize_whnf(a)) {
- (OptionalSome, a) => OptionalLit(None, vec![a]),
- (OptionalNone, a) => OptionalLit(Some(bx(a)), vec![]),
- (NaturalIsZero, NaturalLit(n)) => BoolLit(n == 0),
- (NaturalEven, NaturalLit(n)) => BoolLit(n % 2 == 0),
- (NaturalOdd, NaturalLit(n)) => BoolLit(n % 2 != 0),
- (NaturalToInteger, NaturalLit(n)) => IntegerLit(n as isize),
- (NaturalShow, NaturalLit(n)) => TextLit(n.to_string().into()),
-
- (b, App(f, x)) => match (b, normalize_whnf(&f), x) {
- // fold/build fusion for `Natural`
- (NaturalBuild, Builtin(NaturalFold), x) => {
- normalize_whnf(&x)
- }
- (NaturalFold, Builtin(NaturalBuild), x) => {
- normalize_whnf(&x)
- }
- (b, f, x) => app(Builtin(b), app(f, *x)),
- },
- (b, a) => app(Builtin(b), a),
- },
- (App(f, x), y) => match (normalize_whnf(&f), x, y) {
- // TODO: use whnf
- (Builtin(b), x, y) => match (b, x, normalize::<S, S, A>(&y)) {
- (ListLength, _, ListLit(_, ys)) => NaturalLit(ys.len()),
- (ListHead, _, ListLit(t, ys)) => {
- OptionalLit(t, ys.into_iter().take(1).collect())
- }
- (ListLast, _, ListLit(t, ys)) => OptionalLit(
- t,
- ys.into_iter().last().into_iter().collect(),
- ),
- (ListReverse, _, ListLit(t, ys)) => {
- let mut xs = ys;
- xs.reverse();
- ListLit(t, xs)
- }
-
- // fold/build fusion for `List`
- (
- ListBuild,
- _,
- App(box App(box Builtin(ListFold), _), box e2),
- ) => normalize_whnf(&e2),
- (
- ListFold,
- _,
- App(box App(box Builtin(ListBuild), _), box e2),
- ) => normalize_whnf(&e2),
-
- // fold/build fusion for `Optional`
- (
- OptionalBuild,
- _,
- App(box App(box Builtin(OptionalFold), _), box e2),
- ) => normalize_whnf(&e2),
- (
- OptionalFold,
- _,
- App(box App(box Builtin(OptionalBuild), _), box e2),
- ) => normalize_whnf(&e2),
-
- (ListBuild, a0, k) => {
- let k = bx(k);
- let a1 = bx(shift(1, &V("a".into(), 0), &a0));
- normalize_whnf(
- &dhall_expr!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)),
- )
- }
- (OptionalBuild, a0, g) => {
- let g = bx(g);
- normalize_whnf(
- &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)),
- )
- }
- (b, x, y) => app(App(bx(Builtin(b)), x), y),
- },
- (App(f, x), y, z) => match (normalize_whnf(&f), x, y, z) {
- (App(f, x), y, z, w) => {
- match (normalize_whnf(&f), x, y, z, w) {
- (App(f, x), y, z, w, t) => match (
- normalize_whnf(&f),
- x,
- normalize_whnf(&y),
- z,
- w,
- t,
- ) {
- (
- Builtin(ListFold),
- _,
- ListLit(_, xs),
- _,
- cons,
- nil,
- ) => {
- let e2: Expr<_, _> = xs
- .into_iter()
- .rev()
- .fold((**nil).clone(), |acc, x| {
- let x = bx(x);
- let acc = bx(acc);
- dhall_expr!(cons x acc)
- });
- normalize_whnf(&e2)
+ // TODO: this is more normalization than needed
+ (Builtin(b), args) => match (
+ b,
+ args.iter()
+ .map(normalize_whnf)
+ .collect::<Vec<_>>()
+ .as_slice(),
+ ) {
+ (OptionalSome, [a]) => OptionalLit(None, vec![a.clone()]),
+ (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), vec![]),
+ (NaturalIsZero, [NaturalLit(n)]) => BoolLit(*n == 0),
+ (NaturalEven, [NaturalLit(n)]) => BoolLit(*n % 2 == 0),
+ (NaturalOdd, [NaturalLit(n)]) => BoolLit(*n % 2 != 0),
+ (NaturalToInteger, [NaturalLit(n)]) => IntegerLit(*n as isize),
+ (NaturalShow, [NaturalLit(n)]) => TextLit(n.to_string().into()),
+ (ListLength, [_, ListLit(_, ys)]) => NaturalLit(ys.len()),
+ (ListHead, [_, ListLit(t, ys)]) => OptionalLit(
+ t.clone(),
+ ys.into_iter().take(1).cloned().collect(),
+ ),
+ (ListLast, [_, ListLit(t, ys)]) => OptionalLit(
+ t.clone(),
+ ys.iter().last().cloned().into_iter().collect(),
+ ),
+ (ListReverse, [_, ListLit(t, ys)]) => {
+ let xs = ys.iter().rev().cloned().collect();
+ ListLit(t.clone(), xs)
+ }
+ (ListBuild, [a0, k]) => {
+ // fold/build fusion
+ let k = match k {
+ App(box Builtin(ListFold), args) => {
+ match args.as_slice() {
+ [_, x, rest..] => {
+ return normalize_whnf(&App(
+ bx(x.clone()),
+ rest.to_vec(),
+ ))
}
- (
- Builtin(OptionalFold),
- _,
- OptionalLit(_, xs),
- _,
- just,
- nothing,
- ) => {
- let e2: Expr<_, _> = xs.into_iter().fold(
- (**nothing).clone(),
- |_, y| {
- let y = bx(y);
- dhall_expr!(just y)
- },
- );
- normalize_whnf(&e2)
+ args => app(Builtin(ListFold), args.to_vec()),
+ }
+ }
+ k => k.clone(),
+ };
+ let k = bx(k);
+ let a0 = bx(a0.clone());
+ let a1 = bx(shift(1, &V("a".into(), 0), &a0));
+ normalize_whnf(
+ &dhall_expr!(k (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0)),
+ )
+ }
+ (OptionalBuild, [a0, g]) => {
+ // fold/build fusion
+ let g = match g {
+ App(box Builtin(OptionalFold), args) => {
+ match args.as_slice() {
+ [_, x, rest..] => {
+ return normalize_whnf(&App(
+ bx(x.clone()),
+ rest.to_vec(),
+ ))
}
- (f, x, y, z, w, t) => app(
- App(
- bx(App(
- bx(App(bx(App(bx(f), x)), bx(y))),
- z,
- )),
- w,
- ),
- (**t).clone(),
- ),
- },
- (f, x, y, z, w) => app(
- App(bx(App(bx(App(bx(f), x)), y)), z),
- (**w).clone(),
- ),
+ args => app(Builtin(OptionalFold), args.to_vec()),
+ }
+ }
+ g => g.clone(),
+ };
+ let g = bx(g);
+ let a0 = bx(a0.clone());
+ normalize_whnf(
+ &dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0)),
+ )
+ }
+ (ListFold, [_, ListLit(_, xs), _, cons, nil]) => {
+ let e2: Expr<_, _> =
+ xs.into_iter().rev().fold((*nil).clone(), |acc, x| {
+ let x = bx((x).clone());
+ let acc = bx((acc).clone());
+ let cons = bx((cons).clone());
+ dhall_expr!(cons x acc)
+ });
+ normalize_whnf(&e2)
+ }
+ // // fold/build fusion
+ // (ListFold, [_, App(box Builtin(ListBuild), [_, x, rest..]), rest..]) => {
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // }
+ (OptionalFold, [_, OptionalLit(_, xs), _, just, nothing]) => {
+ let e2: Expr<_, _> =
+ xs.into_iter().fold((*nothing).clone(), |_, y| {
+ let y = bx((y).clone());
+ let just = bx((just).clone());
+ dhall_expr!(just y)
+ });
+ normalize_whnf(&e2)
+ }
+ // // fold/build fusion
+ // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => {
+ // normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ // }
+ (NaturalBuild, [App(f, args)]) => {
+ match (&**f, args.as_slice()) {
+ // fold/build fusion
+ (Builtin(NaturalFold), [x, rest..]) => {
+ normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ }
+ (f, args) => {
+ app(Builtin(NaturalBuild), vec![app(f.clone(), args.to_vec())])
}
}
- (f, x, y, z) => {
- app(App(bx(App(bx(f), x)), y), (**z).clone())
+ }
+ (NaturalFold, [App(f, args)]) => {
+ match (&**f, args.as_slice()) {
+ // fold/build fusion
+ (Builtin(NaturalBuild), [x, rest..]) => {
+ normalize_whnf(&App(bx(x.clone()), rest.to_vec()))
+ }
+ (f, args) => {
+ app(Builtin(NaturalFold), vec![app(f.clone(), args.to_vec())])
+ }
}
- },
- (f, x, y) => app(App(bx(f), x), (**y).clone()),
+ }
+ (b, args) => App(bx(Builtin(b)), args.to_vec()),
},
- (f, a) => app(f, (**a).clone()),
+ (f, args) => App(bx(f), args.to_vec()),
},
BoolIf(b, t, f) => match normalize_whnf(b) {
BoolLit(true) => normalize_whnf(t),
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index c41bd89..ed02619 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -79,7 +79,7 @@ where
}
(&App(ref fL, ref aL), &App(ref fR, ref aR)) => {
if go(ctx, fL, fR) {
- go(ctx, aL, aR)
+ aL.iter().zip(aR.iter()).all(|(aL, aR)| go(ctx, aL, aR))
} else {
false
}
@@ -240,8 +240,13 @@ where
Ok(k) => Ok(Const(k)),
}
}
- App(ref f, ref a) => {
- let tf = normalize(&type_with(ctx, f)?);
+ App(ref f, ref args) => {
+ let (a, args) = match args.split_last() {
+ None => return type_with(ctx, f),
+ Some(x) => x,
+ };
+ let tf =
+ normalize(&type_with(ctx, &App(f.clone(), args.to_vec()))?);
let (x, tA, tB) = match tf {
Pi(x, tA, tB) => (x, tA, tB),
_ => {
@@ -265,7 +270,7 @@ where
Err(TypeError::new(
ctx,
e,
- TypeMismatch((**f).clone(), nf_A, (**a).clone(), nf_A2),
+ TypeMismatch((**f).clone(), nf_A, (*a).clone(), nf_A2),
))
}
}
@@ -435,7 +440,7 @@ where
));
}
}
- Ok(App(bx(Builtin(List)), t))
+ Ok(dhall_expr!(List t))
}
Builtin(ListBuild) => Ok(dhall_expr!(
forall (a: Type) ->
@@ -504,7 +509,7 @@ where
));
}
}
- Ok(App(bx(Builtin(Optional)), t))
+ Ok(dhall_expr!(Optional t))
}
Builtin(OptionalFold) => Ok(dhall_expr!(
forall (a: Type) ->
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 12:56:34 +0000