diff --git a/test/lean/SailTinyArm.expected.lean b/test/lean/SailTinyArm.expected.lean index b1dbd3d47..b479f1f97 100644 --- a/test/lean/SailTinyArm.expected.lean +++ b/test/lean/SailTinyArm.expected.lean @@ -515,7 +515,7 @@ def _update_S2PIRType_bits (v : (BitVec 64)) (x : (BitVec 64)) : (BitVec 64) := (Sail.BitVec.updateSubrange v (HSub.hSub 64 1) 0 x) def _set_MAIRType_bits (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 64)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_bits r v) def _get_S1PIRType_bits (v : (BitVec 64)) : (BitVec 64) := @@ -525,11 +525,11 @@ def _get_S2PIRType_bits (v : (BitVec 64)) : (BitVec 64) := (Sail.BitVec.extractLsb v (HSub.hSub 64 1) 0) def _set_S1PIRType_bits (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 64)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_bits r v) def _set_S2PIRType_bits (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 64)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_bits r v) def _get_MAIRType_Attr0 (v : (BitVec 64)) : (BitVec 8) := @@ -539,7 +539,7 @@ def _update_MAIRType_Attr0 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 7 0 x) def _set_MAIRType_Attr0 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr0 r v) def _get_MAIRType_Attr1 (v : (BitVec 64)) : (BitVec 8) := @@ -549,7 +549,7 @@ def _update_MAIRType_Attr1 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 15 8 x) def _set_MAIRType_Attr1 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr1 r v) def _get_MAIRType_Attr2 (v : (BitVec 64)) : (BitVec 8) := @@ -559,7 +559,7 @@ def _update_MAIRType_Attr2 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 23 16 x) def _set_MAIRType_Attr2 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr2 r v) def _get_MAIRType_Attr3 (v : (BitVec 64)) : (BitVec 8) := @@ -569,7 +569,7 @@ def _update_MAIRType_Attr3 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 31 24 x) def _set_MAIRType_Attr3 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr3 r v) def _get_MAIRType_Attr4 (v : (BitVec 64)) : (BitVec 8) := @@ -579,7 +579,7 @@ def _update_MAIRType_Attr4 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 39 32 x) def _set_MAIRType_Attr4 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr4 r v) def _get_MAIRType_Attr5 (v : (BitVec 64)) : (BitVec 8) := @@ -589,7 +589,7 @@ def _update_MAIRType_Attr5 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 47 40 x) def _set_MAIRType_Attr5 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr5 r v) def _get_MAIRType_Attr6 (v : (BitVec 64)) : (BitVec 8) := @@ -599,7 +599,7 @@ def _update_MAIRType_Attr6 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 55 48 x) def _set_MAIRType_Attr6 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr6 r v) def _get_MAIRType_Attr7 (v : (BitVec 64)) : (BitVec 8) := @@ -609,7 +609,7 @@ def _update_MAIRType_Attr7 (v : (BitVec 64)) (x : (BitVec 8)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 63 56 x) def _set_MAIRType_Attr7 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_MAIRType_Attr7 r v) def undefined_S1PIRType (_ : Unit) : SailM (BitVec 64) := do @@ -628,14 +628,14 @@ def _update_S2PIRType_Perm0 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 3 0 x) def _set_S1PIRType_Perm0 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm0 r v) def _get_S2PIRType_Perm0 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 3 0) def _set_S2PIRType_Perm0 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm0 r v) def _get_S1PIRType_Perm1 (v : (BitVec 64)) : (BitVec 4) := @@ -648,14 +648,14 @@ def _update_S2PIRType_Perm1 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 7 4 x) def _set_S1PIRType_Perm1 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm1 r v) def _get_S2PIRType_Perm1 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 7 4) def _set_S2PIRType_Perm1 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm1 r v) def _get_S1PIRType_Perm10 (v : (BitVec 64)) : (BitVec 4) := @@ -668,14 +668,14 @@ def _update_S2PIRType_Perm10 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 43 40 x) def _set_S1PIRType_Perm10 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm10 r v) def _get_S2PIRType_Perm10 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 43 40) def _set_S2PIRType_Perm10 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm10 r v) def _get_S1PIRType_Perm11 (v : (BitVec 64)) : (BitVec 4) := @@ -688,14 +688,14 @@ def _update_S2PIRType_Perm11 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 47 44 x) def _set_S1PIRType_Perm11 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm11 r v) def _get_S2PIRType_Perm11 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 47 44) def _set_S2PIRType_Perm11 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm11 r v) def _get_S1PIRType_Perm12 (v : (BitVec 64)) : (BitVec 4) := @@ -708,14 +708,14 @@ def _update_S2PIRType_Perm12 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 51 48 x) def _set_S1PIRType_Perm12 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm12 r v) def _get_S2PIRType_Perm12 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 51 48) def _set_S2PIRType_Perm12 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm12 r v) def _get_S1PIRType_Perm13 (v : (BitVec 64)) : (BitVec 4) := @@ -728,14 +728,14 @@ def _update_S2PIRType_Perm13 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 55 52 x) def _set_S1PIRType_Perm13 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm13 r v) def _get_S2PIRType_Perm13 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 55 52) def _set_S2PIRType_Perm13 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm13 r v) def _get_S1PIRType_Perm14 (v : (BitVec 64)) : (BitVec 4) := @@ -748,14 +748,14 @@ def _update_S2PIRType_Perm14 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 59 56 x) def _set_S1PIRType_Perm14 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm14 r v) def _get_S2PIRType_Perm14 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 59 56) def _set_S2PIRType_Perm14 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm14 r v) def _get_S1PIRType_Perm15 (v : (BitVec 64)) : (BitVec 4) := @@ -768,14 +768,14 @@ def _update_S2PIRType_Perm15 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 63 60 x) def _set_S1PIRType_Perm15 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm15 r v) def _get_S2PIRType_Perm15 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 63 60) def _set_S2PIRType_Perm15 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm15 r v) def _get_S1PIRType_Perm2 (v : (BitVec 64)) : (BitVec 4) := @@ -788,14 +788,14 @@ def _update_S2PIRType_Perm2 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 11 8 x) def _set_S1PIRType_Perm2 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm2 r v) def _get_S2PIRType_Perm2 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 11 8) def _set_S2PIRType_Perm2 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm2 r v) def _get_S1PIRType_Perm3 (v : (BitVec 64)) : (BitVec 4) := @@ -808,14 +808,14 @@ def _update_S2PIRType_Perm3 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 15 12 x) def _set_S1PIRType_Perm3 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm3 r v) def _get_S2PIRType_Perm3 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 15 12) def _set_S2PIRType_Perm3 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm3 r v) def _get_S1PIRType_Perm4 (v : (BitVec 64)) : (BitVec 4) := @@ -828,14 +828,14 @@ def _update_S2PIRType_Perm4 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 19 16 x) def _set_S1PIRType_Perm4 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm4 r v) def _get_S2PIRType_Perm4 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 19 16) def _set_S2PIRType_Perm4 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm4 r v) def _get_S1PIRType_Perm5 (v : (BitVec 64)) : (BitVec 4) := @@ -848,14 +848,14 @@ def _update_S2PIRType_Perm5 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 23 20 x) def _set_S1PIRType_Perm5 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm5 r v) def _get_S2PIRType_Perm5 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 23 20) def _set_S2PIRType_Perm5 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm5 r v) def _get_S1PIRType_Perm6 (v : (BitVec 64)) : (BitVec 4) := @@ -868,14 +868,14 @@ def _update_S2PIRType_Perm6 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 27 24 x) def _set_S1PIRType_Perm6 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm6 r v) def _get_S2PIRType_Perm6 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 27 24) def _set_S2PIRType_Perm6 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm6 r v) def _get_S1PIRType_Perm7 (v : (BitVec 64)) : (BitVec 4) := @@ -888,14 +888,14 @@ def _update_S2PIRType_Perm7 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 31 28 x) def _set_S1PIRType_Perm7 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm7 r v) def _get_S2PIRType_Perm7 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 31 28) def _set_S2PIRType_Perm7 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm7 r v) def _get_S1PIRType_Perm8 (v : (BitVec 64)) : (BitVec 4) := @@ -908,14 +908,14 @@ def _update_S2PIRType_Perm8 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 35 32 x) def _set_S1PIRType_Perm8 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm8 r v) def _get_S2PIRType_Perm8 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 35 32) def _set_S2PIRType_Perm8 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm8 r v) def _get_S1PIRType_Perm9 (v : (BitVec 64)) : (BitVec 4) := @@ -928,14 +928,14 @@ def _update_S2PIRType_Perm9 (v : (BitVec 64)) (x : (BitVec 4)) : (BitVec 64) := (Sail.BitVec.updateSubrange v 39 36 x) def _set_S1PIRType_Perm9 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S1PIRType_Perm9 r v) def _get_S2PIRType_Perm9 (v : (BitVec 64)) : (BitVec 4) := (Sail.BitVec.extractLsb v 39 36) def _set_S2PIRType_Perm9 (r_ref : (RegisterRef RegisterType (BitVec 64))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_S2PIRType_Perm9 r v) def undefined_S2PIRType (_ : Unit) : SailM (BitVec 64) := do @@ -1785,11 +1785,11 @@ def wMem_Addr (addr : (BitVec 64)) : Unit := ∧ m ≤ 31 -/ def execute_StoreRegister (t : Nat) (n : Nat) (m : Nat) : SailM Unit := do writeReg _PC (BitVec.addInt (← readReg _PC) 4) - let base_addr ← do (rX n) - let offset ← do (rX m) + let base_addr ← (rX n) + let offset ← (rX m) let addr := (HAdd.hAdd base_addr offset) let _ := (wMem_Addr addr) - let data ← do (rX t) + let data ← (rX t) (wMem addr data) def rMem (addr : (BitVec 64)) : SailM (BitVec 64) := do @@ -1810,17 +1810,17 @@ def rMem (addr : (BitVec 64)) : SailM (BitVec 64) := do ∧ m ≤ 31 -/ def execute_LoadRegister (t : Nat) (n : Nat) (m : Nat) : SailM Unit := do writeReg _PC (BitVec.addInt (← readReg _PC) 4) - let base_addr ← do (rX n) - let offset ← do (rX m) + let base_addr ← (rX n) + let offset ← (rX m) let addr := (HAdd.hAdd base_addr offset) - let data ← do (rMem addr) + let data ← (rMem addr) (wX t data) /-- Type quantifiers: m : Nat, n : Nat, d : Nat, 0 ≤ d ∧ d ≤ 31, 0 ≤ n ∧ n ≤ 31, 0 ≤ m ∧ m ≤ 31 -/ def execute_ExclusiveOr (d : Nat) (n : Nat) (m : Nat) : SailM Unit := do - let operand1 ← do (rX n) - let operand2 ← do (rX m) + let operand1 ← (rX n) + let operand2 ← (rX m) (wX d (HXor.hXor operand1 operand2)) def dataMemoryBarrier (_ : Unit) : SailM Unit := do @@ -1835,9 +1835,9 @@ def execute_DataMemoryBarrier (_ : Unit) : SailM Unit := do /-- Type quantifiers: t : Nat, 0 ≤ t ∧ t ≤ 31 -/ def execute_CompareAndBranch (t : Nat) (offset : (BitVec 64)) : SailM Unit := do - let operand ← do (rX t) + let operand ← (rX t) if (Eq operand (0x0000000000000000 : (BitVec 64))) - then let base ← do (rPC ()) + then let base ← (rPC ()) let addr := (HAdd.hAdd base offset) (wPC addr) else writeReg _PC (BitVec.addInt (← readReg _PC) 4) @@ -1893,7 +1893,7 @@ def iFetch (addr : (BitVec 64)) : SailM (BitVec 32) := do | Err _ => throw Error.Exit def fetch_and_execute (_ : Unit) : SailM Unit := do - let machineCode ← do (iFetch (← readReg _PC)) + let machineCode ← (iFetch (← readReg _PC)) let instr := (decode machineCode) match instr with | some instr => (execute instr) diff --git a/test/lean/bitfield.expected.lean b/test/lean/bitfield.expected.lean index bbfef3860..9463dd3bf 100644 --- a/test/lean/bitfield.expected.lean +++ b/test/lean/bitfield.expected.lean @@ -31,7 +31,7 @@ def _update_cr_type_bits (v : (BitVec 8)) (x : (BitVec 8)) : (BitVec 8) := (Sail.BitVec.updateSubrange v (HSub.hSub 8 1) 0 x) def _set_cr_type_bits (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 8)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_cr_type_bits r v) def _get_cr_type_CR0 (v : (BitVec 8)) : (BitVec 4) := @@ -41,7 +41,7 @@ def _update_cr_type_CR0 (v : (BitVec 8)) (x : (BitVec 4)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 7 4 x) def _set_cr_type_CR0 (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 4)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_cr_type_CR0 r v) def _get_cr_type_CR1 (v : (BitVec 8)) : (BitVec 2) := @@ -51,7 +51,7 @@ def _update_cr_type_CR1 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 3 2 x) def _set_cr_type_CR1 (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 2)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_cr_type_CR1 r v) def _get_cr_type_CR3 (v : (BitVec 8)) : (BitVec 2) := @@ -61,7 +61,7 @@ def _update_cr_type_CR3 (v : (BitVec 8)) (x : (BitVec 2)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 1 0 x) def _set_cr_type_CR3 (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 2)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_cr_type_CR3 r v) def _get_cr_type_GT (v : (BitVec 8)) : (BitVec 1) := @@ -71,7 +71,7 @@ def _update_cr_type_GT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 6 6 x) def _set_cr_type_GT (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 1)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_cr_type_GT r v) def _get_cr_type_LT (v : (BitVec 8)) : (BitVec 1) := @@ -81,7 +81,7 @@ def _update_cr_type_LT (v : (BitVec 8)) (x : (BitVec 1)) : (BitVec 8) := (Sail.BitVec.updateSubrange v 7 7 x) def _set_cr_type_LT (r_ref : (RegisterRef RegisterType (BitVec 8))) (v : (BitVec 1)) : SailM Unit := do - let r ← do (reg_deref r_ref) + let r ← (reg_deref r_ref) writeRegRef r_ref (_update_cr_type_LT r v) def initialize_registers (_ : Unit) : SailM Unit := do diff --git a/test/lean/ite.expected.lean b/test/lean/ite.expected.lean index a15cee9c7..7ef10e347 100644 --- a/test/lean/ite.expected.lean +++ b/test/lean/ite.expected.lean @@ -31,8 +31,8 @@ def elif (n : Nat) : (BitVec 1) := /-- Type quantifiers: n : Nat, 0 ≤ n -/ def monadic_in_out (n : Nat) : SailM Nat := do if (← readReg B) - then writeReg R n - else (pure ()) + then writeReg R n + else (pure ()) readReg R /-- Type quantifiers: n : Nat, 0 ≤ n -/ diff --git a/test/lean/match.expected.lean b/test/lean/match.expected.lean index 906b7cdff..c793a4115 100644 --- a/test/lean/match.expected.lean +++ b/test/lean/match.expected.lean @@ -61,7 +61,7 @@ def match_let (x : E) (y : Int) : SailM Int := do match x with | A => let x := (HAdd.hAdd y y) - let z ← do (pure (HAdd.hAdd (HAdd.hAdd y y) (← (undefined_int ())))) + let z ← (pure (HAdd.hAdd (HAdd.hAdd y y) (← (undefined_int ())))) (pure (HAdd.hAdd z x)) | B => (pure 42) | C => (pure 23)