summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-03-24 14:05:16 +0100
committerNadrieril2019-03-24 14:05:16 +0100
commit6c1a739687f706cf6630c55f8d53c92aacaf6e3d (patch)
tree9fd95a35fe35cd532cd869f4c6f0db6585482225
parentdc8497a1b659bff4e261a0d7f05f56d21c6d2448 (diff)
Disallow builtins as bound variables
-rw-r--r--dhall/tests/parser.rs2
-rw-r--r--dhall_core/src/parser.rs16
-rw-r--r--dhall_parser/src/dhall.abnf12
3 files changed, 20 insertions, 10 deletions
diff --git a/dhall/tests/parser.rs b/dhall/tests/parser.rs
index fcc2fa9..5f57068 100644
--- a/dhall/tests/parser.rs
+++ b/dhall/tests/parser.rs
@@ -62,7 +62,7 @@ parser_success!(spec_parser_success_whitespace, "whitespace");
parser_success!(spec_parser_success_whitespaceBuffet, "whitespaceBuffet");
parser_failure!(spec_parser_failure_annotation, "annotation");
-// parser_failure!(spec_parser_failure_builtins, "builtins");
+parser_failure!(spec_parser_failure_builtins, "builtins");
parser_failure!(spec_parser_failure_doubleBoundsNeg, "doubleBoundsNeg");
parser_failure!(spec_parser_failure_doubleBoundsPos, "doubleBoundsPos");
parser_failure!(spec_parser_failure_importAccess, "importAccess");
diff --git a/dhall_core/src/parser.rs b/dhall_core/src/parser.rs
index 3f53c49..4f26b0f 100644
--- a/dhall_core/src/parser.rs
+++ b/dhall_core/src/parser.rs
@@ -266,6 +266,14 @@ make_parser! {
[simple_label(l)] => l,
[quoted_label(l)] => l,
));
+ rule!(unreserved_label<Label>; children!(
+ [label(l)] => {
+ if Builtin::parse(&String::from(&l)).is_some() {
+ Err(format!("Builtin names are not allowed as bound variables"))?
+ }
+ l
+ },
+ ));
rule!(double_quote_literal<ParsedText>; children!(
[double_quote_chunk(chunks..)] => {
@@ -493,7 +501,7 @@ make_parser! {
));
rule!(lambda_expression<ParsedExpr> as expression; children!(
- [label(l), expression(typ), expression(body)] => {
+ [unreserved_label(l), expression(typ), expression(body)] => {
bx(Expr::Lam(l, typ, body))
}
));
@@ -511,12 +519,12 @@ make_parser! {
));
rule!(let_binding<(Label, Option<ParsedExpr>, ParsedExpr)>; children!(
- [label(name), expression(annot), expression(expr)] => (name, Some(annot), expr),
- [label(name), expression(expr)] => (name, None, expr),
+ [unreserved_label(name), expression(annot), expression(expr)] => (name, Some(annot), expr),
+ [unreserved_label(name), expression(expr)] => (name, None, expr),
));
rule!(forall_expression<ParsedExpr> as expression; children!(
- [label(l), expression(typ), expression(body)] => {
+ [unreserved_label(l), expression(typ), expression(body)] => {
bx(Expr::Pi(l, typ, body))
}
));
diff --git a/dhall_parser/src/dhall.abnf b/dhall_parser/src/dhall.abnf
index d27554c..02edc84 100644
--- a/dhall_parser/src/dhall.abnf
+++ b/dhall_parser/src/dhall.abnf
@@ -168,11 +168,13 @@ quoted-label = 1*quoted-label-char
; NOTE: Dhall does not support Unicode labels, mainly to minimize the potential
; for code obfuscation
-; A label cannot not be any of the reserved identifiers for builtins (unless quoted).
+label = ("`" quoted-label "`" / simple-label)
+
+; An unreserved-label cannot not be any of the reserved identifiers for builtins (unless quoted).
; Their list can be found in semantics.md. This is not enforced by the grammar but
; should be checked by implementations. The only place where this restriction applies
; is bound variables.
-label = ("`" quoted-label "`" / simple-label)
+unreserved-label = label
; An any-label is allowed to be one of the reserved identifiers.
any-label = label
@@ -541,7 +543,7 @@ expression =
/ annotated-expression
; "\(x : a) -> b"
-lambda-expression = lambda whitespace "(" whitespace label whitespace ":" nonempty-whitespace expression ")" whitespace arrow whitespace expression
+lambda-expression = lambda whitespace "(" whitespace unreserved-label whitespace ":" nonempty-whitespace expression ")" whitespace arrow whitespace expression
; "if a then b else c"
ifthenelse-expression = if nonempty-whitespace expression then nonempty-whitespace expression else nonempty-whitespace expression
@@ -550,10 +552,10 @@ ifthenelse-expression = if nonempty-whitespace expression then nonempty-whitespa
; "let x = e1 in e2"
; "let x = e1 let y = e2 in e3"
let-expression = 1*let-binding in nonempty-whitespace expression
-let-binding = let nonempty-whitespace label whitespace [ ":" nonempty-whitespace expression ] "=" whitespace expression
+let-binding = let nonempty-whitespace unreserved-label whitespace [ ":" nonempty-whitespace expression ] "=" whitespace expression
; "forall (x : a) -> b"
-forall-expression = forall whitespace "(" whitespace label whitespace ":" nonempty-whitespace expression ")" whitespace arrow whitespace expression
+forall-expression = forall whitespace "(" whitespace unreserved-label whitespace ":" nonempty-whitespace expression ")" whitespace arrow whitespace expression
; "a -> b"
arrow-expression = operator-expression arrow whitespace expression