Add intermediate JSON AST layer for cleaner parsing #22
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
Introduces a separation between JSON parsing and semantic translation: - jsonASTScript.sml: HOL datatypes mirroring Vyper JSON AST structure - jsonASTLib.sml/sig: SML parser that maps JSON to jsonAST HOL terms - jsonToVyperScript.sml: HOL translation from jsonAST to vyperAST The jsonAST layer captures JSON structure without semantic decisions. Translation to vyperAST handles msg.sender recognition, loop bounds, etc. Phase 4 (integration with vyperTestLib) pending. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
Phase 4: Integration - Add jsonASTLib and jsonToVyperTheory dependencies - Create toplevels_via_jsonast decoder using new pipeline: JSON → annotated_ast → translate_module (EVAL) → vyperAST - Replace old toplevels decoder usage in deployment decoder Phase 5: Cleanup - Remove ~930 lines of old JSON-to-vyperAST decoders - Keep: jsonAST pipeline, call/deployment/trace decoders, ABI decoders, test infrastructure - vyperTestLib.sml reduced from 1435 to 507 lines 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
xrchz
reviewed
Dec 21, 2025
Member
xrchz
left a comment
xrchz
left a comment
There was a problem hiding this comment.
I'm happy with this if we get some evidence that all the tests (from the Vyper test export) that used to pass still pass.
- jsonASTLib.sml: Make Int type field optional for array indices/sizes - jsonASTLib.sml: Fix keywords field handling with orElse pattern - jsonASTLib.sml: Add new json_arg format (ast_type:"arg") - vyperTestLib.sml: Update paths to use vyper-test-exports symlink - vyperTestLib.sml: Add error message to decode failure output - tests/vyperTestDefs*Script.sml: Regenerated test definitions 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Opus 4.5 <[email protected]>
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.
Fixes #21
Summary
jsonASTdatatype that mirrors JSON structure exactlyvyperTestLib.smlfrom 1435 to 507 lines by replacing ad-hoc parsing with principled pipelineArchitecture
New Files
jsonASTScript.smljsonASTLib.sml+.sigjsonToVyperScript.smlTest plan
Holmake🤖 Generated with Claude Code