operator sections

This commit is contained in:
William Ball 2024-12-10 23:39:53 -08:00
parent 4131069cd4
commit 483fa6ec49
6 changed files with 4345 additions and 4050 deletions

View file

@ -46,15 +46,17 @@ module.exports = grammar({
';' ';'
), ),
variable : $ => seq( variable_binding : $ => seq(
choice('variable', 'hypothesis'),
repeat1(seq(
'(', '(',
repeat1(choice($.identifier, $.symbol)), repeat1(choice($.identifier, $.symbol)),
':', ':',
field('type', $.expr), field('type', $.expr),
')' ')',
)), ),
variable : $ => seq(
choice('variable', 'hypothesis'),
repeat1($.variable_binding),
';' ';'
), ),
@ -86,9 +88,16 @@ module.exports = grammar({
$.expr, $.expr,
), ),
op_section : $ => seq(
'(',
$.symbol,
')',
),
term : $ => choice( term : $ => choice(
$.identifier, $.identifier,
$.sort, $.sort,
$.op_section,
seq('(', $.expr, ')'), seq('(', $.expr, ')'),
), ),

63
src/grammar.json generated
View file

@ -116,25 +116,7 @@
} }
] ]
}, },
"variable": { "variable_binding": {
"type": "SEQ",
"members": [
{
"type": "CHOICE",
"members": [
{
"type": "STRING",
"value": "variable"
},
{
"type": "STRING",
"value": "hypothesis"
}
]
},
{
"type": "REPEAT1",
"content": {
"type": "SEQ", "type": "SEQ",
"members": [ "members": [
{ {
@ -174,6 +156,28 @@
"value": ")" "value": ")"
} }
] ]
},
"variable": {
"type": "SEQ",
"members": [
{
"type": "CHOICE",
"members": [
{
"type": "STRING",
"value": "variable"
},
{
"type": "STRING",
"value": "hypothesis"
}
]
},
{
"type": "REPEAT1",
"content": {
"type": "SYMBOL",
"name": "variable_binding"
} }
}, },
{ {
@ -360,6 +364,23 @@
} }
] ]
}, },
"op_section": {
"type": "SEQ",
"members": [
{
"type": "STRING",
"value": "("
},
{
"type": "SYMBOL",
"name": "symbol"
},
{
"type": "STRING",
"value": ")"
}
]
},
"term": { "term": {
"type": "CHOICE", "type": "CHOICE",
"members": [ "members": [
@ -371,6 +392,10 @@
"type": "SYMBOL", "type": "SYMBOL",
"name": "sort" "name": "sort"
}, },
{
"type": "SYMBOL",
"name": "op_section"
},
{ {
"type": "SEQ", "type": "SEQ",
"members": [ "members": [

36
src/node-types.json generated
View file

@ -278,6 +278,21 @@
] ]
} }
}, },
{
"type": "op_section",
"named": true,
"fields": {},
"children": {
"multiple": false,
"required": true,
"types": [
{
"type": "symbol",
"named": true
}
]
}
},
{ {
"type": "pabs", "type": "pabs",
"named": true, "named": true,
@ -440,6 +455,10 @@
"type": "identifier", "type": "identifier",
"named": true "named": true
}, },
{
"type": "op_section",
"named": true
},
{ {
"type": "sort", "type": "sort",
"named": true "named": true
@ -450,9 +469,24 @@
{ {
"type": "variable", "type": "variable",
"named": true, "named": true,
"fields": {},
"children": {
"multiple": true,
"required": true,
"types": [
{
"type": "variable_binding",
"named": true
}
]
}
},
{
"type": "variable_binding",
"named": true,
"fields": { "fields": {
"type": { "type": {
"multiple": true, "multiple": false,
"required": true, "required": true,
"types": [ "types": [
{ {

8143
src/parser.c generated

File diff suppressed because it is too large Load diff

View file

@ -0,0 +1,22 @@
=================
Operator Sections
=================
def foo := (+) one two;
---
(program
(definition
(identifier)
(expr
(app_term
(binex
(app
(term
(op_section
(symbol)))
(term
(identifier))
(term
(identifier))))))))

View file

@ -18,6 +18,7 @@ end Test
(identifier) (identifier)
(program (program
(variable (variable
(variable_binding
(identifier) (identifier)
(identifier) (identifier)
(identifier) (identifier)
@ -27,23 +28,9 @@ end Test
(app (app
(term (term
(sort (sort
(star)))))))) (star)))))))))
(variable (variable
(identifier) (variable_binding
(expr
(app_term
(binex
(app
(term
(identifier))))))
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier))))))
(identifier)
(identifier) (identifier)
(expr (expr
(app_term (app_term
@ -51,6 +38,23 @@ end Test
(app (app
(term (term
(identifier))))))) (identifier)))))))
(variable_binding
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier)))))))
(variable_binding
(identifier)
(identifier)
(expr
(app_term
(binex
(app
(term
(identifier))))))))
(section (section
(identifier) (identifier)
(program (program