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

Compare commits

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

2 commits
c3fbf3368f ... bed94f3d41

Author SHA1 Message Date
William Ball
bed94f3d41 impredicative/predicative split 2024-12-02 20:40:38 -08:00
William Ball
973acd4151 new type hierarchy 2024-12-01 23:36:32 -08:00
12 changed files with 1601 additions and 1284 deletions
Show stats Expand all files Collapse all files

4
grammar.js
View file

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

32
src/grammar.json generated
View file

@ -94,6 +94,32 @@
}
]
},
"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": [
@ -202,11 +228,7 @@
},
{
"type": "SYMBOL",
"name": "star"
},
{
"type": "SYMBOL",
"name": "square"
"name": "sort"
},
{
"type": "SEQ",

25
src/node-types.json generated
View file

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

2728
src/parser.c generated
View file

File diff suppressed because it is too large Load diff

3
test/corpus/application.txt
View file

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

3
test/corpus/arrows.txt
View file

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

3
test/corpus/axioms.txt
View file

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

3
test/corpus/include.txt
View file

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

3
test/corpus/labs.txt
View file

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

6
test/corpus/pabs.txt
View file

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

3
test/corpus/params.txt
View file

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

72
test/corpus/sorts.txt Normal file
View file

@ -0,0 +1,72 @@
=====
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)))))))