Drop old annotation parser implementation#117
Draft
coord-e wants to merge 2 commits into
Draft
Conversation
Remove src/annot.rs (the 1355-line token-based annotation parser) and all code that depended on it. All annotation parsing now goes through the formula_fn mechanism introduced in #57. - Delete src/annot.rs entirely - Simplify extract_require_annot / extract_ensure_annot to use formula_fn paths only, dropping the Resolver generic and self_type_name arguments - Remove extract_param_annots / extract_ret_annot from local_def::Analyzer (param/ret are now handled via refinement_path formula fns from #98) - Remove ParamResolver, ResultResolver, split_param from analyze/annot.rs - Update is_fully_annotated to check requires_path / ensures_path only - Remove the dual-predicate-name workaround in analyze_predicate_definition that existed solely to support the old parser's string-based name lookup - Drop dead helpers: requires_path, ensures_path, param_path, ret_path, param_rty, ret_rty, impl_type https://claude.ai/code/session_01VBt3rgWkzGRyWMV7hfCY6i
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
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.
$(cat <<'EOF'
Closes #70.
Summary
src/annot.rs(1355-line token-based annotation parser)extract_require_annot/extract_ensure_annot— drop theResolvergeneric andself_type_nameargument; only the formula_fn path remainsextract_param_annots/extract_ret_annotfromlocal_def::Analyzer— param/ret are now handled viarefinement_pathformula fns (Add param/ret/sig refinement-type annotations via thrust_macros #98)ParamResolver,ResultResolver,split_paramfromanalyze/annot.rsis_fully_annotatedto checkrequires_path_path/ensures_path_pathonlyanalyze_predicate_definitionthat existed solely to support the old parser's string-based name lookuprequires_path,ensures_path,param_path,ret_path,param_rty,ret_rty,impl_typeNet: −1,750 lines with zero new warnings.
Notes
All three prerequisites from #70 are complete (#85, #98, #111). No test files used the old token-based annotation syntax; every annotation in the test suite already goes through
thrust_macros::*proc macros or explicit#[thrust::formula_fn]+ path statements.is_fully_annotatedpreviously had a third branch —(all_params_annotated && has_ret)— for old-style#[thrust::param]/#[thrust::ret]attributes. That branch is removed. Functions annotated purely via#[thrust_macros::param]/#[thrust_macros::ret](without requires/ensures) are not yet recognized as fully annotated; a follow-up can extend the check to scan for#[thrust::refinement_path(..)]coverage if needed.https://claude.ai/code/session_01VBt3rgWkzGRyWMV7hfCY6i
EOF
)
Generated by Claude Code