Skip to content

Repository files navigation

tree-sitter-p

A tree-sitter grammar for the P programming language.

The grammar follows the ANTLR grammar used by the P compiler:

Comments in grammar.js reference the corresponding parser rules.

Coverage

The grammar covers:

  • Core declarations: event, eventset, type (user-defined and foreign), enum, fun (named, foreign with creates / return/requires/ensures contracts, and anonymous functions), machine (with receives/sends annotations), spec, scenario, interface, module, implementation, test, param
  • State machines: start/hot/cold states, entry/exit, on ... do, on ... goto ... with, defer, ignore, on null/on halt
  • Statements: blocks, assert, assume, print, foreach (with loop invariants), while, if/else, break/continue/return, assignment, insert (+=), remove (-=), new, calls, raise, send, announce, goto, receive/case, and the empty statement ;
  • Expressions: tuples/named tuples and field access (x.0, x.f), collection indexing, keys/values/sizeof/in, default, choose, format, new, casts (as/to), $, $$, halt, this, decimal floats (1.5, .5) and float(base, exp), and all unary/binary operators with the precedence implied by PParser.g4's alternative order (casts bind between +/- and comparisons)
  • PVerifier extensions: invariant, Lemma/Theorem groups, axiom, init-condition, Proof blocks (prove ... using ... except ...), pure functions, quantifiers (forall/exists ... :: ...), ==>, <==>, is, targets, inflight, sent
  • Module system: primitive modules with bindings (A -> B), union, compose, hidee, hidei, rename ... to ... in, main ... in, assert ... in, safety and refinement (refines) tests, pairwise and (N wise) parameterized tests

Runtime compatibility

The generated parser uses Tree-sitter language ABI 15 and requires a Tree-sitter 0.25 or newer runtime. Editor integrations must provide a compatible runtime independently of the editor or plugin version.

Usage

cd tree-sitter-p
tree-sitter generate    # regenerate src/parser.c after editing grammar.js
tree-sitter test        # run the corpus tests in test/corpus/
tree-sitter parse path/to/File.p

When installed as a Node.js package, the default export is a language object for the tree-sitter package:

import Parser from "tree-sitter";
import P from "tree-sitter-p";

const parser = new Parser();
parser.setLanguage(P);
const tree = parser.parse("event Ping;");

queries/highlights.scm provides syntax highlighting captures for editors that consume Tree-sitter queries.

Emacs integration

The emacs/ directory contains an Emacs IDE layer for P, mirroring the feature set of Peasy (the P VS Code extension) and integrating PeasyAI:

  • p-ts-mode.el — tree-sitter major mode: highlighting, indentation (4 spaces), imenu/which-func, plus toolchain commands:
    • C-c C-c (p-ts-compile) — p compile at the nearest .pproj root, with error/warning jumping via compilation-mode.
    • C-c C-t (p-ts-check) — run a test case chosen with completion from p check --list-tests; prefix arg prompts for schedule count.
  • peasy.el — IDE features on top of p-ts-mode:
    • peasy-visualize-machine (C-c C-v) — render the machine at point as a Graphviz state diagram from the tree-sitter parse (Peasy uses Stately/XState for this; current P has dropped --mode stately).
    • peasy-view-trace (C-c C-r) — browse PChecker *.trace.json error traces as a filterable timeline (Peasy's ShiViz equivalent).
    • peasy-minor-mode — Flymake backend running PeasyAI's 12 static validators (no LLM needed) via peasy-bridge.py.
    • peasy-apply-auto-fixes (C-c C-f) — apply PeasyAI's deterministic auto-fixes to the buffer.
    • peasy-syntax-help (C-c C-h), peasy-search-examples (C-c C-s), peasy-doctor, and LLM-backed project commands (peasy-generate-project, peasy-fix-project, peasy-check-project) via the PeasyAI CLI.
  • emacs/snippets/p-ts-mode/ — yasnippet templates ported from Peasy's snippet collection (machine, spec, state, handlers, statements).
  • emacs/peasy-bridge.py — headless JSON bridge to PeasyAI's validation pipeline and RAG search (stdlib-only, no LLM calls).
(use-package p-ts-mode
  :load-path "path/to/tree-sitter-p/emacs"
  :mode "\\.p\\'")

(use-package peasy
  :load-path "path/to/tree-sitter-p/emacs"
  :custom (peasy-peasyai-directory "~/project/P/Src/PeasyAI")
  :hook (p-ts-mode . peasy-minor-mode))

;; Optional: snippets
(with-eval-after-load 'yasnippet
  (add-to-list 'yas-snippet-dirs "path/to/tree-sitter-p/emacs/snippets"))

About

No description, website, or topics provided.

Resources

Stars

1 star

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages