Drop old token-based annotation parser (closes #70)

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

Author: claude

src/analyze.rs

@@ -18,7 +18,6 @@ use rustc_span::def_id::{DefId, LocalDefId};
 use rustc_span::Symbol;
 
 use crate::analyze;
-use crate::annot::{AnnotFormula, AnnotParser, Resolver};
 use crate::chc;
 use crate::pretty::PrettyDisplayExt as _;
 use crate::refine::{self, BasicBlockType, TypeBuilder};
@@ -745,103 +744,48 @@ impl<'tcx> Analyzer<'tcx> {
         None
     }
 
-    // TODO: reduce number of args
-    fn extract_require_annot<T>(
+    fn extract_require_annot(
         &self,
         local_def_id: LocalDefId,
-        resolver: T,
-        self_type_name: Option<String>,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
-    ) -> Option<AnnotFormula<T::Output>>
-    where
-        T: Resolver<Output = rty::FunctionParamIdx>,
-    {
-        let mut require_annot = None;
-        let parser = AnnotParser::new(&resolver, self_type_name);
-        for attrs in self
-            .tcx
-            .get_attrs_by_path(local_def_id.to_def_id(), &analyze::annot::requires_path())
-        {
-            if require_annot.is_some() {
-                unimplemented!();
-            }
-            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let require = parser.parse_formula(ts).unwrap();
-            require_annot = Some(require);
-        }
-
-        if let Some(formula_def_id) =
-            self.extract_path_with_attr(local_def_id, &analyze::annot::requires_path_path())
-        {
-            let Some(formula_def_id) = formula_def_id.as_local() else {
-                panic!(
-                    "require annotation with path is expected to refer to a local def, but found: {:?}",
-                    formula_def_id
-                );
-            };
-            if require_annot.is_some() {
-                unimplemented!();
-            }
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
-                panic!(
-                    "require annotation {:?} is not a formula function",
-                    formula_def_id
-                );
-            };
-            require_annot = Some(formula_fn.to_require_annot());
-        }
-
-        require_annot
+    ) -> Option<chc::Formula<rty::FunctionParamIdx>> {
+        let formula_def_id =
+            self.extract_path_with_attr(local_def_id, &analyze::annot::requires_path_path())?;
+        let Some(formula_def_id) = formula_def_id.as_local() else {
+            panic!(
+                "require annotation with path is expected to refer to a local def, but found: {:?}",
+                formula_def_id
+            );
+        };
+        let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            panic!(
+                "require annotation {:?} is not a formula function",
+                formula_def_id
+            );
+        };
+        Some(formula_fn.to_require_formula())
     }
 
-    // TODO: reduce number of args
-    fn extract_ensure_annot<T>(
+    fn extract_ensure_annot(
         &self,
         local_def_id: LocalDefId,
-        resolver: T,
-        self_type_name: Option<String>,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
-    ) -> Option<AnnotFormula<T::Output>>
-    where
-        T: Resolver<Output = rty::RefinedTypeVar<rty::FunctionParamIdx>>,
-    {
-        let mut ensure_annot = None;
-
-        let parser = AnnotParser::new(&resolver, self_type_name);
-        for attrs in self
-            .tcx
-            .get_attrs_by_path(local_def_id.to_def_id(), &analyze::annot::ensures_path())
-        {
-            if ensure_annot.is_some() {
-                unimplemented!();
-            }
-            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let ensure = parser.parse_formula(ts).unwrap();
-            ensure_annot = Some(ensure);
-        }
-
-        if let Some(formula_def_id) =
-            self.extract_path_with_attr(local_def_id, &analyze::annot::ensures_path_path())
-        {
-            let Some(formula_def_id) = formula_def_id.as_local() else {
-                panic!(
-                    "ensure annotation with path is expected to refer to a local def, but found: {:?}",
-                    formula_def_id
-                );
-            };
-            if ensure_annot.is_some() {
-                unimplemented!();
-            }
-            let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
-                panic!(
-                    "ensure annotation {:?} is not a formula function",
-                    formula_def_id
-                );
-            };
-            ensure_annot = Some(formula_fn.to_ensure_annot());
-        }
-
-        ensure_annot
+    ) -> Option<chc::Formula<rty::RefinedTypeVar<rty::FunctionParamIdx>>> {
+        let formula_def_id =
+            self.extract_path_with_attr(local_def_id, &analyze::annot::ensures_path_path())?;
+        let Some(formula_def_id) = formula_def_id.as_local() else {
+            panic!(
+                "ensure annotation with path is expected to refer to a local def, but found: {:?}",
+                formula_def_id
+            );
+        };
+        let Some(formula_fn) = self.formula_fn_with_args(formula_def_id, generic_args) else {
+            panic!(
+                "ensure annotation {:?} is not a formula function",
+                formula_def_id
+            );
+        };
+        Some(formula_fn.to_ensure_formula())
     }
 
     /// Collects every `#[thrust::refinement_path(..)]` path statement in the

src/analyze/annot.rs

@@ -2,29 +2,10 @@
 
 use rustc_ast::tokenstream::TokenStream;
 use rustc_hir::Attribute;
-use rustc_index::IndexVec;
-use rustc_span::symbol::{Ident, Symbol};
+use rustc_span::symbol::Symbol;
 
-use crate::annot;
-use crate::chc;
 use crate::rty;
 
