Cannot run eliminate_symbol after discriminate
Im forwarding an issue from David Ewert which I received over mail:
I have been trying to get Why3 to completely monomorphise all of the polymorphic logic functions and propositions, in order to avoid the "encoding_smt" transformation. I've found that the "discriminate" transformation pretty much does what I want (especially when setting meta "select_inst_default" "all", meta "select_lskept_default" "all"). Unfortunately, it still keeps the polymorphic functions and propositions (which I don't want) after introducing the monomorphic ones. I also tried running "eliminate_symbol" after "discriminate" setting "ls:eliminate" for some of the sequence functions hoping this would eliminate the polymorphic versions, but this gave the error: "Failure in transformation eliminate_symbol Ident map is not yet declared". I think that it would be useful for Why3 to have a transformation that runs "discriminate" and then eliminates all polymorphic symbols or at least to allow "eliminate_symbol" to work after "discriminate" (although this seems like more of a hack)
Note: He is working with Creusot, so his immediate concern may be solved by !680 (merged), but this still seems like a valid bug report.