Add Interactive Proof Debugger FeatureComplete proof debugging system…

[yaswanth169]

Summary

This PR adds a proof debugging feature that captures the complete execution state of SASyLF proofs and exports them to JSON format for visualization and analysis.

Features

• Complete proof tree capture with all derivation steps
• JSON export for external visualization tools
• Command-line flag: --proof-debug
• Zero performance impact when disabled
• Fully backward compatible

Implementation

New Package: edu.cmu.cs.sasylf.debugger (6 classes, 868 lines)

• ProofDebugger: Main API with thread-local state
• ProofState: Per-theorem state tracker
• DerivationStep: Individual proof step
• ProofTree: Hierarchical structure
• ContextSnapshot: Immutable context capture
• ProofStateExporter: JSON export

Modified Files (46 lines total):

• Main.java: --proof-debug flag and JSON output
• Theorem.java: ProofState initialization hook
• Derivation.java: Push/pop derivation tracking

Testing

✓ All existing regression tests pass
✓ Feature tested on: sum.slf, lambda.slf, featherweight-java.slf
✓ JSON output validated
✓ Backward compatibility confirmed (no flag = no export)

Example Usage

java -jar SASyLF.jar --proof-debug examples/sum.slf

[boyland]

Thanks for your work! It seems very interesting.
I'm open to including your changes, but you have lots of changes of existing files that merely update the formatting. Some of the formatting changes are fine, but others harmful. But in any case, formatting changes should not be mixed with semantic changes. Please update your pull request to change existing files only as needed for your extension, not because your version of VSC wants "if (condition) action" converted to add a newline.

[yaswanth169]

Thanks for the detailed review on PR #133. I’ve fully revised the PR to address the formatting concerns.

What changed

• Removed all non-semantic changes (VSCode auto-formatting, Javadoc reflow, whitespace-only diffs).
• The PR now contains only functional additions required for the Interactive Proof Debugger.

Current scope

• Minimal integration into existing files (34 total new lines):
  • Main.java: flag parsing, help text, JSON export hook
  • Theorem.java: begin/end theorem hooks
  • Derivation.java: push/pop derivation hooks
• New debugger package (~1.4k LOC) is fully self-contained.

Verification

• Compiles cleanly with no warnings.
• Tested with --proof-debug; JSON output generated correctly.
• No behavior or performance changes when the flag is not used.

This version is strictly limited to enabling JSON-based proof debugging. A separate PR will introduce the interactive visualization tool that consumes this output.

[yaswanth169]

Hi @boyland ,
When you have some time, could you please review this feature? I’d also be excited to collaborate on more strong features that have potential for impactful papers.
Let me know your availability whenever it works for you.

[boyland]

Thanks for your offer. I'm going to take a look when I get a chance. I am most interested in getting the earlier PR figured out, but it seems you've have pulled back to the scope of your changes, so I want to honor that by another review. But not yet.