summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--CHANGELOG.md1
m---------dhall-lang0
-rw-r--r--dhall/src/builtins.rs43
-rw-r--r--dhall/src/syntax/text/dhall.abnf7
-rw-r--r--dhall/tests/parser/success/builtinsB.txt2
-rw-r--r--dhall/tests/type-inference/failure/unit/LetWithNonterminatingAnnotation.txt12
-rw-r--r--dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalBuild.txt6
-rw-r--r--dhall/tests/type-inference/failure/unit/RemovedBuiltinOptionalFold.txt6
8 files changed, 29 insertions, 48 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd042c3..8854a31 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2,6 +2,7 @@
#### [Unreleased]
+- BREAKING CHANGE: Remove Optional/build and Optional/fold
- BREAKING CHANGE: Remove the ability to quote paths in URLs
- Allow quoted labels to be empty
- Support Dhall v16.0.0
diff --git a/dhall-lang b/dhall-lang
-Subproject 9358ffa9c8241b0d8446d46010318758b0df38c
+Subproject 549470527dcc0ee59253708c6ac23c0cee45509
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<Nir>, 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`
+ --> <current file>: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``
+ --> <current file>: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``
+ --> <current file>:1:1
+ |
+1 | Optional/fold
+ | ^^^^^^^^^^^^^ not found in this scope
+ |
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-22 21:37:12 +0000