Skip to content

Commit 75ae70d

Browse files
banacornbanacorn
authored
Merge pull request #6 from erydo/unicode
Support Unicode ellipsis, instance brackets, and idiom brackets
2 parents 827aa50 + 2a5d5f8 commit 75ae70d

File tree

5 files changed

+160800
-120390
lines changed

5 files changed

+160800
-120390
lines changed

‎corpus/grammar/function.txt‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -115,3 +115,52 @@ f a with g a
115115
(atom (qualified_name)))
116116
(rhs
117117
(expr (atom)))))
118+
119+
==================
120+
Idiom brackets
121+
==================
122+
123+
x : _
124+
x = (| if a then b else c |)
125+
126+
---
127+
128+
(source_file
129+
(function_clause
130+
(lhs (function_name (qualified_name)))
131+
(rhs (expr (atom))))
132+
(function_clause
133+
(lhs (atom (qualified_name)))
134+
(rhs
135+
(expr (atom (expr
136+
(atom (qualified_name))
137+
(atom (qualified_name))
138+
(atom (qualified_name))
139+
(atom (qualified_name))
140+
(atom (qualified_name))
141+
(atom (qualified_name))))))))
142+
143+
144+
==================
145+
Idiom brackets (Unicode)
146+
==================
147+
148+
x : _
149+
x = ⦇ if a then b else c ⦈
150+
151+
---
152+
153+
(source_file
154+
(function_clause
155+
(lhs (function_name (qualified_name)))
156+
(rhs (expr (atom))))
157+
(function_clause
158+
(lhs (atom (qualified_name)))
159+
(rhs
160+
(expr (atom (expr
161+
(atom (qualified_name))
162+
(atom (qualified_name))
163+
(atom (qualified_name))
164+
(atom (qualified_name))
165+
(atom (qualified_name))
166+
(atom (qualified_name))))))))

‎corpus/grammar/module.txt‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,3 +74,21 @@ open module Nat (A : Set) = Sort {{ ... }}
7474
(module_macro
7575
(name) (typed_binding (atom (qualified_name)) (expr (atom)))
7676
(module_application (qualified_name))))
77+
78+
==================
79+
Module macros (Unicode)
80+
==================
81+
82+
module Sort.Nat (A : Set) = Sort ℕ
83+
84+
open module Nat (A : Set) = Sort ⦃ … ⦄
85+
86+
---
87+
88+
(source_file
89+
(module_macro
90+
(qualified_name) (typed_binding (atom (qualified_name)) (expr (atom)))
91+
(module_application (qualified_name) (atom (qualified_name))))
92+
(module_macro
93+
(name) (typed_binding (atom (qualified_name)) (expr (atom)))
94+
(module_application (qualified_name))))

‎grammar.js‎

