diff options
| -rw-r--r-- | dhall/src/binary.rs | 18 | ||||
| -rw-r--r-- | dhall/src/normalize.rs | 273 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 17 | ||||
| -rw-r--r-- | dhall_core/src/core.rs | 32 | ||||
| -rw-r--r-- | dhall_core/src/parser.rs | 7 | ||||
| -rw-r--r-- | dhall_generator/src/lib.rs | 2 |
6 files changed, 175 insertions, 174 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) -> diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs index ea23cbd..197907a 100644 --- a/dhall_core/src/core.rs +++ b/dhall_core/src/core.rs @@ -304,7 +304,7 @@ pub enum Expr<Note, Embed> { /// `Pi x A B ~ ∀(x : A) -> B` Pi(Label, Box<Expr<Note, Embed>>, Box<Expr<Note, Embed>>), /// `App f A ~ f A` - App(Box<Expr<Note, Embed>>, Box<Expr<Note, Embed>>), + App(Box<Expr<Note, Embed>>, Vec<Expr<Note, Embed>>), /// `Let x Nothing r e ~ let x = r in e` /// `Let x (Just t) r e ~ let x : t = r in e` Let( @@ -646,10 +646,13 @@ impl<S, A: Display> Expr<S, A> { fn fmt_d(&self, f: &mut fmt::Formatter) -> Result<(), fmt::Error> { use crate::Expr::*; match self { - &App(ref a, ref b) => { + &App(ref a, ref args) => { a.fmt_d(f)?; - f.write_str(" ")?; - b.fmt_e(f) + for x in args { + f.write_str(" ")?; + x.fmt_e(f)?; + } + Ok(()) } &Note(_, ref b) => b.fmt_d(f), a => a.fmt_e(f), @@ -842,12 +845,12 @@ where Expr::Pi(var.into(), bx(ty.into()), bx(value.into())) } -pub fn app<S, A, Ef, Ex>(f: Ef, x: Ex) -> Expr<S, A> +pub fn app<S, A, Ef, Ex>(f: Ef, x: Vec<Ex>) -> Expr<S, A> where Ef: Into<Expr<S, A>>, Ex: Into<Expr<S, A>>, { - Expr::App(bx(f.into()), bx(x.into())) + Expr::App(bx(f.into()), x.into_iter().map(|x| x.into()).collect()) } pub type Double = f64; @@ -902,7 +905,10 @@ where Var(V(ref x, n)) => Var(V(map_label(x), n)), Lam(ref x, ref t, ref b) => Lam(map_label(x), bxmap(t), bxmap(b)), Pi(ref x, ref t, ref b) => Pi(map_label(x), bxmap(t), bxmap(b)), - App(ref f, ref a) => App(bxmap(f), bxmap(a)), + App(ref f, ref args) => { + let args = args.iter().map(&map).collect(); + App(bxmap(f), args) + } Let(ref l, ref t, ref a, ref b) => { Let(map_label(l), opt(t), bxmap(a), bxmap(b)) } @@ -1079,7 +1085,11 @@ pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> { let tB2 = shift(d, &V(x.clone(), n2), tB); Pi(x2.clone(), bx(tA2), bx(tB2)) } - App(f, a) => app(shift(d, v, f), shift(d, v, a)), + App(f, args) => { + let f = shift(d, v, f); + let args = args.iter().map(|a| shift(d, v, a)).collect(); + app(f, args) + } Let(f, mt, r, e) => { let n2 = if x == f { n + 1 } else { *n }; let e2 = shift(d, &V(x.clone(), n2), e); @@ -1170,10 +1180,10 @@ where let tA2 = subst(v, e, tA); Pi(y.clone(), bx(tA2), bx(tB2)) } - App(f, a) => { + App(f, args) => { let f2 = subst(v, e, f); - let a2 = subst(v, e, a); - app(f2, a2) + let args = args.iter().map(|a| subst(v, e, a)).collect(); + app(f2, args) } Var(v2) => { if v == v2 { diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs index ddf3f8f..02242bf 100644 --- a/dhall_core/src/parser.rs +++ b/dhall_core/src/parser.rs @@ -746,7 +746,12 @@ rule!(annotated_expression<BoxExpr>; rule!(application_expression<BoxExpr>; children!(first: expression, rest*: expression) => { - rest.fold(first, |acc, e| bx(Expr::App(acc, e))) + let rest: Vec<_> = rest.map(|x| *x).collect(); + if rest.is_empty() { + first + } else { + bx(Expr::App(first, rest)) + } } ); diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs index 512df94..0d84053 100644 --- a/dhall_generator/src/lib.rs +++ b/dhall_generator/src/lib.rs @@ -42,7 +42,7 @@ fn dhall_to_tokenstream( } App(f, a) => { let f = dhall_to_tokenstream_bx(f, ctx); - let a = dhall_to_tokenstream_bx(a, ctx); + let a = vec_to_tokenstream(a, ctx); quote! { App(#f, #a) } } Const(c) => { |