diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/binary.rs | 10 | ||||
-rw-r--r-- | dhall/src/normalize.rs | 35 | ||||
-rw-r--r-- | dhall/src/typecheck.rs | 10 |
3 files changed, 24 insertions, 31 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs index 694043b..cc07431 100644 --- a/dhall/src/binary.rs +++ b/dhall/src/binary.rs @@ -104,16 +104,16 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> { } [U64(5), t] => { let t = bx(cbor_value_to_dhall(&t)?); - Ok(OptionalLit(Some(t), vec![])) + Ok(OptionalLit(Some(t), None)) } [U64(5), Null, x] => { - let x = cbor_value_to_dhall(&x)?; - Ok(OptionalLit(None, vec![x])) + let x = bx(cbor_value_to_dhall(&x)?); + Ok(OptionalLit(None, Some(x))) } [U64(5), t, x] => { - let x = cbor_value_to_dhall(&x)?; + let x = bx(cbor_value_to_dhall(&x)?); let t = bx(cbor_value_to_dhall(&t)?); - Ok(OptionalLit(Some(t), vec![x])) + Ok(OptionalLit(Some(t), Some(x))) } [U64(6), x, y] => { let x = bx(cbor_value_to_dhall(&x)?); diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index 5349c9e..9105ec4 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -48,22 +48,20 @@ where .collect::<Vec<_>>() .as_slice(), ) { - (OptionalSome, [a]) => OptionalLit(None, vec![a.clone()]), - (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), vec![]), + (OptionalSome, [a]) => OptionalLit(None, Some(bx(a.clone()))), + (OptionalNone, [a]) => OptionalLit(Some(bx(a.clone())), None), (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(), - ), + (ListHead, [_, ListLit(t, ys)]) => { + OptionalLit(t.clone(), ys.iter().cloned().map(bx).next()) + } + (ListLast, [_, ListLit(t, ys)]) => { + OptionalLit(t.clone(), ys.iter().cloned().map(bx).last()) + } (ListReverse, [_, ListLit(t, ys)]) => { let xs = ys.iter().rev().cloned().collect(); ListLit(t.clone(), xs) @@ -123,14 +121,13 @@ where // (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) + (OptionalFold, [_, OptionalLit(_, Some(x)), _, just, _]) => { + let x = bx((**x).clone()); + let just = bx(just.clone()); + normalize_whnf(&dhall_expr!(just x)) + } + (OptionalFold, [_, OptionalLit(_, None), _, _, nothing]) => { + (*nothing).clone() } // // fold/build fusion // (OptionalFold, [_, App(box Builtin(OptionalBuild), [_, x, rest..]), rest..]) => { @@ -170,7 +167,7 @@ where b2 => BoolIf(bx(b2), t.clone(), f.clone()), }, OptionalLit(t, es) => { - if !es.is_empty() { + if !es.is_none() { OptionalLit(None, es.clone()) } else { OptionalLit(t.clone(), es.clone()) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index ed02619..0f87d67 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -477,8 +477,8 @@ where let t: Box<Expr<_, _>> = match t { Some(t) => t.clone(), None => { - let first_x = iter.next().unwrap(); - bx(type_with(ctx, first_x)?) + let x = iter.next().unwrap(); + bx(type_with(ctx, x)?) } }; @@ -493,10 +493,6 @@ where )); } } - let n = xs.len(); - if 2 <= n { - return Err(TypeError::new(ctx, e, InvalidOptionalLiteral(n))); - } for x in iter { let t2 = type_with(ctx, x)?; if !prop_equal(&t, &t2) { @@ -505,7 +501,7 @@ where return Err(TypeError::new( ctx, e, - InvalidOptionalElement(nf_t, x.clone(), nf_t2), + InvalidOptionalElement(nf_t, (**x).clone(), nf_t2), )); } } |