Rust Engine: Name Rendering: support `GlobalId` suffixes

[W95Psp]

Context

A GlobalId carries a possible suffix.

This is useful to create new names out of existing names.

This is typically used for:

• naming the pre and post-conditions in traits

  • A precondition for the method f will be embodied by a method whose name is derived from f directly, so that naming is consistent and non-ambiguous

• cast operators

  • Each enum comes with cast operators from the enum to its variant distriminators, e.g.

  enum Foo {
      A,
      B = 42,
      C
  }

  Generates:

  let anon_const_Foo_B__anon_const_0: isize =
    mk_isize 42
  
  let t_Foo_cast_to_repr (x: t_Foo)
      : isize =
    match x <: t_Foo with
    | Foo_A  -> mk_isize 0
    | Foo_B  ->
      anon_const_Foo_B__anon_const_0
    | Foo_C  ->
      anon_const_Foo_B__anon_const_0 +!
      mk_isize 1

Issue

The name rendering of the Rust engine ignores completely such suffixes.

cc @clementblaudeau, as we chatted about it

notion page

[clementblaudeau]

The Lean backend should use those to display pre/post conditions