wball/tree-sitter-perga
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Compare commits

base: wball:bed94f3d41ae94ad2af52b9f04716f90dbde9970
Branches Tags
wball:main
..
compare: wball:c3fbf3368f0223b0b0834824f13ab9417a9c6a40
Branches Tags
wball:main

No commits in common. "bed94f3d41ae94ad2af52b9f04716f90dbde9970" and "c3fbf3368f0223b0b0834824f13ab9417a9c6a40" have entirely different histories.
bed94f3d41 ... c3fbf3368f

12 changed files with 1342 additions and 1659 deletions
Show stats Expand all files Collapse all files

4
grammar.js
View file

@ -33,7 +33,6 @@ module.exports = grammar({
star : $ => "*",
square : $ => choice('□', '[]'),
sort : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)),
labs : $ => seq(
choice('λ', 'fun'),
@ -53,7 +52,8 @@ module.exports = grammar({
term : $ => choice(
$.identifier,
$.sort,
$.star,
$.square,
seq('(', $.expr, ')'),
),

32
src/grammar.json generated
View file

@ -94,32 +94,6 @@
}
]
},
"sort": {
"type": "CHOICE",
"members": [
{
"type": "SYMBOL",
"name": "star"
},
{
"type": "SYMBOL",
"name": "square"
},
{
"type": "SEQ",
"members": [
{
"type": "SYMBOL",
"name": "square"
},
{
"type": "PATTERN",
"value": "[0-9₀₁₂₃₄₅₆₇₈₉]+"
}
]
}
]
},
"labs": {
"type": "SEQ",
"members": [
@ -228,7 +202,11 @@
},
{
"type": "SYMBOL",
"name": "sort"
"name": "star"
},
{
"type": "SYMBOL",
"name": "square"
},
{
"type": "SEQ",

25
src/node-types.json generated
View file

@ -319,25 +319,6 @@
]
}
},
{
"type": "sort",
"named": true,
"fields": {},
"children": {
"multiple": false,
"required": true,
"types": [
{
"type": "square",
"named": true
},
{
"type": "star",
"named": true
}
]
}
},
{
"type": "square",
"named": true,
@ -360,7 +341,11 @@
"named": true
},
{
"type": "sort",
"type": "square",
"named": true
},
{
"type": "star",
"named": true
}
]

2844
src/parser.c generated
View file

File diff suppressed because it is too large Load diff

3
test/corpus/application.txt
View file

@ -17,8 +17,7 @@ def foo (A B : *) (f : A -> B) (x : A) :=
(app_term
(app
(term
(sort
(star)))))))
(star))))))
(param_block
(identifier)
(expr

3
test/corpus/arrows.txt
View file

@ -16,8 +16,7 @@ def foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
(app_term
(app
(term
(sort
(star)))))))
(star))))))
(param_block
(identifier)
(expr

3
test/corpus/axioms.txt
View file

@ -14,5 +14,4 @@ axiom nat : *;
(app_term
(app
(term
(sort
(star)))))))))
(star))))))))

3
test/corpus/include.txt
View file

@ -21,8 +21,7 @@ def baz : * := A;
(app_term
(app
(term
(sort
(star)))))))
(star))))))
(expr
(app_term
(app

3
test/corpus/labs.txt
View file

@ -18,8 +18,7 @@ def foo := fun (A : *) (x : A) : A => x;
(app_term
(app
(term
(sort
(star)))))))
(star))))))
(param_block
(identifier)
(expr

6
test/corpus/pabs.txt
View file

@ -18,8 +18,7 @@ def rel := forall (A : *) (x : A), *;
(app_term
(app
(term
(sort
(star)))))))
(star))))))
(param_block
(identifier)
(expr
@ -31,5 +30,4 @@ def rel := forall (A : *) (x : A), *;
(app_term
(app
(term
(sort
(star)))))))))))
(star))))))))))

3
test/corpus/params.txt
View file

@ -15,8 +15,7 @@ def foo (A : *) (x y z : A) := x;
(app_term
(app
(term
(sort
(star)))))))
(star))))))
(param_block
(identifier)
(identifier)

72
test/corpus/sorts.txt
View file

@ -1,72 +0,0 @@
=====
Sorts
=====
def foo (A : *) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) := A;
---
(program
(definition
(identifier)
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(square)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(square)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(square)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(square)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(square)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(square)))))))
(expr
(app_term
(app
(term
(identifier)))))))