Merge pull request #145 from jackh726/alias-eq-predicate

(Mostly) add AliasEq and start porting chalk projection tests

Author: nikomatsakis

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)

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

@@ -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))

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,33 @@ judgment_fn! {
             (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c)
         )
 
+        (
+            (for_all(&decls, &env, &assumptions, &parameters, &prove_wf) => c)
+            --- ("ADT")
+            (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> {
+    // FIXME: verify self type implements trait
+    for_all(decls, env, assumptions, &parameters, &prove_wf)
+}

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),
 

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();

crates/formality-types/src/grammar/consts.rs

@@ -41,7 +41,7 @@ impl Const {
     }
 }
 
-#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
+#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Visit)]
 pub enum ConstData {
     Value(ValTree, Ty),
     Variable(Variable),

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,

fixme_tests/basic--where-clauses.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))
+    })
 }