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

209
src/grammar.json generated
View file

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

147
src/node-types.json generated
View file

@ -23,7 +23,7 @@
"required": true, "required": true,
"types": [ "types": [
{ {
"type": "binex", "type": "app",
"named": true "named": true
}, },
{ {
@ -87,10 +87,6 @@
{ {
"type": "identifier", "type": "identifier",
"named": true "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", "type": "definition",
"named": true, "named": true,
@ -171,10 +144,6 @@
{ {
"type": "identifier", "type": "identifier",
"named": true "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", "type": "labs",
"named": true, "named": true,
@ -352,7 +302,7 @@
"fields": {}, "fields": {},
"children": { "children": {
"multiple": true, "multiple": true,
"required": true, "required": false,
"types": [ "types": [
{ {
"type": "axiom", "type": "axiom",
@ -362,40 +312,9 @@
"type": "definition", "type": "definition",
"named": true "named": true
}, },
{
"type": "fixity",
"named": true
},
{ {
"type": "preprocess", "type": "preprocess",
"named": true "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": "(", "type": "(",
"named": false "named": false
@ -489,6 +378,10 @@
"type": ",", "type": ",",
"named": false "named": false
}, },
{
"type": "->",
"named": false
},
{ {
"type": ":", "type": ":",
"named": false "named": false
@ -537,10 +430,6 @@
"type": "fun", "type": "fun",
"named": false "named": false
}, },
{
"type": "hypothesis",
"named": false
},
{ {
"type": "identifier", "type": "identifier",
"named": true "named": true
@ -549,14 +438,6 @@
"type": "in", "type": "in",
"named": false "named": false
}, },
{
"type": "infixl",
"named": false
},
{
"type": "infixr",
"named": false
},
{ {
"type": "let", "type": "let",
"named": false "named": false
@ -565,26 +446,10 @@
"type": "post_command", "type": "post_command",
"named": true "named": true
}, },
{
"type": "precedence",
"named": true
},
{
"type": "section",
"named": false
},
{ {
"type": "star", "type": "star",
"named": true "named": true
}, },
{
"type": "symbol",
"named": true
},
{
"type": "variable",
"named": false
},
{ {
"type": "λ", "type": "λ",
"named": false "named": false

7349
src/parser.c generated
View file

File diff suppressed because it is too large Load diff

57
test/corpus/application.txt
View file

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

36
test/corpus/arrows.txt
View file

@ -2,11 +2,11 @@
Arrows 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 (program
(definition (definition
(identifier) (identifier)
(param_block (param_block
@ -14,48 +14,42 @@ def foo (A B : ★) (f : A → A → B) (x : A) := f x x;
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(star)))))))) (star)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(arrow (arrow
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))) (identifier))))
(expr (expr
(arrow (arrow
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))) (identifier))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))))))) (identifier))))))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term
(identifier))))))
(expr
(app_term
(app
(term
(identifier))
(term
(identifier))
(term (term
(identifier))))))) (identifier)))))))
(expr
(app_term
(binex
(app
(term
(identifier))
(term
(identifier))
(term
(identifier))))))))

7
test/corpus/axioms.txt
View file

@ -2,18 +2,17 @@
Axioms Axioms
====== ======
axiom nat : ★; axiom nat : *;
----- -----
(program (program
(axiom (axiom
(identifier) (identifier)
(ascription (ascription
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(star)))))))))) (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))))))))

10
test/corpus/include.txt
View file

@ -4,13 +4,13 @@ Include
@include foo.pg @include foo.pg
def baz : ★ := A; def baz : * := A;
@include bar.pg @include bar.pg
--- ---
(program (program
(preprocess (preprocess
(command) (command)
(post_command)) (post_command))
@ -19,17 +19,15 @@ def baz : ★ := A;
(ascription (ascription
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(star)))))))) (star)))))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(preprocess (preprocess
(command) (command)
(post_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)))))))))))

16
test/corpus/labs.txt
View file

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

20
test/corpus/let.txt
View file

@ -12,7 +12,7 @@ def foo :=
--- ---
(program (program
(definition (definition
(identifier) (identifier)
(expr (expr
@ -23,43 +23,37 @@ def foo :=
(ascription (ascription
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(binding (binding
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(binding (binding
(identifier) (identifier)
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))))))) (identifier))))))))))

13
test/corpus/pabs.txt
View file

@ -2,11 +2,11 @@
Pi Abstraction Pi Abstraction
============== ==============
def rel := forall (A : ★) (x : A), ★; def rel := forall (A : *) (x : A), *;
---------- ----------
(program (program
(definition (definition
(identifier) (identifier)
(expr (expr
@ -16,23 +16,20 @@ def rel := forall (A : ★) (x : A), ★;
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(star)))))))) (star)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier))))))) (identifier))))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(star)))))))))))) (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)))

28
test/corpus/sorts.txt
View file

@ -2,79 +2,71 @@
Sorts 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 (program
(definition (definition
(identifier) (identifier)
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(star)))))))) (star)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(square)))))))) (square)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(square)))))))) (square)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(square)))))))) (square)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(square)))))))) (square)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(square)))))))) (square)))))))
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(sort (sort
(square)))))))) (square)))))))
(expr (expr
(app_term (app_term
(binex
(app (app
(term (term
(identifier)))))))) (identifier)))))))