commit f0a31d7af9366342dc2997ea92bfa216772f5963 Author: William Ball Date: Wed Nov 20 19:29:09 2024 -0800 working? diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..7756ee9 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,43 @@ +root = true + +[*] +charset = utf-8 + +[*.{json,toml,yml,gyp}] +indent_style = space +indent_size = 2 + +[*.js] +indent_style = space +indent_size = 2 + +[*.scm] +indent_style = space +indent_size = 2 + +[*.{c,cc,h}] +indent_style = space +indent_size = 4 + +[*.rs] +indent_style = space +indent_size = 4 + +[*.{py,pyi}] +indent_style = space +indent_size = 4 + +[*.swift] +indent_style = space +indent_size = 4 + +[*.go] +indent_style = tab +indent_size = 8 + +[Makefile] +indent_style = tab +indent_size = 8 + +[parser.c] +indent_size = 2 diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..9d5c5d4 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,13 @@ +* text=auto eol=lf + +src/*.json linguist-generated +src/parser.c linguist-generated +src/tree_sitter/* linguist-generated + +bindings/** linguist-generated +binding.gyp linguist-generated +setup.py linguist-generated +Makefile linguist-generated +CMakeLists.txt linguist-generated +Package.swift linguist-generated +go.mod linguist-generated diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..308fcab --- /dev/null +++ b/.gitignore @@ -0,0 +1,40 @@ +# Rust artifacts +target/ + +# Node artifacts +build/ +prebuilds/ +node_modules/ + +# Swift artifacts +.build/ + +# Go artifacts +_obj/ + +# Python artifacts +.venv/ +dist/ +*.egg-info +*.whl + +# C artifacts +*.a +*.so +*.so.* +*.dylib +*.dll +*.pc + +# Example dirs +/examples/*/ + +# Grammar volatiles +*.wasm +*.obj +*.o + +# Archives +*.tar.gz +*.tgz +*.zip diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 0000000..02c1915 --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,60 @@ +cmake_minimum_required(VERSION 3.13) + +project(tree-sitter-perga + VERSION "0.1.0" + DESCRIPTION "Basic proof assistant based on Calculus of Constructions" + HOMEPAGE_URL "https://forgejo.ballcloud.cc/wball/perga" + LANGUAGES C) + +option(BUILD_SHARED_LIBS "Build using shared libraries" ON) +option(TREE_SITTER_REUSE_ALLOCATOR "Reuse the library allocator" OFF) + +set(TREE_SITTER_ABI_VERSION 14 CACHE STRING "Tree-sitter ABI version") +if(NOT ${TREE_SITTER_ABI_VERSION} MATCHES "^[0-9]+$") + unset(TREE_SITTER_ABI_VERSION CACHE) + message(FATAL_ERROR "TREE_SITTER_ABI_VERSION must be an integer") +endif() + +find_program(TREE_SITTER_CLI tree-sitter DOC "Tree-sitter CLI") + +add_custom_command(OUTPUT "${CMAKE_CURRENT_SOURCE_DIR}/src/parser.c" + DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/src/grammar.json" + COMMAND "${TREE_SITTER_CLI}" generate src/grammar.json + --abi=${TREE_SITTER_ABI_VERSION} + WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" + COMMENT "Generating parser.c") + +add_library(tree-sitter-perga src/parser.c) +if(EXISTS src/scanner.c) + target_sources(tree-sitter-perga PRIVATE src/scanner.c) +endif() +target_include_directories(tree-sitter-perga PRIVATE src) + +target_compile_definitions(tree-sitter-perga PRIVATE + $<$:TREE_SITTER_REUSE_ALLOCATOR> + $<$:TREE_SITTER_DEBUG>) + +set_target_properties(tree-sitter-perga + PROPERTIES + C_STANDARD 11 + POSITION_INDEPENDENT_CODE ON + SOVERSION "${TREE_SITTER_ABI_VERSION}.${PROJECT_VERSION_MAJOR}" + DEFINE_SYMBOL "") + +configure_file(bindings/c/tree-sitter-perga.pc.in + "${CMAKE_CURRENT_BINARY_DIR}/tree-sitter-perga.pc" @ONLY) + +include(GNUInstallDirs) + +install(FILES bindings/c/tree-sitter-perga.h + DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/tree_sitter") +install(FILES "${CMAKE_CURRENT_BINARY_DIR}/tree-sitter-perga.pc" + DESTINATION "${CMAKE_INSTALL_DATAROOTDIR}/pkgconfig") +install(TARGETS tree-sitter-perga + LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}") + +add_custom_target(test "${TREE_SITTER_CLI}" test + WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" + COMMENT "tree-sitter test") + +# vim:ft=cmake: diff --git a/Cargo.toml b/Cargo.toml new file mode 100644 index 0000000..1e8a5fc --- /dev/null +++ b/Cargo.toml @@ -0,0 +1,27 @@ +[package] +name = "tree-sitter-perga" +description = "Basic proof assistant based on Calculus of Constructions" +version = "0.1.0" +authors = ["William Ball "] +license = "GPL3" +readme = "README.md" +keywords = ["incremental", "parsing", "tree-sitter", "perga"] +categories = ["parsing", "text-editors"] +repository = "https://forgejo.ballcloud.cc/wball/perga" +edition = "2021" +autoexamples = false + +build = "bindings/rust/build.rs" +include = ["bindings/rust/*", "grammar.js", "queries/*", "src/*"] + +[lib] +path = "bindings/rust/lib.rs" + +[dependencies] +tree-sitter-language = "0.1" + +[build-dependencies] +cc = "1.1.22" + +[dev-dependencies] +tree-sitter = "0.24.3" diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..bbc8a99 --- /dev/null +++ b/Makefile @@ -0,0 +1,94 @@ +ifeq ($(OS),Windows_NT) +$(error Windows is not supported) +endif + +LANGUAGE_NAME := tree-sitter-perga +HOMEPAGE_URL := https://forgejo.ballcloud.cc/wball/perga +VERSION := 0.1.0 + +# repository +SRC_DIR := src + +TS ?= tree-sitter + +# install directory layout +PREFIX ?= /usr/local +INCLUDEDIR ?= $(PREFIX)/include +LIBDIR ?= $(PREFIX)/lib +PCLIBDIR ?= $(LIBDIR)/pkgconfig + +# source/object files +PARSER := $(SRC_DIR)/parser.c +EXTRAS := $(filter-out $(PARSER),$(wildcard $(SRC_DIR)/*.c)) +OBJS := $(patsubst %.c,%.o,$(PARSER) $(EXTRAS)) + +# flags +ARFLAGS ?= rcs +override CFLAGS += -I$(SRC_DIR) -std=c11 -fPIC + +# ABI versioning +SONAME_MAJOR = $(shell sed -n 's/\#define LANGUAGE_VERSION //p' $(PARSER)) +SONAME_MINOR = $(word 1,$(subst ., ,$(VERSION))) + +# OS-specific bits +ifeq ($(shell uname),Darwin) + SOEXT = dylib + SOEXTVER_MAJOR = $(SONAME_MAJOR).$(SOEXT) + SOEXTVER = $(SONAME_MAJOR).$(SONAME_MINOR).$(SOEXT) + LINKSHARED = -dynamiclib -Wl,-install_name,$(LIBDIR)/lib$(LANGUAGE_NAME).$(SOEXTVER),-rpath,@executable_path/../Frameworks +else + SOEXT = so + SOEXTVER_MAJOR = $(SOEXT).$(SONAME_MAJOR) + SOEXTVER = $(SOEXT).$(SONAME_MAJOR).$(SONAME_MINOR) + LINKSHARED = -shared -Wl,-soname,lib$(LANGUAGE_NAME).$(SOEXTVER) +endif +ifneq ($(filter $(shell uname),FreeBSD NetBSD DragonFly),) + PCLIBDIR := $(PREFIX)/libdata/pkgconfig +endif + +all: lib$(LANGUAGE_NAME).a lib$(LANGUAGE_NAME).$(SOEXT) $(LANGUAGE_NAME).pc + +lib$(LANGUAGE_NAME).a: $(OBJS) + $(AR) $(ARFLAGS) $@ $^ + +lib$(LANGUAGE_NAME).$(SOEXT): $(OBJS) + $(CC) $(LDFLAGS) $(LINKSHARED) $^ $(LDLIBS) -o $@ +ifneq ($(STRIP),) + $(STRIP) $@ +endif + +$(LANGUAGE_NAME).pc: bindings/c/$(LANGUAGE_NAME).pc.in + sed -e 's|@PROJECT_VERSION@|$(VERSION)|' \ + -e 's|@CMAKE_INSTALL_LIBDIR@|$(LIBDIR:$(PREFIX)/%=%)|' \ + -e 's|@CMAKE_INSTALL_INCLUDEDIR@|$(INCLUDEDIR:$(PREFIX)/%=%)|' \ + -e 's|@PROJECT_DESCRIPTION@|$(DESCRIPTION)|' \ + -e 's|@PROJECT_HOMEPAGE_URL@|$(HOMEPAGE_URL)|' \ + -e 's|@CMAKE_INSTALL_PREFIX@|$(PREFIX)|' $< > $@ + +$(PARSER): $(SRC_DIR)/grammar.json + $(TS) generate $^ + +install: all + install -d '$(DESTDIR)$(INCLUDEDIR)'/tree_sitter '$(DESTDIR)$(PCLIBDIR)' '$(DESTDIR)$(LIBDIR)' + install -m644 bindings/c/$(LANGUAGE_NAME).h '$(DESTDIR)$(INCLUDEDIR)'/tree_sitter/$(LANGUAGE_NAME).h + install -m644 $(LANGUAGE_NAME).pc '$(DESTDIR)$(PCLIBDIR)'/$(LANGUAGE_NAME).pc + install -m644 lib$(LANGUAGE_NAME).a '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).a + install -m755 lib$(LANGUAGE_NAME).$(SOEXT) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER) + ln -sf lib$(LANGUAGE_NAME).$(SOEXTVER) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER_MAJOR) + ln -sf lib$(LANGUAGE_NAME).$(SOEXTVER_MAJOR) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXT) + +uninstall: + $(RM) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).a \ + '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER) \ + '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER_MAJOR) \ + '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXT) \ + '$(DESTDIR)$(INCLUDEDIR)'/tree_sitter/$(LANGUAGE_NAME).h \ + '$(DESTDIR)$(PCLIBDIR)'/$(LANGUAGE_NAME).pc + +clean: + $(RM) $(OBJS) $(LANGUAGE_NAME).pc lib$(LANGUAGE_NAME).a lib$(LANGUAGE_NAME).$(SOEXT) + +test: + $(TS) test + +.PHONY: all install uninstall clean test diff --git a/Package.swift b/Package.swift new file mode 100644 index 0000000..c0d688b --- /dev/null +++ b/Package.swift @@ -0,0 +1,37 @@ +// swift-tools-version:5.3 +import PackageDescription + +let package = Package( + name: "TreeSitterPerga", + products: [ + .library(name: "TreeSitterPerga", targets: ["TreeSitterPerga"]), + ], + dependencies: [ + .package(url: "https://github.com/ChimeHQ/SwiftTreeSitter", from: "0.8.0"), + ], + targets: [ + .target( + name: "TreeSitterPerga", + dependencies: [], + path: ".", + sources: [ + "src/parser.c", + // NOTE: if your language has an external scanner, add it here. + ], + resources: [ + .copy("queries") + ], + publicHeadersPath: "bindings/swift", + cSettings: [.headerSearchPath("src")] + ), + .testTarget( + name: "TreeSitterPergaTests", + dependencies: [ + "SwiftTreeSitter", + "TreeSitterPerga", + ], + path: "bindings/swift/TreeSitterPergaTests" + ) + ], + cLanguageStandard: .c11 +) diff --git a/binding.gyp b/binding.gyp new file mode 100644 index 0000000..41c0cf9 --- /dev/null +++ b/binding.gyp @@ -0,0 +1,30 @@ +{ + "targets": [ + { + "target_name": "tree_sitter_perga_binding", + "dependencies": [ + " + +typedef struct TSLanguage TSLanguage; + +extern "C" TSLanguage *tree_sitter_perga(); + +// "tree-sitter", "language" hashed with BLAKE2 +const napi_type_tag LANGUAGE_TYPE_TAG = { + 0x8AF2E5212AD58ABF, 0xD5006CAD83ABBA16 +}; + +Napi::Object Init(Napi::Env env, Napi::Object exports) { + exports["name"] = Napi::String::New(env, "perga"); + auto language = Napi::External::New(env, tree_sitter_perga()); + language.TypeTag(&LANGUAGE_TYPE_TAG); + exports["language"] = language; + return exports; +} + +NODE_API_MODULE(tree_sitter_perga_binding, Init) diff --git a/bindings/node/binding_test.js b/bindings/node/binding_test.js new file mode 100644 index 0000000..afede30 --- /dev/null +++ b/bindings/node/binding_test.js @@ -0,0 +1,9 @@ +/// + +const assert = require("node:assert"); +const { test } = require("node:test"); + +test("can load grammar", () => { + const parser = new (require("tree-sitter"))(); + assert.doesNotThrow(() => parser.setLanguage(require("."))); +}); diff --git a/bindings/node/index.d.ts b/bindings/node/index.d.ts new file mode 100644 index 0000000..efe259e --- /dev/null +++ b/bindings/node/index.d.ts @@ -0,0 +1,28 @@ +type BaseNode = { + type: string; + named: boolean; +}; + +type ChildNode = { + multiple: boolean; + required: boolean; + types: BaseNode[]; +}; + +type NodeInfo = + | (BaseNode & { + subtypes: BaseNode[]; + }) + | (BaseNode & { + fields: { [name: string]: ChildNode }; + children: ChildNode[]; + }); + +type Language = { + name: string; + language: unknown; + nodeTypeInfo: NodeInfo[]; +}; + +declare const language: Language; +export = language; diff --git a/bindings/node/index.js b/bindings/node/index.js new file mode 100644 index 0000000..6657bcf --- /dev/null +++ b/bindings/node/index.js @@ -0,0 +1,7 @@ +const root = require("path").join(__dirname, "..", ".."); + +module.exports = require("node-gyp-build")(root); + +try { + module.exports.nodeTypeInfo = require("../../src/node-types.json"); +} catch (_) {} diff --git a/bindings/python/tests/test_binding.py b/bindings/python/tests/test_binding.py new file mode 100644 index 0000000..fc95f5c --- /dev/null +++ b/bindings/python/tests/test_binding.py @@ -0,0 +1,11 @@ +from unittest import TestCase + +import tree_sitter, tree_sitter_perga + + +class TestLanguage(TestCase): + def test_can_load_grammar(self): + try: + tree_sitter.Language(tree_sitter_perga.language()) + except Exception: + self.fail("Error loading Perga grammar") diff --git a/bindings/python/tree_sitter_perga/__init__.py b/bindings/python/tree_sitter_perga/__init__.py new file mode 100644 index 0000000..6778215 --- /dev/null +++ b/bindings/python/tree_sitter_perga/__init__.py @@ -0,0 +1,42 @@ +"""Basic proof assistant based on Calculus of Constructions""" + +from importlib.resources import files as _files + +from ._binding import language + + +def _get_query(name, file): + query = _files(f"{__package__}.queries") / file + globals()[name] = query.read_text() + return globals()[name] + + +def __getattr__(name): + # NOTE: uncomment these to include any queries that this grammar contains: + + # if name == "HIGHLIGHTS_QUERY": + # return _get_query("HIGHLIGHTS_QUERY", "highlights.scm") + # if name == "INJECTIONS_QUERY": + # return _get_query("INJECTIONS_QUERY", "injections.scm") + # if name == "LOCALS_QUERY": + # return _get_query("LOCALS_QUERY", "locals.scm") + # if name == "TAGS_QUERY": + # return _get_query("TAGS_QUERY", "tags.scm") + + raise AttributeError(f"module {__name__!r} has no attribute {name!r}") + + +__all__ = [ + "language", + # "HIGHLIGHTS_QUERY", + # "INJECTIONS_QUERY", + # "LOCALS_QUERY", + # "TAGS_QUERY", +] + + +def __dir__(): + return sorted(__all__ + [ + "__all__", "__builtins__", "__cached__", "__doc__", "__file__", + "__loader__", "__name__", "__package__", "__path__", "__spec__", + ]) diff --git a/bindings/python/tree_sitter_perga/__init__.pyi b/bindings/python/tree_sitter_perga/__init__.pyi new file mode 100644 index 0000000..abf6633 --- /dev/null +++ b/bindings/python/tree_sitter_perga/__init__.pyi @@ -0,0 +1,10 @@ +from typing import Final + +# NOTE: uncomment these to include any queries that this grammar contains: + +# HIGHLIGHTS_QUERY: Final[str] +# INJECTIONS_QUERY: Final[str] +# LOCALS_QUERY: Final[str] +# TAGS_QUERY: Final[str] + +def language() -> object: ... diff --git a/bindings/python/tree_sitter_perga/binding.c b/bindings/python/tree_sitter_perga/binding.c new file mode 100644 index 0000000..542ab1c --- /dev/null +++ b/bindings/python/tree_sitter_perga/binding.c @@ -0,0 +1,27 @@ +#include + +typedef struct TSLanguage TSLanguage; + +TSLanguage *tree_sitter_perga(void); + +static PyObject* _binding_language(PyObject *Py_UNUSED(self), PyObject *Py_UNUSED(args)) { + return PyCapsule_New(tree_sitter_perga(), "tree_sitter.Language", NULL); +} + +static PyMethodDef methods[] = { + {"language", _binding_language, METH_NOARGS, + "Get the tree-sitter language for this grammar."}, + {NULL, NULL, 0, NULL} +}; + +static struct PyModuleDef module = { + .m_base = PyModuleDef_HEAD_INIT, + .m_name = "_binding", + .m_doc = NULL, + .m_size = -1, + .m_methods = methods +}; + +PyMODINIT_FUNC PyInit__binding(void) { + return PyModule_Create(&module); +} diff --git a/bindings/python/tree_sitter_perga/py.typed b/bindings/python/tree_sitter_perga/py.typed new file mode 100644 index 0000000..e69de29 diff --git a/bindings/rust/build.rs b/bindings/rust/build.rs new file mode 100644 index 0000000..79c26a9 --- /dev/null +++ b/bindings/rust/build.rs @@ -0,0 +1,22 @@ +fn main() { + let src_dir = std::path::Path::new("src"); + + let mut c_config = cc::Build::new(); + c_config.std("c11").include(src_dir); + + #[cfg(target_env = "msvc")] + c_config.flag("-utf-8"); + + let parser_path = src_dir.join("parser.c"); + c_config.file(&parser_path); + println!("cargo:rerun-if-changed={}", parser_path.to_str().unwrap()); + + // NOTE: if your language uses an external scanner, uncomment this block: + /* + let scanner_path = src_dir.join("scanner.c"); + c_config.file(&scanner_path); + println!("cargo:rerun-if-changed={}", scanner_path.to_str().unwrap()); + */ + + c_config.compile("tree-sitter-perga"); +} diff --git a/bindings/rust/lib.rs b/bindings/rust/lib.rs new file mode 100644 index 0000000..8690e34 --- /dev/null +++ b/bindings/rust/lib.rs @@ -0,0 +1,53 @@ +//! This crate provides Perga language support for the [tree-sitter][] parsing library. +//! +//! Typically, you will use the [LANGUAGE][] constant to add this language to a +//! tree-sitter [Parser][], and then use the parser to parse some code: +//! +//! ``` +//! let code = r#" +//! "#; +//! let mut parser = tree_sitter::Parser::new(); +//! let language = tree_sitter_perga::LANGUAGE; +//! parser +//! .set_language(&language.into()) +//! .expect("Error loading Perga parser"); +//! let tree = parser.parse(code, None).unwrap(); +//! assert!(!tree.root_node().has_error()); +//! ``` +//! +//! [Parser]: https://docs.rs/tree-sitter/*/tree_sitter/struct.Parser.html +//! [tree-sitter]: https://tree-sitter.github.io/ + +use tree_sitter_language::LanguageFn; + +extern "C" { + fn tree_sitter_perga() -> *const (); +} + +/// The tree-sitter [`LanguageFn`][LanguageFn] for this grammar. +/// +/// [LanguageFn]: https://docs.rs/tree-sitter-language/*/tree_sitter_language/struct.LanguageFn.html +pub const LANGUAGE: LanguageFn = unsafe { LanguageFn::from_raw(tree_sitter_perga) }; + +/// The content of the [`node-types.json`][] file for this grammar. +/// +/// [`node-types.json`]: https://tree-sitter.github.io/tree-sitter/using-parsers#static-node-types +pub const NODE_TYPES: &str = include_str!("../../src/node-types.json"); + +// NOTE: uncomment these to include any queries that this grammar contains: + +// pub const HIGHLIGHTS_QUERY: &str = include_str!("../../queries/highlights.scm"); +// pub const INJECTIONS_QUERY: &str = include_str!("../../queries/injections.scm"); +// pub const LOCALS_QUERY: &str = include_str!("../../queries/locals.scm"); +// pub const TAGS_QUERY: &str = include_str!("../../queries/tags.scm"); + +#[cfg(test)] +mod tests { + #[test] + fn test_can_load_grammar() { + let mut parser = tree_sitter::Parser::new(); + parser + .set_language(&super::LANGUAGE.into()) + .expect("Error loading Perga parser"); + } +} diff --git a/bindings/swift/TreeSitterPerga/perga.h b/bindings/swift/TreeSitterPerga/perga.h new file mode 100644 index 0000000..2a43f30 --- /dev/null +++ b/bindings/swift/TreeSitterPerga/perga.h @@ -0,0 +1,16 @@ +#ifndef TREE_SITTER_PERGA_H_ +#define TREE_SITTER_PERGA_H_ + +typedef struct TSLanguage TSLanguage; + +#ifdef __cplusplus +extern "C" { +#endif + +const TSLanguage *tree_sitter_perga(void); + +#ifdef __cplusplus +} +#endif + +#endif // TREE_SITTER_PERGA_H_ diff --git a/bindings/swift/TreeSitterPergaTests/TreeSitterPergaTests.swift b/bindings/swift/TreeSitterPergaTests/TreeSitterPergaTests.swift new file mode 100644 index 0000000..fda393a --- /dev/null +++ b/bindings/swift/TreeSitterPergaTests/TreeSitterPergaTests.swift @@ -0,0 +1,12 @@ +import XCTest +import SwiftTreeSitter +import TreeSitterPerga + +final class TreeSitterPergaTests: XCTestCase { + func testCanLoadGrammar() throws { + let parser = Parser() + let language = Language(language: tree_sitter_perga()) + XCTAssertNoThrow(try parser.setLanguage(language), + "Error loading Perga grammar") + } +} diff --git a/ftdetect/perga.vim b/ftdetect/perga.vim new file mode 100644 index 0000000..8e7e342 --- /dev/null +++ b/ftdetect/perga.vim @@ -0,0 +1 @@ +autocmd VimEnter,BufWinEnter,BufRead,BufNewFile *.pg setlocal filetype=perga diff --git a/go.mod b/go.mod new file mode 100644 index 0000000..9e3a2b5 --- /dev/null +++ b/go.mod @@ -0,0 +1,5 @@ +module forgejo.ballcloud.cc/wball/perga + +go 1.22 + +require github.com/tree-sitter/go-tree-sitter v0.23.1 diff --git a/grammar.js b/grammar.js new file mode 100644 index 0000000..00fc15d --- /dev/null +++ b/grammar.js @@ -0,0 +1,98 @@ +/** + * @file Basic proof assistant based on Calculus of Constructions + * @author William Ball + * @license GPL3 + */ + +/// +// @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), + ';', + ), + + } +}); diff --git a/lua/tree-sitter-perga/init.lua b/lua/tree-sitter-perga/init.lua new file mode 100644 index 0000000..081d84e --- /dev/null +++ b/lua/tree-sitter-perga/init.lua @@ -0,0 +1,49 @@ +local M = {} + +local is_windows +if jit ~= nil then + is_windows = jit.os == "Windows" +else + is_windows = package.config:sub(1, 1) == "\\" +end + +local join_paths = function(...) + local separator + if is_windows then + separator = "\\" + else + separator = "/" + end + return table.concat({ ... }, separator) +end + +function M.setup(arg) + local parser_config = require('nvim-treesitter.parsers').get_parser_configs() + parser_config.curse = { + install_info = { + url = arg['local'] and join_paths( + vim.fn.stdpath('data'), + 'site', + 'pack', + 'packer', + 'start', + 'tree-sitter-curse' + ) or 'https://forgejo.ballcloud.cc/wball/tree-sitter-perga', + files = { 'src/parser.c' }, + branch = 'main', + }, + maintainers = { '@wball' } + } + local ok, ft = pcall(require, 'filetype') + if ok then + ft.setup({ + overrides = { + extensions = { + curse = 'perga', + }, + }, + }) + end +end + +return M diff --git a/package.json b/package.json new file mode 100644 index 0000000..458a133 --- /dev/null +++ b/package.json @@ -0,0 +1,56 @@ +{ + "name": "tree-sitter-perga", + "version": "0.1.0", + "description": "Basic proof assistant based on Calculus of Constructions", + "repository": "github:tree-sitter/tree-sitter-perga", + "license": "GPL3", + "author": { + "name": "William Ball", + "email": "williampi103@gmail.com" + }, + "main": "bindings/node", + "types": "bindings/node", + "keywords": [ + "incremental", + "parsing", + "tree-sitter", + "perga" + ], + "files": [ + "grammar.js", + "binding.gyp", + "prebuilds/**", + "bindings/node/*", + "queries/*", + "src/**", + "*.wasm" + ], + "dependencies": { + "node-addon-api": "^8.1.0", + "node-gyp-build": "^4.8.2" + }, + "devDependencies": { + "prebuildify": "^6.0.1", + "tree-sitter-cli": "^0.24.3" + }, + "peerDependencies": { + "tree-sitter": "^0.21.1" + }, + "peerDependenciesMeta": { + "tree-sitter": { + "optional": true + } + }, + "scripts": { + "install": "node-gyp-build", + "prestart": "tree-sitter build --wasm", + "start": "tree-sitter playground", + "test": "node --test bindings/node/*_test.js" + }, + "tree-sitter": [ + { + "scope": "source.perga", + "injection-regex": "^perga$" + } + ] +} diff --git a/pyproject.toml b/pyproject.toml new file mode 100644 index 0000000..3f94623 --- /dev/null +++ b/pyproject.toml @@ -0,0 +1,30 @@ +[build-system] +requires = ["setuptools>=42", "wheel"] +build-backend = "setuptools.build_meta" + +[project] +name = "tree-sitter-perga" +description = "Basic proof assistant based on Calculus of Constructions" +version = "0.1.0" +keywords = ["incremental", "parsing", "tree-sitter", "perga"] +classifiers = [ + "Intended Audience :: Developers", + "License :: OSI Approved :: MIT License", + "Topic :: Software Development :: Compilers", + "Topic :: Text Processing :: Linguistic", + "Typing :: Typed", +] +authors = [{ name = "William Ball", email = "williampi103@gmail.com" }] +requires-python = ">=3.9" +license.text = "GPL3" +readme = "README.md" + +[project.urls] +Homepage = "https://forgejo.ballcloud.cc/wball/perga" + +[project.optional-dependencies] +core = ["tree-sitter~=0.22"] + +[tool.cibuildwheel] +build = "cp39-*" +build-frontend = "build" diff --git a/queries/highlights.scm b/queries/highlights.scm new file mode 100644 index 0000000..a44408c --- /dev/null +++ b/queries/highlights.scm @@ -0,0 +1,8 @@ +[ "fun" "λ" "forall" "∏" ] @keyword +[ "->" "=>" "→" "⇒" "," ":=" ";" ":" ] @punctuation.delimiter +[ "(" ")" ] @punctuation.bracket +;[ "*" "□" "[]" ] @constant.builtin +(comment) @comment +(identifier) @variable +;(param) @variable.parameter +;(type) @type diff --git a/setup.py b/setup.py new file mode 100644 index 0000000..83a680f --- /dev/null +++ b/setup.py @@ -0,0 +1,62 @@ +from os.path import isdir, join +from platform import system + +from setuptools import Extension, find_packages, setup +from setuptools.command.build import build +from wheel.bdist_wheel import bdist_wheel + + +class Build(build): + def run(self): + if isdir("queries"): + dest = join(self.build_lib, "tree_sitter_perga", "queries") + self.copy_tree("queries", dest) + super().run() + + +class BdistWheel(bdist_wheel): + def get_tag(self): + python, abi, platform = super().get_tag() + if python.startswith("cp"): + python, abi = "cp39", "abi3" + return python, abi, platform + + +setup( + packages=find_packages("bindings/python"), + package_dir={"": "bindings/python"}, + package_data={ + "tree_sitter_perga": ["*.pyi", "py.typed"], + "tree_sitter_perga.queries": ["*.scm"], + }, + ext_package="tree_sitter_perga", + ext_modules=[ + Extension( + name="_binding", + sources=[ + "bindings/python/tree_sitter_perga/binding.c", + "src/parser.c", + # NOTE: if your language uses an external scanner, add it here. + ], + extra_compile_args=[ + "-std=c11", + "-fvisibility=hidden", + ] if system() != "Windows" else [ + "/std:c11", + "/utf-8", + ], + define_macros=[ + ("Py_LIMITED_API", "0x03090000"), + ("PY_SSIZE_T_CLEAN", None), + ("TREE_SITTER_HIDE_SYMBOLS", None), + ], + include_dirs=["src"], + py_limited_api=True, + ) + ], + cmdclass={ + "build": Build, + "bdist_wheel": BdistWheel + }, + zip_safe=False +) diff --git a/src/grammar.json b/src/grammar.json new file mode 100644 index 0000000..1eef610 --- /dev/null +++ b/src/grammar.json @@ -0,0 +1,348 @@ +{ + "$schema": "https://tree-sitter.github.io/tree-sitter/assets/schemas/grammar.schema.json", + "name": "perga", + "rules": { + "program": { + "type": "REPEAT", + "content": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "definition" + }, + { + "type": "SYMBOL", + "name": "comment" + } + ] + } + }, + "identifier": { + "type": "PATTERN", + "value": "[a-zA-Z_]\\w*" + }, + "comment": { + "type": "TOKEN", + "content": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "--" + }, + { + "type": "PATTERN", + "value": ".*" + } + ] + } + }, + "param_block": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "identifier" + } + }, + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + }, + "star": { + "type": "STRING", + "value": "*" + }, + "square": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "□" + }, + { + "type": "STRING", + "value": "[]" + } + ] + }, + "lambda": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "λ" + }, + { + "type": "STRING", + "value": "fun" + } + ] + }, + "pi": { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "∏" + }, + { + "type": "STRING", + "value": "forall" + } + ] + }, + "labs": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "lambda" + }, + { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "param_block" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "=>" + }, + { + "type": "STRING", + "value": "⇒" + } + ] + }, + { + "type": "SYMBOL", + "name": "expr" + } + ] + }, + "pabs": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "pi" + }, + { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "param_block" + } + }, + { + "type": "STRING", + "value": "," + }, + { + "type": "SYMBOL", + "name": "expr" + } + ] + }, + "term": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "SYMBOL", + "name": "star" + }, + { + "type": "SYMBOL", + "name": "square" + }, + { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": "(" + }, + { + "type": "SYMBOL", + "name": "expr" + }, + { + "type": "STRING", + "value": ")" + } + ] + } + ] + }, + "app": { + "type": "REPEAT1", + "content": { + "type": "SYMBOL", + "name": "term" + } + }, + "axiom": { + "type": "STRING", + "value": "axiom" + }, + "arrow": { + "type": "PREC_LEFT", + "value": 1, + "content": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "app_term" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "STRING", + "value": "->" + }, + { + "type": "STRING", + "value": "→" + } + ] + }, + { + "type": "SYMBOL", + "name": "expr" + } + ] + } + }, + "app_term": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "labs" + }, + { + "type": "SYMBOL", + "name": "pabs" + }, + { + "type": "SYMBOL", + "name": "app" + } + ] + }, + "expr": { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "app_term" + }, + { + "type": "SYMBOL", + "name": "arrow" + } + ] + }, + "ascription": { + "type": "SEQ", + "members": [ + { + "type": "STRING", + "value": ":" + }, + { + "type": "SYMBOL", + "name": "expr" + } + ] + }, + "definition": { + "type": "SEQ", + "members": [ + { + "type": "SYMBOL", + "name": "identifier" + }, + { + "type": "REPEAT", + "content": { + "type": "SYMBOL", + "name": "param_block" + } + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "ascription" + }, + { + "type": "BLANK" + } + ] + }, + { + "type": "STRING", + "value": ":=" + }, + { + "type": "CHOICE", + "members": [ + { + "type": "SYMBOL", + "name": "expr" + }, + { + "type": "SYMBOL", + "name": "axiom" + } + ] + }, + { + "type": "STRING", + "value": ";" + } + ] + } + }, + "extras": [ + { + "type": "PATTERN", + "value": "\\s" + } + ], + "conflicts": [], + "precedences": [], + "externals": [], + "inline": [], + "supertypes": [] +} diff --git a/src/node-types.json b/src/node-types.json new file mode 100644 index 0000000..2fd46e0 --- /dev/null +++ b/src/node-types.json @@ -0,0 +1,331 @@ +[ + { + "type": "app", + "named": true, + "fields": {}, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "term", + "named": true + } + ] + } + }, + { + "type": "app_term", + "named": true, + "fields": {}, + "children": { + "multiple": false, + "required": true, + "types": [ + { + "type": "app", + "named": true + }, + { + "type": "labs", + "named": true + }, + { + "type": "pabs", + "named": true + } + ] + } + }, + { + "type": "arrow", + "named": true, + "fields": {}, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "app_term", + "named": true + }, + { + "type": "expr", + "named": true + } + ] + } + }, + { + "type": "ascription", + "named": true, + "fields": {}, + "children": { + "multiple": false, + "required": true, + "types": [ + { + "type": "expr", + "named": true + } + ] + } + }, + { + "type": "definition", + "named": true, + "fields": {}, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "ascription", + "named": true + }, + { + "type": "axiom", + "named": true + }, + { + "type": "expr", + "named": true + }, + { + "type": "identifier", + "named": true + }, + { + "type": "param_block", + "named": true + } + ] + } + }, + { + "type": "expr", + "named": true, + "fields": {}, + "children": { + "multiple": false, + "required": true, + "types": [ + { + "type": "app_term", + "named": true + }, + { + "type": "arrow", + "named": true + } + ] + } + }, + { + "type": "labs", + "named": true, + "fields": {}, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "expr", + "named": true + }, + { + "type": "lambda", + "named": true + }, + { + "type": "param_block", + "named": true + } + ] + } + }, + { + "type": "lambda", + "named": true, + "fields": {} + }, + { + "type": "pabs", + "named": true, + "fields": {}, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "expr", + "named": true + }, + { + "type": "param_block", + "named": true + }, + { + "type": "pi", + "named": true + } + ] + } + }, + { + "type": "param_block", + "named": true, + "fields": {}, + "children": { + "multiple": true, + "required": true, + "types": [ + { + "type": "expr", + "named": true + }, + { + "type": "identifier", + "named": true + } + ] + } + }, + { + "type": "pi", + "named": true, + "fields": {} + }, + { + "type": "program", + "named": true, + "root": true, + "fields": {}, + "children": { + "multiple": true, + "required": false, + "types": [ + { + "type": "comment", + "named": true + }, + { + "type": "definition", + "named": true + } + ] + } + }, + { + "type": "square", + "named": true, + "fields": {} + }, + { + "type": "term", + "named": true, + "fields": {}, + "children": { + "multiple": false, + "required": true, + "types": [ + { + "type": "expr", + "named": true + }, + { + "type": "identifier", + "named": true + }, + { + "type": "square", + "named": true + }, + { + "type": "star", + "named": true + } + ] + } + }, + { + "type": "(", + "named": false + }, + { + "type": ")", + "named": false + }, + { + "type": ",", + "named": false + }, + { + "type": "->", + "named": false + }, + { + "type": ":", + "named": false + }, + { + "type": ":=", + "named": false + }, + { + "type": ";", + "named": false + }, + { + "type": "=>", + "named": false + }, + { + "type": "[]", + "named": false + }, + { + "type": "axiom", + "named": true + }, + { + "type": "comment", + "named": true + }, + { + "type": "forall", + "named": false + }, + { + "type": "fun", + "named": false + }, + { + "type": "identifier", + "named": true + }, + { + "type": "star", + "named": true + }, + { + "type": "λ", + "named": false + }, + { + "type": "→", + "named": false + }, + { + "type": "⇒", + "named": false + }, + { + "type": "∏", + "named": false + }, + { + "type": "□", + "named": false + } +] \ No newline at end of file diff --git a/src/parser.c b/src/parser.c new file mode 100644 index 0000000..6cbff8a --- /dev/null +++ b/src/parser.c @@ -0,0 +1,1370 @@ +#include "tree_sitter/parser.h" + +#if defined(__GNUC__) || defined(__clang__) +#pragma GCC diagnostic ignored "-Wmissing-field-initializers" +#endif + +#define LANGUAGE_VERSION 14 +#define STATE_COUNT 52 +#define LARGE_STATE_COUNT 12 +#define SYMBOL_COUNT 39 +#define ALIAS_COUNT 0 +#define TOKEN_COUNT 21 +#define EXTERNAL_TOKEN_COUNT 0 +#define FIELD_COUNT 0 +#define MAX_ALIAS_SEQUENCE_LENGTH 6 +#define PRODUCTION_ID_COUNT 1 + +enum ts_symbol_identifiers { + sym_identifier = 1, + sym_comment = 2, + anon_sym_LPAREN = 3, + anon_sym_COLON = 4, + anon_sym_RPAREN = 5, + sym_star = 6, + anon_sym_u25a1 = 7, + anon_sym_LBRACK_RBRACK = 8, + anon_sym_u03bb = 9, + anon_sym_fun = 10, + anon_sym_u220f = 11, + anon_sym_forall = 12, + anon_sym_EQ_GT = 13, + anon_sym_u21d2 = 14, + anon_sym_COMMA = 15, + sym_axiom = 16, + anon_sym_DASH_GT = 17, + anon_sym_u2192 = 18, + anon_sym_COLON_EQ = 19, + anon_sym_SEMI = 20, + sym_program = 21, + sym_param_block = 22, + sym_square = 23, + sym_lambda = 24, + sym_pi = 25, + sym_labs = 26, + sym_pabs = 27, + sym_term = 28, + sym_app = 29, + sym_arrow = 30, + sym_app_term = 31, + sym_expr = 32, + sym_ascription = 33, + sym_definition = 34, + aux_sym_program_repeat1 = 35, + aux_sym_param_block_repeat1 = 36, + aux_sym_labs_repeat1 = 37, + aux_sym_app_repeat1 = 38, +}; + +static const char * const ts_symbol_names[] = { + [ts_builtin_sym_end] = "end", + [sym_identifier] = "identifier", + [sym_comment] = "comment", + [anon_sym_LPAREN] = "(", + [anon_sym_COLON] = ":", + [anon_sym_RPAREN] = ")", + [sym_star] = "star", + [anon_sym_u25a1] = "\u25a1", + [anon_sym_LBRACK_RBRACK] = "[]", + [anon_sym_u03bb] = "\u03bb", + [anon_sym_fun] = "fun", + [anon_sym_u220f] = "\u220f", + [anon_sym_forall] = "forall", + [anon_sym_EQ_GT] = "=>", + [anon_sym_u21d2] = "\u21d2", + [anon_sym_COMMA] = ",", + [sym_axiom] = "axiom", + [anon_sym_DASH_GT] = "->", + [anon_sym_u2192] = "\u2192", + [anon_sym_COLON_EQ] = ":=", + [anon_sym_SEMI] = ";", + [sym_program] = "program", + [sym_param_block] = "param_block", + [sym_square] = "square", + [sym_lambda] = "lambda", + [sym_pi] = "pi", + [sym_labs] = "labs", + [sym_pabs] = "pabs", + [sym_term] = "term", + [sym_app] = "app", + [sym_arrow] = "arrow", + [sym_app_term] = "app_term", + [sym_expr] = "expr", + [sym_ascription] = "ascription", + [sym_definition] = "definition", + [aux_sym_program_repeat1] = "program_repeat1", + [aux_sym_param_block_repeat1] = "param_block_repeat1", + [aux_sym_labs_repeat1] = "labs_repeat1", + [aux_sym_app_repeat1] = "app_repeat1", +}; + +static const TSSymbol ts_symbol_map[] = { + [ts_builtin_sym_end] = ts_builtin_sym_end, + [sym_identifier] = sym_identifier, + [sym_comment] = sym_comment, + [anon_sym_LPAREN] = anon_sym_LPAREN, + [anon_sym_COLON] = anon_sym_COLON, + [anon_sym_RPAREN] = anon_sym_RPAREN, + [sym_star] = sym_star, + [anon_sym_u25a1] = anon_sym_u25a1, + [anon_sym_LBRACK_RBRACK] = anon_sym_LBRACK_RBRACK, + [anon_sym_u03bb] = anon_sym_u03bb, + [anon_sym_fun] = anon_sym_fun, + [anon_sym_u220f] = anon_sym_u220f, + [anon_sym_forall] = anon_sym_forall, + [anon_sym_EQ_GT] = anon_sym_EQ_GT, + [anon_sym_u21d2] = anon_sym_u21d2, + [anon_sym_COMMA] = anon_sym_COMMA, + [sym_axiom] = sym_axiom, + [anon_sym_DASH_GT] = anon_sym_DASH_GT, + [anon_sym_u2192] = anon_sym_u2192, + [anon_sym_COLON_EQ] = anon_sym_COLON_EQ, + [anon_sym_SEMI] = anon_sym_SEMI, + [sym_program] = sym_program, + [sym_param_block] = sym_param_block, + [sym_square] = sym_square, + [sym_lambda] = sym_lambda, + [sym_pi] = sym_pi, + [sym_labs] = sym_labs, + [sym_pabs] = sym_pabs, + [sym_term] = sym_term, + [sym_app] = sym_app, + [sym_arrow] = sym_arrow, + [sym_app_term] = sym_app_term, + [sym_expr] = sym_expr, + [sym_ascription] = sym_ascription, + [sym_definition] = sym_definition, + [aux_sym_program_repeat1] = aux_sym_program_repeat1, + [aux_sym_param_block_repeat1] = aux_sym_param_block_repeat1, + [aux_sym_labs_repeat1] = aux_sym_labs_repeat1, + [aux_sym_app_repeat1] = aux_sym_app_repeat1, +}; + +static const TSSymbolMetadata ts_symbol_metadata[] = { + [ts_builtin_sym_end] = { + .visible = false, + .named = true, + }, + [sym_identifier] = { + .visible = true, + .named = true, + }, + [sym_comment] = { + .visible = true, + .named = true, + }, + [anon_sym_LPAREN] = { + .visible = true, + .named = false, + }, + [anon_sym_COLON] = { + .visible = true, + .named = false, + }, + [anon_sym_RPAREN] = { + .visible = true, + .named = false, + }, + [sym_star] = { + .visible = true, + .named = true, + }, + [anon_sym_u25a1] = { + .visible = true, + .named = false, + }, + [anon_sym_LBRACK_RBRACK] = { + .visible = true, + .named = false, + }, + [anon_sym_u03bb] = { + .visible = true, + .named = false, + }, + [anon_sym_fun] = { + .visible = true, + .named = false, + }, + [anon_sym_u220f] = { + .visible = true, + .named = false, + }, + [anon_sym_forall] = { + .visible = true, + .named = false, + }, + [anon_sym_EQ_GT] = { + .visible = true, + .named = false, + }, + [anon_sym_u21d2] = { + .visible = true, + .named = false, + }, + [anon_sym_COMMA] = { + .visible = true, + .named = false, + }, + [sym_axiom] = { + .visible = true, + .named = true, + }, + [anon_sym_DASH_GT] = { + .visible = true, + .named = false, + }, + [anon_sym_u2192] = { + .visible = true, + .named = false, + }, + [anon_sym_COLON_EQ] = { + .visible = true, + .named = false, + }, + [anon_sym_SEMI] = { + .visible = true, + .named = false, + }, + [sym_program] = { + .visible = true, + .named = true, + }, + [sym_param_block] = { + .visible = true, + .named = true, + }, + [sym_square] = { + .visible = true, + .named = true, + }, + [sym_lambda] = { + .visible = true, + .named = true, + }, + [sym_pi] = { + .visible = true, + .named = true, + }, + [sym_labs] = { + .visible = true, + .named = true, + }, + [sym_pabs] = { + .visible = true, + .named = true, + }, + [sym_term] = { + .visible = true, + .named = true, + }, + [sym_app] = { + .visible = true, + .named = true, + }, + [sym_arrow] = { + .visible = true, + .named = true, + }, + [sym_app_term] = { + .visible = true, + .named = true, + }, + [sym_expr] = { + .visible = true, + .named = true, + }, + [sym_ascription] = { + .visible = true, + .named = true, + }, + [sym_definition] = { + .visible = true, + .named = true, + }, + [aux_sym_program_repeat1] = { + .visible = false, + .named = false, + }, + [aux_sym_param_block_repeat1] = { + .visible = false, + .named = false, + }, + [aux_sym_labs_repeat1] = { + .visible = false, + .named = false, + }, + [aux_sym_app_repeat1] = { + .visible = false, + .named = false, + }, +}; + +static const TSSymbol ts_alias_sequences[PRODUCTION_ID_COUNT][MAX_ALIAS_SEQUENCE_LENGTH] = { + [0] = {0}, +}; + +static const uint16_t ts_non_terminal_alias_map[] = { + 0, +}; + +static const TSStateId ts_primary_state_ids[STATE_COUNT] = { + [0] = 0, + [1] = 1, + [2] = 2, + [3] = 3, + [4] = 4, + [5] = 5, + [6] = 6, + [7] = 7, + [8] = 8, + [9] = 9, + [10] = 10, + [11] = 11, + [12] = 12, + [13] = 13, + [14] = 14, + [15] = 15, + [16] = 16, + [17] = 17, + [18] = 18, + [19] = 19, + [20] = 20, + [21] = 21, + [22] = 22, + [23] = 23, + [24] = 24, + [25] = 25, + [26] = 26, + [27] = 27, + [28] = 28, + [29] = 29, + [30] = 30, + [31] = 31, + [32] = 32, + [33] = 33, + [34] = 34, + [35] = 35, + [36] = 36, + [37] = 37, + [38] = 38, + [39] = 39, + [40] = 40, + [41] = 41, + [42] = 42, + [43] = 43, + [44] = 44, + [45] = 45, + [46] = 46, + [47] = 47, + [48] = 48, + [49] = 49, + [50] = 50, + [51] = 51, +}; + +static bool ts_lex(TSLexer *lexer, TSStateId state) { + START_LEXER(); + eof = lexer->eof(lexer); + switch (state) { + case 0: + if (eof) ADVANCE(6); + ADVANCE_MAP( + '(', 19, + ')', 21, + '*', 22, + ',', 31, + '-', 2, + ':', 20, + ';', 36, + '=', 3, + '[', 4, + 'a', 16, + 'f', 13, + 0x3bb, 25, + 0x2192, 34, + 0x21d2, 30, + 0x220f, 27, + 0x25a1, 23, + ); + if (('\t' <= lookahead && lookahead <= '\r') || + lookahead == ' ') SKIP(0); + if (('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('b' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 1: + if (lookahead == '(') ADVANCE(19); + if (lookahead == '*') ADVANCE(22); + if (lookahead == '[') ADVANCE(4); + if (lookahead == 'f') ADVANCE(13); + if (lookahead == 0x3bb) ADVANCE(25); + if (lookahead == 0x220f) ADVANCE(27); + if (lookahead == 0x25a1) ADVANCE(23); + if (('\t' <= lookahead && lookahead <= '\r') || + lookahead == ' ') SKIP(1); + if (('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 2: + if (lookahead == '-') ADVANCE(18); + if (lookahead == '>') ADVANCE(33); + END_STATE(); + case 3: + if (lookahead == '>') ADVANCE(29); + END_STATE(); + case 4: + if (lookahead == ']') ADVANCE(24); + END_STATE(); + case 5: + if (eof) ADVANCE(6); + ADVANCE_MAP( + '(', 19, + ')', 21, + '*', 22, + '-', 2, + ':', 20, + ';', 36, + '[', 4, + 0x2192, 34, + 0x25a1, 23, + ); + if (('\t' <= lookahead && lookahead <= '\r') || + lookahead == ' ') SKIP(5); + if (('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 6: + ACCEPT_TOKEN(ts_builtin_sym_end); + END_STATE(); + case 7: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'a') ADVANCE(10); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('b' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 8: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'i') ADVANCE(14); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 9: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'l') ADVANCE(28); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 10: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'l') ADVANCE(9); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 11: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'm') ADVANCE(32); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 12: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'n') ADVANCE(26); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 13: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'o') ADVANCE(15); + if (lookahead == 'u') ADVANCE(12); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 14: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'o') ADVANCE(11); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 15: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'r') ADVANCE(7); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 16: + ACCEPT_TOKEN(sym_identifier); + if (lookahead == 'x') ADVANCE(8); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 17: + ACCEPT_TOKEN(sym_identifier); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 18: + ACCEPT_TOKEN(sym_comment); + if (lookahead != 0 && + lookahead != '\n') ADVANCE(18); + END_STATE(); + case 19: + ACCEPT_TOKEN(anon_sym_LPAREN); + END_STATE(); + case 20: + ACCEPT_TOKEN(anon_sym_COLON); + if (lookahead == '=') ADVANCE(35); + END_STATE(); + case 21: + ACCEPT_TOKEN(anon_sym_RPAREN); + END_STATE(); + case 22: + ACCEPT_TOKEN(sym_star); + END_STATE(); + case 23: + ACCEPT_TOKEN(anon_sym_u25a1); + END_STATE(); + case 24: + ACCEPT_TOKEN(anon_sym_LBRACK_RBRACK); + END_STATE(); + case 25: + ACCEPT_TOKEN(anon_sym_u03bb); + END_STATE(); + case 26: + ACCEPT_TOKEN(anon_sym_fun); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 27: + ACCEPT_TOKEN(anon_sym_u220f); + END_STATE(); + case 28: + ACCEPT_TOKEN(anon_sym_forall); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 29: + ACCEPT_TOKEN(anon_sym_EQ_GT); + END_STATE(); + case 30: + ACCEPT_TOKEN(anon_sym_u21d2); + END_STATE(); + case 31: + ACCEPT_TOKEN(anon_sym_COMMA); + END_STATE(); + case 32: + ACCEPT_TOKEN(sym_axiom); + if (('0' <= lookahead && lookahead <= '9') || + ('A' <= lookahead && lookahead <= 'Z') || + lookahead == '_' || + ('a' <= lookahead && lookahead <= 'z')) ADVANCE(17); + END_STATE(); + case 33: + ACCEPT_TOKEN(anon_sym_DASH_GT); + END_STATE(); + case 34: + ACCEPT_TOKEN(anon_sym_u2192); + END_STATE(); + case 35: + ACCEPT_TOKEN(anon_sym_COLON_EQ); + END_STATE(); + case 36: + ACCEPT_TOKEN(anon_sym_SEMI); + END_STATE(); + default: + return false; + } +} + +static const TSLexMode ts_lex_modes[STATE_COUNT] = { + [0] = {.lex_state = 0}, + [1] = {.lex_state = 5}, + [2] = {.lex_state = 0}, + [3] = {.lex_state = 0}, + [4] = {.lex_state = 0}, + [5] = {.lex_state = 1}, + [6] = {.lex_state = 1}, + [7] = {.lex_state = 1}, + [8] = {.lex_state = 1}, + [9] = {.lex_state = 1}, + [10] = {.lex_state = 1}, + [11] = {.lex_state = 1}, + [12] = {.lex_state = 5}, + [13] = {.lex_state = 5}, + [14] = {.lex_state = 5}, + [15] = {.lex_state = 5}, + [16] = {.lex_state = 5}, + [17] = {.lex_state = 0}, + [18] = {.lex_state = 0}, + [19] = {.lex_state = 0}, + [20] = {.lex_state = 0}, + [21] = {.lex_state = 0}, + [22] = {.lex_state = 0}, + [23] = {.lex_state = 0}, + [24] = {.lex_state = 0}, + [25] = {.lex_state = 0}, + [26] = {.lex_state = 5}, + [27] = {.lex_state = 5}, + [28] = {.lex_state = 0}, + [29] = {.lex_state = 0}, + [30] = {.lex_state = 0}, + [31] = {.lex_state = 0}, + [32] = {.lex_state = 0}, + [33] = {.lex_state = 5}, + [34] = {.lex_state = 0}, + [35] = {.lex_state = 5}, + [36] = {.lex_state = 5}, + [37] = {.lex_state = 5}, + [38] = {.lex_state = 5}, + [39] = {.lex_state = 5}, + [40] = {.lex_state = 0}, + [41] = {.lex_state = 0}, + [42] = {.lex_state = 0}, + [43] = {.lex_state = 0}, + [44] = {.lex_state = 0}, + [45] = {.lex_state = 0}, + [46] = {.lex_state = 0}, + [47] = {.lex_state = 0}, + [48] = {.lex_state = 0}, + [49] = {.lex_state = 0}, + [50] = {.lex_state = 0}, + [51] = {.lex_state = 0}, +}; + +static const uint16_t ts_parse_table[LARGE_STATE_COUNT][SYMBOL_COUNT] = { + [0] = { + [ts_builtin_sym_end] = ACTIONS(1), + [sym_identifier] = ACTIONS(1), + [sym_comment] = ACTIONS(1), + [anon_sym_LPAREN] = ACTIONS(1), + [anon_sym_COLON] = ACTIONS(1), + [anon_sym_RPAREN] = ACTIONS(1), + [sym_star] = ACTIONS(1), + [anon_sym_u25a1] = ACTIONS(1), + [anon_sym_LBRACK_RBRACK] = ACTIONS(1), + [anon_sym_u03bb] = ACTIONS(1), + [anon_sym_fun] = ACTIONS(1), + [anon_sym_u220f] = ACTIONS(1), + [anon_sym_forall] = ACTIONS(1), + [anon_sym_EQ_GT] = ACTIONS(1), + [anon_sym_u21d2] = ACTIONS(1), + [anon_sym_COMMA] = ACTIONS(1), + [sym_axiom] = ACTIONS(1), + [anon_sym_DASH_GT] = ACTIONS(1), + [anon_sym_u2192] = ACTIONS(1), + [anon_sym_COLON_EQ] = ACTIONS(1), + [anon_sym_SEMI] = ACTIONS(1), + }, + [1] = { + [sym_program] = STATE(45), + [sym_definition] = STATE(27), + [aux_sym_program_repeat1] = STATE(27), + [ts_builtin_sym_end] = ACTIONS(3), + [sym_identifier] = ACTIONS(5), + [sym_comment] = ACTIONS(7), + }, + [2] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(44), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + [sym_axiom] = ACTIONS(25), + }, + [3] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(49), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + [sym_axiom] = ACTIONS(27), + }, + [4] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(47), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + [sym_axiom] = ACTIONS(29), + }, + [5] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(41), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [6] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(42), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [7] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(50), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [8] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(40), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [9] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(28), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [10] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(29), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, + [11] = { + [sym_square] = STATE(16), + [sym_lambda] = STATE(32), + [sym_pi] = STATE(34), + [sym_labs] = STATE(22), + [sym_pabs] = STATE(22), + [sym_term] = STATE(12), + [sym_app] = STATE(22), + [sym_arrow] = STATE(23), + [sym_app_term] = STATE(25), + [sym_expr] = STATE(30), + [aux_sym_app_repeat1] = STATE(12), + [sym_identifier] = ACTIONS(9), + [anon_sym_LPAREN] = ACTIONS(11), + [sym_star] = ACTIONS(13), + [anon_sym_u25a1] = ACTIONS(15), + [anon_sym_LBRACK_RBRACK] = ACTIONS(15), + [anon_sym_u03bb] = ACTIONS(17), + [anon_sym_fun] = ACTIONS(19), + [anon_sym_u220f] = ACTIONS(21), + [anon_sym_forall] = ACTIONS(23), + }, +}; + +static const uint16_t ts_small_parse_table[] = { + [0] = 6, + ACTIONS(11), 1, + anon_sym_LPAREN, + STATE(16), 1, + sym_square, + ACTIONS(13), 2, + sym_identifier, + sym_star, + ACTIONS(15), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(13), 2, + sym_term, + aux_sym_app_repeat1, + ACTIONS(31), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [26] = 6, + ACTIONS(36), 1, + anon_sym_LPAREN, + STATE(16), 1, + sym_square, + ACTIONS(33), 2, + sym_identifier, + sym_star, + ACTIONS(41), 2, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + STATE(13), 2, + sym_term, + aux_sym_app_repeat1, + ACTIONS(39), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [52] = 1, + ACTIONS(44), 10, + sym_identifier, + anon_sym_LPAREN, + anon_sym_RPAREN, + sym_star, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [65] = 1, + ACTIONS(46), 10, + sym_identifier, + anon_sym_LPAREN, + anon_sym_RPAREN, + sym_star, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [78] = 1, + ACTIONS(48), 10, + sym_identifier, + anon_sym_LPAREN, + anon_sym_RPAREN, + sym_star, + anon_sym_u25a1, + anon_sym_LBRACK_RBRACK, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [91] = 4, + ACTIONS(50), 1, + anon_sym_LPAREN, + ACTIONS(53), 1, + anon_sym_COLON, + STATE(17), 2, + sym_param_block, + aux_sym_labs_repeat1, + ACTIONS(55), 4, + anon_sym_EQ_GT, + anon_sym_u21d2, + anon_sym_COMMA, + anon_sym_COLON_EQ, + [108] = 5, + ACTIONS(57), 1, + anon_sym_LPAREN, + ACTIONS(59), 1, + anon_sym_COLON, + ACTIONS(61), 1, + anon_sym_COLON_EQ, + STATE(51), 1, + sym_ascription, + STATE(19), 2, + sym_param_block, + aux_sym_labs_repeat1, + [125] = 5, + ACTIONS(57), 1, + anon_sym_LPAREN, + ACTIONS(59), 1, + anon_sym_COLON, + ACTIONS(63), 1, + anon_sym_COLON_EQ, + STATE(46), 1, + sym_ascription, + STATE(17), 2, + sym_param_block, + aux_sym_labs_repeat1, + [142] = 2, + ACTIONS(67), 1, + anon_sym_COLON, + ACTIONS(65), 5, + anon_sym_LPAREN, + anon_sym_EQ_GT, + anon_sym_u21d2, + anon_sym_COMMA, + anon_sym_COLON_EQ, + [153] = 2, + ACTIONS(71), 1, + anon_sym_COLON, + ACTIONS(69), 5, + anon_sym_LPAREN, + anon_sym_EQ_GT, + anon_sym_u21d2, + anon_sym_COMMA, + anon_sym_COLON_EQ, + [164] = 1, + ACTIONS(73), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [172] = 1, + ACTIONS(75), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [180] = 3, + ACTIONS(57), 1, + anon_sym_LPAREN, + ACTIONS(77), 2, + anon_sym_EQ_GT, + anon_sym_u21d2, + STATE(17), 2, + sym_param_block, + aux_sym_labs_repeat1, + [192] = 2, + ACTIONS(79), 2, + anon_sym_DASH_GT, + anon_sym_u2192, + ACTIONS(75), 3, + anon_sym_RPAREN, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [202] = 4, + ACTIONS(81), 1, + ts_builtin_sym_end, + ACTIONS(83), 1, + sym_identifier, + ACTIONS(86), 1, + sym_comment, + STATE(26), 2, + sym_definition, + aux_sym_program_repeat1, + [216] = 4, + ACTIONS(5), 1, + sym_identifier, + ACTIONS(89), 1, + ts_builtin_sym_end, + ACTIONS(91), 1, + sym_comment, + STATE(26), 2, + sym_definition, + aux_sym_program_repeat1, + [230] = 1, + ACTIONS(93), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [238] = 1, + ACTIONS(95), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [246] = 1, + ACTIONS(97), 5, + anon_sym_RPAREN, + anon_sym_DASH_GT, + anon_sym_u2192, + anon_sym_COLON_EQ, + anon_sym_SEMI, + [254] = 3, + ACTIONS(57), 1, + anon_sym_LPAREN, + ACTIONS(99), 1, + anon_sym_COMMA, + STATE(17), 2, + sym_param_block, + aux_sym_labs_repeat1, + [265] = 2, + ACTIONS(57), 1, + anon_sym_LPAREN, + STATE(24), 2, + sym_param_block, + aux_sym_labs_repeat1, + [273] = 3, + ACTIONS(101), 1, + sym_identifier, + ACTIONS(104), 1, + anon_sym_COLON, + STATE(33), 1, + aux_sym_param_block_repeat1, + [283] = 2, + ACTIONS(57), 1, + anon_sym_LPAREN, + STATE(31), 2, + sym_param_block, + aux_sym_labs_repeat1, + [291] = 3, + ACTIONS(106), 1, + sym_identifier, + ACTIONS(108), 1, + anon_sym_COLON, + STATE(37), 1, + aux_sym_param_block_repeat1, + [301] = 1, + ACTIONS(110), 3, + ts_builtin_sym_end, + sym_identifier, + sym_comment, + [307] = 3, + ACTIONS(112), 1, + sym_identifier, + ACTIONS(114), 1, + anon_sym_COLON, + STATE(33), 1, + aux_sym_param_block_repeat1, + [317] = 1, + ACTIONS(116), 3, + ts_builtin_sym_end, + sym_identifier, + sym_comment, + [323] = 1, + ACTIONS(118), 3, + ts_builtin_sym_end, + sym_identifier, + sym_comment, + [329] = 1, + ACTIONS(120), 1, + anon_sym_RPAREN, + [333] = 1, + ACTIONS(122), 1, + anon_sym_COLON_EQ, + [337] = 1, + ACTIONS(124), 1, + anon_sym_RPAREN, + [341] = 1, + ACTIONS(126), 1, + anon_sym_LPAREN, + [345] = 1, + ACTIONS(128), 1, + anon_sym_SEMI, + [349] = 1, + ACTIONS(130), 1, + ts_builtin_sym_end, + [353] = 1, + ACTIONS(132), 1, + anon_sym_COLON_EQ, + [357] = 1, + ACTIONS(134), 1, + anon_sym_SEMI, + [361] = 1, + ACTIONS(136), 1, + anon_sym_LPAREN, + [365] = 1, + ACTIONS(138), 1, + anon_sym_SEMI, + [369] = 1, + ACTIONS(140), 1, + anon_sym_RPAREN, + [373] = 1, + ACTIONS(63), 1, + anon_sym_COLON_EQ, +}; + +static const uint32_t ts_small_parse_table_map[] = { + [SMALL_STATE(12)] = 0, + [SMALL_STATE(13)] = 26, + [SMALL_STATE(14)] = 52, + [SMALL_STATE(15)] = 65, + [SMALL_STATE(16)] = 78, + [SMALL_STATE(17)] = 91, + [SMALL_STATE(18)] = 108, + [SMALL_STATE(19)] = 125, + [SMALL_STATE(20)] = 142, + [SMALL_STATE(21)] = 153, + [SMALL_STATE(22)] = 164, + [SMALL_STATE(23)] = 172, + [SMALL_STATE(24)] = 180, + [SMALL_STATE(25)] = 192, + [SMALL_STATE(26)] = 202, + [SMALL_STATE(27)] = 216, + [SMALL_STATE(28)] = 230, + [SMALL_STATE(29)] = 238, + [SMALL_STATE(30)] = 246, + [SMALL_STATE(31)] = 254, + [SMALL_STATE(32)] = 265, + [SMALL_STATE(33)] = 273, + [SMALL_STATE(34)] = 283, + [SMALL_STATE(35)] = 291, + [SMALL_STATE(36)] = 301, + [SMALL_STATE(37)] = 307, + [SMALL_STATE(38)] = 317, + [SMALL_STATE(39)] = 323, + [SMALL_STATE(40)] = 329, + [SMALL_STATE(41)] = 333, + [SMALL_STATE(42)] = 337, + [SMALL_STATE(43)] = 341, + [SMALL_STATE(44)] = 345, + [SMALL_STATE(45)] = 349, + [SMALL_STATE(46)] = 353, + [SMALL_STATE(47)] = 357, + [SMALL_STATE(48)] = 361, + [SMALL_STATE(49)] = 365, + [SMALL_STATE(50)] = 369, + [SMALL_STATE(51)] = 373, +}; + +static const TSParseActionEntry ts_parse_actions[] = { + [0] = {.entry = {.count = 0, .reusable = false}}, + [1] = {.entry = {.count = 1, .reusable = false}}, RECOVER(), + [3] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 0, 0, 0), + [5] = {.entry = {.count = 1, .reusable = true}}, SHIFT(18), + [7] = {.entry = {.count = 1, .reusable = true}}, SHIFT(27), + [9] = {.entry = {.count = 1, .reusable = false}}, SHIFT(16), + [11] = {.entry = {.count = 1, .reusable = true}}, SHIFT(6), + [13] = {.entry = {.count = 1, .reusable = true}}, SHIFT(16), + [15] = {.entry = {.count = 1, .reusable = true}}, SHIFT(14), + [17] = {.entry = {.count = 1, .reusable = true}}, SHIFT(48), + [19] = {.entry = {.count = 1, .reusable = false}}, SHIFT(48), + [21] = {.entry = {.count = 1, .reusable = true}}, SHIFT(43), + [23] = {.entry = {.count = 1, .reusable = false}}, SHIFT(43), + [25] = {.entry = {.count = 1, .reusable = false}}, SHIFT(44), + [27] = {.entry = {.count = 1, .reusable = false}}, SHIFT(49), + [29] = {.entry = {.count = 1, .reusable = false}}, SHIFT(47), + [31] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app, 1, 0, 0), + [33] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(16), + [36] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(6), + [39] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), + [41] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_app_repeat1, 2, 0, 0), SHIFT_REPEAT(14), + [44] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_square, 1, 0, 0), + [46] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 3, 0, 0), + [48] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_term, 1, 0, 0), + [50] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), SHIFT_REPEAT(35), + [53] = {.entry = {.count = 1, .reusable = false}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), + [55] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_labs_repeat1, 2, 0, 0), + [57] = {.entry = {.count = 1, .reusable = true}}, SHIFT(35), + [59] = {.entry = {.count = 1, .reusable = false}}, SHIFT(5), + [61] = {.entry = {.count = 1, .reusable = true}}, SHIFT(2), + [63] = {.entry = {.count = 1, .reusable = true}}, SHIFT(3), + [65] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 5, 0, 0), + [67] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 5, 0, 0), + [69] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_param_block, 4, 0, 0), + [71] = {.entry = {.count = 1, .reusable = false}}, REDUCE(sym_param_block, 4, 0, 0), + [73] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_app_term, 1, 0, 0), + [75] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_expr, 1, 0, 0), + [77] = {.entry = {.count = 1, .reusable = true}}, SHIFT(10), + [79] = {.entry = {.count = 1, .reusable = true}}, SHIFT(9), + [81] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), + [83] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(18), + [86] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_program_repeat1, 2, 0, 0), SHIFT_REPEAT(26), + [89] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_program, 1, 0, 0), + [91] = {.entry = {.count = 1, .reusable = true}}, SHIFT(26), + [93] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_arrow, 3, 0, 0), + [95] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_labs, 4, 0, 0), + [97] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pabs, 4, 0, 0), + [99] = {.entry = {.count = 1, .reusable = true}}, SHIFT(11), + [101] = {.entry = {.count = 2, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), SHIFT_REPEAT(33), + [104] = {.entry = {.count = 1, .reusable = true}}, REDUCE(aux_sym_param_block_repeat1, 2, 0, 0), + [106] = {.entry = {.count = 1, .reusable = true}}, SHIFT(37), + [108] = {.entry = {.count = 1, .reusable = true}}, SHIFT(7), + [110] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 5, 0, 0), + [112] = {.entry = {.count = 1, .reusable = true}}, SHIFT(33), + [114] = {.entry = {.count = 1, .reusable = true}}, SHIFT(8), + [116] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 4, 0, 0), + [118] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_definition, 6, 0, 0), + [120] = {.entry = {.count = 1, .reusable = true}}, SHIFT(20), + [122] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_ascription, 2, 0, 0), + [124] = {.entry = {.count = 1, .reusable = true}}, SHIFT(15), + [126] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_pi, 1, 0, 0), + [128] = {.entry = {.count = 1, .reusable = true}}, SHIFT(38), + [130] = {.entry = {.count = 1, .reusable = true}}, ACCEPT_INPUT(), + [132] = {.entry = {.count = 1, .reusable = true}}, SHIFT(4), + [134] = {.entry = {.count = 1, .reusable = true}}, SHIFT(39), + [136] = {.entry = {.count = 1, .reusable = true}}, REDUCE(sym_lambda, 1, 0, 0), + [138] = {.entry = {.count = 1, .reusable = true}}, SHIFT(36), + [140] = {.entry = {.count = 1, .reusable = true}}, SHIFT(21), +}; + +#ifdef __cplusplus +extern "C" { +#endif +#ifdef TREE_SITTER_HIDE_SYMBOLS +#define TS_PUBLIC +#elif defined(_WIN32) +#define TS_PUBLIC __declspec(dllexport) +#else +#define TS_PUBLIC __attribute__((visibility("default"))) +#endif + +TS_PUBLIC const TSLanguage *tree_sitter_perga(void) { + static const TSLanguage language = { + .version = LANGUAGE_VERSION, + .symbol_count = SYMBOL_COUNT, + .alias_count = ALIAS_COUNT, + .token_count = TOKEN_COUNT, + .external_token_count = EXTERNAL_TOKEN_COUNT, + .state_count = STATE_COUNT, + .large_state_count = LARGE_STATE_COUNT, + .production_id_count = PRODUCTION_ID_COUNT, + .field_count = FIELD_COUNT, + .max_alias_sequence_length = MAX_ALIAS_SEQUENCE_LENGTH, + .parse_table = &ts_parse_table[0][0], + .small_parse_table = ts_small_parse_table, + .small_parse_table_map = ts_small_parse_table_map, + .parse_actions = ts_parse_actions, + .symbol_names = ts_symbol_names, + .symbol_metadata = ts_symbol_metadata, + .public_symbol_map = ts_symbol_map, + .alias_map = ts_non_terminal_alias_map, + .alias_sequences = &ts_alias_sequences[0][0], + .lex_modes = ts_lex_modes, + .lex_fn = ts_lex, + .primary_state_ids = ts_primary_state_ids, + }; + return &language; +} +#ifdef __cplusplus +} +#endif diff --git a/src/tree_sitter/alloc.h b/src/tree_sitter/alloc.h new file mode 100644 index 0000000..1abdd12 --- /dev/null +++ b/src/tree_sitter/alloc.h @@ -0,0 +1,54 @@ +#ifndef TREE_SITTER_ALLOC_H_ +#define TREE_SITTER_ALLOC_H_ + +#ifdef __cplusplus +extern "C" { +#endif + +#include +#include +#include + +// Allow clients to override allocation functions +#ifdef TREE_SITTER_REUSE_ALLOCATOR + +extern void *(*ts_current_malloc)(size_t size); +extern void *(*ts_current_calloc)(size_t count, size_t size); +extern void *(*ts_current_realloc)(void *ptr, size_t size); +extern void (*ts_current_free)(void *ptr); + +#ifndef ts_malloc +#define ts_malloc ts_current_malloc +#endif +#ifndef ts_calloc +#define ts_calloc ts_current_calloc +#endif +#ifndef ts_realloc +#define ts_realloc ts_current_realloc +#endif +#ifndef ts_free +#define ts_free ts_current_free +#endif + +#else + +#ifndef ts_malloc +#define ts_malloc malloc +#endif +#ifndef ts_calloc +#define ts_calloc calloc +#endif +#ifndef ts_realloc +#define ts_realloc realloc +#endif +#ifndef ts_free +#define ts_free free +#endif + +#endif + +#ifdef __cplusplus +} +#endif + +#endif // TREE_SITTER_ALLOC_H_ diff --git a/src/tree_sitter/array.h b/src/tree_sitter/array.h new file mode 100644 index 0000000..15a3b23 --- /dev/null +++ b/src/tree_sitter/array.h @@ -0,0 +1,290 @@ +#ifndef TREE_SITTER_ARRAY_H_ +#define TREE_SITTER_ARRAY_H_ + +#ifdef __cplusplus +extern "C" { +#endif + +#include "./alloc.h" + +#include +#include +#include +#include +#include + +#ifdef _MSC_VER +#pragma warning(disable : 4101) +#elif defined(__GNUC__) || defined(__clang__) +#pragma GCC diagnostic push +#pragma GCC diagnostic ignored "-Wunused-variable" +#endif + +#define Array(T) \ + struct { \ + T *contents; \ + uint32_t size; \ + uint32_t capacity; \ + } + +/// Initialize an array. +#define array_init(self) \ + ((self)->size = 0, (self)->capacity = 0, (self)->contents = NULL) + +/// Create an empty array. +#define array_new() \ + { NULL, 0, 0 } + +/// Get a pointer to the element at a given `index` in the array. +#define array_get(self, _index) \ + (assert((uint32_t)(_index) < (self)->size), &(self)->contents[_index]) + +/// Get a pointer to the first element in the array. +#define array_front(self) array_get(self, 0) + +/// Get a pointer to the last element in the array. +#define array_back(self) array_get(self, (self)->size - 1) + +/// Clear the array, setting its size to zero. Note that this does not free any +/// memory allocated for the array's contents. +#define array_clear(self) ((self)->size = 0) + +/// Reserve `new_capacity` elements of space in the array. If `new_capacity` is +/// less than the array's current capacity, this function has no effect. +#define array_reserve(self, new_capacity) \ + _array__reserve((Array *)(self), array_elem_size(self), new_capacity) + +/// Free any memory allocated for this array. Note that this does not free any +/// memory allocated for the array's contents. +#define array_delete(self) _array__delete((Array *)(self)) + +/// Push a new `element` onto the end of the array. +#define array_push(self, element) \ + (_array__grow((Array *)(self), 1, array_elem_size(self)), \ + (self)->contents[(self)->size++] = (element)) + +/// Increase the array's size by `count` elements. +/// New elements are zero-initialized. +#define array_grow_by(self, count) \ + do { \ + if ((count) == 0) break; \ + _array__grow((Array *)(self), count, array_elem_size(self)); \ + memset((self)->contents + (self)->size, 0, (count) * array_elem_size(self)); \ + (self)->size += (count); \ + } while (0) + +/// Append all elements from one array to the end of another. +#define array_push_all(self, other) \ + array_extend((self), (other)->size, (other)->contents) + +/// Append `count` elements to the end of the array, reading their values from the +/// `contents` pointer. +#define array_extend(self, count, contents) \ + _array__splice( \ + (Array *)(self), array_elem_size(self), (self)->size, \ + 0, count, contents \ + ) + +/// Remove `old_count` elements from the array starting at the given `index`. At +/// the same index, insert `new_count` new elements, reading their values from the +/// `new_contents` pointer. +#define array_splice(self, _index, old_count, new_count, new_contents) \ + _array__splice( \ + (Array *)(self), array_elem_size(self), _index, \ + old_count, new_count, new_contents \ + ) + +/// Insert one `element` into the array at the given `index`. +#define array_insert(self, _index, element) \ + _array__splice((Array *)(self), array_elem_size(self), _index, 0, 1, &(element)) + +/// Remove one element from the array at the given `index`. +#define array_erase(self, _index) \ + _array__erase((Array *)(self), array_elem_size(self), _index) + +/// Pop the last element off the array, returning the element by value. +#define array_pop(self) ((self)->contents[--(self)->size]) + +/// Assign the contents of one array to another, reallocating if necessary. +#define array_assign(self, other) \ + _array__assign((Array *)(self), (const Array *)(other), array_elem_size(self)) + +/// Swap one array with another +#define array_swap(self, other) \ + _array__swap((Array *)(self), (Array *)(other)) + +/// Get the size of the array contents +#define array_elem_size(self) (sizeof *(self)->contents) + +/// Search a sorted array for a given `needle` value, using the given `compare` +/// callback to determine the order. +/// +/// If an existing element is found to be equal to `needle`, then the `index` +/// out-parameter is set to the existing value's index, and the `exists` +/// out-parameter is set to true. Otherwise, `index` is set to an index where +/// `needle` should be inserted in order to preserve the sorting, and `exists` +/// is set to false. +#define array_search_sorted_with(self, compare, needle, _index, _exists) \ + _array__search_sorted(self, 0, compare, , needle, _index, _exists) + +/// Search a sorted array for a given `needle` value, using integer comparisons +/// of a given struct field (specified with a leading dot) to determine the order. +/// +/// See also `array_search_sorted_with`. +#define array_search_sorted_by(self, field, needle, _index, _exists) \ + _array__search_sorted(self, 0, _compare_int, field, needle, _index, _exists) + +/// Insert a given `value` into a sorted array, using the given `compare` +/// callback to determine the order. +#define array_insert_sorted_with(self, compare, value) \ + do { \ + unsigned _index, _exists; \ + array_search_sorted_with(self, compare, &(value), &_index, &_exists); \ + if (!_exists) array_insert(self, _index, value); \ + } while (0) + +/// Insert a given `value` into a sorted array, using integer comparisons of +/// a given struct field (specified with a leading dot) to determine the order. +/// +/// See also `array_search_sorted_by`. +#define array_insert_sorted_by(self, field, value) \ + do { \ + unsigned _index, _exists; \ + array_search_sorted_by(self, field, (value) field, &_index, &_exists); \ + if (!_exists) array_insert(self, _index, value); \ + } while (0) + +// Private + +typedef Array(void) Array; + +/// This is not what you're looking for, see `array_delete`. +static inline void _array__delete(Array *self) { + if (self->contents) { + ts_free(self->contents); + self->contents = NULL; + self->size = 0; + self->capacity = 0; + } +} + +/// This is not what you're looking for, see `array_erase`. +static inline void _array__erase(Array *self, size_t element_size, + uint32_t index) { + assert(index < self->size); + char *contents = (char *)self->contents; + memmove(contents + index * element_size, contents + (index + 1) * element_size, + (self->size - index - 1) * element_size); + self->size--; +} + +/// This is not what you're looking for, see `array_reserve`. +static inline void _array__reserve(Array *self, size_t element_size, uint32_t new_capacity) { + if (new_capacity > self->capacity) { + if (self->contents) { + self->contents = ts_realloc(self->contents, new_capacity * element_size); + } else { + self->contents = ts_malloc(new_capacity * element_size); + } + self->capacity = new_capacity; + } +} + +/// This is not what you're looking for, see `array_assign`. +static inline void _array__assign(Array *self, const Array *other, size_t element_size) { + _array__reserve(self, element_size, other->size); + self->size = other->size; + memcpy(self->contents, other->contents, self->size * element_size); +} + +/// This is not what you're looking for, see `array_swap`. +static inline void _array__swap(Array *self, Array *other) { + Array swap = *other; + *other = *self; + *self = swap; +} + +/// This is not what you're looking for, see `array_push` or `array_grow_by`. +static inline void _array__grow(Array *self, uint32_t count, size_t element_size) { + uint32_t new_size = self->size + count; + if (new_size > self->capacity) { + uint32_t new_capacity = self->capacity * 2; + if (new_capacity < 8) new_capacity = 8; + if (new_capacity < new_size) new_capacity = new_size; + _array__reserve(self, element_size, new_capacity); + } +} + +/// This is not what you're looking for, see `array_splice`. +static inline void _array__splice(Array *self, size_t element_size, + uint32_t index, uint32_t old_count, + uint32_t new_count, const void *elements) { + uint32_t new_size = self->size + new_count - old_count; + uint32_t old_end = index + old_count; + uint32_t new_end = index + new_count; + assert(old_end <= self->size); + + _array__reserve(self, element_size, new_size); + + char *contents = (char *)self->contents; + if (self->size > old_end) { + memmove( + contents + new_end * element_size, + contents + old_end * element_size, + (self->size - old_end) * element_size + ); + } + if (new_count > 0) { + if (elements) { + memcpy( + (contents + index * element_size), + elements, + new_count * element_size + ); + } else { + memset( + (contents + index * element_size), + 0, + new_count * element_size + ); + } + } + self->size += new_count - old_count; +} + +/// A binary search routine, based on Rust's `std::slice::binary_search_by`. +/// This is not what you're looking for, see `array_search_sorted_with` or `array_search_sorted_by`. +#define _array__search_sorted(self, start, compare, suffix, needle, _index, _exists) \ + do { \ + *(_index) = start; \ + *(_exists) = false; \ + uint32_t size = (self)->size - *(_index); \ + if (size == 0) break; \ + int comparison; \ + while (size > 1) { \ + uint32_t half_size = size / 2; \ + uint32_t mid_index = *(_index) + half_size; \ + comparison = compare(&((self)->contents[mid_index] suffix), (needle)); \ + if (comparison <= 0) *(_index) = mid_index; \ + size -= half_size; \ + } \ + comparison = compare(&((self)->contents[*(_index)] suffix), (needle)); \ + if (comparison == 0) *(_exists) = true; \ + else if (comparison < 0) *(_index) += 1; \ + } while (0) + +/// Helper macro for the `_sorted_by` routines below. This takes the left (existing) +/// parameter by reference in order to work with the generic sorting function above. +#define _compare_int(a, b) ((int)*(a) - (int)(b)) + +#ifdef _MSC_VER +#pragma warning(default : 4101) +#elif defined(__GNUC__) || defined(__clang__) +#pragma GCC diagnostic pop +#endif + +#ifdef __cplusplus +} +#endif + +#endif // TREE_SITTER_ARRAY_H_ diff --git a/src/tree_sitter/parser.h b/src/tree_sitter/parser.h new file mode 100644 index 0000000..799f599 --- /dev/null +++ b/src/tree_sitter/parser.h @@ -0,0 +1,266 @@ +#ifndef TREE_SITTER_PARSER_H_ +#define TREE_SITTER_PARSER_H_ + +#ifdef __cplusplus +extern "C" { +#endif + +#include +#include +#include + +#define ts_builtin_sym_error ((TSSymbol)-1) +#define ts_builtin_sym_end 0 +#define TREE_SITTER_SERIALIZATION_BUFFER_SIZE 1024 + +#ifndef TREE_SITTER_API_H_ +typedef uint16_t TSStateId; +typedef uint16_t TSSymbol; +typedef uint16_t TSFieldId; +typedef struct TSLanguage TSLanguage; +#endif + +typedef struct { + TSFieldId field_id; + uint8_t child_index; + bool inherited; +} TSFieldMapEntry; + +typedef struct { + uint16_t index; + uint16_t length; +} TSFieldMapSlice; + +typedef struct { + bool visible; + bool named; + bool supertype; +} TSSymbolMetadata; + +typedef struct TSLexer TSLexer; + +struct TSLexer { + int32_t lookahead; + TSSymbol result_symbol; + void (*advance)(TSLexer *, bool); + void (*mark_end)(TSLexer *); + uint32_t (*get_column)(TSLexer *); + bool (*is_at_included_range_start)(const TSLexer *); + bool (*eof)(const TSLexer *); + void (*log)(const TSLexer *, const char *, ...); +}; + +typedef enum { + TSParseActionTypeShift, + TSParseActionTypeReduce, + TSParseActionTypeAccept, + TSParseActionTypeRecover, +} TSParseActionType; + +typedef union { + struct { + uint8_t type; + TSStateId state; + bool extra; + bool repetition; + } shift; + struct { + uint8_t type; + uint8_t child_count; + TSSymbol symbol; + int16_t dynamic_precedence; + uint16_t production_id; + } reduce; + uint8_t type; +} TSParseAction; + +typedef struct { + uint16_t lex_state; + uint16_t external_lex_state; +} TSLexMode; + +typedef union { + TSParseAction action; + struct { + uint8_t count; + bool reusable; + } entry; +} TSParseActionEntry; + +typedef struct { + int32_t start; + int32_t end; +} TSCharacterRange; + +struct TSLanguage { + uint32_t version; + uint32_t symbol_count; + uint32_t alias_count; + uint32_t token_count; + uint32_t external_token_count; + uint32_t state_count; + uint32_t large_state_count; + uint32_t production_id_count; + uint32_t field_count; + uint16_t max_alias_sequence_length; + const uint16_t *parse_table; + const uint16_t *small_parse_table; + const uint32_t *small_parse_table_map; + const TSParseActionEntry *parse_actions; + const char * const *symbol_names; + const char * const *field_names; + const TSFieldMapSlice *field_map_slices; + const TSFieldMapEntry *field_map_entries; + const TSSymbolMetadata *symbol_metadata; + const TSSymbol *public_symbol_map; + const uint16_t *alias_map; + const TSSymbol *alias_sequences; + const TSLexMode *lex_modes; + bool (*lex_fn)(TSLexer *, TSStateId); + bool (*keyword_lex_fn)(TSLexer *, TSStateId); + TSSymbol keyword_capture_token; + struct { + const bool *states; + const TSSymbol *symbol_map; + void *(*create)(void); + void (*destroy)(void *); + bool (*scan)(void *, TSLexer *, const bool *symbol_whitelist); + unsigned (*serialize)(void *, char *); + void (*deserialize)(void *, const char *, unsigned); + } external_scanner; + const TSStateId *primary_state_ids; +}; + +static inline bool set_contains(TSCharacterRange *ranges, uint32_t len, int32_t lookahead) { + uint32_t index = 0; + uint32_t size = len - index; + while (size > 1) { + uint32_t half_size = size / 2; + uint32_t mid_index = index + half_size; + TSCharacterRange *range = &ranges[mid_index]; + if (lookahead >= range->start && lookahead <= range->end) { + return true; + } else if (lookahead > range->end) { + index = mid_index; + } + size -= half_size; + } + TSCharacterRange *range = &ranges[index]; + return (lookahead >= range->start && lookahead <= range->end); +} + +/* + * Lexer Macros + */ + +#ifdef _MSC_VER +#define UNUSED __pragma(warning(suppress : 4101)) +#else +#define UNUSED __attribute__((unused)) +#endif + +#define START_LEXER() \ + bool result = false; \ + bool skip = false; \ + UNUSED \ + bool eof = false; \ + int32_t lookahead; \ + goto start; \ + next_state: \ + lexer->advance(lexer, skip); \ + start: \ + skip = false; \ + lookahead = lexer->lookahead; + +#define ADVANCE(state_value) \ + { \ + state = state_value; \ + goto next_state; \ + } + +#define ADVANCE_MAP(...) \ + { \ + static const uint16_t map[] = { __VA_ARGS__ }; \ + for (uint32_t i = 0; i < sizeof(map) / sizeof(map[0]); i += 2) { \ + if (map[i] == lookahead) { \ + state = map[i + 1]; \ + goto next_state; \ + } \ + } \ + } + +#define SKIP(state_value) \ + { \ + skip = true; \ + state = state_value; \ + goto next_state; \ + } + +#define ACCEPT_TOKEN(symbol_value) \ + result = true; \ + lexer->result_symbol = symbol_value; \ + lexer->mark_end(lexer); + +#define END_STATE() return result; + +/* + * Parse Table Macros + */ + +#define SMALL_STATE(id) ((id) - LARGE_STATE_COUNT) + +#define STATE(id) id + +#define ACTIONS(id) id + +#define SHIFT(state_value) \ + {{ \ + .shift = { \ + .type = TSParseActionTypeShift, \ + .state = (state_value) \ + } \ + }} + +#define SHIFT_REPEAT(state_value) \ + {{ \ + .shift = { \ + .type = TSParseActionTypeShift, \ + .state = (state_value), \ + .repetition = true \ + } \ + }} + +#define SHIFT_EXTRA() \ + {{ \ + .shift = { \ + .type = TSParseActionTypeShift, \ + .extra = true \ + } \ + }} + +#define REDUCE(symbol_name, children, precedence, prod_id) \ + {{ \ + .reduce = { \ + .type = TSParseActionTypeReduce, \ + .symbol = symbol_name, \ + .child_count = children, \ + .dynamic_precedence = precedence, \ + .production_id = prod_id \ + }, \ + }} + +#define RECOVER() \ + {{ \ + .type = TSParseActionTypeRecover \ + }} + +#define ACCEPT_INPUT() \ + {{ \ + .type = TSParseActionTypeAccept \ + }} + +#ifdef __cplusplus +} +#endif + +#endif // TREE_SITTER_PARSER_H_ diff --git a/test/corpus/arrows.txt b/test/corpus/arrows.txt new file mode 100644 index 0000000..cea8495 --- /dev/null +++ b/test/corpus/arrows.txt @@ -0,0 +1,54 @@ +====== +Arrows +====== + +foo (A B : *) (f : A -> A -> B) (x : A) := f x x; + +--- + +(program + (definition + (identifier) + (param_block + (identifier) + (identifier) + (expr + (app_term + (app + (term + (star)))))) + (param_block + (identifier) + (expr + (arrow + (app_term + (app + (term + (identifier)))) + (expr + (arrow + (app_term + (app + (term + (identifier)))) + (expr + (app_term + (app + (term + (identifier)))))))))) + (param_block + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) + (expr + (app_term + (app + (term + (identifier)) + (term + (identifier)) + (term + (identifier))))))) diff --git a/test/corpus/axioms.txt b/test/corpus/axioms.txt new file mode 100644 index 0000000..1cdbf91 --- /dev/null +++ b/test/corpus/axioms.txt @@ -0,0 +1,18 @@ +====== +Axioms +====== + +nat : * := axiom; + +----- + +(program + (definition + (identifier) + (ascription + (expr + (app_term + (app + (term + (star)))))) + (axiom))) diff --git a/test/corpus/comments.txt b/test/corpus/comments.txt new file mode 100644 index 0000000..6079025 --- /dev/null +++ b/test/corpus/comments.txt @@ -0,0 +1,19 @@ +======== +Comments +======== + +-- here's a comment + +foo := *; + +--- + +(program + (comment) + (definition + (identifier) + (expr + (app_term + (app + (term + (star))))))) diff --git a/test/corpus/labs.txt b/test/corpus/labs.txt new file mode 100644 index 0000000..b8a55c0 --- /dev/null +++ b/test/corpus/labs.txt @@ -0,0 +1,34 @@ +================== +Lambda Abstraction +================== + +foo := fun (A : *) (x : A) => x; + +---------- + +(program + (definition + (identifier) + (expr + (app_term + (labs + (lambda) + (param_block + (identifier) + (expr + (app_term + (app + (term + (star)))))) + (param_block + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) + (expr + (app_term + (app + (term + (identifier)))))))))) diff --git a/test/corpus/pabs.txt b/test/corpus/pabs.txt new file mode 100644 index 0000000..44bb39e --- /dev/null +++ b/test/corpus/pabs.txt @@ -0,0 +1,34 @@ +============== +Pi Abstraction +============== + +rel := forall (A : *) (x : A), *; + +---------- + +(program + (definition + (identifier) + (expr + (app_term + (pabs + (pi) + (param_block + (identifier) + (expr + (app_term + (app + (term + (star)))))) + (param_block + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) + (expr + (app_term + (app + (term + (star)))))))))) diff --git a/test/corpus/params.txt b/test/corpus/params.txt new file mode 100644 index 0000000..927a406 --- /dev/null +++ b/test/corpus/params.txt @@ -0,0 +1,32 @@ +========== +Definition +========== + +foo (A : *) (x y z : A) := x; + +--- + +(program + (definition + (identifier) + (param_block + (identifier) + (expr + (app_term + (app + (term + (star)))))) + (param_block + (identifier) + (identifier) + (identifier) + (expr + (app_term + (app + (term + (identifier)))))) + (expr + (app_term + (app + (term + (identifier))))))) diff --git a/tree-sitter.json b/tree-sitter.json new file mode 100644 index 0000000..48ef827 --- /dev/null +++ b/tree-sitter.json @@ -0,0 +1,35 @@ +{ + "grammars": [ + { + "name": "perga", + "camelcase": "Perga", + "scope": "source.perga", + "path": ".", + "file-types": ["pg"], + "injection-regex": "^perga$", + "highlights": "queries/highlights.scm" + } + ], + "metadata": { + "version": "0.1.0", + "license": "GPL3", + "description": "Basic proof assistant based on Calculus of Constructions", + "authors": [ + { + "name": "William Ball", + "email": "williampi103@gmail.com" + } + ], + "links": { + "repository": "https://forgejo.ballcloud.cc/wball/perga" + } + }, + "bindings": { + "c": true, + "go": true, + "node": true, + "python": true, + "rust": true, + "swift": true + } +}