From 711164a7a24ab832006b72cac162e78cf434861a Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 4 Aug 2019 11:11:37 +0200
Subject: Remove old-style optional literals
---
dhall/src/phase/binary.rs | 16 +++++++++-------
dhall/src/phase/normalize.rs | 10 +++-------
dhall/src/phase/typecheck.rs | 27 ++++-----------------------
3 files changed, 16 insertions(+), 37 deletions(-)
(limited to 'dhall')
diff --git a/dhall/src/phase/binary.rs b/dhall/src/phase/binary.rs
index 874b4fb..dcf60bb 100644
--- a/dhall/src/phase/binary.rs
+++ b/dhall/src/phase/binary.rs
@@ -115,18 +115,22 @@ fn cbor_value_to_dhall(
.collect::<Result<Vec<_>, _>>()?;
NEListLit(rest)
}
- [U64(5), t] => {
- let t = cbor_value_to_dhall(&t)?;
- OldOptionalLit(None, t)
- }
[U64(5), Null, x] => {
let x = cbor_value_to_dhall(&x)?;
SomeLit(x)
}
+ // Old-style optional literals
+ [U64(5), t] => {
+ let t = cbor_value_to_dhall(&t)?;
+ App(rc(ExprF::Builtin(Builtin::OptionalNone)), t)
+ }
[U64(5), t, x] => {
let x = cbor_value_to_dhall(&x)?;
let t = cbor_value_to_dhall(&t)?;
- OldOptionalLit(Some(x), t)
+ Annot(
+ rc(SomeLit(x)),
+ rc(App(rc(ExprF::Builtin(Builtin::Optional)), t)),
+ )
}
[U64(6), x, y] => {
let x = cbor_value_to_dhall(&x)?;
@@ -460,8 +464,6 @@ where
)
}
Annot(x, y) => ser_seq!(ser; tag(26), expr(x), expr(y)),
- OldOptionalLit(None, t) => ser_seq!(ser; tag(5), expr(t)),
- OldOptionalLit(Some(x), t) => ser_seq!(ser; tag(5), expr(t), expr(x)),
SomeLit(x) => ser_seq!(ser; tag(5), null(), expr(x)),
EmptyListLit(x) => ser_seq!(ser; tag(4), expr(x)),
NEListLit(xs) => ser.collect_seq(
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 35d32cb..f3684d1 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -611,9 +611,9 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
use Value::{
- BoolLit, DoubleLit, EmptyListLit, EmptyOptionalLit, IntegerLit, Lam,
- NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
- TextLit, UnionConstructor, UnionLit, UnionType,
+ BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam, NEListLit,
+ NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType, TextLit,
+ UnionConstructor, UnionLit, UnionType,
};
let ret = match expr {
@@ -639,10 +639,6 @@ pub fn normalize_one_layer(expr: ExprF<Thunk, X>) -> Value {
ExprF::NaturalLit(n) => Ret::Value(NaturalLit(n)),
ExprF::IntegerLit(n) => Ret::Value(IntegerLit(n)),
ExprF::DoubleLit(n) => Ret::Value(DoubleLit(n)),
- ExprF::OldOptionalLit(None, t) => {
- Ret::Value(EmptyOptionalLit(TypeThunk::from_thunk(t)))
- }
- ExprF::OldOptionalLit(Some(e), _) => Ret::Value(NEOptionalLit(e)),
ExprF::SomeLit(e) => Ret::Value(NEOptionalLit(e)),
ExprF::EmptyListLit(t) => {
Ret::Value(EmptyListLit(TypeThunk::from_thunk(t)))
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index efdc2bb..8551503 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -329,9 +329,7 @@ fn type_with(
ctx: &TypecheckContext,
e: SubExpr<Span, Normalized>,
) -> Result<Typed, TypeError> {
- use dhall_syntax::ExprF::{
- Annot, App, Embed, Lam, Let, OldOptionalLit, Pi, SomeLit, Var,
- };
+ use dhall_syntax::ExprF::{Annot, Embed, Lam, Let, Pi, Var};
use Ret::*;
Ok(match e.as_ref() {
@@ -364,18 +362,6 @@ fn type_with(
let v = type_with(ctx, v)?;
return type_with(&ctx.insert_value(x, v.clone())?, e.clone());
}
- OldOptionalLit(None, t) => {
- let none = SubExpr::from_builtin(Builtin::OptionalNone);
- let e = e.rewrap(App(none, t.clone()));
- return type_with(ctx, e);
- }
- OldOptionalLit(Some(x), t) => {
- let optional = SubExpr::from_builtin(Builtin::Optional);
- let x = x.rewrap(SomeLit(x.clone()));
- let t = t.rewrap(App(optional, t.clone()));
- let e = e.rewrap(Annot(x, t));
- return type_with(ctx, e);
- }
Embed(p) => p.clone().into_typed(),
Var(var) => match ctx.lookup(&var) {
Some(typed) => typed,
@@ -423,12 +409,9 @@ fn type_last_layer(
let mkerr = |msg: TypeMessage| TypeError::new(ctx, msg);
match e {
- Lam(_, _, _)
- | Pi(_, _, _)
- | Let(_, _, _, _)
- | OldOptionalLit(_, _)
- | Embed(_)
- | Var(_) => unreachable!(),
+ Lam(_, _, _) | Pi(_, _, _) | Let(_, _, _, _) | Embed(_) | Var(_) => {
+ unreachable!()
+ }
App(f, a) => {
let tf = f.get_type()?;
let (x, tx, tb) = match &tf.to_value() {
@@ -1296,8 +1279,6 @@ mod spec_tests {
ti_success!(ti_success_unit_NaturalShow, "unit/NaturalShow");
ti_success!(ti_success_unit_NaturalToInteger, "unit/NaturalToInteger");
ti_success!(ti_success_unit_None, "unit/None");
- ti_success!(ti_success_unit_OldOptionalNone, "unit/OldOptionalNone");
- ti_success!(ti_success_unit_OldOptionalTrue, "unit/OldOptionalTrue");
ti_success!(ti_success_unit_OperatorAnd, "unit/OperatorAnd");
ti_success!(ti_success_unit_OperatorAndNormalizeArguments, "unit/OperatorAndNormalizeArguments");
ti_success!(ti_success_unit_OperatorEqual, "unit/OperatorEqual");
--
cgit v1.2.3