Drop old annotation parser implementation

[coord-e]

$(cat <<'EOF'
Closes #70.

Summary

• Delete src/annot.rs (1355-line token-based annotation parser)
• Simplify extract_require_annot / extract_ensure_annot — drop the Resolver generic and self_type_name argument; only the formula_fn path remains
• Remove extract_param_annots / extract_ret_annot from local_def::Analyzer — param/ret are now handled via refinement_path formula fns (Add param/ret/sig refinement-type annotations via thrust_macros #98)
• Remove ParamResolver, ResultResolver, split_param from analyze/annot.rs
• Update is_fully_annotated to check requires_path_path / ensures_path_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 now-dead helpers: requires_path, ensures_path, param_path, ret_path, param_rty, ret_rty, impl_type

Net: −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_annotated previously 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

[Copilot]

Pull request overview

This PR completes the migration away from the legacy token-based annotation parser by removing src/annot.rs and simplifying the analysis pipeline to rely exclusively on macro-generated #[thrust::requires_path] / #[thrust::ensures_path] / #[thrust::refinement_path(..)] markers and their associated formula_fns.

Changes:

• Delete the legacy annotation parser module (src/annot.rs) and stop compiling it from src/lib.rs.
• Simplify requires/ensures extraction to only support the *_path-based mechanism (dropping resolver/self-type-name plumbing and the old AnnotFormula wrapper).
• Remove now-dead param/ret annotation extraction paths and the predicate-name workaround that existed solely for the legacy parser.

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/refine/template.rs	Removes unused builder APIs for directly injecting param/ret refined types (legacy path).
src/lib.rs	Stops compiling the legacy annot module.
src/annot.rs	Deletes the old token-based annotation parser implementation.
src/analyze/local_def.rs	Removes legacy param/ret annotation extraction and narrows “fully annotated” detection to requires/ensures path markers.
src/analyze/annot.rs	Removes legacy attribute-path helpers and resolver helpers used only by the old parser.
src/analyze/annot_fn.rs	Replaces AnnotFormula-based helpers with direct chc::Formula helpers for requires/ensures lowering.
src/analyze.rs	Simplifies requires/ensures extraction to only accept *_path-based annotations and updated lowering helpers.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.