Skip to content

Commit

Permalink
Maybe correcter apply with repeated args.
Browse files Browse the repository at this point in the history
  • Loading branch information
Julian committed Jan 3, 2025
1 parent d4f9fbb commit 2bea8da
Show file tree
Hide file tree
Showing 7 changed files with 6,227 additions and 5,844 deletions.
9 changes: 7 additions & 2 deletions grammar.js
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,15 @@ export default grammar({

precedences: $ => [
[
'ite',
'min',
'arrow',
'ite',
'lead',
'arg',
'max',
],
[
'tactic',
'apply',
],
[
'declId',
Expand Down
14 changes: 8 additions & 6 deletions grammar/term.js
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ export default {
$.hole,
$.sorry,
$.anonymousConstructor,
alias($._apply, $.apply),
$.apply,
$.arrow,
$.true,
$.false,
Expand Down Expand Up @@ -49,11 +49,6 @@ export default {
),
anonymousConstructor: $ => seq('⟨', sep0($._term, ','), '⟩'),

_apply: $ => prec.left('apply', seq(
field('function', $._term),
field('argument', $._term),
)),

_typeSpec: $ => field('type', seq(':', $._term)),

_binderIdent: $ => prec('binderIdent', choice($.identifier, $.hole)),
Expand Down Expand Up @@ -82,6 +77,13 @@ export default {
$.implicitBinder,
$.instanceBinder,
),

_arguments: $ => repeat1(prec('arg', field('argument', $._term))),
apply: $ => prec.right('lead', seq(
prec('max', field('lhs', $._term)),
field('argument', $._arguments),
)),

arrow: $ => prec.right('arrow', seq($._term, '→', $._term)),

true: $ => 'true',
Expand Down
98 changes: 63 additions & 35 deletions src/grammar.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions src/node-types.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading

0 comments on commit 2bea8da

Please sign in to comment.