summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/builtins.rs43
-rw-r--r--dhall/src/operations/kind.rs4
-rw-r--r--dhall/src/semantics/tck/typecheck.rs20
-rw-r--r--dhall/src/syntax/ast/span.rs6
-rw-r--r--dhall/src/syntax/text/dhall.abnf66
-rw-r--r--dhall/src/syntax/text/dhall.pest.visibility10
-rw-r--r--dhall/src/syntax/text/parser.rs50
-rw-r--r--dhall/src/syntax/text/printer.rs4
8 files changed, 68 insertions, 135 deletions
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/operations/kind.rs b/dhall/src/operations/kind.rs
index 5415637..0ee9671 100644
--- a/dhall/src/operations/kind.rs
+++ b/dhall/src/operations/kind.rs
@@ -6,6 +6,8 @@ use crate::syntax::{trivial_result, Label};
// pretty-printing to work correctly
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub enum BinOp {
+ /// x === y
+ Equivalence,
/// `x ? y`
ImportAlt,
/// `x || y`
@@ -30,8 +32,6 @@ pub enum BinOp {
BoolEQ,
/// `x != y`
BoolNE,
- /// x === y
- Equivalence,
}
/// Operations
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 361e1b4..d21c7ce 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -137,30 +137,20 @@ fn type_one_layer(
Type::from_const(k)
}
ExprKind::UnionType(kts) => {
- // Check that all types are the same const
- let mut k = None;
+ // An empty union type has type Type;
+ // an union type with only unary variants also has type Type
+ let mut k = Const::Type;
for t in kts.values() {
if let Some(t) = t {
- let c = match t.ty().as_const() {
- Some(c) => c,
+ match t.ty().as_const() {
+ Some(c) => k = max(k, c),
None => {
return mk_span_err(t.span(), "InvalidVariantType")
}
- };
- match k {
- None => k = Some(c),
- Some(k) if k == c => {}
- _ => {
- return mk_span_err(t.span(), "InvalidVariantType")
- }
}
}
}
- // An empty union type has type Type;
- // an union type with only unary variants also has type Type
- let k = k.unwrap_or(Const::Type);
-
Type::from_const(k)
}
ExprKind::Op(op) => typecheck_operation(env, span, op)?,
diff --git a/dhall/src/syntax/ast/span.rs b/dhall/src/syntax/ast/span.rs
index e250602..ab3279b 100644
--- a/dhall/src/syntax/ast/span.rs
+++ b/dhall/src/syntax/ast/span.rs
@@ -66,6 +66,12 @@ impl Span {
end: max(x.end, y.end),
})
}
+ (Parsed(_), Parsed(_)) => panic!(
+ "Tried to union incompatible spans: {:?} and {:?}",
+ self, other
+ ),
+ (Parsed(x), _) => Parsed(x.clone()),
+ (_, Parsed(x)) => Parsed(x.clone()),
_ => panic!(
"Tried to union incompatible spans: {:?} and {:?}",
self, other
diff --git a/dhall/src/syntax/text/dhall.abnf b/dhall/src/syntax/text/dhall.abnf
index 1c3a980..37ec43b 100644
--- a/dhall/src/syntax/text/dhall.abnf
+++ b/dhall/src/syntax/text/dhall.abnf
@@ -206,7 +206,7 @@ quoted-label-char =
; %x60 = '`'
/ %x61-7E
-quoted-label = 1*quoted-label-char
+quoted-label = *quoted-label-char
; NOTE: Dhall does not support Unicode labels, mainly to minimize the potential
; for code obfuscation
@@ -370,7 +370,9 @@ NaN = %x4e.61.4e
Some = %x53.6f.6d.65
toMap = %x74.6f.4d.61.70
assert = %x61.73.73.65.72.74
-forall = %x2200 / %x66.6f.72.61.6c.6c ; "∀" / "forall"
+forall-keyword = %x66.6f.72.61.6c.6c ; "forall"
+forall-symbol = %x2200 ; Unicode FOR ALL
+forall = forall-symbol / forall-keyword
with = %x77.69.74.68
; Unused rule that could be used as negative lookahead in the
@@ -382,9 +384,12 @@ keyword =
/ assert / as
/ Infinity / NaN
/ merge / Some / toMap
- / forall
+ / 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
@@ -406,8 +411,6 @@ builtin =
/ List-last
/ List-indexed
/ List-reverse
- / Optional-fold
- / Optional-build
/ Text-show
/ Bool
/ True
@@ -460,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
@@ -580,7 +581,6 @@ scheme = %x68.74.74.70 [ %x73 ] ; "http" [ "s" ]
; NOTE: This does not match the official grammar for a URI. Specifically:
;
-; * path segments may be quoted instead of using percent-encoding
; * this does not support fragment identifiers, which have no meaning within
; Dhall expressions and do not affect import resolution
; * the characters "(" ")" and "," are not included in the `sub-delims` rule:
@@ -593,13 +593,9 @@ scheme = %x68.74.74.70 [ %x73 ] ; "http" [ "s" ]
;
; Reserved characters in quoted path components should be percent-encoded
; according to https://tools.ietf.org/html/rfc3986#section-2
-http-raw = scheme "://" authority url-path [ "?" query ]
+http-raw = scheme "://" authority path-abempty [ "?" query ]
-; Temporary rule to allow old-style `path-component`s and RFC3986 `segment`s in
-; the same grammar. Eventually we can just use `path-abempty` from the same
-; RFC. See issue #581
-
-url-path = *(path-component / "/" segment)
+path-abempty = *( "/" segment )
; NOTE: Backtrack if parsing the optional user info prefix fails
authority = [ userinfo "@" ] host [ ":" port ]
@@ -757,6 +753,11 @@ expression =
; NOTE: Backtrack if parsing this alternative fails
/ operator-expression whsp arrow whsp expression
+ ; "a with x = b"
+ ;
+ ; NOTE: Backtrack if parsing this alternative fails
+ / with-expression
+
; "merge e1 e2 : t"
;
; NOTE: Backtrack if parsing this alternative fails since we can't tell
@@ -792,9 +793,16 @@ let-binding = let whsp1 nonreserved-label whsp [ ":" whsp1 expression whsp ] "="
empty-list-literal =
"[" whsp [ "," whsp ] "]" whsp ":" whsp1 application-expression
-operator-expression = import-alt-expression
+with-expression =
+ import-expression 1*(whsp1 with whsp1 with-clause)
+
+with-clause =
+ any-label-or-some *(whsp "." whsp any-label-or-some) whsp "=" whsp operator-expression
+
+operator-expression = equivalent-expression
; Nonempty-whitespace to disambiguate `http://a/a?a`
+equivalent-expression = import-alt-expression *(whsp equivalent whsp import-alt-expression)
import-alt-expression = or-expression *(whsp "?" whsp1 or-expression)
or-expression = plus-expression *(whsp "||" whsp plus-expression)
; Nonempty-whitespace to disambiguate `f +2`
@@ -807,13 +815,7 @@ prefer-expression = combine-types-expression *(whsp prefer whsp combine-t
combine-types-expression = times-expression *(whsp combine-types whsp times-expression)
times-expression = equal-expression *(whsp "*" whsp equal-expression)
equal-expression = not-equal-expression *(whsp "==" whsp not-equal-expression)
-not-equal-expression = equivalent-expression *(whsp "!=" whsp equivalent-expression)
-equivalent-expression = with-expression *(whsp equivalent whsp with-expression)
-
-with-expression = application-expression *(whsp1 with whsp1 with-clause)
-
-with-clause =
- any-label-or-some *(whsp "." whsp any-label-or-some) whsp "=" whsp application-expression
+not-equal-expression = application-expression *(whsp "!=" whsp application-expression)
; Import expressions need to be separated by some whitespace, otherwise there
@@ -890,11 +892,9 @@ primitive-expression =
record-type-or-literal =
empty-record-literal
- / non-empty-record-type-or-literal
- / empty-record-type
+ / [non-empty-record-type-or-literal]
empty-record-literal = "="
-empty-record-type = ""
non-empty-record-type-or-literal =
(non-empty-record-type / non-empty-record-literal)
@@ -907,22 +907,18 @@ record-type-entry = any-label-or-some whsp ":" whsp1 expression
non-empty-record-literal =
record-literal-entry *(whsp "," whsp record-literal-entry)
+; If the `record-literal-normal-entry` is absent, that represents a punned
+; record entry, such as in `{ x }`, which is a short-hand for `{ x = x }`
record-literal-entry =
- any-label-or-some (record-literal-normal-entry / record-literal-punned-entry)
+ any-label-or-some [record-literal-normal-entry]
record-literal-normal-entry =
*(whsp "." whsp any-label-or-some) whsp "=" whsp expression
-record-literal-punned-entry = ""
-
+; If the `union-type-entry` is absent, that represents an empty union
+; alternative, such as in `< Heads | Tails >`
union-type =
- non-empty-union-type
- / empty-union-type
-
-empty-union-type = ""
-
-non-empty-union-type =
- union-type-entry *(whsp "|" whsp union-type-entry)
+ [union-type-entry *(whsp "|" whsp union-type-entry)]
; x : Natural
; x
diff --git a/dhall/src/syntax/text/dhall.pest.visibility b/dhall/src/syntax/text/dhall.pest.visibility
index b2114ce..6de7dd2 100644
--- a/dhall/src/syntax/text/dhall.pest.visibility
+++ b/dhall/src/syntax/text/dhall.pest.visibility
@@ -120,7 +120,7 @@ home_path
absolute_path
scheme
http_raw
-url_path
+path_abempty
authority
# userinfo
# host
@@ -178,19 +178,15 @@ selector
labels
# type_selector
primitive_expression
-# record_type_or_literal
+record_type_or_literal
empty_record_literal
-empty_record_type
-non_empty_record_type_or_literal
+# non_empty_record_type_or_literal
non_empty_record_type
record_type_entry
non_empty_record_literal
record_literal_entry
-# record_literal_punned_entry
# record_literal_normal_entry
union_type
-empty_union_type
-# non_empty_union_type
union_type_entry
non_empty_list_literal
# complete_expression
diff --git a/dhall/src/syntax/text/parser.rs b/dhall/src/syntax/text/parser.rs
index 1e1449c..06c1ac3 100644
--- a/dhall/src/syntax/text/parser.rs
+++ b/dhall/src/syntax/text/parser.rs
@@ -130,6 +130,7 @@ lazy_static::lazy_static! {
use Rule::*;
// In order of precedence
let operators = vec![
+ equivalent,
import_alt,
bool_or,
natural_plus,
@@ -142,7 +143,6 @@ lazy_static::lazy_static! {
natural_times,
bool_eq,
bool_ne,
- equivalent,
];
PrecClimber::new(
operators
@@ -514,14 +514,14 @@ impl DhallParser {
fn http_raw(input: ParseInput) -> ParseResult<URL<Expr>> {
Ok(match_nodes!(input.into_children();
- [scheme(sch), authority(auth), url_path(p)] => URL {
+ [scheme(sch), authority(auth), path_abempty(p)] => URL {
scheme: sch,
authority: auth,
path: p,
query: None,
headers: None,
},
- [scheme(sch), authority(auth), url_path(p), query(q)] => URL {
+ [scheme(sch), authority(auth), path_abempty(p), query(q)] => URL {
scheme: sch,
authority: auth,
path: p,
@@ -531,10 +531,10 @@ impl DhallParser {
))
}
- fn url_path(input: ParseInput) -> ParseResult<FilePath> {
+ fn path_abempty(input: ParseInput) -> ParseResult<FilePath> {
Ok(match_nodes!(input.into_children();
- [path_component(components)..] => {
- let mut file_path: Vec<_> = components.collect();
+ [segment(segments)..] => {
+ let mut file_path: Vec<_> = segments.collect();
// An empty path normalizes to "/"
if file_path.is_empty() {
file_path = vec!["".to_owned()];
@@ -548,7 +548,6 @@ impl DhallParser {
Ok(input.as_str().to_owned())
}
- #[alias(path_component)]
fn segment(input: ParseInput) -> ParseResult<String> {
Ok(input.as_str().to_string())
}
@@ -909,26 +908,19 @@ impl DhallParser {
))
}
- #[alias(record_type_or_literal)]
- fn empty_record_literal(input: ParseInput) -> ParseResult<UnspannedExpr> {
- Ok(RecordLit(Default::default()))
- }
-
- #[alias(record_type_or_literal)]
- fn empty_record_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
- Ok(RecordType(Default::default()))
- }
-
- #[alias(record_type_or_literal)]
- fn non_empty_record_type_or_literal(
- input: ParseInput,
- ) -> ParseResult<UnspannedExpr> {
+ fn record_type_or_literal(input: ParseInput) -> ParseResult<UnspannedExpr> {
Ok(match_nodes!(input.children();
+ [empty_record_literal(_)] => RecordLit(Default::default()),
[non_empty_record_type(map)] => RecordType(map),
[non_empty_record_literal(map)] => RecordLit(map),
+ [] => RecordType(Default::default()),
))
}
+ fn empty_record_literal(input: ParseInput) -> ParseResult<()> {
+ Ok(())
+ }
+
fn non_empty_record_type(
input: ParseInput,
) -> ParseResult<BTreeMap<Label, Expr>> {
@@ -997,8 +989,7 @@ impl DhallParser {
}
fn union_type(input: ParseInput) -> ParseResult<UnspannedExpr> {
- let map = match_nodes!(input.children();
- [empty_union_type(_)] => Default::default(),
+ Ok(match_nodes!(input.children();
[union_type_entry(entries)..] => {
let mut map = BTreeMap::default();
for (l, t) in entries {
@@ -1015,14 +1006,9 @@ impl DhallParser {
}
}
}
- map
+ UnionType(map)
},
- );
- Ok(UnionType(map))
- }
-
- fn empty_union_type(_input: ParseInput) -> ParseResult<()> {
- Ok(())
+ ))
}
fn union_type_entry(
@@ -1065,7 +1051,7 @@ pub fn parse_expr(input_str: &str) -> ParseResult<Expr> {
}
#[test]
-#[ignore]
+#[cfg_attr(windows, ignore)]
// Check that the local copy of the grammar file is in sync with the one from dhall-lang.
fn test_grammar_files_in_sync() {
use std::process::Command;
@@ -1079,8 +1065,8 @@ fn test_grammar_files_in_sync() {
.arg("--ignore-space-change")
.arg("--color")
.arg("--")
- .arg(spec_abnf_path)
.arg(local_abnf_path)
+ .arg(spec_abnf_path)
.output()
.expect("failed to run `git diff` command");
diff --git a/dhall/src/syntax/text/printer.rs b/dhall/src/syntax/text/printer.rs
index ccba385..8815d69 100644
--- a/dhall/src/syntax/text/printer.rs
+++ b/dhall/src/syntax/text/printer.rs
@@ -154,7 +154,9 @@ fn fmt_label(label: &Label, f: &mut fmt::Formatter) -> Result<(), fmt::Error> {
| "True" | "False" | "Some" => true,
_ => Builtin::parse(&s).is_some(),
};
- if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) {
+ if s.is_empty() {
+ write!(f, "``")
+ } else if !is_reserved && s.chars().all(|c| c.is_ascii_alphanumeric()) {
write!(f, "{}", s)
} else {
write!(f, "`{}`", s)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 01:49:41 +0000