diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 00bd5222..6fc36ece 100644 --- a/crates/formality-prove/src/decls.rs +++ b/crates/formality-prove/src/decls.rs @@ -1,8 +1,8 @@ use formality_core::{set, Set, Upcast}; use formality_macros::term; use formality_types::grammar::{ - AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc, - Wcs, + AdtId, AliasName, AliasTy, Binder, FnId, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, + Wc, Wcs, }; #[term] @@ -16,6 +16,7 @@ pub struct Decls { pub alias_eq_decls: Vec, pub alias_bound_decls: Vec, pub adt_decls: Vec, + pub fn_decls: Vec, pub local_trait_ids: Set, pub local_adt_ids: Set, } @@ -78,6 +79,13 @@ impl Decls { v.pop().unwrap() } + pub fn fn_decl(&self, fn_id: &FnId) -> &FnDecl { + let mut v: Vec<_> = self.fn_decls.iter().filter(|t| t.id == *fn_id).collect(); + assert!(!v.is_empty(), "no fn named `{fn_id:?}`"); + assert!(v.len() <= 1, "multiple fns named `{fn_id:?}`"); + v.pop().unwrap() + } + /// Return the set of "trait invariants" for all traits. /// See [`TraitDecl::trait_invariants`]. pub fn trait_invariants(&self) -> Set { @@ -96,6 +104,7 @@ impl Decls { alias_eq_decls: vec![], alias_bound_decls: vec![], adt_decls: vec![], + fn_decls: vec![], local_trait_ids: set![], local_adt_ids: set![], } @@ -304,3 +313,21 @@ pub struct AdtDeclBoundData { /// The where-clauses declared on the ADT, pub where_clause: Wcs, } + +/// A "function declaration" declares a function name, its generics, its input and ouput types, and its where-clauses. +/// It doesn't currently capture the function body, or input argument names. +/// +/// In Rust syntax, it covers the `fn foo(_: T) -> U where T: Bar` +#[term(fn $id $binder)] +pub struct FnDecl { + pub id: FnId, + pub binder: Binder, +} + +/// The "bound data" for a [`FnDecl`][]. +#[term(($input_tys) -> $output_ty $:where $where_clause)] +pub struct FnDeclBoundData { + pub input_tys: Vec, + pub output_ty: Ty, + pub where_clause: Wcs, +} diff --git a/crates/formality-prove/src/prove/prove_wf.rs b/crates/formality-prove/src/prove/prove_wf.rs index e6c816b6..790b9d92 100644 --- a/crates/formality-prove/src/prove/prove_wf.rs +++ b/crates/formality-prove/src/prove/prove_wf.rs @@ -42,6 +42,13 @@ judgment_fn! { (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::ScalarId(_), parameters }) => c) ) + ( + // only checks that type is well-formed, does not do any lifetime or borrow check + (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + --- ("ref") + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::Ref(_), parameters }) => c) + ) + ( (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) (let t = decls.adt_decl(&adt_id)) @@ -51,6 +58,21 @@ judgment_fn! { (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::AdtId(adt_id), parameters }) => c) ) + ( + (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + (let t = decls.fn_decl(&fn_id)) + (let t = t.binder.instantiate_with(¶meters).unwrap()) + (prove_after(&decls, c, &assumptions, t.where_clause) => c) + --- ("fn-defs") + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::FnDef(fn_id), parameters }) => c) + ) + + ( + (for_all(&decls, &env, &assumptions, ¶meters, &prove_wf) => c) + --- ("fn-ptr") + (prove_wf(decls, env, assumptions, RigidTy { name: RigidName::FnPtr(_), parameters }) => c) + ) + ( (prove_wf(&decls, &env, &assumptions, ty) => c) --- ("rigid constants") diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs index e62cbd4d..7ca9e600 100644 --- a/crates/formality-rust/src/prove.rs +++ b/crates/formality-rust/src/prove.rs @@ -1,8 +1,8 @@ use crate::grammar::{ Adt, AdtBoundData, AssociatedTy, AssociatedTyBoundData, AssociatedTyValue, - AssociatedTyValueBoundData, Crate, CrateItem, ImplItem, NegTraitImpl, NegTraitImplBoundData, - Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, TraitItem, WhereBound, - WhereBoundData, WhereClause, WhereClauseData, + AssociatedTyValueBoundData, Crate, CrateItem, Fn, FnBoundData, ImplItem, NegTraitImpl, + NegTraitImplBoundData, Program, Trait, TraitBoundData, TraitImpl, TraitImplBoundData, + TraitItem, WhereBound, WhereBoundData, WhereClause, WhereClauseData, }; use formality_core::{seq, Set, To, Upcast, Upcasted}; use formality_prove as prove; @@ -20,6 +20,7 @@ impl Program { alias_eq_decls: self.alias_eq_decls(), alias_bound_decls: self.alias_bound_decls(), adt_decls: self.adt_decls(), + fn_decls: self.fn_decls(), local_trait_ids: self.local_trait_ids(), local_adt_ids: self.local_adt_ids(), } @@ -58,6 +59,10 @@ impl Program { self.crates.iter().flat_map(|c| c.adt_decls()).collect() } + fn fn_decls(&self) -> Vec { + self.crates.iter().flat_map(|c| c.fn_decls()).collect() + } + fn local_trait_ids(&self) -> Set { self.crates .last() @@ -330,6 +335,31 @@ impl Crate { }) .collect() } + + fn fn_decls(&self) -> Vec { + self.items + .iter() + .flat_map(|item| match item { + CrateItem::Fn(f) => Some(f), + _ => None, + }) + .map(|Fn { id, binder }| prove::FnDecl { + id: id.clone(), + binder: binder.map( + |FnBoundData { + input_tys, + output_ty, + where_clauses, + body: _, + }| prove::FnDeclBoundData { + input_tys, + output_ty, + where_clause: where_clauses.to_wcs(), + }, + ), + }) + .collect() + } } pub trait ToWcs { diff --git a/crates/formality-types/src/grammar/ty.rs b/crates/formality-types/src/grammar/ty.rs index 8284e10e..a74f0edb 100644 --- a/crates/formality-types/src/grammar/ty.rs +++ b/crates/formality-types/src/grammar/ty.rs @@ -83,6 +83,14 @@ impl Ty { } .upcast() } + + pub fn unit() -> Ty { + RigidTy { + name: RigidName::Tuple(0), + parameters: vec![], + } + .upcast() + } } impl UpcastFrom for Ty { diff --git a/crates/formality-types/src/grammar/ty/debug_impls.rs b/crates/formality-types/src/grammar/ty/debug_impls.rs index 3b45c435..dd4c535e 100644 --- a/crates/formality-types/src/grammar/ty/debug_impls.rs +++ b/crates/formality-types/src/grammar/ty/debug_impls.rs @@ -32,6 +32,25 @@ impl Debug for RigidTy { write!(f, "()") } } + RigidName::FnDef(name) => { + let parameters = PrettyParameters::new("<", ">", parameters); + write!(f, "{name:?}{parameters:?}",) + } + RigidName::FnPtr(arity) if parameters.len() == *arity + 1 => { + let len = parameters.len(); + if *arity != 0 { + write!( + f, + "{:?}", + PrettyParameters::new("(", ")", ¶meters[..len - 1]) + )?; + } else { + // PrettyParameters would skip the separators + // for 0 arity + write!(f, "()")?; + } + write!(f, "-> {:?}", parameters[len - 1]) + } _ => { write!(f, "{:?}{:?}", name, PrettyParameters::angle(parameters)) } diff --git a/crates/formality-types/src/grammar/ty/parse_impls.rs b/crates/formality-types/src/grammar/ty/parse_impls.rs index 119bd801..f0177f91 100644 --- a/crates/formality-types/src/grammar/ty/parse_impls.rs +++ b/crates/formality-types/src/grammar/ty/parse_impls.rs @@ -7,7 +7,7 @@ use formality_core::Upcast; use formality_core::{seq, Set}; use crate::grammar::{ - AdtId, AssociatedItemId, Bool, ConstData, RefKind, RigidName, Scalar, TraitId, + AdtId, AssociatedItemId, Bool, ConstData, FnId, RefKind, RigidName, Scalar, TraitId, }; use super::{AliasTy, AssociatedTyName, Lt, Parameter, ParameterKind, RigidTy, ScalarId, Ty}; @@ -70,6 +70,37 @@ impl CoreParse for RigidTy { parameters: types.upcast(), }) }); + + parser.parse_variant("Fn", Precedence::default(), |p| { + // parses 'fn name' as fn-def + // or 'fn(params) -> ty' as fn-ptr + p.expect_keyword("fn")?; + + if p.expect_char('(').is_ok() { + p.reject_custom_keywords(&["alias", "rigid", "predicate"])?; + let mut types: Vec = p.comma_nonterminal()?; + p.expect_char(')')?; + let name = RigidName::FnPtr(types.len()); + if p.expect_char('-').is_ok() { + p.expect_char('>')?; + let ret = p.nonterminal()?; + types.push(ret); + } else { + types.push(Ty::unit()); + } + Ok(RigidTy { + name, + parameters: types.upcast(), + }) + } else { + let name: FnId = p.nonterminal()?; + let parameters: Vec = parse_parameters(p)?; + Ok(RigidTy { + name: RigidName::FnDef(name), + parameters, + }) + } + }) }) } } diff --git a/crates/formality-types/src/lib.rs b/crates/formality-types/src/lib.rs index 89adb25c..bc85aa1f 100644 --- a/crates/formality-types/src/lib.rs +++ b/crates/formality-types/src/lib.rs @@ -12,6 +12,7 @@ formality_core::declare_language! { const BINDING_CLOSE = '>'; const KEYWORDS = [ "mut", + "fn", "struct", "enum", "union", diff --git a/src/test/coherence_orphan.rs b/src/test/coherence_orphan.rs index a4e1807b..d8209a50 100644 --- a/src/test/coherence_orphan.rs +++ b/src/test/coherence_orphan.rs @@ -19,24 +19,24 @@ fn neg_CoreTrait_for_CoreStruct_in_Foo() { orphan_check_neg(impl ! CoreTrait for CoreStruct {}) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because - judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + &decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) &name = (adt CoreStruct) the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) &a = CoreStruct the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [], [impl ! CoreTrait(CoreStruct)], [], [], [adt CoreStruct ], [], {}, {}) &goal.trait_id = CoreTrait"#]] ) } @@ -68,26 +68,26 @@ fn mirror_CoreStruct() { orphan_check(impl CoreTrait for ::Assoc { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because - judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + &decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) &name = (adt CoreStruct) the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) &a = CoreStruct the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait , trait Mirror ], [impl Mirror(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Mirror>::Assoc = ^ty0_0], [], [adt CoreStruct ], [], {}, {}) &goal.trait_id = CoreTrait"#]] ) } @@ -154,14 +154,14 @@ fn uncovered_T() { orphan_check(impl CoreTrait for ^ty0_0 { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(!ty_0, FooStruct))}, assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(!ty_0, FooStruct)), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because - judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `is_local_trait_ref { goal: CoreTrait(!ty_0, FooStruct), assumptions: {}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], {}, {FooStruct}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(^ty0_0, FooStruct)], [], [], [], [adt FooStruct ], [], {}, {FooStruct}) &goal.trait_id = CoreTrait"#]] ) } @@ -193,22 +193,22 @@ fn alias_to_unit() { orphan_check(impl CoreTrait for ::Assoc { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(::Assoc))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(::Assoc)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because - judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `is_local_trait_ref { goal: CoreTrait(::Assoc), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `is_local_parameter { goal: ::Assoc, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "local parameter" failed at step #2 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) }` failed at the following rule(s): + judgment `is_local_parameter { goal: (), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + &decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) &name = tuple(0) the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], {}, {FooStruct}) + decls = decls(222, [trait CoreTrait , trait Unit ], [impl Unit(^ty0_0), impl CoreTrait(::Assoc)], [], [alias <^ty0_0 as Unit>::Assoc = ()], [], [adt FooStruct ], [], {}, {FooStruct}) &goal.trait_id = CoreTrait"#]] ) } @@ -232,24 +232,24 @@ fn CoreTrait_for_CoreStruct_in_Foo() { orphan_check(impl CoreTrait for CoreStruct { }) Caused by: - judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ IsLocal(CoreTrait(CoreStruct))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ IsLocal(CoreTrait(CoreStruct)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "trait ref is local" failed at step #0 (src/file.rs:LL:CC) because - judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_trait_ref { goal: CoreTrait(CoreStruct), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "local parameter" failed at step #1 (src/file.rs:LL:CC) because - judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) }` failed at the following rule(s): + judgment `is_local_parameter { goal: CoreStruct, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) }` failed at the following rule(s): the rule "fundamental rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `is_fundamental(&decls, &name)` - &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + &decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) &name = (adt CoreStruct) the rule "local rigid type" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_adt_id(&a)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) &a = CoreStruct the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)` - decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], {}, {}) + decls = decls(222, [trait CoreTrait ], [impl CoreTrait(CoreStruct)], [], [], [], [adt CoreStruct ], [], {}, {}) &goal.trait_id = CoreTrait"#]] ) } diff --git a/src/test/consts.rs b/src/test/consts.rs index 09703dd1..37e45b8f 100644 --- a/src/test/consts.rs +++ b/src/test/consts.rs @@ -18,25 +18,25 @@ fn nonsense_rigid_const_bound() { Caused by: 0: prove_where_clauses_well_formed([type_of_const value(0, bool) is u32]) - 1: judgment `prove_wc_list { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + 1: judgment `prove_wc_list { goal: {u32 = bool, @ wf(u32), @ wf(const value(0, bool))}, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: u32 = bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + judgment had no applicable rules: `prove_via { goal: u32 = bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` the rule "eq" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: u32, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_eq { a: bool, b: u32, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "normalize-l" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_normalize { p: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "normalize-via-assumption" failed at step #1 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }` + judgment had no applicable rules: `prove_normalize_via { goal: bool, via: @ ConstHasType(value(0, bool) , u32), assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }` the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because - cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], {Foo}, {}) }`"#]] + cyclic proof attempt: `prove_eq { a: u32, b: bool, assumptions: {@ ConstHasType(value(0, bool) , u32)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(value(0, bool) , u32)}], [], [], [], [], [], [], {Foo}, {}) }`"#]] ) } @@ -74,9 +74,9 @@ fn mismatch() { check_trait_impl(impl Foo for u32 { }) Caused by: - judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Foo(u32, const value(42, u32))}, assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Foo(u32, const value(42, u32)), assumptions: {}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const value(42, u32))], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) @@ -131,15 +131,15 @@ fn generic_mismatch() { check_trait_impl(impl Foo for u32 where type_of_const ^const0_0 is u32 { }) Caused by: - judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Foo(u32, const !const_0)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Foo(u32, const !const_0), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "positive impl" failed at step #7 (src/file.rs:LL:CC) because - judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], bias: Soundness }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_after { constraints: Constraints { env: Env { variables: [!const_0, ?const_1], bias: Soundness }, known_true: true, substitution: {?const_1 => const !const_0} }, goal: {@ ConstHasType(?const_1 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {@ ConstHasType(!const_0 , bool)}, assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ ConstHasType(!const_0 , bool), assumptions: {@ ConstHasType(!const_0 , u32)}, env: Env { variables: [!const_0], bias: Soundness }, decls: decls(222, [trait Foo where {@ ConstHasType(^const0_1 , bool)}], [impl Foo(u32, const ^const0_0) where {@ ConstHasType(^const0_0 , u32)}], [], [], [], [], [], {Foo}, {}) }` failed at the following rule(s): the rule "const has ty" failed at step #0 (src/file.rs:LL:CC) because pattern `Some((_, const_ty))` did not match value `None` the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because diff --git a/src/test/functions.rs b/src/test/functions.rs index ac4eabda..2ccb156d 100644 --- a/src/test/functions.rs +++ b/src/test/functions.rs @@ -30,7 +30,7 @@ fn ok() { #[test] fn lifetime() { - crate::assert_err!( + crate::assert_ok!( // Test lifetimes on function [ crate Foo { @@ -39,13 +39,20 @@ fn lifetime() { } ] - [ /* TODO */ ] + expect_test::expect!["()"] + ) +} + +#[test] +fn wf() { + crate::assert_ok!( + [ + crate Foo { + fn foo() -> T { trusted } + fn bar(fn foo, fn(u32) -> (), fn(bool)) -> () { trusted } + } + ] - expect_test::expect![[r#" - judgment `prove_wc_list { goal: {@ wf(&!lt_0 !ty_1)}, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ wf(&!lt_0 !ty_1), assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s): - the rule "parameter well formed" failed at step #0 (src/file.rs:LL:CC) because - judgment had no applicable rules: `prove_wf { goal: &!lt_0 !ty_1, assumptions: {}, env: Env { variables: [!lt_0, !ty_1], bias: Soundness }, decls: decls(222, [], [], [], [], [], [], {}, {}) }`"#]] + expect_test::expect!["()"] ) } diff --git a/src/test/mod.rs b/src/test/mod.rs index 7a66c1be..9995c517 100644 --- a/src/test/mod.rs +++ b/src/test/mod.rs @@ -46,13 +46,13 @@ fn hello_world_fail() { Caused by: 0: prove_where_clauses_well_formed([!ty_2 : Bar ]) - 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + 1: judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo where {Bar(^ty0_1, ^ty0_0)}, trait Bar where {Baz(^ty0_1)}, trait Baz ], [], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]] ) @@ -121,15 +121,15 @@ fn basic_where_clauses_fail() { Caused by: 0: prove_where_clauses_well_formed([for u32 : A <^ty0_0>]) - 1: judgment `prove_wc_list { goal: {for @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + 1: judgment `prove_wc_list { goal: {for @ WellFormedTraitRef(A(u32, ^ty0_0))}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: for @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: for @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "forall" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because - judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "some" failed at step #0 (src/file.rs:LL:CC) because - judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): + judgment `prove_wc { goal: B(!ty_0), assumptions: {for A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A where {B(^ty0_1)}, trait B , trait WellFormed where {for A(u32, ^ty0_0)}], [], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s): the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because expression evaluated to an empty collection: `decls.trait_invariants()`"#]] )