Fixes to allow nested polymorphic calls

Author: coord-e

src/analyze.rs

@@ -11,7 +11,6 @@ use std::collections::HashMap;
 use std::rc::Rc;
 
 use rustc_hir::lang_items::LangItem;
-use rustc_index::IndexVec;
 use rustc_middle::mir::{self, BasicBlock, Local};
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
 use rustc_span::def_id::{DefId, LocalDefId};
@@ -105,14 +104,14 @@ impl<'tcx> ReplacePlacesVisitor<'tcx> {
 }
 
 #[derive(Debug, Clone)]
-struct DeferredDefTy<'tcx> {
-    cache: Rc<RefCell<HashMap<Vec<mir_ty::Ty<'tcx>>, rty::RefinedType>>>,
+struct DeferredDefTy {
+    cache: Rc<RefCell<HashMap<rty::TypeArgs, rty::RefinedType>>>,
 }
 
 #[derive(Debug, Clone)]
-enum DefTy<'tcx> {
+enum DefTy {
     Concrete(rty::RefinedType),
-    Deferred(DeferredDefTy<'tcx>),
+    Deferred(DeferredDefTy),
 }
 
 #[derive(Clone)]
@@ -124,7 +123,7 @@ pub struct Analyzer<'tcx> {
     /// currently contains only local-def templates,
     /// but will be extended to contain externally known def's refinement types
     /// (at least for every defs referenced by local def bodies)
-    defs: HashMap<DefId, DefTy<'tcx>>,
+    defs: HashMap<DefId, DefTy>,
 
     /// Resulting CHC system.
     system: Rc<RefCell<chc::System>>,
@@ -242,11 +241,8 @@ impl<'tcx> Analyzer<'tcx> {
     pub fn def_ty_with_args(
         &mut self,
         def_id: DefId,
-        args: mir_ty::GenericArgsRef<'tcx>,
+        rty_args: rty::TypeArgs,
     ) -> Option<rty::RefinedType> {
-        let type_builder = TypeBuilder::new(self.tcx, def_id);
-        let rty_args: IndexVec<_, _> = args.types().map(|ty| type_builder.build(ty)).collect();
-
         let deferred_ty = match self.defs.get(&def_id)? {
             DefTy::Concrete(rty) => {
                 let mut def_ty = rty.clone();
@@ -262,28 +258,24 @@ impl<'tcx> Analyzer<'tcx> {
             DefTy::Deferred(deferred) => deferred,
         };
 
-        let ty_args: Vec<_> = args.types().collect();
         let deferred_ty_cache = Rc::clone(&deferred_ty.cache); // to cut reference to allow &mut self
-        if let Some(rty) = deferred_ty_cache.borrow().get(&ty_args) {
+        if let Some(rty) = deferred_ty_cache.borrow().get(&rty_args) {
             return Some(rty.clone());
         }
-        let local_def_id = def_id.as_local()?;
-
-        let sig = self
-            .tcx
-            .fn_sig(def_id)
-            .instantiate(self.tcx, args)
-            .skip_binder();
-        let expected = self
-            .crate_analyzer()
-            .fn_def_ty_with_sig(local_def_id.to_def_id(), sig)
-            .unwrap();
-        self.local_def_analyzer(local_def_id)
-            .type_builder(type_builder.with_param_mapper(move |ty| rty_args[ty.idx].clone()))
-            .run(&expected);
+
+        let type_builder = TypeBuilder::new(self.tcx, def_id).with_param_mapper({
+            let rty_args = rty_args.clone();
+            move |ty: rty::ParamType| rty_args[ty.idx].clone()
+        });
+        let mut analyzer = self.local_def_analyzer(def_id.as_local()?);
+        analyzer.type_builder(type_builder);
+
+        let expected = analyzer.expected_ty();
         deferred_ty_cache
             .borrow_mut()
-            .insert(ty_args, expected.clone());
+            .insert(rty_args, expected.clone());
+
+        analyzer.run(&expected);
         Some(expected)
     }
 

src/analyze/basic_block.rs

@@ -263,12 +263,15 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 _ty,
             ) => {
                 let func_ty = match operand.const_fn_def() {
-                    Some((def_id, args)) => self
-                        .ctx
-                        .def_ty_with_args(def_id, args)
-                        .expect("unknown def")
-                        .ty
-                        .clone(),
+                    Some((def_id, args)) => {
+                        let rty_args: IndexVec<_, _> =
+                            args.types().map(|ty| self.type_builder.build(ty)).collect();
+                        self.ctx
+                            .def_ty_with_args(def_id, rty_args)
+                            .expect("unknown def")
+                            .ty
+                            .clone()
+                    }
                     _ => unimplemented!(),
                 };
                 PlaceType::with_ty_and_term(func_ty.vacuous(), chc::Term::null())
@@ -468,12 +471,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
                 let ret = rty::RefinedType::new(rty::Type::unit(), ret_formula.into());
                 rty::FunctionType::new([param1, param2].into_iter().collect(), ret).into()
             }
-            Some((def_id, args)) => self
-                .ctx
-                .def_ty_with_args(def_id, args)
-                .expect("unknown def")
-                .ty
-                .vacuous(),
+            Some((def_id, args)) => {
+                let rty_args = args.types().map(|ty| self.type_builder.build(ty)).collect();
+                self.ctx
+                    .def_ty_with_args(def_id, rty_args)
+                    .expect("unknown def")
+                    .ty
+                    .vacuous()
+            }
             _ => self.operand_type(func.clone()).ty,
         };
         let expected_args: IndexVec<_, _> = args

src/analyze/crate_.rs

@@ -5,11 +5,9 @@ use std::collections::HashSet;
 use rustc_hir::def::DefKind;
 use rustc_index::IndexVec;
 use rustc_middle::ty::{self as mir_ty, TyCtxt};
-use rustc_span::def_id::DefId;
-use rustc_span::symbol::Ident;
+use rustc_span::def_id::{DefId, LocalDefId};
 
 use crate::analyze;
-use crate::annot::{self, AnnotFormula, AnnotParser, ResolverExt as _};
 use crate::chc;
 use crate::refine::{self, TypeBuilder};
 use crate::rty::{self, ClauseBuilderExt as _};
@@ -34,188 +32,31 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
     fn refine_local_defs(&mut self) {
         for local_def_id in self.tcx.mir_keys(()) {
             if self.tcx.def_kind(*local_def_id).is_fn_like() {
-                self.refine_fn_def(local_def_id.to_def_id());
+                self.refine_fn_def(*local_def_id);
             }
         }
     }
 
-    fn extract_require_annot<T>(
-        &self,
-        resolver: T,
-        def_id: DefId,
-    ) -> Option<AnnotFormula<T::Output>>
-    where
-        T: annot::Resolver,
-    {
-        let mut require_annot = None;
-        for attrs in self
-            .tcx
-            .get_attrs_by_path(def_id, &analyze::annot::requires_path())
-        {
-            if require_annot.is_some() {
-                unimplemented!();
-            }
-            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let require = AnnotParser::new(&resolver).parse_formula(ts).unwrap();
-            require_annot = Some(require);
-        }
-        require_annot
-    }
+    #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(local_def_id)))]
+    fn refine_fn_def(&mut self, local_def_id: LocalDefId) {
+        let mut analyzer = self.ctx.local_def_analyzer(local_def_id);
 
-    fn extract_ensure_annot<T>(&self, resolver: T, def_id: DefId) -> Option<AnnotFormula<T::Output>>
-    where
-        T: annot::Resolver,
-    {
-        let mut ensure_annot = None;
-        for attrs in self
-            .tcx
-            .get_attrs_by_path(def_id, &analyze::annot::ensures_path())
-        {
-            if ensure_annot.is_some() {
-                unimplemented!();
-            }
-            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let ensure = AnnotParser::new(&resolver).parse_formula(ts).unwrap();
-            ensure_annot = Some(ensure);
+        if analyzer.is_annotated_as_trusted() {
+            assert!(analyzer.is_fully_annotated());
+            self.trusted.insert(local_def_id.to_def_id());
         }
-        ensure_annot
-    }
 
-    fn extract_param_annots<T>(
-        &self,
-        resolver: T,
-        def_id: DefId,
-    ) -> Vec<(Ident, rty::RefinedType<T::Output>)>
-    where
-        T: annot::Resolver,
-    {
-        let mut param_annots = Vec::new();
-        for attrs in self
+        let sig = self
             .tcx
-            .get_attrs_by_path(def_id, &analyze::annot::param_path())
-        {
-            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let (ident, ts) = analyze::annot::split_param(&ts);
-            let param = AnnotParser::new(&resolver).parse_rty(ts).unwrap();
-            param_annots.push((ident, param));
-        }
-        param_annots
-    }
-
-    fn extract_ret_annot<T>(
-        &self,
-        resolver: T,
-        def_id: DefId,
-    ) -> Option<rty::RefinedType<T::Output>>
-    where
-        T: annot::Resolver,
-    {
-        let mut ret_annot = None;
-        for attrs in self
-            .tcx
-            .get_attrs_by_path(def_id, &analyze::annot::ret_path())
-        {
-            if ret_annot.is_some() {
-                unimplemented!();
-            }
-            let ts = analyze::annot::extract_annot_tokens(attrs.clone());
-            let ret = AnnotParser::new(&resolver).parse_rty(ts).unwrap();
-            ret_annot = Some(ret);
-        }
-        ret_annot
-    }
-
-    #[tracing::instrument(skip(self), fields(def_id = %self.tcx.def_path_str(def_id)))]
-    fn refine_fn_def(&mut self, def_id: DefId) {
-        let sig = self.tcx.fn_sig(def_id);
-        let sig = sig.instantiate_identity().skip_binder();
-        if let Some(rty) = self.fn_def_ty_with_sig(def_id, sig) {
-            self.ctx.register_def(def_id, rty);
-        } else {
-            self.ctx.register_deferred_def(def_id);
-        }
-    }
-
-    pub fn fn_def_ty_with_sig(
-        &mut self,
-        def_id: DefId,
-        sig: mir_ty::FnSig<'tcx>,
-    ) -> Option<rty::RefinedType> {
-        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()) {
-            let input_ty = TypeBuilder::new(self.tcx, def_id).build(*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 = TypeBuilder::new(self.tcx, def_id).build(sig.output());
-            let resolver = annot::StackedResolver::default()
-                .resolver(analyze::annot::ResultResolver::new(output_ty.to_sort()))
-                .resolver((&param_resolver).map(rty::RefinedTypeVar::Free));
-            self.extract_ensure_annot(resolver, def_id)
-        };
-        let param_annots = self.extract_param_annots(&param_resolver, def_id);
-        let ret_annot = self.extract_ret_annot(&param_resolver, def_id);
-
-        if self
-            .tcx
-            .get_attrs_by_path(def_id, &analyze::annot::callable_path())
-            .next()
-            .is_some()
-        {
-            if require_annot.is_some() || ensure_annot.is_some() {
-                unimplemented!();
-            }
-
-            require_annot = Some(AnnotFormula::top());
-            ensure_annot = Some(AnnotFormula::top());
-        }
-
-        assert!(require_annot.is_none() || param_annots.is_empty());
-        assert!(ensure_annot.is_none() || ret_annot.is_none());
-
-        if self
-            .tcx
-            .get_attrs_by_path(def_id, &analyze::annot::trusted_path())
-            .next()
-            .is_some()
-        {
-            assert!(require_annot.is_some() || !param_annots.is_empty());
-            assert!(ensure_annot.is_some() || ret_annot.is_some());
-            self.trusted.insert(def_id);
-        }
-
-        let mut builder =
-            TypeBuilder::new(self.tcx, def_id).for_function_template(&mut self.ctx, sig);
-        if let Some(AnnotFormula::Formula(require)) = require_annot {
-            let formula = require.map_var(|idx| {
-                if idx.index() == sig.inputs().len() - 1 {
-                    rty::RefinedTypeVar::Value
-                } else {
-                    rty::RefinedTypeVar::Free(idx)
-                }
-            });
-            builder.param_refinement(formula.into());
-        }
-        if let Some(AnnotFormula::Formula(ensure)) = ensure_annot {
-            builder.ret_refinement(ensure.into());
-        }
-        for (ident, annot_rty) in param_annots {
-            use annot::Resolver as _;
-            let (idx, _) = param_resolver.resolve(ident).expect("unknown param");
-            builder.param_rty(idx, annot_rty);
-        }
-        if let Some(ret_rty) = ret_annot {
-            builder.ret_rty(ret_rty);
-        }
-
-        // can't generate template with type parameter...
+            .fn_sig(local_def_id)
+            .instantiate_identity()
+            .skip_binder();
         use mir_ty::TypeVisitableExt as _;
-        if builder.would_contain_template() && sig.has_param() {
-            None
+        if sig.has_param() && !analyzer.is_fully_annotated() {
+            self.ctx.register_deferred_def(local_def_id.to_def_id());
         } else {
-            Some(rty::RefinedType::unrefined(builder.build().into()))
+            let expected = analyzer.expected_ty();
+            self.ctx.register_def(local_def_id.to_def_id(), expected);
         }
     }