introduce metadata needed by coherence-mode

Author: nikomatsakis

crates/formality-prove/src/decls.rs

@@ -3,9 +3,10 @@ use formality_types::{
     cast::Upcast,
     collections::Set,
     grammar::{
-        AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, Wcs,
-        PR,
+        AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty,
+        Wc, Wcs, PR,
     },
+    set,
 };
 
 #[term]
@@ -16,12 +17,22 @@ pub struct Decls {
     pub neg_impl_decls: Vec<NegImplDecl>,
     pub alias_eq_decls: Vec<AliasEqDecl>,
     pub alias_bound_decls: Vec<AliasBoundDecl>,
+    pub local_trait_ids: Set<TraitId>,
+    pub local_adt_ids: Set<AdtId>,
 }
 
 impl Decls {
     /// Max size used in unit tests that are not stress testing maximum size.
     pub const DEFAULT_MAX_SIZE: usize = 222;
 
+    pub fn is_local_trait_id(&self, trait_id: &TraitId) -> bool {
+        self.local_trait_ids.contains(trait_id)
+    }
+
+    pub fn is_local_adt_id(&self, adt_id: &AdtId) -> bool {
+        self.local_adt_ids.contains(adt_id)
+    }
+
     pub fn impl_decls<'s>(&'s self, trait_id: &'s TraitId) -> impl Iterator<Item = &'s ImplDecl> {
         self.impl_decls
             .iter()
@@ -78,6 +89,8 @@ impl Decls {
             neg_impl_decls: vec![],
             alias_eq_decls: vec![],
             alias_bound_decls: vec![],
+            local_trait_ids: set![],
+            local_adt_ids: set![],
         }
     }
 }

crates/formality-prove/src/prove/env.rs

@@ -13,12 +13,24 @@ use formality_types::{
 #[derive(Default, Debug, Clone, Hash, Ord, Eq, PartialEq, PartialOrd)]
 pub struct Env {
     variables: Vec<Variable>,
+    coherence_mode: bool,
 }
 
 impl Env {
     pub fn only_universal_variables(&self) -> bool {
         self.variables.iter().all(|v| v.is_universal())
     }
+
+    pub fn is_coherence_mode(&self) -> bool {
+        self.coherence_mode
+    }
+
+    pub fn coherence_mode(self) -> Env {
+        Env {
+            coherence_mode: true,
+            ..self
+        }
+    }
 }
 
 cast_impl!(Env);
@@ -199,6 +211,7 @@ impl Env {
                 .iter()
                 .map(|&v| vs.map_var(v).unwrap_or(v))
                 .collect(),
+            coherence_mode: self.coherence_mode,
         }
     }
 

crates/formality-rust/src/prove.rs

@@ -7,8 +7,10 @@ use crate::grammar::{
 use formality_prove as prove;
 use formality_types::{
     cast::{To, Upcast, Upcasted},
+    collections::Set,
     grammar::{
-        fresh_bound_var, AliasTy, Binder, ParameterKind, Predicate, Relation, Ty, Wc, Wcs, PR,
+        fresh_bound_var, AdtId, AliasTy, Binder, ParameterKind, Predicate, Relation, TraitId, Ty,
+        Wc, Wcs, PR,
     },
     seq,
 };
@@ -22,6 +24,8 @@ impl Program {
             neg_impl_decls: self.neg_impl_decls(),
             alias_eq_decls: self.alias_eq_decls(),
             alias_bound_decls: self.alias_bound_decls(),
+            local_trait_ids: self.local_trait_ids(),
+            local_adt_ids: self.local_adt_ids(),
         }
     }
 
@@ -53,6 +57,22 @@ impl Program {
             .flat_map(|c| c.alias_bound_decls())
             .collect()
     }
+
+    fn local_trait_ids(&self) -> Set<TraitId> {
+        self.crates
+            .last()
+            .into_iter()
+            .flat_map(|c| c.trait_decls().into_iter().map(|decl| decl.id))
+            .collect()
+    }
+
+    fn local_adt_ids(&self) -> Set<AdtId> {
+        self.crates
+            .last()
+            .into_iter()
+            .flat_map(|c| c.adt_ids())
+            .collect()
+    }
 }
 
 impl Crate {
@@ -261,6 +281,20 @@ impl Crate {
             })
             .collect()
     }
+
+    fn adt_ids(&self) -> Set<AdtId> {
+        self.items
+            .iter()
+            .flat_map(|item| match item {
+                CrateItem::Struct(v) => Some(v.id.clone()),
+                CrateItem::Enum(v) => Some(v.id.clone()),
+                CrateItem::Trait(_) => None,
+                CrateItem::TraitImpl(_) => None,
+                CrateItem::NegTraitImpl(_) => None,
+                CrateItem::Fn(_) => None,
+            })
+            .collect()
+    }
 }
 
 pub trait ToWcs {