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

infix operators

Browse source
This commit is contained in:
William Ball 2024-12-10 21:40:39 -08:00
parent 3834eb6f0a
commit 4131069cd4
16 changed files with 5502 additions and 3380 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
grammar.js
View file

@ -17,9 +17,17 @@ module.exports = grammar({
rules: { rules: {
program : $ => repeat1(choice($.definition, $.preprocess, $.axiom, $.section, $.variable)), program : $ => repeat1(choice(
$.definition,
$.preprocess,
$.axiom,
$.section,
$.variable,
$.fixity,
)),
identifier : $ => /[a-zA-Z_]\w*/, identifier : $ => /[a-zA-Z_]\w*/,
symbol : $ => /[!@#$%^&*-+=<>,./?\[\]{}\\|`~'\"∧∨⊙×≅]+/,
comment : $ => token(seq('--', /.*/)), comment : $ => token(seq('--', /.*/)),
@ -29,9 +37,24 @@ module.exports = grammar({
'end', $.identifier, 'end', $.identifier,
), ),
precedence : $ => /[0-9]+/,
fixity : $ => seq(
choice('infixl', 'infixr'),
$.precedence,
$.symbol,
';'
),
variable : $ => seq( variable : $ => seq(
choice('variable', 'hypothesis'), choice('variable', 'hypothesis'),
repeat1($.param_block), repeat1(seq(
'(',
repeat1(choice($.identifier, $.symbol)),
':',
field('type', $.expr),
')'
)),
';' ';'
), ),
@ -43,7 +66,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₀₁₂₃₄₅₆₇₈₉]+/)),
@ -69,6 +92,14 @@ 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,
@ -91,7 +122,7 @@ module.exports = grammar({
arrow : $ => prec.left(1, seq( arrow : $ => prec.left(1, seq(
$.app_term, $.app_term,
choice('->', '→'), '→',
$.expr, $.expr,
)), )),
@ -99,7 +130,7 @@ module.exports = grammar({
$.labs, $.labs,
$.pabs, $.pabs,
$.let, $.let,
$.app, $.binex,
), ),
expr : $ => choice( expr : $ => choice(
@ -114,7 +145,7 @@ module.exports = grammar({
axiom : $ => seq( axiom : $ => seq(
'axiom', 'axiom',
field('name', $.identifier), field('name', choice($.identifier, $.symbol)),
repeat($.param_block), repeat($.param_block),
$.ascription, $.ascription,
';' ';'
@ -122,11 +153,11 @@ module.exports = grammar({
definition : $ => seq( definition : $ => seq(
'def', 'def',
field('name', $.identifier), field('name', choice($.identifier, $.symbol)),
repeat($.param_block), repeat($.param_block),
optional($.ascription), optional($.ascription),
':=', ':=',
choice($.expr), $.expr,
';', ';',
), ),

165
src/grammar.json generated
View file

@ -25,6 +25,10 @@
{ {
"type": "SYMBOL", "type": "SYMBOL",
"name": "variable" "name": "variable"
},
{
"type": "SYMBOL",
"name": "fixity"
} }
] ]
} }
@ -33,6 +37,10 @@
"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": {
@ -74,6 +82,40 @@
} }
] ]
}, },
"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": { "variable": {
"type": "SEQ", "type": "SEQ",
"members": [ "members": [
@ -93,8 +135,45 @@
{ {
"type": "REPEAT1", "type": "REPEAT1",
"content": { "content": {
"type": "SYMBOL", "type": "SEQ",
"name": "param_block" "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": ")"
}
]
} }
}, },
{ {
@ -141,7 +220,7 @@
}, },
"star": { "star": {
"type": "STRING", "type": "STRING",
"value": "*" "value": "★"
}, },
"square": { "square": {
"type": "CHOICE", "type": "CHOICE",
@ -311,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": { "binding": {
"type": "SEQ", "type": "SEQ",
"members": [ "members": [
@ -401,17 +510,8 @@
"name": "app_term" "name": "app_term"
}, },
{ {
"type": "CHOICE", "type": "STRING",
"members": [ "value": "→"
{
"type": "STRING",
"value": "->"
},
{
"type": "STRING",
"value": "→"
}
]
}, },
{ {
"type": "SYMBOL", "type": "SYMBOL",
@ -437,7 +537,7 @@
}, },
{ {
"type": "SYMBOL", "type": "SYMBOL",
"name": "app" "name": "binex"
} }
] ]
}, },
@ -482,8 +582,17 @@
"type": "FIELD", "type": "FIELD",
"name": "name", "name": "name",
"content": { "content": {
"type": "SYMBOL", "type": "CHOICE",
"name": "identifier" "members": [
{
"type": "SYMBOL",
"name": "identifier"
},
{
"type": "SYMBOL",
"name": "symbol"
}
]
} }
}, },
{ {
@ -514,8 +623,17 @@
"type": "FIELD", "type": "FIELD",
"name": "name", "name": "name",
"content": { "content": {
"type": "SYMBOL", "type": "CHOICE",
"name": "identifier" "members": [
{
"type": "SYMBOL",
"name": "identifier"
},
{
"type": "SYMBOL",
"name": "symbol"
}
]
} }
}, },
{ {
@ -542,13 +660,8 @@
"value": ":=" "value": ":="
}, },
{ {
"type": "CHOICE", "type": "SYMBOL",
"members": [ "name": "expr"
{
"type": "SYMBOL",
"name": "expr"
}
]
}, },
{ {
"type": "STRING", "type": "STRING",

95
src/node-types.json generated
View file

@ -23,7 +23,7 @@
"required": true, "required": true,
"types": [ "types": [
{ {
"type": "app", "type": "binex",
"named": true "named": true
}, },
{ {
@ -87,6 +87,10 @@
{ {
"type": "identifier", "type": "identifier",
"named": true "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", "type": "definition",
"named": true, "named": true,
@ -144,6 +171,10 @@
{ {
"type": "identifier", "type": "identifier",
"named": true "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", "type": "labs",
"named": true, "named": true,
@ -312,6 +362,10 @@
"type": "definition", "type": "definition",
"named": true "named": true
}, },
{
"type": "fixity",
"named": true
},
{ {
"type": "preprocess", "type": "preprocess",
"named": true "named": true
@ -396,13 +450,28 @@
{ {
"type": "variable", "type": "variable",
"named": true, "named": true,
"fields": {}, "fields": {
"type": {
"multiple": true,
"required": true,
"types": [
{
"type": "expr",
"named": true
}
]
}
},
"children": { "children": {
"multiple": true, "multiple": true,
"required": true, "required": true,
"types": [ "types": [
{ {
"type": "param_block", "type": "identifier",
"named": true
},
{
"type": "symbol",
"named": true "named": true
} }
] ]
@ -420,10 +489,6 @@
"type": ",", "type": ",",
"named": false "named": false
}, },
{
"type": "->",
"named": false
},
{ {
"type": ":", "type": ":",
"named": false "named": false
@ -484,6 +549,14 @@
"type": "in", "type": "in",
"named": false "named": false
}, },
{
"type": "infixl",
"named": false
},
{
"type": "infixr",
"named": false
},
{ {
"type": "let", "type": "let",
"named": false "named": false
@ -492,6 +565,10 @@
"type": "post_command", "type": "post_command",
"named": true "named": true
}, },
{
"type": "precedence",
"named": true
},
{ {
"type": "section", "type": "section",
"named": false "named": false
@ -500,6 +577,10 @@
"type": "star", "type": "star",
"named": true "named": true
}, },
{
"type": "symbol",
"named": true
},
{ {
"type": "variable", "type": "variable",
"named": false "named": false

7780
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 Application
=========== ===========
def foo (A B : *) (f : A -> B) (x : A) := def foo := f x;
(fun (x : B) => x) (f x);
--- ---
(program (program
(definition (definition
(identifier) (identifier)
(param_block (expr
(identifier)
(identifier)
(expr
(app_term
(app
(term
(sort
(star)))))))
(param_block
(identifier)
(expr
(arrow
(app_term (app_term
(app (binex
(term
(identifier))))
(expr
(app_term
(app (app
(term
(identifier))
(term (term
(identifier)))))))) (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 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
(identifier) (identifier)
(identifier) (identifier)
(expr (expr
(app_term (app_term
(app (binex
(term (app
(sort (term
(star))))))) (sort
(param_block (star))))))))
(identifier) (param_block
(expr (identifier)
(arrow
(app_term
(app
(term
(identifier))))
(expr (expr
(arrow (arrow
(app_term (app_term
(app (binex
(term
(identifier))))
(expr
(app_term
(app (app
(term (term
(identifier)))))))))) (identifier)))))
(param_block (expr
(identifier) (arrow
(expr (app_term
(app_term (binex
(app (app
(term (term
(identifier)))))) (identifier)))))
(expr (expr
(app_term (app_term
(app (binex
(term (app
(identifier)) (term
(term (identifier)))))))))))
(identifier)) (param_block
(term (identifier)
(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 Axioms
====== ======
axiom nat : *; axiom nat : ★;
----- -----
(program (program
(axiom (axiom
(identifier) (identifier)
(ascription (ascription
(expr (expr
(app_term (app_term
(app (binex
(term (app
(sort (term
(star))))))))) (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 @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))
(definition (definition
(identifier) (identifier)
(ascription (ascription
(expr (expr
(app_term (app_term
(app (binex
(term (app
(sort (term
(star))))))) (sort
(expr (star))))))))
(app_term (expr
(app (app_term
(term (binex
(identifier)))))) (app
(preprocess (term
(command) (identifier)))))))
(post_command))) (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 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
(app_term (app_term
(labs (labs
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(app (binex
(term (app
(sort (term
(star))))))) (sort
(param_block (star))))))))
(identifier) (param_block
(expr (identifier)
(app_term (expr
(app (app_term
(term (binex
(identifier)))))) (app
(ascription (term
(expr (identifier)))))))
(app_term (ascription
(app (expr
(term (app_term
(identifier)))))) (binex
(expr (app
(app_term (term
(app (identifier)))))))
(term (expr
(identifier)))))))))) (app_term
(binex
(app
(term
(identifier)))))))))))

92
test/corpus/let.txt
View file

@ -12,48 +12,54 @@ def foo :=
--- ---
(program (program
(definition (definition
(identifier) (identifier)
(expr (expr
(app_term (app_term
(let (let
(binding (binding
(identifier) (identifier)
(ascription (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 (expr
(app_term (app_term
(app (binex
(term (app
(identifier)))))) (term
(expr (identifier)))))))))))
(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,34 +2,37 @@
Pi Abstraction Pi Abstraction
============== ==============
def rel := forall (A : *) (x : A), *; def rel := forall (A : ★) (x : A), ★;
---------- ----------
(program (program
(definition (definition
(identifier) (identifier)
(expr (expr
(app_term (app_term
(pabs (pabs
(param_block (param_block
(identifier) (identifier)
(expr (expr
(app_term (app_term
(app (binex
(term (app
(sort (term
(star))))))) (sort
(param_block (star))))))))
(identifier) (param_block
(expr (identifier)
(app_term (expr
(app (app_term
(term (binex
(identifier)))))) (app
(expr (term
(app_term (identifier)))))))
(app (expr
(term (app_term
(sort (binex
(star))))))))))) (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)))))))

96
test/corpus/section.txt
View file

@ -3,7 +3,7 @@ Sections
======== ========
section Test section Test
variable (A B C : *); variable (A B C : ★);
hypothesis (x : A) (y : B) (z1 z2 : C); hypothesis (x : A) (y : B) (z1 z2 : C);
section Nested section Nested
@ -13,60 +13,62 @@ end Test
---- ----
(program
(section
(identifier)
(program (program
(variable
(param_block
(identifier)
(identifier)
(identifier)
(expr
(app_term
(app
(term
(sort
(star))))))))
(variable
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(param_block
(identifier)
(expr
(app_term
(app
(term
(identifier))))))
(param_block
(identifier)
(identifier)
(expr
(app_term
(app
(term
(identifier)))))))
(section (section
(identifier) (identifier)
(program (program
(definition (variable
(identifier) (identifier)
(param_block (identifier)
(identifier) (identifier)
(expr (expr
(app_term (app_term
(binex
(app
(term
(sort
(star))))))))
(variable
(identifier)
(expr
(app_term
(binex
(app (app
(term (term
(identifier)))))) (identifier))))))
(identifier)
(expr (expr
(app_term (app_term
(app (binex
(term (app
(identifier))))))) (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))) (identifier)))
(identifier)))

138
test/corpus/sorts.txt
View file

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