Mono Name-Matcher

[ssyram]

This PR enhanced the name-matcher mechanism to work also for the mono codes. The key is that when the newly added match_mono switch is on, the program now tries to extract out the generics stored within the name and match against this generics. This is a key component to ensure the migration to mono LLBC as in AeneasVerif/eurydice#275 .

Notable issue: now there is a discrepency between the parsers in Rust and OCaml. More concretely, the string used in Eurydice, that: core::slice::index::{core::ops::index::Index<[@T], @I>}::index<'_, @, core::ops::range::Range<usize>, [@]> cannot be recognised by Pattern::parse in Rust.

[Nadrieril]

For the name matcher tests, could you please use the existing rust-name-matcher-tests.rs and ml-name-matcher-tests.rs as much as possible instead of rolling your own logic.

Is there any reason to set match_mono to false? I think having it always true is what users would expect.

[ssyram]

I don't know about why mono did not work. I assumed this might be some dedicated design... So in order not to break the existing usage, I kept the existing codes using false while only in Eurydice use true.

For the test, will try.

[Nadrieril]

That wasn't a design choice, just something not yet implemented. Please remove that option and make the name matchers always work wirh monomorphized names.

[ssyram]

Yes, will do.

[ssyram]

Should have fixed all stuff. Also, I was surprised that in the ML version, the wildcard pattern was not supported. New example added for this case and the wildcard pattern is now supported.