Lean backend [Part 1/3]

[clementblaudeau]

Lean Backend [Part 1/3] (experimental)

This PR provides the first step towards a fully functional Lean backend. It contains the infrastructure for exporting rust programs to Lean, with support for a starting subset of Rust expressions. It should be considered as experimental: unsupported features might not be documented and the actual Lean encoding is susceptible to change in the future.

Dependencies

This PR is based on #1525 (for printing infrastructure) and on #1508 (for reusing OCaml engine phases).

Context

In the current infrastructure, the Rust Engine is able to use the OCaml one (through the bridge of #1508) to apply the engine phases, and get back the output ast (as defined in ast.rs). Therefore, we can implement backends directly in Rust. Some generic infrastructure has been introduced in #1525 (support multiple backends) and #1528 (support for resugaring). This PR introduces a first instance of this infrastructure applied to Lean.

Details

• This PR uses the pretty crate to generate Doc, which can be seen as an extended string type that supports annotations. The Pretty trait is implemented for each part of the AST in lean.rs.
• The Lean backend can be called using cargo hax into lean

Examples

Example rust code

const FORTYTWO: usize = 42;

fn returns42() -> usize {
    FORTYTWO
}

fn add_two_numbers(x: usize, y: usize) -> usize {
    x + y
}

fn letBinding(x: usize, y: usize) -> usize {
    let useless = ();
    let result1 = x + y;
    let result2 = result1 + 2;
    result2 + 1
}

fn closure() -> i32 {
    let x = 41;
    let f = |y| y + x;
    f(1)
}

type usizeAlias = usize;

Lean extract

def FORTYTWO  : usize := 42

def returns42 (_ : hax_Tuple0) : usize := FORTYTWO

def add_two_numbers (x : usize) (y : usize) : usize := (hax_machine_int_add x y)

def letBinding (x : usize) (y : usize) : usize :=
  let useless := (.constr_hax_Tuple0 : hax_Tuple0);
  let result1 := (hax_machine_int_add x y);
  let result2 := (hax_machine_int_add result1 2);
  (hax_machine_int_add result2 1)

def closure (_ : hax_Tuple0) : i32 :=
  let x := 41;
  let f := (fun y => (hax_machine_int_add y x));
  (ops_function_Fn_call f
    (.constr_hax_Tuple1 {hax_Tuple1_Tuple0 := 1} : (hax_Tuple1 i32)))

abbrev usizeAlias := usize

Note that, without a Lean prelude, all the identifiers introduced by Hax are undefined: the code is syntactically valid but does not typecheck.

Goals

• Support basic rust expressions and types (functions definition and application, let binding, if-then-else)
• Provide a POC Lean Library for encoding of Rust/Hax primitives and intrinsics
• Demonstrate the Lean backend on some examples
• Add working examples to the CI

This PR does not provide support more advanced features (enums, traits, structures, generic arguments, etc).

[W95Psp]

LGTM, I only have a few comments :)

[franziskuskiefer]

Looks like we should get this in.
Just two nits/questions.

[W95Psp]

Let's merge!