From f0a31d7af9366342dc2997ea92bfa216772f5963 Mon Sep 17 00:00:00 2001 From: William Ball Date: Wed, 20 Nov 2024 19:29:09 -0800 Subject: [PATCH] working? --- .editorconfig | 43 + .gitattributes | 13 + .gitignore | 40 + CMakeLists.txt | 60 + Cargo.toml | 27 + Makefile | 94 ++ Package.swift | 37 + binding.gyp | 30 + bindings/c/tree-sitter-perga.h | 16 + bindings/c/tree-sitter-perga.pc.in | 11 + bindings/go/binding.go | 13 + bindings/go/binding_test.go | 15 + bindings/node/binding.cc | 20 + bindings/node/binding_test.js | 9 + bindings/node/index.d.ts | 28 + bindings/node/index.js | 7 + bindings/python/tests/test_binding.py | 11 + bindings/python/tree_sitter_perga/__init__.py | 42 + .../python/tree_sitter_perga/__init__.pyi | 10 + bindings/python/tree_sitter_perga/binding.c | 27 + bindings/python/tree_sitter_perga/py.typed | 0 bindings/rust/build.rs | 22 + bindings/rust/lib.rs | 53 + bindings/swift/TreeSitterPerga/perga.h | 16 + .../TreeSitterPergaTests.swift | 12 + ftdetect/perga.vim | 1 + go.mod | 5 + grammar.js | 98 ++ lua/tree-sitter-perga/init.lua | 49 + package.json | 56 + pyproject.toml | 30 + queries/highlights.scm | 8 + setup.py | 62 + src/grammar.json | 348 +++++ src/node-types.json | 331 ++++ src/parser.c | 1370 +++++++++++++++++ src/tree_sitter/alloc.h | 54 + src/tree_sitter/array.h | 290 ++++ src/tree_sitter/parser.h | 266 ++++ test/corpus/arrows.txt | 54 + test/corpus/axioms.txt | 18 + test/corpus/comments.txt | 19 + test/corpus/labs.txt | 34 + test/corpus/pabs.txt | 34 + test/corpus/params.txt | 32 + tree-sitter.json | 35 + 46 files changed, 3850 insertions(+) create mode 100644 .editorconfig create mode 100644 .gitattributes create mode 100644 .gitignore create mode 100644 CMakeLists.txt create mode 100644 Cargo.toml create mode 100644 Makefile create mode 100644 Package.swift create mode 100644 binding.gyp create mode 100644 bindings/c/tree-sitter-perga.h create mode 100644 bindings/c/tree-sitter-perga.pc.in create mode 100644 bindings/go/binding.go create mode 100644 bindings/go/binding_test.go create mode 100644 bindings/node/binding.cc create mode 100644 bindings/node/binding_test.js create mode 100644 bindings/node/index.d.ts create mode 100644 bindings/node/index.js create mode 100644 bindings/python/tests/test_binding.py create mode 100644 bindings/python/tree_sitter_perga/__init__.py create mode 100644 bindings/python/tree_sitter_perga/__init__.pyi create mode 100644 bindings/python/tree_sitter_perga/binding.c create mode 100644 bindings/python/tree_sitter_perga/py.typed create mode 100644 bindings/rust/build.rs create mode 100644 bindings/rust/lib.rs create mode 100644 bindings/swift/TreeSitterPerga/perga.h create mode 100644 bindings/swift/TreeSitterPergaTests/TreeSitterPergaTests.swift create mode 100644 ftdetect/perga.vim create mode 100644 go.mod create mode 100644 grammar.js create mode 100644 lua/tree-sitter-perga/init.lua create mode 100644 package.json create mode 100644 pyproject.toml create mode 100644 queries/highlights.scm create mode 100644 setup.py create mode 100644 src/grammar.json create mode 100644 src/node-types.json create mode 100644 src/parser.c create mode 100644 src/tree_sitter/alloc.h create mode 100644 src/tree_sitter/array.h create mode 100644 src/tree_sitter/parser.h create mode 100644 test/corpus/arrows.txt create mode 100644 test/corpus/axioms.txt create mode 100644 test/corpus/comments.txt create mode 100644 test/corpus/labs.txt create mode 100644 test/corpus/pabs.txt create mode 100644 test/corpus/params.txt create mode 100644 tree-sitter.json 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 + } +}