Get rid of TermKind in annot module

Author: coord-e

src/analyze/annot.rs

@@ -1,10 +1,10 @@
 use rustc_ast::ast::Attribute;
 use rustc_ast::tokenstream::TokenStream;
 use rustc_index::IndexVec;
-use rustc_middle::ty as mir_ty;
 use rustc_span::symbol::{Ident, Symbol};
 
 use crate::annot;
+use crate::chc;
 use crate::rty;
 
 pub fn requires_path() -> [Symbol; 2] {
@@ -31,64 +31,50 @@ pub fn callable_path() -> [Symbol; 2] {
     [Symbol::intern("thrust"), Symbol::intern("callable")]
 }
 
-fn ty_to_term_kind(ty: &mir_ty::Ty<'_>) -> annot::TermKind {
-    match ty.kind() {
-        mir_ty::TyKind::Ref(_, ty, mir_ty::Mutability::Mut) => {
-            annot::TermKind::mut_(ty_to_term_kind(ty))
-        }
-        mir_ty::TyKind::Ref(_, ty, mir_ty::Mutability::Not) => {
-            annot::TermKind::box_(ty_to_term_kind(ty))
-        }
-        mir_ty::TyKind::Adt(def, _) if def.is_box() => annot::TermKind::box_(ty_to_term_kind(ty)),
-        _ => annot::TermKind::other(),
-    }
-}
-
 #[derive(Debug, Clone, Default)]
 pub struct ParamResolver {
-    params: IndexVec<rty::FunctionParamIdx, (Symbol, annot::TermKind)>,
+    params: IndexVec<rty::FunctionParamIdx, (Symbol, chc::Sort)>,
 }
 
 impl annot::Resolver for ParamResolver {
     type Output = rty::FunctionParamIdx;
-    fn resolve(&self, ident: Ident) -> Option<(Self::Output, annot::TermKind)> {
+    fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
         self.params
             .iter_enumerated()
             .find(|(_, (name, _))| name == &ident.name)
-            .map(|(idx, (_, kind))| (idx, kind.clone()))
+            .map(|(idx, (_, sort))| (idx, sort.clone()))
     }
 }
 
 impl ParamResolver {
-    pub fn push_param(&mut self, name: Symbol, ty: &mir_ty::Ty<'_>) {
-        self.params.push((name, ty_to_term_kind(ty)));
+    pub fn push_param(&mut self, name: Symbol, sort: chc::Sort) {
+        self.params.push((name, sort));
     }
 }
 
 #[derive(Debug, Clone)]
 pub struct ResultResolver {
     result_symbol: Symbol,
-    result_kind: annot::TermKind,
+    result_sort: chc::Sort,
 }
 
 impl annot::Resolver for ResultResolver {
     type Output = rty::RefinedTypeVar<rty::FunctionParamIdx>;
-    fn resolve(&self, ident: Ident) -> Option<(Self::Output, annot::TermKind)> {
+    fn resolve(&self, ident: Ident) -> Option<(Self::Output, chc::Sort)> {
         if ident.name == self.result_symbol {
-            Some((rty::RefinedTypeVar::Value, self.result_kind.clone()))
+            Some((rty::RefinedTypeVar::Value, self.result_sort.clone()))
         } else {
             None
         }
     }
 }
 
 impl ResultResolver {
-    pub fn new(result_ty: &mir_ty::Ty<'_>) -> Self {
+    pub fn new(result_sort: chc::Sort) -> Self {
         let result_symbol = Symbol::intern("result");
-        let result_kind = ty_to_term_kind(result_ty);
         Self {
             result_symbol,
-            result_kind,
+            result_sort,
         }
     }
 }

src/analyze/crate_.rs

@@ -120,13 +120,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
 
         let mut param_resolver = analyze::annot::ParamResolver::default();
         for (input_ident, input_ty) in self.tcx.fn_arg_names(def_id).iter().zip(sig.inputs()) {
-            param_resolver.push_param(input_ident.name, input_ty);
+            let input_ty = self.ctx.unrefined_ty(*input_ty);
+            param_resolver.push_param(input_ident.name, input_ty.to_sort());
         }
 
         let mut require_annot = self.extract_require_annot(&param_resolver, def_id);
         let mut ensure_annot = {
+            let output_ty = self.ctx.unrefined_ty(sig.output());
             let resolver = annot::StackedResolver::default()
-                .resolver(analyze::annot::ResultResolver::new(&sig.output()))
+                .resolver(analyze::annot::ResultResolver::new(output_ty.to_sort()))
                 .resolver((&param_resolver).map(rty::RefinedTypeVar::Free));
             self.extract_ensure_annot(resolver, def_id)
         };