Lean: Partially fix remove_e_assign rewrite

[Alasdair]

Fixes one of the broken cases for the remove_e_assign rewrite. See issue #1003 for details.

Adjusts the type system so it can handle nested type variables better, and check things like:

val f : nat -> unit

val main : unit -> unit

function main() =
  let i : nat = 0 in
  let j =
    let k : nat = i + 1 in
    k
  in
  let _ = f(j) in
  print_int("j = ", j)

where the constraint and type variable for k goes upwards to the variable j in the outer scope.

This kind of pattern is introduced by the rewrite.

[github-actions]

Test Results

   13 files     27 suites   0s ⏱️
  854 tests   854 ✅ 0 💤 0 ❌
3 716 runs  3 716 ✅ 0 💤 0 ❌

Results for commit 57a1570.

♻️ This comment has been updated with latest results.

[tobiasgrosser]

Thank you for this update. This is amazing. I just tested this. While it does not regress, it seemingly does not resolve the issue that have seen for the following code:

This patch still leads the following two warnings:

invalid reassignment, value has type
  Unit × Int × Int : Type
but is expected to have type
  Int × Int : Type
LeanRV64DLEAN.lean:105632:10
application type mismatch
  pure loop_vars
argument
  loop_vars
has type
  Int × Int : Type
but is expected to have type
  Unit × Int × Int : Type

in the following code:

def loop (_ : Unit) : SailM Unit := do
  let insns_per_tick := (plat_insns_per_tick ())
  let i : Int := 0
  let step_no : Int := 0
  let (u__3, i, step_no) ← (( do
    let mut loop_vars := (i, step_no)
    while (← (λ (i, step_no) => do (pure (not (← readReg htif_done)))) loop_vars) do
      let (i, step_no) := loop_vars
      loop_vars ← do
        let stepped ← do (step step_no)
        let step_no ← (( do
          if stepped
          then
            let step_no : Int := (step_no +i 1)
            let _ : Unit :=
              if (get_config_print_instr ())
              then (print_step ())
              else ()
            (cycle_count ())
            (pure step_no)
          else (pure step_no) ) : SailM Int )
        (pure ((← do
            if (← readReg htif_done)
            then
              let exit_val ← do (pure (BitVec.toNat (← readReg htif_exit_code)))
              if (BEq.beq exit_val 0)
              then (pure (print "SUCCESS"))
              else (pure (print_int "FAILURE: " exit_val))
            else
              let i := ((i +i 1) : Int)
              if (BEq.beq i insns_per_tick)
              then
                (tick_clock ())
                (tick_platform ())
                let i := (0 : Int)
                (pure ())
              else (pure ())), i, step_no))
    (pure loop_vars) ) : SailM (Unit × Int × Int) )

[tobiasgrosser]

I am currently still applying the following patch to risc-v, but if I drop it I get another well-known error:

diff --git a/model/riscv_step.sail b/model/riscv_step.sail
index 7a6d9450..dd38bdc3 100644
--- a/model/riscv_step.sail
+++ b/model/riscv_step.sail
@@ -118,6 +118,7 @@ function loop () : unit -> unit = {
         /* for now, we drive the platform i/o at every clock tick. */
         tick_platform();
         i = 0;
+	()
       }
     }
   }

Error without patch:

Type error:
riscv_step.sail:120.8-9:
120 |        i = 0;
    |        ^ checking function argument has type (unit, int, int)
    | Cannot modify immutable let-bound constant or enumeration constructor i
make[3]: *** [model/lean_RV64D_LEAN.lean] Error 1

[javra]

It fixes the snippet @Alasdair mentions above. On the RISC-V code I still get

error: ././././LeanRV64DLEAN.lean:105632:10: application type mismatch
  pure loop_vars
argument
  loop_vars
has type
  Int × Int : Type
but is expected to have type
  Unit × Int × Int : Type
error: ././././LeanRV64DLEAN.lean:105603:6: invalid reassignment, value has type
  Unit × Int × Int : Type
but is expected to have type
  Int × Int : Type

But @Alasdair also didn't claim it resolves the issue there.

[Alasdair]

It seems like sometimes we end up rewriting to a while statement into something of type unit * loop_vars and other times just loop_vars. I don't really understand the rationale for introducing the extra unit type right now, or the cases where it wouldn't be introduced.

[Alasdair]

Ah, it's not that it's an extra unit type, it's just that pretty_print_lean.ml only works for loops that update zero variables right now.

[javra]

We do have some test cases working for updating variables (loop.sail)

[Alasdair]

Looks like it has to do with purity of the loop in combination with updating variables. Adding a print statement inside the loop breaks it right now.

[Alasdair]

Might be fixed now... I have the tests I added simple_while, simple_while2, and simple_while3 all passing.

[tobiasgrosser]

I tried this, and it now works flawlessly. Let's get this in?