diff --git a/grammar.js b/grammar.js index 0b8302b..3e509f9 100644 --- a/grammar.js +++ b/grammar.js @@ -26,9 +26,6 @@ module.exports = grammar({ $.fixity, )), - identifier : $ => /[a-zA-Z_]\w*/, - symbol : $ => /[!@#$%^&*-+=<>,./?{}\\|`~'\"∧∨⊙×≅]+/, - comment : $ => token(seq('--', /.*/)), section : $ => seq( @@ -60,7 +57,7 @@ module.exports = grammar({ ')' ), - star : $ => "★", + star : $ => choice("★", "⋆"), square : $ => choice('□', '[]'), sort : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)), @@ -177,5 +174,8 @@ module.exports = grammar({ command : $ => '@include', + identifier : $ => /[a-zA-Z_]\w*/, + symbol : $ => /[!@#$%^&*-+=<>,./?{}\\|`~'\"∧∨⊙×≅]+/, + } }); diff --git a/test/corpus/sorts.txt b/test/corpus/sorts.txt index c6e28a0..0386c3b 100644 --- a/test/corpus/sorts.txt +++ b/test/corpus/sorts.txt @@ -2,7 +2,7 @@ Sorts ===== -def foo (A : ★) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) := A; +def foo (A : ★) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) (H : ⋆) := A; --- @@ -72,6 +72,15 @@ def foo (A : ★) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □ (term (sort (square)))))))) + (param_block + (identifier) + (expr + (app_term + (binex + (app + (term + (sort + (star)))))))) (expr (app_term (binex