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

Compare commits

base: wball:4131069cd40a56235c4777e8b485614e2bd70ac4
Branches Tags
wball:main
..
compare: wball:bed94f3d41ae94ad2af52b9f04716f90dbde9970
Branches Tags
wball:main

No commits in common. "4131069cd40a56235c4777e8b485614e2bd70ac4" and "bed94f3d41ae94ad2af52b9f04716f90dbde9970" have entirely different histories.
4131069cd4 ... bed94f3d41

16 changed files with 2714 additions and 5837 deletions
Show stats Expand all files Collapse all files

57
grammar.js
View file

@ -17,47 +17,12 @@ module.exports = grammar({
rules: {
program : $ => repeat1(choice(
$.definition,
$.preprocess,
$.axiom,
$.section,
$.variable,
$.fixity,
)),
program : $ => repeat(choice($.definition, $.preprocess, $.axiom)),
identifier : $ => /[a-zA-Z_]\w*/,
symbol : $ => /[!@#$%^&*-+=<>,./?\[\]{}\\|`~'\"∧∨⊙×≅]+/,
comment : $ => token(seq('--', /.*/)),
section : $ => seq(
'section', $.identifier,
$.program,
'end', $.identifier,
),
precedence : $ => /[0-9]+/,
fixity : $ => seq(
choice('infixl', 'infixr'),
$.precedence,
$.symbol,
';'
),
variable : $ => seq(
choice('variable', 'hypothesis'),
repeat1(seq(
'(',
repeat1(choice($.identifier, $.symbol)),
':',
field('type', $.expr),
')'
)),
';'
),
param_block : $ => seq(
'(',
field('param', repeat1($.identifier)),
@ -66,7 +31,7 @@ module.exports = grammar({
')'
),
star : $ => "★",
star : $ => "*",
square : $ => choice('□', '[]'),
sort : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)),
@ -92,14 +57,6 @@ module.exports = grammar({
seq('(', $.expr, ')'),
),
// HACK:
// completely ignore precedence and associativity for treesitter
// this is enough to get the syntax highlighting right
binex : $ => seq(
$.app,
optional(seq($.symbol, $.binex)),
),
binding : $ => seq(
'(',
$.identifier,
@ -122,7 +79,7 @@ module.exports = grammar({
arrow : $ => prec.left(1, seq(
$.app_term,
'→',
choice('->', '→'),
$.expr,
)),
@ -130,7 +87,7 @@ module.exports = grammar({
$.labs,
$.pabs,
$.let,
$.binex,
$.app,
),
expr : $ => choice(
@ -145,7 +102,7 @@ module.exports = grammar({
axiom : $ => seq(
'axiom',
field('name', choice($.identifier, $.symbol)),
field('name', $.identifier),
repeat($.param_block),
$.ascription,
';'
@ -153,11 +110,11 @@ module.exports = grammar({
definition : $ => seq(
'def',
field('name', choice($.identifier, $.symbol)),
field('name', $.identifier),
repeat($.param_block),
optional($.ascription),
':=',
$.expr,
choice($.expr),
';',
),

225
src/grammar.json generated
View file

@ -2,7 +2,7 @@
"name": "perga",
"rules": {
"program": {
"type": "REPEAT1",
"type": "REPEAT",
"content": {
"type": "CHOICE",
"members": [
@ -17,18 +17,6 @@
{
"type": "SYMBOL",
"name": "axiom"
},
{
"type": "SYMBOL",
"name": "section"
},
{
"type": "SYMBOL",
"name": "variable"
},
{
"type": "SYMBOL",
"name": "fixity"
}
]
}
@ -37,10 +25,6 @@
"type": "PATTERN",
"value": "[a-zA-Z_]\\w*"
},
"symbol": {
"type": "PATTERN",
"value": "[!@#$%^&*-+=<>,./?\\[\\]{}\\\\|`~'\\\"∧∨⊙×≅]+"
},
"comment": {
"type": "TOKEN",
"content": {
@ -57,131 +41,6 @@
]
}
},
"section": {
"type": "SEQ",
"members": [
{
"type": "STRING",
"value": "section"
},
{
"type": "SYMBOL",
"name": "identifier"
},
{
"type": "SYMBOL",
"name": "program"
},
{
"type": "STRING",
"value": "end"
},
{
"type": "SYMBOL",
"name": "identifier"
}
]
},
"precedence": {
"type": "PATTERN",
"value": "[0-9]+"
},
"fixity": {
"type": "SEQ",
"members": [
{
"type": "CHOICE",
"members": [
{
"type": "STRING",
"value": "infixl"
},
{
"type": "STRING",
"value": "infixr"
}
]
},
{
"type": "SYMBOL",
"name": "precedence"
},
{
"type": "SYMBOL",
"name": "symbol"
},
{
"type": "STRING",
"value": ";"
}
]
},
"variable": {
"type": "SEQ",
"members": [
{
"type": "CHOICE",
"members": [
{
"type": "STRING",
"value": "variable"
},
{
"type": "STRING",
"value": "hypothesis"
}
]
},
{
"type": "REPEAT1",
"content": {
"type": "SEQ",
"members": [
{
"type": "STRING",
"value": "("
},
{
"type": "REPEAT1",
"content": {
"type": "CHOICE",
"members": [
{
"type": "SYMBOL",
"name": "identifier"
},
{
"type": "SYMBOL",
"name": "symbol"
}
]
}
},
{
"type": "STRING",
"value": ":"
},
{
"type": "FIELD",
"name": "type",
"content": {
"type": "SYMBOL",
"name": "expr"
}
},
{
"type": "STRING",
"value": ")"
}
]
}
},
{
"type": "STRING",
"value": ";"
}
]
},
"param_block": {
"type": "SEQ",
"members": [
@ -220,7 +79,7 @@
},
"star": {
"type": "STRING",
"value": "★"
"value": "*"
},
"square": {
"type": "CHOICE",
@ -390,36 +249,6 @@
}
]
},
"binex": {
"type": "SEQ",
"members": [
{
"type": "SYMBOL",
"name": "app"
},
{
"type": "CHOICE",
"members": [
{
"type": "SEQ",
"members": [
{
"type": "SYMBOL",
"name": "symbol"
},
{
"type": "SYMBOL",
"name": "binex"
}
]
},
{
"type": "BLANK"
}
]
}
]
},
"binding": {
"type": "SEQ",
"members": [
@ -510,8 +339,17 @@
"name": "app_term"
},
{
"type": "STRING",
"value": "→"
"type": "CHOICE",
"members": [
{
"type": "STRING",
"value": "->"
},
{
"type": "STRING",
"value": "→"
}
]
},
{
"type": "SYMBOL",
@ -537,7 +375,7 @@
},
{
"type": "SYMBOL",
"name": "binex"
"name": "app"
}
]
},
@ -582,17 +420,8 @@
"type": "FIELD",
"name": "name",
"content": {
"type": "CHOICE",
"members": [
{
"type": "SYMBOL",
"name": "identifier"
},
{
"type": "SYMBOL",
"name": "symbol"
}
]
"type": "SYMBOL",
"name": "identifier"
}
},
{
@ -623,17 +452,8 @@
"type": "FIELD",
"name": "name",
"content": {
"type": "CHOICE",
"members": [
{
"type": "SYMBOL",
"name": "identifier"
},
{
"type": "SYMBOL",
"name": "symbol"
}
]
"type": "SYMBOL",
"name": "identifier"
}
},
{
@ -660,8 +480,13 @@
"value": ":="
},
{
"type": "SYMBOL",
"name": "expr"
"type": "CHOICE",
"members": [
{
"type": "SYMBOL",
"name": "expr"
}
]
},
{
"type": "STRING",

147
src/node-types.json generated
View file

@ -23,7 +23,7 @@
"required": true,
"types": [
{
"type": "binex",
"type": "app",
"named": true
},
{
@ -87,10 +87,6 @@
{
"type": "identifier",
"named": true
},
{
"type": "symbol",
"named": true
}
]
}
@ -137,29 +133,6 @@
]
}
},
{
"type": "binex",
"named": true,
"fields": {},
"children": {
"multiple": true,
"required": true,
"types": [
{
"type": "app",
"named": true
},
{
"type": "binex",
"named": true
},
{
"type": "symbol",
"named": true
}
]
}
},
{
"type": "definition",
"named": true,
@ -171,10 +144,6 @@
{
"type": "identifier",
"named": true
},
{
"type": "symbol",
"named": true
}
]
}
@ -217,25 +186,6 @@
]
}
},
{
"type": "fixity",
"named": true,
"fields": {},
"children": {
"multiple": true,
"required": true,
"types": [
{
"type": "precedence",
"named": true
},
{
"type": "symbol",
"named": true
}
]
}
},
{
"type": "labs",
"named": true,
@ -352,7 +302,7 @@
"fields": {},
"children": {
"multiple": true,
"required": true,
"required": false,
"types": [
{
"type": "axiom",
@ -362,40 +312,9 @@
"type": "definition",
"named": true
},
{
"type": "fixity",
"named": true
},
{
"type": "preprocess",
"named": true
},
{
"type": "section",
"named": true
},
{
"type": "variable",
"named": true
}
]
}
},
{
"type": "section",
"named": true,
"fields": {},
"children": {
"multiple": true,
"required": true,
"types": [
{
"type": "identifier",
"named": true
},
{
"type": "program",
"named": true
}
]
}
@ -447,36 +366,6 @@
]
}
},
{
"type": "variable",
"named": true,
"fields": {
"type": {
"multiple": true,
"required": true,
"types": [
{
"type": "expr",
"named": true
}
]
}
},
"children": {
"multiple": true,
"required": true,
"types": [
{
"type": "identifier",
"named": true
},
{
"type": "symbol",
"named": true
}
]
}
},
{
"type": "(",
"named": false
@ -489,6 +378,10 @@
"type": ",",
"named": false
},
{
"type": "->",
"named": false
},
{
"type": ":",
"named": false
@ -537,10 +430,6 @@
"type": "fun",
"named": false
},
{
"type": "hypothesis",
"named": false
},
{
"type": "identifier",
"named": true
@ -549,14 +438,6 @@
"type": "in",
"named": false
},
{
"type": "infixl",
"named": false
},
{
"type": "infixr",
"named": false
},
{
"type": "let",
"named": false
@ -565,26 +446,10 @@
"type": "post_command",
"named": true
},
{
"type": "precedence",
"named": true
},
{
"type": "section",
"named": false
},
{
"type": "star",
"named": true
},
{
"type": "symbol",
"named": true
},
{
"type": "variable",
"named": false
},
{
"type": "λ",
"named": false

7349
src/parser.c generated
View file

File diff suppressed because it is too large Load diff

65
test/corpus/application.txt
View file

@ -2,18 +2,67 @@
Application
===========
def foo := f x;
def foo (A B : *) (f : A -> B) (x : A) :=
(fun (x : B) => x) (f x);
---
(program
(definition
(identifier)
(expr
(program
(definition
(identifier)
(param_block
(identifier)
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(arrow
(app_term
(binex
(app
(term
(identifier))))
(expr
(app_term
(app
(term
(identifier))
(term
(identifier))))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(expr
(app_term
(labs
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier)))))))))
(term
(expr
(app_term
(app
(term
(identifier))
(term
(identifier)))))))))))

92
test/corpus/arrows.txt
View file

@ -2,60 +2,54 @@
Arrows
======
def foo (A B : ★) (f : A → A → B) (x : A) := f x x;
def foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
---
(program
(definition
(identifier)
(param_block
(identifier)
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(param_block
(identifier)
(program
(definition
(identifier)
(param_block
(identifier)
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(arrow
(app_term
(app
(term
(identifier))))
(expr
(arrow
(app_term
(binex
(app
(term
(identifier)))))
(expr
(arrow
(app_term
(binex
(app
(term
(identifier)))))
(expr
(app_term
(binex
(app
(term
(identifier)))))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier))
(term
(identifier))
(term
(identifier))))))))
(identifier))))
(expr
(app_term
(app
(term
(identifier))))))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))
(term
(identifier))
(term
(identifier)))))))

