Refactor ecPhlConseq.ml: break up monolithic dispatcher and document#965
Draft
Refactor ecPhlConseq.ml: break up monolithic dispatcher and document#965
Conversation
Member
strub
commented
Apr 3, 2026
strub
commented
- Split the ~500-line t_hi_conseq into 8 per-goal-type functions (hoareS/F, bdHoareS/F, ehoareS/F, equivS/F) with a thin dispatcher
- Extract shared helpers (t_hi_trivial, t_hi_apply_r, etc.) to module level
- Unify three identical gen_conseq_nm variants into a single polymorphic one
- Factor shared proof-term processing pipeline into process_conseq_core
- Rename process_conseq_1/2 to process_conseq_hs/ss for clarity
- Add module-level documentation: naming conventions, processing pipeline, section headers, and supported-combination comments for each dispatcher
- Split the ~500-line t_hi_conseq into 8 per-goal-type functions (hoareS/F, bdHoareS/F, ehoareS/F, equivS/F) with a thin dispatcher - Extract shared helpers (t_hi_trivial, t_hi_apply_r, etc.) to module level - Unify three identical gen_conseq_nm variants into a single polymorphic one - Factor shared proof-term processing pipeline into process_conseq_core - Rename process_conseq_1/2 to process_conseq_hs/ss for clarity - Add module-level documentation: naming conventions, processing pipeline, section headers, and supported-combination comments for each dispatcher Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Extract cond_F_notmod_core / cond_S_notmod_core shared helpers,
reducing cond_{hoare,bdHoare}{F,S}_notmod to 3-line wrappers
- Document transitivity_side_cond and t_*_conseq_equiv rules
- Document t_conseqauto algorithm
- Document process_concave tactic processing
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add inference-rule comments to every t_* function that generates subgoals via xmutate1, covering: - Core consequence rules (hoare, ehoare, bdhoare, equiv, eager) - Bound change rules (bdHoare) - Non-modification rules (notmod) - Concavity / Jensen's inequality (ehoare) - Cross-logic rules (conjunction, hoare↔bdhoare, equiv↔bdhoare) - Transitivity via equivalence (hoare/bdhoare/ehoare) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The recursive calls in t_hi_conseq_equivS and t_hi_conseq_equivF always stay within the same goal type, so the indirection through t_hi_conseq is unnecessary. Make both functions directly recursive (let rec) and remove the ~recurse parameter. t_hi_conseq no longer needs rec either. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Introduce hi_arg type alias for (proofterm option * form) option and annotate all t_hi_conseq_* dispatchers, helpers (t_hi_apply_r, t_hi_error, pp_f_node, pp_opt_f), and the main t_hi_conseq dispatcher with explicit argument and return types. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.