Lean backend [M2] - 3/3 - Resugarings

[clementblaudeau]

This PR is a follow-up of #1590. It uses the visitors of #1585 to implement resugarings, i.e. passes over the AST that replace certain patterns with special resugared nodes, allowing for a special treatment by the backend.
The Lean extracted code is made much more readable and close to the Rust code. This PR only defines resugaring for some binary arithmetic operations, as a proof of concept.

Example

For instance, the barrett extracted code goes from

def barrett_reduce (value : i32) : Result i32 := do
  let (t : i64) ← (← hax_machine_int_mul
    (← convert_From_from value)
      BARRETT_MULTIPLIER);
  let (t : i64) ← (← hax_machine_int_add t (← hax_machine_int_shr BARRETT_R 1));
  let (quotient : i64) ← (← hax_machine_int_shr t BARRETT_SHIFT);
  let (quotient : i32) ← (← hax_cast_op quotient);
  let (sub : i32) ← (← hax_machine_int_mul quotient FIELD_MODULUS);
  let (_ : hax_Tuple0) ← hax_Tuple0; (← hax_machine_int_sub value sub)

to

def barrett_reduce (value : i32) : Result i32 := do
  let (t : i64) ← ((← convert_From_from value) *? BARRETT_MULTIPLIER);
  let (t : i64) ← (t +? (BARRETT_R >>>? 1));
  let (quotient : i64) ← (t >>>? BARRETT_SHIFT);
  let (quotient : i32) ← (← hax_cast_op quotient);
  let (sub : i32) ← (quotient *? FIELD_MODULUS); (value -? sub)

[W95Psp]

Thanks, this looks OK to me.
The if/else if chain is a pity, we should probably offer a nicer API in the BinOp resugaring.
But let's address that later.

[franziskuskiefer]

lgtm, just a few questions and nits