summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/binary.rs6
-rw-r--r--dhall/src/normalize.rs25
-rw-r--r--dhall/src/typecheck.rs28
-rw-r--r--dhall_core/src/core.rs10
-rw-r--r--dhall_core/src/parser.rs44
-rw-r--r--dhall_generator/src/lib.rs22
6 files changed, 61 insertions, 74 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 9099afc..e8fcdab 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -105,16 +105,16 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
}
[U64(5), t] => {
let t = cbor_value_to_dhall(&t)?;
- OptionalLit(Some(t), None)
+ EmptyOptionalLit(t)
}
[U64(5), Null, x] => {
let x = cbor_value_to_dhall(&x)?;
- OptionalLit(None, Some(x))
+ NEOptionalLit(x)
}
[U64(5), t, x] => {
let x = cbor_value_to_dhall(&x)?;
let t = cbor_value_to_dhall(&t)?;
- OptionalLit(Some(t), Some(x))
+ Annot(rc(NEOptionalLit(x)), t)
}
[U64(6), x, y] => {
let x = cbor_value_to_dhall(&x)?;
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 7eba0cc..65a9552 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -50,8 +50,8 @@ where
let evaled_arg = arg_to_eval.map(|i| args[i].as_ref());
let ret = match (b, evaled_arg, args.as_slice()) {
- (OptionalSome, _, [x, ..]) => rc(OptionalLit(None, Some(Rc::clone(x)))),
- (OptionalNone, _, [t, ..]) => rc(OptionalLit(Some(Rc::clone(t)), None)),
+ (OptionalSome, _, [x, ..]) => rc(NEOptionalLit(Rc::clone(x))),
+ (OptionalNone, _, [t, ..]) => rc(EmptyOptionalLit(Rc::clone(t))),
(NaturalIsZero, Some(NaturalLit(n)), _) => rc(BoolLit(*n == 0)),
(NaturalEven, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 == 0)),
(NaturalOdd, Some(NaturalLit(n)), _) => rc(BoolLit(*n % 2 != 0)),
@@ -64,16 +64,16 @@ where
(ListLength, Some(EmptyListLit(_)), _) => rc(NaturalLit(0)),
(ListLength, Some(NEListLit(ys)), _) => rc(NaturalLit(ys.len())),
(ListHead, Some(EmptyListLit(t)), _) => {
- rc(OptionalLit(Some(t.clone()), None))
+ rc(EmptyOptionalLit(t.clone()))
}
(ListHead, Some(NEListLit(ys)), _) => {
- rc(OptionalLit(None, ys.iter().cloned().next()))
+ rc(NEOptionalLit(ys.first().unwrap().clone()))
}
(ListLast, Some(EmptyListLit(t)), _) => {
- rc(OptionalLit(Some(t.clone()), None))
+ rc(EmptyOptionalLit(t.clone()))
}
(ListLast, Some(NEListLit(ys)), _) => {
- rc(OptionalLit(None, ys.iter().cloned().last()))
+ rc(NEOptionalLit(ys.last().unwrap().clone()))
}
(ListReverse, Some(EmptyListLit(t)), _) => rc(EmptyListLit(t.clone())),
(ListReverse, Some(NEListLit(ys)), _) => {
@@ -124,7 +124,7 @@ where
};
let a0 = Rc::clone(a0);
// TODO: use Embed to avoid reevaluating g
- break dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] : Optional a0) ([] : Optional a0));
+ break dhall_expr!((g (Optional a0)) (λ(x: a0) -> Some x) (None a0));
}
}
(ListFold, Some(EmptyListLit(_)), [_, _, _, _, nil, ..]) => {
@@ -144,7 +144,7 @@ where
// }
(
OptionalFold,
- Some(OptionalLit(_, Some(x))),
+ Some(NEOptionalLit(x)),
[_, _, _, just, _, ..],
) => {
let x = x.clone();
@@ -153,7 +153,7 @@ where
}
(
OptionalFold,
- Some(OptionalLit(_, None)),
+ Some(EmptyOptionalLit(_)),
[_, _, _, _, nothing, ..],
) => Rc::clone(nothing),
// // fold/build fusion
@@ -254,13 +254,6 @@ where
_ => rc(BoolIf(b, t.clone(), f.clone())),
}
}
- OptionalLit(t, es) => {
- if !es.is_none() {
- rc(OptionalLit(None, es.clone()))
- } else {
- rc(OptionalLit(t.clone(), es.clone()))
- }
- }
// TODO: interpolation
// TextLit(t) =>
BinOp(o, x, y) => {
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 15fb344..32ffe0e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -372,29 +372,17 @@ where
}
return Ok(dhall_expr!(List t));
}
- OptionalLit(t, xs) => {
- let mut iter = xs.iter();
- let t: Rc<Expr<_, _>> = match t {
- Some(t) => t.clone(),
- None => {
- let x = iter.next().unwrap();
- type_with(ctx, x.clone())?
- }
- };
-
+ EmptyOptionalLit(t) => {
+ let s = normalized_type_with(ctx, t.clone())?;
+ ensure_is_type(s, InvalidOptionalType(t.clone()))?;
+ let t = normalize(t.clone());
+ return Ok(dhall_expr!(Optional t));
+ }
+ NEOptionalLit(x) => {
+ let t: Rc<Expr<_, _>> = type_with(ctx, x.clone())?;
let s = normalized_type_with(ctx, t.clone())?;
ensure_is_type(s, InvalidOptionalType(t.clone()))?;
let t = normalize(t);
- for x in iter {
- let t2 = normalized_type_with(ctx, x.clone())?;
- if !prop_equal(t.as_ref(), t2.as_ref()) {
- return Err(mkerr(InvalidOptionalElement(
- t,
- x.clone(),
- t2,
- )));
- }
- }
return Ok(dhall_expr!(Optional t));
}
RecordType(kts) => {
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 1d733aa..52fc0cf 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -195,9 +195,10 @@ pub enum Expr<Note, Embed> {
EmptyListLit(SubExpr<Note, Embed>),
/// [x, y, z]
NEListLit(Vec<SubExpr<Note, Embed>>),
- /// `OptionalLit t [e] ~ [e] : Optional t`
- /// `OptionalLit t [] ~ [] : Optional t`
- OptionalLit(Option<SubExpr<Note, Embed>>, Option<SubExpr<Note, Embed>>),
+ /// None t
+ EmptyOptionalLit(SubExpr<Note, Embed>),
+ /// Some e
+ NEOptionalLit(SubExpr<Note, Embed>),
/// `Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }`
RecordType(BTreeMap<Label, SubExpr<Note, Embed>>),
/// `RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }`
@@ -346,7 +347,8 @@ where
BinOp(o, x, y) => BinOp(*o, map(x), map(y)),
EmptyListLit(t) => EmptyListLit(map(t)),
NEListLit(es) => NEListLit(vec(es)),
- OptionalLit(t, es) => OptionalLit(opt(t), opt(es)),
+ EmptyOptionalLit(t) => EmptyOptionalLit(map(t)),
+ NEOptionalLit(e) => NEOptionalLit(map(e)),
RecordType(kts) => RecordType(btmap(kts)),
RecordLit(kvs) => RecordLit(btmap(kvs)),
UnionType(kts) => UnionType(btmap(kts)),
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 3310bb9..b07094d 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -123,10 +123,10 @@ macro_rules! match_pair {
match_pair!(@make_child_match, ($($vars)*), ($($outer_acc)*), ($($acc)*, ParsedValue::$ty($x)), ($($rest_of_match)*) => $body, $($rest)*)
};
(@make_child_match, ($($vars:tt)*), ($($outer_acc:tt)*), (, $($acc:tt)*), ($(,)*) => $body:expr, $($rest:tt)*) => {
- match_pair!(@make_matches, ($($vars)*), ([$($acc)*] => { $body }, $($outer_acc)*), $($rest)*)
+ match_pair!(@make_matches, ($($vars)*), ($($outer_acc)* [$($acc)*] => { $body },), $($rest)*)
};
(@make_child_match, ($($vars:tt)*), ($($outer_acc:tt)*), (), ($(,)*) => $body:expr, $($rest:tt)*) => {
- match_pair!(@make_matches, ($($vars)*), ([] => { $body }, $($outer_acc)*), $($rest)*)
+ match_pair!(@make_matches, ($($vars)*), ($($outer_acc)* [] => { $body },), $($rest)*)
};
(@make_matches, ($($vars:tt)*), ($($acc:tt)*), [$($args:tt)*] => $body:expr, $($rest:tt)*) => {
@@ -469,17 +469,17 @@ make_parser! {
rule!(Optional<()>; raw_pair!(_) => ());
rule!(empty_collection<ParsedExpr> as expression; children!(
- [List(_), expression(y)] => {
- bx(Expr::EmptyListLit(y))
+ [List(_), expression(t)] => {
+ bx(Expr::EmptyListLit(t))
},
- [Optional(_), expression(y)] => {
- bx(Expr::OptionalLit(Some(y), None))
+ [Optional(_), expression(t)] => {
+ bx(Expr::EmptyOptionalLit(t))
},
));
rule!(non_empty_optional<ParsedExpr> as expression; children!(
- [expression(x), Optional(_), expression(z)] => {
- bx(Expr::OptionalLit(Some(z), Some(x)))
+ [expression(x), Optional(_), expression(t)] => {
+ rc(Expr::Annot(rc(Expr::NEOptionalLit(x)), t))
}
));
@@ -557,24 +557,36 @@ make_parser! {
));
rule!(annotated_expression<ParsedExpr> as expression; children!(
+ [expression(e)] => e,
[expression(e), expression(annot)] => {
bx(Expr::Annot(e, annot))
},
- [expression(e)] => e,
));
rule!(application_expression<ParsedExpr> as expression; children!(
- [expression(first), expression(rest..)] => {
- let rest: Vec<_> = rest.collect();
- if rest.is_empty() {
- first
- } else {
- bx(Expr::App(first, rest))
+ [expression(e)] => e,
+ [expression(first), expression(second)] => {
+ match first.as_ref() {
+ Expr::Builtin(Builtin::OptionalNone) =>
+ bx(Expr::EmptyOptionalLit(second)),
+ Expr::Builtin(Builtin::OptionalSome) =>
+ bx(Expr::NEOptionalLit(second)),
+ _ => bx(Expr::App(first, vec![second])),
}
- }
+ },
+ [expression(first), expression(second), expression(rest..)] => {
+ match first.as_ref() {
+ Expr::Builtin(Builtin::OptionalNone) =>
+ bx(Expr::App(bx(Expr::EmptyOptionalLit(second)), rest.collect())),
+ Expr::Builtin(Builtin::OptionalSome) =>
+ bx(Expr::App(bx(Expr::NEOptionalLit(second)), rest.collect())),
+ _ => bx(Expr::App(first, std::iter::once(second).chain(rest).collect())),
+ }
+ },
));
rule!(selector_expression_raw<ParsedExpr> as expression; children!(
+ [expression(e)] => e,
[expression(first), selector_raw(rest..)] => {
rest.fold(first, |acc, e| bx(Expr::Field(acc, e)))
}
diff --git a/dhall_generator/src/lib.rs b/dhall_generator/src/lib.rs
index a246818..328bc3e 100644
--- a/dhall_generator/src/lib.rs
+++ b/dhall_generator/src/lib.rs
@@ -63,10 +63,13 @@ fn dhall_to_tokenstream(
NaturalLit(n) => {
quote! { NaturalLit(#n) }
}
- OptionalLit(t, e) => {
- let t = option_to_tokenstream(t, ctx);
- let e = option_to_tokenstream(e, ctx);
- quote! { OptionalLit(#t, #e) }
+ EmptyOptionalLit(x) => {
+ let x = dhall_to_tokenstream_bx(x, ctx);
+ quote! { EmptyOptionalLit(#x) }
+ }
+ NEOptionalLit(x) => {
+ let x = dhall_to_tokenstream_bx(x, ctx);
+ quote! { NEOptionalLit(#x) }
}
EmptyListLit(t) => {
let t = dhall_to_tokenstream_bx(t, ctx);
@@ -153,17 +156,6 @@ fn map_to_tokenstream(
} }
}
-fn option_to_tokenstream(
- e: &Option<DhallExpr>,
- ctx: &Context<Label, ()>,
-) -> TokenStream {
- let e = e.as_ref().map(|x| dhall_to_tokenstream_bx(x, ctx));
- match e {
- Some(x) => quote! { Some(#x) },
- None => quote! { None },
- }
-}
-
fn vec_to_tokenstream(
e: &Vec<DhallExpr>,
ctx: &Context<Label, ()>,
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 12:12:40 +0000