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",

  rules: {

    program : $ => repeat(choice(
      $.definition,
      $.comment,
    )),

    identifier : $ => /[a-zA-Z_]\w*/,

    comment : $ => token(seq('--', /.*/)),

    param : $ => $.identifier,

    param_block : $ => seq(
      '(',
      repeat($.param),
      ':',
      $.type,
      ')'
    ),

    type : $ => $.expr,

    star   : $ => "*",
    square : $ => choice('□', '[]'),
    lambda : $ => choice('λ', 'fun'),
    pi     : $ => choice('∏', 'forall'),

    labs : $ => seq(
      $.lambda,
      repeat1($.param_block),
      choice('=>', '⇒'),
      $.expr,
    ),

    pabs : $ => seq(
      $.pi,
      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(
      ':',
      $.type,
    ),

    definition : $ => seq(
      $.identifier,
      repeat($.param_block),
      optional($.ascription),
      ':=',
      choice($.expr, $.axiom),
      ';',
    ),

  }
});