[Lean Backend] Add basic support for traits

[clementblaudeau]

This PR adds support for traits and implementations, and makes the output style more uniform. In a nutshell, Rust traits are represented as Lean classes, while Rust impl are Lean instances. The Lean code relies on the typeclass inference of Lean.

Overview

// 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)
    }
}

class Lean_tests.Traits.Basic.T1 (Self : Type) where
  f1 : Self -> Result usize
  f2 : Self -> Self -> Result usize

structure Lean_tests.Traits.Basic.S where

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

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

Details

• Super trait bounds are represented as extra fields

Rust

trait Test<T: T1>: T2 {
    fn f_test(&self, x: &T) -> usize;
}

Lean

class Lean_tests.Traits.Bounds.Test (Self : Type) (T : Type) where
  [_constr_8040238289193487104 : (Lean_tests.Traits.Bounds.T2 Self)]
  [_constr_7570495343596639253 : (Lean_tests.Traits.Bounds.T1 T)]
  f_test : Self -> T -> Result usize

• The support for associated types is restricted to types defined within the current trait

Rust

mod associated_types {
    trait T1 {
        type T;
        fn f(&self, x: Self::T) -> Self::T;
    }

    trait T2 {
        type T: T1;
        fn f(&self, x: Self::T) -> usize;
    }

    trait Foo<T> {}
    trait Bar {}

    trait T3 {
        type T: Foo<()>;
        type Tp<T: Bar>: Foo<T>;
        fn f<A: Bar>(&self, x: Self::T, y: Self::Tp<A>) -> usize;
    }
}

Lean

class Lean_tests.Traits.Associated_types.Foo (Self : Type) (T : Type) where


class Lean_tests.Traits.Associated_types.Bar (Self : Type) where


class Lean_tests.Traits.Associated_types.T1 (Self : Type) where
  T : Type
  f : Self -> T -> Result T

class Lean_tests.Traits.Associated_types.T3 (Self : Type) where
  T : Type
  [_constr_13086648656846024831 :
    (Lean_tests.Traits.Associated_types.Foo T Rust_primitives.Hax.Tuple0)]
  Tp : Type
  [_constr_15450263461214744089 : (Lean_tests.Traits.Associated_types.Foo Tp T)]
  f (A : Type) [(Lean_tests.Traits.Associated_types.Bar A)] :
    Self -> T -> Tp -> Result usize

class Lean_tests.Traits.Associated_types.T2 (Self : Type) where
  T : Type
  [_constr_18277713886489441014 : (Lean_tests.Traits.Associated_types.T1 T)]
  f : Self -> T -> Result usize

[maximebuyse]

I made a first pass and have some comments. The resulting code looks nice, it's great to have support for traits!

[maximebuyse]

General comment about the description:

The support for associated types is restricted to types defined within the current trait

The example that comes after is supposed to show what is not supported? I think what is also interesting here is to try to define instances for these traits. I tried to do so and check the result with the F* backend, but I run into #1046. Anyway from the output you show it seems that the Lean support is the roughly the same as F* in this case.

[clementblaudeau]

The example was to show the supported part (access only associated types defined within the same trait). I've added more test (and the missing support for types fields in impls) in 937ec0d.

[clementblaudeau]

I've rebased on main.