From ac7e39a752c41c06155e27e84404c67c1341065d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 25 Jun 2020 14:28:48 +0100 Subject: spec!: remove Optional/build and Optional/fold --- dhall/src/builtins.rs | 43 ---------------------- dhall/src/syntax/text/dhall.abnf | 7 ++-- dhall/tests/parser/success/builtinsB.txt | 2 +- .../unit/LetWithNonterminatingAnnotation.txt | 12 ++++++ .../failure/unit/RemovedBuiltinOptionalBuild.txt | 6 +++ .../failure/unit/RemovedBuiltinOptionalFold.txt | 6 +++ 6 files changed, 28 insertions(+), 48 deletions(-) create mode 100644 dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt create mode 100644 dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt create mode 100644 dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt (limited to 'dhall') diff --git a/dhall/src/builtins.rs b/dhall/src/builtins.rs index 67929a0..16d656f 100644 --- a/dhall/src/builtins.rs +++ b/dhall/src/builtins.rs @@ -42,8 +42,6 @@ pub enum Builtin { ListLast, ListIndexed, ListReverse, - OptionalFold, - OptionalBuild, TextShow, } @@ -79,8 +77,6 @@ impl Builtin { "List/last" => Some(ListLast), "List/indexed" => Some(ListIndexed), "List/reverse" => Some(ListReverse), - "Optional/fold" => Some(OptionalFold), - "Optional/build" => Some(OptionalBuild), "Text/show" => Some(TextShow), _ => None, } @@ -245,22 +241,6 @@ pub fn type_of_builtin(b: Builtin) -> Hir { forall (a: Type) -> (List a) -> List a ), - OptionalBuild => make_type!( - forall (a: Type) -> - (forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional) -> - Optional a - ), - OptionalFold => make_type!( - forall (a: Type) -> - (Optional a) -> - forall (optional: Type) -> - forall (just: a -> optional) -> - forall (nothing: optional) -> - optional - ), OptionalNone => make_type!( forall (A: Type) -> Optional A ), @@ -510,27 +490,6 @@ fn apply_builtin(b: Builtin, args: Vec, env: NzEnv) -> NirKind { } _ => Ret::DoneAsIs, }, - (Builtin::OptionalBuild, [t, f]) => { - let optional_t = - Nir::from_builtin(Builtin::Optional).app(t.clone()); - Ret::Nir( - f.app(optional_t) - .app( - make_closure(make_closure!( - λ(T : Type) -> - λ(a : var(T)) -> - Some(var(a)) - )) - .app(t.clone()), - ) - .app(EmptyOptionalLit(t.clone()).into_nir()), - ) - } - (Builtin::OptionalFold, [_, v, _, just, nothing]) => match &*v.kind() { - EmptyOptionalLit(_) => Ret::Nir(nothing.clone()), - NEOptionalLit(x) => Ret::Nir(just.app(x.clone())), - _ => Ret::DoneAsIs, - }, (Builtin::NaturalBuild, [f]) => Ret::Nir( f.app(Nir::from_builtin(Builtin::Natural)) .app(make_closure(make_closure!( @@ -600,8 +559,6 @@ impl std::fmt::Display for Builtin { ListLast => "List/last", ListIndexed => "List/indexed", ListReverse => "List/reverse", - OptionalFold => "Optional/fold", - OptionalBuild => "Optional/build", TextShow => "Text/show", }) } diff --git a/dhall/src/syntax/text/dhall.abnf b/dhall/src/syntax/text/dhall.abnf index 173209c..37ec43b 100644 --- a/dhall/src/syntax/text/dhall.abnf +++ b/dhall/src/syntax/text/dhall.abnf @@ -387,6 +387,9 @@ keyword = / forall-keyword / with +; Note that there is a corresponding parser test in +; `tests/parser/success/builtinsA.dhall`. Please update it when +; you modify this `builtin` rule. builtin = Natural-fold / Natural-build @@ -408,8 +411,6 @@ builtin = / List-last / List-indexed / List-reverse - / Optional-fold - / Optional-build / Text-show / Bool / True @@ -462,8 +463,6 @@ List-head = %x4c.69.73.74.2f.68.65.61.64 List-last = %x4c.69.73.74.2f.6c.61.73.74 List-indexed = %x4c.69.73.74.2f.69.6e.64.65.78.65.64 List-reverse = %x4c.69.73.74.2f.72.65.76.65.72.73.65 -Optional-fold = %x4f.70.74.69.6f.6e.61.6c.2f.66.6f.6c.64 -Optional-build = %x4f.70.74.69.6f.6e.61.6c.2f.62.75.69.6c.64 Text-show = %x54.65.78.74.2f.73.68.6f.77 ; Operators diff --git a/dhall/tests/parser/success/builtinsB.txt b/dhall/tests/parser/success/builtinsB.txt index 4e3ed79..1005949 100644 --- a/dhall/tests/parser/success/builtinsB.txt +++ b/dhall/tests/parser/success/builtinsB.txt @@ -1 +1 @@ -λ(x : { field0 : Bool, field1 : Optional (Optional Bool), field2 : Natural, field3 : Integer, field4 : Double, field5 : Text, field6 : List (List Bool) }) → { field00 = Natural/fold, field01 = Natural/build, field02 = Natural/isZero, field03 = Natural/even, field04 = Natural/odd, field05 = Natural/toInteger, field06 = Natural/show, field07 = Integer/show, field08 = Double/show, field09 = List/build, field10 = List/fold, field11 = List/length, field12 = List/head, field13 = List/last, field14 = List/indexed, field15 = List/reverse, field16 = Optional/fold, field17 = Optional/build, field18 = True, field19 = False, field20 = None } +[Natural/fold, Natural/build, Natural/isZero, Natural/even, Natural/odd, Natural/toInteger, Natural/show, Integer/toDouble, Integer/show, Integer/negate, Integer/clamp, Natural/subtract, Double/show, List/build, List/fold, List/length, List/head, List/last, List/indexed, List/reverse, Text/show, Bool, True, False, Optional, None, Natural, Integer, Double, Text, List, Type, Kind, Sort] diff --git a/dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt b/dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt new file mode 100644 index 0000000..6e360da --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt @@ -0,0 +1,12 @@ +Type error: error: expected function, found `Natural` + --> :6:25 + | + 1 | -- When you check if an inferred type is equivalent to an annotation, + 2 | -- you must alpha-beta-normalize both sides first. But it is not safe + 3 | -- to beta-normalise an expression which hasn't first been + 4 | -- typechecked. +... +10 | let a +11 | : (λ(x : Natural) → x x) (λ(x : Natural) → x x) + | ^ function application requires a function + | diff --git a/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt new file mode 100644 index 0000000..e4e285c --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt @@ -0,0 +1,6 @@ +Type error: error: unbound variable ``Optional/build`` + --> :1:1 + | +1 | Optional/build + | ^^^^^^^^^^^^^^ not found in this scope + | diff --git a/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt new file mode 100644 index 0000000..3d6c6aa --- /dev/null +++ b/dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt @@ -0,0 +1,6 @@ +Type error: error: unbound variable ``Optional/fold`` + --> :1:1 + | +1 | Optional/fold + | ^^^^^^^^^^^^^ not found in this scope + | -- cgit v1.2.3