feat(lean): Add support for namespaces

[clementblaudeau]

Overview

This PR uses the module mechanism of the rust-engine to gather definitions in Lean namespaces, shortening their names. To do so, a refactor of global ids have been made, adding a proper FreshModule case. The logic for rendering those is not done yet (see #1779), as it will only be required by F*-like bundling in the rust engine (which might only come when porting the F* backend).

Example

• Rust

// Simple trait
mod basic {
    trait T1 {
        fn f1(&self) -> usize;
        fn f2(&self, other: &Self) -> usize;
    }

    // Simple Impl
    struct S;

    impl T1 for S {
        fn f1(&self) -> usize {
            42
        }

        fn f2(&self, other: &Self) -> usize {
            43
        }
    }

    // Simple ImplExpr
    fn f<T: T1>(x: T) -> usize {
        x.f1() + x.f2(&x)
    }
}

• Lean (without namespacing)

class Playground.Basic.T1 (Self : Type) where
  f1 : (Self -> RustM usize)
  f2 : (Self -> Self -> RustM usize)

structure Playground.Basic.S where


instance Playground.Basic.Impl : Playground.Basic.T1 Playground.Basic.S where
  f1 (self : Playground.Basic.S) := do (pure (42 : usize))
  f2 (self : Playground.Basic.S) (other : Playground.Basic.S) := do
    (pure (43 : usize))

def Playground.Basic.f
  (T : Type) [(Playground.Basic.T1 T)] (x : T)
  : RustM usize
  := do
  ((← (Playground.Basic.T1.f1 x)) +? (← (Playground.Basic.T1.f2 x x)))

• Lean with namespacing

namespace Playground.Basic

class T1 (Self : Type) where
  f1 : (Self -> RustM usize)
  f2 : (Self -> Self -> RustM usize)

structure S where
  -- no fields

instance Impl : T1 S where
  f1 (self : S) := do (pure (42 : usize))
  f2 (self : S) (other : S) := do (pure (43 : usize))

def f (T : Type) [(T1 T)] (x : T) : RustM usize := do
  ((← (T1.f1 x)) +? (← (T1.f2 x x)))

end Playground.Basic

[W95Psp]

Thanks, that generally looks good to me, though I have a few remarks :)

[W95Psp]

Maybe change to "Fresh modules are not implemented yet in the Rust engine" or something in those lines?
See my comment in #1779, it's not so much F* specific

[W95Psp]

Let's implement https://doc.rust-lang.org/std/fmt/trait.Debug.html instead of creating a new trait

[W95Psp]

This should be a phase, no?

[W95Psp]

We should pull that out of the backend trait: this method should not be overridable IMO 🤔

[W95Psp]

Ah, that was not part of the trait?

[W95Psp]

Makes sense, this should be the same logic for every backend

[W95Psp]

Let's not bring an extra dependency for such a small utility function, just add it to as an helper somewhere (e.g. in a helper.rs file)

[W95Psp]

(sorry, I meant request changes, not approving 😓)