Encode domains and axioms for traits#52
Encode domains and axioms for traits#52zgrannan wants to merge 14 commits intoAurel300:rewrite-2023from
Conversation
zgrannan
changed the title
|
relevant diff: |
| traits::ImplSource::UserDefined(ud) => { | ||
| self.deps.require_dep::<UserDefinedTraitImplEnc>(ud.impl_def_id).unwrap(); | ||
| } | ||
| traits::ImplSource::Param(_) => {} |
There was a problem hiding this comment.
I'm a little surprised to see that there's nothing generated for trait bounds on parameters? Don't we need to generate some opaque value so that we can instantiate trait axioms?
There was a problem hiding this comment.
I'm afraid I don't quite understand this comment. I think what the ImplSource::Param case corresponds to is e.g. the call to g(x) in :
fn f<T: Clone + Eq>(x: T) {
g(x)
}
fn g<T: Clone>(t: T) {
}where the call is allowed because the type of x must implement Clone in f. So we don't need to add any additional Viper axioms because the precondition implements_Clone(typeof(x)) in the encoding of f will satisfy the corresponding precondition in g.
BTW in case it's not clear this would be different for a call of e.g. g(1) somewhere in the code; we would want to ensure the axiom asserting implements_Clone(s_u32_type()) is generated.
There was a problem hiding this comment.
ah yea, i didn't catch that this was for the bounds of a called function, where indeed we don't want to generate axioms.
2 participants
Encodes domains for traits, uninterpreted functions (i.e. to check if a type implements a trait), and axioms based on trait impls; #51 should be merged first.