added block comments

This commit is contained in:
William Ball 2024-11-21 13:14:46 -08:00
parent e5e219e0e9
commit ece43957c9
10 changed files with 853 additions and 679 deletions

View file

@ -10,17 +10,32 @@
module.exports = grammar({ module.exports = grammar({
name: "perga", name: "perga",
extras: $ => [
$.comment,
$.block_comment,
/\s/,
],
rules: { rules: {
program : $ => repeat(choice( program : $ => repeat($.definition),
$.definition,
$.comment,
)),
identifier : $ => /[a-zA-Z_]\w*/, identifier : $ => /[a-zA-Z_]\w*/,
comment : $ => token(seq('--', /.*/)), comment : $ => token(seq('--', /.*/)),
block_comment: $ => token(seq(
'[*',
repeat(choice(
/[^\[\]*]/,
/\[[^*]/,
/\*[^\]]/,
/\[\*/,
/\*\]/,
)),
'*]'
)),
param_block : $ => seq( param_block : $ => seq(
'(', '(',
field('param', repeat($.identifier)), field('param', repeat($.identifier)),

65
src/grammar.json generated
View file

@ -4,17 +4,8 @@
"program": { "program": {
"type": "REPEAT", "type": "REPEAT",
"content": { "content": {
"type": "CHOICE", "type": "SYMBOL",
"members": [ "name": "definition"
{
"type": "SYMBOL",
"name": "definition"
},
{
"type": "SYMBOL",
"name": "comment"
}
]
} }
}, },
"identifier": { "identifier": {
@ -37,6 +28,50 @@
] ]
} }
}, },
"block_comment": {
"type": "TOKEN",
"content": {
"type": "SEQ",
"members": [
{
"type": "STRING",
"value": "[*"
},
{
"type": "REPEAT",
"content": {
"type": "CHOICE",
"members": [
{
"type": "PATTERN",
"value": "[^\\[\\]*]"
},
{
"type": "PATTERN",
"value": "\\[[^*]"
},
{
"type": "PATTERN",
"value": "\\*[^\\]]"
},
{
"type": "PATTERN",
"value": "\\[\\*"
},
{
"type": "PATTERN",
"value": "\\*\\]"
}
]
}
},
{
"type": "STRING",
"value": "*]"
}
]
}
},
"param_block": { "param_block": {
"type": "SEQ", "type": "SEQ",
"members": [ "members": [
@ -342,6 +377,14 @@
} }
}, },
"extras": [ "extras": [
{
"type": "SYMBOL",
"name": "comment"
},
{
"type": "SYMBOL",
"name": "block_comment"
},
{ {
"type": "PATTERN", "type": "PATTERN",
"value": "\\s" "value": "\\s"

8
src/node-types.json generated
View file

@ -201,10 +201,6 @@
"multiple": true, "multiple": true,
"required": false, "required": false,
"types": [ "types": [
{
"type": "comment",
"named": true
},
{ {
"type": "definition", "type": "definition",
"named": true "named": true
@ -284,6 +280,10 @@
"type": "axiom", "type": "axiom",
"named": true "named": true
}, },
{
"type": "block_comment",
"named": true
},
{ {
"type": "comment", "type": "comment",
"named": true "named": true

1235
src/parser.c generated

File diff suppressed because it is too large Load diff

View file

@ -0,0 +1,66 @@
===========
Application
===========
foo (A B : *) (f : A -> B) (x : A) :=
(fun (x : B) => x) (f x);
---
(program
(definition
(identifier)
(param_block
(identifier)
(identifier)
(expr
(app_term
(app
(term
(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
(term
(identifier))
(term
(identifier)))))))))))

View file

@ -10,46 +10,39 @@ foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
(definition (definition
(identifier) (identifier)
(param_block (param_block
(param (identifier)
(identifier)) (identifier)
(param (expr
(identifier)) (app_term
(type (app
(expr (term
(star))))))
(param_block
(identifier)
(expr
(arrow
(app_term (app_term
(app (app
(term (term
(star))))))) (identifier))))
(param_block (expr
(param (arrow
(identifier)) (app_term
(type (app
(expr (term
(arrow (identifier))))
(app_term (expr
(app
(term
(identifier))))
(expr
(arrow
(app_term (app_term
(app (app
(term (term
(identifier)))) (identifier))))))))))
(expr
(app_term
(app
(term
(identifier)))))))))))
(param_block (param_block
(param (identifier)
(identifier)) (expr
(type (app_term
(expr (app
(app_term (term
(app (identifier))))))
(term
(identifier)))))))
(expr (expr
(app_term (app_term
(app (app

View file

@ -10,10 +10,9 @@ nat : * := axiom;
(definition (definition
(identifier) (identifier)
(ascription (ascription
(type (expr
(expr (app_term
(app_term (app
(app (term
(term (star))))))
(star)))))))
(axiom))) (axiom)))

View file

@ -4,7 +4,10 @@ Comments
-- here's a comment -- here's a comment
foo := *; foo :=
-- and a comment in the middle
[* and a [* nested *] block comment *]
*;
--- ---
@ -12,6 +15,8 @@ foo := *;
(comment) (comment)
(definition (definition
(identifier) (identifier)
(comment)
(block_comment)
(expr (expr
(app_term (app_term
(app (app

View file

@ -12,25 +12,20 @@ foo := fun (A : *) (x : A) => x;
(expr (expr
(app_term (app_term
(labs (labs
(lambda)
(param_block (param_block
(param (identifier)
(identifier)) (expr
(type (app_term
(expr (app
(app_term (term
(app (star))))))
(term
(star)))))))
(param_block (param_block
(param (identifier)
(identifier)) (expr
(type (app_term
(expr (app
(app_term (term
(app (identifier))))))
(term
(identifier)))))))
(expr (expr
(app_term (app_term
(app (app

View file

@ -12,25 +12,20 @@ rel := forall (A : *) (x : A), *;
(expr (expr
(app_term (app_term
(pabs (pabs
(pi)
(param_block (param_block
(param (identifier)
(identifier)) (expr
(type (app_term
(expr (app
(app_term (term
(app (star))))))
(term
(star)))))))
(param_block (param_block
(param (identifier)
(identifier)) (expr
(type (app_term
(expr (app
(app_term (term
(app (identifier))))))
(term
(identifier)))))))
(expr (expr
(app_term (app_term
(app (app