Library multi_add_s_s_u_prg

Require Import machine_int.
Import MachineInt.
Require Import mips_cmd.
Import expr_m.
Require Import pick_sign_prg multi_lt_prg multi_add_u_u_prg multi_sub_u_u_prg.
Require Import multi_negate_prg copy_s_u_prg multi_is_zero_u_prg abs_prg.
Require Import multi_zero_s_prg copy_s_s_prg.

Local Open Scope mips_cmd_scope.

Definition multi_add_s_s_u0 rk rz rx ry a0 a1 a2 a3 a4 ret X Z : while.cmd :=
   lw Z four16 rz ;
   lw X four16 rx ;
   pick_sign rx a0 a1 ;
   If_bgez a1 Then
     If_beq a1, r0 Then
       copy_s_u rk rz ry a0 a1 a2 a3 ;
       addiu a3 r0 zero16
     Else
       multi_add_u_u rk a1 ry X Z a2 a3 a4 ;
       mflo a3;
       sw rk zero16 rz
   Else
   (multi_lt rk ry X a0 a1 ret a2 a3 a4 ;
    If_beq ret, r0 Then
      If_beq a2, r0 Then
        multi_zero_s rz ;
        addiu a3 r0 zero16
      Else
        multi_sub_u_u rk ry X Z a0 a1 a2 a3 a4 ret;
        sw rk zero16 rz
    Else
     (multi_sub_u_u rk X ry Z a0 a1 ret a3 a2 a4;
      subu a0 r0 rk ;
      sw a0 zero16 rz
     )).

Definition multi_add_s_s_u rk rz rx ry a0 a1 a2 a3 a4 ret X Z :=
  multi_is_zero_u rk ry a0 a1 a2 ;
  If_bne a2 , r0 Then
    copy_s_s rk rz rx a0 a1 a2 a3 a4 ;
    addiu a3 r0 zero16
  Else
    multi_add_s_s_u0 rk rz rx ry a0 a1 a2 a3 a4 ret X Z.