/**
 * @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 : $ => repeat(choice($.definition, $.preprocess, $.axiom)),

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

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

    param_block : $ => seq(
      '(',
      field('param', repeat1($.identifier)),
      ':',
      field('type', $.expr),
      ')'
    ),

    star   : $ => "*",
    square : $ => choice('□', '[]'),
    sort   : $ => choice($.star, $.square, seq($.square, /[0-9₀₁₂₃₄₅₆₇₈₉]+/)),

    labs : $ => seq(
      choice('λ', 'fun'),
      repeat1($.param_block),
      optional($.ascription),
      choice('=>', '⇒'),
      $.expr,
    ),

    pabs : $ => seq(
      choice('∏', 'forall'),
      repeat1($.param_block),
      optional($.ascription),
      ',',
      $.expr,
    ),

    term : $ => choice(
      $.identifier,
      $.sort,
      seq('(', $.expr, ')'),
    ),

    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,
      choice('->', '→'),
      $.expr,
    )),

    app_term : $ => choice(
      $.labs,
      $.pabs,
      $.let,
      $.app,
    ),

    expr : $ => choice(
      $.app_term,
      $.arrow,
    ),

    ascription : $ => seq(
      ':',
      field('type', $.expr),
    ),

    axiom : $ => seq(
      'axiom',
      field('name', $.identifier),
      repeat($.param_block),
      $.ascription,
      ';'
    ),

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

    preprocess : $ => seq($.command, $.post_command),

    post_command : $ => /.+/,

    command : $ => '@include',

  }
});