Add DDM grammar productivity checker with correctness proofs#1156
Add DDM grammar productivity checker with correctness proofs#1156julesmt wants to merge 1 commit into
Conversation
Decides whether each declared category in a dialect admits a finite parse tree. Productivity is rooted in `frameworkAtomicCategories` — the categories the parser constructs directly — with all other categories derived from operator chains. * Strata/DDM/Analysis/Productivity.lean — algorithm + wrapper * Strata/DDM/Analysis/Productivity/Spec.lean — sound, complete, and correctness proofs for the fixpoint kernel and the top-level wrapper * StrataTest/DDM/Analysis/ProductivityTest.lean — unit tests * Scripts/ProductivityCheck.lean — `lake exe productivityCheck` One sorry remains: `transitiveImports.fuel_suffices` — proving the `n³` fuel bound is enough for the dialect-import-graph traversal.
github-actions
Bot
added
Waiting-For-Review
dependencies
| , Strata.B3AST | ||
| , Strata.B3CST | ||
| , Strata.Laurel.Laurel | ||
| ] |
There was a problem hiding this comment.
This seems like a candiate to move somewhere else and share it. strata print has a form of this. Can we reuse?
| /-! ## HashSet membership -/ | ||
|
|
||
| def Mem (s : Std.HashSet QualifiedIdent) (c : QualifiedIdent) : Prop := | ||
| s.contains c = true |
There was a problem hiding this comment.
Why introduce the special Prop? You could just use c \in s.
| | byOp : ∀ (op : OpInfo), | ||
| op ∈ ops → | ||
| (∀ a ∈ op.args, Productive ops base a) → | ||
| Productive ops base op.result |
There was a problem hiding this comment.
A docstring would really help here. What is the relationship between OpInfo and the dialects?
joehendrix
left a comment
joehendrix
left a comment
There was a problem hiding this comment.
Hi, this is an well written contribution — the proof work is clean and well-tested.
However, I'd recommend substantial changes for the goal of avoiding stack overflows. I may have used the wrong term when mentioning a productivity checker. The property we need is guaranteed progress — every cycle in the parser's call graph must consume input before recursing. Productivity (every category has a finite derivation) is a weaker property that doesn't prevent parser loops. For example, A → B ...; B → A ... will spin the Pratt parser without consuming input even though both categories are productive.
Checking progress requires knowing the operator syntax layout (which tokens come before recursive calls), which the OpInfo extraction discards. So this isn't something that can be adapted without a fundamental rework of the approach.
We could potentially adapt this as a DDM linter for unproductive non-terminals. They are potentially useful for dialects intended to be imported (like Init), but effectively dead code in terminal dialects.
3 participants
Decides whether each declared category in a dialect admits a finite parse tree. Productivity is rooted in
frameworkAtomicCategories— the categories the parser constructs directly — with all other categories derived from operator chains.lake exe productivityCheckOne sorry remains:
transitiveImports.fuel_suffices— proving then³fuel bound is enough for the dialect-import-graph traversal.Issue #, if available:
Description of changes:
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.