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:4131069cd40a56235c4777e8b485614e2bd70ac4
Branches Tags
wball:main

2 commits
bed94f3d41 ... 4131069cd4

Author SHA1 Message Date
William Ball
4131069cd4 infix operators 2024-12-10 21:40:39 -08:00
William Ball
3834eb6f0a sections 2024-12-06 15:25:45 -08:00
16 changed files with 5811 additions and 2688 deletions
Show stats Expand all files Collapse all files

57
grammar.js
View file

@ -17,12 +17,47 @@ module.exports = grammar({
rules: {
program : $ => repeat(choice($.definition, $.preprocess, $.axiom)),
program : $ => repeat1(choice(
$.definition,
$.preprocess,
$.axiom,
$.section,
$.variable,
$.fixity,
)),
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)),
@ -31,7 +66,7 @@ module.exports = grammar({
')'
),
star : $ => "*",
star : $ => "★",
square : $ => choice('□', '[]'),
sort : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)),
@ -57,6 +92,14 @@ 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,
@ -79,7 +122,7 @@ module.exports = grammar({
arrow : $ => prec.left(1, seq(
$.app_term,
choice('->', '→'),
'→',
$.expr,
)),
@ -87,7 +130,7 @@ module.exports = grammar({
$.labs,
$.pabs,
$.let,
$.app,
$.binex,
),
expr : $ => choice(
@ -102,7 +145,7 @@ module.exports = grammar({
axiom : $ => seq(
'axiom',
field('name', $.identifier),
field('name', choice($.identifier, $.symbol)),
repeat($.param_block),
$.ascription,
';'
@ -110,11 +153,11 @@ module.exports = grammar({
definition : $ => seq(
'def',
field('name', $.identifier),
field('name', choice($.identifier, $.symbol)),
repeat($.param_block),
optional($.ascription),
':=',
choice($.expr),
$.expr,
';',
),

225
src/grammar.json generated
View file

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

147
src/node-types.json generated
View file

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

7297
src/parser.c generated
View file

File diff suppressed because it is too large Load diff

65
test/corpus/application.txt
View file

@ -2,67 +2,18 @@
Application
===========
def foo (A B : *) (f : A -> B) (x : A) :=
(fun (x : B) => x) (f x);
def foo := f x;
---
(program
(definition
(identifier)
(param_block
(identifier)
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(arrow
(program
(definition
(identifier)
(expr
(app_term
(app
(term
(identifier))))
(expr
(app_term
(binex
(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,54 +2,60 @@
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
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(arrow
(app_term
(app
(term
(identifier))))
(program
(definition
(identifier)
(param_block
(identifier)
(identifier)
(expr
(app_term
(binex
(app
(term
(sort
(star))))))))
(param_block
(identifier)
(expr
(arrow
(app_term
(app
(term
(identifier))))
(expr
(app_term
(binex
(app
(term
(identifier))))))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))
(term
(identifier))
(term
(identifier)))))))
(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))))))))

23
test/corpus/axioms.txt
View file

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

36
test/corpus/definition.txt Normal file
View file

@ -0,0 +1,36 @@
==========
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,30 +4,32 @@ Include
@include foo.pg
def baz : * := A;
def baz : ★ := A;
@include bar.pg
---
(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)))
(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)))

45
test/corpus/infix.txt Normal file
View file

@ -0,0 +1,45 @@
===============
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,39 +2,43 @@
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
(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))))))))))
(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)))))))))))

92
test/corpus/let.txt
View file

@ -12,48 +12,54 @@ def foo :=
---
(program
(definition
(identifier)
(expr
(app_term
(let
(binding
(identifier)
(ascription
(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)))))))
(expr
(app_term
(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))))))))))
(binex
(app
(term
(identifier)))))))))))

59
test/corpus/pabs.txt
View file

@ -2,34 +2,37 @@
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
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(expr
(app_term
(app
(term
(sort
(star)))))))))))
(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))))))))))))

33
test/corpus/params.txt
View file

@ -1,33 +0,0 @@
==========
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 Normal file
View file

@ -0,0 +1,74 @@
========
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,71 +2,79 @@
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
(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)))))))
(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))))))))