181 lines
3.2 KiB
JavaScript
181 lines
3.2 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,
|
|
/\s/,
|
|
],
|
|
|
|
rules: {
|
|
|
|
program : $ => repeat1(choice(
|
|
$.definition,
|
|
$.preprocess,
|
|
$.axiom,
|
|
$.section,
|
|
$.variable,
|
|
$.fixity,
|
|
)),
|
|
|
|
comment : $ => token(seq('--', /.*/)),
|
|
|
|
section : $ => seq(
|
|
'section', $.identifier,
|
|
$.program,
|
|
'end', $.identifier,
|
|
),
|
|
|
|
precedence : $ => /[0-9]+/,
|
|
|
|
fixity : $ => seq(
|
|
choice('infixl', 'infixr'),
|
|
$.precedence,
|
|
$.symbol,
|
|
';'
|
|
),
|
|
|
|
variable : $ => seq(
|
|
choice('variable', 'hypothesis'),
|
|
repeat1($.param_block),
|
|
';'
|
|
),
|
|
|
|
param_block : $ => seq(
|
|
'(',
|
|
field('param', repeat1(choice($.identifier, $.symbol))),
|
|
':',
|
|
field('type', $.expr),
|
|
')'
|
|
),
|
|
|
|
star : $ => choice("★", "⋆"),
|
|
square : $ => choice('□', '[]'),
|
|
sort : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)),
|
|
|
|
labs : $ => seq(
|
|
choice('λ', 'fun'),
|
|
repeat1($.param_block),
|
|
choice('=>', '⇒'),
|
|
$.expr,
|
|
),
|
|
|
|
labs_alt : $ => seq(
|
|
'[',
|
|
field('param', repeat1($.identifier)),
|
|
':',
|
|
field('type', $.expr),
|
|
']',
|
|
$.expr,
|
|
),
|
|
|
|
pabs : $ => seq(
|
|
choice('∏', 'forall'),
|
|
repeat1($.param_block),
|
|
',',
|
|
$.expr,
|
|
),
|
|
|
|
op_section : $ => seq(
|
|
'(',
|
|
$.symbol,
|
|
')',
|
|
),
|
|
|
|
term : $ => choice(
|
|
$.identifier,
|
|
$.sort,
|
|
$.op_section,
|
|
seq('(', $.expr, ')'),
|
|
),
|
|
|
|
// HACK:
|
|
// completely ignore precedence and associativity for treesitter
|
|
// the syntax tree is completely wrong, but it's good enough for syntax
|
|
// highlighting
|
|
binex : $ => seq(
|
|
$.app,
|
|
optional(seq($.symbol, $.binex)),
|
|
),
|
|
|
|
binding : $ => seq(
|
|
'(',
|
|
$.identifier,
|
|
repeat($.param_block),
|
|
optional($.ascription),
|
|
':=',
|
|
$.expr,
|
|
')',
|
|
),
|
|
|
|
let : $ => seq(
|
|
'let',
|
|
repeat1($.binding),
|
|
'in',
|
|
$.expr,
|
|
'end',
|
|
),
|
|
|
|
app : $ => repeat1($.term),
|
|
|
|
arrow : $ => prec.left(1, seq(
|
|
$.app_term,
|
|
'→',
|
|
$.expr,
|
|
)),
|
|
|
|
app_term : $ => choice(
|
|
$.labs,
|
|
$.labs_alt,
|
|
$.pabs,
|
|
$.let,
|
|
$.binex,
|
|
),
|
|
|
|
expr : $ => choice(
|
|
$.app_term,
|
|
$.arrow,
|
|
),
|
|
|
|
ascription : $ => seq(
|
|
':',
|
|
field('type', $.expr),
|
|
),
|
|
|
|
axiom : $ => seq(
|
|
'axiom',
|
|
field('name', choice($.identifier, $.symbol)),
|
|
repeat($.param_block),
|
|
$.ascription,
|
|
';'
|
|
),
|
|
|
|
definition : $ => seq(
|
|
'def',
|
|
field('name', choice($.identifier, $.symbol)),
|
|
repeat($.param_block),
|
|
optional($.ascription),
|
|
':=',
|
|
$.expr,
|
|
';',
|
|
),
|
|
|
|
preprocess : $ => seq($.command, $.post_command),
|
|
|
|
post_command : $ => /.+/,
|
|
|
|
command : $ => '@include',
|
|
|
|
identifier : $ => /[a-zA-Z_]\w*/,
|
|
symbol : $ => /[!@#$%^&*-+=<>,./?{}\\|`~'\"∧∨⊙×≅]+/,
|
|
|
|
}
|
|
});
|