diff --git a/crates/formality-check/src/fns.rs b/crates/formality-check/src/fns.rs index 15f2357a..a2130f4c 100644 --- a/crates/formality-check/src/fns.rs +++ b/crates/formality-check/src/fns.rs @@ -1,9 +1,9 @@ use formality_prove::Env; use formality_rust::{ - grammar::{Fn, FnBoundData}, + grammar::{Fn, FnBody, FnBoundData, MaybeFnBody}, prove::ToWcs, }; -use formality_types::grammar::{Fallible, Wcs}; +use formality_types::grammar::{Fallible, Relation, Wcs}; use crate::Check; @@ -29,7 +29,8 @@ impl Check<'_> { input_tys, output_ty, where_clauses, - body: _, + effect: declared_effect, + body, } = env.instantiate_universally(binder); let fn_assumptions: Wcs = (in_assumptions, &where_clauses).to_wcs(); @@ -42,6 +43,35 @@ impl Check<'_> { self.prove_goal(&env, &fn_assumptions, output_ty.well_formed())?; + // prove that the body type checks (if present) + match body { + MaybeFnBody::NoFnBody => { + // No fn body: this occurs e.g. for the fn `bar` + // in `trait Foo { fn bar(); }`. No check required. + } + MaybeFnBody::FnBody(fn_body) => match fn_body { + FnBody::TrustedFnBody => { + // Trusted: just assume it's ok, useful for tests + // to indicate things we don't want to think about. + } + FnBody::MirFnBody(_mir_fn_body) => { + // TODO: this nikomatsakis is theoretically working on removing + // though he has not made much time for it. + unimplemented!() + } + FnBody::FnBodyWithEffect(body_effect) => { + // Useful for tests: declares "some body" with the + // given effect. So we need to check that the effect + // is in bounds of the declaration. + self.prove_goal( + &env, + &fn_assumptions, + Relation::EffectSubset(body_effect, declared_effect) + )?; + } + } + } + Ok(()) } } diff --git a/crates/formality-check/src/impls.rs b/crates/formality-check/src/impls.rs index aa0cb294..98a525ee 100644 --- a/crates/formality-check/src/impls.rs +++ b/crates/formality-check/src/impls.rs @@ -11,8 +11,9 @@ use formality_rust::{ }, prove::ToWcs, }; +use formality_types::grammar::AtomicEffect::Runtime; use formality_types::{ - grammar::{Binder, Fallible, Relation, Substitution, Wcs}, + grammar::{Binder, Effect, Fallible, Relation, Substitution, Wcs}, rust::Term, }; @@ -24,6 +25,7 @@ impl super::Check<'_> { let mut env = Env::default(); let TraitImplBoundData { + effect, trait_id, self_ty, trait_parameters, @@ -31,7 +33,7 @@ impl super::Check<'_> { impl_items, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(self_ty, trait_parameters); + let trait_ref = trait_id.with(&effect, self_ty, trait_parameters); self.prove_where_clauses_well_formed(&env, &where_clauses, &where_clauses)?; @@ -43,6 +45,7 @@ impl super::Check<'_> { let TraitBoundData { where_clauses: _, trait_items, + effect_items: _, } = trait_decl.binder.instantiate_with(&trait_ref.parameters)?; self.check_safety_matches(trait_decl, trait_impl)?; @@ -67,7 +70,7 @@ impl super::Check<'_> { where_clauses, } = env.instantiate_universally(binder); - let trait_ref = trait_id.with(self_ty, trait_parameters); + let trait_ref = trait_id.with(&Effect::Atomic(Runtime), self_ty, trait_parameters); // Negative impls are always safe (rustc E0198) regardless of the trait's safety. if *safety == Safety::Unsafe { @@ -115,6 +118,44 @@ impl super::Check<'_> { } } + /// Check that function `ii_fn` that appears in an impl is valid. + /// This includes the core check from [`Self::check_fn`][], + /// but also additional checks to ensure that the signature in the impl + /// matches what is declared in the trait. + /// + /// # Example + /// + /// Suppose we are checking ` as Potable>::drink` in this example... + /// + /// ```rust,ignore + /// trait Potable { + /// fn drink(&self); // `trait_items` includes these fns + /// fn smell(&self); // + /// } + /// + /// struct Water; + /// impl Potable for Water { + /// fn drink(&self) {} + /// fn smell(&self) {} + /// } + /// + /// struct Cup; + /// impl Potable for Cup // <-- env has `L` in scope + /// where + /// L: Potable, // <-- `impl_assumptions` + /// { + /// fn drink(&self) {} // <-- `ii_fn` + /// fn smell(&self) {} // not currently being checked + /// } + /// ``` + /// + /// # Parameters + /// + /// * `env`, the environment from the impl header + /// * `impl_assumptions`, where-clauses declared on the impl + /// * `trait_items`, items declared in the trait that is being implemented + /// (we search this to find the corresponding declaration of the method) + /// * `ii_fn`, the fn as declared in the impl fn check_fn_in_impl( &self, env: &Env, @@ -143,16 +184,21 @@ impl super::Check<'_> { let mut env = env.clone(); let ( + // ii_: the signature of the function as found in the impl item (ii) FnBoundData { input_tys: ii_input_tys, output_ty: ii_output_ty, where_clauses: ii_where_clauses, + effect: ii_effect, body: _, }, + + // ti_: the signature of the function as found in the trait item (ti) FnBoundData { input_tys: ti_input_tys, output_ty: ti_output_ty, where_clauses: ti_where_clauses, + effect: ti_effect, body: _, }, ) = env.instantiate_universally(&self.merge_binders(&ii_fn.binder, &ti_fn.binder)?); @@ -163,6 +209,7 @@ impl super::Check<'_> { &ii_where_clauses, )?; + // Must have same number of arguments as declared in the trait if ii_input_tys.len() != ti_input_tys.len() { bail!( "impl has {} function arguments but trait has {} function arguments", @@ -171,6 +218,16 @@ impl super::Check<'_> { ) } + // The type `ii_input_ty` of argument `i` in the impl + // must be a supertype of the correspond type `ti_input_ty` from the trait. + // + // e.g. if you have `fn foo(arg: for<'a> fn(&u8))` in the trait + // you can have `fn foo(arg: fn(&'static u8))` in the impl. + // + // Why? Trait guarantees you are receiving a fn that can take + // an `&u8` in any lifetime. Impl is saying "I only need a fn that can + // take `&u8` in static lifetime", which is more narrow, and that's ok, + // because a functon that can handle any lifetime can also handle static. for (ii_input_ty, ti_input_ty) in ii_input_tys.iter().zip(&ti_input_tys) { self.prove_goal( &env, @@ -179,12 +236,20 @@ impl super::Check<'_> { )?; } + // Impl must return a subtype of the return type from the trait. self.prove_goal( &env, (&impl_assumptions, &ii_where_clauses), Relation::sub(ii_output_ty, ti_output_ty), )?; + // Impl must not have more effects than what are declared in the trait. + self.prove_goal( + &env, + (&impl_assumptions, &ii_where_clauses), + Relation::EffectSubset(ii_effect, ti_effect), + )?; + Ok(()) } diff --git a/crates/formality-check/src/traits.rs b/crates/formality-check/src/traits.rs index d319f652..4fa9873f 100644 --- a/crates/formality-check/src/traits.rs +++ b/crates/formality-check/src/traits.rs @@ -14,12 +14,14 @@ impl super::Check<'_> { safety: _, id: _, binder, + effect: _, } = t; let mut env = Env::default(); let TraitBoundData { where_clauses, trait_items, + effect_items: _, } = env.instantiate_universally(&binder.explicit_binder); self.check_trait_items_have_unique_names(&trait_items)?; diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 00bd5222..948e3112 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,8 +1,9 @@ use formality_core::{set, Set, Upcast}; use formality_macros::term; +use formality_types::grammar::Effect; use formality_types::grammar::{ - AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, - Wcs, + AdtId, AliasName, AliasTy, AtomicEffect, Binder, Parameter, Predicate, Relation, TraitId, + TraitRef, Ty, Wc, Wcs, }; #[term] @@ -153,8 +154,9 @@ pub enum Safety { /// It doesn't capture the trait items, which will be transformed into other sorts of rules. /// /// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`. -#[term($?safety trait $id $binder)] +#[term($?effect $?safety trait $id $binder)] pub struct TraitDecl { + pub effect: Effect, /// The name of the trait pub id: TraitId, @@ -187,6 +189,7 @@ impl TraitDecl { is_supertrait(self_var, binder.peek()) } formality_types::grammar::WcData::Implies(_, c) => is_supertrait(self_var, c), + formality_types::grammar::WcData::EffectSubset(_, _) => todo!(), } } @@ -197,7 +200,7 @@ impl TraitDecl { binder: Binder::new( &variables, TraitInvariantBoundData { - trait_ref: TraitRef::new(&self.id, &variables), + trait_ref: TraitRef::new(AtomicEffect::Runtime, &self.id, &variables), where_clause, }, ), diff --git a/crates/formality-prove/src/prove.rs b/crates/formality-prove/src/prove.rs index 315d7e1e..dcb75367 100644 --- a/crates/formality-prove/src/prove.rs +++ b/crates/formality-prove/src/prove.rs @@ -5,6 +5,7 @@ mod is_local; mod minimize; mod negation; mod prove_after; +mod prove_effect_subset; mod prove_eq; mod prove_normalize; mod prove_via; diff --git a/crates/formality-prove/src/prove/prove_effect_subset.rs b/crates/formality-prove/src/prove/prove_effect_subset.rs new file mode 100644 index 00000000..5d560fb7 --- /dev/null +++ b/crates/formality-prove/src/prove/prove_effect_subset.rs @@ -0,0 +1,152 @@ +use formality_core::judgment_fn; +use formality_types::grammar::{AtomicEffect, Effect, Relation, Wcs}; + +use crate::{ + prove::{prove_after::prove_after, prove_eq::prove_traitref_eq}, + Decls, +}; + +use super::{Constraints, Env}; + +judgment_fn! { + /// Prove an effect is the subset of another effect. + pub fn prove_effect_subset( + _decls: Decls, + env: Env, + assumptions: Wcs, + subset: Effect, + superset: Effect, + ) => Constraints { + debug(subset, superset, assumptions, env) + trivial(subset == superset => Constraints::none(env)) + + // (A union B) is a subset of C if + // * A is a subset of C and + // * B is a subset of C + ( + // first prove that `A -subset- C` + (prove_effect_subset(&decls, env, &assumptions, &*subset1, &superset) => c) + + // now prove that `B -subset- C` + (prove_after(&decls, c, &assumptions, Relation::effect_subset(&*subset2, &superset)) => c) + --- ("union") + (prove_effect_subset(decls, env, assumptions, Effect::Union(subset1, subset2), superset) => c) + ) + + // If `subset` is an atomic effect, then use the `prove_atomic_effect_subset` rule + ( + (prove_atomic_effect_subset(&decls, env, assumptions, subeffect, superset) => constraints) + --- ("atomic") + (prove_effect_subset(decls, env, assumptions, Effect::Atomic(subeffect), superset) => constraints) + ) + + // For associated effect, we get the actual effect from the trait_ref, then proceed with normal prove_effect_subset. + ( + (let subeffect = trait_ref.get_effect()) + (prove_effect_subset(decls, env, assumptions, subeffect, superset) => constraints) + --- ("associated effect") + (prove_effect_subset(decls, env, assumptions, Effect::Atomic(AtomicEffect::AssociatedEffect(trait_ref)), superset) => constraints) + + ) + + } +} + +judgment_fn! { + /// Prove that an atomic effect appears in `superset`. + /// Search for any atomic element of superset and check that it is equal. + fn prove_atomic_effect_subset( + _decls: Decls, + env: Env, + assumptions: Wcs, + atomic_subeffect: AtomicEffect, + superset: Effect, + ) => Constraints { + debug(atomic_subeffect, superset, assumptions, env) + + ( + // find some atomic effect in the superset... + (some_atomic_effect(superset) => supereffect) + // ...and prove it is equal to the atomic from the subset + (prove_atomic_effect_eq(&decls, &env, &assumptions, &atomic_subeffect, supereffect) => constraints) + --- ("union-subset-lhs") + (prove_atomic_effect_subset(decls, env, assumptions, atomic_subeffect, superset) => constraints) + ) + + // Example: we are trying to prove `X <= S` + ( + // If we can find some other effect `B` such that `X <= B`... + (prove_effect_upper_bound(&decls, env, &assumptions, &atomic_subeffect) => (c, bounding_effect)) + + // ...and we can prove `B <= S`, then we know `X <= S` (transitivity). + (prove_after(&decls, c, &assumptions, Relation::effect_subset(bounding_effect, &superset)) => c) + ----------------------------- ("transitive") + (prove_atomic_effect_subset(decls, env, assumptions, atomic_subeffect, superset) => c) + ) + + } +} + +judgment_fn! { + /// `prove_effect_bound(..., a) => b` means that `a <= b` + fn prove_effect_upper_bound( + _decls: Decls, + env: Env, + assumptions: Wcs, + f1: AtomicEffect, + ) => (Constraints, AtomicEffect) { + debug(f1, assumptions, env) + + + ( + --- ("const bounded by runtime") + (prove_effect_upper_bound(_decls, env, _assumptions, AtomicEffect::Const) => (Constraints::none(env), AtomicEffect::Runtime)) + ) + } +} + +judgment_fn! { + /// Prove two atomic effects are equal. + fn prove_atomic_effect_eq( + _decls: Decls, + env: Env, + assumptions: Wcs, + f1: AtomicEffect, + f2: AtomicEffect, + ) => Constraints { + debug(f1, f2, assumptions, env) + trivial(f1 == f2 => Constraints::none(env)) + + ( + (prove_traitref_eq(decls, env, assumptions, &*tr1, &*tr2) => constraints) + --- ("associated-effect") + (prove_atomic_effect_eq(decls, env, assumptions, AtomicEffect::AssociatedEffect(tr1), AtomicEffect::AssociatedEffect(tr2)) => constraints) + ) + } +} + +judgment_fn! { + /// Get any atomic effect from an Effect::Union. + fn some_atomic_effect( + f1: Effect + ) => AtomicEffect { + debug(f1) + + ( + (some_atomic_effect(&*f1) => e) + --- ("union-lhs") + (some_atomic_effect(Effect::Union(f1, _f2)) => e) + ) + + ( + (some_atomic_effect(&*f2) => e) + --- ("union-rhs") + (some_atomic_effect(Effect::Union(_f1, f2)) => e) + ) + + ( + --- ("atomic") + (some_atomic_effect(Effect::Atomic(e)) => e) + ) + } +} diff --git a/crates/formality-prove/src/prove/prove_eq.rs b/crates/formality-prove/src/prove/prove_eq.rs index 92dc3470..73eb0ca0 100644 --- a/crates/formality-prove/src/prove/prove_eq.rs +++ b/crates/formality-prove/src/prove/prove_eq.rs @@ -1,9 +1,11 @@ use formality_core::visit::CoreVisit; -use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast}; +use formality_core::{judgment_fn, Downcast, ProvenSet, Upcast, UpcastFrom}; use formality_core::{Deduplicate, Upcasted}; +use formality_types::grammar::TraitRef; +use formality_types::grammar::WcData; use formality_types::grammar::{ AliasTy, ExistentialVar, Parameter, Relation, RigidTy, Substitution, TyData, UniversalVar, - Variable, Wcs, + Variable, Wc, Wcs, }; use crate::{ @@ -64,8 +66,21 @@ judgment_fn! { (prove_eq(decls, env, assumptions, Variable::ExistentialVar(v), r) => c) ) + // Example: we are trying to prove `x` (which equals ` as Iterator>::Item`) + // is equal to some type `z`. ( + // Normalize `x` will find alternative "spellings" that it is equivalent to. + // For example, if there is an impl like + // `impl Iterator for SomeX { type Item = u32; ... }` + // then `prove_normalize` would yield `(c, u32)` where `c` are any constraints + // needed to show that it normalized (in this case, `c` would include the + // substitution `?V = i32`). (prove_normalize(&decls, env, &assumptions, &x) => (c, y)) + + // Now that we know that `x` is equivalent to `y`, we try to prove + // that `y` is equivalent to `z` (our original goal). + // We do that with `prove_after` so that the constraints `c` are considered + // (e.g., if `z` includes `?V`, it will be replaced with `i32`). (prove_after(&decls, c, &assumptions, eq(y, &z)) => c) ----------------------------- ("normalize-l") (prove_eq(decls, env, assumptions, x, z) => c) @@ -73,6 +88,32 @@ judgment_fn! { } } +judgment_fn! { + pub fn prove_traitref_eq( + _decls: Decls, + env: Env, + assumptions: Wcs, + a: TraitRef, + b: TraitRef, + ) => Constraints { + debug(a, b, assumptions, env) + + trivial(a == b => Constraints::none(env)) + + // Two trait_refs are equal if they have the same id, effect, and parameters. + ( + (let TraitRef { effect: a_effect, trait_id: a_trait_id, parameters: a_parameters } = a) + (let TraitRef { effect: b_effect, trait_id: b_trait_id, parameters: b_parameters } = b) + (if a_trait_id == b_trait_id)! + (prove(&decls, env, assumptions.clone(), Wcs::all_eq(a_parameters, b_parameters)) => constraints) + (prove_after(&decls, constraints, assumptions.clone(), Wc::upcast_from(WcData::EffectSubset(a_effect.clone(), b_effect.clone()))) => constraints) + (prove_after(&decls, constraints, assumptions.clone(),Wc::upcast_from(WcData::EffectSubset(b_effect.clone(), a_effect.clone()))) => constraints) + ----------------------------- ("traitref") + (prove_traitref_eq(decls, env, assumptions, a, b) => constraints) + ) + } +} + judgment_fn! { pub fn prove_existential_var_eq( _decls: Decls, diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs index 4ddbd463..0d89ff56 100644 --- a/crates/formality-prove/src/prove/prove_via.rs +++ b/crates/formality-prove/src/prove/prove_via.rs @@ -1,5 +1,5 @@ use formality_core::judgment_fn; -use formality_types::grammar::{WcData, Wcs}; +use formality_types::grammar::{DebonedPredicate, WcData, Wcs}; use crate::{ decls::Decls, @@ -23,30 +23,35 @@ judgment_fn! { debug(goal, via, assumptions, env) ( - // `c` = "clause", the name for something that we are assuming is true. - (let (skel_c, parameters_c) = pred_1.debone()) - // `g` = "goal, the name for something that we are trying to prove. - (let (skel_g, parameters_g) = pred_2.debone()) + // `c` = "clause", the name for something that we are assuming is true + (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c, effects: effects_c } = pred_c.debone()) + // `g` = "goal, the name for something that we are trying to prove + (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g, effects: effects_g } = pred_g.debone()) (if skel_c == skel_g)! (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c) + (if effects_c == effects_g) // FIXME: this is not general enough but we will revisit it ----------------------------- ("predicate-congruence-axiom") - (prove_via(decls, env, assumptions, WcData::Predicate(pred_1), WcData::Predicate(pred_2)) => c) + (prove_via(decls, env, assumptions, WcData::Predicate(pred_c), WcData::Predicate(pred_g)) => c) ) ( - (let (skel_c, parameters_c) = rel_1.debone()) - (let (skel_g, parameters_g) = rel_2.debone()) + (let DebonedPredicate { skeleton: skel_c, parameters: parameters_c, effects: effects_c } = rel_c.debone()) + (let DebonedPredicate { skeleton: skel_g, parameters: parameters_g, effects: effects_g } = rel_g.debone()) (if skel_c == skel_g) - (if parameters_c == parameters_g)! // for relations, we require 100% match + // for relations, we require 100% match + (if parameters_c == parameters_g) + (if effects_c == effects_g)! ----------------------------- ("relation-axiom") - (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env)) + (prove_via(_decls, env, _assumptions, WcData::Relation(rel_c), WcData::Relation(rel_g)) => Constraints::none(env)) ) - // If you have `where for<'a> T: Trait<'a>` then you can prove `T: Trait<'b>` for any `'b`. + // If you have `where for<'a> T: Trait<'a>` then you can prove `T: Trait<'b>` for any `'b` ( + // replace `'a` with an existential variable `?a` (let (env, subst) = env.existential_substitution(&binder)) (let via1 = binder.instantiate_with(&subst).unwrap()) - // Try to prove `T: Trait == goal`. + + // try to prove `T: Trait == goal` (prove_via(decls, env, assumptions, via1, goal) => c) ----------------------------- ("forall") (prove_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst)) diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs index 1f4f8f25..caa49ed1 100644 --- a/crates/formality-prove/src/prove/prove_wc.rs +++ b/crates/formality-prove/src/prove/prove_wc.rs @@ -9,6 +9,7 @@ use crate::{ is_local::{is_local_trait_ref, may_be_remote}, prove, prove_after::prove_after, + prove_effect_subset::prove_effect_subset, prove_eq::prove_eq, prove_via::prove_via, prove_wf::prove_wf, @@ -133,5 +134,10 @@ judgment_fn! { ----------------------------- ("const has ty") (prove_wc(decls, env, assumptions, Predicate::ConstHasType(ct, ty)) => c) ) + ( + (prove_effect_subset(decls, env, assumptions, e1, e2) => c) + ------------------------ ("effect subset") + (prove_wc(decls, env, assumptions, Relation::EffectSubset(e1, e2)) => c) + ) } } diff --git a/crates/formality-rust/src/grammar.rs b/crates/formality-rust/src/grammar.rs index 5efda3da..e834b4ce 100644 --- a/crates/formality-rust/src/grammar.rs +++ b/crates/formality-rust/src/grammar.rs @@ -2,6 +2,8 @@ use std::sync::Arc; use formality_core::{term, Upcast}; use formality_prove::Safety; +use formality_types::grammar::AtomicEffect::Runtime; +use formality_types::grammar::Effect; use formality_types::{ grammar::{ AdtId, AliasTy, AssociatedItemId, Binder, Const, ConstData, CrateId, Fallible, FieldId, @@ -174,9 +176,10 @@ pub struct Variant { pub fields: Vec, } -#[term($?safety trait $id $binder)] +#[term($?safety $?effect trait $id $binder)] pub struct Trait { pub safety: Safety, + pub effect: Effect, pub id: TraitId, pub binder: TraitBinder, } @@ -194,10 +197,11 @@ impl TraitBinder { } } -#[term($:where $,where_clauses { $*trait_items })] +#[term($:where $,where_clauses { $*effect_items $*trait_items })] pub struct TraitBoundData { pub where_clauses: Vec, pub trait_items: Vec, + pub effect_items: Vec, } #[term] @@ -214,10 +218,11 @@ pub struct Fn { pub binder: Binder, } -#[term($(input_tys) -> $output_ty $:where $,where_clauses $body)] +#[term($(input_tys) -> $output_ty $:where $,where_clauses $:do $effect $body)] pub struct FnBoundData { pub input_tys: Vec, pub output_ty: Ty, + pub effect: Effect, pub where_clauses: Vec, pub body: MaybeFnBody, } @@ -239,6 +244,9 @@ pub enum FnBody { #[cast] #[grammar(= $v0 ;)] MirFnBody(MirFnBody), + + #[grammar({($v0)})] + FnBodyWithEffect(Effect), } #[term(type $id $binder ;)] @@ -266,10 +274,14 @@ impl TraitImpl { pub fn trait_id(&self) -> &TraitId { &self.binder.peek().trait_id } + pub fn effect(&self) -> Effect { + self.binder.peek().effect.clone() + } } -#[term($trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] +#[term($?effect $trait_id $ for $self_ty $:where $,where_clauses { $*impl_items })] pub struct TraitImplBoundData { + pub effect: Effect, pub trait_id: TraitId, pub self_ty: Ty, pub trait_parameters: Vec, @@ -279,7 +291,8 @@ pub struct TraitImplBoundData { impl TraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&self.self_ty, &self.trait_parameters) + self.trait_id + .with(&self.effect, &self.self_ty, &self.trait_parameters) } } @@ -299,7 +312,11 @@ pub struct NegTraitImplBoundData { impl NegTraitImplBoundData { pub fn trait_ref(&self) -> TraitRef { - self.trait_id.with(&self.self_ty, &self.trait_parameters) + self.trait_id.with( + &Effect::Atomic(Runtime), + &self.self_ty, + &self.trait_parameters, + ) } } @@ -337,7 +354,7 @@ impl WhereClause { match self.data() { WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => Some( trait_id - .with(self_ty, parameters) + .with(&Effect::Atomic(Runtime), self_ty, parameters) .not_implemented() .upcast(), ), @@ -354,9 +371,10 @@ impl WhereClause { pub fn well_formed(&self) -> Wcs { match self.data() { - WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(self_ty, parameters).well_formed().upcast() - } + WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => trait_id + .with(&Effect::Atomic(Runtime), self_ty, parameters) + .well_formed() + .upcast(), WhereClauseData::AliasEq(alias_ty, ty) => { let alias_param: Parameter = alias_ty.upcast(); let ty_param: Parameter = ty.upcast(); diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index e62cbd4d..b516fb74 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -6,8 +6,10 @@ use crate::grammar::{ }; use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; +use formality_types::grammar::AtomicEffect::Runtime; use formality_types::grammar::{ - AdtId, AliasTy, Binder, BoundVar, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, + AdtId, AliasTy, Binder, BoundVar, Effect, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, + Wcs, }; impl Program { @@ -80,15 +82,22 @@ impl Crate { self.items .iter() .flat_map(|item| match item { - CrateItem::Trait(Trait { id, binder, safety }) => { + CrateItem::Trait(Trait { + id, + binder, + safety, + effect, + }) => { let ( vars, TraitBoundData { where_clauses, trait_items: _, + effect_items: _, }, ) = binder.open(); Some(prove::TraitDecl { + effect: effect.clone(), safety: safety.clone(), id: id.clone(), binder: Binder::new( @@ -115,6 +124,7 @@ impl Crate { let ( vars, TraitImplBoundData { + effect: _, trait_id, self_ty, trait_parameters, @@ -127,7 +137,11 @@ impl Crate { binder: Binder::new( vars, prove::ImplDeclBoundData { - trait_ref: trait_id.with(self_ty, trait_parameters), + trait_ref: trait_id.with( + &Effect::Atomic(Runtime), + self_ty, + trait_parameters, + ), where_clause: where_clauses.to_wcs(), }, ), @@ -157,7 +171,11 @@ impl Crate { binder: Binder::new( vars, prove::NegImplDeclBoundData { - trait_ref: trait_id.with(self_ty, trait_parameters), + trait_ref: trait_id.with( + &Effect::Atomic(Runtime), + self_ty, + trait_parameters, + ), where_clause: where_clauses.to_wcs(), }, ), @@ -176,6 +194,7 @@ impl Crate { let ( impl_vars, TraitImplBoundData { + effect: _, trait_id, self_ty, trait_parameters, @@ -232,12 +251,14 @@ impl Crate { safety: _, id: trait_id, binder, + .. }) => { let ( trait_vars, TraitBoundData { where_clauses: trait_wc, trait_items, + effect_items: _, }, ) = binder.open(); @@ -409,9 +430,9 @@ impl ToWcs for [WhereClause] { impl ToWcs for WhereClause { fn to_wcs(&self) -> Wcs { match self.data() { - WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => { - trait_id.with(self_ty, parameters).upcast() - } + WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => trait_id + .with(&Effect::Atomic(Runtime), self_ty, parameters) + .upcast(), WhereClauseData::AliasEq(alias_ty, ty) => { Predicate::AliasEq(alias_ty.clone(), ty.clone()).upcast() } @@ -435,9 +456,9 @@ impl WhereBound { let self_ty: Ty = self_ty.upcast(); match self.data() { - WhereBoundData::IsImplemented(trait_id, parameters) => { - trait_id.with(self_ty, parameters).upcast() - } + WhereBoundData::IsImplemented(trait_id, parameters) => trait_id + .with(&Effect::Atomic(Runtime), self_ty, parameters) + .upcast(), WhereBoundData::Outlives(lt) => Relation::outlives(self_ty, lt).upcast(), WhereBoundData::ForAll(binder) => { let (vars, bound) = binder.open(); diff --git a/crates/formality-rust/src/test.rs b/crates/formality-rust/src/test.rs index cc2c0001..59b40be9 100644 --- a/crates/formality-rust/src/test.rs +++ b/crates/formality-rust/src/test.rs @@ -33,6 +33,9 @@ fn test_parse_rust_like_trait_impl_syntax() { Ty, ], term: TraitImplBoundData { + effect: Atomic( + Runtime, + ), trait_id: PartialEq, self_ty: Ty { data: Variable( @@ -84,6 +87,9 @@ fn test_parse_rust_like_trait_syntax() { Trait( Trait { safety: Safe, + effect: Atomic( + Runtime, + ), id: Foo, binder: where ^ty0_1 : Bar <^ty0_0> { }, }, diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs index d9522c21..58245e1f 100644 --- a/crates/formality-types/src/grammar/formulas.rs +++ b/crates/formality-types/src/grammar/formulas.rs @@ -1,3 +1,5 @@ +use std::sync::Arc; + use formality_core::term; use formality_core::To; @@ -66,6 +68,10 @@ impl TraitRef { pub fn not_implemented(&self) -> Predicate { Predicate::NotImplemented(self.clone()) } + + pub fn get_effect(&self) -> Effect { + return self.effect.clone(); + } } impl Ty { @@ -97,52 +103,86 @@ pub enum Skeleton { WellFormedTraitRef(TraitId), IsLocal(TraitId), ConstHasType, + EffectSubset, Equals, Sub, Outlives, } +/// A "deboned predicate" is an alternate representation +/// of a [`Predicate`][] where the "constant" parts of the +/// predicate (e.g., which variant is it, the traid-id, etc) +/// are pulled into the "skeleton" and the unifiable parts +/// (types, lifetimes, effects) are pulled into a distinct list. +/// +/// This is useful for unifying predicates because you can +/// (1) compare the skeletons with `==` and then (2) unify the rest +/// and you don't have to write a bunch of tedious code to +/// match variants one by one. +#[term] +pub struct DebonedPredicate { + pub skeleton: Skeleton, + pub parameters: Vec, + pub effects: Vec, +} + impl Predicate { /// Separate an atomic predicate into the "skeleton" (which can be compared for equality using `==`) /// and the parameters (which must be related). #[tracing::instrument(level = "trace", ret)] - pub fn debone(&self) -> (Skeleton, Vec) { + pub fn debone(&self) -> DebonedPredicate { match self { Predicate::IsImplemented(TraitRef { + effect: _, trait_id, parameters, - }) => ( - Skeleton::IsImplemented(trait_id.clone()), - parameters.clone(), - ), + }) => DebonedPredicate { + skeleton: Skeleton::IsImplemented(trait_id.clone()), + parameters: parameters.clone(), + effects: Default::default(), + }, Predicate::NotImplemented(TraitRef { + effect: _, trait_id, parameters, - }) => ( - Skeleton::NotImplemented(trait_id.clone()), - parameters.clone(), - ), + }) => DebonedPredicate { + skeleton: Skeleton::NotImplemented(trait_id.clone()), + parameters: parameters.clone(), + effects: Default::default(), + }, Predicate::AliasEq(AliasTy { name, parameters }, ty) => { let mut params = parameters.clone(); params.push(ty.clone().upcast()); - (Skeleton::AliasEq(name.clone()), params) + DebonedPredicate { + skeleton: Skeleton::AliasEq(name.clone()), + parameters: params, + effects: Default::default(), + } } Predicate::WellFormedTraitRef(TraitRef { + effect: _, trait_id, parameters, - }) => ( - Skeleton::WellFormedTraitRef(trait_id.clone()), - parameters.clone(), - ), + }) => DebonedPredicate { + skeleton: Skeleton::WellFormedTraitRef(trait_id.clone()), + parameters: parameters.clone(), + effects: Default::default(), + }, Predicate::IsLocal(TraitRef { + effect: _, trait_id, parameters, - }) => (Skeleton::IsLocal(trait_id.clone()), parameters.clone()), - Predicate::ConstHasType(ct, ty) => ( - Skeleton::ConstHasType, - vec![ct.clone().upcast(), ty.clone().upcast()], - ), + }) => DebonedPredicate { + skeleton: Skeleton::IsLocal(trait_id.clone()), + parameters: parameters.clone(), + effects: Default::default(), + }, + Predicate::ConstHasType(ct, ty) => DebonedPredicate { + skeleton: Skeleton::ConstHasType, + parameters: vec![ct.clone().upcast(), ty.clone().upcast()], + effects: Default::default(), + }, } } } @@ -177,22 +217,74 @@ pub enum Relation { #[grammar(@wf($v0))] WellFormed(Parameter), + + // Means that the effects `$v0` are a subset of `$v1`. + #[grammar(@subset($v0, $v1))] + EffectSubset(Effect, Effect), } impl Relation { #[tracing::instrument(level = "trace", ret)] - pub fn debone(&self) -> (Skeleton, Vec) { + pub fn debone(&self) -> DebonedPredicate { match self { - Relation::Equals(a, b) => (Skeleton::Equals, vec![a.clone(), b.clone()]), - Relation::Sub(a, b) => (Skeleton::Sub, vec![a.clone(), b.clone()]), - Relation::Outlives(a, b) => (Skeleton::Outlives, vec![a.clone(), b.clone()]), - Relation::WellFormed(p) => (Skeleton::WellFormed, vec![p.clone()]), + Relation::Equals(a, b) => DebonedPredicate { + skeleton: Skeleton::Equals, + parameters: vec![a.clone(), b.clone()], + effects: Default::default(), + }, + Relation::Sub(a, b) => DebonedPredicate { + skeleton: Skeleton::Sub, + parameters: vec![a.clone(), b.clone()], + effects: Default::default(), + }, + Relation::Outlives(a, b) => DebonedPredicate { + skeleton: Skeleton::Outlives, + parameters: vec![a.clone(), b.clone()], + effects: Default::default(), + }, + Relation::WellFormed(p) => DebonedPredicate { + skeleton: Skeleton::WellFormed, + parameters: vec![p.clone()], + effects: Default::default(), + }, + Relation::EffectSubset(e1, e2) => DebonedPredicate { + skeleton: Skeleton::EffectSubset, + parameters: Default::default(), + effects: vec![e1, e2].upcast(), + }, } } } -#[term($trait_id ( $,parameters ))] +#[term] +pub enum Effect { + #[cast] + Atomic(AtomicEffect), + + #[grammar(union($v0, $v1))] + Union(Arc, Arc), +} + +impl Default for Effect { + fn default() -> Self { + AtomicEffect::default().upcast() + } +} + +#[term] +#[derive(Default)] +pub enum AtomicEffect { + Const, + #[default] + Runtime, + // For >::E, TraitRef can uniquely identify an impl, and an impl has only one effect. + #[grammar(AssociatedEffect($v0))] + AssociatedEffect(Arc), +} + +#[term($?effect $trait_id ( $,parameters ))] pub struct TraitRef { + pub effect: Effect, pub trait_id: TraitId, pub parameters: Parameters, } @@ -200,23 +292,24 @@ pub struct TraitRef { impl TraitId { pub fn with( &self, + effect: &Effect, self_ty: impl Upcast, parameters: impl Upcast>, ) -> TraitRef { let self_ty: Ty = self_ty.upcast(); let parameters: Vec = parameters.upcast(); - TraitRef::new(self, (Some(self_ty), parameters)) + TraitRef::new(effect, self, (Some(self_ty), parameters)) } } pub trait Debone { - fn debone(&self) -> (Skeleton, Vec); + fn debone(&self) -> DebonedPredicate; } macro_rules! debone_impl { ($t:ty) => { impl Debone for $t { - fn debone(&self) -> (Skeleton, Vec) { + fn debone(&self) -> DebonedPredicate { self.debone() } } diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs index c85361ad..c5d8c28b 100644 --- a/crates/formality-types/src/grammar/wc.rs +++ b/crates/formality-types/src/grammar/wc.rs @@ -4,7 +4,7 @@ use formality_core::{ cast_impl, set, term, Cons, DowncastFrom, DowncastTo, Set, Upcast, UpcastFrom, Upcasted, }; -use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef}; +use super::{Binder, BoundVar, Effect, Parameter, Predicate, Relation, TraitRef}; #[term($set)] #[derive(Default)] @@ -134,8 +134,18 @@ pub enum WcData { #[grammar(for $v0)] ForAll(Binder), + // An *implication* `if $v0 $v1` says "assuming v0 is true, v1 is true". + // These are useful to express hypothetical syntax like + // `for<'a: 'b, 'b>` or as part of an implied bounds scheme + // where you might make the Rust syntax `for<'a, 'b> T: Something<'a, 'b>` + // expand to `for<'a, 'b> if ('a: 'b) (T: Something<'a, 'b>)` + // (given `trait Something<'a, 'b> where 'a: 'b`). #[grammar(if $v0 $v1)] Implies(Wcs, Wc), + + // Means that the effects `$v0` are a subset of `$v1`. + #[grammar(subset($v0, $v1))] + EffectSubset(Effect, Effect), } // --- diff --git a/tests/const_trait.rs b/tests/const_trait.rs new file mode 100644 index 00000000..9c9a6f1f --- /dev/null +++ b/tests/const_trait.rs @@ -0,0 +1,226 @@ +#![allow(non_snake_case)] // we embed type names into the names for our test functions + +use a_mir_formality::{test_program_ok, test_where_clause}; +use formality_core::test_util::ResultTestExt; +use formality_macros::test; + +#[test] +fn test_const_syntax() { + let gen_program = |addl: &str| { + const BASE_PROGRAM: &str = "[ + crate core { + const trait Default { + } + + impl const Default for () { + } + } + + ]"; + + BASE_PROGRAM.replace("ADDITIONAL", addl) + }; + + test_program_ok(&gen_program("")).assert_ok(expect_test::expect!["()"]); +} + +#[test] +fn test_runtime_fn_with_runtime_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do runtime {(runtime)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +#[test] +fn test_const_fn_with_const_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do const {(const)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +#[test] +fn test_runtime_fn_with_const_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do runtime {(const)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +#[test] +fn test_const_fn_with_runtime_effect() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do const {(runtime)} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); + } + + +// FIXME(tiif): The trait ref syntax is a little bit confusing for now, +// `const Foo()` is the syntax for a trait ref named Foo with const effect +// `Foo()` is the syntax for a trait ref named Foo with runtime effect. + + +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// +/// { +/// ::default() +/// } +/// ```` +#[test] +fn test_associated_effect_reflexive() { + // FIXME (tiif): we should find a way to define the trait, and only using the TraitId instead of creating + // Default trait ref twice.... + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do AssociatedEffect(Default()) {(AssociatedEffect(Default()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + } + + +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// const +/// { +/// ::default() +/// } +/// ```` +#[test] +fn test_const_associated_effect_in_const_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do const {(AssociatedEffect(const Default()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + } + + +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// runtime +/// { +/// ::default() +/// } +/// ```` +#[test] +fn test_const_associated_effect_in_runtime_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do runtime {(AssociatedEffect(const Default()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + } + +/// Somewhat equivalent to +/// ``` +/// fn foo() +/// where +/// T: Default, +/// do +/// const +/// { +/// ::default() +/// } +/// ```` +#[test] +fn test_runtime_associated_effect_in_const_fn() { + let BASE_PROGRAM: &str = "[ + crate test { + fn foo() -> () random_keyword do const {(AssociatedEffect(Default()))} + } + ]"; + test_where_clause( + BASE_PROGRAM, + "{} => {}", + ) + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(AssociatedEffect(Default()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(AssociatedEffect(Default()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(AssociatedEffect(Default()) , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: AssociatedEffect(Default()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "associated effect" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: AssociatedEffect(Default()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: AssociatedEffect(Default()), assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: AssociatedEffect(Default()), f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); + } + diff --git a/tests/effects.rs b/tests/effects.rs new file mode 100644 index 00000000..f68c6e6a --- /dev/null +++ b/tests/effects.rs @@ -0,0 +1,100 @@ +use a_mir_formality::test_where_clause; +use formality_core::test_util::ResultTestExt; +use formality_types::grammar::{TraitId, TraitRef}; + +// FIXME: we don't need this for the current set of test to pass, but we might eventually need this, so keep this here. +const EFFECT_PREFIX: &str = "[ + crate test { + trait Foo { + } + } +]"; + +// Basic tests for const-runtime relation that should pass. +#[test] +fn test_const_runtime_basic() { + // (const) <: (runtime) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(const, runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + // (runtime) <: (runtime, const) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(runtime, union(runtime, const))}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + // (const) <: (runtime, const) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(const, union(runtime, const))}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + // (const, runtime) <: (runtime) + test_where_clause(EFFECT_PREFIX, "{} => {@subset(union(const, runtime), runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +// Runtime is not subset of const, so this test should fail. +#[test] +fn test_runtime_subset_const() { + test_where_clause(EFFECT_PREFIX, "{} => {@subset(runtime, const)}") + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(runtime , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(runtime , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); +} + +// Test if the rule is still correct when there is more than two atomic effects. +#[test] +fn test_three_atomic_effect() { + //union(union(const, const), runtime) <: runtime + test_where_clause(EFFECT_PREFIX, "{} => {@subset(union(union(const, const), runtime), runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); +} + +#[test] +fn test_associated_effect() { + // A runtime associated effect is subset of runtime. + test_where_clause(EFFECT_PREFIX, "{} => {@ subset(AssociatedEffect(Foo()) , runtime)}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + + + // An associated effect is subset of itself. + test_where_clause(EFFECT_PREFIX, "{} => {@ subset(AssociatedEffect(Foo()) , AssociatedEffect(Foo()))}") + .assert_ok(expect_test::expect!["{Constraints { env: Env { variables: [], bias: Soundness }, known_true: true, substitution: {} }}"]); + +} + +#[test] +fn test_assoc_runtime_not_subset_of_const() { + // A runtime associated effect is NOT subset of const. + test_where_clause(EFFECT_PREFIX, "{} => {@ subset(AssociatedEffect(Foo()) , const)}") + .assert_err(expect_test::expect![[r#" + judgment `prove { goal: {@ subset(AssociatedEffect(Foo()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo ], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + failed at (src/file.rs:LL:CC) because + judgment `prove_wc_list { goal: {@ subset(AssociatedEffect(Foo()) , const)}, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "some" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_wc { goal: @ subset(AssociatedEffect(Foo()) , const), assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "effect subset" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: AssociatedEffect(Foo()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "associated effect" failed at step #1 (src/file.rs:LL:CC) because + judgment `prove_effect_subset { subset: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: runtime, superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: runtime, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: runtime, f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_atomic_effect_subset { atomic_subeffect: AssociatedEffect(Foo()), superset: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s): + the rule "transitive" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_effect_upper_bound { f1: AssociatedEffect(Foo()), assumptions: {}, env: Env { variables: [], bias: Soundness } }` + the rule "union-subset-lhs" failed at step #1 (src/file.rs:LL:CC) because + judgment had no applicable rules: `prove_atomic_effect_eq { f1: AssociatedEffect(Foo()), f2: const, assumptions: {}, env: Env { variables: [], bias: Soundness } }`"#]]); +}