You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, the vir module in which statements and expressions are defined has no notion of type parameters. To support Rust code that uses type parameters, Prusti uses a fragile regexp-based approach implemented in prusti-common/src/vir/ast/typaram.rs, plus a variety of hacks that can be found by searching for one of the following comments.
// FIXME; hideous monstrosity...
// FIXME oh dear...
// FIXME: the following fields serve a grotesque hack.
// FIXME: A hack. Replaces all generic types with their instantiations
To avoid the regular expressions and the hacks, we could extend vir::Expr and vir::Type to make them aware of type parameters and type substitutions.
The text was updated successfully, but these errors were encountered:
I think we should check whether it would be cleaner to have two layers of VIR: a generic VIR and monomorphic VIR that can be directly translated into Viper.
I'll close this. We no longer have the fragile regexp-base hack in the codebase (since #899 and a bunch of work by @vl0w), so generics are much more robust, although associated types might still take some more work (possible changes in #980). I also think having "first-class type parameters" in the VIR is the wrong decision: this is the job of the compiler. VIR poly thus should (and does not) have type parameters. @vakaras might be using them in the unsafe core proof VIR layers for dealing with lifetimes.
Currently, the
vir
module in which statements and expressions are defined has no notion of type parameters. To support Rust code that uses type parameters, Prusti uses a fragile regexp-based approach implemented inprusti-common/src/vir/ast/typaram.rs
, plus a variety of hacks that can be found by searching for one of the following comments.// FIXME; hideous monstrosity...
// FIXME oh dear...
// FIXME: the following fields serve a grotesque hack.
// FIXME: A hack. Replaces all generic types with their instantiations
To avoid the regular expressions and the hacks, we could extend
vir::Expr
andvir::Type
to make them aware of type parameters and type substitutions.The text was updated successfully, but these errors were encountered: