WIP add AliasEq and start porting chalk projection tests

rust-lang · Oct 12, 2023 · bc8eaf8 · bc8eaf8
1 parent bca36ec
commit bc8eaf8
Show file tree

Hide file tree

Showing 13 changed files with 385 additions and 62 deletions.
diff --git a/crates/formality-check/src/where_clauses.rs b/crates/formality-check/src/where_clauses.rs
@@ -37,6 +37,10 @@ impl super::Check<'_> {
                     assumptions,
                     trait_id.with(self_ty, parameters),
                 ),
+            WhereClauseData::AliasEq(alias_ty, ty) => {
+                self.prove_parameter_well_formed(in_env, &assumptions, alias_ty)?;
+                self.prove_parameter_well_formed(in_env, &assumptions, ty)
+            }
             WhereClauseData::Outlives(a, b) => {
                 self.prove_parameter_well_formed(in_env, &assumptions, a)?;
                 self.prove_parameter_well_formed(in_env, assumptions, b)

diff --git a/crates/formality-prove/src/prove/constraints.rs b/crates/formality-prove/src/prove/constraints.rs
@@ -81,7 +81,8 @@ impl Constraints {
     ///
     /// * `self` -- the constraints from solving `A`
     /// * `c2` -- the constraints from solving `B` (after applying substitution from `self` to `B`)
-    pub fn seq(&self, c2: impl Upcast<Constraints>) -> Constraints {
+    pub fn seq(&self, c2: impl Upcast<Constraints> + std::fmt::Debug) -> Constraints {
+        dbg!(&self, &c2);
         let c2: Constraints = c2.upcast();
 
         self.assert_valid();
@@ -110,7 +111,7 @@ impl Constraints {
         Constraints {
             env: c2.env,
             known_true: self.known_true && c2.known_true,
-            substitution: c1_substitution.into_iter().chain(c2.substitution).collect(),
+            substitution: dbg!(c1_substitution.into_iter().chain(c2.substitution).collect()),
         }
     }
 

diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
@@ -58,7 +58,7 @@ judgment_fn! {
             (prove_after(&decls, c, co_assumptions, &i.where_clause) => c)
             (prove_after(&decls, c, &assumptions, &t.where_clause) => c)
             ----------------------------- ("positive impl")
-            (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
+            (prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => dbg!(c).pop_subst(&subst))
         )
 
         (
@@ -78,6 +78,12 @@ judgment_fn! {
             (prove_wc(decls, env, assumptions, Predicate::NotImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
+        (
+            (prove_eq(decls, env, assumptions, alias_ty, ty) => c)
+            ----------------------------- ("alias eq")
+            (prove_wc(decls, env, assumptions, Predicate::AliasEq(alias_ty, ty)) => c)
+        )
+
         (
             (decls.trait_invariants() => ti)
             (let (env, subst) = env.existential_substitution(&ti.binder))

diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs
@@ -1,6 +1,6 @@
 use formality_types::{
-    grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs},
-    judgment_fn,
+    grammar::{ConstData, Parameter, RigidName, RigidTy, UniversalVar, Wcs, AliasTy, Parameters, AliasName},
+    judgment_fn, collections::Set,
 };
 
 use crate::{decls::Decls, prove::combinators::for_all};
@@ -39,10 +39,35 @@ judgment_fn! {
             (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c)
         )
 
+        (
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            --- ("integers and booleans")
+            (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(_), parameters }) => c)
+        )
+
         (
             (prove_wf(&decls, &env, &assumptions, ty) => c)
             --- ("rigid constants")
             (prove_wf(decls, env, assumptions, ConstData::Value(_, ty)) => c)
         )
+
+        (
+            (prove_alias_wf(&decls, &env, &assumptions, name, parameters) => c)
+            --- ("aliases")
+            (prove_wf(decls, env, assumptions, AliasTy { name, parameters }) => c)
+        )
     }
 }
+
+pub fn prove_alias_wf(
+    decls: &Decls,
+    env: &Env,
+    assumptions: &Wcs,
+    _name: AliasName,
+    parameters: Parameters,
+) -> Set<Constraints> {
+    tracing::debug!(?_name, ?parameters);
+
+    // FIXME: verify self type implements trait
+    for_all(decls, env, assumptions, &parameters, &prove_wf)
+}
diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs
@@ -5,7 +5,7 @@ use formality_types::{
     cast::Upcast,
     grammar::{
         AdtId, AssociatedItemId, Binder, Const, CrateId, Fallible, FieldId, FnId, Lt, Parameter,
-        TraitId, TraitRef, Ty, Wc,
+        TraitId, TraitRef, Ty, Wc, AliasTy,
     },
     term::Term,
 };
@@ -325,6 +325,7 @@ impl WhereClause {
                     .not_implemented()
                     .upcast(),
             ),
+            WhereClauseData::AliasEq(_, _) => None,
             WhereClauseData::Outlives(_, _) => None,
             WhereClauseData::ForAll(binder) => {
                 let (vars, where_clause) = binder.open();
@@ -341,6 +342,9 @@ pub enum WhereClauseData {
     #[grammar($v0 : $v1 < $,v2 >)]
     IsImplemented(Ty, TraitId, Vec<Parameter>),
 
+    #[grammar($v0 => $v1)]
+    AliasEq(AliasTy, Ty),
+
     #[grammar($v0 : $v1)]
     Outlives(Parameter, Lt),
 

diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
@@ -377,6 +377,9 @@ impl ToWcs for WhereClause {
             WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => {
                 trait_id.with(self_ty, parameters).upcast()
             }
+            WhereClauseData::AliasEq(alias_ty, ty) => {
+                Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast()
+            }
             WhereClauseData::Outlives(a, b) => Relation::outlives(a, b).upcast(),
             WhereClauseData::ForAll(binder) => {
                 let (vars, wc) = binder.open();

diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs
@@ -4,6 +4,8 @@ use crate::cast::To;
 use crate::cast::Upcast;
 use crate::cast_impl;
 
+use super::AliasName;
+use super::AliasTy;
 use super::Const;
 use super::Parameter;
 use super::Parameters;
@@ -23,6 +25,9 @@ pub enum Predicate {
     #[grammar(!$v0)]
     NotImplemented(TraitRef),
 
+    #[cast]
+    AliasEq(AliasTy, Ty),
+
     #[grammar(@WellFormedTraitRef($v0))]
     WellFormedTraitRef(TraitRef),
 
@@ -80,6 +85,7 @@ impl Parameter {
 pub enum Skeleton {
     IsImplemented(TraitId),
     NotImplemented(TraitId),
+    AliasEq(AliasName),
     WellFormed,
     WellFormedTraitRef(TraitId),
     IsLocal(TraitId),
@@ -110,6 +116,15 @@ impl Predicate {
                 Skeleton::NotImplemented(trait_id.clone()),
                 parameters.clone(),
             ),
+            Predicate::AliasEq(AliasTy { name, parameters }, ty) => {
+                let mut params = parameters.clone();
+                params.push(ty.clone().upcast());
+                (
+                    Skeleton::AliasEq(name.clone()),
+                    params,
+                )
+
+            }
             Predicate::WellFormedTraitRef(TraitRef {
                 trait_id,
                 parameters,

diff --git a/fixme_tests/basic--where-clauses.rs b/fixme_tests/basic--where-clauses.rs
diff --git a/src/lib.rs b/src/lib.rs
@@ -45,9 +45,11 @@ pub fn test_program_ok(input: &str) -> anyhow::Result<()> {
 }
 
 pub fn test_where_clause(program: &str, assertion: &str) -> anyhow::Result<Set<Constraints>> {
-    let program: Program = try_term(program)?;
-    check_all_crates(&program)?;
-    let assertion: Arc<TestAssertion> = try_term(assertion)?;
-    let decls = program.to_prove_decls();
-    Ok(formality_prove::test_util::test_prove(decls, assertion))
+    formality_core::with_tracing_logs(|| {
+        let program: Program = try_term(program)?;
+        check_all_crates(&program)?;
+        let assertion: Arc<TestAssertion> = try_term(assertion)?;
+        let decls = program.to_prove_decls();
+        Ok(formality_prove::test_util::test_prove(decls, assertion))
+    })
 }