summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/binary.rs10
-rw-r--r--dhall/src/normalize.rs35
-rw-r--r--dhall/src/typecheck.rs10
-rw-r--r--dhall_core/src/core.rs18
-rw-r--r--dhall_core/src/parser.rs4
-rw-r--r--dhall_generator/src/lib.rs6
6 files changed, 38 insertions, 45 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),
));
}
}
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 197907a..a7b6b53 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -339,7 +339,10 @@ pub enum Expr<Note, Embed> {
ListLit(Option<Box<Expr<Note, Embed>>>, Vec<Expr<Note, Embed>>),
/// `OptionalLit t [e] ~ [e] : Optional t`
/// `OptionalLit t [] ~ [] : Optional t`
- OptionalLit(Option<Box<Expr<Note, Embed>>>, Vec<Expr<Note, Embed>>),
+ OptionalLit(
+ Option<Box<Expr<Note, Embed>>>,
+ Option<Box<Expr<Note, Embed>>>,
+ ),
/// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
Record(BTreeMap<Label, Expr<Note, Embed>>),
/// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
@@ -576,7 +579,7 @@ impl<S, A: Display> Expr<S, A> {
Ok(())
}
&OptionalLit(ref t, ref es) => {
- match es.iter().next() {
+ match es {
None => {
write!(f, "None ")?;
t.as_ref().unwrap().fmt_e(f)?;
@@ -925,10 +928,7 @@ where
let es = es.iter().map(&map).collect();
ListLit(opt(t), es)
}
- OptionalLit(ref t, ref es) => {
- let es = es.iter().map(&map).collect();
- OptionalLit(opt(t), es)
- }
+ OptionalLit(ref t, ref es) => OptionalLit(opt(t), opt(es)),
Record(ref kts) => {
Record(map_record_value_and_keys(kts, map, map_label))
}
@@ -1112,9 +1112,9 @@ pub fn shift<S, T, A: Clone>(d: isize, v: &V, e: &Expr<S, A>) -> Expr<T, A> {
t.as_ref().map(|t| bx(shift(d, v, t))),
es.iter().map(|e| shift(d, v, e)).collect(),
),
- OptionalLit(t, es) => OptionalLit(
+ OptionalLit(t, e) => OptionalLit(
t.as_ref().map(|t| bx(shift(d, v, t))),
- es.iter().map(|e| shift(d, v, e)).collect(),
+ e.as_ref().map(|t| bx(shift(d, v, t))),
),
Record(a) => Record(map_record_value(a, |val| shift(d, v, val))),
RecordLit(a) => RecordLit(map_record_value(a, |val| shift(d, v, val))),
@@ -1218,7 +1218,7 @@ where
}
OptionalLit(a, b) => {
let a2 = a.as_ref().map(|a| bx(subst(v, e, a)));
- let b2 = b.iter().map(|be| subst(v, e, be)).collect();
+ let b2 = b.as_ref().map(|a| bx(subst(v, e, a)));
OptionalLit(a2, b2)
}
Record(kts) => Record(map_record_value(kts, |t| subst(v, e, t))),
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 02242bf..9cbd878 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -648,7 +648,7 @@ rule!(merge_expression<BoxExpr>;
rule!(empty_collection<BoxExpr>;
children!(x: str, y: expression) => {
match x {
- "Optional" => bx(Expr::OptionalLit(Some(y), vec![])),
+ "Optional" => bx(Expr::OptionalLit(Some(y), None)),
"List" => bx(Expr::ListLit(Some(y), vec![])),
_ => unreachable!(),
}
@@ -657,7 +657,7 @@ rule!(empty_collection<BoxExpr>;
rule!(non_empty_optional<BoxExpr>;
children!(x: expression, _y: str, z: expression) => {
- bx(Expr::OptionalLit(Some(z), vec![*x]))
+ bx(Expr::OptionalLit(Some(z), Some(x)))
}
);
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index 0d84053..1d51f9e 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -59,10 +59,10 @@ fn dhall_to_tokenstream(
let b = dhall_to_tokenstream_bx(b, ctx);
quote! { BinOp(#o, #a, #b) }
}
- OptionalLit(t, es) => {
+ OptionalLit(t, e) => {
let t = option_to_tokenstream(t, ctx);
- let es = vec_to_tokenstream(es, ctx);
- quote! { OptionalLit(#t, #es) }
+ let e = option_to_tokenstream(e, ctx);
+ quote! { OptionalLit(#t, #e) }
}
ListLit(t, es) => {
let t = option_to_tokenstream(t, ctx);
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 05:12:13 +0000