23
test/corpus/axioms.txt
View file

@ -2,18 +2,17 @@
Axioms
======
axiom nat : ★;
axiom nat : *;
-----
(program
(axiom
(identifier)
(ascription
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))))
(program
(axiom
(identifier)
(ascription
(expr
(app_term
(app
(term
(sort
(star)))))))))

36
test/corpus/definition.txt
View file

@ -1,36 +0,0 @@
==========
Definition
==========
def foo (A : ★) (x y z : A) := x;
---
(program
(definition
(identifier)
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(param_block
(identifier)
(identifier)
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier))))))))

46
test/corpus/include.txt
View file

@ -4,32 +4,30 @@ Include
@include foo.pg
def baz : ★ := A;
def baz : * := A;
@include bar.pg
---
(program
(preprocess
(command)
(post_command))
(definition
(identifier)
(ascription
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(preprocess
(command)
(post_command)))
(program
(preprocess
(command)
(post_command))
(definition
(identifier)
(ascription
(expr
(app_term
(app
(term
(sort
(star)))))))
(expr
(app_term
(app
(term
(identifier))))))
(preprocess
(command)
(post_command)))

45
test/corpus/infix.txt
View file

@ -1,45 +0,0 @@
===============
Infix Operators
===============
infixl 20 +;
infixl 30 *;
infixr 40 ^;
def computation := one + two * four ^ three;
---
(program
(fixity
(precedence)
(symbol))
(fixity
(precedence)
(symbol))
(fixity
(precedence)
(symbol))
(definition
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))
(symbol)
(binex
(app
(term
(identifier)))
(symbol)
(binex
(app
(term
(identifier)))
(symbol)
(binex
(app
(term
(identifier)))))))))))