-pub fn requires_path() -> [Symbol; 2] {
-    [Symbol::intern("thrust"), Symbol::intern("requires")]
-}
-
-pub fn ensures_path() -> [Symbol; 2] {
-    [Symbol::intern("thrust"), Symbol::intern("ensures")]
-}
-
-pub fn param_path() -> [Symbol; 2] {
-    [Symbol::intern("thrust"), Symbol::intern("param")]
-}
-
-pub fn ret_path() -> [Symbol; 2] {
-    [Symbol::intern("thrust"), Symbol::intern("ret")]
-}
-
 pub fn trusted_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("trusted")]
 }
@@ -249,62 +230,6 @@ pub fn closure_postcondition_path() -> [Symbol; 3] {
     ]
 }
 
-/// A [`annot::Resolver`] implementation for resolving function parameters.
-///
-/// The parameter names and their sorts needs to be configured via
-/// [`ParamResolver::push_param`] before use.
-#[derive(Debug, Clone, Default)]
-pub struct ParamResolver {
-    params: IndexVec<rty::FunctionParamIdx, (Symbol, chc::Sort)>,
-}
-
-impl annot::Resolver for ParamResolver {
-    type Output = rty::FunctionParamIdx;
-    fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
-        self.params
-            .iter_enumerated()
-            .find(|(_, (name, _))| name == &ident.name)
-            .map(|(idx, (_, sort))| (idx, sort.clone()))
-    }
-}
-
-impl ParamResolver {
-    pub fn push_param(&mut self, name: Symbol, sort: chc::Sort) {
-        self.params.push((name, sort));
-    }
-}
-
-/// A [`annot::Resolver`] implementation for resolving the special identifier `result`.
-///
-/// The `result` identifier is used to refer to [`rty::RefinedTypeVar::Value`] in postconditions, denoting
-/// the return value of a function.
-#[derive(Debug, Clone)]
-pub struct ResultResolver {
-    result_symbol: Symbol,
-    result_sort: chc::Sort,
-}
-
-impl annot::Resolver for ResultResolver {
-    type Output = rty::RefinedTypeVar<rty::FunctionParamIdx>;
-    fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
-        if ident.name == self.result_symbol {
-            Some((rty::RefinedTypeVar::Value, self.result_sort.clone()))
-        } else {
-            None
-        }
-    }
-}
-
-impl ResultResolver {
-    pub fn new(result_sort: chc::Sort) -> Self {
-        let result_symbol = Symbol::intern("result");
-        Self {
-            result_symbol,
-            result_sort,
-        }
-    }
-}
-
 pub fn extract_annot_tokens(attr: Attribute) -> TokenStream {
     let Attribute::Unparsed(item) = attr else {
         panic!("invalid attribute: expected unparsed");
@@ -368,18 +293,3 @@ pub fn parse_type_position(ts: &TokenStream) -> rty::TypePosition {
     rty::TypePosition::new(steps)
 }
 
-pub fn split_param(ts: &TokenStream) -> (Ident, TokenStream) {
-    use rustc_ast::token::TokenKind;
-    use rustc_ast::tokenstream::TokenTree;
-
-    let mut iter = ts.iter();
-    let (ident, _) = match iter.next() {
-        Some(TokenTree::Token(t, _)) => t.ident().expect("expected parameter name"),
-        _ => panic!("expected parameter name"),
-    };
-    match iter.next() {
-        Some(TokenTree::Token(t, _)) if t.kind == TokenKind::Colon => {}
-        _ => panic!("expected :"),
-    }
-    (ident, iter.cloned().collect())
-}

src/analyze/annot_fn.rs

@@ -6,7 +6,6 @@ use rustc_index::IndexVec;
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 
 use crate::analyze::{self, did_cache::DefIdCache};
-use crate::annot::AnnotFormula;
 use crate::chc;
 use crate::refine::{self, TypeBuilder};
 use crate::rty;
@@ -44,24 +43,24 @@ impl<'tcx> FormulaFn<'tcx> {
         &self.formula
     }
 
-    pub fn to_require_annot(&self) -> AnnotFormula<rty::FunctionParamIdx> {
-        AnnotFormula::Formula(self.formula.clone())
+    pub fn to_require_formula(&self) -> chc::Formula<rty::FunctionParamIdx> {
+        self.formula.clone()
     }
 
-    /// Lowers an `ensures` formula function into a postcondition annotation.
+    /// Lowers an `ensures` formula function into a postcondition formula.
     ///
     /// Relies on the layout produced by `thrust_macros::ensures`: parameter `0`
     /// is the function's return value (bound to [`rty::RefinedTypeVar::Value`])
     /// and parameters `1..n` are the enclosing function's parameters in order
     /// (mapped to [`rty::RefinedTypeVar::Free`]).
-    pub fn to_ensure_annot(&self) -> AnnotFormula<rty::RefinedTypeVar<rty::FunctionParamIdx>> {
-        AnnotFormula::Formula(self.formula.clone().map_var(|v| {
+    pub fn to_ensure_formula(&self) -> chc::Formula<rty::RefinedTypeVar<rty::FunctionParamIdx>> {
+        self.formula.clone().map_var(|v| {
             if v.as_usize() == 0 {
                 rty::RefinedTypeVar::Value
             } else {
                 rty::RefinedTypeVar::Free(rty::FunctionParamIdx::from(v.as_usize() - 1))
             }
-        }))
+        })
     }
 
     /// Lowers a refinement-type formula function (generated by the `param` /