Add Gusto DSL #131
Draft
Add Gusto DSL #131
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jonaprieto
force-pushed
the
jonaprieto/syntax-enhancements
branch
from
93c17ac to
0395de6
Compare
jonaprieto
force-pushed
the
jonaprieto/syntax-enhancements
branch
from
d2c0a99 to
1c2e4d3
Compare
added 10 commits
October 21, 2025 00:42
- Introduces `#see` command and `seeThis` macro for enhanced debugging. - Adds options to control output format, including the use of `dbg_trace` vs `logInfo`, and the display of file paths and positions. - Implements filtering and exclusion of messages based on prefix patterns. - Includes tests for various output scenarios and option configurations.
- Introduces a new file `Syntax.lean` that defines the syntax categories and grammar for the Gusto DSL, a Python-like language. - Implements syntax for basic expressions, statements, compound statements, type annotations, and decorators. - Establishes a comprehensive structure for parsing Gusto code, including support for function and class definitions, as well as multi-methods.
- Adds a new file `Types.lean` defining the intermediate representation (IR) types for the Gusto language. - Implements various inductive types for function categories, member kinds, expression information, statement information, and module structures. - Establishes a comprehensive framework for representing classes, methods, fields, and decorators within the Gusto ecosystem.
- Introduces a new file `Parser.lean` that provides a comprehensive parser for the Gusto intermediate representation (IR). - Implements modular parsing functions for types, expressions, statements, parameters, decorators, fields, functions, classes, and modules. - Enhances the parsing framework with detailed error handling and debugging output for improved developer experience. - Establishes a structured approach to parse Gusto code, facilitating the translation of syntax into IR representations.
- Introduces a new file `AVM.lean` that provides the elaboration framework for Gusto classes. - Implements functions to generate enums for constructors, methods, and destructors, as well as data structures and class labels. - Enhances the class elaboration process with detailed logging for better debugging and tracking of generated components. - Establishes a structured approach to elaborate Gusto classes and modules, facilitating the development of the Gusto ecosystem.
- Introduces a new file `SyntaxTests.lean` containing comprehensive test cases for Gusto syntax. - Verifies correct parsing of various expressions, statements, and operator precedence according to the PEG grammar specification. - Utilizes `#check_failure` to ensure syntax parsing works without requiring elaboration functions, which will be implemented later. - Enhances the testing framework for Gusto, facilitating future development and debugging.
- Introduces a new file `Gusto.lean` that sets up the Gusto namespace and imports necessary components for Gusto's functionality. - Updates `Applib.lean` to include the new Gusto module, facilitating the organization and development of Gusto-related features.
- Introduces a new file `KudosGusto.lean` that defines the `Kudos` class using Gusto syntax. - Implements methods for minting, transferring, and burning tokens, encapsulating the core functionality of the Kudos module. - Establishes a foundational structure for token management within the Gusto ecosystem.
- Introduces a new file `KudosBankGusto.lean` that defines the `KudosBank`, `Check`, and `Auction` classes using Gusto syntax. - Implements methods for managing balances, transferring tokens, and handling auctions, encapsulating core banking functionalities. - Establishes multi-methods for cross-object transactions, enhancing the interaction between `KudosBank` and `Check` classes. - Provides a foundational structure for token management and auction processes within the Gusto ecosystem.
- Introduces a new file `SUMMARY.md` that provides a comprehensive overview of the Gusto DSL. - Details the purpose, syntax, and structure of Gusto, including examples for basic and advanced usage. - Explains the rationale behind using Python-like syntax and the current status of Gusto's development. - Outlines future extensibility and the advantages of Gusto as a Lean4 DSL, enhancing the documentation for developers.
jonaprieto
force-pushed
the
jonaprieto/syntax-enhancements
branch
from
1c2e4d3 to
4d30622
Compare
jonaprieto
added
documentation
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Write-up here: https://gist.github.com/jonaprieto/20004994c6ef3a760792794de76b68c7