70
test/corpus/labs.txt
View file

@ -2,43 +2,39 @@
Lambda Abstraction
==================
def foo := fun (A : ★) (x : A) : A => x;
def foo := fun (A : *) (x : A) : A => x;
----------
(program
(definition
(identifier)
(expr
(app_term
(labs
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(ascription
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier)))))))))))
(program
(definition
(identifier)
(expr
(app_term
(labs
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(ascription
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))))))))))

92
test/corpus/let.txt
View file

@ -12,54 +12,48 @@ def foo :=
---
(program
(definition
(identifier)
(expr
(app_term
(let
(binding
(identifier)
(ascription
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(binding
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(binding
(identifier)
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(program
(definition
(identifier)
(expr
(app_term
(let
(binding
(identifier)
(ascription
(expr
(app_term
(binex
(app
(term
(identifier)))))))))))
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))))))
(binding
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(binding
(identifier)
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))))))))))

59
test/corpus/pabs.txt
View file

@ -2,37 +2,34 @@
Pi Abstraction
==============
def rel := forall (A : ★) (x : A), ★;
def rel := forall (A : *) (x : A), *;
----------
(program
(definition
(identifier)
(expr
(app_term
(pabs
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))))))
(program
(definition
(identifier)
(expr
(app_term
(pabs
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(sort
(star)))))))))))

33
test/corpus/params.txt Normal file
View file

@ -0,0 +1,33 @@
==========
Definition
==========
def foo (A : *) (x y z : A) := x;
---
(program
(definition
(identifier)
(param_block
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(identifier)
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier)))))))

74
test/corpus/section.txt
View file

@ -1,74 +0,0 @@
========
Sections
========
section Test
variable (A B C : ★);
hypothesis (x : A) (y : B) (z1 z2 : C);
section Nested
def foo (x : A) := y;
end Nested
end Test
----
(program
(section
(identifier)
(program
(variable
(identifier)
(identifier)
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(variable
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier))))))
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier))))))
(identifier)
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(section
(identifier)
(program
(definition
(identifier)
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier))))))))
(identifier)))
(identifier)))

138
test/corpus/sorts.txt
View file

@ -2,79 +2,71 @@
Sorts
=====
def foo (A : ★) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) := A;
def foo (A : *) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) := A;
---
(program
(definition
(identifier)
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(square))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(square))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(square))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(square))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(square))))))))
(param_block
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(square))))))))
(expr
(app_term
(binex
(app
(term
(identifier))))))))
(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)))))))