summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/binary.rs2
-rw-r--r--dhall/src/normalize.rs13
-rw-r--r--dhall/src/typecheck.rs8
-rw-r--r--dhall_core/src/core.rs4
-rw-r--r--dhall_core/src/parser.rs2
-rw-r--r--dhall_core/src/printer.rs11
-rw-r--r--dhall_core/src/visitor.rs3
-rw-r--r--dhall_generator/src/quote.rs7
8 files changed, 15 insertions, 35 deletions
diff --git a/dhall/src/binary.rs b/dhall/src/binary.rs
index 62ebcf7..7ded3a5 100644
--- a/dhall/src/binary.rs
+++ b/dhall/src/binary.rs
@@ -111,7 +111,7 @@ fn cbor_value_to_dhall(data: &cbor::Value) -> Result<ParsedExpr, DecodeError> {
}
[U64(5), Null, x] => {
let x = cbor_value_to_dhall(&x)?;
- NEOptionalLit(x)
+ SomeLit(x)
}
[U64(5), t, x] => {
let x = cbor_value_to_dhall(&x)?;
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 9e7c531..f092c4d 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -366,10 +366,12 @@ impl WHNF {
WHNF::NaturalLit(n) => rc(ExprF::NaturalLit(n)),
WHNF::IntegerLit(n) => rc(ExprF::IntegerLit(n)),
WHNF::EmptyOptionalLit(n) => {
- rc(ExprF::EmptyOptionalLit(n.normalize().normalize_to_expr()))
+ WHNF::Expr(rc(ExprF::Builtin(Builtin::OptionalNone)))
+ .app(n.normalize())
+ .normalize_to_expr()
}
WHNF::NEOptionalLit(n) => {
- rc(ExprF::NEOptionalLit(n.normalize().normalize_to_expr()))
+ rc(ExprF::SomeLit(n.normalize().normalize_to_expr()))
}
WHNF::EmptyListLit(n) => {
rc(ExprF::EmptyListLit(n.normalize().normalize_to_expr()))
@@ -628,12 +630,7 @@ fn normalize_whnf(ctx: NormalizationContext, expr: InputSubExpr) -> WHNF {
ExprF::OldOptionalLit(Some(e), _) => {
WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
}
- ExprF::EmptyOptionalLit(e) => {
- WHNF::EmptyOptionalLit(Now::new(ctx, e.clone()))
- }
- ExprF::NEOptionalLit(e) => {
- WHNF::NEOptionalLit(Now::new(ctx, e.clone()))
- }
+ ExprF::SomeLit(e) => WHNF::NEOptionalLit(Now::new(ctx, e.clone())),
ExprF::EmptyListLit(e) => WHNF::EmptyListLit(Now::new(ctx, e.clone())),
ExprF::NEListLit(elts) => WHNF::NEListLit(
elts.iter()
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index ddb96da..b26f845 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -563,13 +563,7 @@ fn type_last_layer(
let e = dhall::subexpr!(Some x : Optional t);
Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned()))
}
- EmptyOptionalLit(t) => {
- let t = t.normalize();
- ensure_simple_type!(t, mkerr(InvalidOptionalType(t)));
- let t = t.embed();
- Ok(RetExpr(dhall::expr!(Optional t)))
- }
- NEOptionalLit(x) => {
+ SomeLit(x) => {
let tx = x.get_type_move()?;
ensure_simple_type!(
tx,
diff --git a/dhall_core/src/core.rs b/dhall_core/src/core.rs
index 9a8acc2..fa6fca4 100644
--- a/dhall_core/src/core.rs
+++ b/dhall_core/src/core.rs
@@ -180,10 +180,8 @@ pub enum ExprF<SubExpr, Label, Note, Embed> {
/// `[] : Optional a`
/// `[x] : Optional a`
OldOptionalLit(Option<SubExpr>, SubExpr),
- /// `None t`
- EmptyOptionalLit(SubExpr),
/// `Some e`
- NEOptionalLit(SubExpr),
+ SomeLit(SubExpr),
/// `{ k1 : t1, k2 : t1 }`
RecordType(BTreeMap<Label, SubExpr>),
/// `{ k1 = v1, k2 = v2 }`
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 31249a9..ba15bae 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -754,7 +754,7 @@ make_parser! {
children!(
[expression(e)] => e,
[Some_(()), expression(e)] => {
- spanned(span, NEOptionalLit(rc(e)))
+ spanned(span, SomeLit(rc(e)))
},
[merge(()), expression(x), expression(y)] => {
spanned(span, Merge(rc(x), rc(y), None))
diff --git a/dhall_core/src/printer.rs b/dhall_core/src/printer.rs
index ea291a9..c4bad71 100644
--- a/dhall_core/src/printer.rs
+++ b/dhall_core/src/printer.rs
@@ -38,10 +38,7 @@ impl<SE: Display + Clone, N, E: Display> Display for ExprF<SE, Label, N, E> {
OldOptionalLit(Some(x), t) => {
write!(f, "[{}] : Optional {}", x, t)?;
}
- EmptyOptionalLit(t) => {
- write!(f, "None {}", t)?;
- }
- NEOptionalLit(e) => {
+ SomeLit(e) => {
write!(f, "Some {}", e)?;
}
Merge(a, b, c) => {
@@ -159,8 +156,7 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
| EmptyListLit(_)
| NEListLit(_)
| OldOptionalLit(_, _)
- | EmptyOptionalLit(_)
- | NEOptionalLit(_)
+ | SomeLit(_)
| Merge(_, _, _)
| Annot(_, _)
if phase > Base =>
@@ -200,8 +196,7 @@ impl<S: Clone, A: Display + Clone> Expr<S, A> {
),
EmptyListLit(t) => EmptyListLit(t.phase(Import)),
OldOptionalLit(x, t) => OldOptionalLit(x, t.phase(Import)),
- EmptyOptionalLit(t) => EmptyOptionalLit(t.phase(Import)),
- NEOptionalLit(e) => NEOptionalLit(e.phase(Import)),
+ SomeLit(e) => SomeLit(e.phase(Import)),
ExprF::App(f, a) => ExprF::App(f.phase(Import), a.phase(Import)),
Field(a, b) => Field(a.phase(Primitive), b),
Projection(e, ls) => Projection(e.phase(Primitive), ls),
diff --git a/dhall_core/src/visitor.rs b/dhall_core/src/visitor.rs
index c15aacd..caaefce 100644
--- a/dhall_core/src/visitor.rs
+++ b/dhall_core/src/visitor.rs
@@ -153,8 +153,7 @@ where
opt(x, |e| v.visit_subexpr(e))?,
v.visit_subexpr(t)?,
),
- EmptyOptionalLit(t) => EmptyOptionalLit(v.visit_subexpr(t)?),
- NEOptionalLit(e) => NEOptionalLit(v.visit_subexpr(e)?),
+ SomeLit(e) => SomeLit(v.visit_subexpr(e)?),
RecordType(kts) => RecordType(btmap(kts, v)?),
RecordLit(kvs) => RecordLit(btmap(kvs, v)?),
UnionType(kts) => UnionType(btoptmap(kts, v)?),
diff --git a/dhall_generator/src/quote.rs b/dhall_generator/src/quote.rs
index 38910a8..c588eda 100644
--- a/dhall_generator/src/quote.rs
+++ b/dhall_generator/src/quote.rs
@@ -66,11 +66,8 @@ where
BoolLit(b) => {
quote! { dhall_core::ExprF::BoolLit(#b) }
}
- EmptyOptionalLit(x) => {
- quote! { dhall_core::ExprF::EmptyOptionalLit(#x) }
- }
- NEOptionalLit(x) => {
- quote! { dhall_core::ExprF::NEOptionalLit(#x) }
+ SomeLit(x) => {
+ quote! { dhall_core::ExprF::SomeLit(#x) }
}
EmptyListLit(t) => {
quote! { dhall_core::ExprF::EmptyListLit(#t) }
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 23:38:43 +0000