113 lines
1.9 KiB
JavaScript
113 lines
1.9 KiB
JavaScript
/**
|
|
* @file Basic proof assistant based on Calculus of Constructions
|
|
* @author William Ball <williampi103@gmail.com>
|
|
* @license GPL3
|
|
*/
|
|
|
|
/// <reference types="tree-sitter-cli/dsl" />
|
|
// @ts-check
|
|
|
|
module.exports = grammar({
|
|
name: "perga",
|
|
|
|
extras: $ => [
|
|
$.comment,
|
|
$.block_comment,
|
|
/\s/,
|
|
],
|
|
|
|
rules: {
|
|
|
|
program : $ => repeat(choice($.definition, $.preprocess)),
|
|
|
|
identifier : $ => /[a-zA-Z_]\w*/,
|
|
|
|
comment : $ => token(seq('--', /.*/)),
|
|
|
|
block_comment: $ => token(seq(
|
|
'[*',
|
|
repeat(choice(
|
|
/[^\[\]*]/,
|
|
/\[[^*]/,
|
|
/\*[^\]]/,
|
|
/\[\*/,
|
|
/\*\]/,
|
|
)),
|
|
'*]'
|
|
)),
|
|
|
|
param_block : $ => seq(
|
|
'(',
|
|
field('param', repeat($.identifier)),
|
|
':',
|
|
field('type', $.expr),
|
|
')'
|
|
),
|
|
|
|
star : $ => "*",
|
|
square : $ => choice('□', '[]'),
|
|
|
|
labs : $ => seq(
|
|
choice('λ', 'fun'),
|
|
repeat1($.param_block),
|
|
choice('=>', '⇒'),
|
|
$.expr,
|
|
),
|
|
|
|
pabs : $ => seq(
|
|
choice('∏', 'forall'),
|
|
repeat1($.param_block),
|
|
',',
|
|
$.expr,
|
|
),
|
|
|
|
term : $ => choice(
|
|
$.identifier,
|
|
$.star,
|
|
$.square,
|
|
seq('(', $.expr, ')'),
|
|
),
|
|
|
|
app : $ => repeat1($.term),
|
|
|
|
axiom : $ => 'axiom',
|
|
|
|
arrow : $ => prec.left(1, seq(
|
|
$.app_term,
|
|
choice('->', '→'),
|
|
$.expr,
|
|
)),
|
|
|
|
app_term : $ => choice(
|
|
$.labs,
|
|
$.pabs,
|
|
$.app,
|
|
),
|
|
|
|
expr : $ => choice(
|
|
$.app_term,
|
|
$.arrow,
|
|
),
|
|
|
|
ascription : $ => seq(
|
|
':',
|
|
field('type', $.expr),
|
|
),
|
|
|
|
definition : $ => seq(
|
|
field('name', $.identifier),
|
|
repeat($.param_block),
|
|
optional($.ascription),
|
|
':=',
|
|
choice($.expr, $.axiom),
|
|
';',
|
|
),
|
|
|
|
preprocess : $ => seq($.command, $.post_command),
|
|
|
|
post_command : $ => /.+/,
|
|
|
|
command : $ => '@include',
|
|
|
|
}
|
|
});
|