Lines changed: 71 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,14 @@ const float = /(\-?(0x[0-9a-fA-F]+|[0-9]+)\.(0x[0-9a-fA-F]+|[0-9]+)([eE][-+]?(0x
1515
const name = /([^\s\\.\"\(\)\{\}@\'\\_]|\\[^\sa-zA-Z]|_[^\s;\.\"\(\)\{\}@])[^\s;\.\"\(\)\{\}@]*/;
1616
const qualified_name = /(([^\s;\.\"\(\)\{\}@\'\\_]|\\[^\sa-zA-Z]|_[^\s;\.\"\(\)\{\}@])[^\s;\.\"\(\)\{\}@]*\.)*([^\s;\.\"\(\)\{\}@\'\\_]|\\[^\sa-zA-Z]|_[^\s;\.\"\(\)\{\}@])[^\s;\.\"\(\)\{\}@]*/;
1717

18+
const BKT_CURL1 = [['{', '}']];
19+
const BKT_CURL2 = [['{{', '}}'], ['⦃', '⦄']];
20+
const BKT_CURLS = [...BKT_CURL1, ...BKT_CURL2];
21+
22+
const BKT_IDIOM = [['(|', '|)'], ['⦇', '⦈']];
23+
const BKT_PAREN = [['(', ')']];
24+
25+
1826
module.exports = grammar({
1927
name: 'agda',
2028

@@ -64,6 +72,7 @@ module.exports = grammar({
6472
_const_forall: $ => token(choice('forall', '∀')),
6573
_const_right_arrow: $ => token(choice('->','→')),
6674
_const_lambda: $ => token(choice('\\','λ')),
75+
_const_ellipsis: $ => token(choice('...','…')),
6776

6877
////////////////////////////////////////////////////////////////////////
6978
// Literals
@@ -99,12 +108,14 @@ module.exports = grammar({
99108
_arg_names: $ => repeat1($._arg_name),
100109
_arg_name: $ => choice(
101110
maybeDotted($._field_name),
102-
seq('{' , repeat1(maybeDotted($._field_name)), '}' ),
103-
seq('{{', repeat1(maybeDotted($._field_name)), '}}'),
104-
seq('.' , '{', repeat1($._field_name), '}'),
105-
seq('..', '{', repeat1($._field_name), '}'),
106-
seq('.' , '{{', repeat1($._field_name), '}}'),
107-
seq('..', '{{', repeat1($._field_name), '}}'),
111+
bracketWith(
112+
(left, right) => choice(
113+
seq(left, repeat1(maybeDotted($._field_name)), right),
114+
seq('.', left, repeat1($._field_name), right),
115+
seq('..', left, repeat1($._field_name), right),
116+
),
117+
BKT_CURLS,
118+
),
108119
),
109120

110121
////////////////////////////////////////////////////////////////////////
@@ -332,10 +343,13 @@ module.exports = grammar({
332343
$.name,
333344
seq('(', $._const_lambda, $.name, $._const_right_arrow, $.name, ')'),
334345
seq('(', $._const_lambda, '_', $._const_right_arrow, $.name, ')'),
335-
seq('{', $.simple_hole, '}'),
336-
seq('{{', $.simple_hole, '}}'),
337-
seq('{', $.simple_hole, '=', $.simple_hole, '}'),
338-
seq('{{', $.simple_hole, '=', $.simple_hole, '}}')
346+
bracket(
347+
choice(
348+
seq($.simple_hole),
349+
seq($.simple_hole, '=', $.simple_hole),
350+
),
351+
BKT_CURLS,
352+
),
339353
),
340354

341355
simple_hole: $ => choice(
@@ -454,7 +468,10 @@ module.exports = grammar({
454468
),
455469

456470
module_application: $ => choice(
457-
prec(1, seq($.qualified_name, '{{', '...', '}}')),
471+
bracketWith(
472+
(left, right) => prec(1, seq($.qualified_name, left, $._const_ellipsis, right)),
473+
BKT_CURL2,
474+
),
458475
seq($.qualified_name, optional($._open_args1)),
459476
),
460477

@@ -574,15 +591,17 @@ module.exports = grammar({
574591
////////////////////////////////////////////////////////////////////////
575592

576593
// "LamBinds"
577-
_lambda_binding: $ => (choice(
594+
_lambda_binding: $ => choice(
578595
seq($.untyped_binding, $._lambda_binding),
579596
seq($.typed_binding, $._lambda_binding),
580597
$.untyped_binding,
581598
$.typed_binding,
582-
seq('(', ')'),
583-
seq('{', '}'),
584-
seq('{{', '}}')
585-
)),
599+
bracket(
600+
seq(),
601+
BKT_PAREN,
602+
BKT_CURLS,
603+
),
604+
),
586605

587606
catchall_pragma: $ => seq('{-#', 'CATCHALL', '#-}'),
588607

@@ -631,18 +650,25 @@ module.exports = grammar({
631650
// "DomainFreeBinding"
632651
untyped_binding: $ => maybeDotted(choice(
633652
seq($._binding_name),
634-
seq('{', $._application, '}'),
635-
seq('{{', $._application, '}}')
653+
bracket(
654+
$._application,
655+
BKT_CURLS,
656+
),
636657
)),
637658

638659
_typed_bindings1: $ => (repeat1($.typed_binding)),
639660

640661
// "TypedBindings"
641662
typed_binding: $ => choice(
642-
maybeDotted(bracketed(seq(
643-
$._application, ':', $.expr
644-
))),
645-
seq('(', $.open, ')'),
663+
maybeDotted(bracket(
664+
seq($._application, ':', $.expr),
665+
BKT_PAREN,
666+
BKT_CURLS,
667+
)),
668+
bracket(
669+
$.open,
670+
BKT_PAREN,
671+
),
646672
// seq('(', 'let', $._let_body, ')')
647673
),
648674

@@ -762,15 +788,20 @@ module.exports = grammar({
762788
'quote',
763789
'quoteTerm',
764790
'unquote',
765-
seq('{{', $.expr, '}}'),
766-
seq('(', $.expr, ')'),
767-
seq('(|', $.expr, '|)'),
768-
seq('(', ')'),
769-
seq('{{', '}}'),
770-
// seq($.name_at, $.atom),
791+
bracket(
792+
$.expr,
793+
BKT_CURL2,
794+
BKT_IDIOM,
795+
BKT_PAREN,
796+
),
797+
bracket(
798+
seq(),
799+
BKT_CURL2,
800+
BKT_PAREN,
801+
),
771802
seq('.', $.atom),
772803
$.record_assignments,
773-
'...'
804+
$._const_ellipsis,
774805
),
775806

776807
}
@@ -810,13 +841,17 @@ function maybeDotted(rule) {
810841
rule, // Relevant
811842
seq('.', rule), // Irrelevant
812843
seq('..', rule), // NonStrict
813-
)
844+
);
814845
}
815846

816-
function bracketed(rule) {
817-
return choice(
818-
seq('(', rule, ')'), // ( )
819-
seq('{', rule, '}'), // { }
820-
seq('{{', rule, '}}'), // {{ }}
821-
)
847+
function flatten(arrOfArrs) {
848+
return arrOfArrs.reduce((res, arr) => [...res, ...arr], []);
849+
}
850+
851+
function bracketWith(fn, ...pairs) {
852+
return choice(...flatten(pairs).map(([left, right]) => fn(left, right)));
853+
}
854+
855+
function bracket(expr, ...pairs) {
856+
return bracketWith((left, right) => seq(left, expr, right), ...pairs);
822857
}

0 commit comments

Comments
 (0)