tree-sitter-perga/grammar.js

/**
 * @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,
    )),

    identifier : $ => /[a-zA-Z_]\w*/,
    symbol     : $ => /[!@#$%^&*-+=<>,./?{}\\|`~'\"∧∨⊙×≅]+/,

    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   : $ => "★",
    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',

  }
});