diff options
author | Nadrieril | 2019-03-15 23:41:04 +0100 |
---|---|---|
committer | Nadrieril | 2019-03-15 23:41:04 +0100 |
commit | 22aa5de3fb5836daf066add3e128173bbd396003 (patch) | |
tree | 3220a06b6cf62ee2f73dbfba650f6e752989a32c /dhall/src | |
parent | 4e09c0205469de021fd95490be0a3d19bba8bfc2 (diff) |
Store a vec in App
Closes #26
Diffstat (limited to 'dhall/src')
-rw-r--r-- | dhall/src/binary.rs | 18 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 273 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 17 |
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) -> |