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

getting closer?

Browse source
This commit is contained in:
William Ball 2024-11-20 21:46:51 -08:00
parent ec8579d599
commit 3db7a588ad
10 changed files with 759 additions and 655 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
grammar.js
View file

@ -21,32 +21,26 @@ module.exports = grammar({
comment : $ => token(seq('--', /.*/)), comment : $ => token(seq('--', /.*/)),
param : $ => $.identifier,
param_block : $ => seq( param_block : $ => seq(
'(', '(',
repeat($.param), field('param', repeat($.identifier)),
':', ':',
$.type, field('type', $.expr),
')' ')'
), ),
type : $ => $.expr,
star : $ => "*", star : $ => "*",
square : $ => choice('□', '[]'), square : $ => choice('□', '[]'),
lambda : $ => choice('λ', 'fun'),
pi : $ => choice('∏', 'forall'),
labs : $ => seq( labs : $ => seq(
$.lambda, choice('λ', 'fun'),
repeat1($.param_block), repeat1($.param_block),
choice('=>', '⇒'), choice('=>', '⇒'),
$.expr, $.expr,
), ),
pabs : $ => seq( pabs : $ => seq(
$.pi, choice('∏', 'forall'),
repeat1($.param_block), repeat1($.param_block),
',', ',',
$.expr, $.expr,
@ -82,11 +76,11 @@ module.exports = grammar({
ascription : $ => seq( ascription : $ => seq(
':', ':',
$.type, field('type', $.expr),
), ),
definition : $ => seq( definition : $ => seq(
$.identifier, field('name', $.identifier),
repeat($.param_block), repeat($.param_block),
optional($.ascription), optional($.ascription),
':=', ':=',

55
src/grammar.json generated
View file

@ -1,5 +1,4 @@
{ {
"$schema": "https://tree-sitter.github.io/tree-sitter/assets/schemas/grammar.schema.json",
"name": "perga", "name": "perga",
"rules": { "rules": {
"program": { "program": {
@ -46,19 +45,27 @@
"value": "(" "value": "("
}, },
{ {
"type": "FIELD",
"name": "param",
"content": {
"type": "REPEAT", "type": "REPEAT",
"content": { "content": {
"type": "SYMBOL", "type": "SYMBOL",
"name": "identifier" "name": "identifier"
} }
}
}, },
{ {
"type": "STRING", "type": "STRING",
"value": ":" "value": ":"
}, },
{ {
"type": "FIELD",
"name": "type",
"content": {
"type": "SYMBOL", "type": "SYMBOL",
"name": "expr" "name": "expr"
}
}, },
{ {
"type": "STRING", "type": "STRING",
@ -83,7 +90,10 @@
} }
] ]
}, },
"lambda": { "labs": {
"type": "SEQ",
"members": [
{
"type": "CHOICE", "type": "CHOICE",
"members": [ "members": [
{ {
@ -96,26 +106,6 @@
} }
] ]
}, },
"pi": {
"type": "CHOICE",
"members": [
{
"type": "STRING",
"value": "∏"
},
{
"type": "STRING",
"value": "forall"
}
]
},
"labs": {
"type": "SEQ",
"members": [
{
"type": "SYMBOL",
"name": "lambda"
},
{ {
"type": "REPEAT1", "type": "REPEAT1",
"content": { "content": {
@ -146,8 +136,17 @@
"type": "SEQ", "type": "SEQ",
"members": [ "members": [
{ {
"type": "SYMBOL", "type": "CHOICE",
"name": "pi" "members": [
{
"type": "STRING",
"value": "∏"
},
{
"type": "STRING",
"value": "forall"
}
]
}, },
{ {
"type": "REPEAT1", "type": "REPEAT1",
@ -279,17 +278,25 @@
"value": ":" "value": ":"
}, },
{ {
"type": "FIELD",
"name": "type",
"content": {
"type": "SYMBOL", "type": "SYMBOL",
"name": "expr" "name": "expr"
} }
}
] ]
}, },
"definition": { "definition": {
"type": "SEQ", "type": "SEQ",
"members": [ "members": [
{ {
"type": "FIELD",
"name": "name",
"content": {
"type": "SYMBOL", "type": "SYMBOL",
"name": "identifier" "name": "identifier"
}
}, },
{ {
"type": "REPEAT", "type": "REPEAT",

60
src/node-types.json generated
View file

@ -59,8 +59,8 @@
{ {
"type": "ascription", "type": "ascription",
"named": true, "named": true,
"fields": {}, "fields": {
"children": { "type": {
"multiple": false, "multiple": false,
"required": true, "required": true,
"types": [ "types": [
@ -70,11 +70,23 @@
} }
] ]
} }
}
}, },
{ {
"type": "definition", "type": "definition",
"named": true, "named": true,
"fields": {}, "fields": {
"name": {
"multiple": false,
"required": true,
"types": [
{
"type": "identifier",
"named": true
}
]
}
},
"children": { "children": {
"multiple": true, "multiple": true,
"required": true, "required": true,
@ -91,10 +103,6 @@
"type": "expr", "type": "expr",
"named": true "named": true
}, },
{
"type": "identifier",
"named": true
},
{ {
"type": "param_block", "type": "param_block",
"named": true "named": true
@ -133,10 +141,6 @@
"type": "expr", "type": "expr",
"named": true "named": true
}, },
{
"type": "lambda",
"named": true
},
{ {
"type": "param_block", "type": "param_block",
"named": true "named": true
@ -144,11 +148,6 @@
] ]
} }
}, },
{
"type": "lambda",
"named": true,
"fields": {}
},
{ {
"type": "pabs", "type": "pabs",
"named": true, "named": true,
@ -164,10 +163,6 @@
{ {
"type": "param_block", "type": "param_block",
"named": true "named": true
},
{
"type": "pi",
"named": true
} }
] ]
} }
@ -175,31 +170,32 @@
{ {
"type": "param_block", "type": "param_block",
"named": true, "named": true,
"fields": {}, "fields": {
"children": { "param": {
"multiple": true, "multiple": true,
"required": true, "required": false,
"types": [ "types": [
{
"type": "expr",
"named": true
},
{ {
"type": "identifier", "type": "identifier",
"named": true "named": true
} }
] ]
}
}, },
"type": {
"multiple": false,
"required": true,
"types": [
{ {
"type": "pi", "type": "expr",
"named": true, "named": true
"fields": {} }
]
}
}
}, },
{ {
"type": "program", "type": "program",
"named": true, "named": true,
"root": true,
"fields": {}, "fields": {},
"children": { "children": {
"multiple": true, "multiple": true,

1011
src/parser.c generated
View file

File diff suppressed because it is too large Load diff

8
src/tree_sitter/alloc.h generated
View file

@ -12,10 +12,10 @@ extern "C" {
// Allow clients to override allocation functions // Allow clients to override allocation functions
#ifdef TREE_SITTER_REUSE_ALLOCATOR #ifdef TREE_SITTER_REUSE_ALLOCATOR
extern void *(*ts_current_malloc)(size_t size); extern void *(*ts_current_malloc)(size_t);
extern void *(*ts_current_calloc)(size_t count, size_t size); extern void *(*ts_current_calloc)(size_t, size_t);
extern void *(*ts_current_realloc)(void *ptr, size_t size); extern void *(*ts_current_realloc)(void *, size_t);
extern void (*ts_current_free)(void *ptr); extern void (*ts_current_free)(void *);
#ifndef ts_malloc #ifndef ts_malloc
#define ts_malloc ts_current_malloc #define ts_malloc ts_current_malloc

21
test/corpus/arrows.txt
View file

@ -10,15 +10,20 @@ foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
(definition (definition
(identifier) (identifier)
(param_block (param_block
(identifier) (param
(identifier) (identifier))
(param
(identifier))
(type
(expr (expr
(app_term (app_term
(app (app
(term (term
(star)))))) (star)))))))
(param_block (param_block
(identifier) (param
(identifier))
(type
(expr (expr
(arrow (arrow
(app_term (app_term
@ -35,14 +40,16 @@ foo (A B : *) (f : A -> A -> B) (x : A) := f x x;
(app_term (app_term
(app (app
(term (term
(identifier)))))))))) (identifier)))))))))))
(param_block (param_block
(identifier) (param
(identifier))
(type
(expr (expr
(app_term (app_term
(app (app
(term (term
(identifier)))))) (identifier)))))))
(expr (expr
(app_term (app_term
(app (app

3
test/corpus/axioms.txt
View file

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

12
test/corpus/labs.txt
View file

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

12
test/corpus/pabs.txt
View file

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

26
test/corpus/params.txt
View file

@ -10,21 +10,27 @@ foo (A : *) (x y z : A) := x;
(definition (definition
(identifier) (identifier)
(param_block (param_block
(identifier) (param
(identifier))
(type
(expr (expr
(app_term (app_term
(app (app
(term (term
(star)))))) (star)))))))
(param_block (param_block
(identifier) (param
(identifier) (identifier))
(identifier) (param
(expr (identifier))
(app_term (param
(app (identifier))
(term (type
(identifier)))))) (expr
(app_term
(app
(term
(identifier)))))))
(expr (expr
(app_term (app_term
(app (app