Resolve impls + pprint AliasReft

flux-rs · Feb 12, 2024 · 501b27e · 501b27e
1 parent 960fb1d
commit 501b27e
Show file tree

Hide file tree

Showing 4 changed files with 29 additions and 2 deletions.
diff --git a/crates/flux-desugar/src/resolver.rs b/crates/flux-desugar/src/resolver.rs
@@ -265,6 +265,9 @@ impl<'genv, 'tcx> CrateResolver<'genv, 'tcx> {
 
     fn resolve_impl(&mut self, owner_id: OwnerId) -> Result {
         let impl_ = &self.specs.impls[&owner_id];
+        ItemResolver::run(self, owner_id, |item_resolver| {
+            item_resolver.visit_impl(impl_);
+        })?;
         RefinementResolver::resolve_impl(self, owner_id, impl_)
     }
 
@@ -595,6 +598,10 @@ impl NameResTable {
                 collector.visit_generics(generics);
                 collector.visit_ty(ty);
             }
+            ItemKind::Impl(impl_) => {
+                collector.visit_generics(impl_.generics);
+                collector.visit_ty(impl_.self_ty);
+            }
             _ => {}
         }
         collector.into_result()

diff --git a/crates/flux-middle/src/rty/expr.rs b/crates/flux-middle/src/rty/expr.rs
@@ -925,7 +925,7 @@ mod pretty {
                     w!("{:?}", kvar)
                 }
                 ExprKind::Alias(alias, args) => {
-                    w!("{:?}({:?}", ^alias, join!(", ", args))
+                    w!("{:?}({:?})", alias, join!(", ", args))
                 }
                 ExprKind::Abs(lam) => {
                     w!("{:?}", lam)
@@ -935,6 +935,18 @@ mod pretty {
         }
     }
 
+    impl Pretty for AliasReft {
+        fn fmt(&self, cx: &PPrintCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            define_scoped!(cx, f);
+            w!("<{:?} as {:?}", self.self_ty(), self.trait_id)?;
+            let args = &self.args[1..];
+            if !args.is_empty() {
+                w!("<{:?}>", join!(", ", args))?;
+            }
+            w!("::{}", ^self.name)
+        }
+    }
+
     impl Pretty for Lambda {
         fn fmt(&self, cx: &PPrintCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
             define_scoped!(cx, f);

diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs
@@ -560,6 +560,12 @@ pub struct AliasReft {
     // pub refine_args: RefineArgs,
 }
 
+impl AliasReft {
+    fn self_ty(&self) -> Ty {
+        self.args[0].expect_type().clone()
+    }
+}
+
 #[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
 pub enum TyKind {
     Indexed(BaseTy, Expr),

diff --git a/crates/flux-middle/src/rty/subst.rs b/crates/flux-middle/src/rty/subst.rs
@@ -293,7 +293,9 @@ impl GenericsSubstDelegate for GenericArgsDelegate<'_> {
     fn bty_for_param(&mut self, param_ty: ParamTy, idx: &Expr) -> Ty {
         match self.0.get(param_ty.index as usize) {
             Some(GenericArg::BaseTy(arg)) => arg.replace_bound_expr(idx),
-            Some(arg) => bug!("expected base type for generic parameter, found `{:?}`", arg),
+            Some(arg) => {
+                bug!("expected base type for generic parameter, found `{:?}`", arg)
+            }
             None => bug!("type parameter out of range"),
         }
     }