Lines Matching defs:sh
1258 fun DecodeShift sh = (Cast.natToShiftType o BitsN.toNat) sh;
1280 fun ExtendValue N (value,(ty,sh)) =
1293 val len = Nat.min(len,Nat.-(BitsN.size(BitsN.BV(0x0,N)),sh))
1296 (Bitstring.<<(Bitstring.bits(Nat.-(len,1),0) value,sh),unsigned)
1299 fun ExtendReg N (reg,(ty,sh)) = ExtendValue N (X N reg,(ty,sh));
5982 AddSubShiftedRegister''32(_,(opc,(s,(sh,(rm,(imm6,(rn,rd))))))) =>
5988 BitsN.B(0xB,5),BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
5990 | AddSubShiftedRegister''64(_,(opc,(s,(sh,(rm,(imm6,(rn,rd))))))) =>
5994 BitsN.B(0xB,5),BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
6043 (sf,(opc,(invert,(s,(sh,(imm,(rm,(rn,rd)))))))) =>
6053 BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
6059 (sf,(opc,(invert,(s,(sh,(imm,(rm,(rn,rd)))))))) =>
6069 BitsN.fromNat(Cast.ShiftTypeToNat sh,2),
6088 | Shift''32(_,(sh,(rm,(rn,rd)))) =>
6092 BitsN.fromNat(Cast.ShiftTypeToNat sh,2),rn,rd])
6093 | Shift''64(_,(sh,(rm,(rn,rd)))) =>
6097 BitsN.fromNat(Cast.ShiftTypeToNat sh,2),rn,rd])
7058 fun p_shift_amount (sh,s) =
7060 Option.SOME v => Option.SOME(sh,v)
7639 Option.SOME(sh,amount) =>
7650 (setflags,(sh,(xm,(imm6,(xn,xd)))))))))
7656 (setflags,(sh,(wm,(imm6,(wn,wd)))))))))
7658 if sh = ShiftType_LSL
7685 (Option.SOME(true,(xd,(xn,xm))),Option.SOME(sh,amount)) =>
7689 (opc,(invert,(setflags,(sh,(amount,(xm,(xn,xd))))))))))
7690 | (Option.SOME(false,(wd,(wn,wm))),Option.SOME(sh,amount)) =>
7694 (opc,(invert,(setflags,(sh,(amount,(wm,(wn,wd))))))))))
7735 (Option.SOME(true,imm16),Option.SOME(sh,amount))) =>
8680 fun s_shift_amount (shift_type,sh) =
8681 if (sh = 0) andalso (shift_type = ShiftType_LSL)
8683 else String.concat[", ",s_shift_type shift_type," ",s_nat sh];
8895 val sh = Nat.*(BitsN.toNat hw,16)
8903 (BitsN.<<(BitsN.fromNat(BitsN.toNat imm,64),sh))))
8914 (BitsN.fromNat(BitsN.toNat imm,64),sh)))
8918 (BitsN.fromNat(BitsN.toNat imm,32),sh)))))
8924 else ", lsl " ^ (s_nat sh)])
8929 val sh = Nat.*(BitsN.toNat hw,16)
8937 (BitsN.<<(BitsN.fromNat(BitsN.toNat imm,64),sh))))
8948 (BitsN.fromNat(BitsN.toNat imm,64),sh)))
8952 (BitsN.fromNat(BitsN.toNat imm,32),sh)))))
8958 else ", lsl " ^ (s_nat sh)])